Return list of tuples as counter examples

firstpass_teacher.py

@@ -73,10 +73,10 @@ def test_firstpass_teacher():
     teacher = FirstpassTeacher()
     teacher.set_old_state_bound(lb=[6.0, 5.0], ub=[11.0, 10.0])
     teacher.dump_model()
-    result = teacher.check(CAND1)
+    result = teacher.check(CAND0)
     print(result)
     if result == z3.sat:
-        teacher.model()
+        print(teacher.model())
     elif result == z3.unsat:
         print("candidate is verified")
     else:

teacher_base.py

 import abc
+from typing import Sequence, Tuple
 
 import gurobipy as gp
 import numpy as np
@@ -14,7 +15,7 @@ class TeacherBase(abc.ABC):
         raise NotImplementedError
 
     @abc.abstractmethod
-    def model(self) -> z3.ModelRef:
+    def model(self):
         raise NotImplementedError
 
     @abc.abstractmethod
@@ -73,16 +74,17 @@ class GurobiTeacherBase(TeacherBase):
             basename = self._gp_model.ModelName
         self._gp_model.write(basename + ".lp")
 
-    def model(self) -> z3.ModelRef:
-        if self._gp_model.status == gp.GRB.OPTIMAL:
+    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
             print('Obj: %g, ObjBound: %g, x: %s, z: %s\n'
                    % (m.objVal, m.objBound, x.x, z.x))
+            return [tuple(x.x) + tuple(z.x)]
         else:
-            raise z3.Z3Exception("model is not available")
+            return []
 
     def reason_unknown(self) -> str:
         if self._gp_model.status == gp.GRB.INF_OR_UNBD: