diff --git a/debugging_notes.txt b/debugging_notes.txt index bc53307ad5b7296bc91988d88b4cb3dccd167b1a..4ee3d313faccbf17bc8928b93bdb82b5c7ec5b35 100644 --- a/debugging_notes.txt +++ b/debugging_notes.txt @@ -1,3 +1,11 @@ + +# 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) diff --git a/dtree_synth.py b/dtree_synth.py index 318f597a0c186730505bc1d19d7f3681e7504ea6..79e7b667c7a1fe2cc3e658298100959e68011cae 100644 --- a/dtree_synth.py +++ b/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)