Merge branch 'main' of gitlab.engr.illinois.edu:chsieh16/cs598mp-fall2021-proj into main

dtree_teacher_gem_stanley.py

+import pickle
+
+import gurobipy as gp
 import numpy as np
 
 from gem_stanley_teacher import GEMStanleyTeacher
@@ -28,6 +31,9 @@ class DTreeTeacherGEMStanley(GEMStanleyTeacher):
         cons = m.addMConstr(coeff_mat, z_diff, '<', cut_vec)
         self._prev_candidate_constr.append(cons)
 
+        # L2-norm objective
+        m.setObjective(z_diff @ z_diff, gp.GRB.MINIMIZE)
+
 
 def test_dtree_gem_stanley_teacher():
     a_mat = np.array([[0., -1., 0.],
@@ -47,5 +53,18 @@ def test_dtree_gem_stanley_teacher():
     teacher.dump_model()
 
 
+def test_verified_candidate():
+    with open("winnerDnf.pickle", "rb") as dnf_pkl:
+        winner_dnf = pickle.load(dnf_pkl)
+
+    print(winner_dnf)
+    teacher = DTreeTeacherGEMStanley()
+    teacher.set_old_state_bound(lb=[0.0, -1.0, 0.2], ub=[30.0, -0.9, 0.22])
+    for cand in winner_dnf:
+        print(teacher.check(cand))
+        print(teacher.reason_unknown())
+
+
 if __name__ == "__main__":
-    test_dtree_gem_stanley_teacher()
+    # test_dtree_gem_stanley_teacher()
+    test_verified_candidate()

gurobi.env

-DualReductions 0
 OutputFlag 0

teacher_base.py

@@ -125,6 +125,10 @@ class GurobiTeacherBase(TeacherBase):
     def check(self, candidate) -> z3.CheckSatResult:
         self._set_candidate(candidate)
         self._gp_model.optimize()
+        if self._gp_model.status == gp.GRB.INF_OR_UNBD:
+            self._gp_model.setParam("DualReductions", 0)
+            self._gp_model.optimize()
+
         if self._gp_model.status in [gp.GRB.OPTIMAL, gp.GRB.SUBOPTIMAL]:
             return z3.sat
         elif self._gp_model.status == gp.GRB.INFEASIBLE: