fixed-size min-heap for tracking top-k literals (#7752)

* very basic setup

* ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* respect smt configuration parameter in elim_unconstrained simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* indentation

* add bash files for test runs

* add option to selectively disable variable solving for only ground expressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove verbose output

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #7745

axioms for len(substr(...)) escaped due to nested rewriting

* ensure atomic constraints are processed by arithmetic solver

* #7739 optimization

add simplification rule for at(x, offset) = ""

Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions.
The example highlights some opportunities for simplification, noteworthy at(..) = "".
The example is solved in both versions after adding this simplification.

* fix unsound len(substr) axiom

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* FreshConst is_sort (#7748)

* #7750

add pre-processing simplification

* Add parameter validation for selected API functions

* updates to ac-plugin

fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.

* enable passive, add check for bloom up-to-date

* add top-k fixed-sized min-heap priority queue for top scoring literals

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com>

run_local_tests.sh

@@ -0,0 +1,32 @@
+#!/bin/bash
+# run from inside ./z3/build
+
+Z3=./z3
+OPTIONS="-v:0 -st smt.threads=4"
+OUT_FILE="../z3_results.txt"
+BASE_PATH="../../z3-poly-testing/inputs/"
+
+# List of relative test files (relative to BASE_PATH)
+REL_TEST_FILES=(
+    "QF_NIA_small/Ton_Chanh_15__Singapore_v1_false-termination.c__p27381_terminationG_0.smt2"
+    "QF_UFDTLIA_SAT/52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2"
+)
+
+# Clear output file
+> "$OUT_FILE"
+
+# Loop through and run Z3 on each file
+for rel_path in "${REL_TEST_FILES[@]}"; do
+    full_path="$BASE_PATH$rel_path"
+    test_name="$rel_path"
+
+    echo "Running: $test_name"
+    echo "===== $test_name =====" | tee -a "$OUT_FILE"
+
+    # Run Z3 and pipe output to both screen and file
+    $Z3 "$full_path" $OPTIONS 2>&1 | tee -a "$OUT_FILE"
+
+    echo "" | tee -a "$OUT_FILE"
+done
+
+echo "Results written to $OUT_FILE"

src/api/api_ast.cpp

@@ -225,13 +225,15 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_fresh_func_decl(c, prefix, domain_size, domain, range);
         RESET_ERROR_CODE();
+        CHECK_IS_SORT(range, nullptr);
+        CHECK_SORTS(domain_size, domain, nullptr);
         if (prefix == nullptr) {
             prefix = "";
         }
 
         func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix,
                                                        domain_size,
-                                                       reinterpret_cast<sort*const*>(domain),
+                                                       to_sorts(domain),
                                                        to_sort(range), false);
 
         mk_c(c)->save_ast_trail(d);
@@ -243,9 +245,11 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_fresh_const(c, prefix, ty);
         RESET_ERROR_CODE();
+        CHECK_IS_SORT(ty, nullptr);
         if (prefix == nullptr) {
             prefix = "";
         }
+
         app* a = mk_c(c)->m().mk_fresh_const(prefix, to_sort(ty), false);
         mk_c(c)->save_ast_trail(a);
         RETURN_Z3(of_ast(a));
@@ -654,6 +658,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_sort_name(c, t);
         RESET_ERROR_CODE();
+        CHECK_IS_SORT(t, of_symbol(symbol::null));
         CHECK_VALID_AST(t, of_symbol(symbol::null));
         return of_symbol(to_sort(t)->get_name());
         Z3_CATCH_RETURN(of_symbol(symbol::null));

src/api/api_context.h

@@ -286,10 +286,13 @@ namespace api {
 inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*>(c); }
 #define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); }
 #define SET_ERROR_CODE(ERR, MSG) { mk_c(c)->set_error_code(ERR, MSG); }
-#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == 0) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
+#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == nullptr) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
-#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
+#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
 inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
-#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
+#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == nullptr || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
+#define CHECK_IS_SORT(_p_, _ret_) { if (_p_ == nullptr || !is_sort(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } }
+#define CHECK_SORTS(_n_, _ps_, _ret_) { for (unsigned i = 0; i < _n_; ++i) if (!is_sort(_ps_[i])) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } }
+
 inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
-#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } }
+#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } }
 inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); }

src/api/api_util.h

@@ -67,6 +67,7 @@ inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast<ast* con
 
 inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); }
 inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); }
+inline bool is_sort(Z3_sort a) { return is_sort(to_sort(a)); }
 
 inline sort * const *  to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); }
 inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }

src/api/python/z3/z3.py

@@ -1506,6 +1506,8 @@ def Consts(names, sort):
 
 def FreshConst(sort, prefix="c"):
     """Create a fresh constant of a specified sort"""
+    if z3_debug():
+        _z3_assert(is_sort(sort), f"Z3 sort expected, got {type(sort)}")
     ctx = _get_ctx(sort.ctx)
     return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
 

src/ast/euf/euf_ac_plugin.cpp

