fix stack overflow regression in bool_rewriter

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 29, 2024 · 6ea6831 · 6ea6831
1 parent 3526d03
commit 6ea6831
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 12 deletions.
diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
@@ -775,8 +775,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             std::swap(lhs, rhs);
 
         if (m().is_not(lhs, lhs)) {
-            mk_eq(lhs, rhs, result);
-            mk_not(result, result);
+            result = m().mk_not(m().mk_eq(lhs, rhs));
             return BR_REWRITE2;
         }
 

diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
@@ -91,12 +91,11 @@ namespace sls {
             auto const& vars = m_ev.terms.uninterp_occurs(a);
             VERIFY(!vars.empty());
             TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": ";
-            for (auto e : vars)
-                tout << mk_bounded_pp(e, m) << " ";
-            tout << "\n";);
+                        for (auto e : vars) tout << mk_bounded_pp(e, m) << " ";
+                        tout << "\n";);
             return vars;
         }
-        return m_vars;
+        return m_empty_vars;
     }
 
 
@@ -258,10 +257,10 @@ namespace sls {
                     else
                         has_tabu = true;
                 }
-                else if (m.is_bool(a) && m_ev.can_eval1(a)) {
-
+                else if (is_root(a))
                     rescore(a);
-                }
+                else if (m.is_bool(a))
+                    continue;
                 else {
                     IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n");
                     has_tabu = true;
@@ -379,9 +378,11 @@ namespace sls {
                         max_depth = std::max(max_depth, get_depth(p));
                     }
                 }
-                else if (m.is_bool(e) && m_ev.can_eval1(e)) {
+                else if (is_root(e)) {
                     rescore(e);
                 }
+                else if (m.is_bool(e))
+                    continue;
                 else {
                     UNREACHABLE();
                 }
@@ -450,6 +451,7 @@ namespace sls {
     void bv_lookahead::rescore() {
         m_top_score = 0;
         m_rescore = false;
+        m_is_root.reset();
         for (auto lit : ctx.root_literals()) {
             auto e = ctx.atom(lit.var());
             if (!e || !is_app(e))
@@ -461,6 +463,7 @@ namespace sls {
             double score = new_score(a);
             set_score(a, score);
             m_top_score += score;
+            m_is_root.mark(a);
         }
         verbose_stream() << "top score " << m_top_score << "\n";
 

diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h
@@ -67,7 +67,9 @@ namespace sls {
         bvect m_best_value;
         expr* m_best_expr = nullptr;
         bool  m_rescore = true;
-        ptr_vector<expr> m_vars;
+        ptr_vector<expr> m_empty_vars;
+        obj_map<expr, bool_info> m_bool_info;
+        expr_mark m_is_root;
 
         void init_updates();
 
@@ -84,11 +86,12 @@ namespace sls {
 
         void rescore();
 
-        obj_map<expr, bool_info> m_bool_info;
+
         unsigned get_weight(expr* e);
         void     inc_weight(expr* e);
         void     dec_weight(expr* e);
         void     recalibrate_weights();
+        bool     is_root(expr* e) { return m_is_root.is_marked(e); }
 
         void try_set(expr* u, bvect const& new_value);
         void add_updates(expr* u);