Fix bugs in setting new candidate for teacher

firstpass_teacher.py

@@ -61,6 +61,8 @@ def test_firstpass_teacher():
     teacher.set_old_state_bound(lb=[6.0, 5.0], ub=[11.0, 10.0])
     result = teacher.check(CAND0)
     teacher.dump_model()
+    result = teacher.check(CAND1)
+    teacher.dump_model("firstpass2")
     print(result)
     if result == z3.sat:
         print(teacher.model())

teacher_base.py

 import abc
-from typing import Sequence, Tuple
+from typing import List, Sequence, Tuple
 
 import gurobipy as gp
 import numpy as np
@@ -48,6 +48,16 @@ class GurobiTeacherBase(TeacherBase):
         self._add_system()
         self._add_unsafe()
 
+        # Add intermediate variables with constraints for candidates
+        z_diff = m.addMVar(name="z-(Ax+b)", shape=perc_dim, **self.FREEVAR)
+        z_dist = m.addMVar(name="|z-(Ax+b)|", shape=perc_dim, **self.NNEGVAR)
+        for zi, abs_zi in zip(z_diff.tolist(), z_dist.tolist()):
+            m.addConstr(abs_zi == gp.abs_(zi))
+        self._percept_diff = z_diff
+        self._percept_dist = z_dist
+
+        self._prev_candidate_constr: List = []
+
     @property
     def state_dim(self) -> int:
         return self._old_state.shape[0]
@@ -68,51 +78,52 @@ class GurobiTeacherBase(TeacherBase):
     def _add_unsafe(self) -> None:
         raise NotImplementedError
 
-    def _add_candidate(self, candidate) -> None:
+    def _set_candidate(self, candidate) -> None:
         shape_sel, coeff, intercept, radius = candidate  # TODO parse candidate
         # Variable Aliases
         m = self._gp_model
         x = self._old_state
         z = self._percept
-        # Constraints on values of z
-        z_diff = m.addMVar(name="z-(Ax+b)", shape=z.shape[0], **self.FREEVAR)
-        m.addConstr(z_diff == z - (coeff @ x + intercept))
+        z_diff = self._percept_diff
+        z_dist = self._percept_dist
+
+        # TODO Modify coefficients instead of remove and add back contraints
+        # Remove contraints from previous candidate first
+        m.remove(self._prev_candidate_constr)
+        self._prev_candidate_constr.clear()
         m.update()
 
+        # Constraints on values of z
+        cons = m.addConstr(z_diff == z - (coeff @ x + intercept))
+        self._prev_candidate_constr.append(cons)
+
         if shape_sel == 0:
-            z_dist = 0.0
-            for zi in z_diff.tolist():
-                abs_zi_name = "|%s|" % zi.VarName
-                abs_zi = m.addVar(name=abs_zi_name, **self.NNEGVAR)
-                m.addConstr(abs_zi == gp.abs_(zi))
-                z_dist += abs_zi
-            m.addConstr(z_dist <= radius, "||z-(Ax+b)||_1 <= r")
+            cons_r = m.addConstr(z_dist.sum() <= radius, "||z-(Ax+b)||_1 <= r")
+            self._prev_candidate_constr.append(cons_r)
             # L1-norm objective
-            m.setObjective(z_dist, gp.GRB.MINIMIZE)
+            m.setObjective(z_dist.sum(), gp.GRB.MINIMIZE)
         elif shape_sel == 1:
-            m.addConstr(z_diff @ z_diff <= radius*radius,
-                        name="||z-(Ax+b)||^2 <= r^2")
+            cons_r = m.addConstr(z_diff @ z_diff <= radius*radius,
+                                 name="||z-(Ax+b)||^2 <= r^2")
+            self._prev_candidate_constr.append(cons_r)
             # L2-norm objective
             m.setObjective(z_diff @ z_diff, gp.GRB.MINIMIZE)
         elif shape_sel == 2:
-            abs_zi_list = []
-            for zi in z_diff.tolist():
-                abs_zi_name = "|%s|" % zi.VarName
-                abs_zi = m.addVar(name=abs_zi_name, **self.NNEGVAR)
-                m.addConstr(abs_zi == gp.abs_(zi))
-                abs_zi_list.append(abs_zi)
-            z_dist = m.addVar(name="||z-(Ax+b)||_oo", **self.NNEGVAR)
-            m.addConstr(z_dist == gp.max_(abs_zi_list))
-            m.addConstr(z_dist <= radius, "||z-(Ax+b)||_oo <= r")
-
-            m.setObjective(z_dist, gp.GRB.MINIMIZE)
+            dist_oo = m.addVar(name="||z-(Ax+b)||_oo", **self.NNEGVAR)
+            cons_max = m.addConstr(dist_oo == gp.max_(*z_dist.tolist()))
+            cons_r = m.addConstr(dist_oo <= radius, "||z-(Ax+b)||_oo <= r")
+            self._prev_candidate_constr.extend([dist_oo, cons_max, cons_r])
+            # Loo-norm objective
+            m.setObjective(dist_oo, gp.GRB.MINIMIZE)
+        else:
+            raise ValueError("Unknown shape. shape_sel=%d" % shape_sel)
 
     def set_old_state_bound(self, lb, ub) -> None:
         self._old_state.lb = lb
         self._old_state.ub = ub
 
     def check(self, candidate) -> z3.CheckSatResult:
-        self._add_candidate(candidate)
+        self._set_candidate(candidate)
         self._gp_model.optimize()
         if self._gp_model.status in [gp.GRB.OPTIMAL, gp.GRB.SUBOPTIMAL]:
             return z3.sat
@@ -129,8 +140,6 @@ class GurobiTeacherBase(TeacherBase):
 
     def model(self) -> Sequence[Tuple]:
         if self._gp_model.status in [gp.GRB.OPTIMAL, gp.GRB.SUBOPTIMAL]:
-            # TODO return satisfiable instance
-            m = self._gp_model
             x = self._old_state
             z = self._percept
             return [tuple(x.x) + tuple(z.x)]