Clean up top level algorithm

region_synth.py

@@ -61,76 +61,61 @@ def extractAiBi(term):
 #     else:
 #         print(e)
 
-def synth_region():
-    x = Real('x')
-    y = Real('y')
-    x_p = Real('x_p')
-    y_p = Real('y_p')
-    sqr = Function('sqr', RealSort(),RealSort() )
-    variable_map = { str(x):x, str(y):y, str(x_p):x_p, str(y_p):y_p,  str(sqr):sqr}
+def synth_region(num_max_iterations:int = 10):
     ### Chiao: Read in positive samples
     positive_examples: List[Tuple[float,...]] = [
         (10.0, -10.0, 11.0, -11.0),
         (10.0, -10.0, 9.0, -9.0),
         (1.0, 1.0, 1.5, 2.3),
     ]
-
     
     teacher = FirstpassTeacher()
+    #  x >= 6.0 and y >= 5
+    # teacher.set_old_state_bound(lb=[6.0, 5.0], ub=[11.0, 10.0])
+
     learner = FirstpassLearner()
     learner.add_positive_examples(*positive_examples)
-    #print(learner._solver.assertions())
-    #candidate = learner.learn()
-    #print(candidate)
-    #print(type(model))
-    #print(model)
-    candidates = []
-    while True:
+    past_candidate_list = []
 
+    for k in range(num_max_iterations):
         candidate = learner.learn()
-        if candidate != None:
-            candidates.append(candidate)
-            print("candidate: "+ f"{candidate}")
+        if candidate is None:  # learning FAILED
+            break
         else:
-            #learning FAILED
-            return candidates
-
+            print("candidate: "+ f"{candidate}")
+            past_candidate_list.append(candidate)
         
-        #QUERYING TEACHER IF THERE ARE NEGATIVE EXAMPLES
+        # 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}")
+            print("negative examples: "+ f"{m}")
             learner.add_negative_examples(*m)
-            
         elif result == z3.unsat:
             print("we are done!")
-            return candidates
+            return past_candidate_list
         else:
             print(teacher.reason_unknown())
-            return candidates
+            return past_candidate_list
 
-        
-        
-
-    # 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])
-    
+def test_parse_sygus_output():
+    pass
     ###Angello create learner and add constraints to grammar
-
+    # x = Real('x')
+    # y = Real('y')
+    # x_p = Real('x_p')
+    # y_p = Real('y_p')
+    # sqr = Function('sqr', RealSort(),RealSort() )
+    # variable_map = { str(x):x, str(y):y, str(x_p):x_p, str(y_p):y_p,  str(sqr):sqr}
     #res = os.popen('../cvc4-1.8 --sygus-out=sygus-standard --lang=sygus2 circleSygus.sl').read()
     # print(res)
     # print("######")
     #exprBody = res[67:-2].strip()
     #print(exprBody)
     #print("======")
-    
+
     #z3_expr = parse_smt2_string("(assert "+exprBody+" )", decls=variable_map)
     # seen = {}
     # seen_sub = {}
@@ -140,7 +125,6 @@ def synth_region():
     # if len(z3_expr)>=1 and z3_expr[0].sort_kind() == Z3_BOOL_SORT:
     #     for e in visitor(z3_expr[0],seen):
     #         sub_term_sqr.append(e)
-        
     #     print(sub_term_sqr)
     #     print()
     #     for t in sub_term_sqr:
@@ -148,7 +132,6 @@ def synth_region():
     #             print(extractAiBi(t))
     #         count +=1
 
-    
     # if len(z3_expr)>=1 and is_expr(z3_expr[0]) and z3_expr[0].sort_kind() == Z3_BOOL_SORT:
     #     print("in if")
     #     print(z3_expr[0].decl())
@@ -158,10 +141,6 @@ def synth_region():
     
     #if circle:
     #    extract Ai bi and radius
-    
-
-
-
 
 
 if __name__ == "__main__":