working version of teacher learner loop

learner_base.py

@@ -32,6 +32,7 @@ class Z3LearnerBase(LearnerBase):
     def __init__(self, state_dim, perc_dim) -> None:
         super().__init__()
         self._solver = z3.SolverFor('QF_LRA')
+        self._solver.set(timeout=1000)
         real_var_vec = z3.RealVarVector(state_dim + perc_dim)
         self._state_vars = real_var_vec[0:state_dim]
         self._percept_vars = real_var_vec[state_dim:state_dim+perc_dim]

region_synth.py

@@ -75,17 +75,53 @@ def synth_region():
         (1.0, 1.0, 1.5, 2.3),
     ]
 
-    model = None
-
+    
+    teacher = FirstpassTeacher()
     learner = FirstpassLearner()
     learner.add_positive_examples(*positive_examples)
     #print(learner._solver.assertions())
-    model = learner.learn()
+    #candidate = learner.learn()
+    #print(candidate)
     #print(type(model))
     #print(model)
+    candidates = []
+    while True:
 
-    teacher = FirstpassTeacher()
+        candidate = learner.learn()
+        if candidate != None:
+            candidates.append(candidate)
+            print("candidate: "+ f"{candidate}")
+        else:
+            #learning FAILED
+            return candidates
+
+        
+        #QUERYING TEACHER IF THERE ARE NEGATIVE EXAMPLES
+        result = teacher.check(candidate)
+        m  = teacher.model()
+        if result == z3.sat:
+            assert len(m)> 0
+            print("negative example: "+ f"{m}")
+            learner.add_negative_examples(*m)
+            
+        elif result == z3.unsat:
+            print("we are done!")
+            return candidates
+        else:
+            print(teacher.reason_unknown())
+            return candidates
 
+        
+        
+
+    # print(coeffN)
+    # print(interceptN)
+    # print(radiusN)
+
+
+    #  x >= 6.0 and y >= 5
+    #teacher.set_old_state_bound(lb=[6.0, 5.0], ub=[11.0, 10.0])
+    
     ###Angello create learner and add constraints to grammar
 
     #res = os.popen('../cvc4-1.8 --sygus-out=sygus-standard --lang=sygus2 circleSygus.sl').read()