Merge branch 'master' into polysat

src/sat/smt/CMakeLists.txt

@@ -22,6 +22,7 @@ z3_add_component(sat_smt
     euf_invariant.cpp
     euf_model.cpp
     euf_proof.cpp
+    euf_proof_checker.cpp
     euf_relevancy.cpp
     euf_solver.cpp
     fpa_solver.cpp

src/sat/smt/arith_axioms.cpp

@@ -264,11 +264,12 @@ namespace arith {
         SASSERT(k1 != k2 || kind1 != kind2);
 
         auto bin_clause = [&](sat::literal l1, sat::literal l2) {
-            sat::proof_hint* bound_params = nullptr;
+            arith_proof_hint* bound_params = nullptr;
             if (ctx.use_drat()) {
-                bound_params = &m_farkas2;
-                m_farkas2.m_literals[0] = std::make_pair(rational(1), ~l1);
-                m_farkas2.m_literals[1] = std::make_pair(rational(1), ~l2);
+                m_arith_hint.set_type(ctx, hint_type::farkas_h);
+                m_arith_hint.add_lit(rational(1), ~l1);
+                m_arith_hint.add_lit(rational(1), ~l2);
+                bound_params = m_arith_hint.mk(ctx);
             }
             add_clause(l1, l2, bound_params);            
         };

src/sat/smt/arith_diagnostics.cpp

@@ -15,6 +15,8 @@ Author:
 
 --*/
 
+#include "ast/ast_util.h"
+#include "ast/scoped_proof.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/arith_solver.h"
 
@@ -81,7 +83,6 @@ namespace arith {
     }
 
     void solver::explain_assumptions() {
-        m_arith_hint.reset();
         unsigned i = 0;
         for (auto const & ev : m_explanation) {
             ++i;
@@ -91,14 +92,12 @@ namespace arith {
             switch (m_constraint_sources[idx]) {
             case inequality_source: {
                 literal lit = m_inequalities[idx];
-                m_arith_hint.m_literals.push_back({ev.coeff(), lit});
+                m_arith_hint.add_lit(ev.coeff(), lit);
                 break;                
             }
             case equality_source: {
                 auto [u, v] = m_equalities[idx];
-                ctx.drat_log_expr(u->get_expr());
-                ctx.drat_log_expr(v->get_expr());
-                m_arith_hint.m_eqs.push_back({u->get_expr_id(), v->get_expr_id()});
+                m_arith_hint.add_eq(u, v);
                 break;
             }
             default:
@@ -115,22 +114,65 @@ namespace arith {
      * such that there is a r >= 1
      * (r1*a1+..+r_k*a_k) = r*a, (r1*b1+..+r_k*b_k) <= r*b
      */
-    sat::proof_hint const* solver::explain(sat::hint_type ty, sat::literal lit) {
+    arith_proof_hint const* solver::explain(hint_type ty, sat::literal lit) {
         if (!ctx.use_drat())
             return nullptr;
-        m_arith_hint.m_ty = ty;
+        m_arith_hint.set_type(ctx, ty);
         explain_assumptions();
         if (lit != sat::null_literal)
-            m_arith_hint.m_literals.push_back({rational(1), ~lit});
-        return &m_arith_hint;
+            m_arith_hint.add_lit(rational(1), ~lit);
+        return m_arith_hint.mk(ctx);
     }
 
-    sat::proof_hint const* solver::explain_implied_eq(euf::enode* a, euf::enode* b) {
+    arith_proof_hint const* solver::explain_implied_eq(euf::enode* a, euf::enode* b) {
         if (!ctx.use_drat())
             return nullptr;
-        m_arith_hint.m_ty = sat::hint_type::implied_eq_h;
+        m_arith_hint.set_type(ctx, hint_type::implied_eq_h);
         explain_assumptions();
-        m_arith_hint.m_diseqs.push_back({a->get_expr_id(), b->get_expr_id()});
-        return &m_arith_hint;
+        m_arith_hint.add_diseq(a, b);
+        return m_arith_hint.mk(ctx);
+    }
+
+    expr* arith_proof_hint::get_hint(euf::solver& s) const {
+        ast_manager& m = s.get_manager();
+        family_id fid = m.get_family_id("arith");
+        arith_util arith(m);
+        solver& a = dynamic_cast<solver&>(*s.fid2solver(fid));
+        char const* name;
+        switch (m_ty) {
+        case hint_type::farkas_h:
+            name = "farkas";
+            break;
+        case hint_type::bound_h:
+            name = "bound";
+            break;
+        case hint_type::implied_eq_h:
+            name = "implied-eq";
+            break;
+        }
+        rational lc(1);
+        for (unsigned i = m_lit_head; i < m_lit_tail; ++i) 
+            lc = lcm(lc, denominator(a.m_arith_hint.lit(i).first));
+            
+        expr_ref_vector args(m);
+        sort_ref_vector sorts(m);
+        for (unsigned i = m_lit_head; i < m_lit_tail; ++i) {            
+            auto const& [coeff, lit] = a.m_arith_hint.lit(i);
+            args.push_back(arith.mk_int(abs(coeff*lc)));
+            args.push_back(s.literal2expr(lit));
+        }
+        for (unsigned i = m_eq_head; i < m_eq_tail; ++i) {
+            auto const& [x, y, is_eq] = a.m_arith_hint.eq(i);            
+            expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m);
+            if (!is_eq) eq = m.mk_not(eq);
+            args.push_back(arith.mk_int(1));
+            args.push_back(eq);
+        }
+        for (expr* arg : args)
+            sorts.push_back(arg->get_sort());
+        sort* range = m.mk_proof_sort();
+        func_decl* d = m.mk_func_decl(symbol(name), args.size(), sorts.data(), range);
+        expr* r = m.mk_app(d, args);
+        return r;
     }
 }

src/sat/smt/arith_proof_checker.h

@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2020 Microsoft Corporation
+Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
 
@@ -11,7 +11,15 @@ Abstract:
 
 Author:
 
-    Nikolaj Bjorner (nbjorner) 2020-09-08
+    Nikolaj Bjorner (nbjorner) 2022-08-28
+
+Notes:
+
+The module assumes a limited repertoire of arithmetic proof rules.
+
+- farkas - inequalities, equalities and disequalities with coefficients
+- implied-eq - last literal is a disequality. The literals before imply the corresponding equality.
+- bound - last literal is a bound. It is implied by prior literals.
 
 --*/
 #pragma once
@@ -19,11 +27,12 @@ Author:
 #include "util/obj_pair_set.h"
 #include "ast/ast_trail.h"
 #include "ast/arith_decl_plugin.h"
+#include "sat/smt/euf_proof_checker.h"
 
 
 namespace arith {
 
-    class proof_checker {
+    class proof_checker : public euf::proof_checker_plugin {
         struct row {
             obj_map<expr, rational> m_coeffs;
             rational m_coeff;
@@ -32,16 +41,19 @@ namespace arith {
                 m_coeff = 0;
             }
         };
-        
+       
         ast_manager& m;
-        arith_util a;
+        arith_util   a;
         vector<std::pair<rational, expr*>> m_todo;
-        bool m_strict = false;
-        row m_ineq;
-        row m_conseq;
-        vector<row> m_eqs;
-        vector<row> m_ineqs;
-        vector<row> m_diseqs;
+        bool         m_strict = false;
+        row          m_ineq;
+        row          m_conseq;
+        vector<row>  m_eqs;
+        vector<row>  m_ineqs;
+        vector<row>  m_diseqs;
+        symbol       m_farkas;
+        symbol       m_implied_eq;
+        symbol       m_bound;
         
         void add(row& r, expr* v, rational const& coeff) {
             rational coeff1;
@@ -131,11 +143,15 @@ namespace arith {
             SASSERT(m_todo.empty());
             m_todo.push_back({ mul, e });
             rational coeff1;
-            expr* e1, *e2;
+            expr* e1, *e2, *e3;
             for (unsigned i = 0; i < m_todo.size(); ++i) {
                 auto [coeff, e] = m_todo[i];
                 if (a.is_mul(e, e1, e2) && a.is_numeral(e1, coeff1))
                     m_todo.push_back({coeff*coeff1, e2});
+                else if (a.is_mul(e, e1, e2) && a.is_uminus(e1, e3) && a.is_numeral(e3, coeff1))
+                    m_todo.push_back({-coeff*coeff1, e2});
+                else if (a.is_mul(e, e1, e2) && a.is_uminus(e2, e3) && a.is_numeral(e3, coeff1))
+                    m_todo.push_back({ -coeff * coeff1, e1 });
                 else if (a.is_mul(e, e1, e2) && a.is_numeral(e2, coeff1))
                     m_todo.push_back({coeff*coeff1, e1});
                 else if (a.is_add(e))
@@ -149,6 +165,8 @@ namespace arith {
                 }
                 else if (a.is_numeral(e, coeff1)) 
                     r.m_coeff += coeff*coeff1;
+                else if (a.is_uminus(e, e1) && a.is_numeral(e1, coeff1))
+                    r.m_coeff -= coeff*coeff1;
                 else
                     add(r, e, coeff);
             }
@@ -296,10 +314,16 @@ namespace arith {
             rows.push_back(row());
             return rows.back();
         }
-
         
     public:
-        proof_checker(ast_manager& m): m(m), a(m) {}
+        proof_checker(ast_manager& m): 
+            m(m), 
+            a(m), 
+            m_farkas("farkas"), 
+            m_implied_eq("implied-eq"), 
+            m_bound("bound") {}
+
+        ~proof_checker() override {}
         
         void reset() {
             m_ineq.reset();
@@ -313,7 +337,8 @@ namespace arith {
         bool add_ineq(rational const& coeff, expr* e, bool sign) {
             if (!m_diseqs.empty())
                 return add_literal(fresh(m_ineqs), abs(coeff), e, sign);
-            return add_literal(m_ineq, abs(coeff), e, sign);
+            else 
+                return add_literal(m_ineq, abs(coeff), e, sign);
         }
         
         bool add_conseq(rational const& coeff, expr* e, bool sign) {
@@ -350,6 +375,76 @@ namespace arith {
             return out;
         }
 
+        bool check(expr_ref_vector const& clause, app* jst, expr_ref_vector& units) override {
+            reset();
+            expr_mark pos, neg;
+            for (expr* e : clause)
+                if (m.is_not(e, e))
+                    neg.mark(e, true);
+                else
+                    pos.mark(e, true);
+
+            if (jst->get_name() != m_farkas &&
+                jst->get_name() != m_bound &&
+                jst->get_name() != m_implied_eq) {
+                IF_VERBOSE(0, verbose_stream() << "unhandled inference " << mk_pp(jst, m) << "\n");
+                return false;
+            }
+            bool is_bound = jst->get_name() == m_bound;
+            bool even = true;
+            rational coeff;
+            expr* x, * y;
+            unsigned j = 0;
+            for (expr* arg : *jst) {
+                if (even) {
+                    if (!a.is_numeral(arg, coeff)) {
+                        IF_VERBOSE(0, verbose_stream() << "not numeral " << mk_pp(jst, m) << "\n");
+                        return false;
+                    }
+                }
+                else {
+                    bool sign = m.is_not(arg, arg);
+                    if (a.is_le(arg) || a.is_lt(arg) || a.is_ge(arg) || a.is_gt(arg)) {
+                        if (is_bound && j + 1 == jst->get_num_args())
+                            add_conseq(coeff, arg, sign);
+                        else
+                            add_ineq(coeff, arg, sign);
+                    }
+                    else if (m.is_eq(arg, x, y)) {
+                        if (sign)
+                            add_diseq(x, y);
+                        else
+                            add_eq(x, y);
+                    }
+                    else {
+                        IF_VERBOSE(0, verbose_stream() << "not a recognized arithmetical relation " << mk_pp(arg, m) << "\n");
+                        return false;
+                    }
+
+                    if (sign && !pos.is_marked(arg)) {
+                        units.push_back(m.mk_not(arg));
+                        pos.mark(arg, false);
+                    }
+                    else if (!sign && !neg.is_marked(arg)) {
+                        units.push_back(arg);
+                        neg.mark(arg, false);
+                    }
+                }
+                even = !even;
+                ++j;
+            }
+            if (check()) 
+                return true;
+            
+            IF_VERBOSE(0, verbose_stream() << "did not check condition\n" << mk_pp(jst, m) << "\n"; display(verbose_stream()); );
+            return false;
+        }
+
+        void register_plugins(euf::proof_checker& pc) override {
+            pc.register_plugin(m_farkas, this);
+            pc.register_plugin(m_bound, this);
+            pc.register_plugin(m_implied_eq, this);
+        }
         
     };
 

src/sat/smt/arith_solver.cpp

@@ -39,8 +39,6 @@ namespace arith {
         lp().settings().set_random_seed(get_config().m_random_seed);
         
         m_lia = alloc(lp::int_solver, *m_solver.get());
-        m_farkas2.m_ty = sat::hint_type::farkas_h;
-        m_farkas2.m_literals.resize(2);
     }
 
     solver::~solver() {
@@ -197,11 +195,12 @@ namespace arith {
         reset_evidence();
         m_core.push_back(lit1);
         TRACE("arith", tout << lit2 << " <- " << m_core << "\n";);
-        sat::proof_hint* ph = nullptr;
+        arith_proof_hint* ph = nullptr;
         if (ctx.use_drat()) {
-            ph = &m_farkas2;
-            m_farkas2.m_literals[0] = std::make_pair(rational(1), lit1);
-            m_farkas2.m_literals[1] = std::make_pair(rational(1), ~lit2);
+            m_arith_hint.set_type(ctx, hint_type::farkas_h);
+            m_arith_hint.add_lit(rational(1), lit1);
+            m_arith_hint.add_lit(rational(1), ~lit2);
+            ph = m_arith_hint.mk(ctx);
         }
         assign(lit2, m_core, m_eqs, ph); 
         ++m_stats.m_bounds_propagations;
@@ -262,7 +261,7 @@ namespace arith {
             TRACE("arith", for (auto lit : m_core) tout << lit << ": " << s().value(lit) << "\n";);
             DEBUG_CODE(for (auto lit : m_core) { VERIFY(s().value(lit) == l_true); });
             ++m_stats.m_bound_propagations1;
-            assign(lit, m_core, m_eqs, explain(sat::hint_type::bound_h, lit));
+            assign(lit, m_core, m_eqs, explain(hint_type::bound_h, lit));
         }
 
         if (should_refine_bounds() && first)
@@ -378,7 +377,7 @@ namespace arith {
         reset_evidence();
         m_explanation.clear();
         lp().explain_implied_bound(be, m_bp);
-        assign(bound, m_core, m_eqs, explain(sat::hint_type::farkas_h, bound));
+        assign(bound, m_core, m_eqs, explain(hint_type::farkas_h, bound));
     }
 
 
@@ -386,20 +385,16 @@ namespace arith {
         TRACE("arith", tout << b << "\n";);
         lp::constraint_index ci = b.get_constraint(is_true);
         lp().activate(ci);
-        if (is_infeasible()) {
+        if (is_infeasible()) 
             return;
-        }
         lp::lconstraint_kind k = bound2constraint_kind(b.is_int(), b.get_bound_kind(), is_true);
-        if (k == lp::LT || k == lp::LE) {
+        if (k == lp::LT || k == lp::LE) 
             ++m_stats.m_assert_lower;
-        }
-        else {
+        else 
             ++m_stats.m_assert_upper;
-        }
         inf_rational value = b.get_value(is_true);
-        if (propagate_eqs() && value.is_rational()) {
+        if (propagate_eqs() && value.is_rational()) 
             propagate_eqs(b.tv(), ci, k, b, value.get_rational());
-        }
 #if 0
         if (propagation_mode() != BP_NONE)
             lp().mark_rows_for_bound_prop(b.tv().id());
@@ -617,8 +612,7 @@ namespace arith {
                        verbose_stream() << eval << " " << value << " " << ctx.bpp(n) << "\n";
                        verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n";
                        verbose_stream() << *b << "\n";);
-            IF_VERBOSE(0, ctx.display(verbose_stream()));
-            IF_VERBOSE(0, verbose_stream() << mdl << "\n");
+            IF_VERBOSE(0, ctx.display_validation_failure(verbose_stream(), mdl, n));
             UNREACHABLE();
         }
     }
@@ -1119,16 +1113,23 @@ namespace arith {
     }
 
     bool solver::check_delayed_eqs() {
-        for (auto p : m_delayed_eqs) {
+        bool found_diseq = false;
+        if (m_delayed_eqs_qhead == m_delayed_eqs.size())
+            return true;
+        force_push();
+        ctx.push(value_trail<unsigned>(m_delayed_eqs_qhead));
+        for (; m_delayed_eqs_qhead < m_delayed_eqs.size(); ++ m_delayed_eqs_qhead) {
+            auto p = m_delayed_eqs[m_delayed_eqs_qhead];
             auto const& e = p.first;
             if (p.second)
                 new_eq_eh(e);
             else if (is_eq(e.v1(), e.v2())) {
                 mk_diseq_axiom(e);
-                return false;
+                found_diseq = true;
+                break;
             }
-        }
-        return true;
+        }        
+        return !found_diseq;
     }
 
     lbool solver::check_lia() {
@@ -1178,7 +1179,7 @@ namespace arith {
             app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
             IF_VERBOSE(4, verbose_stream() << "cut " << b << "\n");
             literal lit = expr2literal(b);
-            assign(lit, m_core, m_eqs, explain(sat::hint_type::bound_h, lit));
+            assign(lit, m_core, m_eqs, explain(hint_type::bound_h, lit));
             lia_check = l_false;
             break;
         }
@@ -1200,7 +1201,7 @@ namespace arith {
         return lia_check;
     }
 
-    void solver::assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, sat::proof_hint const* pma) {        
+    void solver::assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, euf::th_proof_hint const* pma) {        
         if (core.size() < small_lemma_size() && eqs.empty()) {
             m_core2.reset();
             for (auto const& c : core)
@@ -1247,7 +1248,7 @@ namespace arith {
         for (literal& c : m_core)
             c.neg();
 
-        add_clause(m_core, explain(sat::hint_type::farkas_h));
+        add_clause(m_core, explain(hint_type::farkas_h));
     }
 
     bool solver::is_infeasible() const {

src/sat/smt/arith_solver.h

@@ -48,8 +48,61 @@ namespace arith {
     typedef sat::literal_vector literal_vector;
     typedef lp_api::bound<sat::literal> api_bound;
 
+    enum class hint_type {
+        farkas_h,
+        bound_h,
+        implied_eq_h    
+    };
+
+    struct arith_proof_hint : public euf::th_proof_hint {
+        hint_type                              m_ty;
+        unsigned m_lit_head, m_lit_tail, m_eq_head, m_eq_tail;
+        arith_proof_hint(hint_type t, unsigned lh, unsigned lt, unsigned eh, unsigned et):
+            m_ty(t), m_lit_head(lh), m_lit_tail(lt), m_eq_head(eh), m_eq_tail(et) {}
+        expr* get_hint(euf::solver& s) const override;
+    };
+
+    class arith_proof_hint_builder {
+        vector<std::pair<rational, literal>>   m_literals;
+        svector<std::tuple<euf::enode*,euf::enode*,bool>> m_eqs;
+        hint_type                              m_ty;
+        unsigned                               m_lit_head = 0, m_lit_tail = 0, m_eq_head = 0, m_eq_tail = 0;
+        void reset() { m_lit_head = m_lit_tail; m_eq_head = m_eq_tail; }
+        void add(euf::enode* a, euf::enode* b, bool is_eq) {
+            if (m_eq_tail < m_eqs.size()) 
+                m_eqs[m_eq_tail] = std::tuple(a, b, is_eq); 
+            else 
+                m_eqs.push_back(std::tuple(a, b, is_eq)); 
+            m_eq_tail++; 
+        }
+    public:
+        void set_type(euf::solver& ctx, hint_type ty) { 
+            ctx.push(value_trail<unsigned>(m_eq_tail)); 
+            ctx.push(value_trail<unsigned>(m_lit_tail)); 
+            m_ty = ty; 
+            reset(); 
+        }
+        void add_eq(euf::enode* a, euf::enode* b) { add(a, b, true); }
+        void add_diseq(euf::enode* a, euf::enode* b) { add(a, b, false); }
+        void add_lit(rational const& coeff, literal lit) { 
+            if (m_lit_tail < m_literals.size())
+                m_literals[m_lit_tail] = {coeff, lit};
+            else
+                m_literals.push_back({coeff, lit}); 
+            m_lit_tail++;
+        }
+        std::pair<rational, literal> const& lit(unsigned i) const { return m_literals[i]; }
+        std::tuple<enode*, enode*, bool> const& eq(unsigned i) const { return m_eqs[i]; }
+        arith_proof_hint* mk(euf::solver& s) { 
+            return new (s.get_region()) arith_proof_hint(m_ty, m_lit_head, m_lit_tail, m_eq_head, m_eq_tail);
+        }
+    };
+
+
     class solver : public euf::th_euf_solver {
 
+        friend struct arith_proof_hint;
+
         struct scope {
             unsigned m_bounds_lim;
             unsigned m_idiv_lim;
@@ -165,6 +218,7 @@ namespace arith {
         svector<euf::enode_pair>                      m_equalities;      // asserted rows corresponding to equalities.
         svector<theory_var>                           m_definitions;     // asserted rows corresponding to definitions
         svector<std::pair<euf::th_eq, bool>>          m_delayed_eqs;
+        unsigned                                      m_delayed_eqs_qhead = 0;
 
         literal_vector  m_asserted;
         expr* m_not_handled{ nullptr };
@@ -414,15 +468,15 @@ namespace arith {
         void set_conflict();
         void set_conflict_or_lemma(literal_vector const& core, bool is_conflict);
         void set_evidence(lp::constraint_index idx);
-        void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, sat::proof_hint const* pma);
+        void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, euf::th_proof_hint const* pma);
 
         void false_case_of_check_nla(const nla::lemma& l);        
         void dbg_finalize_model(model& mdl);
 
-        sat::proof_hint m_arith_hint;
-        sat::proof_hint m_farkas2;
-        sat::proof_hint const* explain(sat::hint_type ty, sat::literal lit = sat::null_literal);
-        sat::proof_hint const* explain_implied_eq(euf::enode* a, euf::enode* b);
+        arith_proof_hint_builder m_arith_hint;
+
+        arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal);
+        arith_proof_hint const* explain_implied_eq(euf::enode* a, euf::enode* b);
         void explain_assumptions();
 
 

src/sat/smt/array_axioms.cpp

@@ -265,7 +265,8 @@ namespace array {
         args1.push_back(e1);
         args2.push_back(e2);
         for (func_decl* f : funcs) {
-            expr* k = m.mk_app(f, e1, e2);
+            expr_ref k(m.mk_app(f, e1, e2), m);
+            rewrite(k);
             args1.push_back(k);
             args2.push_back(k);
         }
@@ -699,6 +700,23 @@ namespace array {
             n->unmark1();
     }
 
+    /**
+    * \brief check that lambda expressions are beta redexes.
+    * The array solver is not a decision procedure for lambdas that do not occur in beta 
+    * redexes.
+    */
+    bool solver::check_lambdas() {
+        unsigned num_vars = get_num_vars();
+        for (unsigned i = 0; i < num_vars; i++) {
+            auto* n = var2enode(i);
+            if (a.is_as_array(n->get_expr()) || is_lambda(n->get_expr()))
+                for (euf::enode* p : euf::enode_parents(n))
+                    if (!ctx.is_beta_redex(p, n))
+                        return false;
+        }
+        return true;
+    }
+
     bool solver::is_shared_arg(euf::enode* r) {
         SASSERT(r->is_root());
         for (euf::enode* n : euf::enode_parents(r)) {

src/sat/smt/array_internalize.cpp

@@ -252,6 +252,8 @@ namespace array {
             return p->get_arg(0)->get_root() == n->get_root();
         if (a.is_map(p->get_expr()))
             return true;
+        if (a.is_store(p->get_expr()))
+            return true;
         return false;
     }
 

src/sat/smt/array_solver.cpp

@@ -108,7 +108,9 @@ namespace array {
         if (m_delay_qhead < m_axiom_trail.size()) 
             return sat::check_result::CR_CONTINUE;
 
-        
+        if (!check_lambdas())
+            return sat::check_result::CR_GIVEUP;
+
         // validate_check();
         return sat::check_result::CR_DONE;
     }

src/sat/smt/array_solver.h

@@ -218,6 +218,7 @@ namespace array {
         bool should_prop_upward(var_data const& d) const;
         bool can_beta_reduce(euf::enode* n) const { return can_beta_reduce(n->get_expr()); }
         bool can_beta_reduce(expr* e) const;
+        bool check_lambdas();
 
         var_data& get_var_data(euf::enode* n) { return get_var_data(n->get_th_var(get_id())); }
         var_data& get_var_data(theory_var v) { return *m_var_data[v]; }

src/sat/smt/bv_ackerman.cpp

@@ -49,16 +49,19 @@ namespace bv {
         update_glue(*other);
 
         vv::push_to_front(m_queue, other);
-        if (other == n) {
+        bool do_gc = other == n;
+        if (other == n) 
             new_tmp();        
-            gc();
-        }
+               
         if (other->m_glue == 0) {
+            do_gc = false;
             remove(other);
             add_cc(v1, v2);
         }
-        else if (other->m_count > m_propagate_high_watermark) 
-            s.s().set_should_simplify();
+        else if (other->m_count > 2*m_propagate_high_watermark) 
+            propagate();
+        if (do_gc)
+            gc();
     }
 
     void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) {
@@ -76,8 +79,8 @@ namespace bv {
             new_tmp();
             gc();
         }
-        if (other->m_count > m_propagate_high_watermark) 
-            s.s().set_should_simplify();
+        if (other->m_count > 2*m_propagate_high_watermark) 
+            propagate();
     }
 
     void ackerman::update_glue(vv& v) {
@@ -137,6 +140,9 @@ namespace bv {
         if (m_num_propagations_since_last_gc <= s.get_config().m_dack_gc) 
             return;
         m_num_propagations_since_last_gc = 0;
+
+        if (m_table.size() > m_gc_threshold) 
+            propagate();
         
         while (m_table.size() > m_gc_threshold) 
             remove(m_queue->prev());     
@@ -147,7 +153,6 @@ namespace bv {
     }
 
     void ackerman::propagate() {
-        SASSERT(s.s().at_base_lvl());
         auto* n = m_queue;
         vv* k = nullptr;
         unsigned num_prop = static_cast<unsigned>(s.s().get_stats().m_conflict * s.get_config().m_dack_factor);

src/sat/smt/bv_ackerman.h

@@ -51,13 +51,13 @@ namespace bv {
 
         solver&       s;
         table_t       m_table;
-        vv*           m_queue { nullptr };
-        vv*           m_tmp_vv { nullptr };
+        vv*           m_queue = nullptr;
+        vv*           m_tmp_vv = nullptr;
 
-        unsigned      m_gc_threshold { 100 };
-        unsigned      m_propagate_high_watermark { 10000 };
-        unsigned      m_propagate_low_watermark { 10 };
-        unsigned      m_num_propagations_since_last_gc { 0 };
+        unsigned      m_gc_threshold = 100;
+        unsigned      m_propagate_high_watermark = 10000;
+        unsigned      m_propagate_low_watermark = 10;
+        unsigned      m_num_propagations_since_last_gc = 0;
         bool_vector   m_diff_levels;
 
         void update_glue(vv& v);

src/sat/smt/bv_delay_internalize.cpp

@@ -47,7 +47,7 @@ namespace bv {
             return true;
         unsigned num_vars = e->get_num_args();
         for (expr* arg : *e) 
-            if (!m.is_value(arg))
+            if (m.is_value(arg))
                 --num_vars;
         if (num_vars <= 1) 
             return true;
@@ -72,6 +72,55 @@ namespace bv {
         return expr_ref(bv.mk_numeral(val, get_bv_size(v)), m);
     }
 
+    /**
+       \brief expose the multiplication circuit lazily.
+       It adds clauses for multiplier output one by one to enforce
+       the semantics of multipliers.
+     */
+
+    bool solver::check_lazy_mul(app* e, expr* arg_value, expr* mul_value) {
+        SASSERT(e->get_num_args() >= 2);
+        expr_ref_vector args(m), new_args(m), new_out(m);
+        lazy_mul* lz = nullptr;
+        rational v0, v1;
+        unsigned sz, diff = 0;
+        VERIFY(bv.is_numeral(arg_value, v0, sz));
+        VERIFY(bv.is_numeral(mul_value, v1));
+        for (diff = 0; diff < sz; ++diff) 
+            if (v0.get_bit(diff) != v1.get_bit(diff))
+                break;
+        SASSERT(diff < sz);
+        auto set_bits = [&](unsigned j, expr_ref_vector& bits) {
+            bits.reset();
+            for (unsigned i = 0; i < sz; ++i)
+                bits.push_back(bv.mk_bit2bool(e->get_arg(0), j));            
+        };
+        if (!m_lazymul.find(e, lz)) {
+            set_bits(0, args);
+            for (unsigned j = 1; j < e->get_num_args(); ++j) {
+                new_out.reset();
+                set_bits(j, new_args);
+                m_bb.mk_multiplier(sz, args.data(), new_args.data(), new_out);
+                new_out.swap(args);
+            }
+            lz = alloc(lazy_mul, e, args);
+            m_lazymul.insert(e, lz);
+            ctx.push(new_obj_trail(lz));
+            ctx.push(insert_obj_map(m_lazymul, e));
+        }
+        if (lz->m_out.size() == lz->m_bits)
+            return false;
+        for (unsigned i = lz->m_bits; i <= diff; ++i) {
+            sat::literal bit1 = mk_literal(lz->m_out.get(i));
+            sat::literal bit2 = mk_literal(bv.mk_bit2bool(e, i));
+            add_equiv(bit1, bit2);
+        }
+        ctx.push(value_trail(lz->m_bits));
+        IF_VERBOSE(1, verbose_stream() << "expand lazy mul " << mk_pp(e, m) << " to " << diff << "\n");
+        lz->m_bits = diff;
+        return false;
+    }
+
     bool solver::check_mul(app* e) {
         SASSERT(e->get_num_args() >= 2);
         expr_ref_vector args(m);
@@ -96,6 +145,12 @@ namespace bv {
         if (!check_mul_invertibility(e, args, r1))
             return false;
 
+#if 0
+        // unsound?
+
+        if (!check_lazy_mul(e, r1, r2))
+            return false;
+#endif
         // Some other possible approaches:
         // algebraic rules:
         // x*(y+z), and there are nodes for x*y or x*z -> x*(y+z) = x*y + x*z
@@ -177,18 +232,17 @@ namespace bv {
     bool solver::check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* mul_value, expr* arg_value) {
         SASSERT(mul_value != arg_value);
         SASSERT(!(bv.is_zero(mul_value) && bv.is_zero(arg_value)));
-        if (bv.is_zero(arg_value)) {
+        if (bv.is_zero(arg_value) && false) {
             unsigned sz = n->get_num_args();
             expr_ref_vector args(m, sz, n->get_args());
             for (unsigned i = 0; i < sz && !s().inconsistent(); ++i) {
-
                 args[i] = arg_value;
                 expr_ref r(m.mk_app(n->get_decl(), args), m);
                 set_delay_internalize(r, internalize_mode::init_bits_only_i); // do not bit-blast this multiplier.
                 args[i] = n->get_arg(i);                
                 add_unit(eq_internalize(r, arg_value));
             }
-            IF_VERBOSE(2, verbose_stream() << "delay internalize @" << s().scope_lvl() << "\n");
+            IF_VERBOSE(2, verbose_stream() << "delay internalize @" << s().scope_lvl() << " " << mk_pp(n, m) << "\n");
             return false;
         }
         if (bv.is_zero(mul_value)) {

src/sat/smt/bv_internalize.cpp

@@ -139,7 +139,9 @@ namespace bv {
             return true;
 
         SASSERT(!n || !n->is_attached_to(get_id()));
-        bool suppress_args = !reflect() && !m.is_considered_uninterpreted(a->get_decl());
+        bool suppress_args = !reflect() 
+            && !m.is_considered_uninterpreted(a->get_decl())
+            && !bv.is_int2bv(e) && !bv.is_bv2int(e);
         if (!n)
             n = mk_enode(e, suppress_args);
 
@@ -314,7 +316,6 @@ namespace bv {
         euf::enode* n = bool_var2enode(l.var());
         if (!n->is_attached_to(get_id())) 
             mk_var(n);
-
         set_bit_eh(v, l, idx);
     }
 
@@ -435,7 +436,9 @@ namespace bv {
             args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero));        
         expr_ref sum(m_autil.mk_add(sz, args.data()), m);
         sat::literal lit = eq_internalize(n, sum);
-	add_unit(lit);
+        m_bv2ints.push_back(expr2enode(n));
+        ctx.push(push_back_vector<euf::enode_vector>(m_bv2ints));
+	    add_unit(lit);
     }
 
     void solver::internalize_int2bv(app* n) {
@@ -454,6 +457,12 @@ namespace bv {
      * Create the axioms:
      *   bit2bool(i,n) == ((e div 2^i) mod 2 != 0)
      * for i = 0,.., sz-1
+     *
+     * Alternative axiomatization:
+     * e = sum bit2bool(i,n)*2^i + 2^n * (div(e, 2^n))
+     * possibly term div(e,2^n) is not correct with respect to adapted semantics?
+     * if not, use fresh variable or similar. Overall should be much beter.
+     * Note: based on superb question raised at workshop on 9/1/22.
      */
     void solver::assert_int2bv_axiom(app* n) {
         expr* e = nullptr;
@@ -464,8 +473,8 @@ namespace bv {
         unsigned sz = bv.get_bv_size(n);
         numeral mod = power(numeral(2), sz);
         rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
-	sat::literal eq_lit = eq_internalize(lhs, rhs);
-	add_unit(eq_lit);
+        sat::literal eq_lit = eq_internalize(lhs, rhs);
+        add_unit(eq_lit);
        
         expr_ref_vector n_bits(m);
         get_bits(n_enode, n_bits);
@@ -476,8 +485,8 @@ namespace bv {
             rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2));
             rhs = mk_eq(rhs, m_autil.mk_int(1));
             lhs = n_bits.get(i);
-	    eq_lit = eq_internalize(lhs, rhs);
-	    add_unit(eq_lit);
+            eq_lit = eq_internalize(lhs, rhs);
+	        add_unit(eq_lit);
         }
     }
 
@@ -534,27 +543,27 @@ namespace bv {
         internalize_binary(a, bin);
     }
 
-    void solver::internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& iun) {
+    void solver::internalize_interp(app* n, std::function<expr* (expr*, expr*)>& ibin, std::function<expr* (expr*)>& iun) {
         bv_rewriter_params p(s().params());
         expr* arg1 = n->get_arg(0);
         expr* arg2 = n->get_arg(1);
         mk_bits(get_th_var(n));
-	sat::literal eq_lit;
+        sat::literal eq_lit;
         if (p.hi_div0()) {
             eq_lit = eq_internalize(n, ibin(arg1, arg2));
-	    add_unit(eq_lit);
-	}
-	else {
-	    unsigned sz = bv.get_bv_size(n);
-	    expr_ref zero(bv.mk_numeral(0, sz), m);
-	    sat::literal eqZ = eq_internalize(arg2, zero);
-	    sat::literal eqU = eq_internalize(n, iun(arg1));
-	    sat::literal eqI = eq_internalize(n, ibin(arg1, arg2));
-	    add_clause(~eqZ, eqU);
-	    add_clause(eqZ, eqI);
-	    ctx.add_aux(~eqZ, eqU);
-	    ctx.add_aux(eqZ, eqI);
-	}
+            add_unit(eq_lit);
+        }
+        else {
+            unsigned sz = bv.get_bv_size(n);
+            expr_ref zero(bv.mk_numeral(0, sz), m);
+            sat::literal eqZ = eq_internalize(arg2, zero);
+            sat::literal eqU = mk_literal(iun(arg1));
+            sat::literal eqI = mk_literal(ibin(arg1, arg2));
+            add_clause(~eqZ, eqU);
+            add_clause(eqZ, eqI);
+            ctx.add_aux(~eqZ, eqU);
+            ctx.add_aux(eqZ, eqI);
+        }
     }
 
     void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) {
@@ -574,11 +583,9 @@ namespace bv {
         init_bits(n, bits);
     }
 
-
     void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
         SASSERT(e->get_num_args() >= 1);
-        expr_ref_vector bits(m), new_bits(m), arg_bits(m);
-        
+        expr_ref_vector bits(m), new_bits(m), arg_bits(m);        
         get_arg_bits(e, 0, bits);
         for (unsigned i = 1; i < e->get_num_args(); ++i) {
             arg_bits.reset();
@@ -658,7 +665,7 @@ namespace bv {
             conc.push_back(arg);
         expr_ref r(bv.mk_concat(conc), m);
         mk_bits(get_th_var(e));
-	sat::literal eq_lit = eq_internalize(e, r);
+        sat::literal eq_lit = eq_internalize(e, r);
         add_unit(eq_lit);
     }
 
@@ -667,9 +674,8 @@ namespace bv {
         expr* arg = nullptr;
         VERIFY(bv.is_bit2bool(n, arg, idx));
         euf::enode* argn = expr2enode(arg);
-        if (!argn->is_attached_to(get_id())) {
-            mk_var(argn);
-        }        
+        if (!argn->is_attached_to(get_id())) 
+            mk_var(argn);   
         theory_var v_arg = argn->get_th_var(get_id());        
         SASSERT(idx < get_bv_size(v_arg));
         sat::literal lit = expr2literal(n);
@@ -771,7 +777,7 @@ namespace bv {
             e1 = bv.mk_bit2bool(o1, i);
             e2 = bv.mk_bit2bool(o2, i);
             literal eq = eq_internalize(e1, e2);
-	    add_clause(eq, ~oeq);
+            add_clause(eq, ~oeq);
             eqs.push_back(~eq);
         }
         TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);

src/sat/smt/bv_solver.cpp

@@ -212,19 +212,32 @@ namespace bv {
             return;
         }
         euf::enode* n1 = var2enode(eq.v1());
-        for (euf::enode* bv2int : euf::enode_class(n1)) {
-            if (!bv.is_bv2int(bv2int->get_expr()))
-                continue;
+
+        auto propagate_bv2int = [&](euf::enode* bv2int) {
             euf::enode* bv2int_arg = bv2int->get_arg(0);
             for (euf::enode* p : euf::enode_parents(n1->get_root())) {
                 if (bv.is_int2bv(p->get_expr()) && p->get_sort() == bv2int_arg->get_sort() && p->get_root() != bv2int_arg->get_root()) {
-                    euf::enode_pair_vector eqs;
-                    eqs.push_back({ n1, p->get_arg(0) });
-                    eqs.push_back({ n1, bv2int });
-                    ctx.propagate(p, bv2int_arg, euf::th_explain::propagate(*this, eqs, p, bv2int_arg));
+                    theory_var v1 = get_th_var(p);
+                    theory_var v2 = get_th_var(bv2int_arg);
+                    SASSERT(v1 != euf::null_theory_var);
+                    SASSERT(v2 != euf::null_theory_var);
+                    ctx.propagate(p, bv2int_arg, mk_bv2int_justification(v1, v2, n1, p->get_arg(0), bv2int));
                     break;
                 }
             }
+        };
+
+        if (m_bv2ints.size() < n1->class_size()) {
+            for (auto* bv2int : m_bv2ints) {
+                if (bv2int->get_root() == n1->get_root())
+                    propagate_bv2int(bv2int);
+            }
+        }
+        else {
+            for (euf::enode* bv2int : euf::enode_class(n1)) {                
+                if (bv.is_bv2int(bv2int->get_expr()))
+                    propagate_bv2int(bv2int);
+            }
         }
     }
 
@@ -282,6 +295,8 @@ namespace bv {
             ++m_stats.m_num_ne2bit;
             s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent));
         }
+        else if (!get_config().m_bv_eq_axioms) 
+            ;
         else if (s().at_search_lvl()) {
             force_push();
             assert_ackerman(v1, v2);
@@ -368,6 +383,11 @@ namespace bv {
             r.push_back(b);
             break;
         }
+        case bv_justification::kind_t::bv2int: {
+            ctx.add_antecedent(c.a, c.b);
+            ctx.add_antecedent(c.a, c.c);
+            break;
+        }
         }
         if (!probing && ctx.use_drat())
             log_drat(c);
@@ -375,19 +395,26 @@ namespace bv {
 
     void solver::log_drat(bv_justification const& c) {
         // introduce dummy literal for equality.
-        sat::literal leq(s().num_vars() + 1, false);
-        expr_ref eq(m);
-        if (c.m_kind != bv_justification::kind_t::bit2ne) {
+        sat::literal leq1(s().num_vars() + 1, false);
+        sat::literal leq2(s().num_vars() + 2, false);
+        expr_ref eq1(m), eq2(m);
+        if (c.m_kind == bv_justification::kind_t::bv2int) {
+            eq1 = m.mk_eq(c.a->get_expr(), c.b->get_expr());
+            eq2 = m.mk_eq(c.a->get_expr(), c.c->get_expr());
+            ctx.set_tmp_bool_var(leq1.var(), eq1);
+            ctx.set_tmp_bool_var(leq2.var(), eq1);
+        }
+        else if (c.m_kind != bv_justification::kind_t::bit2ne) {
             expr* e1 = var2expr(c.m_v1);
             expr* e2 = var2expr(c.m_v2);
-            eq = m.mk_eq(e1, e2);       
-            ctx.drat_eq_def(leq, eq);
+            eq1 = m.mk_eq(e1, e2);      
+            ctx.set_tmp_bool_var(leq1.var(), eq1);
         }
 
         sat::literal_vector lits;
         switch (c.m_kind) {
         case bv_justification::kind_t::eq2bit:
-            lits.push_back(~leq);
+            lits.push_back(~leq1);
             lits.push_back(~c.m_antecedent);
             lits.push_back(c.m_consequent);
             break;
@@ -396,10 +423,10 @@ namespace bv {
             lits.push_back(c.m_consequent);
             break;
         case bv_justification::kind_t::bit2eq:      
-            get_antecedents(leq, c.to_index(), lits, true);
+            get_antecedents(leq1, c.to_index(), lits, true);
             for (auto& lit : lits)
                 lit.neg();
-            lits.push_back(leq);
+            lits.push_back(leq1);
             break;
         case bv_justification::kind_t::bit2ne: 
             get_antecedents(c.m_consequent, c.to_index(), lits, true);
@@ -407,9 +434,20 @@ namespace bv {
                 lit.neg();
             lits.push_back(c.m_consequent);            
             break;
+        case bv_justification::kind_t::bv2int:
+            get_antecedents(leq1, c.to_index(), lits, true);
+            get_antecedents(leq2, c.to_index(), lits, true);
+            for (auto& lit : lits)
+                lit.neg();
+            lits.push_back(leq1);
+            lits.push_back(leq2);
+            break;
         }
         ctx.get_drat().add(lits, status());
         // TBD, a proper way would be to delete the lemma after use.
+        ctx.set_tmp_bool_var(leq1.var(), nullptr);
+        ctx.set_tmp_bool_var(leq2.var(), nullptr);
+
     }
 
     void solver::asserted(literal l) {
@@ -665,7 +703,9 @@ namespace bv {
             return out << "bv <- v" << v1 << "[" << cidx << "] != v" << v2 << "[" << cidx << "] " << m_bits[v1][cidx] << " != " << m_bits[v2][cidx];
         }
         case bv_justification::kind_t::ne2bit: 
-            return out << "bv <- " << m_bits[v1] << " != " << m_bits[v2] << " @" << cidx;                                                 
+            return out << "bv <- " << m_bits[v1] << " != " << m_bits[v2] << " @" << cidx;
+        case bv_justification::kind_t::bv2int:
+            return out << "bv <- v" << v1 << " == v" << v2 << " <== " << ctx.bpp(c.a) << " == " << ctx.bpp(c.b) << " == " << ctx.bpp(c.c);
         default:
             UNREACHABLE();
             break;
@@ -826,28 +866,41 @@ namespace bv {
         void* mem = get_region().allocate(bv_justification::get_obj_size());
         sat::constraint_base::initialize(mem, this);
         auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2, c, a);
-        return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+        auto jst = sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+        TRACE("bv", tout << jst << " " << constraint << "\n");
+        return jst;
     }
 
     sat::ext_justification_idx solver::mk_bit2eq_justification(theory_var v1, theory_var v2) {
         void* mem = get_region().allocate(bv_justification::get_obj_size());
         sat::constraint_base::initialize(mem, this);
         auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2);
-        return constraint->to_index();
+        auto jst = constraint->to_index();
+        return jst;
     }
 
     sat::justification solver::mk_bit2ne_justification(unsigned idx, sat::literal c) {
         void* mem = get_region().allocate(bv_justification::get_obj_size());
         sat::constraint_base::initialize(mem, this);
         auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(idx, c);
-        return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+        auto jst = sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+        return jst;
     }
 
     sat::justification solver::mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a) {
         void* mem = get_region().allocate(bv_justification::get_obj_size());
         sat::constraint_base::initialize(mem, this);
         auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(idx, v1, v2, c, a);
-        return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+        auto jst = sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+        return jst;
+    }
+
+    sat::ext_constraint_idx solver::mk_bv2int_justification(theory_var v1, theory_var v2, euf::enode* a, euf::enode* b, euf::enode* c) {
+        void* mem = get_region().allocate(bv_justification::get_obj_size());
+        sat::constraint_base::initialize(mem, this);
+        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2, a, b, c);
+        auto jst = constraint->to_index();
+        return jst;
     }
 
     bool solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {

src/sat/smt/bv_solver.h

@@ -27,6 +27,15 @@ namespace euf {
 
 namespace bv {
 
+    struct lazy_mul {
+        expr_ref_vector m_out;
+        unsigned        m_bits;
+        lazy_mul(app* a, expr_ref_vector& out):
+            m_out(out), 
+            m_bits(0) {
+        }
+    };
+
     class solver : public euf::th_euf_solver {
         typedef rational numeral;
         typedef euf::theory_var theory_var;
@@ -52,13 +61,15 @@ namespace bv {
         };
 
         struct bv_justification {
-            enum kind_t { eq2bit, ne2bit, bit2eq, bit2ne };
+            enum kind_t { eq2bit, ne2bit, bit2eq, bit2ne, bv2int };
             kind_t     m_kind;
-            unsigned   m_idx{ UINT_MAX };
-            theory_var m_v1{ euf::null_theory_var };
-            theory_var m_v2 { euf::null_theory_var };
+            unsigned   m_idx = UINT_MAX;
+            theory_var m_v1 = euf::null_theory_var;
+            theory_var m_v2 = euf::null_theory_var;
             sat::literal m_consequent;
             sat::literal m_antecedent;
+            euf::enode* a, *b, *c;
+                    
             bv_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
                 m_kind(bv_justification::kind_t::eq2bit), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
             bv_justification(theory_var v1, theory_var v2):
@@ -67,6 +78,8 @@ namespace bv {
                 m_kind(bv_justification::kind_t::bit2ne), m_idx(idx), m_consequent(c) {}
             bv_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
                 m_kind(bv_justification::kind_t::ne2bit), m_idx(idx), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
+            bv_justification(theory_var v1, theory_var v2, euf::enode* a, euf::enode* b, euf::enode* c):
+                m_kind(bv_justification::kind_t::bv2int), m_v1(v1), m_v2(v2), a(a), b(b), c(c) {}
             sat::ext_constraint_idx to_index() const { 
                 return sat::constraint_base::mem2base(this); 
             }
@@ -80,6 +93,7 @@ namespace bv {
         sat::ext_justification_idx mk_bit2eq_justification(theory_var v1, theory_var v2);
         sat::justification mk_bit2ne_justification(unsigned idx, sat::literal c);
         sat::justification mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a);
+        sat::ext_constraint_idx mk_bv2int_justification(theory_var v1, theory_var v2, euf::enode* a, euf::enode* b, euf::enode* c);
         void log_drat(bv_justification const& c);
  
 
@@ -210,8 +224,10 @@ namespace bv {
         literal_vector             m_tmp_literals;
         svector<propagation_item>  m_prop_queue;
         unsigned_vector            m_prop_queue_lim;
-        unsigned                   m_prop_queue_head { 0 };
-        sat::literal               m_true { sat::null_literal };
+        unsigned                   m_prop_queue_head = 0;
+        sat::literal               m_true = sat::null_literal;
+        euf::enode_vector          m_bv2ints;
+        obj_map<app, lazy_mul*>   m_lazymul;
 
         // internalize
         void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); }
@@ -312,6 +328,7 @@ namespace bv {
         bool m_cheap_axioms{ true };
         bool should_bit_blast(app * n);
         bool check_delay_internalized(expr* e);
+        bool check_lazy_mul(app* e, expr* mul_value, expr* arg_value);
         bool check_mul(app* e);
         bool check_mul_invertibility(app* n, expr_ref_vector const& arg_values, expr* value);
         bool check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);

src/sat/smt/euf_internalize.cpp

@@ -167,7 +167,7 @@ namespace euf {
             lit = lit2;
         }
 
-        TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";);
+        TRACE("euf", tout << "attach v" << 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) {
@@ -264,7 +264,11 @@ namespace euf {
         sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
         if (sz <= 1) 
             return;
-        if (sz <= distinct_max_args) {
+        sort* srt = e->get_arg(0)->get_sort();
+        auto sort_sz = srt->get_num_elements();
+        if (sort_sz.is_finite() && sort_sz.size() < sz)
+            s().add_clause(0, nullptr, st);
+        else if (sz <= distinct_max_args) {
             for (unsigned i = 0; i < sz; ++i) {
                 for (unsigned j = i + 1; j < sz; ++j) {
                     expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
@@ -274,8 +278,7 @@ namespace euf {
             }
         }
         else {
-            // dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n
-            sort* srt = e->get_arg(0)->get_sort();
+            // dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n            
             SASSERT(!m.is_bool(srt));
             sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
             func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m);

src/sat/smt/euf_proof.cpp

@@ -16,96 +16,26 @@ Author:
 --*/
 
 #include "sat/smt/euf_solver.h"
+#include "ast/ast_util.h"
+#include <iostream>
 
 namespace euf {
 
-    void solver::init_drat() {
-        if (!m_drat_initialized) {
+    void solver::init_proof() {
+        if (!m_proof_initialized) {
             get_drat().add_theory(get_id(), symbol("euf"));
             get_drat().add_theory(m.get_basic_family_id(), symbol("bool"));
         }
-        m_drat_initialized = true;
-    }
-
-    void solver::drat_log_expr1(expr* e) {
-        if (is_app(e)) {
-            app* a = to_app(e);
-            drat_log_decl(a->get_decl());
-            std::stringstream strm;
-            strm << mk_ismt2_func(a->get_decl(), m);
-            get_drat().def_begin('e', e->get_id(), strm.str());
-            for (expr* arg : *a)
-                get_drat().def_add_arg(arg->get_id());
-            get_drat().def_end();
+        if (!m_proof_out && s().get_config().m_drat && 
+            (get_config().m_lemmas2console || s().get_config().m_smt_proof.is_non_empty_string())) {
+            TRACE("euf", tout << "init-proof\n");
+            m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out);
+            if (get_config().m_lemmas2console) 
+                get_drat().set_clause_eh(*this);
+            if (s().get_config().m_smt_proof.is_non_empty_string()) 
+                get_drat().set_clause_eh(*this);
         }
-        else if (is_var(e)) {
-            var* v = to_var(e);
-            get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
-            get_drat().def_add_arg(v->get_idx());
-            get_drat().def_end();
-        }
-        else if (is_quantifier(e)) {
-            quantifier* q = to_quantifier(e);
-            std::stringstream strm;           
-            strm << "(" << (is_forall(q) ? "forall" : (is_exists(q) ? "exists" : "lambda"));
-            for (unsigned i = 0; i < q->get_num_decls(); ++i) 
-                strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";            
-            strm << ")";
-            get_drat().def_begin('q', q->get_id(), strm.str());
-            get_drat().def_add_arg(q->get_expr()->get_id());
-            get_drat().def_end();
-        }
-        else 
-            UNREACHABLE();
-        m_drat_asts.insert(e);
-        push(insert_obj_trail<ast>(m_drat_asts, e));
-    }
-
-    void solver::drat_log_expr(expr* e) {
-        if (m_drat_asts.contains(e))
-            return;
-        ptr_vector<expr>::scoped_stack _sc(m_drat_todo);
-        m_drat_todo.push_back(e);
-        while (!m_drat_todo.empty()) {
-            e = m_drat_todo.back();
-            unsigned sz = m_drat_todo.size();
-            if (is_app(e)) 
-                for (expr* arg : *to_app(e))
-                    if (!m_drat_asts.contains(arg))
-                        m_drat_todo.push_back(arg);
-            if (is_quantifier(e)) {
-                expr* arg = to_quantifier(e)->get_expr();
-                if (!m_drat_asts.contains(arg))
-                    m_drat_todo.push_back(arg);                
-            }                
-            if (m_drat_todo.size() != sz)
-                continue;
-            if (!m_drat_asts.contains(e))
-                drat_log_expr1(e);
-            m_drat_todo.pop_back();                   
-        }
-    }
-
-    void solver::drat_bool_def(sat::bool_var v, expr* e) {
-        if (!use_drat())
-            return;
-        drat_log_expr(e);
-        get_drat().bool_def(v, e->get_id());
-    }
-
-
-    void solver::drat_log_decl(func_decl* f) {
-        if (f->get_family_id() != null_family_id) 
-            return;
-        if (m_drat_asts.contains(f))
-            return;
-        m_drat_asts.insert(f);
-        push(insert_obj_trail< ast>(m_drat_asts, f));
-        std::ostringstream strm;
-        smt2_pp_environment_dbg env(m);
-        ast_smt2_pp(strm, f, env);
-        get_drat().def_begin('f', f->get_small_id(), strm.str());
-        get_drat().def_end();
+        m_proof_initialized = true;
     }
 
     /**
@@ -144,16 +74,20 @@ namespace euf {
         }
     }
 
+    void solver::set_tmp_bool_var(bool_var b, expr* e) {
+        m_bool_var2expr.setx(b, e, nullptr);
+    }
+
     void solver::log_justification(literal l, th_explain const& jst) {
         literal_vector lits;
-        unsigned nv = s().num_vars();
         expr_ref_vector eqs(m);
+        unsigned nv = s().num_vars();
         auto add_lit = [&](enode_pair const& eq) {
+            unsigned v = nv;
             ++nv;
-            literal lit(nv, false);
             eqs.push_back(m.mk_eq(eq.first->get_expr(), eq.second->get_expr()));
-            drat_eq_def(lit, eqs.back());            
-            return lit;
+            set_tmp_bool_var(v, eqs.back());
+            return literal(v, false);
         };
 
         for (auto lit : euf::th_explain::lits(jst))
@@ -167,18 +101,137 @@ namespace euf {
         if (jst.eq_consequent().first != nullptr) 
             lits.push_back(add_lit(jst.eq_consequent()));
         get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id(), jst.get_pragma()));
+        for (unsigned i = s().num_vars(); i < nv; ++i)
+            set_tmp_bool_var(i, nullptr);
     }
 
-    void solver::drat_eq_def(literal lit, expr* eq) {
-        expr *a = nullptr, *b = nullptr;
-        VERIFY(m.is_eq(eq, a, b));
-        drat_log_expr(a);
-        drat_log_expr(b);
-        get_drat().def_begin('e', eq->get_id(), std::string("="));
-        get_drat().def_add_arg(a->get_id());
-        get_drat().def_add_arg(b->get_id());
-        get_drat().def_end();
-        get_drat().bool_def(lit.var(), eq->get_id());
+    void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
+        TRACE("euf", tout << "on-clause " << n << "\n");
+        on_lemma(n, lits, st);
+        on_proof(n, lits, st);
+    }
+
+    void solver::on_proof(unsigned n, literal const* lits, sat::status st) {
+        if (!m_proof_out)
+            return;
+        flet<bool> _display_all_decls(m_display_all_decls, true);
+        std::ostream& out = *m_proof_out;
+        if (!visit_clause(out, n, lits))
+            return;
+        if (st.is_asserted()) 
+            display_redundant(out, n, lits, status2proof_hint(st));
+        else if (st.is_deleted()) 
+            display_deleted(out, n, lits);        
+        else if (st.is_redundant()) 
+            display_redundant(out, n, lits, status2proof_hint(st));
+        else if (st.is_input()) 
+            display_assume(out, n, lits);
+        else 
+            UNREACHABLE();
+        out.flush();
+    }
+        
+    void solver::on_lemma(unsigned n, literal const* lits, sat::status st) {
+        if (!get_config().m_lemmas2console) 
+            return;
+        if (!st.is_redundant() && !st.is_asserted()) 
+            return;
+        
+        std::ostream& out = std::cout;
+        if (!visit_clause(out, n, lits))
+            return;
+        std::function<symbol(int)> ppth = [&](int th) {
+            return m.get_family_name(th);
+        };
+        if (!st.is_sat())
+            out << "; " << sat::status_pp(st, ppth) << "\n";
+
+        display_assert(out, n, lits);
+    }
+
+    void solver::on_instantiation(unsigned n, sat::literal const* lits, unsigned k, euf::enode* const* bindings) {
+        std::ostream& out = std::cout;
+        for (unsigned i = 0; i < k; ++i)
+            visit_expr(out, bindings[i]->get_expr());        
+        VERIFY(visit_clause(out, n, lits));
+        out << "(instantiate";
+        display_literals(out, n, lits);
+        for (unsigned i = 0; i < k; ++i) 
+            display_expr(out << " :binding ", bindings[i]->get_expr());
+        out << ")\n";
+    }
+
+    bool solver::visit_clause(std::ostream& out, unsigned n, literal const* lits) {
+        for (unsigned i = 0; i < n; ++i) {
+            expr* e = bool_var2expr(lits[i].var());
+            if (!e)
+                return false;
+            visit_expr(out, e);
+        }
+        return true;
+    }
+
+    void solver::display_assert(std::ostream& out, unsigned n, literal const* lits) {
+        display_literals(out << "(assert (or", n, lits) << "))\n";
+    }
+    
+    void solver::display_assume(std::ostream& out, unsigned n, literal const* lits) {
+        display_literals(out << "(assume", n, lits) << ")\n";        
+    }
+
+    void solver::display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) {
+        if (proof_hint)
+            visit_expr(out, proof_hint);
+        display_hint(display_literals(out << "(learn", n, lits), proof_hint) << ")\n";        
+    }
+
+    void solver::display_deleted(std::ostream& out, unsigned n, literal const* lits) {
+        display_literals(out << "(del", n, lits) << ")\n";        
+    }
+
+    std::ostream& solver::display_hint(std::ostream& out, expr* proof_hint) {
+        if (proof_hint)
+            return display_expr(out << " ", proof_hint);
+        else
+            return out;
+    }
+
+    expr_ref solver::status2proof_hint(sat::status st) {
+        if (st.is_sat()) 
+            return expr_ref(m.mk_const("rup", m.mk_proof_sort()), m); // provable by reverse unit propagation
+        auto* h = reinterpret_cast<euf::th_proof_hint const*>(st.get_hint());
+        if (!h)
+            return expr_ref(m);
+
+        expr* e = h->get_hint(*this);
+        if (e)
+            return expr_ref(e, m);
+
+        return expr_ref(m);        
+    }
+
+    std::ostream& solver::display_literals(std::ostream& out, unsigned n, literal const* lits) {
+        for (unsigned i = 0; i < n; ++i) {
+            expr* e = bool_var2expr(lits[i].var());
+            if (lits[i].sign())
+                display_expr(out << " (not ", e) << ")";
+            else
+                display_expr(out << " ", e);
+        }
+        return out;
+    }
+
+    void solver::visit_expr(std::ostream& out, expr* e) {
+        m_clause_visitor.collect(e);
+        if (m_display_all_decls)
+            m_clause_visitor.display_decls(out);
+        else
+            m_clause_visitor.display_skolem_decls(out);
+        m_clause_visitor.define_expr(out, e);
+    }
+
+    std::ostream& solver::display_expr(std::ostream& out, expr* e) {
+        return m_clause_visitor.display_expr_def(out, e);
     }
 
 }

src/sat/smt/euf_proof_checker.cpp

@@ -0,0 +1,50 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    euf_proof_checker.cpp
+
+Abstract:
+
+    Plugin manager for checking EUF proofs
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "sat/smt/euf_proof_checker.h"
+#include "sat/smt/arith_proof_checker.h"
+
+namespace euf {
+
+    proof_checker::proof_checker(ast_manager& m):
+        m(m) {
+        arith::proof_checker* apc = alloc(arith::proof_checker, m);
+        m_plugins.push_back(apc);
+        apc->register_plugins(*this);
+        (void)m;
+    }
+
+    proof_checker::~proof_checker() {}
+
+    void proof_checker::register_plugin(symbol const& rule, proof_checker_plugin* p) {
+        m_map.insert(rule, p);
+    }
+
+    bool proof_checker::check(expr_ref_vector const& clause, expr* e, expr_ref_vector& units) {
+        if (!e || !is_app(e))
+            return false;
+        units.reset();
+        app* a = to_app(e);
+        proof_checker_plugin* p = nullptr;
+        if (m_map.find(a->get_decl()->get_name(), p)) 
+            return p->check(clause, a, units);
+        return false;
+    }
+
+}
+

src/sat/smt/euf_proof_checker.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    euf_proof_checker.h
+
+Abstract:
+
+    Plugin manager for checking EUF proofs
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-08-25
+
+--*/
+#pragma once
+
+#include "util/map.h"
+#include "util/scoped_ptr_vector.h"
+#include "ast/ast.h"
+
+namespace euf {
+
+    class proof_checker;
+
+    class proof_checker_plugin {
+    public:
+        virtual ~proof_checker_plugin() {}
+        virtual bool check(expr_ref_vector const& clause, app* jst, expr_ref_vector& units) = 0;        
+        virtual void register_plugins(proof_checker& pc) = 0;
+    };
+
+    class proof_checker {
+        ast_manager& m;
+        scoped_ptr_vector<proof_checker_plugin> m_plugins;
+        map<symbol, proof_checker_plugin*, symbol_hash_proc, symbol_eq_proc> m_map;
+    public:
+        proof_checker(ast_manager& m);
+        ~proof_checker();
+        void register_plugin(symbol const& rule, proof_checker_plugin*);
+        bool check(expr_ref_vector const& clause, expr* e, expr_ref_vector& units);
+    };
+
+}
+

src/sat/smt/euf_solver.cpp

@@ -49,7 +49,8 @@ namespace euf {
         m_lookahead(nullptr),
         m_to_m(&m),
         m_to_si(&si),
-        m_values(m)
+        m_values(m),
+        m_clause_visitor(m)
     {
         updt_params(p);
         m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2);
@@ -347,8 +348,7 @@ namespace euf {
             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()));
+                set_conflict(conflict_constraint().to_index());
                 return true;
             }
             bool propagated1 = false;
@@ -488,7 +488,8 @@ namespace euf {
         };
         if (merge_shared_bools())
             cont = true;
-        for (auto* e : m_solvers) {
+        for (unsigned i = 0; i < m_solvers.size(); ++i) {
+            auto* e = m_solvers[i];
             if (!m.inc())
                 return sat::check_result::CR_GIVEUP;
             if (e == m_qsolver)
@@ -519,7 +520,7 @@ namespace euf {
         bool merged = false;
         for (unsigned i = m_egraph.nodes().size(); i-- > 0; ) {
             euf::enode* n = m_egraph.nodes()[i];
-            if (!is_shared(n) || !m.is_bool(n->get_expr()))
+            if (!m.is_bool(n->get_expr()) || !is_shared(n))
                 continue;
             if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) {
                 m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
@@ -616,15 +617,17 @@ namespace euf {
             else 
                 lit = si.internalize(e, false);
             VERIFY(lit.var() == v);     
-            if (!m_egraph.find(e) && (!m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e))) {
+            if (!m_egraph.find(e) && !m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e) && !m.is_implies(e) && !m.is_xor(e)) {
                 ptr_buffer<euf::enode> args;
                 if (is_app(e))
                     for (expr* arg : *to_app(e))
                         args.push_back(e_internalize(arg));
+                internalize(e, true);
                 if (!m_egraph.find(e))
                     mk_enode(e, args.size(), args.data());
             }
-            attach_lit(lit, e);            
+            else 
+                attach_lit(lit, e);            
         }
         
         if (relevancy_enabled())
@@ -778,7 +781,7 @@ namespace euf {
         }
         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))
+            if (th && th->is_fixed(thv.get_var(), val, explain))
                 return true;
         }
         return false;
@@ -863,7 +866,13 @@ namespace euf {
         out << "bool-vars\n";
         for (unsigned v : m_var_trail) {
             expr* e = m_bool_var2expr[v];
-            out << v << (is_relevant(v)?"":"n") << ": " << 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);
+            euf::enode* n = m_egraph.find(e);
+            if (n) {
+                for (auto const& th : enode_th_vars(n))
+                    out << " " << m_id2solver[th.get_id()]->name();
+            }
+            out << "\n";        
         }
         for (auto* e : m_solvers)
             e->display(out);
@@ -1067,10 +1076,7 @@ namespace euf {
         user_propagator::fresh_eh_t& fresh_eh) {
         m_user_propagator = alloc(user_solver::solver, *this);
         m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
-        for (unsigned i = m_scopes.size(); i-- > 0; )
-            m_user_propagator->push();
-        m_solvers.push_back(m_user_propagator);
-        m_id2solver.setx(m_user_propagator->get_id(), m_user_propagator, nullptr);
+        add_solver(m_user_propagator);
     }
 
     bool solver::watches_fixed(enode* n) const {

src/sat/smt/euf_solver.h

@@ -60,11 +60,10 @@ namespace euf {
         std::ostream& display(std::ostream& out) const;
     };
 
-    class solver : public sat::extension, public th_internalizer, public th_decompile {
+    class solver : public sat::extension, public th_internalizer, public th_decompile, public sat::clause_eh {
         typedef top_sort<euf::enode> deps_t;
         friend class ackerman;
         class user_sort;
-        // friend class sat::ba_solver;
         struct stats {
             unsigned m_ackerman;
             unsigned m_final_checks;
@@ -161,7 +160,6 @@ namespace euf {
         void collect_dependencies(user_sort& us, deps_t& deps);
         void values2model(deps_t const& deps, model_ref& mdl);
         void validate_model(model& mdl);
-        void display_validation_failure(std::ostream& out, model& mdl, enode* n);
 
         // solving
         void propagate_literals();
@@ -175,19 +173,22 @@ namespace euf {
         void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
         void log_antecedents(literal l, literal_vector const& r);
         void log_justification(literal l, th_explain const& jst);
-        void drat_log_decl(func_decl* f);
-        void drat_log_expr1(expr* n);
-        ptr_vector<expr> m_drat_todo;
-        obj_hashtable<ast> m_drat_asts;
-        bool m_drat_initialized{ false };
-        void init_drat();
+
+        bool m_proof_initialized = false;
+        void init_proof();
+        ast_pp_util m_clause_visitor;
+        bool m_display_all_decls = false;
+        void on_clause(unsigned n, literal const* lits, sat::status st) override;
+        void on_lemma(unsigned n, literal const* lits, sat::status st);
+        void on_proof(unsigned n, literal const* lits, sat::status st);
+        std::ostream& display_literals(std::ostream& out, unsigned n, sat::literal const* lits);
+        void display_assume(std::ostream& out, unsigned n, literal const* lits);
+        void display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint);        
+        void display_deleted(std::ostream& out, unsigned n, literal const* lits);
+        std::ostream& display_hint(std::ostream& out, expr* proof_hint);
+        expr_ref status2proof_hint(sat::status st);
 
         // 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;
@@ -340,11 +341,16 @@ namespace euf {
 
 
         // proof
-        bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
+        bool use_drat() { return s().get_config().m_drat && (init_proof(), true); }
         sat::drat& get_drat() { return s().get_drat(); }
-        void drat_bool_def(sat::bool_var v, expr* n);
-        void drat_eq_def(sat::literal lit, expr* eq);
-        void drat_log_expr(expr* n);
+
+        void set_tmp_bool_var(sat::bool_var b, expr* e);
+        bool visit_clause(std::ostream& out, unsigned n, literal const* lits);
+        void display_assert(std::ostream& out, unsigned n, literal const* lits);
+        void visit_expr(std::ostream& out, expr* e);
+        std::ostream& display_expr(std::ostream& out, expr* e);        
+        void on_instantiation(unsigned n, sat::literal const* lits, unsigned k, euf::enode* const* bindings);
+        scoped_ptr<std::ostream> m_proof_out;
 
         // decompile
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
@@ -403,6 +409,7 @@ namespace euf {
         obj_map<expr, enode*> const& values2root();
         void model_updated(model_ref& mdl);
         expr* node2value(enode* n) const;
+        void display_validation_failure(std::ostream& out, model& mdl, enode* n);
 
         // diagnostics
         func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }

src/sat/smt/pb_solver.cpp

@@ -1430,10 +1430,9 @@ namespace pb {
             IF_VERBOSE(0, verbose_stream() << *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";
-            };
-            m_solver->get_drat().log_adhoc(fn);
+            auto * out = s().get_drat().out();
+            if (out)
+                *out << "c ba constraint " << *c << " 0\n";
         }
     }
 

src/sat/smt/q_ematch.cpp

@@ -372,16 +372,21 @@ namespace q {
     }
 
     void ematch::propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx) {
-        if (is_conflict) {
+        if (is_conflict) 
             ++m_stats.m_num_conflicts;
-            ctx.set_conflict(j_idx);
-        }
-        else {
+        else
             ++m_stats.m_num_propagations;
-            auto& j = justification::from_index(j_idx);
-            auto lit = instantiate(j.m_clause, j.m_binding, j.m_clause[idx]);
-            ctx.propagate(lit, j_idx);
-        }
+
+        auto& j = justification::from_index(j_idx);
+        sat::literal_vector lits;
+        lits.push_back(~j.m_clause.m_literal);
+        for (unsigned i = 0; i < j.m_clause.size(); ++i) 
+            lits.push_back(instantiate(j.m_clause, j.m_binding, j.m_clause[i])); 
+        m_qs.log_instantiation(lits, &j);
+        euf::th_proof_hint* ph = nullptr;
+        if (ctx.use_drat()) 
+            ph = q_proof_hint::mk(ctx, j.m_clause.size(), j.m_binding);
+        m_qs.add_clause(lits, ph);               
     }
 
     bool ematch::flush_prop_queue() {
@@ -408,6 +413,7 @@ namespace q {
     void ematch::add_instantiation(clause& c, binding& b, sat::literal lit) {
         m_evidence.reset();
         ctx.propagate(lit, mk_justification(UINT_MAX, c, b.nodes()));
+        m_qs.log_instantiation(~c.m_literal, lit);
     }
 
     sat::literal ematch::instantiate(clause& c, euf::enode* const* binding, lit const& l) {

src/sat/smt/q_eval.cpp

@@ -47,21 +47,21 @@ namespace q {
             unsigned lim = m_indirect_nodes.size();
             lit l = c[i];
             lbool cmp = compare(n, binding, l.lhs, l.rhs, evidence);
+            TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is " << cmp << "\n";);
             switch (cmp) {
-            case l_false:
+            case l_false:                
                 m_indirect_nodes.shrink(lim);
                 if (!l.sign)
                     break;
                 c.m_watch = i;
                 return l_true;
-            case l_true:
+            case l_true:   
                 m_indirect_nodes.shrink(lim);
                 if (l.sign)
-                    break;
+                    break;                
                 c.m_watch = i;
                 return l_true;
             case l_undef:
-                TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";);
                 if (idx != UINT_MAX) {
                     idx = UINT_MAX;
                     return l_undef;

src/sat/smt/q_mam.cpp

@@ -1961,7 +1961,7 @@ namespace q {
                 for (unsigned i = 0; i < num_args; i++)
                     m_args[i] = m_registers[pc->m_iregs[i]]->get_root();
                 for (enode* n : euf::enode_class(r)) {
-                    if (n->get_decl() == f) {
+                    if (n->get_decl() == f && num_args == n->num_args()) {
                         unsigned i = 0;
                         for (; i < num_args; i++) {
                             if (n->get_arg(i)->get_root() != m_args[i])

src/sat/smt/q_mam.h

@@ -45,7 +45,7 @@ namespace q {
 
         static mam * mk(euf::solver& ctx, ematch& em);
         
-        virtual ~mam() {}
+        virtual ~mam() = default;
         
         virtual void add_pattern(quantifier * q, app * mp) = 0;
 

src/sat/smt/q_mbi.cpp

@@ -68,10 +68,21 @@ namespace q {
             }
         }
         m_max_cex += ctx.get_config().m_mbqi_max_cexs;
-        for (auto const& [qlit, fml, generation] : m_instantiations) {
+        for (auto const& [qlit, fml, inst, generation] : m_instantiations) {
             euf::solver::scoped_generation sg(ctx, generation + 1);
             sat::literal lit = ctx.mk_literal(fml);
-            m_qs.add_clause(~qlit, ~lit);
+            euf::th_proof_hint* ph = nullptr;
+            if (!inst.empty()) {
+                ph = q_proof_hint::mk(ctx, inst.size(), inst.data());
+                sat::literal_vector lits;
+                lits.push_back(~qlit);
+                lits.push_back(~lit);
+                m_qs.add_clause(lits, ph);
+            }
+            else {
+                m_qs.add_clause(~qlit, ~lit);
+            }
+            m_qs.log_instantiation(~qlit, ~lit);
         }
         m_instantiations.reset();
         if (result != l_true)
@@ -223,10 +234,31 @@ namespace q {
         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));
+        unsigned generation = ctx.get_max_generation(proj);
+        expr_ref_vector inst = extract_binding(q);
+        m_instantiations.push_back(instantiation_t(qlit, proj, inst, generation));
     }
 
+    expr_ref_vector mbqi::extract_binding(quantifier* q) {
+        if (!m_defs.empty()) {
+            expr_safe_replace sub(m);
+            for (unsigned i = m_defs.size(); i-- > 0; ) {
+                sub(m_defs[i].term);
+                sub.insert(m_defs[i].var, m_defs[i].term);
+            }
+            q_body* qb = q2body(q);
+            expr_ref_vector inst(m);
+            for (expr* v : qb->vars) {
+                expr_ref t(m);
+                sub(v, t);
+                inst.push_back(t);
+            }
+            return inst;
+        }
+        return expr_ref_vector(m);
+    }
+
+
     void mbqi::add_universe_restriction(q_body& qb) {
         for (app* v : qb.vars) {
             sort* s = v->get_sort();
@@ -283,6 +315,7 @@ namespace q {
         expr_ref_vector fmls(qb.vbody);
         app_ref_vector vars(qb.vars);
         bool fmls_extracted = false;
+        m_defs.reset();
         TRACE("q",
               tout << "Project\n";
               tout << fmls << "\n";
@@ -313,16 +346,22 @@ namespace q {
                 fmls_extracted = true;
             }
             if (!p)
-                continue;
-            if (!(*p)(*m_model, vars, fmls))
-                return expr_ref(nullptr, m);
+                continue; 
+            if (ctx.use_drat()) {
+                if (!p->project(*m_model, vars, fmls, m_defs))
+                    return expr_ref(m);                
+            }
+            else if (!(*p)(*m_model, vars, fmls))
+                return expr_ref(m);
         }
         for (app* v : vars) {
             expr_ref term(m);
             expr_ref val = (*m_model)(v);
             val = m_model->unfold_as_array(val);
             term = replace_model_value(val);
-            rep.insert(v, term);        
+            rep.insert(v, term);
+            if (ctx.use_drat())
+                m_defs.push_back(mbp::def(expr_ref(v, m), term));
             eqs.push_back(m.mk_eq(v, val));
         }
         rep(fmls);
@@ -596,8 +635,8 @@ namespace q {
     void mbqi::collect_statistics(statistics& st) const {
         if (m_solver)
             m_solver->collect_statistics(st);
-        st.update("q-num-instantiations", m_stats.m_num_instantiations);
-        st.update("q-num-checks", m_stats.m_num_checks);
+        st.update("q mbi instantiations", m_stats.m_num_instantiations);
+        st.update("q mbi num checks", m_stats.m_num_checks);
     }
 
 }

src/sat/smt/q_mbi.h

@@ -66,15 +66,17 @@ namespace q {
         scoped_ptr_vector<obj_hashtable<expr>> m_values;
         scoped_ptr_vector<mbp::project_plugin> m_plugins;
         obj_map<quantifier, q_body*>           m_q2body;
-        unsigned                               m_max_cex{ 1 };
-        unsigned                               m_max_quick_check_rounds { 100 };
-        unsigned                               m_max_unbounded_equalities { 10 };
-        unsigned                               m_max_choose_candidates { 10 };
-        unsigned                               m_generation_bound{ UINT_MAX };
-        unsigned                               m_generation_max { UINT_MAX };
-        typedef std::tuple<sat::literal, expr_ref, unsigned> instantiation_t;
+        unsigned                               m_max_cex = 1;
+        unsigned                               m_max_quick_check_rounds = 100;
+        unsigned                               m_max_unbounded_equalities = 10;
+        unsigned                               m_max_choose_candidates = 10;
+        unsigned                               m_generation_bound = UINT_MAX;
+        unsigned                               m_generation_max = UINT_MAX;
+        typedef std::tuple<sat::literal, expr_ref, expr_ref_vector, unsigned> instantiation_t;
         vector<instantiation_t> m_instantiations;
+        vector<mbp::def>        m_defs;
 
+        expr_ref_vector extract_binding(quantifier* q);
         void restrict_to_universe(expr * sk, ptr_vector<expr> const & universe);
         // void register_value(expr* e);
         expr_ref replace_model_value(expr* e);

src/sat/smt/q_model_fixer.h

@@ -43,7 +43,7 @@ namespace q {
         ast_manager& m;
     public:
         projection_function(ast_manager& m) : m(m) {}
-        virtual ~projection_function() {}
+        virtual ~projection_function() = default;
         virtual expr* mk_lt(expr* a, expr* b) = 0;
         expr* mk_le(expr* a, expr* b) { return m.mk_not(mk_lt(b, a)); }
         virtual bool operator()(expr* a, expr* b) const = 0;

src/sat/smt/q_solver.cpp

@@ -24,6 +24,7 @@ Author:
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/sat_th.h"
 #include "qe/lite/qe_lite.h"
+#include <iostream>
 
 
 namespace q {
@@ -356,4 +357,43 @@ namespace q {
         m_ematch.get_antecedents(l, idx, r, probing);
     }
 
+    void solver::log_instantiation(unsigned n, sat::literal const* lits, justification* j) {
+        TRACE("q", for (unsigned i = 0; i < n; ++i) tout << literal2expr(lits[i]) << "\n";);
+        if (get_config().m_instantiations2console) {
+            ctx.on_instantiation(n, lits, j ? j->m_clause.num_decls() : 0, j ? j->m_binding : nullptr);
+        }
+    }
+
+    q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned n, euf::enode* const* bindings) {
+        auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n));
+        q_proof_hint* ph = new (mem) q_proof_hint();
+        ph->m_num_bindings = n;
+        for (unsigned i = 0; i < n; ++i)
+            ph->m_bindings[i] = bindings[i]->get_expr();
+        return ph;
+    }
+
+    q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned n, expr* const* bindings) {
+        auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n));
+        q_proof_hint* ph = new (mem) q_proof_hint();
+        ph->m_num_bindings = n;
+        for (unsigned i = 0; i < n; ++i)
+            ph->m_bindings[i] = bindings[i];
+        return ph;
+    }
+
+    expr* q_proof_hint::get_hint(euf::solver& s) const {
+        ast_manager& m = s.get_manager();
+        expr_ref_vector args(m);
+        sort_ref_vector sorts(m);
+        for (unsigned i = 0; i < m_num_bindings; ++i) {
+            args.push_back(m_bindings[i]);
+            sorts.push_back(args.back()->get_sort());
+        }
+        sort* range = m.mk_proof_sort();
+        func_decl* d = m.mk_func_decl(symbol("inst"), args.size(), sorts.data(), range);
+        expr* r = m.mk_app(d, args);
+        return r;
+    }
+
 }

src/sat/smt/q_solver.h

@@ -29,6 +29,16 @@ namespace euf {
 
 namespace q {
 
+    struct q_proof_hint : public euf::th_proof_hint {
+        unsigned     m_num_bindings;
+        expr*        m_bindings[0];
+        q_proof_hint() {}
+        static size_t get_obj_size(unsigned num_bindings) { return sizeof(q_proof_hint) + num_bindings*sizeof(expr*); }
+        static q_proof_hint* mk(euf::solver& s, unsigned n, euf::enode* const* bindings);
+        static q_proof_hint* mk(euf::solver& s, unsigned n, expr* const* bindings);
+        expr* get_hint(euf::solver& s) const override;
+    };
+
     class solver : public euf::th_euf_solver {
 
         typedef obj_map<quantifier, quantifier*> flat_table;
@@ -88,5 +98,9 @@ namespace q {
         sat::literal_vector const& universal() const { return m_universal; }
         quantifier* flatten(quantifier* q);
 
+        void log_instantiation(sat::literal q, sat::literal i, justification* j = nullptr) { sat::literal lits[2] = { q, i }; log_instantiation(2, lits, j); }
+        void log_instantiation(sat::literal_vector const& lits, justification* j) { log_instantiation(lits.size(), lits.data(), j); }
+        void log_instantiation(unsigned n, sat::literal const* lits, justification* j);
+
     };
 }

src/sat/smt/sat_internalizer.h

@@ -21,7 +21,7 @@ Author:
 namespace sat {
     class sat_internalizer {
     public:
-        virtual ~sat_internalizer() {}
+        virtual ~sat_internalizer() = default;
         virtual bool is_bool_op(expr* e) const = 0;
         virtual literal internalize(expr* e, bool learned) = 0;
         virtual bool_var to_bool_var(expr* e) = 0;

src/sat/smt/sat_th.cpp

@@ -125,7 +125,7 @@ namespace euf {
             pop_core(n);        
     }
 
-    sat::status th_euf_solver::mk_status(sat::proof_hint const* ps) {
+    sat::status th_euf_solver::mk_status(th_proof_hint const* ps) {
         return sat::status::th(m_is_redundant, get_id(), ps);
     }
 
@@ -149,7 +149,7 @@ namespace euf {
         return add_clause(2, lits);
     }
 
-    bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::proof_hint const* ps) {      
+    bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps) {      
         sat::literal lits[2] = { a, b };
         return add_clause(2, lits, ps);
     }
@@ -164,7 +164,7 @@ namespace euf {
         return add_clause(4, lits);
     }
 
-    bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, sat::proof_hint const* ps) {
+    bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) {
         bool was_true = false;
         for (unsigned i = 0; i < n; ++i)       
             was_true |= is_true(lits[i]);
@@ -226,13 +226,14 @@ namespace euf {
         return ctx.s().rand()();
     }
 
-    size_t th_explain::get_obj_size(unsigned num_lits, unsigned num_eqs, sat::proof_hint const* pma) {
-        return sat::constraint_base::obj_size(sizeof(th_explain) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs + (pma?pma->to_string().length()+1:1));
+    size_t th_explain::get_obj_size(unsigned num_lits, unsigned num_eqs) {
+        return sat::constraint_base::obj_size(sizeof(th_explain) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs);
     }
 
-    th_explain::th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& p, sat::proof_hint const* pma) {
+    th_explain::th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& p, th_proof_hint const* pma) {
         m_consequent = c;
         m_eq = p;
+        m_proof_hint = pma;
         m_num_literals = n_lits;
         m_num_eqs = n_eqs;
         char * base_ptr = reinterpret_cast<char*>(this) + sizeof(th_explain); 
@@ -244,33 +245,24 @@ namespace euf {
         m_eqs = reinterpret_cast<enode_pair*>(base_ptr);
         for (i = 0; i < n_eqs; ++i)
             m_eqs[i] = eqs[i];
-        base_ptr += sizeof(enode_pair) * n_eqs;        
-        m_pragma = reinterpret_cast<char*>(base_ptr);
-        i = 0;
-        if (pma) {
-            std::string s = pma->to_string();
-            for (i = 0; s[i]; ++i)
-                m_pragma[i] = s[i];
-        }
-        m_pragma[i] = 0;
     }
 
-    th_explain* th_explain::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, sat::proof_hint const* pma) {
+    th_explain* th_explain::mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, th_proof_hint const* pma) {
         region& r = th.ctx.get_region();
-        void* mem = r.allocate(get_obj_size(n_lits, n_eqs, pma));
+        void* mem = r.allocate(get_obj_size(n_lits, n_eqs));
         sat::constraint_base::initialize(mem, &th);
-        return new (sat::constraint_base::ptr2mem(mem)) th_explain(n_lits, lits, n_eqs, eqs, c, enode_pair(x, y));
+        return new (sat::constraint_base::ptr2mem(mem)) th_explain(n_lits, lits, n_eqs, eqs, c, enode_pair(x, y), pma);
     }
 
-    th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, sat::proof_hint const* pma) {
+    th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* pma) {
         return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), consequent, nullptr, nullptr, pma);
     }
 
-    th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma) {
+    th_explain* th_explain::propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma) {
         return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), sat::null_literal, x, y, pma);
     }
 
-    th_explain* th_explain::propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma) {
+    th_explain* th_explain::propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma) {
         return mk(th, 0, nullptr, eqs.size(), eqs.data(), sat::null_literal, x, y, pma);
     }
 
@@ -313,8 +305,8 @@ namespace euf {
             out << "--> " << m_consequent;
         if (m_eq.first != nullptr)
             out << "--> " << m_eq.first->get_expr_id() << " == " << m_eq.second->get_expr_id();
-        if (m_pragma != nullptr)
-            out << " p " << m_pragma;
+        if (m_proof_hint != nullptr)
+            out << " p ";
         return out;
     }
 

src/sat/smt/sat_th.h

@@ -39,7 +39,7 @@ namespace euf {
         virtual bool post_visit(expr* e, bool sign, bool root) { return false; }
 
     public:
-        virtual ~th_internalizer() {}
+        virtual ~th_internalizer() = default;
 
         virtual sat::literal internalize(expr* e, bool sign, bool root, bool redundant) = 0;
 
@@ -58,9 +58,10 @@ namespace euf {
 
     };
 
+
     class th_decompile {
     public:
-        virtual ~th_decompile() {}
+        virtual ~th_decompile() = default;
 
         virtual bool to_formulas(std::function<expr_ref(sat::literal)>& lit2expr, expr_ref_vector& fmls) { return false; }
     };
@@ -68,7 +69,7 @@ namespace euf {
     class th_model_builder {
     public:
 
-        virtual ~th_model_builder() {}
+        virtual ~th_model_builder() = default;
 
         /**
            \brief compute the value for enode \c n and store the value in \c values
@@ -138,6 +139,11 @@ namespace euf {
 
     };
 
+    class th_proof_hint : public sat::proof_hint {
+    public:
+        virtual expr* get_hint(euf::solver& s) const = 0;
+    };
+
     class th_euf_solver : public th_solver {
     protected:
         solver& ctx;
@@ -150,16 +156,16 @@ namespace euf {
         region& get_region();
 
 
-        sat::status mk_status(sat::proof_hint const* ps = nullptr);
+        sat::status mk_status(th_proof_hint const* ps = nullptr);
         bool add_unit(sat::literal lit);
         bool add_units(sat::literal_vector const& lits);
         bool add_clause(sat::literal lit) { return add_unit(lit); }
         bool add_clause(sat::literal a, sat::literal b);
-        bool add_clause(sat::literal a, sat::literal b, sat::proof_hint const* ps);
+        bool add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps);
         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, sat::proof_hint const* ps = nullptr) { return add_clause(lits.size(), lits.data(), ps); }
-        bool add_clause(unsigned n, sat::literal* lits, sat::proof_hint const* ps = nullptr);
+        bool add_clause(sat::literal_vector const& lits, th_proof_hint const* ps = nullptr) { return add_clause(lits.size(), lits.data(), ps); }
+        bool add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps = nullptr);
         void add_equiv(sat::literal a, sat::literal b);
         void add_equiv_and(sat::literal a, sat::literal_vector const& bs);
 
@@ -220,16 +226,16 @@ namespace euf {
     * that retrieve literals on demand.
     */
     class th_explain {
-        sat::literal   m_consequent = sat::null_literal; // literal consequent for propagations
-        enode_pair     m_eq = enode_pair();              // equality consequent for propagations
+        sat::literal     m_consequent = sat::null_literal; // literal consequent for propagations
+        enode_pair       m_eq = enode_pair();              // equality consequent for propagations
+        th_proof_hint const* m_proof_hint;
         unsigned       m_num_literals;
         unsigned       m_num_eqs;        
         sat::literal*  m_literals;
         enode_pair*    m_eqs;
-        char*          m_pragma = nullptr;
-        static size_t get_obj_size(unsigned num_lits, unsigned num_eqs, sat::proof_hint const* pma);
-        th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq, sat::proof_hint const* pma = nullptr);
-        static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, sat::proof_hint const* pma = nullptr);
+        static size_t get_obj_size(unsigned num_lits, unsigned num_eqs);
+        th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& eq, th_proof_hint const* pma = nullptr);
+        static th_explain* mk(th_euf_solver& th, unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode* x, enode* y, th_proof_hint const* pma = nullptr);
 
     public:
         static th_explain* conflict(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs);
@@ -240,9 +246,9 @@ namespace euf {
         static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
         static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y);
         static th_explain* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
-        static th_explain* propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma = nullptr);
-        static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, sat::proof_hint const* pma = nullptr);
-        static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma = nullptr);
+        static th_explain* propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma = nullptr);
+        static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, th_proof_hint const* pma = nullptr);
+        static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, th_proof_hint const* pma = nullptr);
 
         sat::ext_constraint_idx to_index() const {
             return sat::constraint_base::mem2base(this);
@@ -277,7 +283,7 @@ namespace euf {
 
         enode_pair eq_consequent() const { return m_eq; }
 
-        sat::proof_hint const* get_pragma() const { return nullptr; } //*m_pragma ? m_pragma : nullptr; }
+        th_proof_hint const* get_pragma() const { return m_proof_hint; } 
 
     };
 

src/sat/smt/xor_solver.cpp

@@ -0,0 +1,79 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    xor_solver.h
+
+Abstract:
+
+    XOR solver.
+    Interface outline.
+
+--*/
+
+
+#include "sat/smt/xor_solver.h"
+#include "sat/sat_simplifier_params.hpp"
+#include "sat/sat_xor_finder.h"
+
+namespace xr {
+
+    solver::solver(euf::solver& ctx):
+        th_solver(ctx.get_manager(), symbol("xor-solver"), ctx.get_manager().get_family_id("xor-solver"))
+    {}
+
+    euf::th_solver* solver::clone(euf::solver& ctx) {
+        // and relevant copy internal state
+        return alloc(solver, ctx);
+    }
+
+    void solver::asserted(sat::literal l) {
+
+    }
+
+    bool solver::unit_propagate() {
+        return false;
+    }
+    
+    void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx,
+                                 sat::literal_vector & r, bool probing) {
+        
+    }
+    
+    sat::check_result solver::check() {
+        return sat::check_result::CR_DONE;
+    }
+    
+    void solver::push() {
+    }
+    
+    void solver::pop(unsigned n) {
+    }
+
+    // inprocessing
+    // pre_simplify: decompile all xor constraints to allow other in-processing.
+    // simplify: recompile clauses to xor constraints
+    // literals that get added to xor constraints are tagged with the theory.
+    void solver::pre_simplify() {
+        
+    }
+
+    void solver::simplify() {
+        
+    }
+
+    std::ostream& solver::display(std::ostream& out) const {
+        return out;
+    }
+    
+    std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const  {
+        return out;
+    }
+    
+    std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
+        return out;
+    }
+    
+}
+

src/sat/smt/xor_solver.h

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    xor_solver.h
+
+Abstract:
+
+    XOR solver.
+    Interface outline.
+
+--*/
+
+#pragma once
+
+#include "sat/smt/euf_solver.h"
+
+namespace xr {
+    class solver : public euf::th_solver {
+    public:
+        solver(euf::solver& ctx);
+        
+        th_solver* clone(euf::solver& ctx) override;
+
+        sat::literal internalize(expr* e, bool sign, bool root, bool redundant)  override { UNREACHABLE(); return sat::null_literal; }
+
+        void internalize(expr* e, bool redundant) override { UNREACHABLE(); }
+
+
+        void asserted(sat::literal l) override;
+        bool unit_propagate() override;
+        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override;
+
+        void pre_simplify() override;
+        void simplify() override;
+
+        sat::check_result check() override;
+        void push() override;
+        void pop(unsigned n) 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;
+
+    };
+
+}