diff --git a/dtree_teacher_gem_stanley.py b/dtree_teacher_gem_stanley.py index 8baf5f8f7fc55e1272fb664831bb4c2d9f2d1532..0cd904d10087bea5eba6e88a20e2e81a53f7963a 100644 --- a/dtree_teacher_gem_stanley.py +++ b/dtree_teacher_gem_stanley.py @@ -1,3 +1,6 @@ +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() diff --git a/gurobi.env b/gurobi.env index 3dd7d0edb7f4113cac7d61e8857d802b31f69494..663b6f061040f70adb4585c8452f709745f07073 100644 --- a/gurobi.env +++ b/gurobi.env @@ -1,2 +1 @@ -DualReductions 0 OutputFlag 0 diff --git a/teacher_base.py b/teacher_base.py index 6f9449f85c6552d576cab46b8012dfaad160f8ed..4e98bb8095a1a003442548a1ae8707c3af0b8000 100644 --- a/teacher_base.py +++ b/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: