Move spurious check to TeacherBase

gem_stanley_teacher.py

@@ -31,12 +31,6 @@ NEW_ATAN_K_CTE_V_LIM = np.arctan(NEW_K_CTE_V_LIM)
 NEW_RAW_ANG_ERR_LIM = ANG_LIM + FORWARD_VEL * CYCLE_TIME
 
 
-def z3_float64_const_to_real(v: float) -> z3.RatNumRef:
-    return z3.simplify(
-        z3.fpToReal(z3.FPVal(v, z3.Float64()))
-    )
-
-
 class GEMStanleyDRealTeacher(DRealTeacherBase):
 
     def __init__(self, name="gem_stanley", norm_ord=2, delta=0.001) -> None:
@@ -90,20 +84,6 @@ class GEMStanleyGurobiTeacher(GurobiTeacherBase):
     PERC_GT = np.array([[0., -1., 0.],
                         [0., 0., -1.]], float)
 
-    @staticmethod
-    def is_spurious_example(state_dim: int, perc_dim: int, candidate: z3.BoolRef, cex: Tuple[float, ...]) -> bool:
-        state_subs_map = [(z3.Real(f"x_{i}"), z3_float64_const_to_real(cex[i])) for i in range(state_dim)]
-        perc_subs_map = [(z3.Real(f"z_{i}"), z3_float64_const_to_real(cex[i+state_dim])) for i in range(perc_dim)]
-        sub_map = state_subs_map + perc_subs_map
-        val = z3.simplify(z3.substitute(candidate, *sub_map))
-        assert z3.is_bool(val)
-        if z3.is_false(val):
-            return True
-        elif z3.is_true(val):
-            return False
-        else:
-            raise RuntimeError(f"Cannot validate negative example {cex} by substitution")
-
     def __init__(self, name="gem_stanley", norm_ord=2, ultimate_bound: float=0.0) -> None:
         assert ultimate_bound >= 0.0
         self._ultimate_bound = ultimate_bound

teacher_base.py

@@ -10,7 +10,28 @@ import z3
 import dreal
 
 
+def z3_float64_const_to_real(v: float) -> z3.RatNumRef:
+    return z3.simplify(
+        z3.fpToReal(z3.FPVal(v, z3.Float64()))
+    )
+
+
 class TeacherBase(abc.ABC):
+
+    @staticmethod
+    def is_spurious_example(state_dim: int, perc_dim: int, candidate: z3.BoolRef, cex: Tuple[float, ...]) -> bool:
+        state_subs_map = [(z3.Real(f"x_{i}"), z3_float64_const_to_real(cex[i])) for i in range(state_dim)]
+        perc_subs_map = [(z3.Real(f"z_{i}"), z3_float64_const_to_real(cex[i+state_dim])) for i in range(perc_dim)]
+        sub_map = state_subs_map + perc_subs_map
+        val = z3.simplify(z3.substitute(candidate, *sub_map))
+        assert z3.is_bool(val)
+        if z3.is_false(val):
+            return True
+        elif z3.is_true(val):
+            return False
+        else:
+            raise RuntimeError(f"Cannot validate negative example {cex} by substitution")
+
     def __init__(self) -> None:
         pass