Output smtlib for Z3

dtree_synth.py

@@ -43,7 +43,7 @@ def synth_dtree(learner: LearnerBase, teacher: TeacherBase, num_max_iterations:
             continue
         elif result == z3.unsat:
             print("we are done!")
-            return True, (k, z3.simplify(candidate, arith_lhs=True).sexpr())
+            return True, (k, z3.simplify(candidate, arith_lhs=True))
         else:
             return False, f"Reason Unknown {teacher.reason_unknown()}"
 
@@ -110,12 +110,15 @@ def synth_dtree_per_part(
                                      num_max_iterations=num_max_iter)
             print(f"Found? {found}")
             if found:
-                k, expr = ret
+                k, z3_expr = ret
+                solver = z3.Solver()
+                solver.add(z3_expr)
+                smtlib = solver.to_smt2()
                 result.append({"part": part,
                                "feature_domain": feature_domain,
                                "ultimate_bound": ult_bound,
                                "status": "found",
-                               "result": {"k": k, "formula": expr}})
+                               "result": {"k": k, "formula": z3_expr.sexpr(), "smtlib": smtlib}})
             else:
                 result.append({"part": part,
                                "feature_domain": feature_domain,