@@ -136,15 +136,13 @@ namespace euf {
 
     // unit -> {}
     void ac_plugin::add_unit(enode* u) {
-        m_units.push_back(u);
+        push_equation(u, nullptr);
-        mk_node(u);
-        auto m_id = to_monomial(u, {});
-        init_equation(eq(to_monomial(u), m_id, justification::axiom(get_id())));
     }
 
     // zero x -> zero
     void ac_plugin::add_zero(enode* z) {
         mk_node(z)->is_zero = true;
+        // zeros persist
     }
 
     void ac_plugin::register_shared(enode* n) {
@@ -165,12 +163,16 @@ namespace euf {
         push_undo(is_register_shared);
     }
 
+    void ac_plugin::push_scope_eh() {
+        push_undo(is_push_scope);
+    }
+
     void ac_plugin::undo() {
         auto k = m_undo.back();
         m_undo.pop_back();
         switch (k) {
-        case is_add_eq: {
+        case is_queue_eq: {
-            m_active.pop_back();
+            m_queued.pop_back();
             break;
         }
         case is_add_node: {
@@ -180,14 +182,15 @@ namespace euf {
             n->~node();
             break;
         }
-        case is_add_monomial: {
+        case is_push_scope: {
-            m_monomials.pop_back();
+            m_active.reset();
+            m_passive.reset();
+            m_units.reset();
+            m_queue_head = 0;
             break;
         }
-        case is_update_eq: {
+        case is_add_monomial: {
-            auto const& [idx, eq] = m_update_eq_trail.back();
+            m_monomials.pop_back();
-            m_active[idx] = eq;
-            m_update_eq_trail.pop_back();
             break;
         }
         case is_add_shared_index: {
@@ -316,14 +319,24 @@ namespace euf {
     }
 
     void ac_plugin::merge_eh(enode* l, enode* r) {
-        if (l == r)
+        push_equation(l, r);
-            return;
+    }
+
+    void ac_plugin::pop_equation(enode* l, enode* r) {
         m_fuel += m_fuel_inc;
+        if (!r) {
+            m_units.push_back(l);
+            mk_node(l);
+            auto m_id = to_monomial(l, {});
+            init_equation(eq(to_monomial(l), m_id, justification::axiom(get_id())), true);
+        }
+        else {
             auto j = justification::equality(l, r);
             auto m1 = to_monomial(l);
             auto m2 = to_monomial(r);
             TRACE(plugin, tout << "merge: " << m_name << " " << g.bpp(l) << " == " << g.bpp(r) << " " << m_pp_ll(*this, monomial(m1)) << " == " << m_pp_ll(*this, monomial(m2)) << "\n");
-        init_equation(eq(m1, m2, j));
+            init_equation(eq(m1, m2, j), true);
+        }
     }
 
     void ac_plugin::diseq_eh(enode* eq) {
@@ -336,12 +349,32 @@ namespace euf {
         register_shared(b);
     }
 
-    bool ac_plugin::init_equation(eq const& e) {
+    void ac_plugin::push_equation(enode* l, enode* r) {
-        m_active.push_back(e);
+        if (l == r)
-        auto& eq = m_active.back();
+            return;
-        deduplicate(monomial(eq.l).m_nodes, monomial(eq.r).m_nodes);
+        m_queued.push_back({ l, r });
+        push_undo(is_queue_eq);
+    }
 
-        if (orient_equation(eq)) {
+    bool ac_plugin::init_equation(eq eq, bool is_active) {
+        deduplicate(monomial(eq.l), monomial(eq.r));
+        if (!orient_equation(eq))
+            return false;
+
+#if 1
+        if (is_reducing(eq))
+            is_active = true;
+#else
+
+        is_active = true; // set to active by default
+#endif
+
+        if (!is_active) {
+            m_passive.push_back(eq);
+            return true;          
+        }
+
+        m_active.push_back(eq);
         auto& ml = monomial(eq.l);
         auto& mr = monomial(eq.r);
 
@@ -388,11 +421,7 @@ namespace euf {
 
         return true;
     }
-        else {
+    
-            m_active.pop_back();
-            return false;
-        }
-    }
 
     bool ac_plugin::orient_equation(eq& e) {
         auto& ml = monomial(e.l);
@@ -455,8 +484,11 @@ namespace euf {
 
     uint64_t ac_plugin::filter(monomial_t& m) {
         auto& bloom = m.m_bloom;
-        if (bloom.m_tick == m_tick)
+
+        if (bloom.m_tick == m_tick) {
+            SASSERT(bloom_filter_is_correct(m.m_nodes, m.m_bloom));
             return bloom.m_filter;
+        }
         bloom.m_filter = 0;
         for (auto n : m)
             bloom.m_filter |= (1ull << (n->id() % 64ull));
@@ -466,6 +498,13 @@ namespace euf {
         return bloom.m_filter;
     }
 
+    bool ac_plugin::bloom_filter_is_correct(ptr_vector<node> const& m, bloom const& b) const {
+        uint64_t f = 0;
+        for (auto n : m)
+            f |= (1ull << (n->id() % 64ull));
+        return b.m_filter == f;
+    }
+
     bool ac_plugin::can_be_subset(monomial_t& subset, monomial_t& superset) {
         if (subset.size() > superset.size())
             return false;
@@ -477,6 +516,7 @@ namespace euf {
     bool ac_plugin::can_be_subset(monomial_t& subset, ptr_vector<node> const& m, bloom& bloom) {
         if (subset.size() > m.size())
             return false;
+        SASSERT(bloom.m_tick != m_tick || bloom_filter_is_correct(m, bloom));
         if (bloom.m_tick != m_tick) {
             bloom.m_filter = 0;
             for (auto n : m)
@@ -562,6 +602,10 @@ namespace euf {
     }
 
     void ac_plugin::propagate() {
+        while (m_queue_head < m_queued.size()) {
+            auto [l, r] = m_queued[m_queue_head++];
+            pop_equation(l, r);
+        }
         while (true) {
         loop_start:
             if (m_fuel == 0)
@@ -583,7 +627,7 @@ namespace euf {
                     goto loop_start;
 
             auto& eq = m_active[eq_id];
-            deduplicate(monomial(eq.l).m_nodes, monomial(eq.r).m_nodes);
+            deduplicate(monomial(eq.l), monomial(eq.r));
             if (monomial(eq.l).size() == 0) {
                 set_status(eq_id, eq_status::is_dead_eq);
                 continue;
@@ -623,12 +667,20 @@ namespace euf {
     }
 
     unsigned ac_plugin::pick_next_eq() {
+        init_pick:
         while (!m_to_simplify_todo.empty()) {
             unsigned id = *m_to_simplify_todo.begin();
             if (id < m_active.size() && is_to_simplify(id))
                 return id;
             m_to_simplify_todo.remove(id);
         }
+        if (!m_passive.empty()) {
+            auto eq = m_passive.back();
+            // verbose_stream() << "pick passive " << eq_pp_ll(*this, eq) << "\n";
+            m_passive.pop_back();
+            init_equation(eq, true);
+            goto init_pick;
+        }
         return UINT_MAX;
     }
 
@@ -640,11 +692,7 @@ namespace euf {
         if (are_equal(monomial(eq.l), monomial(eq.r)))
             s = eq_status::is_dead_eq;
 
-        if (eq.status != s) {
-            m_update_eq_trail.push_back({ id, eq });
         eq.status = s;
-            push_undo(is_update_eq);
-        }
         switch (s) {
         case eq_status::is_processed_eq:
         case eq_status::is_reducing_eq:
@@ -673,7 +721,7 @@ namespace euf {
     }
 
     //
-    // backward iterator allows simplification of eq
+    // forward iterator allows simplification of eq
     // The rhs of eq is a super-set of lhs of other eq.
     // 
     unsigned_vector const& ac_plugin::forward_iterator(unsigned eq_id) {
@@ -749,7 +797,7 @@ namespace euf {
     }
 
     //
-    // forward iterator simplifies other eqs where their rhs is a superset of lhs of eq
+    // backward iterator simplifies other eqs where their rhs is a superset of lhs of eq
     // 
     unsigned_vector const& ac_plugin::backward_iterator(unsigned eq_id) {
         auto& eq = m_active[eq_id];
@@ -843,10 +891,8 @@ namespace euf {
         reduce(m_src_r, j);
         auto new_r = to_monomial(m_src_r);
         index_new_r(dst_eq, monomial(m_active[dst_eq].r), monomial(new_r));
-        m_update_eq_trail.push_back({ dst_eq, m_active[dst_eq] });
         m_active[dst_eq].r = new_r;
         m_active[dst_eq].j = j;
-        push_undo(is_update_eq);
         m_src_r.reset();
         m_src_r.append(monomial(src.r).m_nodes);
         TRACE(plugin_verbose, tout << "rewritten to " << m_pp_ll(*this, monomial(new_r)) << "\n");
@@ -862,7 +908,7 @@ namespace euf {
         //
         // dst_ids, dst_count contain rhs of dst_eq
         //
-        TRACE(plugin, tout << "backward simplify " << eq_pp_ll(*this, src) << " " << eq_pp_ll(*this, dst) << " can-be-subset: " << can_be_subset(monomial(src.l), monomial(dst.r)) << "\n");
+        TRACE(plugin, tout << "forward simplify " << eq_pp_ll(*this, src) << " " << eq_pp_ll(*this, dst) << " can-be-subset: " << can_be_subset(monomial(src.l), monomial(dst.r)) << "\n");
 
         if (forward_subsumes(src_eq, dst_eq)) {
             set_status(dst_eq, eq_status::is_dead_eq);
@@ -891,11 +937,9 @@ namespace euf {
         reduce(m, j);
         auto new_r = to_monomial(m);
         index_new_r(dst_eq, monomial(m_active[dst_eq].r), monomial(new_r));
-        m_update_eq_trail.push_back({ dst_eq, m_active[dst_eq] });
         m_active[dst_eq].r = new_r;
         m_active[dst_eq].j = j;
         TRACE(plugin, tout << "rewritten to " << m_pp(*this, monomial(new_r)) << "\n");
-        push_undo(is_update_eq);
 
         return true;
     }
@@ -975,7 +1019,9 @@ namespace euf {
             SASSERT(!are_equal(m_active[src_eq], m_active[dst_eq]));
             return false;
         }
-        return all_of(monomial(dst.r), [&](node* n) { unsigned id = n->id(); return m_src_r_counts[id] == m_dst_r_counts[id]; });
+        bool r = all_of(monomial(dst.r), [&](node* n) { unsigned id = n->id(); return m_src_r_counts[id] == m_dst_r_counts[id]; });
+        SASSERT(r || !are_equal(m_active[src_eq], m_active[dst_eq]));
+        return r;
     }
 
     // src_l_counts, src_r_counts are initialized for src.l, src.r
@@ -1079,8 +1125,7 @@ namespace euf {
                     goto init_loop;
                 }
             }
-        }
+        } while (false);
-        while (false);
         VERIFY(sz >= m.size());
         return change;
     }
@@ -1177,7 +1222,7 @@ namespace euf {
         unsigned max_left_new = std::max(m_src_r.size(), m_dst_r.size());
         unsigned min_right_new = std::min(m_src_r.size(), m_dst_r.size());
         if (max_left_new <= max_left && min_right_new <= min_right)
-            added_eq = init_equation(eq(to_monomial(m_src_r), to_monomial(m_dst_r), j));
+            added_eq = init_equation(eq(to_monomial(m_src_r), to_monomial(m_dst_r), j), false);
 
         CTRACE(plugin, added_eq,
             tout << "superpose: " << m_name << " " << eq_pp_ll(*this, src) << " " << eq_pp_ll(*this, dst) << " --> ";
@@ -1202,23 +1247,36 @@ namespace euf {
             SASSERT(is_active(other_eq));
             backward_reduce(eq, other_eq);
         }
+        for (auto p : m_passive) {
+            bool change = false;
+            if (backward_reduce_monomial(eq, p, monomial(p.l)))
+                change = true;
+            if (backward_reduce_monomial(eq, p, monomial(p.r)))
+                change = true;
+            (void)change;
+            CTRACE(plugin, change,
+                verbose_stream() << "backward reduce " << eq_pp_ll(*this, eq) << " " << eq_pp_ll(*this, p) << "\n");
+        }           
     }
 
-    // TODO: this is destructive. It breaks reversibility.
-    // TODO: also need justifications from eq if there is a change.
     void ac_plugin::backward_reduce(eq const& eq, unsigned other_eq_id) {
         auto& other_eq = m_active[other_eq_id];
+        TRACE(plugin_verbose,
+            tout << "backward reduce " << eq_pp_ll(*this, eq) << " " << eq_pp_ll(*this, other_eq) << "\n");
         bool change = false;
-        if (backward_reduce_monomial(eq, monomial(other_eq.l)))
+        if (backward_reduce_monomial(eq, other_eq, monomial(other_eq.l)))
             change = true;
-        if (backward_reduce_monomial(eq, monomial(other_eq.r)))
+        if (backward_reduce_monomial(eq, other_eq, monomial(other_eq.r)))
             change = true;
-        if (change) 
+        CTRACE(plugin, change,
+            tout << "backward reduce " << eq_pp_ll(*this, eq) << " " << eq_pp_ll(*this, other_eq) << "\n");
+        if (change) {
             set_status(other_eq_id, eq_status::is_to_simplify_eq);
         }
+    }
 
-    bool ac_plugin::backward_reduce_monomial(eq const& eq, monomial_t& m) {
+    bool ac_plugin::backward_reduce_monomial(eq const& src, eq& dst, monomial_t& m) {
-        auto const& r = monomial(eq.r);
+        auto const& r = monomial(src.r);
         unsigned j = 0;
         bool change = false;
         for (auto n : m) {
@@ -1241,6 +1299,10 @@ namespace euf {
             m.m_nodes[j++] = r[0];
         }
         m.m_nodes.shrink(j);
+        if (change) {
+            m.m_bloom.m_tick = 0;
+            dst.j = join(dst.j, src);
+        }
         return change;
     }
 
@@ -1277,8 +1339,17 @@ namespace euf {
         return true;
     }
 
+
+    void ac_plugin::deduplicate(monomial_t& a, monomial_t& b) {
+        unsigned sza = a.size(), szb = b.size();
+        deduplicate(a.m_nodes, b.m_nodes);
+        if (sza != a.size())
+            a.m_bloom.m_tick = 0;
+        if (szb != b.size())
+            b.m_bloom.m_tick = 0;
+    }
+
     void ac_plugin::deduplicate(ptr_vector<node>& a, ptr_vector<node>& b) {
-        {
         for (auto n : a) {
             if (n->is_zero) {
                 a[0] = n;
@@ -1293,7 +1364,6 @@ namespace euf {
                 break;
             }
         }
-        }
 
         if (!m_is_injective)
             return;
@@ -1385,9 +1455,7 @@ namespace euf {
         push_undo(is_update_shared);
         m_shared[idx].m = new_m;
         m_shared[idx].j = j;
-
         TRACE(plugin_verbose, tout << "shared simplified to " << m_pp_ll(*this, monomial(new_m)) << "\n");
-        
         push_merge(old_n, new_n, j);
     }
 
@@ -1397,19 +1465,15 @@ namespace euf {
     }
 
     justification::dependency* ac_plugin::justify_equation(unsigned eq) {
-        auto const& e = m_active[eq];
+        return m_dep_manager.mk_leaf(m_active[eq].j);
-        auto* j = m_dep_manager.mk_leaf(e.j);
-        j = justify_monomial(j, monomial(e.l));
-        j = justify_monomial(j, monomial(e.r));
-        return j;
-    }
-
-    justification::dependency* ac_plugin::justify_monomial(justification::dependency* j, monomial_t const& m) {
-        return j;
     }
 
     justification ac_plugin::join(justification j, unsigned eq) {
         return justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(j), justify_equation(eq)));
     }
 
+    justification ac_plugin::join(justification j, eq const& eq) {
+        return justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(j), m_dep_manager.mk_leaf(eq.j)));
+    }
+
 }

src/ast/euf/euf_ac_plugin.h

@@ -123,6 +123,7 @@ namespace euf {
         func_decl*               m_decl = nullptr;
         bool                     m_is_injective = false;
         vector<eq>               m_active, m_passive;
+        enode_pair_vector        m_queued;
         ptr_vector<node>         m_nodes;
         bool_vector              m_shared_nodes;
         vector<monomial_t>       m_monomials;
@@ -146,21 +147,21 @@ namespace euf {
 
         // backtrackable state
         enum undo_kind {
-            is_add_eq,
+            is_queue_eq,
             is_add_monomial,
             is_add_node,
-            is_update_eq,
             is_add_shared_index,
             is_add_eq_index,
             is_register_shared,
-            is_update_shared
+            is_update_shared,
+            is_push_scope
         };
         svector<undo_kind>       m_undo;
         ptr_vector<node>         m_node_trail;
+        unsigned                 m_queue_head = 0;
 
         svector<std::pair<unsigned, shared>> m_update_shared_trail;
         svector<std::tuple<node*, unsigned, unsigned>> m_merge_trail;
-        svector<std::pair<unsigned, eq>> m_update_eq_trail;
 
 
 
@@ -178,6 +179,7 @@ namespace euf {
         enode* from_monomial(ptr_vector<node> const& m);
         monomial_t const& monomial(unsigned i) const { return m_monomials[i]; }
         monomial_t& monomial(unsigned i) { return m_monomials[i]; }
+        
         void sort(monomial_t& monomial);
         bool is_sorted(monomial_t const& monomial) const;
         uint64_t filter(monomial_t& m);
@@ -188,11 +190,12 @@ namespace euf {
         bool are_equal(eq const& a, eq const& b)  {
             return are_equal(monomial(a.l), monomial(b.l)) && are_equal(monomial(a.r), monomial(b.r));
         }
+        bool bloom_filter_is_correct(ptr_vector<node> const& m, bloom const& b) const;
         bool well_formed(eq const& e) const;
         bool is_reducing(eq const& e) const;
         void backward_reduce(unsigned eq_id);
-        void backward_reduce(eq const& src, unsigned dst);
+        void backward_reduce(eq const& eq, unsigned dst);
-        bool backward_reduce_monomial(eq const& eq, monomial_t& m);
+        bool backward_reduce_monomial(eq const& src, eq & dst, monomial_t& m);
         void forward_subsume_new_eqs();
         bool is_forward_subsumed(unsigned dst_eq);
         bool forward_subsumes(unsigned src_eq, unsigned dst_eq);
@@ -208,7 +211,9 @@ namespace euf {
             return nullptr;
         }
        
-        bool init_equation(eq const& e);
+        bool init_equation(eq e, bool is_active);
+        void push_equation(enode* l, enode* r);
+        void pop_equation(enode* l, enode* r);
         bool orient_equation(eq& e);
         void set_status(unsigned eq_id, eq_status s);
         unsigned pick_next_eq();
@@ -217,6 +222,7 @@ namespace euf {
         void backward_simplify(unsigned eq_id, unsigned using_eq);
         bool forward_simplify(unsigned eq_id, unsigned using_eq);
         bool superpose(unsigned src_eq, unsigned dst_eq);
+        void deduplicate(monomial_t& a, monomial_t& b);
         void deduplicate(ptr_vector<node>& a, ptr_vector<node>& b);
         
         ptr_vector<node> m_src_r, m_src_l, m_dst_r, m_dst_l;
@@ -260,8 +266,8 @@ namespace euf {
 
         justification justify_rewrite(unsigned eq1, unsigned eq2);
         justification::dependency* justify_equation(unsigned eq);
-        justification::dependency* justify_monomial(justification::dependency* d, monomial_t const& m);
         justification join(justification j1, unsigned eq);
+        justification join(justification j1, eq const& eq);
 
         bool is_correct_ref_count(monomial_t const& m, ref_counts const& counts) const;
         bool is_correct_ref_count(ptr_vector<node> const& m, ref_counts const& counts) const;
@@ -301,6 +307,8 @@ namespace euf {
 
         void undo() override;
 
+        void push_scope_eh() override;
+
         void propagate() override;
         
         std::ostream& display(std::ostream& out) const override;

src/ast/euf/euf_arith_plugin.h

@@ -43,6 +43,11 @@ namespace euf {
 
         void undo() override;
 
+        void push_scope_eh() override {
+            m_add.push_scope_eh();
+            m_mul.push_scope_eh();
+        }
+
         void propagate() override;
         
         std::ostream& display(std::ostream& out) const override;

src/ast/euf/euf_egraph.cpp

@@ -103,6 +103,9 @@ namespace euf {
             m_scopes.push_back(m_updates.size());
             m_region.push_scope();
             m_updates.push_back(update_record(m_new_th_eqs_qhead, update_record::new_th_eq_qhead()));
+            for (auto p : m_plugins)
+                if (p)
+                    p->push_scope_eh();
         }
         SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
     }

src/ast/euf/euf_plugin.h

@@ -53,6 +53,8 @@ namespace euf {
 
         virtual void undo() = 0;
 
+        virtual void push_scope_eh() {}
+        
         virtual std::ostream& display(std::ostream& out) const = 0;
 
         virtual void collect_statistics(statistics& st) const {}

src/ast/rewriter/bv_rewriter.cpp

@@ -2265,6 +2265,20 @@ br_status bv_rewriter::mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref
         unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64_t>(bv_size));
         return mk_bv_rotate_left(shift, arg1, result);
     }
+    expr* x = nullptr, * y = nullptr;
+    if (m_util.is_ext_rotate_right(arg1, x, y) && arg2 == y) {
+        // bv_ext_rotate_left(bv_ext_rotate_right(x, y), y) --> x
+        result = x;
+        return BR_DONE;
+    }
+    if (m_util.is_ext_rotate_left(arg1, x, y)) {
+        result = m_util.mk_bv_rotate_left(x, m_util.mk_bv_add(y, arg2));
+        return BR_REWRITE2;
+    }
+    if (m_util.is_ext_rotate_right(arg1, x, y)) {
+        result = m_util.mk_bv_rotate_left(x, m_util.mk_bv_sub(arg2, y));
+        return BR_REWRITE2;
+    }
     return BR_FAILED;
 }
 
@@ -2275,6 +2289,20 @@ br_status bv_rewriter::mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref
         unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64_t>(bv_size));
         return mk_bv_rotate_right(shift, arg1, result);
     }
+    expr* x = nullptr, * y = nullptr;
+    if (m_util.is_ext_rotate_left(arg1, x, y) && arg2 == y) {
+        // bv_ext_rotate_right(bv_ext_rotate_left(x, y), y) --> x
+        result = x;
+        return BR_DONE;
+    }
+    if (m_util.is_ext_rotate_right(arg1, x, y)) {
+        result = m_util.mk_bv_rotate_right(x, m_util.mk_bv_add(y, arg2));
+        return BR_REWRITE2;
+    }
+    if (m_util.is_ext_rotate_left(arg1, x, y)) {
+        result = m_util.mk_bv_rotate_right(x, m_util.mk_bv_sub(arg2, y));
+        return BR_REWRITE2;
+    }
     return BR_FAILED;
 }
 

src/ast/rewriter/seq_axioms.cpp

@@ -1224,16 +1224,40 @@ namespace seq {
         let n = len(x)
         - len(a ++ b) = len(a) + len(b) if x = a ++ b
         - len(unit(u)) = 1              if x = unit(u)
+        - len(extract(x, o, l)) = l     if len(x) >= o + l etc
         - len(str) = str.length()       if x = str
         - len(empty) = 0                if x = empty
         - len(int.to.str(i)) >= 1       if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|))
         - len(x) >= 0                   otherwise
     */
     void axioms::length_axiom(expr* n) {
-        expr* x = nullptr;
+        expr* x = nullptr, * y = nullptr, * offs = nullptr, * l = nullptr;
         VERIFY(seq.str.is_length(n, x));
-        if (seq.str.is_concat(x) ||
+        if (seq.str.is_concat(x) && to_app(x)->get_num_args() != 0) {
-            seq.str.is_unit(x) ||
+            ptr_vector<expr> args;
+            for (auto arg : *to_app(x)) 
+                args.push_back(seq.str.mk_length(arg));
+            expr_ref len(a.mk_add(args), m);
+            add_clause(mk_eq(len, n));
+        }        
+        else if (seq.str.is_extract(x, y, offs, l)) {
+            // len(extract(y, o, l)) = l if len(y) >= o + l, o >= 0, l >= 0
+            // len(extract(y, o, l)) = 0 if o < 0 or l <= 0 or len(y) < o
+            // len(extract(y, o, l)) = len(y) - o if o <= len(y) < o + l
+            expr_ref len_y(mk_len(y), m);
+            expr_ref z(a.mk_int(0), m);
+            expr_ref y_ge_l = mk_ge(a.mk_sub(len_y, a.mk_add(offs, l)), 0);
+            expr_ref y_ge_o = mk_ge(a.mk_sub(len_y, offs), 0); 
+            expr_ref offs_ge_0 = mk_ge(offs, 0);
+            expr_ref l_ge_0 = mk_ge(l, 0);
+            
+            add_clause(~offs_ge_0, ~l_ge_0, ~y_ge_l, mk_eq(n, l));
+            add_clause(offs_ge_0, mk_eq(n, z));
+            add_clause(l_ge_0, mk_eq(n, z));
+            add_clause(y_ge_o, mk_eq(n, z));
+            add_clause(~y_ge_o, y_ge_l, mk_eq(n, a.mk_sub(len_y, offs))); 
+        }
+        else if (seq.str.is_unit(x) ||
             seq.str.is_empty(x) ||
             seq.str.is_string(x)) {
             expr_ref len(n, m);

src/ast/rewriter/seq_rewriter.cpp

@@ -6021,6 +6021,12 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
         result = m_autil.mk_lt(s, zero());
         return true;
     }
+    // at(s, offset) = "" <=> len(s) <= offset or offset < 0
+    if (str().is_at(r, s, offset)) {
+        expr_ref len_s(str().mk_length(s), m()); 
+        result = m().mk_or(m_autil.mk_le(len_s, offset), m_autil.mk_lt(offset, zero()));
+        return true;
+    }
     return false;
 }
 

src/ast/simplifiers/elim_unconstrained.cpp

@@ -112,7 +112,7 @@ eliminate:
 --*/
 
 
-
+#include "params/smt_params_helper.hpp"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
 #include "ast/recfun_decl_plugin.h"
@@ -166,7 +166,7 @@ void elim_unconstrained::eliminate() {
         expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m);
         bool inverted = m_inverter(t->get_decl(), t->get_num_args(), m_args.data() + sz, r);
         proof_ref pr(m);
-        if (inverted && m_enable_proofs) {
+        if (inverted && m_config.m_enable_proofs) {
             expr * s    = m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz);
             expr * eq   = m.mk_eq(s, r);
             proof * pr1 = m.mk_def_intro(eq);
@@ -267,7 +267,7 @@ void elim_unconstrained::reset_nodes() {
  */
 void elim_unconstrained::init_nodes() {
 
-    m_enable_proofs = false;
+    m_config.m_enable_proofs = false;
     m_trail.reset();
     m_fmls.freeze_suffix();
 
@@ -276,7 +276,7 @@ void elim_unconstrained::init_nodes() {
         auto [f, p, d] = m_fmls[i]();
         terms.push_back(f);
         if (p)
-            m_enable_proofs = true;
+            m_config.m_enable_proofs = true;
     }
 
     m_heap.reset();
@@ -303,7 +303,7 @@ void elim_unconstrained::init_nodes() {
     for (expr* e : terms)
         get_node(e).set_top();      
 
-    m_inverter.set_produce_proofs(m_enable_proofs);
+    m_inverter.set_produce_proofs(m_config.m_enable_proofs);
         
 }
 
@@ -422,6 +422,8 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
 }
 
 void elim_unconstrained::reduce() {
+    if (!m_config.m_enabled)
+        return;
     generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
     m_inverter.set_model_converter(mc.get());
     m_created_compound = true;
@@ -436,3 +438,8 @@ void elim_unconstrained::reduce() {
         mc->reset();        
     }
 }
+
+void elim_unconstrained::updt_params(params_ref const& p) {
+    smt_params_helper sp(p);
+    m_config.m_enabled = sp.elim_unconstrained();
+}

src/ast/simplifiers/elim_unconstrained.h

@@ -79,6 +79,10 @@ class elim_unconstrained : public dependent_expr_simplifier {
         unsigned m_num_eliminated = 0;
         void reset() { m_num_eliminated = 0; }
     };
+    struct config {
+        bool m_enabled = true;
+        bool m_enable_proofs = false;
+    };
     expr_inverter            m_inverter;
     ptr_vector<node>         m_nodes;
     var_lt                   m_lt;
@@ -86,8 +90,8 @@ class elim_unconstrained : public dependent_expr_simplifier {
     expr_ref_vector          m_trail;
     expr_ref_vector          m_args;
     stats                    m_stats;
+    config                   m_config;
     bool                     m_created_compound = false;
-    bool                     m_enable_proofs = false;
 
     bool is_var_lt(int v1, int v2) const;
     node& get_node(unsigned n) const { return *m_nodes[n]; }
@@ -119,4 +123,7 @@ public:
     void collect_statistics(statistics& st) const override { st.update("elim-unconstrained", m_stats.m_num_eliminated); }
 
     void reset_statistics() override { m_stats.reset(); }
+
+    void updt_params(params_ref const& p) override;
+    
 };

src/ast/simplifiers/solve_eqs.cpp

@@ -46,6 +46,7 @@ Outline of a presumably better scheme:
 #include "ast/simplifiers/solve_context_eqs.h"
 #include "ast/converters/generic_model_converter.h"
 #include "params/tactic_params.hpp"
+#include "params/smt_params_helper.hpp"
 
 
 namespace euf {
@@ -119,6 +120,9 @@ namespace euf {
                     if (m_fmls.frozen(v))
                         continue;
 
+                    if (!m_config.m_enable_non_ground && has_quantifiers(t)) 
+                        continue;                        
+
                     bool is_safe = true;                    
                     unsigned todo_sz = todo.size();
 
@@ -126,6 +130,8 @@ namespace euf {
                     // all time-stamps must be at or above current level
                     // unexplored variables that are part of substitution are appended to work list.
                     SASSERT(m_todo.empty());
+
+
                     m_todo.push_back(t);
                     expr_fast_mark1 visited;
                     while (!m_todo.empty()) {
@@ -224,6 +230,9 @@ namespace euf {
     
     void solve_eqs::reduce() {
 
+        if (!m_config.m_enabled)
+            return;
+
         m_fmls.freeze_suffix();
 
         for (extract_eq* ex : m_extract_plugins)
@@ -330,6 +339,9 @@ namespace euf {
         for (auto* ex : m_extract_plugins)
             ex->updt_params(p);
         m_rewriter.updt_params(p);
+        smt_params_helper sp(p);
+        m_config.m_enabled = sp.solve_eqs();
+        m_config.m_enable_non_ground = sp.solve_eqs_non_ground();
     }
 
     void solve_eqs::collect_param_descrs(param_descrs& r) {

src/ast/simplifiers/solve_eqs.h

@@ -41,6 +41,8 @@ namespace euf {
         struct config {
             bool m_context_solve = true;
             unsigned m_max_occs = UINT_MAX;
+            bool m_enabled = true;
+            bool m_enable_non_ground = true;
         };
 
         stats                         m_stats;

src/params/smt_params_helper.pyg

@@ -20,6 +20,7 @@ def_module_params(module_name='smt',
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
                           ('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'),
                           ('solve_eqs', BOOL, True, 'pre-processing: solve equalities'),
+                          ('solve_eqs.non_ground', BOOL, True, 'pre-processing: solve equalities. Allow eliminating variables by non-ground solutions which can break behavior for model evaluation.'),
                           ('propagate_values', BOOL, True, 'pre-processing: propagate values'),
                           ('bound_simplifier', BOOL, True, 'apply bounds simplification during pre-processing'),
                           ('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'),

src/smt/priority_queue.h

@@ -0,0 +1,191 @@
+// SOURCE: https://github.com/Ten0/updatable_priority_queue/blob/master/updatable_priority_queue.h
+
+#include <utility>
+#include <vector>
+
+namespace updatable_priority_queue {
+	template <typename Key, typename Priority>
+		struct priority_queue_node {
+			Priority priority;
+			Key key;
+			priority_queue_node(const Key& key, const Priority& priority) : priority(priority), key(key) {}
+			friend bool operator<(const priority_queue_node& pqn1, const priority_queue_node& pqn2) {
+				return pqn1.priority > pqn2.priority;
+			}
+			friend bool operator>(const priority_queue_node& pqn1, const priority_queue_node& pqn2) {
+				return pqn1.priority < pqn2.priority;
+			}
+		};
+
+	/** Key has to be an uint value (convertible to size_t)
+	 * This is a max heap (max is on top), to match stl's pQ */
+	template <typename Key, typename Priority>
+		class priority_queue {
+			protected:
+				std::vector<size_t> id_to_heappos;
+				std::vector<priority_queue_node<Key,Priority>> heap;
+				std::size_t max_size = 4; // std::numeric_limits<std::size_t>::max(); // Create a variable max_size that defaults to the largest size_t value possible
+
+			public:
+				// priority_queue() {}
+				priority_queue(std::size_t max_size = std::numeric_limits<std::size_t>::max()): max_size(max_size) {}
+
+				// Returns a const reference to the internal heap storage
+				const std::vector<priority_queue_node<Key, Priority>>& get_heap() const {
+					return heap;
+				}
+
+				bool empty()       const { return heap.empty(); }
+				std::size_t size() const { return heap.size(); }
+
+				/** first is priority, second is key */
+				const priority_queue_node<Key,Priority>& top() const { return heap.front(); }
+
+				void pop(bool remember_key=false) {
+					if(size() == 0) return;
+					id_to_heappos[heap.front().key] = -1-remember_key;
+					if(size() > 1) {
+						*heap.begin() = std::move(*(heap.end()-1));
+						id_to_heappos[heap.front().key] = 0;
+					}
+					heap.pop_back();
+					sift_down(0);
+				}
+
+				priority_queue_node<Key,Priority> pop_value(bool remember_key=true) {
+					if(size() == 0) return priority_queue_node<Key, Priority>(-1, Priority());
+					priority_queue_node<Key,Priority> ret = std::move(*heap.begin());
+					id_to_heappos[ret.key] = -1-remember_key;
+					if(size() > 1) {
+						*heap.begin() = std::move(*(heap.end()-1));
+						id_to_heappos[heap.front().key] = 0;
+					}
+					heap.pop_back();
+					sift_down(0);
+					return ret;
+				}
+
+				/** Sets the priority for the given key. If not present, it will be added, otherwise it will be updated
+				 *  Returns true if the priority was changed.
+				 * */
+				bool set(const Key& key, const Priority& priority, bool only_if_higher=false) {
+					if(key < id_to_heappos.size() && id_to_heappos[key] < ((size_t)-2)) // This key is already in the pQ
+						return update(key, priority, only_if_higher);
+					else
+						return push(key, priority, only_if_higher);
+				}
+
+				std::pair<bool,Priority> get_priority(const Key& key) {
+					if(key < id_to_heappos.size()) {
+						size_t pos = id_to_heappos[key];
+						if(pos < ((size_t)-2)) {
+							return {true, heap[pos].priority};
+						}
+					}
+					return {false, 0};
+				}
+
+				/** Returns true if the key was not inside and was added, otherwise does nothing and returns false
+				 *  If the key was remembered and only_if_unknown is true, does nothing and returns false
+				 * */
+				bool push(const Key& key, const Priority& priority, bool only_if_unknown = false) {
+    				extend_ids(key);
+					if (id_to_heappos[key] < ((size_t)-2)) return false; // already inside
+					if (only_if_unknown && id_to_heappos[key] == ((size_t)-2)) return false; // was evicted and only_if_unknown prevents re-adding
+
+					if (heap.size() < max_size) {
+						// We have room: just add new element
+						size_t n = heap.size();
+						id_to_heappos[key] = n;
+						heap.emplace_back(key, priority);
+						sift_up(n);
+						return true;
+					} else {
+						// Heap full: heap[0] is the smallest priority in the top-k (min-heap)
+						if (priority <= heap[0].priority) {
+							// New element priority too small or equal, discard it
+							return false;
+						}
+						// Evict smallest element at heap[0]
+						Key evicted_key = heap[0].key;
+						id_to_heappos[evicted_key] = -2; // Mark evicted
+
+						heap[0] = priority_queue_node<Key, Priority>(key, priority);
+						id_to_heappos[key] = 0;
+						sift_down(0); // restore min-heap property
+						return true;
+					}
+				}
+
+
+
+				/** Returns true if the key was already inside and was updated, otherwise does nothing and returns false */
+				bool update(const Key& key, const Priority& new_priority, bool only_if_higher=false) {
+					if(key >= id_to_heappos.size()) return false;
+					size_t heappos = id_to_heappos[key];
+					if(heappos >= ((size_t)-2)) return false;
+					Priority& priority = heap[heappos].priority;
+					if(new_priority > priority) {
+						priority = new_priority;
+						sift_up(heappos);
+						return true;
+					}
+					else if(!only_if_higher && new_priority < priority) {
+						priority = new_priority;
+						sift_down(heappos);
+						return true;
+					}
+					return false;
+				}
+
+				void clear() {
+					heap.clear();
+					id_to_heappos.clear();
+				}
+
+
+			private:
+				void extend_ids(Key k) {
+					size_t new_size = k+1;
+					if(id_to_heappos.size() < new_size)
+						id_to_heappos.resize(new_size, -1);
+				}
+
+				void sift_down(size_t heappos) {
+					size_t len = heap.size();
+					size_t child = heappos*2+1;
+					if(len < 2 || child >= len) return;
+					if(child+1 < len && heap[child+1] > heap[child]) ++child; // Check whether second child is higher
+					if(!(heap[child] > heap[heappos])) return; // Already in heap order
+
+					priority_queue_node<Key,Priority> val = std::move(heap[heappos]);
+					do {
+						heap[heappos] = std::move(heap[child]);
+						id_to_heappos[heap[heappos].key] = heappos;
+						heappos = child;
+						child = 2*child+1;
+						if(child >= len) break;
+						if(child+1 < len && heap[child+1] > heap[child]) ++child;
+					} while(heap[child] > val);
+					heap[heappos] = std::move(val);
+					id_to_heappos[heap[heappos].key] = heappos;
+				}
+
+				void sift_up(size_t heappos) {
+					size_t len = heap.size();
+					if(len < 2 || heappos <= 0) return;
+					size_t parent = (heappos-1)/2;
+					if(!(heap[heappos] > heap[parent])) return;
+					priority_queue_node<Key, Priority> val = std::move(heap[heappos]);
+					do {
+						heap[heappos] = std::move(heap[parent]);
+						id_to_heappos[heap[heappos].key] = heappos;
+						heappos = parent;
+						if(heappos <= 0) break;
+						parent = (parent-1)/2;
+					} while(val > heap[parent]);
+					heap[heappos] = std::move(val);
+					id_to_heappos[heap[heappos].key] = heappos;
+				}
+		};
+}

src/smt/smt_context.h

@@ -50,6 +50,7 @@ Revision History:
 #include "model/model.h"
 #include "solver/progress_callback.h"
 #include "solver/assertions/asserted_formulas.h"
+#include "smt/priority_queue.h"
 #include <tuple>
 
 // there is a significant space overhead with allocating 1000+ contexts in
@@ -189,7 +190,9 @@ namespace smt {
         unsigned_vector             m_lit_occs;    //!< occurrence count of literals
         svector<bool_var_data>      m_bdata;       //!< mapping bool_var -> data
         svector<double>             m_activity;
-        svector<double>             m_scores[2];
+        updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
+        svector<std::array<double, 2>> m_lit_scores; 
+
         clause_vector               m_aux_clauses;
         clause_vector               m_lemmas;
         vector<clause_vector>       m_clauses_to_reinit;
@@ -932,10 +935,11 @@ namespace smt {
         void dump_axiom(unsigned n, literal const* lits);
         void add_scores(unsigned n, literal const* lits);
         void reset_scores() {
-            for (auto& s : m_scores) s[0] = s[1] = 0.0;
+            for (auto& s : m_lit_scores) s[0] = s[1] = 0.0;
+            m_pq_scores.clear();  // Clear the priority queue heap as well
         }
         double get_score(literal l) const {
-            return m_scores[l.var()][l.sign()];
+            return m_lit_scores[l.var()][l.sign()];
         }
     public:        
 

src/smt/smt_internalizer.cpp

@@ -928,9 +928,8 @@ namespace smt {
         set_bool_var(id, v);
         m_bdata.reserve(v+1);
         m_activity.reserve(v+1);
-        m_scores[0].reserve(v + 1);
+        m_lit_scores.reserve(v + 1);
-        m_scores[1].reserve(v + 1);
+        m_lit_scores[v][0] = m_lit_scores[v][1] = 0.0;
-        m_scores[0][v] = m_scores[1][v] = 0.0;
         m_bool_var2expr.reserve(v+1);
         m_bool_var2expr[v] = n;
         literal l(v, false);
@@ -1528,11 +1527,25 @@ namespace smt {
         }} 
     }
 
+    // void context::add_scores(unsigned n, literal const* lits) {
+    //     for (unsigned i = 0; i < n; ++i) {
+    //         auto lit = lits[i];
+    //         unsigned v = lit.var();
+    //         m_lit_scores[v][lit.sign()] += 1.0 / n;
+    //     }
+    // }
+
     void context::add_scores(unsigned n, literal const* lits) {
         for (unsigned i = 0; i < n; ++i) {
             auto lit = lits[i];
-            unsigned v = lit.var();
+            unsigned v = lit.var(); // unique key per literal
-            m_scores[lit.sign()][v] += 1.0 / n;
+
+            auto curr_score = m_lit_scores[v][0] * m_lit_scores[v][1];
+            m_lit_scores[v][lit.sign()] += 1.0 / n;
+            
+            auto new_score = m_lit_scores[v][0] * m_lit_scores[v][1];
+            m_pq_scores.set(v, new_score);
+
         }
     }
 

src/smt/smt_parallel.cpp

@@ -92,66 +92,86 @@ namespace smt {
             sl.push_child(&(new_m->limit()));
         }
 
-        // Access socres as follows:
-        // ctx.m_scores[lit.sign()][lit.var()]
 
-        // auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
+        auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
-        //     lookahead lh(ctx);
+            lookahead lh(ctx);
-        //     c = lh.choose();
+            c = lh.choose();
-        //     if (c) {
+            if (c) {
-        //         if ((ctx.get_random_value() % 2) == 0) 
-        //             c = c.get_manager().mk_not(c);
-        //         lasms.push_back(c);
-        //     }
-        // };
-
-        auto cube = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
-            lookahead lh(ctx); // Create lookahead object to use get_score for evaluation
-
-            std::vector<std::pair<expr_ref, double>> candidates; // List of candidate literals and their scores
-            unsigned budget = 10; // Maximum number of variables to sample for building the cubes
-
-            // Loop through all Boolean variables in the context
-            for (bool_var v = 0; v < ctx.m_bool_var2expr.size(); ++v) {
-                if (ctx.get_assignment(v) != l_undef) continue; // Skip already assigned variables
-
-                expr* e = ctx.bool_var2expr(v); // Get expression associated with variable
-                if (!e) continue; // Skip if not a valid variable
-
-                literal lit(v, false); // Create literal for v = true
-
-                ctx.push_scope(); // Save solver state
-                ctx.assign(lit, b_justification::mk_axiom(), true); // Assign v = true with axiom justification
-                ctx.propagate(); // Propagate consequences of assignment
-
-                if (!ctx.inconsistent()) { // Only keep variable if assignment didn’t lead to conflict
-                    double score = lh.get_score(); // Evaluate current state using lookahead scoring
-                    candidates.emplace_back(expr_ref(e, ctx.get_manager()), score); // Store (expr, score) pair
-                }
-
-                ctx.pop_scope(1); // Restore solver state
-
-                if (candidates.size() >= budget) break; // Stop early if sample budget is exhausted
-            }
-
-            // Sort candidates in descending order by score (higher score = better)
-            std::sort(candidates.begin(), candidates.end(),
-                [](auto& a, auto& b) { return a.second > b.second; });
-
-            unsigned cube_size = 2; // compute_cube_size_from_feedback(); // NEED TO IMPLEMENT: Decide how many literals to include (adaptive)
-
-            // Select top-scoring literals to form the cube
-            for (unsigned i = 0; i < std::min(cube_size, (unsigned)candidates.size()); ++i) {
-                expr_ref lit = candidates[i].first;
-
-                // Randomly flip polarity with 50% chance (introduces polarity diversity)
                 if ((ctx.get_random_value() % 2) == 0) 
-                    lit = ctx.get_manager().mk_not(lit);
+                    c = c.get_manager().mk_not(c);
-
+                lasms.push_back(c);
-                lasms.push_back(lit); // Add literal as thread-local assumption
             }
         };
 
+        auto cube_batch_pq = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
+            unsigned k = 4; // Number of top literals you want
+            ast_manager& m = ctx.get_manager();
+
+            // Get the entire fixed-size priority queue (it's not that big)
+            auto candidates = ctx.m_pq_scores.get_heap();  // returns vector<node<key, priority>>
+
+            // Sort descending by priority (higher priority first)
+            std::sort(candidates.begin(), candidates.end(),
+                    [](const auto& a, const auto& b) { return a.priority > b.priority; });
+
+            expr_ref_vector conjuncts(m);
+            unsigned count = 0;
+
+            for (const auto& node : candidates) {
+                if (ctx.get_assignment(node.key) != l_undef) continue;
+
+                expr* e = ctx.bool_var2expr(node.key);
+                if (!e) continue;
+
+
+                expr_ref lit(e, m);
+                conjuncts.push_back(lit);
+
+                if (++count >= k) break;
+            }
+
+            c = mk_and(conjuncts);
+            lasms.push_back(c);
+        };
+
+        auto cube_batch = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
+            std::vector<std::pair<expr_ref, double>> candidates;
+            unsigned k = 4; // Get top-k scoring literals
+            ast_manager& m = ctx.get_manager();
+
+            // std::cout << ctx.m_bool_var2expr.size() << std::endl; // Prints the size of m_bool_var2expr
+            // Loop over first 100 Boolean vars
+            for (bool_var v = 0; v < 100; ++v) {
+                if (ctx.get_assignment(v) != l_undef) continue;
+
+                expr* e = ctx.bool_var2expr(v);
+                if (!e) continue;
+
+                literal lit(v, false);
+                double score = ctx.get_score(lit);
+                if (score == 0.0) continue;
+
+                candidates.emplace_back(expr_ref(e, m), score);
+            }
+
+            // Sort all candidate literals descending by score
+            std::sort(candidates.begin(), candidates.end(),
+                [](auto& a, auto& b) { return a.second > b.second; });
+
+            // Clear c and build it as conjunction of top-k
+            expr_ref_vector conjuncts(m);
+
+            for (unsigned i = 0; i < std::min(k, (unsigned)candidates.size()); ++i) {
+                expr_ref lit = candidates[i].first;
+                conjuncts.push_back(lit);
+            }
+
+            // Build conjunction and store in c
+            c = mk_and(conjuncts);
+
+            // Add the single cube formula to lasms (not each literal separately)
+            lasms.push_back(c);
+        };
 
         obj_hashtable<expr> unit_set;
         expr_ref_vector unit_trail(ctx.m);
@@ -192,33 +212,47 @@ namespace smt {
 
         std::mutex mux;
 
+        // Lambda defining the work each SMT thread performs
         auto worker_thread = [&](int i) {
             try {
+                // Get thread-specific context and AST manager
                 context& pctx = *pctxs[i];
                 ast_manager& pm = *pms[i];
+
+                // Initialize local assumptions and cube
                 expr_ref_vector lasms(pasms[i]);
                 expr_ref c(pm);
 
+                // Set the max conflict limit for this thread
                 pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts);
+
+                // Periodically generate cubes based on frequency
                 if (num_rounds > 0 && (num_rounds % pctx.get_fparams().m_threads_cube_frequency) == 0) 
-                    cube(pctx, lasms, c);
+                    cube_batch(pctx, lasms, c);
+
+                // Optional verbose logging
                 IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; 
                         if (num_rounds > 0) verbose_stream() << " :round " << num_rounds;
                         if (c) verbose_stream() << " :cube " << mk_bounded_pp(c, pm, 3);
                         verbose_stream() << ")\n";);
+
+                // Check satisfiability of assumptions
                 lbool r = pctx.check(lasms.size(), lasms.data());
 
+                // Handle results based on outcome and conflict count
                 if (r == l_undef && pctx.m_num_conflicts >= max_conflicts)
-                    ; // no-op
+                    ; // no-op, allow loop to continue
                 else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts)
-                    return;
+                    return; // quit thread early
+
+                // If cube was unsat and it's in the core, learn from it
                 else if (r == l_false && pctx.unsat_core().contains(c)) {
                     IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")");
                     pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));
                     return;
                 }
 
-
+                // Begin thread-safe update of shared result state
                 bool first = false;
                 {
                     std::lock_guard<std::mutex> lock(mux);
@@ -232,29 +266,27 @@ namespace smt {
                         finished_id = i;
                         result = r;                        
                     }
-                    else if (!first) return;
+                    else if (!first) return; // nothing new to contribute
                 }
 
+                // Cancel limits on other threads now that a result is known
                 for (ast_manager* m : pms) {
                     if (m != &pm) m->limit().cancel();
                 }
 
-            }
+            } catch (z3_error & err) {
-            catch (z3_error & err) {
                 if (finished_id == UINT_MAX) {
                     error_code = err.error_code();
                     ex_kind = ERROR_EX;
                     done = true;
                 }
-            }
+            } catch (z3_exception & ex) {
-            catch (z3_exception & ex) {
                 if (finished_id == UINT_MAX) {
                     ex_msg = ex.what();
                     ex_kind = DEFAULT_EX;
                     done = true;
                 }
-            }
+            } catch (...) {
-            catch (...) {
                 if (finished_id == UINT_MAX) {
                     ex_msg = "unknown exception";
                     ex_kind = ERROR_EX;
@@ -263,29 +295,37 @@ namespace smt {
             }
         };
 
-        // for debugging:  num_threads = 1;
+        // Thread scheduling loop
-
         while (true) {
             vector<std::thread> threads(num_threads);
+
+            // Launch threads
             for (unsigned i = 0; i < num_threads; ++i) {
                 // [&, i] is the lambda's capture clause: capture all variables by reference (&) except i, which is captured by value.
                 threads[i] = std::thread([&, i]() { worker_thread(i); });
             }
+
+            // Wait for all threads to finish
             for (auto & th : threads) {
                 th.join();
             }
+
+            // Stop if one finished with a result
             if (done) break;
 
+            // Otherwise update shared state and retry
             collect_units();
             ++num_rounds;
             max_conflicts = (max_conflicts < thread_max_conflicts) ? 0 : (max_conflicts - thread_max_conflicts);
             thread_max_conflicts *= 2;            
         }
 
+        // Gather statistics from all solver contexts
         for (context* c : pctxs) {
             c->collect_statistics(ctx.m_aux_stats);
         }
 
+        // If no thread finished successfully, throw recorded error
         if (finished_id == UINT_MAX) {
             switch (ex_kind) {
             case ERROR_EX: throw z3_error(error_code);
@@ -293,6 +333,7 @@ namespace smt {
             }
         }
 
+        // Handle result: translate model/unsat core back to main context
         model_ref mdl;        
         context& pctx = *pctxs[finished_id];
         ast_translation tr(*pms[finished_id], m);

src/smt/theory_seq.cpp

@@ -439,7 +439,6 @@ final_check_status theory_seq::final_check_eh() {
 }
 
 
-
 bool theory_seq::set_empty(expr* x) {
     add_axiom(~mk_eq(m_autil.mk_int(0), mk_len(x), false), mk_eq_empty(x));
     return true;
@@ -475,10 +474,9 @@ bool theory_seq::check_fixed_length(bool is_zero, bool check_long_strings) {
     bool found = false;    
     for (unsigned i = 0; i < m_length.size(); ++i) {
         expr* e = m_length.get(i);
-        if (fixed_length(e, is_zero, check_long_strings)) {
+        if (fixed_length(e, is_zero, check_long_strings)) 
             found = true;        
     }
-    }
     return found;
 }