Add documentation

debugging_notes.txt

+
+# April 20, 2022
+
+iteration: 199
+candidate: ITE(1.0*x_2 + z_1 <= -0.0088842, False, 1.0*x_1 + 1.0*x_2 + z_0 + z_1 > -0.5997313)
+
+
+
 debugging notes: (high level )
 
 Gurobi cannot express < , >  (strickly less than or strickly greater than)

dtree_synth.py

@@ -45,7 +45,7 @@ def test_synth_dtree():
     #  0.0 <= x <= 30.0 and -1.0 <= y <= 0.9 and 0.2 <= theta <= 0.22
     teacher.set_old_state_bound(lb=[0.0, -1.0, 0.2], ub=[30.0, -0.9, 0.22])
 
-    synth_dtree(positive_examples, teacher, num_max_iterations=10)
+    synth_dtree(positive_examples, teacher, num_max_iterations=2000)
 
 
 def synth_dtree(positive_examples, teacher, num_max_iterations: int = 10):
@@ -55,6 +55,10 @@ def synth_dtree(positive_examples, teacher, num_max_iterations: int = 10):
     a_mat_0 = np.array([[0., -1., 0.],
                         [0., 0., -1.]])
     b_vec_0 = np.zeros(2)
+    # Let z = [z_0, z_1] = [d, psi]; x = [x_0, x_1, x_2] = [x, y, theta]
+    # a_mat_0 @ [x, y, theta] + b_vec_0 = [-y, -theta]
+    # z - (a_mat_0 @ x + b_vec_0) = [d, psi] - [-y, -theta] = [d+y, psi+theta] defined as [fvar0_A0, fvar1_A0]
+
     learner.set_grammar([(a_mat_0, b_vec_0)])
     learner.add_positive_examples(*positive_examples)