prepare polysat

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

src/sat/sat_elim_eqs.cpp

@@ -229,11 +229,12 @@ namespace sat {
             literal r  = roots[v];
             SASSERT(v != r.var());
 
-            if (m_solver.m_cut_simplifier) m_solver.m_cut_simplifier->set_root(v, r);
+            if (m_solver.m_cut_simplifier)
+                m_solver.m_cut_simplifier->set_root(v, r);
+
             bool set_root = m_solver.set_root(l, r);
-            bool root_ok = !m_solver.is_external(v) || set_root;
             TRACE("elim_eqs", tout << l << " " << r << "\n";);
-            if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
+            if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !set_root))) {
                 // cannot really eliminate v, since we have to notify extension of future assignments
                 if (m_solver.m_config.m_drat) {
                     m_solver.m_drat.add(~l, r, sat::status::redundant());

src/sat/sat_solver.cpp

@@ -288,6 +288,7 @@ namespace sat {
             m_free_vars.pop_back();
             m_active_vars.push_back(v);
             reset_var(v, ext, dvar);
+            SASSERT(v < m_justification.size());
             return v;
         }
         m_active_vars.push_back(v);
@@ -3008,7 +3009,7 @@ namespace sat {
         svector<double> logits(vars.size(), 0.0);
         double itau = m_config.m_reorder_itau;
         double lse = 0;
-        double mid = m_rand.max_value()/2;
+        double mid = (double)(m_rand.max_value()/2);
         double max = 0;
         for (double& f : logits) {
             f = itau * (m_rand() - mid)/mid;
@@ -3508,7 +3509,6 @@ namespace sat {
         unsigned old_num_vars = m_vars_lim.pop(num_scopes);
         if (old_num_vars == m_active_vars.size())
             return;
-        unsigned free_vars_head = m_free_vars.size();
         unsigned sz = m_active_vars.size(), j = old_num_vars;
         unsigned new_lvl = m_scopes.size() - num_scopes;
 
@@ -3531,16 +3531,14 @@ namespace sat {
 
         for (unsigned i = old_num_vars; i < sz; ++i) {
             bool_var v = m_active_vars[i];
-            if (is_visited(v) || is_active(v)) {
+            if (is_external(v) || is_visited(v) || is_active(v)) {
                 m_vars_to_reinit.push_back(v);
                 m_active_vars[j++] = v;
                 m_var_scope[v] = new_lvl;
             }
             else {
                 set_eliminated(v, true);
-                if (!is_external(v) || true) {
-                    m_free_vars.push_back(v);                   
-                }
+                m_vars_to_free.push_back(v);                                   
             }
         }
         m_active_vars.shrink(j);
@@ -3550,8 +3548,7 @@ namespace sat {
                 IF_VERBOSE(0, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
             }
         };
-        for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) {
-            bool_var v = m_free_vars[i];
+        for (bool_var v : m_vars_to_free) {
             cleanup_watch(literal(v, false));
             cleanup_watch(literal(v, true));
             
@@ -3560,7 +3557,7 @@ namespace sat {
             tout << "clauses to reinit: " << (m_clauses_to_reinit.size() - old_sz) << "\n";
             tout << "new level:         " << new_lvl << "\n";
             tout << "vars to reinit:    " << m_vars_to_reinit << "\n";
-            tout << "free vars:         " << bool_var_vector(m_free_vars.size() - free_vars_head, m_free_vars.data() + free_vars_head) << "\n";
+            tout << "free vars:         " << bool_var_vector(m_vars_to_free) << "\n";
             for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; )
                 tout << "reinit:           " << m_clauses_to_reinit[i] << "\n";
             display(tout););        
@@ -3599,7 +3596,6 @@ namespace sat {
     void solver::pop(unsigned num_scopes) {
         if (num_scopes == 0)
             return;
-        unsigned free_vars_head = m_free_vars.size();
         if (m_ext) {
             pop_vars(num_scopes);
             m_ext->pop(num_scopes);
@@ -3609,13 +3605,16 @@ namespace sat {
         scope & s        = m_scopes[new_lvl];
         m_inconsistent   = false; // TBD: use model seems to make this redundant: s.m_inconsistent;
         unassign_vars(s.m_trail_lim, new_lvl);
-        for (unsigned i = m_free_vars.size(); i-- > free_vars_head; )
-            m_case_split_queue.del_var_eh(m_free_vars[i]);
+        for (bool_var v : m_vars_to_free)
+            m_case_split_queue.del_var_eh(v);
         m_scope_lvl -= num_scopes;
         reinit_clauses(s.m_clauses_to_reinit_lim);
         m_scopes.shrink(new_lvl);
-        if (m_ext) 
+        if (m_ext) {
             m_ext->pop_reinit();
+            m_free_vars.append(m_vars_to_free);
+            m_vars_to_free.reset();
+        }
     }
 
     void solver::unassign_vars(unsigned old_sz, unsigned new_lvl) {
@@ -3656,17 +3655,17 @@ namespace sat {
             clause_wrapper cw = m_clauses_to_reinit[i];
             bool reinit = false;
             if (cw.is_binary()) {
-                if (propagate_bin_clause(cw[0], cw[1]) && !at_base_lvl()) 
+                if (propagate_bin_clause(cw[0], cw[1]) && !at_base_lvl())
                     m_clauses_to_reinit[j++] = cw;
-                else if (has_variables_to_reinit(cw[0], cw[1]))
+                else if (has_variables_to_reinit(cw[0], cw[1]) && !at_base_lvl())
                     m_clauses_to_reinit[j++] = cw;
             }
             else {
                 clause & c = *(cw.get_clause());
                 if (ENABLE_TERNARY && c.size() == 3) {
-                    if (!at_base_lvl() && propagate_ter_clause(c))
+                    if (propagate_ter_clause(c) && !at_base_lvl())
                         m_clauses_to_reinit[j++] = cw;                
-                    else if (has_variables_to_reinit(c))
+                    else if (has_variables_to_reinit(c) && !at_base_lvl())
                         m_clauses_to_reinit[j++] = cw;
                     else 
                         c.set_reinit_stack(false);
@@ -3674,13 +3673,13 @@ namespace sat {
                 }
                 detach_clause(c);
                 attach_clause(c, reinit);
-                if (!at_base_lvl() && reinit) 
+                if (reinit && !at_base_lvl()) 
                     // clause propagated literal, must keep it in the reinit stack.
                     m_clauses_to_reinit[j++] = cw;                
-                else if (has_variables_to_reinit(c))
+                else if (has_variables_to_reinit(c) && !at_base_lvl())
                     m_clauses_to_reinit[j++] = cw;
                 else 
-                    c.set_reinit_stack(false);                
+                    c.set_reinit_stack(false);   
             }
         }
         m_clauses_to_reinit.shrink(j);
@@ -3692,6 +3691,7 @@ namespace sat {
     //
 
     void solver::user_push() {
+
         pop_to_base_level();
         m_free_var_freeze.push_back(m_free_vars);
         m_free_vars.reset(); // resetting free_vars forces new variables to be assigned above new_v

src/sat/sat_solver.h

@@ -124,7 +124,7 @@ namespace sat {
         clause_vector           m_clauses;
         clause_vector           m_learned;
         unsigned                m_num_frozen;
-        unsigned_vector         m_active_vars, m_free_vars, m_vars_to_reinit;
+        unsigned_vector         m_active_vars, m_free_vars, m_vars_to_free, m_vars_to_reinit;
         vector<watch_list>      m_watches;
         svector<lbool>          m_assignment;
         svector<justification>  m_justification; 
@@ -266,6 +266,11 @@ namespace sat {
         //
         // -----------------------
         void add_clause(unsigned num_lits, literal * lits, sat::status st) override { mk_clause(num_lits, lits, st); }
+        void add_clause(literal l1, literal l2, status st) {
+            literal lits[2] = { l1, l2 };
+            add_clause(2, lits, st);
+        }
+        void add_clause(literal lit, status st) { literal lits[1] = { lit }; add_clause(1, lits, st); }
         bool_var add_var(bool ext) override { return mk_var(ext, true); }
 
         bool_var mk_var(bool ext = false, bool dvar = true);
@@ -444,9 +449,10 @@ namespace sat {
         void       flush_roots();
         typedef std::pair<literal, literal> bin_clause;
         struct bin_clause_hash { unsigned operator()(bin_clause const& b) const { return b.first.hash() + 2*b.second.hash(); } };
-    protected:
-        watch_list & get_wlist(literal l) { return m_watches[l.index()]; }
-        watch_list const & get_wlist(literal l) const { return m_watches[l.index()]; }
+
+        watch_list const& get_wlist(literal l) const { return m_watches[l.index()]; }
+        watch_list& get_wlist(literal l) { return m_watches[l.index()]; }
+    protected:            
         watch_list & get_wlist(unsigned l_idx) { return m_watches[l_idx]; }
         bool is_marked(bool_var v) const { return m_mark[v]; }
         void mark(bool_var v) { SASSERT(!is_marked(v)); m_mark[v] = true; }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -280,8 +280,8 @@ public:
         m_inserted_const2bits.reset();
         m_map.pop(n);
         SASSERT(n <= m_num_scopes);
-        m_solver.user_pop(n);
         m_goal2sat.user_pop(n);
+        m_solver.user_pop(n);
         m_num_scopes -= n;
         // ? m_internalized_converted = false;
         m_has_uninterpreted.pop(n);
@@ -683,10 +683,15 @@ public:
         ensure_euf()->user_propagate_register_diseq(diseq_eh);
     }
     
-    unsigned user_propagate_register(expr* e) override { 
-        return ensure_euf()->user_propagate_register(e);
+    unsigned user_propagate_register_expr(expr* e) override { 
+        return ensure_euf()->user_propagate_register_expr(e);
     }
 
+    void user_propagate_register_created(user_propagator::created_eh_t& r) {
+        ensure_euf()->user_propagate_register_created(r);
+    }
+
+
 private:
 
     lbool internalize_goal(goal_ref& g) {        

src/sat/sat_solver_core.h

@@ -35,10 +35,7 @@ namespace sat {
 
         // add clauses
         virtual void add_clause(unsigned n, literal* lits, status st) = 0;
-        void add_clause(literal l1, literal l2, status st) {
-            literal lits[2] = {l1, l2};
-            add_clause(2, lits, st);
-        }
+        
         void add_clause(literal l1, literal l2, literal l3, status st) {
             literal lits[3] = {l1, l2, l3};
             add_clause(3, lits, st);

src/sat/smt/CMakeLists.txt

@@ -38,7 +38,6 @@ z3_add_component(sat_smt
     q_queue.cpp
     q_solver.cpp
     recfun_solver.cpp
-    sat_dual_solver.cpp
     sat_th.cpp
     user_solver.cpp
   COMPONENT_DEPENDENCIES

src/sat/smt/arith_axioms.cpp

@@ -49,6 +49,14 @@ namespace arith {
         }
     }
 
+    void solver::mk_abs_axiom(app* n) {
+        expr* x = nullptr;
+        VERIFY(a.is_abs(n, x));
+        literal is_nonneg = mk_literal(a.mk_ge(x, a.mk_numeral(rational::zero(), n->get_sort())));
+        add_clause(~is_nonneg, eq_internalize(n, x));
+        add_clause(is_nonneg, eq_internalize(n, a.mk_uminus(x)));
+    }
+
     // t = n^0
     void solver::mk_power0_axioms(app* t, app* n) {
         expr_ref p0(a.mk_power0(n, t->get_arg(1)), m);

src/sat/smt/arith_internalize.cpp

@@ -237,9 +237,10 @@ namespace arith {
                 if (!is_first) {
                     // skip recursive internalization
                 }
-                else if (a.is_to_int(n, n1)) {
-                    mk_to_int_axiom(t);
-                }
+                else if (a.is_to_int(n, n1)) 
+                    mk_to_int_axiom(t);                
+                else if (a.is_abs(n)) 
+                    mk_abs_axiom(t);                
                 else if (a.is_idiv(n, n1, n2)) {
                     if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
                     m_idiv_terms.push_back(n);
@@ -268,17 +269,16 @@ namespace arith {
                 }
                 else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) {
                     found_unsupported(n);
+                    ensure_arg_vars(to_app(n));
                 }
                 else {
-                    // no-op
+                    ensure_arg_vars(to_app(n));
                 }
             }
             else {
                 if (is_app(n)) {
                     internalize_args(to_app(n));
-                    for (expr* arg : *to_app(n)) 
-                        if (a.is_arith_expr(arg) && !m.is_bool(arg))
-                            internalize_term(arg);
+                    ensure_arg_vars(to_app(n));
                 }
                 theory_var v = mk_evar(n);
                 coeffs[vars.size()] = coeffs[index];
@@ -425,6 +425,12 @@ namespace arith {
             e_internalize(arg);
     }
 
+    void solver::ensure_arg_vars(app* n) {
+        for (expr* arg : *to_app(n))
+            if (a.is_real(arg) || a.is_int(arg))
+                internalize_term(arg);
+    }
+
     theory_var solver::internalize_power(app* t, app* n, unsigned p) {
         internalize_args(t, true);
         bool _has_var = has_var(t);
@@ -545,11 +551,13 @@ namespace arith {
         }
         m_left_side.clear();
         // reset the coefficients after they have been used.
-        for (unsigned i = 0; i < vars.size(); ++i) {
-            theory_var var = vars[i];
+        for (theory_var var : vars) {
             rational const& r = m_columns[var];
             if (!r.is_zero()) {
-                m_left_side.push_back(std::make_pair(r, register_theory_var_in_lar_solver(var)));
+                auto vi = register_theory_var_in_lar_solver(var);
+                if (lp::tv::is_term(vi))
+                    vi = lp().map_term_index_to_column_index(vi);
+                m_left_side.push_back(std::make_pair(r, vi));
                 m_columns[var].reset();
             }
         }

src/sat/smt/arith_solver.cpp

@@ -561,6 +561,8 @@ namespace arith {
     }
 
     void solver::dbg_finalize_model(model& mdl) {
+        if (m_not_handled)
+            return;
         bool found_bad = false;
         for (unsigned v = 0; v < get_num_vars(); ++v) {
             if (!is_bool(v))
@@ -953,6 +955,7 @@ namespace arith {
             if (n1->get_root() == n2->get_root())
                 continue;
             literal eq = eq_internalize(n1, n2);
+            ctx.mark_relevant(eq);
             if (s().value(eq) != l_true)
                 return true;
         }
@@ -1446,21 +1449,19 @@ namespace arith {
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
-        if (!m_nla) {
-            TRACE("arith", tout << "no nla\n";);
+        CTRACE("arith", !m_nla, tout << "no nla\n";);
+        if (!m_nla) 
             return l_true;
-        }
         if (!m_nla->need_check())
             return l_true;
 
         m_a1 = nullptr; m_a2 = nullptr;
         lbool r = m_nla->check(m_nla_lemma_vector);
         switch (r) {
-        case l_false: {
+        case l_false: 
             for (const nla::lemma& l : m_nla_lemma_vector)
                 false_case_of_check_nla(l);
             break;
-        }
         case l_true:
             if (assume_eqs())
                 return l_false;
@@ -1477,11 +1478,28 @@ namespace arith {
     }
 
     bool solver::include_func_interp(func_decl* f) const {
-        return 
-            a.is_div0(f) ||
-            a.is_idiv0(f) ||
-            a.is_power0(f) ||
-            a.is_rem0(f) ||
-            a.is_mod0(f);        
+        SASSERT(f->get_family_id() == get_id());
+        switch (f->get_decl_kind()) {
+        case OP_ADD:
+        case OP_SUB:
+        case OP_UMINUS:
+        case OP_MUL:
+        case OP_LE:
+        case OP_LT:
+        case OP_GE:
+        case OP_GT:
+        case OP_MOD:
+        case OP_REM:
+        case OP_DIV:
+        case OP_IDIV:
+        case OP_POWER:
+        case OP_IS_INT:
+        case OP_TO_INT:
+        case OP_TO_REAL:
+        case OP_NUM:
+            return false;
+        default:
+            return true;            
+        }
     }
 }

src/sat/smt/arith_solver.h

@@ -239,6 +239,7 @@ namespace arith {
         void add_def_constraint(lp::constraint_index index, theory_var v);
         void add_def_constraint_and_equality(lpvar vi, lp::lconstraint_kind kind, const rational& bound);
         void internalize_args(app* t, bool force = false);
+        void ensure_arg_vars(app* t);
         theory_var internalize_power(app* t, app* n, unsigned p);
         theory_var internalize_mul(app* t);
         theory_var internalize_def(expr* term);
@@ -263,6 +264,7 @@ namespace arith {
         // axioms
         void mk_div_axiom(expr* p, expr* q);
         void mk_to_int_axiom(app* n);
+        void mk_abs_axiom(app* n);
         void mk_is_int_axiom(expr* n);
         void mk_idiv_mod_axioms(expr* p, expr* q);
         void mk_rem_axiom(expr* dividend, expr* divisor);
@@ -445,6 +447,8 @@ namespace arith {
         bool is_shared(theory_var v) const override;
         lbool get_phase(bool_var v) override;
         bool include_func_interp(func_decl* f) const override;
+        bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); }
+        bool has_unhandled() const override { return m_not_handled != nullptr; }
 
         // bounds and equality propagation callbacks
         lp::lar_solver& lp() { return *m_solver; }

src/sat/smt/array_axioms.cpp

@@ -57,8 +57,6 @@ namespace array {
 
     bool solver::assert_axiom(unsigned idx) {
         axiom_record& r = m_axiom_trail[idx];
-        if (!is_relevant(r))
-            return false;
         switch (r.m_kind) {
         case axiom_record::kind_t::is_store:
             return assert_store_axiom(to_app(r.n->get_expr()));
@@ -86,35 +84,12 @@ namespace array {
             return assert_default_const_axiom(to_app(child));
         else if (a.is_store(child))
             return assert_default_store_axiom(to_app(child));
-        else if (a.is_map(child))
+        else if (is_map_combinator(child))
             return assert_default_map_axiom(to_app(child));
         else
             return false;                
     }
 
-
-    bool solver::is_relevant(axiom_record const& r) const {
-        return true;
-#if 0
-        // relevancy propagation is currently incomplete on terms
-
-        expr* child = r.n->get_expr();
-        switch (r.m_kind) {
-        case axiom_record::kind_t::is_select: {
-            app* select = r.select->get_app();
-            for (unsigned i = 1; i < select->get_num_args(); ++i)
-                if (!ctx.is_relevant(select->get_arg(i)))
-                    return false;
-            return ctx.is_relevant(child);            
-        }
-        case axiom_record::kind_t::is_default:
-            return ctx.is_relevant(child);            
-        default:
-            return true;
-        }
-#endif
-    }
-
     bool solver::assert_select(unsigned idx, axiom_record& r) {
         expr* child = r.n->get_expr();
         app* select = r.select->get_app();
@@ -140,7 +115,7 @@ namespace array {
             return assert_select_as_array_axiom(select, to_app(child));
         else if (a.is_store(child))
             return assert_select_store_axiom(select, to_app(child));
-        else if (a.is_map(child))
+        else if (is_map_combinator(child))
             return assert_select_map_axiom(select, to_app(child));
         else if (is_lambda(child))
             return assert_select_lambda_axiom(select, child);
@@ -215,10 +190,17 @@ namespace array {
             return new_prop;
         
         sat::literal sel_eq = sat::null_literal;
+        auto ensure_relevant = [&](sat::literal lit) {
+            if (ctx.is_relevant(lit))
+                return;
+            new_prop = true;
+            ctx.mark_relevant(lit);            
+        };
         auto init_sel_eq = [&]() {
             if (sel_eq != sat::null_literal) 
                 return true;
             sel_eq = mk_literal(sel_eq_e);
+            ensure_relevant(sel_eq);
             return s().value(sel_eq) != l_true;
         };
 
@@ -235,6 +217,7 @@ namespace array {
                 break;
             }
             sat::literal idx_eq = eq_internalize(idx1, idx2);
+            ensure_relevant(idx_eq);
             if (s().value(idx_eq) == l_true)
                 continue;
             if (s().value(idx_eq) == l_undef)
@@ -253,8 +236,7 @@ namespace array {
      * Assert
      *    select(const(v), i) = v
      */
-    bool solver::assert_select_const_axiom(app* select, app* cnst) {
-        
+    bool solver::assert_select_const_axiom(app* select, app* cnst) {        
         ++m_stats.m_num_select_const_axiom;
         expr* val = nullptr;
         VERIFY(a.is_const(cnst, val));
@@ -291,16 +273,19 @@ namespace array {
         return add_clause(lit1, ~lit2);
     }
 
+    bool solver::is_map_combinator(expr* map) const {
+        return a.is_map(map) || a.is_union(map) || a.is_intersect(map) || a.is_difference(map) || a.is_complement(map);
+    }
+
     /**
     * Assert axiom:
     * select(map[f](a, ... d), i) = f(select(a,i),...,select(d,i))
     */
     bool solver::assert_select_map_axiom(app* select, app* map) {
         ++m_stats.m_num_select_map_axiom;
-        SASSERT(a.is_map(map));
         SASSERT(a.is_select(select));
+        SASSERT(is_map_combinator(map));
         SASSERT(map->get_num_args() > 0);
-        func_decl* f = a.get_map_func_decl(map);
         unsigned num_args = select->get_num_args();
         ptr_buffer<expr> args1, args2;
         vector<ptr_vector<expr> > args2l;
@@ -321,7 +306,8 @@ namespace array {
 
         expr_ref sel1(m), sel2(m);
         sel1 = a.mk_select(args1);
-        sel2 = m.mk_app(f, args2);
+        sel2 = apply_map(map, args2.size(), args2.data());
+
         rewrite(sel2); 
         euf::enode* n1 = e_internalize(sel1);
         euf::enode* n2 = e_internalize(sel2);
@@ -348,21 +334,44 @@ namespace array {
         return ctx.propagate(n1, n2, array_axiom());
     }
 
+    expr_ref solver::apply_map(app* map, unsigned n, expr* const* args) {
+        expr_ref result(m);
+        if (a.is_map(map)) 
+            result = m.mk_app(a.get_map_func_decl(map), n, args);
+        else if (a.is_union(map)) 
+            result = m.mk_or(n, args);
+        else if (a.is_intersect(map)) 
+            result = m.mk_and(n, args);
+        else if (a.is_difference(map)) {
+            SASSERT(n > 0);
+            result = args[0];
+            for (unsigned i = 1; i < n; ++i)
+                result = m.mk_and(result, m.mk_not(args[i]));
+        }
+        else if (a.is_complement(map)) {
+            SASSERT(n == 1);
+            result = m.mk_not(args[0]);
+        }
+        else {            
+            UNREACHABLE();
+        }
+        rewrite(result);
+        return result;
+    }
+
+
     /**
      * Assert:
      *    default(map[f](a,..,d)) = f(default(a),..,default(d))
      */
     bool solver::assert_default_map_axiom(app* map) {
         ++m_stats.m_num_default_map_axiom;
-        SASSERT(a.is_map(map));
-        func_decl* f = a.get_map_func_decl(map);
-        SASSERT(map->get_num_args() == f->get_arity());
+        SASSERT(is_map_combinator(map));
         expr_ref_vector args2(m);
         for (expr* arg : *map)
             args2.push_back(a.mk_default(arg));
         expr_ref def1(a.mk_default(map), m);
-        expr_ref def2(m.mk_app(f, args2), m);
-        rewrite(def2);
+        expr_ref def2 = apply_map(map, args2.size(), args2.data());
         return ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom());
     }
 
@@ -534,11 +543,14 @@ namespace array {
         unsigned num_vars = get_num_vars();
         bool change = false;
         for (unsigned v = 0; v < num_vars; v++) {
-            propagate_parent_select_axioms(v);
             auto& d = get_var_data(v);
             if (!d.m_prop_upward)
                 continue;
             euf::enode* n = var2enode(v);
+            if (!ctx.is_relevant(n))
+                continue;
+            for (euf::enode* lambda : d.m_parent_lambdas)
+                propagate_select_axioms(d, lambda);
             if (add_as_array_eqs(n))
                 change = true;
             bool has_default = false;
@@ -552,8 +564,8 @@ namespace array {
         m_delay_qhead = 0;
         
         for (; m_delay_qhead < sz; ++m_delay_qhead) 
-            if (m_axiom_trail[m_delay_qhead].is_delayed() && assert_axiom(m_delay_qhead))
-                change = true;  
+            if (m_axiom_trail[m_delay_qhead].is_delayed() && assert_axiom(m_delay_qhead)) 
+                change = true;              
         flet<bool> _enable_delay(m_enable_delay, false);
         if (unit_propagate())
             change = true;
@@ -567,6 +579,8 @@ namespace array {
             return false;
         for (unsigned i = 0; i < ctx.get_egraph().enodes_of(f).size(); ++i) {
             euf::enode* p = ctx.get_egraph().enodes_of(f)[i];
+            if (!ctx.is_relevant(p))
+                continue;
             expr_ref_vector select(m);
             select.push_back(n->get_expr());
             for (expr* arg : *to_app(p->get_expr()))
@@ -574,7 +588,8 @@ namespace array {
             expr_ref _e(a.mk_select(select.size(), select.data()), m);
             euf::enode* e = e_internalize(_e);
             if (e->get_root() != p->get_root()) {
-                add_unit(eq_internalize(_e, p->get_expr()));
+                sat::literal eq = eq_internalize(_e, p->get_expr());
+                add_unit(eq);
                 change = true;
             }
         }
@@ -594,13 +609,12 @@ namespace array {
                 expr* e2 = var2expr(v2);
                 if (e1->get_sort() != e2->get_sort())
                     continue;
-                if (must_have_different_model_values(v1, v2)) {
-                    continue;
-                }
-                if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) {
-                    continue;
-                }
+                if (must_have_different_model_values(v1, v2)) 
+                    continue;                
+                if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) 
+                    continue;                
                 sat::literal lit = eq_internalize(e1, e2);
+                ctx.mark_relevant(lit);
                 if (s().value(lit) == l_undef) 
                     prop = true;
             }
@@ -612,10 +626,11 @@ namespace array {
         ptr_buffer<euf::enode> to_unmark;
         unsigned num_vars = get_num_vars();
         for (unsigned i = 0; i < num_vars; i++) {
-            euf::enode * n = var2enode(i);
-            
+            euf::enode * n = var2enode(i);            
             if (!is_array(n)) 
-                continue;            
+                continue;
+            if (!ctx.is_relevant(n))
+                continue;
             euf::enode * r = n->get_root();
             if (r->is_marked1()) 
                 continue;            

src/sat/smt/array_internalize.cpp

@@ -49,7 +49,7 @@ namespace array {
         if (v == euf::null_theory_var) {
             mk_var(n);
             if (is_lambda(n->get_expr()))
-                internalize_lambda(n);
+                internalize_lambda_eh(n);
         }
     }
 
@@ -57,45 +57,6 @@ namespace array {
         ensure_var(n);
     }
 
-    void solver::internalize_store(euf::enode* n) {
-        add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n);   
-        push_axiom(store_axiom(n));
-        add_lambda(n->get_th_var(get_id()), n);
-        SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
-    }
-
-    void solver::internalize_map(euf::enode* n) {
-        for (auto* arg : euf::enode_args(n)) {
-            add_parent_lambda(arg->get_th_var(get_id()), n);
-            set_prop_upward(arg);
-        }
-        push_axiom(default_axiom(n));
-        add_lambda(n->get_th_var(get_id()), n);
-        SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
-    }
-
-    void solver::internalize_lambda(euf::enode* n) {
-        SASSERT(is_lambda(n->get_expr()) || a.is_const(n->get_expr()) || a.is_as_array(n->get_expr()));
-        theory_var v = n->get_th_var(get_id());
-        push_axiom(default_axiom(n));
-        add_lambda(v, n);
-        set_prop_upward(v);
-    }
-
-    void solver::internalize_select(euf::enode* n) {
-        add_parent_select(n->get_arg(0)->get_th_var(get_id()), n);
-    }
-
-    void solver::internalize_ext(euf::enode* n) {
-        SASSERT(is_array(n->get_arg(0)));
-        push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
-    }
-
-    void solver::internalize_default(euf::enode* n) {
-        add_parent_default(n->get_arg(0)->get_th_var(get_id()), n);
-        set_prop_upward(n);
-    }
-
     bool solver::visited(expr* e) {
         euf::enode* n = expr2enode(e);
         return n && n->is_attached_to(get_id());        
@@ -116,7 +77,8 @@ namespace array {
 
     bool solver::post_visit(expr* e, bool sign, bool root) {
         euf::enode* n = expr2enode(e);
-        app* a = to_app(e);        
+        app *a = to_app(e);
+        (void)a;
         SASSERT(!n || !n->is_attached_to(get_id()));
         if (!n) 
             n = mk_enode(e, false);
@@ -124,40 +86,111 @@ namespace array {
             mk_var(n);
         for (auto* arg : euf::enode_args(n))
             ensure_var(arg);  
-        switch (a->get_decl_kind()) {
-        case OP_STORE:           
-            internalize_store(n); 
+        internalize_eh(n);
+        if (ctx.is_relevant(n))
+            relevant_eh(n);
+        return true;
+    }
+
+    void solver::internalize_lambda_eh(euf::enode* n) {
+        push_axiom(default_axiom(n));
+        auto& d = get_var_data(find(n));
+        ctx.push_vec(d.m_lambdas, n);
+    }
+
+    void solver::internalize_eh(euf::enode* n) {
+        switch (n->get_decl()->get_decl_kind()) {
+        case OP_STORE:          
+            ctx.push_vec(get_var_data(find(n)).m_lambdas, n);
+            push_axiom(store_axiom(n));
             break;
-        case OP_SELECT:          
-            internalize_select(n); 
+        case OP_SELECT:
             break;
         case OP_AS_ARRAY:
-        case OP_CONST_ARRAY:     
-            internalize_lambda(n); 
+        case OP_CONST_ARRAY:
+            internalize_lambda_eh(n);
             break;
-        case OP_ARRAY_EXT:       
-            internalize_ext(n); 
+        case OP_ARRAY_EXT:
+            SASSERT(is_array(n->get_arg(0)));
+            push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
             break;
-        case OP_ARRAY_DEFAULT:   
-            internalize_default(n); 
+        case OP_ARRAY_DEFAULT:
+            add_parent_default(find(n->get_arg(0)), n);
             break;
-        case OP_ARRAY_MAP:       
-            internalize_map(n); 
+        case OP_ARRAY_MAP:
+        case OP_SET_UNION:
+        case OP_SET_INTERSECT:
+        case OP_SET_DIFFERENCE:
+        case OP_SET_COMPLEMENT:
+            for (auto* arg : euf::enode_args(n)) 
+                add_parent_lambda(find(arg), n);
+            internalize_lambda_eh(n);
             break;
-        case OP_SET_UNION:       
-        case OP_SET_INTERSECT:   
-        case OP_SET_DIFFERENCE:  
-        case OP_SET_COMPLEMENT:  
-        case OP_SET_SUBSET:      
-        case OP_SET_HAS_SIZE:    
-        case OP_SET_CARD:        
-            ctx.unhandled_function(a->get_decl()); 
+        case OP_SET_SUBSET: {
+            expr* x, *y;
+            VERIFY(a.is_subset(n->get_expr(), x, y));
+            expr_ref diff(a.mk_setminus(x, y), m);
+            expr_ref emp(a.mk_empty_set(x->get_sort()), m);
+            sat::literal eq = eq_internalize(diff, emp);
+            sat::literal sub = expr2literal(n->get_expr());
+            add_equiv(eq, sub);
+            break;
+        }            
+        case OP_SET_HAS_SIZE:
+        case OP_SET_CARD:
+            ctx.unhandled_function(n->get_decl());
             break;
         default:
             UNREACHABLE();
-            break;            
+            break;
+        }
+    }
+
+    void solver::relevant_eh(euf::enode* n) {
+        if (is_lambda(n->get_expr())) {
+            set_prop_upward(find(n));
+            return;
+        }
+        if (!is_app(n->get_expr()))
+            return;
+        if (n->get_decl()->get_family_id() != a.get_family_id())
+            return;
+        switch (n->get_decl()->get_decl_kind()) {
+        case OP_STORE:
+            add_parent_lambda(find(n->get_arg(0)), n);   
+            break;
+        case OP_SELECT:
+            add_parent_select(find(n->get_arg(0)), n);
+            break;
+        case OP_CONST_ARRAY:
+        case OP_AS_ARRAY:
+            set_prop_upward(find(n));            
+            propagate_parent_default(find(n));
+            break;
+        case OP_ARRAY_EXT:
+            break;
+        case OP_ARRAY_DEFAULT:
+            set_prop_upward(find(n->get_arg(0)));
+            break;
+        case OP_ARRAY_MAP:
+        case OP_SET_UNION:
+        case OP_SET_INTERSECT:
+        case OP_SET_DIFFERENCE:
+        case OP_SET_COMPLEMENT:
+            for (auto* arg : euf::enode_args(n)) 
+                set_prop_upward_store(arg);
+            set_prop_upward(find(n));
+            break;
+        case OP_SET_SUBSET:
+            break;
+        case OP_SET_HAS_SIZE:
+        case OP_SET_CARD:
+            ctx.unhandled_function(n->get_decl());
+            break;
+        default:
+            UNREACHABLE();
+            break;
         }
-        return true;
     }
 
     /**

src/sat/smt/array_model.cpp

@@ -60,6 +60,11 @@ namespace array {
         ptr_vector<expr> args;
         sort* srt = n->get_sort();
         n = n->get_root();
+        if (a.is_as_array(n->get_expr())) {
+            values.set(n->get_expr_id(), n->get_expr());
+            return;
+        }
+            
         unsigned arity = get_array_arity(srt);
         func_decl * f    = mk_aux_decl_for_array_sort(m, srt);
         func_interp * fi = alloc(func_interp, m, arity);

src/sat/smt/array_solver.cpp

@@ -186,17 +186,16 @@ namespace array {
         if (should_set_prop_upward(d))
             set_prop_upward(d);
         ctx.push_vec(d.m_lambdas, lambda);
-        if (should_set_prop_upward(d)) {
-            set_prop_upward(lambda);
-            propagate_select_axioms(d, lambda);
-        }
+        propagate_select_axioms(d, lambda);
+        if (should_set_prop_upward(d)) 
+            set_prop_upward_store(lambda);                    
     }
 
     void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) {
         SASSERT(can_beta_reduce(lambda));
         auto& d = get_var_data(find(v_child));
         ctx.push_vec(d.m_parent_lambdas, lambda);
-        if (should_set_prop_upward(d))
+        if (should_prop_upward(d))        
             propagate_select_axioms(d, lambda);
     }
 
@@ -231,6 +230,9 @@ namespace array {
         for (euf::enode* lambda : d.m_lambdas) 
             propagate_select_axioms(d, lambda);        
         
+        if (!should_prop_upward(d))
+            return;
+
         for (euf::enode* lambda : d.m_parent_lambdas)
             propagate_select_axioms(d, lambda);
     }
@@ -246,14 +248,14 @@ namespace array {
         set_prop_upward(d);
     }
 
-    void solver::set_prop_upward(euf::enode* n) {
+    void solver::set_prop_upward_store(euf::enode* n) {
         if (a.is_store(n->get_expr()))
             set_prop_upward(n->get_arg(0)->get_th_var(get_id()));
     }
 
     void solver::set_prop_upward(var_data& d) {
         for (auto* p : d.m_lambdas)
-            set_prop_upward(p);
+            set_prop_upward_store(p);
     }
 
     /**
@@ -273,6 +275,6 @@ namespace array {
     }
 
     bool solver::can_beta_reduce(expr* c) const {
-        return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || a.is_map(c);
+        return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || is_map_combinator(c);
     }
 }

src/sat/smt/array_solver.h

@@ -66,6 +66,7 @@ namespace array {
         array_union_find                     m_find;
 
         theory_var find(theory_var v) { return m_find.find(v); }
+        theory_var find(euf::enode* n) { return find(n->get_th_var(get_id())); }
         func_decl_ref_vector const& sort2diff(sort* s);
 
         // internalize
@@ -73,12 +74,8 @@ namespace array {
         bool visited(expr* e) override;
         bool post_visit(expr* e, bool sign, bool root) override;
         void ensure_var(euf::enode* n);
-        void internalize_store(euf::enode* n);
-        void internalize_select(euf::enode* n);
-        void internalize_lambda(euf::enode* n);
-        void internalize_ext(euf::enode* n);
-        void internalize_default(euf::enode* n);
-        void internalize_map(euf::enode* n);
+        void internalize_eh(euf::enode* n);
+        void internalize_lambda_eh(euf::enode* n);
 
         // axioms
         struct axiom_record {
@@ -157,7 +154,6 @@ namespace array {
         bool assert_axiom(unsigned idx);
         bool assert_select(unsigned idx, axiom_record & r);
         bool assert_default(axiom_record & r);
-        bool is_relevant(axiom_record const& r) const;
         void set_applied(unsigned idx) { m_axiom_trail[idx].set_applied(); }
         bool is_applied(unsigned idx) const { return m_axiom_trail[idx].is_applied(); }
         bool is_delayed(unsigned idx) const { return m_axiom_trail[idx].is_delayed(); }
@@ -185,7 +181,9 @@ namespace array {
         bool assert_congruent_axiom(expr* e1, expr* e2);
         bool add_delayed_axioms();
         bool add_as_array_eqs(euf::enode* n);
-        
+        expr_ref apply_map(app* map, unsigned n, expr* const* args);
+        bool is_map_combinator(expr* e) const;
+
         bool has_unitary_domain(app* array_term);
         bool has_large_domain(expr* array_term);
         std::pair<app*, func_decl*> mk_epsilon(sort* s);
@@ -197,7 +195,7 @@ namespace array {
         // solving          
         void add_parent_select(theory_var v_child, euf::enode* select);
         void add_parent_default(theory_var v_child, euf::enode* def);
-        void add_lambda(theory_var v, euf::enode* lambda);
+        void add_lambda(theory_var v, euf::enode* lambda);        
         void add_parent_lambda(theory_var v_child, euf::enode* lambda);
 
         void propagate_select_axioms(var_data const& d, euf::enode* a);
@@ -206,7 +204,7 @@ namespace array {
 
         void set_prop_upward(theory_var v);
         void set_prop_upward(var_data& d);
-        void set_prop_upward(euf::enode* n);
+        void set_prop_upward_store(euf::enode* n);
         unsigned get_lambda_equiv_size(var_data const& d) const;
         bool should_set_prop_upward(var_data const& d) const;
         bool should_prop_upward(var_data const& d) const;
@@ -256,6 +254,7 @@ namespace array {
         void new_diseq_eh(euf::th_eq const& eq) override;
         bool unit_propagate() override;
         void init_model() override;
+        bool include_func_interp(func_decl* f) const override { return a.is_ext(f); }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
@@ -264,7 +263,9 @@ namespace array {
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override;
         bool enable_self_propagate() const override { return true; }
-
+        void relevant_eh(euf::enode* n) override;
+        bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_array(n->get_sort()); }
+ 
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
         void unmerge_eh(theory_var v1, theory_var v2) {}

src/sat/smt/bv_delay_internalize.cpp

@@ -21,7 +21,10 @@ Author:
 namespace bv {
 
     bool solver::check_delay_internalized(expr* e) {
-        if (!ctx.is_relevant(e))
+        euf::enode* n = expr2enode(e);
+        if (!n)
+            return true;
+        if (!ctx.is_relevant(n))
             return true;
         if (get_internalize_mode(e) != internalize_mode::delay_i)
             return true;
@@ -247,7 +250,7 @@ namespace bv {
             return;
         expr_ref tmp = literal2expr(bits.back());
         for (unsigned i = bits.size() - 1; i-- > 0; ) {
-            auto b = bits[i];
+            sat::literal b = bits[i];
             tmp = m.mk_or(literal2expr(b), tmp);
             xs.push_back(tmp);
         }
@@ -356,10 +359,28 @@ namespace bv {
     solver::internalize_mode solver::get_internalize_mode(expr* e) {
         if (!bv.is_bv(e))
             return internalize_mode::no_delay_i;
-        if (!get_config().m_bv_delay)
-            return internalize_mode::no_delay_i;
         if (!reflect())
             return internalize_mode::no_delay_i;
+        if (get_config().m_bv_polysat) {
+            switch (to_app(e)->get_decl_kind()) {
+            case OP_BMUL: 
+            case OP_BUMUL_NO_OVFL:
+            case OP_BSMOD_I:
+            case OP_BUREM_I:
+            case OP_BUDIV_I:
+            case OP_BADD:
+                return internalize_mode::polysat_i;
+            case OP_BSMUL_NO_OVFL:
+            case OP_BSMUL_NO_UDFL:
+            case OP_BSDIV_I: 
+            case OP_BSREM_I:
+            default:
+                return internalize_mode::no_delay_i;
+            }
+        }
+
+        if (!get_config().m_bv_delay)
+            return internalize_mode::no_delay_i;
         internalize_mode mode;
         switch (to_app(e)->get_decl_kind()) {
         case OP_BMUL: 

src/sat/smt/bv_internalize.cpp

@@ -144,10 +144,16 @@ namespace bv {
         SASSERT(!n->is_attached_to(get_id()));
         mk_var(n);
         SASSERT(n->is_attached_to(get_id()));
-        if (internalize_mode::no_delay_i != get_internalize_mode(a)) 
-            mk_bits(n->get_th_var(get_id()));
-        else
+        switch (get_internalize_mode(a)) {
+        case internalize_mode::no_delay_i:
             internalize_circuit(a);
+            break;
+        case internalize_mode::polysat_i:
+            NOT_IMPLEMENTED_YET();
+            break;
+        default:
+            mk_bits(n->get_th_var(get_id()));
+        }
         return true;
     }
 
@@ -166,6 +172,7 @@ namespace bv {
 #define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
 #define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
 #define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun);
+#define if_unary(F) if (a->get_num_args() == 1) { internalize_un(F); break; }
 
         switch (a->get_decl_kind()) {
         case OP_BV_NUM:           internalize_num(a); break;
@@ -190,7 +197,7 @@ namespace bv {
         case OP_BXOR:             internalize_ac(mk_xor); break;
         case OP_BNAND:            internalize_bin(mk_nand); break;
         case OP_BNOR:             internalize_bin(mk_nor); break;
-        case OP_BXNOR:            internalize_bin(mk_xnor); break;
+        case OP_BXNOR:            if_unary(mk_not); internalize_bin(mk_xnor); break;
         case OP_BCOMP:            internalize_bin(mk_comp); break;        
         case OP_SIGN_EXT:         internalize_pun(mk_sign_extend); break;
         case OP_ZERO_EXT:         internalize_pun(mk_zero_extend); break;
@@ -370,6 +377,7 @@ namespace bv {
         if (m_true == sat::null_literal) {
             ctx.push(value_trail<sat::literal>(m_true));
             m_true = ctx.internalize(m.mk_true(), false, true, false);
+            s().assign_unit(m_true);
         }
         return m_true;
     }
@@ -426,7 +434,6 @@ namespace bv {
         expr_ref sum(m_autil.mk_add(sz, args.data()), m);
         sat::literal lit = eq_internalize(n, sum);
 	add_unit(lit);
-	ctx.add_root(lit);
     }
 
     void solver::internalize_int2bv(app* n) {
@@ -456,7 +463,6 @@ namespace bv {
         rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
 	sat::literal eq_lit = eq_internalize(lhs, rhs);
 	add_unit(eq_lit);
-	ctx.add_root(eq_lit);
        
         expr_ref_vector n_bits(m);
         get_bits(n_enode, n_bits);
@@ -469,7 +475,6 @@ namespace bv {
             lhs = n_bits.get(i);
 	    eq_lit = eq_internalize(lhs, rhs);
 	    add_unit(eq_lit);
-	    ctx.add_root(eq_lit);
         }
     }
 
@@ -535,7 +540,6 @@ namespace bv {
         if (p.hi_div0()) {
             eq_lit = eq_internalize(n, ibin(arg1, arg2));
 	    add_unit(eq_lit);
-	    ctx.add_root(eq_lit);
 	}
 	else {
 	    unsigned sz = bv.get_bv_size(n);
@@ -653,7 +657,6 @@ namespace bv {
         mk_bits(get_th_var(e));
 	sat::literal eq_lit = eq_internalize(e, r);
         add_unit(eq_lit);
-	ctx.add_root(eq_lit);
     }
 
     void solver::internalize_bit2bool(app* n) {

src/sat/smt/bv_solver.cpp

@@ -58,6 +58,15 @@ namespace bv {
         m_bb.set_flat(false);
     }
 
+    bool solver::is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) {
+        numeral n;
+        if (!get_fixed_value(v, n))
+            return false;
+        val = bv.mk_numeral(n, m_bits[v].size());
+        lits.append(m_bits[v]);
+        return true;
+    }
+
     void solver::fixed_var_eh(theory_var v1) {
         numeral val1, val2;
         VERIFY(get_fixed_value(v1, val1));
@@ -158,7 +167,7 @@ namespace bv {
         SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
         TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2););
         m_stats.m_num_diseq_static++;
-        expr_ref eq = mk_var_eq(v1, v2);
+        expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m);
         add_unit(~ctx.internalize(eq, false, false, m_is_redundant));
     }
 
@@ -740,6 +749,7 @@ namespace bv {
     void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
 
         TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";);
+
         if (!merge_zero_one_bits(r1, r2)) {
             TRACE("bv", tout << "conflict detected\n";);
             return; // conflict was detected

src/sat/smt/bv_solver.h

@@ -226,6 +226,7 @@ namespace bv {
         void get_bits(euf::enode* n, expr_ref_vector& r);
         void get_arg_bits(app* n, unsigned idx, expr_ref_vector& r);
         void fixed_var_eh(theory_var v);
+        bool is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) override;
         bool is_bv(theory_var v) const { return bv.is_bv(var2expr(v)); }
         void register_true_false_bit(theory_var v, unsigned i);
         void add_bit(theory_var v, sat::literal lit);
@@ -266,6 +267,7 @@ namespace bv {
         enum class internalize_mode {
             delay_i,
             no_delay_i,
+            polysat_i,
             init_bits_only_i
         };
 

src/sat/smt/euf_ackerman.cpp

@@ -99,14 +99,38 @@ namespace euf {
         m_tmp_inference->init(m_tmp_inference);
     }
 
+    bool ackerman::enable_cc(app* a, app* b) {
+        if (!s.enable_ackerman_axioms(a))
+            return false;
+        if (!s.enable_ackerman_axioms(b))
+            return false;
+        for (expr* arg : *a)
+            if (!s.enable_ackerman_axioms(arg))
+                return false;
+        for (expr* arg : *b)
+            if (!s.enable_ackerman_axioms(arg))
+                return false;
+        return true;
+    }
+
+    bool ackerman::enable_eq(expr* a, expr* b, expr* c) {
+        return s.enable_ackerman_axioms(a) && 
+            s.enable_ackerman_axioms(b) && 
+            s.enable_ackerman_axioms(c);           
+    }
+
     void ackerman::cg_conflict_eh(expr * n1, expr * n2) {
         if (!is_app(n1) || !is_app(n2))
             return;
+        if (!s.enable_ackerman_axioms(n1))
+            return;
         SASSERT(!s.m_drating);
         app* a = to_app(n1);
         app* b = to_app(n2);
         if (a->get_decl() != b->get_decl() || a->get_num_args() != b->get_num_args())
             return;
+        if (!enable_cc(a, b))
+            return;
         TRACE("ack", tout << "conflict eh: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";);
         insert(a, b);
         gc();
@@ -117,6 +141,8 @@ namespace euf {
             return;
         if (s.m_drating)
             return;
+        if (!enable_eq(a, b, c))
+            return;
         TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";);
         insert(a, b, c);
         gc();
@@ -128,6 +154,8 @@ namespace euf {
         TRACE("ack", tout << "used cc: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";);
         SASSERT(a->get_decl() == b->get_decl());
         SASSERT(a->get_num_args() == b->get_num_args());
+        if (!enable_cc(a, b))
+            return;
         insert(a, b);
         gc();
     }
@@ -173,13 +201,13 @@ namespace euf {
         app* b = to_app(_b);
         TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
         sat::literal_vector lits;
-        unsigned sz = a->get_num_args();
+        unsigned sz = a->get_num_args();        
         
         for (unsigned i = 0; i < sz; ++i) {
-            expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m);
+            expr_ref eq = s.mk_eq(a->get_arg(i), b->get_arg(i));
             lits.push_back(~s.mk_literal(eq));
         }
-        expr_ref eq(m.mk_eq(a, b), m);
+        expr_ref eq = s.mk_eq(a, b);
         lits.push_back(s.mk_literal(eq));
         s.s().mk_clause(lits, sat::status::th(true, m.get_basic_family_id()));
     }
@@ -187,9 +215,9 @@ namespace euf {
     void ackerman::add_eq(expr* a, expr* b, expr* c) {
         flet<bool> _is_redundant(s.m_is_redundant, true);
         sat::literal lits[3];
-        expr_ref eq1(m.mk_eq(a, c), m);
-        expr_ref eq2(m.mk_eq(b, c), m);
-        expr_ref eq3(m.mk_eq(a, b), m);
+        expr_ref eq1(s.mk_eq(a, c), m);
+        expr_ref eq2(s.mk_eq(b, c), m);
+        expr_ref eq3(s.mk_eq(a, b), m);
         TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";);
         lits[0] = ~s.mk_literal(eq1);
         lits[1] = ~s.mk_literal(eq2);

src/sat/smt/euf_ackerman.h

@@ -70,6 +70,9 @@ namespace euf {
         void add_cc(expr* a, expr* b);
         void add_eq(expr* a, expr* b, expr* c);        
         void gc();
+        bool enable_cc(app* a, app* b);
+        bool enable_eq(expr* a, expr* b, expr* c);
+
 
     public:
         ackerman(solver& s, ast_manager& m);

src/sat/smt/euf_internalize.cpp

@@ -162,31 +162,34 @@ namespace euf {
             sat::literal lit2 = literal(v, false);
             s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
             s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
-            if (relevancy_enabled()) {
-                add_aux(~lit, lit2);
-                add_aux(lit, ~lit2);
-            }
+            add_aux(~lit, lit2);
+            add_aux(lit, ~lit2);
             lit = lit2;
         }
 
+        TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";);
         m_bool_var2expr.reserve(v + 1, nullptr);
         if (m_bool_var2expr[v] && m_egraph.find(e)) {
+            if (m_egraph.find(e)->bool_var() != v) {
+                IF_VERBOSE(0, verbose_stream()
+                 << "var " << v << "\n"
+                 << "found var " << m_egraph.find(e)->bool_var() << "\n"
+                 << mk_pp(m_bool_var2expr[v], m) << "\n"
+                 << mk_pp(e, m) << "\n");
+            }
             SASSERT(m_egraph.find(e)->bool_var() == v);
             return lit;
         }
-        TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";);
+
         m_bool_var2expr[v] = e;
-        m_var_trail.push_back(v);
+        m_var_trail.push_back(v);        
         enode* n = m_egraph.find(e);
-        if (!n) {
+        if (!n) 
             n = mk_enode(e, 0, nullptr);
-        }
         SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v);
         m_egraph.set_bool_var(n, v);
         if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
             m_egraph.set_merge_enabled(n, false);
-        if (!si.is_bool_op(e))
-            track_relevancy(lit.var());
         if (s().value(lit) != l_undef) 
             m_egraph.set_value(n, s().value(lit));
         return lit;
@@ -224,9 +227,8 @@ namespace euf {
                     lits.push_back(lit);
                 }
             }
+            add_root(lits);
             s().mk_clause(lits, st);
-            if (relevancy_enabled())
-                add_root(lits);
         }
         else {
             // g(f(x_i)) = x_i
@@ -244,15 +246,13 @@ namespace euf {
                 expr_ref gapp(m.mk_app(g, fapp.get()), m);
                 expr_ref eq = mk_eq(gapp, arg);
                 sat::literal lit = mk_literal(eq);
-                s().add_clause(1, &lit, st);
+                s().add_clause(lit, st);
                 eqs.push_back(mk_eq(fapp, a));
             }
             pb_util pb(m);
             expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m);
             sat::literal lit = si.internalize(at_least2, m_is_redundant);
-            s().mk_clause(1, &lit, st);
-            if (relevancy_enabled())
-                add_root(1, &lit);
+            s().add_clause(lit, st);
         }
     }
 
@@ -268,9 +268,7 @@ namespace euf {
                 for (unsigned j = i + 1; j < sz; ++j) {
                     expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
                     sat::literal lit = ~mk_literal(eq);
-                    s().add_clause(1, &lit, st);
-                    if (relevancy_enabled())
-                        add_root(1, &lit);
+                    s().add_clause(lit, st);
                 }
             }
         }
@@ -287,9 +285,7 @@ namespace euf {
                 n->mark_interpreted();
                 expr_ref eq = mk_eq(fapp, fresh);
                 sat::literal lit = mk_literal(eq);
-                s().add_clause(1, &lit, st);
-                if (relevancy_enabled())
-                    add_root(1, &lit);
+                s().add_clause(lit, st);
             }
         }
     }
@@ -302,16 +298,16 @@ namespace euf {
             expr_ref eq_th = mk_eq(e, th);
             sat::literal lit_th = mk_literal(eq_th);
             if (th == el) {
-                s().add_clause(1, &lit_th, st);
+                s().add_clause(lit_th, st);
             }
             else {
                 sat::literal lit_c = mk_literal(c);
                 expr_ref eq_el = mk_eq(e, el);
                 sat::literal lit_el = mk_literal(eq_el);
-                literal lits1[2] = { ~lit_c,  lit_th };
-                literal lits2[2] = { lit_c, lit_el };
-                s().add_clause(2, lits1, st);
-                s().add_clause(2, lits2, st);
+                add_root(~lit_c, lit_th);
+                add_root(lit_c, lit_el);
+                s().add_clause(~lit_c, lit_th, st);
+                s().add_clause(lit_c, lit_el, st);
             }
         }
         else if (m.is_distinct(e)) {
@@ -326,10 +322,10 @@ namespace euf {
             expr_ref fml(m.mk_or(eqs), m);
             sat::literal dist(si.to_bool_var(e), false);
             sat::literal some_eq = si.internalize(fml, m_is_redundant);
-            sat::literal lits1[2] = { ~dist, ~some_eq };
-            sat::literal lits2[2] = { dist, some_eq };
-            s().add_clause(2, lits1, st);
-            s().add_clause(2, lits2, st);
+            add_root(~dist, ~some_eq);
+            add_root(dist, some_eq);
+            s().add_clause(~dist, ~some_eq, st);
+            s().add_clause(dist, some_eq, st);
         }
         else if (m.is_eq(e, th, el) && !m.is_iff(e)) {
             sat::literal lit1 = expr2literal(e);
@@ -338,10 +334,10 @@ namespace euf {
             enode* n2 = m_egraph.find(e2);
             if (n2) {
                 sat::literal lit2 = expr2literal(e2);
-                sat::literal lits1[2] = { ~lit1, lit2 };
-                sat::literal lits2[2] = { lit1, ~lit2 };
-                s().add_clause(2, lits1, st);
-                s().add_clause(2, lits2, st);
+                add_root(~lit1, lit2);
+                add_root(lit1, ~lit2);
+                s().add_clause(~lit1, lit2, st);
+                s().add_clause(lit1, ~lit2, st);
             }
         }
     }
@@ -357,7 +353,7 @@ namespace euf {
         // contains a parent application.
         
         family_id th_id = m.get_basic_family_id();
-        for (auto p : euf::enode_th_vars(n)) {
+        for (auto const& p : euf::enode_th_vars(n)) {
             family_id id = p.get_id();
             if (m.get_basic_family_id() != id) {
                 if (th_id != m.get_basic_family_id())
@@ -402,7 +398,7 @@ namespace euf {
         // Remark: The inconsistency is not going to be detected if they are
         // not marked as shared.
 
-        for (auto p : euf::enode_th_vars(n)) 
+        for (auto const& p : euf::enode_th_vars(n)) 
             if (fid2solver(p.get_id())->is_shared(p.get_var()))
                 return true;
 

src/sat/smt/euf_model.cpp

@@ -35,7 +35,7 @@ namespace euf {
             s(s), m(s.m), mdl(mdl), values(values), factory(m) {}
 
         ~user_sort() {
-            for (auto kv : sort2values)
+            for (auto const& kv : sort2values)
                 mdl->register_usort(kv.m_key, kv.m_value->size(), kv.m_value->data());
         }
 
@@ -161,10 +161,9 @@ namespace euf {
                 default:
                     break;
                 }
-                if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
-                    continue;
                 sat::bool_var v = get_enode(e)->bool_var();
-                SASSERT(v != sat::null_bool_var);
+                if (v == sat::null_bool_var)
+                    continue;
                 switch (s().value(v)) {
                 case l_true:
                     m_values.set(id, m.mk_true());
@@ -200,6 +199,8 @@ namespace euf {
             expr* e = n->get_expr();
             if (!is_app(e))
                 continue;
+            if (!is_relevant(n))
+                continue;
             app* a = to_app(e);
             func_decl* f = a->get_decl();       
             if (!include_func_interp(f))
@@ -224,7 +225,7 @@ namespace euf {
                     enode* earg = get_enode(arg); 
                     expr* val = m_values.get(earg->get_root_id());
                     args.push_back(val);                
-                    CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";);
+                    CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n" << bpp(n) << "\n"; display(tout););
                     SASSERT(val);
                 }
                 SASSERT(args.size() == arity);
@@ -259,7 +260,7 @@ namespace euf {
             if (n->is_root() && m_values.get(n->get_expr_id()))
                 m_values2root.insert(m_values.get(n->get_expr_id()), n);
         TRACE("model", 
-              for (auto kv : m_values2root) 
+              for (auto const& kv : m_values2root) 
                   tout << mk_bounded_pp(kv.m_key, m) << "\n    -> " << bpp(kv.m_value) << "\n";);
         
         return m_values2root;
@@ -271,6 +272,7 @@ namespace euf {
 
     void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
         out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
+        s().display(out);
         euf::enode_vector nodes;
         nodes.push_back(n);
         for (unsigned i = 0; i < nodes.size(); ++i) {
@@ -289,14 +291,20 @@ namespace euf {
         for (euf::enode* r : nodes)
             r->unmark1();
         out << mdl << "\n";
-        s().display(out);
     }
 
     void solver::validate_model(model& mdl) {
+        if (!m_unhandled_functions.empty())
+            return;
+        for (auto* s : m_solvers)
+            if (s && s->has_unhandled())
+                return;
         model_evaluator ev(mdl);
         ev.set_model_completion(true);
         TRACE("model",
             for (enode* n : m_egraph.nodes()) {
+                if (!is_relevant(n))
+                    continue;
                 unsigned id = n->get_root_id();
                 expr* val = m_values.get(id, nullptr);
                 if (!val)
@@ -322,8 +330,8 @@ namespace euf {
             IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
             CTRACE("euf", first, display_validation_failure(tout, mdl, n););
             (void)first;
-            exit(1);
             first = false;
+            exit(1);
         }        
     }
 

src/sat/smt/euf_relevancy.cpp

@@ -3,157 +3,326 @@ Copyright (c) 2020 Microsoft Corporation
 
 Module Name:
 
-    euf_relevancy.cpp
+    smt_relevant.cpp
 
 Abstract:
 
-    Features for relevancy tracking.
-    A reduced (minimal) implicant is extracted by running a dual solver.
-    Then the literals in the implicant are used as a basis for marking
-    subterms relevant.
+    Relevancy propagation
 
 Author:
 
-    Nikolaj Bjorner (nbjorner) 2020-09-22
+    Nikolaj Bjorner (nbjorner) 2021-12-27
 
 --*/
-
+#include "sat/sat_solver.h"
 #include "sat/smt/euf_solver.h"
+#include "sat/smt/euf_relevancy.h"
+
 
 namespace euf {
-
-    void solver::add_auto_relevant(expr* e) {
-        if (!relevancy_enabled())
-            return;
-        for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes) 
-            m_auto_relevant_lim.push_back(m_auto_relevant.size());
-        // std::cout << "add-auto " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
-        m_auto_relevant.push_back(e);
-    }
     
-    void solver::pop_relevant(unsigned n) {
-        if (m_auto_relevant_scopes >= n) {
-            m_auto_relevant_scopes -= n;
+    void relevancy::pop(unsigned n) {
+        if (!m_enabled)
+            return;
+        if (n <= m_num_scopes) {
+            m_num_scopes -= n;
             return;
         }
-        n -= m_auto_relevant_scopes;
-        m_auto_relevant_scopes = 0;
-        unsigned top = m_auto_relevant_lim.size() - n;
-        unsigned lim = m_auto_relevant_lim[top];
-        m_auto_relevant_lim.shrink(top);
-        m_auto_relevant.shrink(lim);        
+        else if (m_num_scopes > 0) {
+            n -= m_num_scopes;
+            m_num_scopes = 0;
+        }
+        SASSERT(n > 0);
+        unsigned sz = m_lim[m_lim.size() - n];
+        for (unsigned i = m_trail.size(); i-- > sz; ) {
+            auto const& [u, idx] = m_trail[i];
+            switch (u) {
+            case update::relevant_var:
+                m_relevant_var_ids[idx] = false;
+                break;
+            case update::add_queue:
+                m_queue.pop_back();
+                break;
+            case update::add_clause: {
+                sat::clause* c = m_clauses.back();
+                for (sat::literal lit : *c) {
+                    SASSERT(m_occurs[lit.index()].back() == m_clauses.size() - 1);
+                    m_occurs[lit.index()].pop_back();
+                }
+                m_clauses.pop_back();
+                m_roots.pop_back();
+                m_alloc.del_clause(c);
+                break;
+            }
+            case update::set_root:
+                m_roots[idx] = false;
+                break;
+            case update::set_qhead:
+                m_qhead = idx;
+                break;
+            default:
+                UNREACHABLE();
+                break;
+            }
+        }
+        m_trail.shrink(sz);
+        m_lim.shrink(m_lim.size() - n);
     }
     
-    void solver::push_relevant() {
-        ++m_auto_relevant_scopes;
-    }
-
-    bool solver::is_relevant(expr* e) const { 
-        return m_relevant_expr_ids.get(e->get_id(), true); 
-    }
-
-    bool solver::is_relevant(enode* n) const { 
-        return m_relevant_expr_ids.get(n->get_expr_id(), true); 
-    }
-
-    void solver::ensure_dual_solver() {
-        if (m_dual_solver)
+    void relevancy::add_root(unsigned n, sat::literal const* lits) {
+        if (!m_enabled)
             return;
-        m_dual_solver = alloc(sat::dual_solver, s().rlimit());
-        for (unsigned i = s().num_user_scopes(); i-- > 0; )
-            m_dual_solver->push();        
+        flush();
+        TRACE("relevancy", tout << "root " << sat::literal_vector(n, lits) << "\n");
+        sat::literal true_lit = sat::null_literal;
+        for (unsigned i = 0; i < n; ++i) {
+            if (ctx.s().value(lits[i]) == l_true) {
+                if (is_relevant(lits[i]))
+                    return;
+                true_lit = lits[i];                
+            }
+        }
+        if (true_lit != sat::null_literal) {
+            mark_relevant(true_lit);
+            return;
+        }
+
+        sat::clause* cl = m_alloc.mk_clause(n, lits, false);
+        unsigned sz = m_clauses.size();
+        m_clauses.push_back(cl);
+        m_roots.push_back(true);
+        m_trail.push_back(std::make_pair(update::add_clause, 0));
+        for (sat::literal lit : *cl) {
+            ctx.s().set_external(lit.var());
+            occurs(lit).push_back(sz);
+        }
+    }
+    
+    void relevancy::add_def(unsigned n, sat::literal const* lits) {        
+        if (!m_enabled)
+            return;
+        flush();
+        TRACE("relevancy", tout << "def " << sat::literal_vector(n, lits) << "\n");
+        for (unsigned i = 0; i < n; ++i) {
+            if (ctx.s().value(lits[i]) == l_false && is_relevant(lits[i])) {
+                add_root(n, lits);
+                return;
+            }
+        }
+        sat::clause* cl = m_alloc.mk_clause(n, lits, false);
+        unsigned sz = m_clauses.size();
+        m_clauses.push_back(cl);
+        m_roots.push_back(false);
+        m_trail.push_back(std::make_pair(update::add_clause, 0));
+        for (sat::literal lit : *cl) {
+            ctx.s().set_external(lit.var());
+            occurs(lit).push_back(sz);
+        }
+    }
+
+    void relevancy::add_to_propagation_queue(sat::literal lit) {
+        m_trail.push_back(std::make_pair(update::add_queue, lit.var()));
+        m_queue.push_back(std::make_pair(lit, nullptr));
+    }
+
+    void relevancy::set_relevant(sat::literal lit) {
+        euf::enode* n = ctx.bool_var2enode(lit.var());
+        if (n)
+            mark_relevant(n);        
+        m_relevant_var_ids.setx(lit.var(), true, false);
+        m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
+    }
+
+    void relevancy::set_asserted(sat::literal lit) {
+        SASSERT(!is_relevant(lit));
+        SASSERT(ctx.s().value(lit) == l_true);
+        set_relevant(lit);
+        add_to_propagation_queue(lit);
+        ctx.asserted(lit);
     }
 
     /**
-     * Add a root clause. Root clauses must all be satisfied by the 
-     * final assignment. If a clause is added above search level it
-     * is subject to removal on backtracking. These clauses are therefore
-     * not tracked.
-     */
-    void solver::add_root(unsigned n, sat::literal const* lits) {
-        if (!relevancy_enabled())
+    * Boolean variable is set relevant because an E-node is relevant.
+    * 
+    */
+    void relevancy::relevant_eh(sat::bool_var v) {
+        if (is_relevant(v))
             return;
-        ensure_dual_solver();
-        m_dual_solver->add_root(n, lits);
-    }
-
-    void solver::add_aux(unsigned n, sat::literal const* lits) {
-        if (!relevancy_enabled())
-            return;
-        ensure_dual_solver();
-        m_dual_solver->add_aux(n, lits);
-    }
-
-    void solver::track_relevancy(sat::bool_var v) {
-        ensure_dual_solver();
-        m_dual_solver->track_relevancy(v);
-    }
-
-    bool solver::init_relevancy() {
-        m_relevant_expr_ids.reset();
-        if (!relevancy_enabled())
-            return true;
-        if (!m_dual_solver)
-            return true;
-        if (!(*m_dual_solver)(s()))
-            return false;
-        unsigned max_id = 0;
-        for (enode* n : m_egraph.nodes())
-            max_id = std::max(max_id, n->get_expr_id());
-        m_relevant_expr_ids.resize(max_id + 1, false);
-        ptr_vector<expr>& todo = m_relevant_todo;
-        bool_vector& visited = m_relevant_visited;
-        auto const& core = m_dual_solver->core();
-        todo.reset();
-        for (auto lit : core) {
-            expr* e = m_bool_var2expr.get(lit.var(), nullptr);
-            if (e)
-                todo.push_back(e);
+        sat::literal lit(v);
+        switch (ctx.s().value(lit)) {
+        case l_undef:
+            set_relevant(lit);
+            break;
+        case l_true:
+            set_asserted(lit);
+            break;
+        case l_false:
+            set_asserted(~lit);
+            break;
         }
-#if 0
-        std::cout << "init-relevant\n";
-        for (expr* e : m_auto_relevant)
-            std::cout << "auto-relevant " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
-#endif
-        todo.append(m_auto_relevant);
-        for (unsigned i = 0; i < todo.size(); ++i) {
-            expr* e = todo[i];
-            if (visited.get(e->get_id(), false))
+    }
+
+    void relevancy::asserted(sat::literal lit) {
+        TRACE("relevancy", tout << "asserted " << lit << " relevant " << is_relevant(lit) << "\n");
+        if (!m_enabled)
+            return;
+        flush();
+        if (is_relevant(lit)) {
+            add_to_propagation_queue(lit);
+            return;
+        }
+        if (ctx.s().lvl(lit) <= ctx.s().search_lvl()) {
+            set_relevant(lit);
+            add_to_propagation_queue(lit);
+            return;
+        }
+
+        for (auto idx : occurs(lit)) {
+            if (!m_roots[idx])
                 continue;
-            visited.setx(e->get_id(), true, false);
-            if (!si.is_bool_op(e)) 
-                m_relevant_expr_ids.setx(e->get_id(), true, false);
-            if (!is_app(e))
+            for (sat::literal lit2 : *m_clauses[idx]) 
+                if (lit2 != lit && ctx.s().value(lit2) == l_true && is_relevant(lit2))
+                    goto next;  
+            set_relevant(lit);
+            add_to_propagation_queue(lit);
+            return;
+        next:
+            ;
+        }
+    }
+
+    void relevancy::propagate() {
+        if (!m_enabled)
+            return;
+        flush();
+        if (m_qhead == m_queue.size())
+            return;
+        m_trail.push_back(std::make_pair(update::set_qhead, m_qhead));
+        while (m_qhead < m_queue.size() && !ctx.s().inconsistent() && ctx.get_manager().inc()) {
+            auto const& [lit, n] = m_queue[m_qhead++];
+            SASSERT(n || lit != sat::null_literal);
+            SASSERT(!n || lit == sat::null_literal);
+            if (n)
+                propagate_relevant(n);
+            else 
+                propagate_relevant(lit);            
+        }
+    }
+
+    void relevancy::merge(euf::enode* root, euf::enode* other) {
+        TRACE("relevancy", tout << "merge #" << ctx.bpp(root) << " " << is_relevant(root) << " #" << ctx.bpp(other) << " " << is_relevant(other) << "\n");
+        if (is_relevant(root))
+            mark_relevant(other);
+        else if (is_relevant(other))
+            mark_relevant(root);
+    }
+    
+    void relevancy::mark_relevant(euf::enode* n) {
+        if (!m_enabled)
+            return;
+        flush();
+        if (is_relevant(n))
+            return;
+        TRACE("relevancy", tout << "mark #" << ctx.bpp(n) << "\n");
+        m_trail.push_back(std::make_pair(update::add_queue, 0));
+        m_queue.push_back(std::make_pair(sat::null_literal, n));
+    }
+
+    void relevancy::mark_relevant(sat::literal lit) {
+        TRACE("relevancy", tout << "mark " << lit << " " << is_relevant(lit) << " " << ctx.s().value(lit) << " lim: " << m_lim.size() << "\n");
+        if (!m_enabled)
+            return;
+        flush();
+        if (is_relevant(lit))
+            return;        
+        set_relevant(lit);
+        switch (ctx.s().value(lit)) {
+        case l_true:
+            break;
+        case l_false:
+            lit.neg();
+            break;
+        default:
+            return;               
+        }
+        add_to_propagation_queue(lit);
+    }
+
+    void relevancy::propagate_relevant(sat::literal lit) {
+        SASSERT(m_num_scopes == 0);
+        TRACE("relevancy", tout << "propagate " << lit << " lim: " << m_lim.size() << "\n");
+        SASSERT(ctx.s().value(lit) == l_true);
+        SASSERT(is_relevant(lit));
+        euf::enode* n = ctx.bool_var2enode(lit.var());
+        if (n && !ctx.get_si().is_bool_op(n->get_expr()))
+            return;
+        for (auto idx : occurs(~lit)) {
+            if (m_roots[idx])
                 continue;
-            expr* c = nullptr, *th = nullptr, *el = nullptr;
-            if (m.is_ite(e, c, th, el) && get_enode(c)) {
-                sat::literal lit = expr2literal(c);
-                todo.push_back(c);
-                switch (s().value(lit)) {
-                case l_true:
-                    todo.push_back(th);
-                    break;
-                case l_false:
-                    todo.push_back(el);
-                    break;
-                default:
-                    todo.push_back(th);
-                    todo.push_back(el);
-                    break;
+            sat::clause* cl = m_clauses[idx];
+            sat::literal true_lit = sat::null_literal;
+            for (sat::literal lit2 : *cl) {
+                if (ctx.s().value(lit2) == l_true) {
+                    if (is_relevant(lit2))
+                        goto next;
+                    true_lit = lit2;
                 }
-                continue;
             }
-            for (expr* arg : *to_app(e))
-                todo.push_back(arg);
+
+            if (true_lit != sat::null_literal) 
+                set_asserted(true_lit);            
+            else {
+                m_trail.push_back(std::make_pair(update::set_root, idx));
+                m_roots[idx] = true;
+            }
+        next:
+            TRACE("relevancy", tout << "propagate " << lit << " " << true_lit << " " << m_roots[idx] << "\n");
+            ;
         }
-
-        for (auto * e : todo)
-            visited[e->get_id()] = false;
-
-        TRACE("euf",
-            for (enode* n : m_egraph.nodes())
-                if (is_relevant(n)) 
-                    tout << "relevant " << n->get_expr_id() << " [r" << n->get_root_id() << "]: " << mk_bounded_pp(n->get_expr(), m) << "\n";);
-              return true;
     }
+
+    void relevancy::propagate_relevant(euf::enode* n) {
+        m_todo.push_back(n);
+        while (!m_todo.empty()) {
+            n = m_todo.back();
+            m_todo.pop_back();
+            TRACE("relevancy", tout << "propagate #" << ctx.bpp(n) << " lim: " << m_lim.size() << "\n");
+            if (n->is_relevant())
+                continue;
+            m_stack.push_back(n);
+            while (!m_stack.empty()) {
+                n = m_stack.back();
+                unsigned sz = m_stack.size();
+                bool is_bool_op = ctx.get_si().is_bool_op(n->get_expr());
+                if (!is_bool_op)
+                    for (euf::enode* arg : euf::enode_args(n))
+                        if (!arg->is_relevant())
+                            m_stack.push_back(arg);
+                if (sz != m_stack.size())
+                    continue;
+                if (!n->is_relevant()) {
+                    ctx.get_egraph().set_relevant(n);
+                    ctx.relevant_eh(n);
+                    sat::bool_var v = n->bool_var();                    
+                    if (v != sat::null_bool_var)
+                        relevant_eh(v);
+                    for (euf::enode* sib : euf::enode_class(n))
+                        if (!sib->is_relevant())
+                            m_todo.push_back(sib);
+                }
+                if (!ctx.get_manager().inc()) {
+                    m_todo.reset();
+                    m_stack.reset();
+                    return;
+                }
+                m_stack.pop_back();
+            }
+        }
+    }
+
+    void relevancy::set_enabled(bool e) {
+        m_enabled = e;
+        ctx.get_egraph().set_default_relevant(!e);
+    }
+
 }

src/sat/smt/euf_relevancy.h

@@ -0,0 +1,173 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    smt_relevant.h
+
+Abstract:
+
+    Relevancy propagation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-12-27
+
+
+Clauses are split into two parts:
+
+- Roots
+- Defs
+
+The goal is to establish a labeling of literals as "relevant" such that
+- the set of relevant literals satisfies Roots
+- there is a set of blocked literals that can be used to satisfy the clauses in Defs
+  independent of their real assignment.
+
+The idea is that the Defs clauses are obtained from Tseitin transformation so they can be
+grouped by the blocked literal that was used to introduce them.
+For example, when clausifying (and a b) we have the clauses
+(=> (and a b) a)
+(=> (and a b) b)
+(or (not a) (not b) (and a b))
+then the literal for "(and a b)" is blocked.
+And recursively for clauses introduced for a, b if they use a Boolean connectives
+at top level.
+
+The state transitions are:
+
+- A literal lit is assigned:
+  lit appears positively in a Root clause R and no other literal in R are relevant.
+  ->
+  lit is set relevant
+
+  lit is justified at search level
+  -> 
+  lit is set relevant
+
+- An equality n1 = n2 is assigned:
+  n1 is relevant
+  -> 
+  n2 is marked as relevant
+
+- A lit is set relevant:
+  -> 
+  all clauses D in Defs where lit appears negatively are added to Roots
+
+- When a clause R is added to Roots:
+  R contains a positive literal lit that is relevant
+  ->
+  skip adding R to Roots
+
+- When a clause R is added to Roots:
+  R contains a positive literal lit, no positive literal in R are relevant
+  ->
+  lit is set relevant 
+
+- When a clause D is added to Defs:
+  D contains a negative literal that is relevant
+  -> 
+  Add D to Roots
+
+- When an expression is set relevant:
+  All non-relevant children above Boolean connectives are set relevant
+  If nodes are treated as Boolean connectives because they are clausified
+  to (=> cond (= n then)) and (=> (not cond) (= n else))
+
+Replay:
+  - literals that are replayed in clauses that are marked relevant are 
+    marked relevant again.
+
+  - expressions corresponding to auxiliary clauses are added as auxiliary clauses.
+  
+  - TBD: Are root clauses added under a scope discarded?
+    The SAT solver re-initializes clauses on its own, should we just use this mechanism?
+
+Can a literal that is not in a root be set relevant?
+ - yes, if we propagate over expressions
+
+Do we need full watch lists instead of 2-watch lists?
+ - probably, but unclear. The dual SAT solver only uses 2-watch lists, but uses a large clause for tracking 
+   roots.
+
+
+   State machine for literals: relevant(lit), assigned(lit)
+
+relevant(lit) transitions false -> true
+   if assigned(lit):     add to propagation queue
+   if not assigned(lit): no-op (or mark enodes as relevant)
+
+assigned(lit) transitions false -> true
+   if relevant(lit):      add to propagation queue
+   if not relevant(lit):  set relevant if member of root, add to propagation queue
+
+
+--*/
+#pragma once
+#include "sat/sat_solver.h"
+#include "sat/smt/sat_th.h"
+
+
+namespace euf {
+
+    class solver;
+
+    class relevancy {
+        euf::solver&         ctx;
+
+        enum class update { relevant_var, add_queue, add_clause, set_root, set_qhead };
+       
+        bool                                 m_enabled = false;
+        svector<std::pair<update, unsigned>> m_trail;
+        unsigned_vector                      m_lim;
+        unsigned                             m_num_scopes = 0;
+        bool_vector                          m_relevant_var_ids;  // identifiers of relevant Boolean variables
+        sat::clause_allocator                m_alloc;
+        sat::clause_vector                   m_clauses;           // clauses
+        bool_vector                          m_roots;             // indicate if clause is a root
+        vector<unsigned_vector>              m_occurs;            // where do literals occur
+        unsigned                             m_qhead = 0;         // queue head for relevancy
+        svector<std::pair<sat::literal, euf::enode*>> m_queue;    // propagation queue for relevancy
+        euf::enode_vector                    m_stack, m_todo;
+
+        void push_core() { m_lim.push_back(m_trail.size()); }
+        void flush() { for (; m_num_scopes > 0; --m_num_scopes) push_core(); }
+
+        unsigned_vector& occurs(sat::literal lit) { m_occurs.reserve(lit.index() + 1); return m_occurs[lit.index()]; }
+
+        void propagate_relevant(sat::literal lit);
+
+        void add_to_propagation_queue(sat::literal lit);        
+
+        void set_relevant(sat::literal lit);
+
+        void set_asserted(sat::literal lit);
+
+        void relevant_eh(sat::bool_var v);
+
+        void propagate_relevant(euf::enode* n);
+
+    public:
+        relevancy(euf::solver& ctx): ctx(ctx) {}
+
+        void push() { if (m_enabled) ++m_num_scopes; }
+        void pop(unsigned n);
+
+        void add_root(unsigned n, sat::literal const* lits);
+        void add_def(unsigned n, sat::literal const* lits);
+        void asserted(sat::literal lit);
+        void propagate();
+        bool can_propagate() const { return m_qhead < m_queue.size(); }
+
+        void mark_relevant(euf::enode* n);
+        void mark_relevant(sat::literal lit);
+        void merge(euf::enode* n1, euf::enode* n2);
+
+        bool is_relevant(sat::bool_var v) const { return !m_enabled || m_relevant_var_ids.get(v, false); }
+        bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); }
+        bool is_relevant(euf::enode* n) const { return !m_enabled || n->is_relevant(); }
+        
+        bool enabled() const { return m_enabled; }
+        void set_enabled(bool e);
+    };
+}

src/sat/smt/euf_solver.cpp

@@ -41,6 +41,7 @@ namespace euf {
         extension(symbol("euf"), m.mk_family_id("euf")),
         m(m),
         si(si),
+        m_relevancy(*this),
         m_egraph(m),
         m_trail(),
         m_rewriter(m),
@@ -51,12 +52,21 @@ namespace euf {
         m_values(m)
     {
         updt_params(p);
+        m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2);
 
         std::function<void(std::ostream&, void*)> disp =
             [&](std::ostream& out, void* j) { 
             display_justification_ptr(out, reinterpret_cast<size_t*>(j)); 
         };
         m_egraph.set_display_justification(disp);
+
+        if (m_relevancy.enabled()) {
+            std::function<void(euf::enode* root, euf::enode* other)> on_merge =
+                [&](enode* root, enode* other) {
+                m_relevancy.merge(root, other);
+            };
+            m_egraph.set_on_merge(on_merge);
+        }
     }
 
     void solver::updt_params(params_ref const& p) {
@@ -183,7 +193,7 @@ namespace euf {
     }
 
     void solver::propagate(literal lit, ext_justification_idx idx) {
-        add_auto_relevant(bool_var2expr(lit.var()));
+        mark_relevant(lit);
         s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
 
@@ -233,11 +243,11 @@ namespace euf {
         m_egraph.explain_eq<size_t>(m_explain, a, b);
     }
 
-    void solver::add_diseq_antecedent(enode* a, enode* b) {
-        sat::bool_var v = get_egraph().explain_diseq(m_explain, a, b);
+    void solver::add_diseq_antecedent(ptr_vector<size_t>& ex, enode* a, enode* b) {
+        sat::bool_var v = get_egraph().explain_diseq(ex, a, b);
         SASSERT(v == sat::null_bool_var || s().value(v) == l_false);
         if (v != sat::null_bool_var) 
-            m_explain.push_back(to_ptr(sat::literal(v, true)));
+            ex.push_back(to_ptr(sat::literal(v, true)));
     }
 
     bool solver::propagate(enode* a, enode* b, ext_justification_idx idx) {
@@ -286,6 +296,11 @@ namespace euf {
     }
 
     void solver::asserted(literal l) {
+
+        m_relevancy.asserted(l);
+        if (!m_relevancy.is_relevant(l))
+            return;        
+
         expr* e = m_bool_var2expr.get(l.var(), nullptr);
         TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
         if (!e) 
@@ -329,6 +344,8 @@ namespace euf {
     bool solver::unit_propagate() {
         bool propagated = false;
         while (!s().inconsistent()) {
+            if (m_relevancy.enabled())
+                m_relevancy.propagate();
             if (m_egraph.inconsistent()) {  
                 unsigned lvl = s().scope_lvl();
                 s().set_conflict(sat::justification::mk_ext_justification(lvl, conflict_constraint().to_index()));
@@ -345,9 +362,13 @@ namespace euf {
                 if (m_solvers[i]->unit_propagate())
                     propagated1 = true;
             
-            if (!propagated1)
-                break;
-            propagated = true;             
+            if (propagated1) {
+                propagated = true;
+                continue;
+            }
+            if (m_relevancy.enabled() && m_relevancy.can_propagate())
+                continue;
+            break;                  
         }
         DEBUG_CODE(if (!propagated && !s().inconsistent()) check_missing_eq_propagation(););
         return propagated;
@@ -422,12 +443,10 @@ namespace euf {
     void solver::propagate_th_eqs() {
         for (; m_egraph.has_th_eq() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_th_eq()) {
             th_eq eq = m_egraph.get_th_eq();
-            if (eq.is_eq()) {
-                if (!is_self_propagated(eq))
-                    m_id2solver[eq.id()]->new_eq_eh(eq);    
-            }
-            else
+            if (!eq.is_eq())
                 m_id2solver[eq.id()]->new_diseq_eh(eq);
+            else if (!is_self_propagated(eq))
+                m_id2solver[eq.id()]->new_eq_eh(eq);                                
         }
     }
 
@@ -458,9 +477,6 @@ namespace euf {
 
         if (unit_propagate())
             return sat::check_result::CR_CONTINUE;
-
-        if (!init_relevancy())
-            give_up = true;
         
         unsigned num_nodes = m_egraph.num_nodes();
         auto apply_solver = [&](th_solver* e) {
@@ -525,9 +541,7 @@ namespace euf {
         for (auto* e : m_solvers)
             e->push();
         m_egraph.push();
-        if (m_dual_solver)
-            m_dual_solver->push();
-        push_relevant();
+        m_relevancy.push();
     }
 
     void solver::pop(unsigned n) {
@@ -537,7 +551,7 @@ namespace euf {
             e->pop(n);
         si.pop(n);
         m_egraph.pop(n);
-        pop_relevant(n);
+        m_relevancy.pop(n);
         scope const & sc = m_scopes[m_scopes.size() - n];
         for (unsigned i = m_var_trail.size(); i-- > sc.m_var_lim; ) {
             bool_var v = m_var_trail[i];
@@ -546,8 +560,6 @@ namespace euf {
         }
         m_var_trail.shrink(sc.m_var_lim);        
         m_scopes.shrink(m_scopes.size() - n);
-        if (m_dual_solver)
-            m_dual_solver->pop(n);
         SASSERT(m_egraph.num_scopes() == m_scopes.size());
         TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n"););
     }
@@ -720,6 +732,58 @@ namespace euf {
         }
     }
 
+    bool solver::is_relevant(bool_var v) const {
+        if (m_relevancy.enabled())
+            return m_relevancy.is_relevant(v);
+        auto* e = bool_var2enode(v);
+        return !e || is_relevant(e);
+    }
+
+    void solver::relevant_eh(euf::enode* n) {
+        if (m_qsolver)
+            m_qsolver->relevant_eh(n);
+        for (auto const& thv : enode_th_vars(n)) {
+            auto* th = m_id2solver.get(thv.get_id(), nullptr);
+            if (th && th != m_qsolver)
+                th->relevant_eh(n);
+        }       
+    }
+
+    bool solver::enable_ackerman_axioms(expr* e) const {
+        euf::enode* n = get_enode(e);
+        if (!n)
+            return false;
+        for (auto const& thv : enode_th_vars(n)) {
+            auto* th = m_id2solver.get(thv.get_id(), nullptr);
+            if (th && !th->enable_ackerman_axioms(n))
+                return false;
+        }
+        return true;
+    }
+
+    bool solver::is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain) {
+        if (n->bool_var() != sat::null_bool_var) {
+            switch (s().value(n->bool_var())) {
+            case l_true:
+                val = m.mk_true();
+                explain.push_back(sat::literal(n->bool_var()));
+                return true;                
+            case l_false:
+                val = m.mk_false();
+                explain.push_back(~sat::literal(n->bool_var()));
+                return true;
+            default:
+                return false;
+            }
+        }
+        for (auto const& thv : enode_th_vars(n)) {
+            auto* th = m_id2solver.get(thv.get_id(), nullptr);
+            if (th && !th->is_fixed(thv.get_var(), val, explain))
+                return true;
+        }
+        return false;
+    }
+
     void solver::pre_simplify() {
         for (auto* e : m_solvers)
             e->pre_simplify();
@@ -765,13 +829,18 @@ namespace euf {
     }
 
     bool solver::set_root(literal l, literal r) {
-        expr* e = bool_var2expr(l.var());
-        if (!e)
-            return true;
+        if (m_relevancy.enabled())
+            return false;
         bool ok = true;
         for (auto* s : m_solvers)
             if (!s->set_root(l, r))
                 ok = false;
+
+        if (!ok)
+            return false;
+        expr* e = bool_var2expr(l.var());
+        if (!e)
+            return true;
         if (m.is_eq(e) && !m.is_iff(e))
             ok = false;
         euf::enode* n = get_enode(e);
@@ -794,7 +863,7 @@ namespace euf {
         out << "bool-vars\n";
         for (unsigned v : m_var_trail) {
             expr* e = m_bool_var2expr[v];
-            out << v << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
+            out << v << (is_relevant(v)?"":"n") << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
         }
         for (auto* e : m_solvers)
             e->display(out);

src/sat/smt/euf_solver.h

@@ -25,11 +25,12 @@ Author:
 #include "sat/sat_extension.h"
 #include "sat/smt/atom2bool_var.h"
 #include "sat/smt/sat_th.h"
-#include "sat/smt/sat_dual_solver.h"
 #include "sat/smt/euf_ackerman.h"
 #include "sat/smt/user_solver.h"
+#include "sat/smt/euf_relevancy.h"
 #include "smt/params/smt_params.h"
 
+
 namespace euf {
     typedef sat::literal literal;
     typedef sat::ext_constraint_idx ext_constraint_idx;
@@ -91,6 +92,7 @@ namespace euf {
         std::function<::solver*(void)>   m_mk_solver;
         ast_manager&                     m;
         sat::sat_internalizer& si;
+        relevancy              m_relevancy;
         smt_params             m_config;
         euf::egraph            m_egraph;
         trail_stack            m_trail;
@@ -181,17 +183,17 @@ namespace euf {
         void init_drat();
 
         // relevancy
-        bool_vector m_relevant_expr_ids;
-        bool_vector m_relevant_visited;
-        ptr_vector<expr> m_relevant_todo;
-        void ensure_dual_solver();
-        bool init_relevancy();
-
-
+        //bool_vector m_relevant_expr_ids;
+        //bool_vector m_relevant_visited;
+        //ptr_vector<expr> m_relevant_todo;
+        //void init_relevant_expr_ids();
+        //void push_relevant(sat::bool_var v);
+        bool is_propagated(sat::literal lit);
         // invariant
         void check_eqc_bool_assignment() const;
         void check_missing_bool_enode_propagation() const;
         void check_missing_eq_propagation() const;
+        
 
         // diagnosis
         std::ostream& display_justification_ptr(std::ostream& out, size_t* j) const;
@@ -250,6 +252,10 @@ namespace euf {
         sat::sat_internalizer& get_si() { return si; }
         ast_manager& get_manager() { return m; }
         enode* get_enode(expr* e) const { return m_egraph.find(e); }
+        enode* bool_var2enode(sat::bool_var b) const {
+            expr* e = m_bool_var2expr.get(b, nullptr);
+            return e ? get_enode(e) : nullptr;
+        }
         sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); }
         sat::literal enode2literal(enode* n) const { return sat::literal(n->bool_var(), false); }
         lbool value(enode* n) const { return s().value(enode2literal(n)); }
@@ -299,7 +305,9 @@ namespace euf {
         void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override;
         void get_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing);
         void add_antecedent(enode* a, enode* b);
-        void add_diseq_antecedent(enode* a, enode* b);
+        void add_diseq_antecedent(ptr_vector<size_t>& ex, enode* a, enode* b);
+        void add_explain(size_t* p) { m_explain.push_back(p); }
+        void reset_explain() { m_explain.reset(); }
         void set_eliminated(bool_var v) override;
         void asserted(literal l) override;
         sat::check_result check() override;
@@ -362,32 +370,29 @@ namespace euf {
         th_rewriter& get_rewriter() { return m_rewriter; }
         void rewrite(expr_ref& e) { m_rewriter(e); }
         bool is_shared(euf::enode* n) const;
+        bool enable_ackerman_axioms(expr* n) const;
+        bool is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain);
 
         // relevancy
-        bool m_relevancy = true;
-        scoped_ptr<sat::dual_solver>  m_dual_solver;
-        ptr_vector<expr>              m_auto_relevant;
-        unsigned_vector               m_auto_relevant_lim;
-        unsigned                      m_auto_relevant_scopes = 0;
 
-        bool relevancy_enabled() const { return m_relevancy && get_config().m_relevancy_lvl > 0; }
-        void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy = false;  }
-        void add_root(unsigned n, sat::literal const* lits);
+        bool relevancy_enabled() const { return m_relevancy.enabled(); }
+        void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy.set_enabled(false); }
+        void add_root(unsigned n, sat::literal const* lits) { m_relevancy.add_root(n, lits); }
         void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); }
         void add_root(sat::literal lit) { add_root(1, &lit); }
-        void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); }
+        void add_root(sat::literal lit1, sat::literal lit2) { sat::literal lits[2] = { lit1, lit2, }; add_root(2, lits); }
         void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); }
-        void add_aux(unsigned n, sat::literal const* lits);
+        void add_aux(unsigned n, sat::literal const* lits) { m_relevancy.add_def(n, lits); }
         void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); }
         void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } 
         void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); }
-        void track_relevancy(sat::bool_var v);
-        bool is_relevant(expr* e) const;
-        bool is_relevant(enode* n) const;
-        void add_auto_relevant(expr* e);
-        void pop_relevant(unsigned n);
-        void push_relevant();
+        void mark_relevant(sat::literal lit) { m_relevancy.mark_relevant(lit); }
+        bool is_relevant(enode* n) const { return m_relevancy.is_relevant(n); }
+        bool is_relevant(bool_var v) const;
+        bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); }
+        void relevant_eh(euf::enode* n);
 
+        relevancy& get_relevancy() { return m_relevancy; }
 
         // model construction
         void update_model(model_ref& mdl);
@@ -425,7 +430,11 @@ namespace euf {
             check_for_user_propagator();
             m_user_propagator->register_diseq(diseq_eh);
         }
-        unsigned user_propagate_register(expr* e) {
+        void user_propagate_register_created(user_propagator::created_eh_t& ceh) {
+            check_for_user_propagator();
+            m_user_propagator->register_created(ceh);
+        }
+        unsigned user_propagate_register_expr(expr* e) {
             check_for_user_propagator();
             return m_user_propagator->add_expr(e);
         }

src/sat/smt/fpa_solver.cpp

@@ -269,7 +269,7 @@ namespace fpa {
         expr* xe = e_x->get_expr();
         expr* ye = e_y->get_expr();
 
-        if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye))
+        if (fu.is_bvwrap(xe) || fu.is_bvwrap(ye))
             return;
 
         expr_ref xc = convert(xe);

src/sat/smt/pb_internalize.cpp

@@ -18,6 +18,7 @@ Author:
 
 #include "sat/smt/pb_solver.h"
 #include "ast/pb_decl_plugin.h"
+#include "sat/smt/euf_solver.h"
 
 namespace pb {
 
@@ -27,8 +28,12 @@ namespace pb {
 
     literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
         flet<bool> _redundant(m_is_redundant, redundant);
-        if (m_pb.is_pb(e)) 
-            return internalize_pb(e, sign, root);
+        if (m_pb.is_pb(e)) {
+            sat::literal lit = internalize_pb(e, sign, root);
+            if (m_ctx && !root && lit != sat::null_literal)
+                m_ctx->attach_lit(lit, e);            
+            return lit;
+        }
         UNREACHABLE();
         return sat::null_literal;
     }

src/sat/smt/pb_solver.cpp

@@ -1338,7 +1338,9 @@ namespace pb {
     }
 
     solver::solver(euf::solver& ctx, euf::theory_id id) :
-        solver(ctx.get_manager(), ctx.get_si(), id) {}
+        solver(ctx.get_manager(), ctx.get_si(), id) {
+        m_ctx = &ctx;
+    }
 
     solver::solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id)
         : euf::th_solver(m, symbol("ba"), id),
@@ -1370,6 +1372,21 @@ namespace pb {
             s().mk_clause(_lits.size(), _lits.data(), sat::status::th(learned, get_id()));
             return nullptr;
         }
+
+        if (k == 0) {
+            if (lit != sat::null_literal)
+                s().add_clause(lit, sat::status::th(false, get_id()));
+            return nullptr;
+        }
+
+        if (k > lits.size()) {
+            if (lit == sat::null_literal)
+                s().add_clause(0, nullptr, sat::status::th(false, get_id()));
+            else
+                s().add_clause(~lit, sat::status::th(false, get_id()));
+            return nullptr;
+        }
+
         if (!learned && clausify(lit, lits.size(), lits.data(), k)) {
             return nullptr;
         }
@@ -1403,8 +1420,10 @@ namespace pb {
             if (m_solver) m_solver->set_external(lit.var());
             c->watch_literal(*this, lit);
             c->watch_literal(*this, ~lit);
-        }        
-        SASSERT(c->well_formed());
+        }     
+        if (!c->well_formed()) 
+            std::cout << *c << "\n";
+        VERIFY(c->well_formed());
         if (m_solver && m_solver->get_config().m_drat) {
             std::function<void(std::ostream& out)> fn = [&](std::ostream& out) {
                 out << "c ba constraint " << *c << " 0\n";
@@ -1429,12 +1448,27 @@ namespace pb {
 
     constraint* solver::add_pb_ge(literal lit, svector<wliteral> const& wlits, unsigned k, bool learned) {
         bool units = true;
-        for (wliteral wl : wlits) units &= wl.first == 1;
-        if (k == 0 && lit == sat::null_literal) {
+        for (wliteral wl : wlits) 
+            units &= wl.first == 1;
+
+        if (k == 0) {
+            if (lit != sat::null_literal)
+                s().add_clause(lit, sat::status::th(false, get_id()));
+            return nullptr;
+        }
+        rational weight(0);
+        for (auto const [w, l] : wlits)
+            weight += w;
+        if (weight < k) {
+            if (lit == sat::null_literal)
+                s().add_clause(0, nullptr, sat::status::th(false, get_id()));
+            else
+                s().add_clause(~lit, sat::status::th(false, get_id()));
             return nullptr;
         }
         if (!learned) {
-            for (wliteral wl : wlits) s().set_external(wl.second.var()); 
+            for (wliteral wl : wlits) 
+                s().set_external(wl.second.var()); 
         }
         if (units || k == 1) {
             literal_vector lits;
@@ -2006,7 +2040,7 @@ namespace pb {
             s().pop_to_base_level();
         if (s().inconsistent())
             return;
-        unsigned trail_sz, count = 0;
+        unsigned trail_sz = 0, count = 0;
         do {
             trail_sz = s().init_trail_size();
             m_simplify_change = false;
@@ -2159,12 +2193,13 @@ namespace pb {
     }
 
     bool solver::set_root(literal l, literal r) { 
-        if (s().is_assumption(l.var())) {
+        if (s().is_assumption(l.var())) 
             return false;
-        }
         reserve_roots();
         m_roots[l.index()] = r;
         m_roots[(~l).index()] = ~r;
+        m_roots[r.index()] = r;
+        m_roots[(~r).index()] = ~r;
         m_root_vars[l.var()] = true;
         return true;
     }
@@ -2180,7 +2215,6 @@ namespace pb {
             flush_roots(*m_learned[i]);
         cleanup_constraints();
         // validate();
-
         // validate_eliminated();
     }
 
@@ -2191,7 +2225,8 @@ namespace pb {
 
     void solver::validate_eliminated(ptr_vector<constraint> const& cs) {
         for (constraint const* c : cs) {
-            if (c->learned()) continue;
+            if (c->learned())
+                continue;
             for (auto l : constraint::literal_iterator(*c))
                 VERIFY(!s().was_eliminated(l.var()));
         }
@@ -2415,9 +2450,10 @@ namespace pb {
         for (unsigned i = 0; !found && i < c.size(); ++i) {
             found = m_root_vars[c.get_lit(i).var()];
         }
-        if (!found) return;
+        if (!found)
+            return;
         clear_watch(c);
-        
+
         // this could create duplicate literals
         for (unsigned i = 0; i < c.size(); ++i) {
             literal lit = m_roots[c.get_lit(i).index()];

src/sat/smt/pb_solver.h

@@ -80,7 +80,8 @@ namespace pb {
         sat::sat_internalizer&      si;
         pb_util                m_pb;
 
-        sat::lookahead*        m_lookahead{ nullptr };
+        sat::lookahead*        m_lookahead = nullptr;
+        euf::solver*           m_ctx = nullptr;
         stats                  m_stats; 
         small_object_allocator m_allocator;
        

src/sat/smt/q_clause.h

@@ -122,18 +122,17 @@ namespace q {
         return out << "]";
     }
 
-
     struct justification {
-        expr*     m_lhs, *m_rhs;
+        expr* m_lhs, * m_rhs;
         bool      m_sign;
-        unsigned  m_num_ev;
-        euf::enode_pair* m_evidence;
-        clause&   m_clause;
+        unsigned  m_num_ex;
+        size_t** m_explain;
+        clause& m_clause;
         euf::enode* const* m_binding;
-        justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, euf::enode_pair* ev):
-            m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ev(n), m_evidence(ev), m_clause(c), m_binding(b) {}
-        sat::ext_constraint_idx to_index() const { 
-            return sat::constraint_base::mem2base(this); 
+        justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, size_t** ev) :
+            m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ex(n), m_explain(ev), m_clause(c), m_binding(b) {}
+        sat::ext_constraint_idx to_index() const {
+            return sat::constraint_base::mem2base(this);
         }
         static justification& from_index(size_t idx) {
             return *reinterpret_cast<justification*>(sat::constraint_base::from_index(idx)->mem());

src/sat/smt/q_ematch.cpp

@@ -31,6 +31,7 @@ Done:
 #include "ast/ast_util.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/rewriter_def.h"
+#include "ast/normal_forms/pull_quant.h"
 #include "solver/solver.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/euf_solver.h"
@@ -69,10 +70,16 @@ namespace q {
             m_mam->add_node(n, false);
         };
         ctx.get_egraph().set_on_merge(_on_merge);
-        ctx.get_egraph().set_on_make(_on_make);
+        if (!ctx.relevancy_enabled())
+            ctx.get_egraph().set_on_make(_on_make);
         m_mam = mam::mk(ctx, *this);
     }
 
+    void ematch::relevant_eh(euf::enode* n) {
+        if (ctx.relevancy_enabled())
+            m_mam->add_node(n, false);
+    }
+
     void ematch::ensure_ground_enodes(expr* e) {
         mam::ground_subterms(e, m_ground);
         for (expr* g : m_ground) 
@@ -90,32 +97,58 @@ namespace q {
         }
     }
 
+    /**
+    * Create a justification for binding b.
+    * The justification involves equalities in the E-graph that have
+    * explanations. Retrieve the explanations while the justification
+    * is created to ensure the justification trail is well-founded
+    * during conflict resolution.
+    */
     sat::ext_justification_idx ematch::mk_justification(unsigned idx, clause& c, euf::enode* const* b) {
         void* mem = ctx.get_region().allocate(justification::get_obj_size());
         sat::constraint_base::initialize(mem, &m_qs);
         bool sign = false;
-        expr* l = nullptr, *r = nullptr;            
-        lit lit(expr_ref(l, m), expr_ref(r, m), sign); 
+        expr* l = nullptr, * r = nullptr;
+        lit lit(expr_ref(l, m), expr_ref(r, m), sign);
         if (idx != UINT_MAX)
             lit = c[idx];
-        auto* ev = static_cast<euf::enode_pair*>(ctx.get_region().allocate(sizeof(euf::enode_pair) * m_evidence.size()));
-        for (unsigned i = m_evidence.size(); i-- > 0; )
-            ev[i] = m_evidence[i];
-        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b, m_evidence.size(), ev);
+        m_explain.reset();
+        ctx.get_egraph().begin_explain();
+        ctx.reset_explain();
+        for (auto const& [a, b] : m_evidence) {
+            SASSERT(a->get_root() == b->get_root() || ctx.get_egraph().are_diseq(a, b));
+            if (a->get_root() == b->get_root())
+                ctx.get_egraph().explain_eq<size_t>(m_explain, a, b);
+            else
+                ctx.add_diseq_antecedent(m_explain, a, b);
+        }
+        ctx.get_egraph().end_explain();
+
+        size_t** ev = static_cast<size_t**>(ctx.get_region().allocate(sizeof(size_t*) * m_explain.size()));
+        for (unsigned i = m_explain.size(); i-- > 0; )
+            ev[i] = m_explain[i];
+        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b, m_explain.size(), ev);
         return constraint->to_index();
     }
 
     void ematch::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) {
-        m_eval.explain(l, justification::from_index(idx), r, probing);
+        justification& j = justification::from_index(idx);
+        for (unsigned i = 0; i < j.m_num_ex; ++i)
+            ctx.add_explain(j.m_explain[i]);
+        r.push_back(j.m_clause.m_literal);
     }
 
     quantifier_ref ematch::nnf_skolem(quantifier* q) {
+        SASSERT(is_forall(q));
         expr_ref r(m);
         proof_ref p(m);
         m_new_defs.reset();
         m_new_proofs.reset();
         m_nnf(q, m_new_defs, m_new_proofs, r, p);
-        SASSERT(is_quantifier(r));
+        SASSERT(is_forall(r));
+        pull_quant pull(m);
+        pull(r, r, p);
+        SASSERT(is_forall(r));
         for (expr* d : m_new_defs)
             m_qs.add_unit(m_qs.mk_literal(d));
         CTRACE("q", r != q, tout << mk_pp(q, m) << " -->\n" << r << "\n" << m_new_defs << "\n";);
@@ -295,7 +328,7 @@ namespace q {
         TRACE("q", b->display(ctx, tout << "on-binding " << mk_pp(q, m) << "\n") << "\n";);
 
 
-        if (false && propagate(false, _binding, max_generation, c, new_propagation))
+        if (propagate(false, _binding, max_generation, c, new_propagation))
             return;
 
         binding::push_to_front(c.m_bindings, b);
@@ -304,6 +337,10 @@ namespace q {
     }
 
     bool ematch::propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) {
+        if (!m_enable_propagate)
+            return false;
+        if (ctx.s().inconsistent())
+            return true;
         TRACE("q", c.display(ctx, tout) << "\n";);
         unsigned idx = UINT_MAX;
         m_evidence.reset();
@@ -331,7 +368,7 @@ namespace q {
             propagate(ev == l_false, idx, j_idx);
         else
             m_prop_queue.push_back(prop(ev == l_false, idx, j_idx));
-        propagated = true;
+        propagated = true;        
         return true;
     }
 
@@ -352,7 +389,7 @@ namespace q {
         if (m_prop_queue.empty())
             return false;
         for (unsigned i = 0; i < m_prop_queue.size(); ++i) {
-            auto [is_conflict, idx, j_idx] = m_prop_queue[i];
+            auto const& [is_conflict, idx, j_idx] = m_prop_queue[i];
             propagate(is_conflict, idx, j_idx);
         }
         m_prop_queue.reset();
@@ -527,7 +564,7 @@ namespace q {
     };
 
     void ematch::add(quantifier* _q) {
-        TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";);
+        TRACE("q", tout << "add " << mk_pp(_q, m) << "\n");
         clause* c = clausify(_q);
         quantifier* q = c->q();
         if (m_q2clauses.contains(q)) {
@@ -551,7 +588,7 @@ namespace q {
             app * mp = to_app(q->get_pattern(i));
             SASSERT(m.is_pattern(mp));
             bool unary = (mp->get_num_args() == 1);
-            TRACE("q", tout << "adding:\n" << expr_ref(mp, m) << "\n";);
+            TRACE("q", tout << "adding:\n" << expr_ref(mp, m) << "\n");
             if (!unary && j >= num_eager_multi_patterns) {
                 TRACE("q", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n";);
                 if (!m_lazy_mam)
@@ -570,7 +607,7 @@ namespace q {
 
 
     bool ematch::unit_propagate() {
-        return false;
+        // return false;
         return ctx.get_config().m_ematching && propagate(false);
     }
 
@@ -581,7 +618,7 @@ namespace q {
             return m_inst_queue.propagate() || propagated;
         ctx.push(value_trail<unsigned>(m_qhead));
         ptr_buffer<binding> to_remove;
-        for (; m_qhead < m_clause_queue.size(); ++m_qhead) {
+        for (; m_qhead < m_clause_queue.size() && m.inc(); ++m_qhead) {
             unsigned idx = m_clause_queue[m_qhead];
             clause& c = *m_clauses[idx];
             binding* b = c.m_bindings;
@@ -589,7 +626,7 @@ namespace q {
                 continue;
 
             do {                
-                if (false && propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
+                if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
                     to_remove.push_back(b);
                 else if (flush) {
                     instantiate(*b);
@@ -642,7 +679,7 @@ namespace q {
     void ematch::collect_statistics(statistics& st) const {
         m_inst_queue.collect_statistics(st);
         st.update("q redundant", m_stats.m_num_redundant);
-        st.update("q units",     m_stats.m_num_propagations);
+        st.update("q unit propagations",     m_stats.m_num_propagations);
         st.update("q conflicts", m_stats.m_num_conflicts);
         st.update("q delayed bindings", m_stats.m_num_delayed_bindings);
     }

src/sat/smt/q_ematch.h

@@ -89,11 +89,13 @@ namespace q {
         unsigned                      m_qhead = 0;
         unsigned_vector               m_clause_queue;
         euf::enode_pair_vector        m_evidence;
+        bool                          m_enable_propagate = true;
 
         euf::enode* const* copy_nodes(clause& c, euf::enode* const* _binding);
         binding* tmp_binding(clause& c, app* pat, euf::enode* const* _binding);
         binding* alloc_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top);
-        
+       
+        ptr_vector<size_t> m_explain;
         sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b);
 
         void ensure_ground_enodes(expr* e);
@@ -135,9 +137,10 @@ namespace q {
 
         bool unit_propagate();        
 
-
         void add(quantifier* q);
 
+        void relevant_eh(euf::enode* n);
+
         void collect_statistics(statistics& st) const;
 
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing);

src/sat/smt/q_eval.cpp

@@ -230,13 +230,17 @@ namespace q {
                 if (!n)
                     return nullptr;
                 for (unsigned i = args.size(); i-- > 0; ) {
-                    if (args[i] != n->get_arg(i)) {
-                        // roots could be different when using commutativity
-                        // instead of compensating for this, we just bail out
-                        if (args[i]->get_root() != n->get_arg(i)->get_root())
-                            return nullptr;
-                        evidence.push_back(euf::enode_pair(args[i], n->get_arg(i)));
-                    }
+                    euf::enode* a = args[i], *b = n->get_arg(i);
+                    if (a == b)
+                        continue;
+
+                    // roots could be different when using commutativity
+                    // instead of compensating for this, we just bail out
+                    if (a->get_root() != b->get_root())
+                        return nullptr;
+
+                    TRACE("q", tout << "evidence " << ctx.bpp(a) << " " << ctx.bpp(b) << "\n");
+                    evidence.push_back(euf::enode_pair(a, b));
                 }
                 m_indirect_nodes.push_back(n);
                 m_eval.setx(t->get_id(), n, nullptr);
@@ -246,20 +250,5 @@ namespace q {
         }
         return m_eval[e->get_id()];
     }
-
-    void eval::explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing) {
-        clause& c = j.m_clause;
-        for (unsigned i = 0; i < j.m_num_ev; ++i) {
-            auto [a, b] = j.m_evidence[i];
-            SASSERT(a->get_root() == b->get_root() || ctx.get_egraph().are_diseq(a, b));
-            if (a->get_root() == b->get_root())
-                ctx.add_antecedent(a, b);
-            else
-                ctx.add_diseq_antecedent(a, b);                            
-        }
-        r.push_back(c.m_literal);
-        (void)probing; // ignored        
-    }
-
     
 }

src/sat/smt/q_eval.h

@@ -43,7 +43,6 @@ namespace q {
         
     public:
         eval(euf::solver& ctx);
-        void explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing);
 
         lbool operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence);
         lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence);

src/sat/smt/q_mam.cpp

@@ -424,15 +424,19 @@ namespace q {
         friend class compiler;
         friend class code_tree_manager;
 
-        void display_seq(std::ostream & out, instruction * head, unsigned indent) const {
-            for (unsigned i = 0; i < indent; i++) {
+        void spaces(std::ostream& out, unsigned indent) const {
+            for (unsigned i = 0; i < indent; i++) 
                 out << "    ";
-            }
+        }
+
+        void display_seq(std::ostream & out, instruction * head, unsigned indent) const {
+            spaces(out, indent);
             instruction * curr = head;
             out << *curr;
             curr = curr->m_next;
             while (curr != nullptr && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) {
                 out << "\n";
+                spaces(out, indent);
                 out << *curr;
                 curr = curr->m_next;
             }
@@ -549,8 +553,8 @@ namespace q {
         void unmark(unsigned head) {
             for (unsigned i = m_candidates.size(); i-- > head; ) {
                 enode* app = m_candidates[i];
-                if (app->is_marked1())
-                    app->unmark1();
+                if (app->is_marked3())
+                    app->unmark3();
             }
         }
 
@@ -598,7 +602,7 @@ namespace q {
                 ast_manager & m = m_egraph->get_manager();
                 out << "patterns:\n";
                 for (auto [q, a] : m_patterns) 
-                    out << mk_pp(q, m) << " " << mk_pp(a, m) << "\n";
+                    out << q->get_id() << ": " << mk_pp(q, m) << " " << mk_pp(a, m) << "\n";
             }
 #endif
             out << "function: " << m_root_lbl->get_name();
@@ -942,9 +946,9 @@ namespace q {
         void linearise_core() {
             m_aux.reset();
             app *         first_app = nullptr;
-            unsigned      first_app_reg;
-            unsigned      first_app_sz;
-            unsigned      first_app_num_unbound_vars;
+            unsigned      first_app_reg = 0;
+            unsigned      first_app_sz = 0;
+            unsigned      first_app_num_unbound_vars = 0;
             // generate first the non-BIND operations
             for (unsigned reg : m_todo) {
                 expr *  p    = m_registers[reg];
@@ -2018,9 +2022,9 @@ namespace q {
                 code_tree::scoped_unmark _unmark(t);
                 while ((app = t->next_candidate()) && !ctx.resource_limits_exceeded()) {
                     TRACE("trigger_bug", tout << "candidate\n" << ctx.bpp(app) << "\n";);
-                    if (!app->is_marked1() && app->is_cgr()) {
+                    if (!app->is_marked3() && app->is_cgr()) {
                         execute_core(t, app);                       
-                        app->mark1();
+                        app->mark3();
                     }
                 }
             }
@@ -2878,8 +2882,10 @@ namespace q {
                 if (tree->expected_num_args() == p->get_num_args()) 
                     m_compiler.insert(tree, qa, mp, first_idx, false);
             }
-            DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
-                       ctx.push(push_back_trail<std::pair<quantifier*,app*>, false>(m_trees[lbl_id]->get_patterns())););
+            DEBUG_CODE(if (first_idx == 0) {
+                m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
+                ctx.push(push_back_trail<std::pair<quantifier*, app*>, false>(m_trees[lbl_id]->get_patterns()));
+            });
             TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
         }
 
@@ -3089,7 +3095,7 @@ namespace q {
         void add_candidate(code_tree * t, enode * app) {
             if (!t)
                 return;
-            TRACE("q", tout << "candidate " << t << " " << ctx.bpp(app) << "\n";);
+            TRACE("q", tout << "candidate " << ctx.bpp(app) << "\n";);
             if (!t->has_candidates()) {
                 ctx.push(push_back_trail<code_tree*, false>(m_to_match));
                 m_to_match.push_back(t);

src/sat/smt/q_mbi.cpp

@@ -51,7 +51,7 @@ namespace q {
         m_instantiations.reset();
         for (sat::literal lit : m_qs.m_universal) {
             quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
-            if (!ctx.is_relevant(q))
+            if (!ctx.is_relevant(lit.var()))
                 continue;
             init_model();
             switch (check_forall(q)) {
@@ -67,11 +67,10 @@ namespace q {
             }
         }
         m_max_cex += ctx.get_config().m_mbqi_max_cexs;
-        for (auto [qlit, fml, generation] : m_instantiations) {
+        for (auto const& [qlit, fml, generation] : m_instantiations) {
             euf::solver::scoped_generation sg(ctx, generation + 1);
             sat::literal lit = ctx.mk_literal(fml);
             m_qs.add_clause(~qlit, ~lit);
-            ctx.add_root(~qlit, ~lit);
         }
         m_instantiations.reset();
         return result;
@@ -130,7 +129,7 @@ namespace q {
                 r = n;
             }
             else if (n->generation() == gen) {
-                if ((++count) % m_qs.random() == 0)
+                if ((m_qs.random() % ++count) == 0)
                     r = n;
             }
             if (count > m_max_choose_candidates)
@@ -156,7 +155,7 @@ namespace q {
         unsigned inc = 1;
         while (true) {
             ::solver::scoped_push _sp(*m_solver);
-            add_universe_restriction(q, *qb);
+            add_universe_restriction(*qb);
             m_solver->assert_expr(qb->mbody);
             ++m_stats.m_num_checks;
             lbool r = m_solver->check_sat(0, nullptr);
@@ -218,17 +217,17 @@ namespace q {
             qlit.neg();
         ctx.rewrite(proj);
         TRACE("q", tout << "project: " << proj << "\n";);
+        IF_VERBOSE(11, verbose_stream() << "mbi:\n" << mk_pp(q, m) << "\n" << proj << "\n");
         ++m_stats.m_num_instantiations;        
         unsigned generation = ctx.get_max_generation(proj);    
         m_instantiations.push_back(instantiation_t(qlit, proj, generation));
     }
 
-    void mbqi::add_universe_restriction(quantifier* q, q_body& qb) {
-        unsigned sz = q->get_num_decls();
-        for (unsigned i = 0; i < sz; ++i) {
-            sort* s = q->get_decl_sort(i);
+    void mbqi::add_universe_restriction(q_body& qb) {
+        for (app* v : qb.vars) {
+            sort* s = v->get_sort();
             if (m_model->has_uninterpreted_sort(s))
-                restrict_to_universe(qb.vars.get(i), m_model->get_universe(s));
+                restrict_to_universe(v, m_model->get_universe(s));
         }
     }
 
@@ -309,8 +308,10 @@ namespace q {
                 proj.extract_literals(*m_model, vars, fmls);
                 fmls_extracted = true;
             }
-            if (p)
-                (*p)(*m_model, vars, fmls);
+            if (!p)
+                continue;
+            if (!(*p)(*m_model, vars, fmls))
+                return expr_ref(nullptr, m);
         }
         for (app* v : vars) {
             expr_ref term(m);

src/sat/smt/q_mbi.h

@@ -83,7 +83,7 @@ namespace q {
         q_body* specialize(quantifier* q);
         q_body* q2body(quantifier* q);
         expr_ref solver_project(model& mdl, q_body& qb, expr_ref_vector& eqs, bool use_inst);
-        void add_universe_restriction(quantifier* q, q_body& qb);
+        void add_universe_restriction(q_body& qb);
         void add_domain_eqs(model& mdl, q_body& qb);
         void add_domain_bounds(model& mdl, q_body& qb);
         void eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb);

src/sat/smt/q_model_fixer.cpp

@@ -66,7 +66,7 @@ namespace q {
         ptr_vector<quantifier> univ;
         for (sat::literal lit : m_qs.universal()) {
             quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
-            if (ctx.is_relevant(q))
+            if (ctx.is_relevant(lit.var()))
                 univ.push_back(q);
         }
         if (univ.empty())
@@ -256,7 +256,7 @@ namespace q {
               tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
               if (v2r.find(value, r)) 
                   tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";
-              ctx.display(tout);              
+              /*ctx.display(tout); */
               );
         if (v2r.find(value, r)) 
             return r->get_expr();

src/sat/smt/q_queue.cpp

@@ -146,15 +146,10 @@ namespace q {
                 
         unsigned gen = get_new_gen(f, ent.m_cost);
         bool new_propagation = false;
-        if (false && em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
+        if (em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
             return;
 
-#if 0
-        std::cout << mk_pp(q, m) << "\n";
-        std::cout << num_bindings << "\n";
-        for (unsigned i = 0; i < num_bindings; ++i)
-            std::cout << mk_pp(f[i]->get_expr(), m) << " " << mk_pp(f[i]->get_sort(), m) << "\n";
-#endif
+
         auto* ebindings = m_subst(q, num_bindings);
         for (unsigned i = 0; i < num_bindings; ++i)
             ebindings[i] = f[i]->get_expr();
@@ -168,7 +163,15 @@ namespace q {
 
         m_stats.m_num_instances++;
 
-        // f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") <<  "\n";
+#if 0
+        std::cout << "instantiate\n";
+        for (unsigned i = 0; i < num_bindings; ++i)
+            std::cout << ctx.bpp(f[i]) << " ";
+        std::cout << "\n";
+        std::cout << mk_pp(q, m) << "\n";
+#endif
+
+//        f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") <<  "\n";
 
         
         euf::solver::scoped_generation _sg(ctx, gen);

src/sat/smt/q_solver.cpp

@@ -19,9 +19,11 @@ Author:
 #include "ast/well_sorted.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/normal_forms/pull_quant.h"
+#include "ast/rewriter/inj_axiom.h"
 #include "sat/smt/q_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/sat_th.h"
+#include "qe/lite/qe_lite.h"
 
 
 namespace q {
@@ -44,19 +46,23 @@ namespace q {
         if (l.sign() == is_forall(e)) {
             sat::literal lit = skolemize(q);
             add_clause(~l, lit);
-            ctx.add_root(~l, lit);
+            return;
         }
-        else if (expand(q)) {
-            for (expr* e : m_expanded) {
-                sat::literal lit = ctx.internalize(e, l.sign(), false, false);
-                add_clause(~l, lit);
-                ctx.add_root(~l, lit);
+        quantifier* q_flat = nullptr;
+        if (!m_flat.find(q, q_flat)) {
+            if (expand(q)) {
+                for (expr* e : m_expanded) {
+                    sat::literal lit = ctx.internalize(e, l.sign(), false, false);
+                    add_clause(~l, lit);
+                }
+                return;
             }
+            q_flat = flatten(q);
         }
-        else if (is_ground(q->get_expr())) {
-            auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false);
+            
+        if (is_ground(q_flat->get_expr())) {
+            auto lit = ctx.internalize(q_flat->get_expr(), l.sign(), false, false);
             add_clause(~l, lit);
-            ctx.add_root(~l, lit);
         }
         else {
             ctx.push_vec(m_universal, l);
@@ -72,9 +78,12 @@ namespace q {
 
         if (ctx.get_config().m_mbqi) {
             switch (m_mbqi()) {
-            case l_true:  return sat::check_result::CR_DONE;
-            case l_false: return sat::check_result::CR_CONTINUE;
-            case l_undef: break;
+            case l_true:  
+                return sat::check_result::CR_DONE;
+            case l_false: 
+                return sat::check_result::CR_CONTINUE;
+            case l_undef: 
+                break;
             }
         }
         return sat::check_result::CR_GIVEUP;
@@ -169,13 +178,18 @@ namespace q {
 
     quantifier* solver::flatten(quantifier* q) {
         quantifier* q_flat = nullptr;
-        if (!has_quantifiers(q->get_expr())) 
-            return q;
         if (m_flat.find(q, q_flat))
             return q_flat;
+
+        expr_ref new_q(q, m), r(m);
         proof_ref pr(m);
-        expr_ref  new_q(m);
-        if (is_forall(q)) {
+        if (!has_quantifiers(q->get_expr())) {
+            if (!ctx.get_config().m_refine_inj_axiom)
+                return q;
+            if (!simplify_inj_axiom(m, q, new_q))
+                return q;
+        }
+        else if (is_forall(q)) {
             pull_quant pull(m);
             pull(q, new_q, pr);
             SASSERT(is_well_sorted(m, new_q));
@@ -221,15 +235,34 @@ namespace q {
         return val;
     }
 
+    /**
+     * Expand returns true if it was able to rewrite the formula.
+     * If the rewrite results in a quantifier, the rewritten quantifier
+     * is stored in m_flat to avoid repeated expansions.
+     * 
+     */
     bool solver::expand(quantifier* q) {
-        expr_ref r(m);
+        expr_ref r(q, m);
         proof_ref pr(m);
-        m_der(q, r, pr);
+        ctx.rewrite(r);
+        m_der(r, r, pr);
+        if (ctx.get_config().m_qe_lite) {
+            qe_lite qe(m, ctx.s().params());
+            qe(r);
+        }
         m_expanded.reset();
-        if (r != q) {
-            ctx.get_rewriter()(r);
-            m_expanded.push_back(r);
-            return true;
+        bool updated = q != r;
+        if (updated) {
+            ctx.rewrite(r);
+            if (!is_quantifier(r)) {
+                m_expanded.push_back(r);
+                return true;
+            }            
+            if (is_forall(q)  != is_forall(r)) {
+                m_expanded.push_back(r);
+                return true;
+            }
+            q = to_quantifier(r);
         }
         if (is_forall(q)) 
             flatten_and(q->get_expr(), m_expanded);
@@ -253,6 +286,11 @@ namespace q {
                     idx = i;
                 }
             }
+            if (!e1 && updated) {
+                m_expanded.reset();
+                m_expanded.push_back(r);
+                return true;
+            }
             if (!e1)
                 return false;
 
@@ -267,12 +305,19 @@ namespace q {
         if (m_expanded.size() > 1) {
             for (unsigned i = m_expanded.size(); i-- > 0; ) {
                 expr_ref tmp(m.update_quantifier(q, m_expanded.get(i)), m);
-                ctx.get_rewriter()(tmp);
+                ctx.rewrite(tmp);
                 m_expanded[i] = tmp;
             }
             return true;
         }
-        return false;
+        else if (m_expanded.size() == 1 && updated) {
+            m_expanded[0] = r;
+            flatten(to_quantifier(r));
+            return true;
+        }
+        else {
+            return false;
+        }
     }
 
     bool solver::split(expr* arg, expr_ref& e1, expr_ref& e2) {

src/sat/smt/q_solver.h

@@ -83,6 +83,7 @@ namespace q {
         void init_search() override;
         void finalize_model(model& mdl) override;
         bool is_shared(euf::theory_var v) const override { return true; }
+        void relevant_eh(euf::enode* n) override { m_ematch.relevant_eh(n); }
 
         ast_manager& get_manager() { return m; }
         sat::literal_vector const& universal() const { return m_universal; }

src/sat/smt/recfun_solver.cpp

@@ -68,8 +68,8 @@ namespace recfun {
         TRACEFN("case expansion " << e);
         SASSERT(e.m_def->is_fun_macro());
         auto & vars = e.m_def->get_vars();
-        auto lhs = e.m_lhs;
-        auto rhs = apply_args(vars, e.m_args, e.m_def->get_rhs());
+        app_ref lhs = e.m_lhs;
+        expr_ref rhs = apply_args(vars, e.m_args, e.m_def->get_rhs());
         unsigned generation = std::max(ctx.get_max_generation(lhs), ctx.get_max_generation(rhs));
         euf::solver::scoped_generation _sgen(ctx, generation + 1);
         auto eq = eq_internalize(lhs, rhs);

src/sat/smt/sat_dual_solver.cpp

@@ -1,185 +0,0 @@
-/*++
-Copyright (c) 2020 Microsoft Corporation
-
-Module Name:
-
-    sat_dual_solver.cpp
-
-Abstract:
-
-    Solver for obtaining implicant.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2020-08-25
-
---*/
-#include "sat/smt/sat_dual_solver.h"
-
-namespace sat {
-
-    dual_solver::dual_solver(reslimit& l):
-        m_solver(m_params, l)
-    {
-        SASSERT(!m_solver.get_config().m_drat);
-        m_solver.set_incremental(true);
-    }
-
-    void dual_solver::flush() {
-        while (m_num_scopes > 0) {
-            m_solver.user_push();
-            m_roots.push_scope();
-            m_tracked_vars.push_scope();
-            m_units.push_scope();
-            m_vars.push_scope();
-            --m_num_scopes;
-        }
-    }
-
-    void dual_solver::push() {
-        ++m_num_scopes;
-    }
-
-    void dual_solver::pop(unsigned num_scopes) {        
-        if (m_num_scopes >= num_scopes) {
-            m_num_scopes -= num_scopes;
-            return;
-        }
-        num_scopes -= m_num_scopes;
-        m_num_scopes = 0;
-        m_solver.user_pop(num_scopes);
-        unsigned old_sz = m_tracked_vars.old_size(num_scopes);
-        for (unsigned i = m_tracked_vars.size(); i-- > old_sz; )
-            m_is_tracked[m_tracked_vars[i]] = false; 
-        old_sz = m_vars.old_size(num_scopes);
-        for (unsigned i = m_vars.size(); i-- > old_sz; ) {
-            unsigned v = m_vars[i];
-            unsigned w = m_ext2var[v];
-            m_ext2var[v] = null_bool_var;
-            m_var2ext[w] = null_bool_var;
-        }
-        m_vars.pop_scope(num_scopes);
-        m_units.pop_scope(num_scopes);
-        m_roots.pop_scope(num_scopes);
-        m_tracked_vars.pop_scope(num_scopes);
-    }
-
-    bool_var dual_solver::ext2var(bool_var v) {
-        bool_var w = m_ext2var.get(v, null_bool_var);
-        if (null_bool_var == w) {
-            w = m_solver.mk_var();
-            m_solver.set_external(w);
-            m_ext2var.setx(v, w, null_bool_var);
-            m_var2ext.setx(w, v, null_bool_var);
-            m_vars.push_back(v);
-        }
-        return w;
-    }
-
-    void dual_solver::track_relevancy(bool_var w) {
-        flush();
-        bool_var v = ext2var(w);
-        if (!m_is_tracked.get(v, false)) {
-            m_is_tracked.setx(v, true, false);
-            m_tracked_vars.push_back(v);
-        }
-    }
-
-    literal dual_solver::ext2lit(literal lit) {
-        return literal(ext2var(lit.var()), lit.sign());
-    }
-
-    literal dual_solver::lit2ext(literal lit) {
-        return literal(m_var2ext[lit.var()], lit.sign());
-    }
-
-    void dual_solver::add_root(unsigned sz, literal const* clause) {      
-        flush();
-        if (false && sz == 1) {
-            TRACE("dual", tout << "unit: " << clause[0] << "\n";);
-            m_units.push_back(clause[0]);
-            return;
-        }
-        literal root;
-        if (sz == 1) 
-            root = ext2lit(clause[0]);
-        else {
-            root = literal(m_solver.mk_var(), false);
-            for (unsigned i = 0; i < sz; ++i)
-                m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
-        }        
-        m_solver.set_external(root.var());
-        m_roots.push_back(~root);
-        TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";);
-    }
-
-    void dual_solver::add_aux(unsigned sz, literal const* clause) {
-        flush();        
-        m_lits.reset();
-        for (unsigned i = 0; i < sz; ++i) 
-            m_lits.push_back(ext2lit(clause[i]));
-        TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << " -> " << m_lits << "\n";);
-        m_solver.mk_clause(sz, m_lits.data(), status::input());
-    }
-
-    void dual_solver::add_assumptions(solver const& s) {
-        flush();
-        m_lits.reset();
-        for (bool_var v : m_tracked_vars)
-            m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
-        for (auto lit : m_units) {
-            bool_var w = m_ext2var.get(lit.var(), null_bool_var);
-            if (w != null_bool_var)
-                m_lits.push_back(ext2lit(lit));            
-        }
-    }
-
-    bool dual_solver::operator()(solver const& s) {        
-        m_core.reset();
-        m_core.append(m_units);
-        if (m_roots.empty())
-            return true;
-        m_solver.user_push();
-        m_solver.add_clause(m_roots.size(), m_roots.data(), status::input());
-        add_assumptions(s);
-        lbool is_sat = m_solver.check(m_lits.size(), m_lits.data());
-        if (is_sat == l_false) 
-            for (literal lit : m_solver.get_core())
-                m_core.push_back(lit2ext(lit));        
-        if (is_sat == l_true) {
-            TRACE("dual", display(s, tout); s.display(tout););
-            IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n");
-            UNREACHABLE();
-            return false;
-        }
-        TRACE("dual", m_solver.display(tout << "is-sat: " << is_sat << " core: " << m_core << "\n"););
-        m_solver.user_pop(1);
-        return is_sat == l_false;
-    }
-
-    std::ostream& dual_solver::display(solver const& s, std::ostream& out) const {        
-        for (unsigned v = 0; v < m_solver.num_vars(); ++v) {
-            bool_var w = m_var2ext.get(v, null_bool_var);
-            if (w == null_bool_var)
-                continue;
-            lbool v1 = m_solver.value(v);
-            lbool v2 = s.value(w);
-            if (v1 == v2 || v2 == l_undef)
-                continue;
-            out << "ext: " << w << " " << v2 << "\n";
-            out << "int: " << v << " " << v1 << "\n";
-        }
-        literal_vector lits;
-        for (bool_var v : m_tracked_vars) 
-            lits.push_back(literal(m_var2ext[v], l_false == s.value(m_var2ext[v])));
-        out << "tracked: " << lits << "\n";  
-        lits.reset();
-        for (literal r : m_roots) 
-            if (m_solver.value(r) == l_true)
-                lits.push_back(r);
-        out << "roots: " << lits << "\n";
-        m_solver.display(out);
-
-        return out;
-    }
-}

src/sat/smt/sat_dual_solver.h

@@ -1,83 +0,0 @@
-/*++
-Copyright (c) 2020 Microsoft Corporation
-
-Module Name:
-
-    sat_dual_solver.h
-
-Abstract:
-
-    Solver for obtaining implicant.
-    Based on an idea by Armin Biere to use dual propagation 
-    for representation of negated goal.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2020-08-25
-
---*/
-#pragma once
-#include "util/lim_vector.h"
-#include "sat/sat_solver.h"
-
-namespace sat {
-
-    class dual_solver {
-        class dual_params : public no_drat_params {
-        public:
-            dual_params() {
-                set_bool("core.minimize", false);
-            }
-        };
-        dual_params     m_params;
-        solver          m_solver;
-        lim_svector<literal> m_units, m_roots;
-        lim_svector<bool_var> m_tracked_vars;
-        literal_vector  m_lits, m_core;
-        bool_var_vector m_is_tracked;
-        unsigned_vector m_ext2var;
-        unsigned_vector m_var2ext;
-        lim_svector<unsigned> m_vars;
-        unsigned        m_num_scopes = 0;
-        void add_literal(literal lit);
-
-        bool_var ext2var(bool_var v);
-        bool_var var2ext(bool_var v);
-        literal  ext2lit(literal lit);
-        literal  lit2ext(literal lit);
-
-        void add_assumptions(solver const& s);
-
-        std::ostream& display(solver const& s, std::ostream& out) const;
-
-        void flush();
-
-    public:
-        dual_solver(reslimit& l);
-        void push();
-        void pop(unsigned num_scopes);
-
-        /*
-        * track model relevancy for variable 
-        */
-        void track_relevancy(bool_var v);
-
-        /*
-        * Add a root clause from the input problem.
-        * At least one literal has to be satisfied in every root.
-        */
-        void add_root(unsigned sz, literal const* clause);
-
-        /*
-        * Add auxiliary clauses that originate from compiling definitions.
-        */
-        void add_aux(unsigned sz, literal const* clause);
-
-        /*
-        * Extract a minimized subset of relevant literals from a model for s.
-        */
-        bool operator()(solver const& s);
-
-        literal_vector const& core() const { return m_core; }
-    };
-}

src/sat/smt/sat_th.cpp

@@ -132,6 +132,7 @@ namespace euf {
     bool th_euf_solver::add_unit(sat::literal lit) {
         bool was_true = is_true(lit);
         ctx.s().add_clause(1, &lit, mk_status());
+        ctx.add_root(lit);
         return !was_true;
     }
 
@@ -143,32 +144,27 @@ namespace euf {
         return is_new;
     }
 
-    bool th_euf_solver::add_clause(sat::literal a, sat::literal b) {
-        bool was_true = is_true(a, b);
+    bool th_euf_solver::add_clause(sat::literal a, sat::literal b) {      
         sat::literal lits[2] = { a, b };
-        ctx.s().add_clause(2, lits, mk_status());
-        return !was_true;
+        return add_clause(2, lits);
     }
 
-    bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {
-        bool was_true = is_true(a, b, c);
+    bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {      
         sat::literal lits[3] = { a, b, c };
-        ctx.s().add_clause(3, lits, mk_status());
-        return !was_true;
+        return add_clause(3, lits);
     }
 
     bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) {
-        bool was_true = is_true(a, b, c, d);
         sat::literal lits[4] = { a, b, c, d };
-        ctx.s().add_clause(4, lits, mk_status());
-        return !was_true;
+        return add_clause(4, lits);
     }
 
-    bool th_euf_solver::add_clause(sat::literal_vector const& lits) {
+    bool th_euf_solver::add_clause(unsigned n, sat::literal* lits) {
         bool was_true = false;
-        for (auto lit : lits)
-            was_true |= is_true(lit);
-        s().add_clause(lits.size(), lits.data(), mk_status());
+        for (unsigned i = 0; i < n; ++i)       
+            was_true |= is_true(lits[i]);
+        ctx.add_root(n, lits);
+        s().add_clause(n, lits, mk_status());
         return !was_true;
     }
 

src/sat/smt/sat_th.h

@@ -95,6 +95,11 @@ namespace euf {
           \brief conclude model building
         */
         virtual void finalize_model(model& mdl) {}
+
+        /**
+        * \brief does solver have an unhandled function.
+        */
+        virtual bool has_unhandled() const { return false; }
     };
 
     class th_solver : public sat::extension, public th_model_builder, public th_decompile, public th_internalizer {
@@ -111,6 +116,12 @@ namespace euf {
 
         virtual void new_diseq_eh(euf::th_eq const& eq) {}
 
+        virtual bool enable_ackerman_axioms(euf::enode* n) const { return true; }
+
+        virtual bool is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) { return false; }
+
+        virtual void relevant_eh(euf::enode* n) {}
+
         /**
            \brief Parametric theories (e.g. Arrays) should implement this method.
         */
@@ -139,7 +150,8 @@ namespace euf {
         bool add_clause(sat::literal a, sat::literal b);
         bool add_clause(sat::literal a, sat::literal b, sat::literal c);
         bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d);
-        bool add_clause(sat::literal_vector const& lits);
+        bool add_clause(sat::literal_vector const& lits) { return add_clause(lits.size(), lits.data()); }
+        bool add_clause(unsigned n, sat::literal* lits);
         void add_equiv(sat::literal a, sat::literal b);
         void add_equiv_and(sat::literal a, sat::literal_vector const& bs);
 

src/sat/smt/user_solver.cpp

@@ -36,6 +36,10 @@ namespace user_solver {
             return n->get_th_var(get_id());
         euf::theory_var v = mk_var(n);
         ctx.attach_th_var(n, this, v);
+        expr_ref r(m);
+        sat::literal_vector explain;
+        if (ctx.is_fixed(n, r, explain))
+            m_prop.push_back(prop_info(explain, v, r));
         return v;
     }
 
@@ -93,6 +97,18 @@ namespace user_solver {
         m_pop_eh(m_user_context, num_scopes);
     }
 
+    void solver::propagate_consequence(prop_info const& prop) {
+        sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true);
+        if (s().value(lit) != l_true) {
+            s().assign(lit, mk_justification(m_qhead));
+            ++m_stats.m_num_propagations;
+        }
+    }
+
+    void solver::propagate_new_fixed(prop_info const& prop) {
+        new_fixed_eh(prop.m_var, prop.m_conseq, prop.m_lits.size(), prop.m_lits.data());
+    }
+
     bool solver::unit_propagate() {
         if (m_qhead == m_prop.size())
             return false;
@@ -100,12 +116,11 @@ namespace user_solver {
         ctx.push(value_trail<unsigned>(m_qhead));
         unsigned np = m_stats.m_num_propagations;
         for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) {
-            auto const& prop = m_prop[m_qhead];            
-            sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true);
-            if (s().value(lit) != l_true) {
-                s().assign(lit, mk_justification(m_qhead));
-                ++m_stats.m_num_propagations;
-            }
+            auto const& prop = m_prop[m_qhead];
+            if (prop.m_var == euf::null_theory_var)
+                propagate_consequence(prop);
+            else
+                propagate_new_fixed(prop);
         }       
         return np < m_stats.m_num_propagations;
     }
@@ -171,5 +186,51 @@ namespace user_solver {
         return result;
     }
 
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        if (!visit_rec(m, e, sign, root, redundant)) {
+            TRACE("array", tout << mk_pp(e, m) << "\n";);
+            return sat::null_literal;
+        }
+        sat::literal lit = ctx.expr2literal(e);
+        if (sign)
+            lit.neg();
+        if (root)
+            add_unit(lit);
+        return lit;
+    }
+
+    void solver::internalize(expr* e, bool redundant) {
+        visit_rec(m, e, false, false, redundant);
+    }
+
+    bool solver::visit(expr* e) {
+        if (visited(e))
+            return true;
+        if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
+            ctx.internalize(e, m_is_redundant);
+            return true;
+        }
+        m_stack.push_back(sat::eframe(e));
+        return false;        
+    }
+    
+    bool solver::visited(expr* e) {
+        euf::enode* n = expr2enode(e);
+        return n && n->is_attached_to(get_id());        
+    }
+    
+    bool solver::post_visit(expr* e, bool sign, bool root) {
+        euf::enode* n = expr2enode(e);
+        SASSERT(!n || !n->is_attached_to(get_id()));
+        if (!n) 
+            n = mk_enode(e, false);        
+        auto v = add_expr(e);
+        if (m_created_eh)
+            m_created_eh(m_user_context, this, e, v);
+        return true;
+    }
+
+
+
 }
 

src/sat/smt/user_solver.h

@@ -32,6 +32,9 @@ namespace user_solver {
             unsigned_vector m_ids;
             expr_ref        m_conseq;
             svector<std::pair<unsigned, unsigned>> m_eqs;
+            sat::literal_vector                    m_lits;
+            euf::theory_var                        m_var = euf::null_theory_var;
+
             prop_info(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr_ref const& c):
                 m_ids(num_fixed, fixed_ids),
                 m_conseq(c)
@@ -39,6 +42,12 @@ namespace user_solver {
                 for (unsigned i = 0; i < num_eqs; ++i)
                     m_eqs.push_back(std::make_pair(eq_lhs[i], eq_rhs[i]));
             }
+
+            prop_info(sat::literal_vector const& lits, euf::theory_var v, expr_ref const& val):
+                m_conseq(val),
+                m_lits(lits),
+                m_var(v) {}
+
         };
 
         struct stats {
@@ -55,6 +64,7 @@ namespace user_solver {
         user_propagator::fixed_eh_t     m_fixed_eh;
         user_propagator::eq_eh_t        m_eq_eh;
         user_propagator::eq_eh_t        m_diseq_eh;
+        user_propagator::created_eh_t   m_created_eh;
         user_propagator::context_obj*   m_api_context = nullptr;
         unsigned               m_qhead = 0;
         vector<prop_info>      m_prop;
@@ -80,8 +90,15 @@ namespace user_solver {
 
         sat::justification mk_justification(unsigned propagation_index);
 
+        void propagate_consequence(prop_info const& prop);
+        void propagate_new_fixed(prop_info const& prop);
+
 	void validate_propagation();
 
+        bool visit(expr* e) override;
+        bool visited(expr* e) override;
+        bool post_visit(expr* e, bool sign, bool root) override;
+
     public:
         solver(euf::solver& ctx);
         
@@ -107,6 +124,7 @@ namespace user_solver {
         void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }
         void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; }
         void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; }
+        void register_created(user_propagator::created_eh_t& created_eh) { m_created_eh = created_eh; }
 
         bool has_fixed() const { return (bool)m_fixed_eh; }
 
@@ -122,8 +140,8 @@ namespace user_solver {
         bool unit_propagate() override;
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override;
         void collect_statistics(statistics& st) const override;
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override { UNREACHABLE(); return sat::null_literal; }
-        void internalize(expr* e, bool redundant) override { UNREACHABLE(); }
+        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
+        void internalize(expr* e, bool redundant) override;
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;

src/sat/tactic/goal2sat.cpp

@@ -125,20 +125,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     bool top_level_relevant() {
         return m_top_level && relevancy_enabled();
     }
-
-    void add_dual_def(unsigned n, sat::literal const* lits) {
-        if (relevancy_enabled())
-            ensure_euf()->add_aux(n, lits);        
-    }
-
-    void add_dual_root(unsigned n, sat::literal const* lits) {
-        if (relevancy_enabled())
-            ensure_euf()->add_root(n, lits);
-    }
-
-    void add_dual_root(sat::literal lit) {
-        add_dual_root(1, &lit);
-    }
     
     void mk_clause(sat::literal l) {
         mk_clause(1, &l);
@@ -156,7 +142,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     void mk_clause(unsigned n, sat::literal * lits) {
         TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
-        add_dual_def(n, lits);
+        if (relevancy_enabled())
+            ensure_euf()->add_aux(n, lits);
         m_solver.add_clause(n, lits, mk_status());
     }
 
@@ -176,7 +163,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     void mk_root_clause(unsigned n, sat::literal * lits) {
         TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
-        add_dual_root(n, lits);
+        if (relevancy_enabled())
+            ensure_euf()->add_root(n, lits);
         m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input());
     }
 
@@ -186,8 +174,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
             return v;
         v = m_solver.add_var(is_ext);
         log_def(v, n);
-        if (top_level_relevant() && !is_bool_op(n))
-            ensure_euf()->track_relevancy(v);
         return v;
     }
 
@@ -216,14 +202,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (!m_expr2var_replay || !m_expr2var_replay->find(t, v))  
             v = add_var(true, t);
         m_map.insert(t, v);
-        if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) {
-            add_dual_root(sat::literal(v, m.is_false(t)));
-            ensure_euf()->track_relevancy(v);
-        }
         return v;
     }
 
     sat::bool_var add_bool_var(expr* t) override {
+        force_push();
         sat::bool_var v = m_map.to_bool_var(t);
         if (v == sat::null_bool_var) 
             v = mk_bool_var(t);
@@ -238,11 +221,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
         for (; m_num_scopes > 0; --m_num_scopes) {
             m_map.push();
             m_cache_lim.push_back(m_cache_trail.size());
-        }
+        }        
     }
 
     void push() override {
-        ++m_num_scopes;
+        ++m_num_scopes;        
     }
 
     void pop(unsigned n) override {
@@ -263,7 +246,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             }
         }
         m_cache_trail.shrink(k);
-        m_cache_lim.shrink(m_cache_lim.size() - n);                              
+        m_cache_lim.shrink(m_cache_lim.size() - n);    
     }
 
     // remove non-external literals from cache.
@@ -677,8 +660,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
         if (lit == sat::null_literal) 
             return;
-        if (top_level_relevant())
-            euf->track_relevancy(lit.var());
         if (root)
             mk_root_clause(lit);
         else

src/sat/tactic/sat_tactic.cpp

@@ -201,8 +201,8 @@ public:
     char const* name() const override { return "sat"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
-        if (m_imp) m_imp->updt_params(p);
+        m_params.append(p);
+        if (m_imp) m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {