Skip to content
Snippets Groups Projects
Commit bbed64bb authored by chsieh16's avatar chsieh16
Browse files

Remove custom simplify for z3 expression

parent fd4c628a
No related merge requests found
...@@ -54,12 +54,12 @@ def synth_dtree(learner: LearnerBase, teacher: TeacherBase, num_max_iterations: ...@@ -54,12 +54,12 @@ def synth_dtree(learner: LearnerBase, teacher: TeacherBase, num_max_iterations:
continue continue
elif result == z3.unsat: elif result == z3.unsat:
print("we are done!") print("we are done!")
z3_expr = tacticSimplify(z3.simplify(candidate, arith_lhs=True)) z3_expr = z3.simplify(candidate, arith_lhs=True)
ret = {"k": k, "formula": z3_expr.sexpr(), "smtlib": z3_expr.serialize()} ret = {"k": k, "formula": z3_expr.sexpr(), "smtlib": z3_expr.serialize()}
return True, ret, (teacher_time,learner_time) return True, ret, (teacher_time,learner_time)
else: else:
assert result == z3.unknown assert result == z3.unknown
z3_expr = tacticSimplify(z3.simplify(candidate, arith_lhs=True)) z3_expr = z3.simplify(candidate, arith_lhs=True)
ret = { ret = {
"reason": f"Reason Unknown {teacher.reason_unknown()}", "reason": f"Reason Unknown {teacher.reason_unknown()}",
"k": k, "formula": z3_expr.sexpr(), "smtlib": z3_expr.serialize() "k": k, "formula": z3_expr.sexpr(), "smtlib": z3_expr.serialize()
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment