From fb470e27ec45da04427fe768d67dd1393802304b Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Sun, 23 Jun 2024 18:14:42 -0700
Subject: [PATCH] perf: isolate overhead for unsat core query generation

---
 src/halmos/__main__.py | 17 +++++++++++------
 src/halmos/sevm.py     | 11 +++++++----
 2 files changed, 18 insertions(+), 10 deletions(-)

diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index 088decc8..6f03c980 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -1072,9 +1072,10 @@ def solve(
         if not dump_filename:
             dump_filename = f"/tmp/{uuid.uuid4().hex}.smt2"
 
-        named_assertions = "".join(
-            [f"(assert (! |{assert_id}| :named <{assert_id}>))\n" for assert_id in query.assertions]
-        )
+        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:
@@ -1083,7 +1084,8 @@ def solve(
                 f.write("(set-option :produce-unsat-cores true)\n")
             f.write("(set-logic QF_AUFBV)\n")
             f.write(query.smtlib)
-            f.write(named_assertions)
+            if args.cache_solver:
+                f.write(named_assertions)
             f.write("(check-sat)\n")
             f.write("(get-model)\n")
             if args.cache_solver:
@@ -1126,8 +1128,11 @@ def solve(
         ctx = Context()
         solver = mk_solver(args, ctx=ctx, assertion=True)
         solver.from_string(query.smtlib)
-        ids = [Bool(f"{x}", ctx) for x in query.assertions]
-        result = solver.check(*ids)
+        if args.cache_solver:
+            ids = [Bool(f"{x}", ctx) for x in query.assertions]
+            result = solver.check(*ids)
+        else:
+            result = solver.check()
         model = copy_model(solver.model()) if result == sat else None
 
         unsat_core = None
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index 2fd7b9b5..143aea1c 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -508,10 +508,13 @@ def __str__(self) -> str:
     def to_smt2(self, args) -> SMTQuery:
         ids = [str(cond.get_id()) for cond in self.conditions]
 
-        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()
+        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()
+        else:
+            query = self.solver.to_smt2()
         query = query.replace("(check-sat)", "")  # see __main__.solve()
 
         return SMTQuery(query, ids)