implementing the algorithm

region_synth.py

 from __future__ import print_function
 from z3 import *
 from typing import List,Tuple
-
-
+from firstpass_learner import FirstpassLearner
+from firstpass_teacher import FirstpassTeacher
 
 def visitor(e, seen):
     if e in seen:
@@ -69,18 +69,33 @@ def synth_region():
     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}
     ### Chiao: Read in positive samples
-    positive_eyamples: List[Tuple[float,...]] = []
+    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),
+    ]
+
+    model = None
+
+    learner = FirstpassLearner()
+    learner.add_positive_examples(*positive_examples)
+    #print(learner._solver.assertions())
+    model = learner.learn()
+    #print(type(model))
+    #print(model)
+
+    teacher = FirstpassTeacher()
 
     ###Angello create learner and add constraints to grammar
 
-    res = os.popen('../cvc4-1.8 --sygus-out=sygus-standard --lang=sygus2 circleSygus.sl').read()
+    #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("======")
+    #exprBody = res[67:-2].strip()
+    #print(exprBody)
+    #print("======")
     
-    z3_expr = parse_smt2_string("(assert "+exprBody+" )", decls=variable_map)
+    #z3_expr = parse_smt2_string("(assert "+exprBody+" )", decls=variable_map)
     # seen = {}
     # seen_sub = {}
     # sub_term_sqr = []