From 378ab288f6d7d32e4bbfdac6314a74fef1889660 Mon Sep 17 00:00:00 2001
From: Angello Astorga <aastorg2@illinois.edu>
Date: Mon, 29 Nov 2021 15:58:06 -0500
Subject: [PATCH] trying to parse sygus output
---
circleSygus.sl | 8 ++--
region_synth.py | 117 ++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 121 insertions(+), 4 deletions(-)
create mode 100644 region_synth.py
diff --git a/circleSygus.sl b/circleSygus.sl
index 8446fa2..642b653 100755
--- a/circleSygus.sl
+++ b/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 ) )
diff --git a/region_synth.py b/region_synth.py
new file mode 100644
index 0000000..692277a
--- /dev/null
+++ b/region_synth.py
@@ -0,0 +1,117 @@
+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
--
GitLab