perf: custom smtlib generation, vs to_smt2()

src/halmos/__main__.py

@@ -1071,20 +1071,13 @@ def solve(
         if not dump_filename:
             dump_filename = f"/tmp/{uuid.uuid4().hex}.smt2"
 
-        if args.cache_solver:
-            named_assertions = "".join(
-                [f"(assert (! |{assert_id}| :named <{assert_id}>))\n" for assert_id in query.assertions]
-            )
-
         with open(dump_filename, "w") as f:
             if args.verbose >= 1:
                 print(f"Writing SMT query to {dump_filename}")
             if args.cache_solver:
                 f.write("(set-option :produce-unsat-cores true)\n")
             f.write("(set-logic QF_AUFBV)\n")
             f.write(query.smtlib)
-            if args.cache_solver:
-                f.write(named_assertions)
             f.write("(check-sat)\n")
             f.write("(get-model)\n")
             if args.cache_solver:

src/halmos/sevm.py

@@ -484,12 +484,14 @@ class Path:
     num_scopes: int
     # path constraints include both explicit branching conditions and implicit assumptions (eg, no hash collisions)
     conditions: Dict  # cond -> bool (true if explicit branching conditions)
+    variables: Dict
     pending: List
 
     def __init__(self, solver: Solver):
         self.solver = solver
         self.num_scopes = 0
         self.conditions = {}
+        self.variables = {}
         self.pending = []
         self.forked = False
 
@@ -501,21 +503,20 @@ def __str__(self) -> str:
             [
                 f"- {cond}\n"
                 for cond in self.conditions
-                if self.conditions[cond] and str(cond) != "True"
+                if self.conditions[cond][0] and str(cond) != "True"
             ]
         )
 
     def to_smt2(self, args) -> SMTQuery:
         ids = [str(cond.get_id()) for cond in self.conditions]
 
+        decls = [f"{decl}\n" for decl in self.variables.values()]
         if args.cache_solver:
-            tmp_solver = SolverFor("QF_AUFBV")
-            for cond in self.conditions:
-                tmp_solver.assert_and_track(cond, str(cond.get_id()))
-            query = tmp_solver.to_smt2()
+            asserts = [f"(assert (! {sexpr} :named <{cond.get_id()}>))\n" for cond, (_, sexpr) in self.conditions.items()]
         else:
-            query = self.solver.to_smt2()
-        query = query.replace("(check-sat)", "")  # see __main__.solve()
+            asserts = [f"(assert {sexpr})\n" for _, sexpr in self.conditions.values()]
+
+        query = "".join(decls + asserts)
 
         return SMTQuery(query, ids)
 
@@ -541,6 +542,7 @@ def branch(self, cond):
         # shallow copy because existing conditions won't change
         # note: deep copy would be needed later for advanced query optimizations (eg, constant propagation)
         path.conditions = self.conditions.copy()
+        path.variables = self.variables.copy()
 
         # store the branching condition aside until the new path is activated.
         path.pending.append(cond)
@@ -572,7 +574,24 @@ def append(self, cond, branching=False):
 
         if cond not in self.conditions:
             self.solver.add(cond)
-            self.conditions[cond] = branching
+            self.conditions[cond] = (branching, cond.sexpr())
+            self.update_vars(cond)
+
+    def update_vars(self, term):
+        decl = term.decl()
+
+        if is_const(term):
+            if decl.kind() == Z3_OP_UNINTERPRETED:  # variable
+                if term not in self.variables:
+                    self.variables[term] = term.decl().sexpr()
+
+        else:
+            if is_func_decl(decl) and (decl.name().startswith("f_") or decl.name().startswith("evm_")):
+                if decl not in self.variables:
+                    self.variables[decl] = decl.sexpr()
+
+            for child in term.children():
+                self.update_vars(child)
 
     def extend(self, conds, branching=False):
         for cond in conds: