From d193ecc734973ec69a495094d699be301aad42aa Mon Sep 17 00:00:00 2001
From: "Hsieh, Chiao" <chsieh16@illinois.edu>
Date: Tue, 30 Nov 2021 16:17:08 -0600
Subject: [PATCH] Clean up top level algorithm
---
region_synth.py | 67 +++++++++++++++++--------------------------------
1 file changed, 23 insertions(+), 44 deletions(-)
diff --git a/region_synth.py b/region_synth.py
index c4cf321..364a037 100644
--- a/region_synth.py
+++ b/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__":
--
GitLab