trying to parse sygus output

circleSygus.sl

@@ -15,7 +15,7 @@
      (ite (> yP 0) (- y 1) (ite (= yP 0) y (+ y 1)))
 )
 
-(synth-fun inCircle ((x Real) (y Real) (xP Real) (yP Real)) Bool
+(synth-fun inCircle ((x Real) (y Real) (x_p Real) (y_p Real)) Bool
 
         ;; Declare the non-terminals that would be used in the grammar
     ( (B Bool) (R Real) (C Real))
@@ -24,8 +24,8 @@
         (B Bool ( (<= R (sqr C)) ))
 
         (R Real (
-                    (+  (sqr (- xP (+ (* C x) (* C y) 0 ) ))
-                        (sqr (- yP (+ (* C x) (* C y) 0 ) ))
+                    (+  (sqr (- x_p (+ (* C x) (* C y) 0 ) ))
+                        (sqr (- y_p (+ (* C x) (* C y) 0 ) ))
                     )
                 )
         )
@@ -39,7 +39,7 @@
 )
 
 
-
+ 
 ;; Define the semantic constraints on the function
 
 (constraint  (= (inCircle 10 (- 10) 11 (- 11) ) true ) )

region_synth.py

+from __future__ import print_function
+from z3 import *
+from typing import List,Tuple
+
+
+
+def visitor(e, seen):
+    if e in seen:
+        return
+    seen[e] = True
+    yield e
+    
+    if is_app(e):
+        #print(" call to ToReal()")
+        #print(e)
+        #and e.decl() == "+"
+        descendants = e.children() 
+        for ch in descendants:
+            # print("child. "+ str(ch))
+            # print()
+            for e in visitor(ch, seen):
+                
+                if  is_app_of(e, Z3_OP_ADD) and e.num_args()== 3:
+                    yield e
+                #return
+        
+        return
+    #ANGELLO: DONT NEED THIS METHOD
+    if is_quantifier(e):
+        
+        for e in visitor(e.body(), seen):
+            yield e
+        return
+
+def extractAiBi(term):
+    assert is_app_of(term, Z3_OP_ADD) and term.num_args()== 3
+    seen = {}
+    def subterms(term):
+        descendants = term.children()
+        for ch in descendants:
+            if ch in seen:
+                continue
+            seen[ch] = True
+            yield ch
+            constants_terms = subterms(ch)
+            for sub in constants_terms:
+                if sub.decl().kind()== Z3_OP_ANUM:
+                    yield RealVal(sub)
+
+                if sub.decl().kind()== Z3_OP_UMINUS:
+                    yield sub
+
+    ret = [t for t in subterms(term) ]
+    return ret
+# x, y = Ints('x y')
+# fml = x + x + y > 2 
+# seen = {}
+# for e in visitor(fml, seen):
+#     if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED:
+#         print("Variable", e)
+#     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}
+    ### Chiao: Read in positive samples
+    positive_eyamples: List[Tuple[float,...]] = []
+
+    ###Angello create learner and add constraints to grammar
+
+    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 = {}
+    # sub_term_sqr = []
+    # ai_bi = []
+    # count = 0
+    # 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:
+    #         if count != 0:
+    #             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())
+    #     print(z3_expr[0].sort_kind())
+    #     print("======")
+    #     print(z3_expr[0].children())
+    
+    #if circle:
+    #    extract Ai bi and radius
+    
+
+
+
+
+
+if __name__ == "__main__":
+    synth_region()
\ No newline at end of file