From df77541aae7d76207e61ea8b4037c3c2b6365759 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Jun 2023 16:21:31 -0700 Subject: [PATCH] #6758 check-assumptions with compound formulas create fresh proxy variables both during compilation to internal format and for the assumptions. These fresh variables may occur in lemmas that are created during search. The lemmas are garbage for future check-sats, but the solver needs to be allowed to invoke GC. Adding a GC call before a check-sat with assumptions allows removing some lemmas every time a new assumptions are used. Eager GC when using assumptions is used elsewhere, for example in cube&conquer scenarios where lemmas learned from one set of assumptions are less likely to be useful for other assumptions. With the GC invocation memory grows at a lesser pace. However, it is not entirely free of memory increases. To avoid memory bloat, have the solver pre-compile the assumptions by defining them as propositional variables, add assertions that the propositional variables are equivalent to the compound formulas and use the propositional variables as assumptions. The same propositional variables come with no extra overhead when invoking check-assumptions. The lemmas are then over the same fixed vocabulary. It is generally a good idea to recycle useful lemmas during the enumeration pass. --- src/smt/smt_context.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4125b24de..e55208575 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3337,6 +3337,7 @@ namespace smt { reset_assumptions(); m_literal2assumption.reset(); m_unsat_core.reset(); + if (!asms.empty()) { // We must give a chance to the theories to propagate before we create a new scope... propagate(); @@ -3346,6 +3347,7 @@ namespace smt { return; if (get_cancel_flag()) return; + del_inactive_lemmas(); push_scope(); vector> asm2proxy; internalize_proxies(asms, asm2proxy);