release nodes

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

src/ast/euf/euf_egraph.cpp

@@ -130,6 +130,11 @@ namespace euf {
         return n;
     }
 
+    void egraph::~egraph() {
+        for (enode* n : m_nodes) 
+            n->~enode();        
+    }
+
     void egraph::pop(unsigned num_scopes) {
         if (num_scopes <= m_num_scopes) {
             m_num_scopes -= num_scopes;

src/ast/euf/euf_egraph.h

@@ -106,6 +106,7 @@ namespace euf {
         
     public:
         egraph(ast_manager& m): m(m), m_table(m), m_exprs(m) {}
+        ~egraph();
         enode* find(expr* f) { return m_expr2enode.get(f->get_id(), nullptr); }
         enode* mk(expr* f, unsigned n, enode *const* args);
         void push() { ++m_num_scopes; }

src/ast/euf/euf_etable.cpp

@@ -169,7 +169,7 @@ namespace euf {
         binary_table* tb = UNTAG(binary_table*, t);
         out << "b ";
         for (enode* n : *tb) {
-            out << n->get_owner_id() << " " << cg_binary_hash()(n) << " ";
+            out << n->get_owner_id() << " ";
         }
         out << "\n";
     }

src/sat/smt/CMakeLists.txt

@@ -5,6 +5,7 @@ z3_add_component(sat_smt
     xor_solver.cpp
     ba_internalize.cpp
     euf_ackerman.cpp
+    euf_internalize.cpp
     euf_solver.cpp
     euf_model.cpp
   COMPONENT_DEPENDENCIES

src/sat/smt/ba_internalize.cpp

@@ -21,7 +21,8 @@ Author:
 
 namespace sat {
 
-    literal ba_solver::internalize(expr* e, bool sign, bool root) {
+    literal ba_solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        flet<bool> _redundant(m_is_redundant, redundant);
         if (m_pb.is_pb(e)) 
             return internalize_pb(e, sign, root);
         if (m.is_xor(e))
@@ -35,7 +36,7 @@ namespace sat {
         sat::bool_var v = s().add_var(true);
         lits.push_back(literal(v, true));
         auto add_expr = [&](expr* a) {
-            literal lit = si.internalize(a);
+            literal lit = si.internalize(a, m_is_redundant);
             s().set_external(lit.var());
             lits.push_back(lit);
         };
@@ -47,7 +48,7 @@ namespace sat {
         for (unsigned i = 1; i + 1 < lits.size(); ++i) {
             lits[i].neg();
         }
-        add_xr(lits);
+        add_xr(lits, m_is_redundant);
         auto* aig = s().get_cut_simplifier();
         if (aig) aig->add_xor(~lits.back(), lits.size() - 1, lits.c_ptr() + 1);
         sat::literal lit(v, sign);
@@ -100,7 +101,7 @@ namespace sat {
 
     void ba_solver::convert_pb_args(app* t, literal_vector& lits) {
         for (expr* arg : *t) {
-            lits.push_back(si.internalize(arg));
+            lits.push_back(si.internalize(arg, m_is_redundant));
             s().set_external(lits.back().var());
         }
     }

src/sat/smt/ba_solver.cpp

@@ -1748,7 +1748,7 @@ namespace sat {
 
     void ba_solver::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
         literal lit = v == null_bool_var ? null_literal : literal(v, false);
-        add_at_least(lit, lits, k, false);
+        add_at_least(lit, lits, k, m_is_redundant);
     }
 
     ba_solver::constraint* ba_solver::add_at_least(literal lit, literal_vector const& lits, unsigned k, bool learned) {
@@ -1840,7 +1840,7 @@ namespace sat {
 
     void ba_solver::add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k) {
         literal lit = v == null_bool_var ? null_literal : literal(v, false);
-        add_pb_ge(lit, wlits, k, false);
+        add_pb_ge(lit, wlits, k, m_is_redundant);
     }
 
     /*

src/sat/smt/ba_solver.h

@@ -554,6 +554,7 @@ namespace sat {
         void convert_to_wlits(app* t, sat::literal_vector const& lits, svector<wliteral>& wlits);
         void convert_pb_args(app* t, svector<wliteral>& wlits);
         void convert_pb_args(app* t, literal_vector& lits);
+        bool m_is_redundant{ false };
         literal internalize_pb(expr* e, bool sign, bool root);
         literal internalize_xor(expr* e, bool sign, bool root);
 
@@ -599,7 +600,7 @@ namespace sat {
         bool is_blocked(literal l, ext_constraint_idx idx) override;
         bool check_model(model const& m) const override;
 
-        literal internalize(expr* e, bool sign, bool root) override;
+        literal internalize(expr* e, bool sign, bool root, bool redundant) override;
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
         th_solver* fresh(solver* s, ast_manager& m, sat_internalizer& si) override;
 

src/sat/smt/euf_ackerman.cpp

@@ -189,11 +189,11 @@ namespace euf {
         unsigned sz = a->get_num_args();
         for (unsigned i = 0; i < sz; ++i) {
             expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m);
-            sat::literal lit = s.internalize(eq, true, false);
+            sat::literal lit = s.internalize(eq, true, false, true);
             lits.push_back(~lit);
         }
         expr_ref eq(m.mk_eq(a, b), m);
-        lits.push_back(s.internalize(eq, false, false));
+        lits.push_back(s.internalize(eq, false, false, true));
         s.s().mk_clause(lits, true);
     }
 
@@ -202,9 +202,9 @@ namespace euf {
         expr_ref eq1(m.mk_eq(a, c), m);
         expr_ref eq2(m.mk_eq(b, c), m);
         expr_ref eq3(m.mk_eq(a, b), m);
-        lits[0] = s.internalize(eq1, true, false);
-        lits[1] = s.internalize(eq2, true, false);
-        lits[2] = s.internalize(eq3, false, false);
+        lits[0] = s.internalize(eq1, true, false, true);
+        lits[1] = s.internalize(eq2, true, false, true);
+        lits[2] = s.internalize(eq3, false, false, true);
         s.s().mk_clause(3, lits, true);
     }
 }

src/sat/smt/euf_internalize.cpp

@@ -0,0 +1,242 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    euf_internalize.cpp
+
+Abstract:
+
+    Internalize utilities for EUF solver plugin.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "ast/pb_decl_plugin.h"
+#include "tactic/tactic_exception.h"
+#include "sat/smt/euf_solver.h"
+
+namespace euf {
+
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
+        flet<bool> _is_learned(m_is_redundant, learned);
+        auto* ext = get_solver(e);
+        if (ext)
+            return ext->internalize(e, sign, root, learned);
+        IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(e, m) << "\n");
+        SASSERT(!si.is_bool_op(e));
+        sat::scoped_stack _sc(m_stack);
+        unsigned sz = m_stack.size();
+        euf::enode* n = visit(e);
+        while (m_stack.size() > sz) {
+        loop:
+            if (!m.inc())
+                throw tactic_exception(m.limit().get_cancel_msg());
+            sat::frame & fr = m_stack.back();
+            expr* e = fr.m_e;
+            if (m_egraph.find(e)) {
+                m_stack.pop_back();
+                continue;
+            }
+            unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
+            
+            while (fr.m_idx < num) {
+                expr* arg = to_app(e)->get_arg(fr.m_idx);
+                fr.m_idx++;
+                n = visit(arg);
+                if (!n)
+                    goto loop;
+            }
+            m_args.reset();
+            for (unsigned i = 0; i < num; ++i)
+                m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
+            if (root && internalize_root(to_app(e), m_args.c_ptr(), sign))
+                return sat::null_literal;
+            n = m_egraph.mk(e, num, m_args.c_ptr());
+            attach_node(n);
+        }        
+        SASSERT(m_egraph.find(e));
+        return literal(m_expr2var.to_bool_var(e), sign);
+    }
+
+    euf::enode* solver::visit(expr* e) {
+        euf::enode* n = m_egraph.find(e);
+        if (n)
+            return n;
+        if (si.is_bool_op(e)) {
+            sat::literal lit = si.internalize(e, m_is_redundant);
+            n = m_var2node.get(lit.var(), nullptr);
+            if (n && !lit.sign())
+                return n;
+            
+            n = m_egraph.mk(e, 0, nullptr);
+            attach_lit(lit, n);
+            if (!m.is_true(e) && !m.is_false(e)) 
+                s().set_external(lit.var());
+            return n;
+        }
+        if (is_app(e) && to_app(e)->get_num_args() > 0) {
+            m_stack.push_back(sat::frame(e));
+            return nullptr;
+        }
+        n = m_egraph.mk(e, 0, nullptr);
+        attach_node(n);
+        return n;
+    }
+
+    void solver::attach_node(euf::enode* n) {
+        expr* e = n->get_owner();
+        if (m.is_bool(e)) {
+            sat::bool_var v = si.add_bool_var(e);
+            attach_lit(literal(v, false),  n);
+        }
+        axiomatize_basic(n);
+    }
+
+    void solver::attach_lit(literal lit, euf::enode* n) {
+        if (lit.sign()) {
+            sat::bool_var v = si.add_bool_var(n->get_owner());
+            sat::literal lit2 = literal(v, false);
+            s().mk_clause(~lit, lit2, false);
+            s().mk_clause(lit, ~lit2, false);
+            lit = lit2;
+        }
+        sat::bool_var v = lit.var();
+        m_var2node.reserve(v + 1, nullptr);
+        SASSERT(m_var2node[v] == nullptr);
+        m_var2node[v] = n;
+        m_var_trail.push_back(v);
+    }
+
+    bool solver::internalize_root(app* e, enode* const* args, bool sign) {
+        if (m.is_distinct(e)) {
+            if (sign)
+                add_not_distinct_axiom(e, args);
+            else
+                add_distinct_axiom(e, args);
+            return true;
+        }
+        return false;
+    }
+
+    void solver::add_not_distinct_axiom(app* e, enode* const* args) {
+        SASSERT(m.is_distinct(e));
+        unsigned sz = e->get_num_args();
+        if (sz <= 1)
+            return;
+
+        static const unsigned distinct_max_args = 24;
+        if (sz <= distinct_max_args) {
+            sat::literal_vector lits;
+            for (unsigned i = 0; i < sz; ++i) {
+                for (unsigned j = i + 1; j < sz; ++j) {
+                    expr_ref eq(m.mk_eq(args[i]->get_owner(), args[j]->get_owner()), m);
+                    sat::literal lit = internalize(eq, false, false, m_is_redundant);
+                    lits.push_back(lit);
+                }
+            }
+            s().mk_clause(lits, false);
+        }
+        else {
+            // g(f(x_i)) = x_i
+            // f(x_1) = a + .... + f(x_n) = a >= 2
+            sort* srt = m.get_sort(e->get_arg(0));
+            SASSERT(!m.is_bool(srt));
+            sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
+            sort* u_ptr = u.get();
+            func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m);
+            func_decl_ref g(m.mk_fresh_func_decl("dist-g", "", 1, &u_ptr, srt), m);
+            expr_ref a(m.mk_fresh_const("a", u), m);
+            expr_ref_vector eqs(m);
+            for (expr* arg : *e) {
+                expr_ref fapp(m.mk_app(f, arg), m);
+                expr_ref gapp(m.mk_app(g, fapp.get()), m);
+                expr_ref eq(m.mk_eq(gapp, arg), m);
+                sat::literal lit = internalize(eq, false, false, m_is_redundant);
+                s().add_clause(1, &lit, false);
+                eqs.push_back(m.mk_eq(fapp, a));
+            }
+            pb_util pb(m);
+            expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.c_ptr(), 2), m);
+            sat::literal lit = si.internalize(at_least2, m_is_redundant);
+            s().mk_clause(1, &lit, false);
+        }
+    }
+
+    void solver::add_distinct_axiom(app* e, enode* const* args) {
+        SASSERT(m.is_distinct(e));
+        static const unsigned distinct_max_args = 24;
+        unsigned sz = e->get_num_args();
+        if (sz <= 1) {
+            s().mk_clause(0, nullptr, m_is_redundant);
+            return;
+        }           
+        if (sz <= distinct_max_args) {
+            for (unsigned i = 0; i < sz; ++i) {
+                for (unsigned j = i + 1; j < sz; ++j) {
+                    expr_ref eq(m.mk_eq(args[i]->get_owner(), args[j]->get_owner()), m);
+                    sat::literal lit = internalize(eq, true, false, m_is_redundant);
+                    s().add_clause(1, &lit, m_is_redundant);
+                }
+            }
+        }
+        else {
+            // dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n
+            sort* srt = m.get_sort(e->get_arg(0));
+            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);
+            for (unsigned i = 0; i < sz; ++i) {
+                expr_ref fapp(m.mk_app(f, e->get_arg(i)), m);
+                expr_ref fresh(m.mk_fresh_const("dist-value", u), m);
+                enode* n = m_egraph.mk(fresh, 0, nullptr);
+                n->mark_interpreted();
+                expr_ref eq(m.mk_eq(fapp, fresh), m);
+                sat::literal lit = internalize(eq, false, false, m_is_redundant);
+                s().add_clause(1, &lit, m_is_redundant);
+            }
+        }
+    }
+
+    void solver::axiomatize_basic(enode* n) {
+        expr* e = n->get_owner();
+        if (m.is_ite(e)) {        
+            app* a = to_app(e);
+            expr* c = a->get_arg(0);
+            expr* th = a->get_arg(1);
+            expr* el = a->get_arg(2);
+            sat::bool_var v = m_expr2var.to_bool_var(c);
+            SASSERT(v != sat::null_bool_var);
+            expr_ref eq_th(m.mk_eq(a, th), m);
+            expr_ref eq_el(m.mk_eq(a, el), m);
+            sat::literal lit_th = internalize(eq_th, false, false, m_is_redundant);
+            sat::literal lit_el = internalize(eq_el, false, false, m_is_redundant);
+            literal lits1[2] = { literal(v, true),  lit_th };
+            literal lits2[2] = { literal(v, false), lit_el };
+            s().add_clause(2, lits1, m_is_redundant);
+            s().add_clause(2, lits2, m_is_redundant);
+        }
+        else if (m.is_distinct(e)) {
+            expr_ref_vector eqs(m);
+            unsigned sz = n->num_args();
+            for (unsigned i = 0; i < sz; ++i) {
+                for (unsigned j = i + 1; j < sz; ++j) {
+                    expr_ref eq(m.mk_eq(n->get_arg(i)->get_owner(), n->get_arg(j)->get_owner()), m);
+                    eqs.push_back(eq);
+                }
+            }
+            expr_ref fml(m.mk_or(eqs), m);
+            sat::literal dist(m_expr2var.to_bool_var(e), false);
+            sat::literal some_eq = si.internalize(fml, m_is_redundant);
+            sat::literal lits1[2] = { ~dist, ~some_eq };
+            sat::literal lits2[2] = { dist, some_eq };
+            s().add_clause(2, lits1, m_is_redundant);
+            s().add_clause(2, lits2, m_is_redundant);            
+        }
+    }
+
+}

src/sat/smt/euf_model.cpp

@@ -31,8 +31,12 @@ namespace euf {
     }
 
     bool solver::include_func_interp(func_decl* f) {
+        if (f->is_skolem())
+            return false;
         if (f->get_family_id() == null_family_id)
             return true;
+        if (f->get_family_id() == m.get_basic_family_id())
+            return false;
         sat::th_model_builder* mb = get_solver(f);
         return mb && mb->include_func_interp(f);
     }
@@ -97,7 +101,7 @@ namespace euf {
             if (!is_app(e))
                 continue;
             app* a = to_app(e);
-            func_decl* f = a->get_decl();
+            func_decl* f = a->get_decl();            
             if (!include_func_interp(f))
                 continue;
             if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(f))

src/sat/smt/euf_solver.cpp

@@ -16,7 +16,6 @@ Author:
 --*/
 
 #include "ast/pb_decl_plugin.h"
-#include "tactic/tactic_exception.h"
 #include "sat/sat_solver.h"
 #include "sat/smt/sat_smt.h"
 #include "sat/smt/ba_solver.h"
@@ -32,10 +31,9 @@ namespace euf {
     * retrieve extension that is associated with Boolean variable.
     */
     sat::th_solver* solver::get_solver(sat::bool_var v) {
-        unsigned idx = literal(v, false).index();
-        if (idx >= m_lit2node.size())
+        if (v >= m_var2node.size())
             return nullptr;
-        euf::enode* n = m_lit2node[idx];
+        euf::enode* n = m_var2node[v];
         if (!n)
             return nullptr;
         return get_solver(n->get_owner());
@@ -111,19 +109,20 @@ namespace euf {
             m_egraph.explain<unsigned>(m_explain);
             break;
         case constraint::kind_t::eq:
-            n = m_lit2node[l.index()];
+            n = m_var2node[l.var()];
             SASSERT(n);
             SASSERT(m_egraph.is_equality(n));
+            SASSERT(!l.sign());
             m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1), n->commutative());
             break;
         case constraint::kind_t::lit:
-            n = m_lit2node[l.index()];
+            n = m_var2node[l.var()];
             SASSERT(n);
             SASSERT(m.is_bool(n->get_owner()));
             m_egraph.explain_eq<unsigned>(m_explain, n, (l.sign() ? mk_false() : mk_true()), false);
             break;
         default:
-            std::cout << (unsigned)j.kind() << "\n";
+            IF_VERBOSE(0, verbose_stream() << (unsigned)j.kind() << "\n");
             UNREACHABLE();
         }
         for (unsigned* idx : m_explain) 
@@ -133,27 +132,25 @@ namespace euf {
     void solver::asserted(literal l) {
         auto* ext = get_solver(l.var());
         if (ext) {
-            force_push();
             ext->asserted(l);
             return;
         }
 
         bool sign = l.sign();
-        unsigned idx = sat::literal(l.var(), false).index();
-        auto n = m_lit2node.get(idx, nullptr);
+        auto n = m_var2node.get(l.var(), nullptr);
         if (!n)
             return;
-        force_push();
         
         expr* e = n->get_owner();
         if (m.is_eq(e) && !sign) {
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
+            TRACE("euf", tout << "merge " << na->get_owner_id() << nb->get_owner_id() << "\n";);
             m_egraph.merge(na, nb, base_ptr() + l.index());
         }
         else {            
             euf::enode* nb = sign ? mk_false() : mk_true();
-            std::cout << "merge " << n->get_owner_id() << " " << sign << " " << nb->get_owner_id() << "\n";
+            TRACE("euf", tout << "merge " << n->get_owner_id() << " " << mk_pp(nb->get_owner(), m)  << "\n";);
             m_egraph.merge(n, nb, base_ptr() + l.index());
         }
         // TBD: delay propagation?
@@ -222,7 +219,7 @@ namespace euf {
 
     void solver::push() {
 		scope s;
-		s.m_lit_lim = m_lit_trail.size();
+		s.m_var_lim = m_var_trail.size();
 		s.m_trail_lim = m_trail.size();
 		m_scopes.push_back(s);
 		m_region.push_scope();
@@ -244,9 +241,9 @@ namespace euf {
 
         scope const & s = m_scopes[m_scopes.size() - n];
 
-        for (unsigned i = m_lit_trail.size(); i-- > s.m_lit_lim; )
-            m_lit2node[m_lit_trail[i]] = nullptr;
-        m_lit_trail.shrink(s.m_lit_lim);
+        for (unsigned i = m_var_trail.size(); i-- > s.m_var_lim; )
+            m_var2node[m_var_trail[i]] = nullptr;
+        m_var_trail.shrink(s.m_var_lim);
         
         undo_trail_stack(*this, m_trail, s.m_trail_lim);
 
@@ -280,9 +277,11 @@ namespace euf {
 
     std::ostream& solver::display(std::ostream& out) const {
         m_egraph.display(out);
-        for (unsigned idx : m_lit_trail) {
-            euf::enode* n = m_lit2node[idx];
-            out << sat::to_literal(idx) << ": " << m_egraph.pp(n);
+
+        out << "bool-vars\n";
+        for (unsigned v : m_var_trail) {
+            euf::enode* n = m_var2node[v];
+            out << v << ": " << m_egraph.pp(n);
         }
         for (auto* e : m_solvers)
             e->display(out);
@@ -369,8 +368,8 @@ namespace euf {
     unsigned solver::max_var(unsigned w) const { 
         for (auto* e : m_solvers)
             w = e->max_var(w);
-        for (unsigned sz = m_lit2node.size(); sz-- > 0; ) {
-            euf::enode* n = m_lit2node[sz];
+        for (unsigned sz = m_var2node.size(); sz-- > 0; ) {
+            euf::enode* n = m_var2node[sz];
             if (n && m.is_bool(n->get_owner())) {
                 w = std::max(w, sz);
                 break;
@@ -413,86 +412,6 @@ namespace euf {
         m_egraph.set_used_cc(used_cc);
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root) {
-        force_push();
-        auto* ext = get_solver(e);
-        if (ext)
-            return ext->internalize(e, sign, root);
-        IF_VERBOSE(0, verbose_stream() << "internalize: " << mk_pp(e, m) << "\n");
-        SASSERT(!si.is_bool_op(e));
-        sat::scoped_stack _sc(m_stack);
-        unsigned sz = m_stack.size();
-        euf::enode* n = visit(e);
-        while (m_stack.size() > sz) {
-        loop:
-            if (!m.inc())
-                throw tactic_exception(m.limit().get_cancel_msg());
-            sat::frame & fr = m_stack.back();
-            expr* e = fr.m_e;
-            if (m_egraph.find(e)) {
-                m_stack.pop_back();
-                continue;
-            }
-            unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
-            
-            while (fr.m_idx < num) {
-                expr* arg = to_app(e)->get_arg(fr.m_idx);
-                fr.m_idx++;
-                n = visit(arg);
-                if (!n)
-                    goto loop;
-            }
-            m_args.reset();
-            for (unsigned i = 0; i < num; ++i)
-                m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
-            n = m_egraph.mk(e, num, m_args.c_ptr());
-            attach_bool_var(n);
-        }        
-        SASSERT(m_egraph.find(e));
-        return literal(m_expr2var.to_bool_var(e), sign);
-    }
-
-    euf::enode* solver::visit(expr* e) {
-        euf::enode* n = m_egraph.find(e);
-        if (n)
-            return n;
-        if (si.is_bool_op(e)) {
-            sat::literal lit = si.internalize(e);
-            n = m_lit2node.get(lit.index(), nullptr);
-            if (n)
-                return n;
-            
-            n = m_egraph.mk(e, 0, nullptr);
-            attach_lit(lit, n);
-            if (!m.is_true(e) && !m.is_false(e)) 
-                s().set_external(lit.var());
-            return n;
-        }
-        if (is_app(e) && to_app(e)->get_num_args() > 0) {
-            m_stack.push_back(sat::frame(e));
-            return nullptr;
-        }
-        n = m_egraph.mk(e, 0, nullptr);
-        attach_bool_var(n);
-        return n;
-    }
-
-    void solver::attach_bool_var(euf::enode* n) {
-        expr* e = n->get_owner();
-        if (m.is_bool(e)) {
-            sat::bool_var v = si.add_bool_var(e);
-            attach_lit(literal(v, false),  n);
-        }
-    }
-
-    void solver::attach_lit(literal lit, euf::enode* n) {
-        unsigned v = lit.index();
-        m_lit2node.reserve(v + 1, nullptr);
-        SASSERT(m_lit2node[v] == nullptr);
-        m_lit2node[v] = n;
-        m_lit_trail.push_back(v);
-    }
-
     bool solver::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
         for (auto* th : m_solvers) {            
             if (!th->to_formulas(l2e, fmls))

src/sat/smt/euf_solver.h

@@ -57,7 +57,7 @@ namespace euf {
             void reset() { memset(this, 0, sizeof(*this)); }
         };
         struct scope {
-            unsigned m_lit_lim;
+            unsigned m_var_lim;
             unsigned m_trail_lim;
         };
         typedef ptr_vector<trail<solver> > trail_stack;
@@ -79,12 +79,12 @@ namespace euf {
         sat::sat_internalizer* m_to_si;
         scoped_ptr<euf::ackerman>   m_ackerman;
 
-        ptr_vector<euf::enode>                          m_lit2node;
+        ptr_vector<euf::enode>                          m_var2node;
         ptr_vector<unsigned>                            m_explain;
         euf::enode_vector                               m_args;
         svector<sat::frame>                             m_stack;
         unsigned                                        m_num_scopes { 0 };
-        unsigned_vector                                 m_lit_trail;
+        unsigned_vector                                 m_var_trail;
         svector<scope>                                  m_scopes;
         scoped_ptr_vector<sat::th_solver>               m_solvers;
         ptr_vector<sat::th_solver>                      m_id2solver;
@@ -97,9 +97,14 @@ namespace euf {
         unsigned * base_ptr() { return reinterpret_cast<unsigned*>(this); }
 
         // internalization
+        bool m_is_redundant { false };
         euf::enode* visit(expr* e);
-        void attach_bool_var(euf::enode* n);
+        void attach_node(euf::enode* n);
         void attach_lit(sat::literal lit, euf::enode* n);
+        void add_distinct_axiom(app* e, euf::enode* const* args);
+        void add_not_distinct_axiom(app* e, euf::enode* const* args);
+        void axiomatize_basic(enode* n);
+        bool internalize_root(app* e, enode* const* args, bool sign);
         euf::enode* mk_true();
         euf::enode* mk_false();
 
@@ -199,7 +204,7 @@ namespace euf {
                         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;
 
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
-        sat::literal internalize(expr* e, bool sign, bool root) override;
+        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void update_model(model_ref& mdl);
 
         func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }

src/sat/smt/sat_smt.h

@@ -38,7 +38,7 @@ namespace sat {
     public:
         virtual ~sat_internalizer() {}
         virtual bool is_bool_op(expr* e) const = 0;
-        virtual literal internalize(expr* e) = 0;
+        virtual literal internalize(expr* e, bool learned) = 0;
         virtual bool_var add_bool_var(expr* e)  = 0;
         virtual void cache(app* t, literal l) = 0;
     };

src/sat/smt/sat_th.h

@@ -26,7 +26,7 @@ namespace sat {
     public:
         virtual ~th_internalizer() {}
 
-        virtual literal internalize(expr* e, bool sign, bool root) = 0;
+        virtual literal internalize(expr* e, bool sign, bool root, bool redundant) = 0;
     };
 
     class th_decompile {

src/sat/tactic/goal2sat.cpp

@@ -70,6 +70,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     bool                        m_default_external;
     bool                        m_xor_solver;
     bool                        m_euf;
+    bool                        m_is_redundant { false };
     sat::literal_vector         aig_lits;
     
     imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
@@ -93,7 +94,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_ite_extra  = p.get_bool("ite_extra", true);
         m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
         m_xor_solver = p.get_bool("xor_solver", false);
-        m_euf = false; // true;
+        m_euf = true; // false; // true;
     }
 
     void throw_op_not_handled(std::string const& s) {
@@ -103,22 +104,22 @@ struct goal2sat::imp : public sat::sat_internalizer {
     
     void mk_clause(sat::literal l) {
         TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
-        m_solver.add_clause(1, &l, false);
+        m_solver.add_clause(1, &l, m_is_redundant);
     }
 
     void mk_clause(sat::literal l1, sat::literal l2) {
         TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
-        m_solver.add_clause(l1, l2, false);
+        m_solver.add_clause(l1, l2, m_is_redundant);
     }
 
     void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
         TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
-        m_solver.add_clause(l1, l2, l3, false);
+        m_solver.add_clause(l1, l2, l3, m_is_redundant);
     }
 
     void mk_clause(unsigned num, sat::literal * lits) {
         TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
-        m_solver.add_clause(num, lits, false);
+        m_solver.add_clause(num, lits, m_is_redundant);
     }
 
     sat::literal mk_true() {
@@ -246,6 +247,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 return true;
             }
         case OP_DISTINCT: {
+            if (m_euf) {
+                convert_euf(t, root, sign);
+                return true;
+            }                
             TRACE("goal2sat_not_handled", tout << mk_ismt2_pp(t, m) << "\n";);
             std::ostringstream strm;
             strm << mk_ismt2_pp(t, m);
@@ -481,7 +486,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         euf::solver* euf = nullptr;
         if (!ext) {
             euf = alloc(euf::solver, m, m_map, *this);
-            std::cout << "set euf\n";
             m_solver.set_extension(euf);
             for (unsigned i = m_solver.num_scopes(); i-- > 0; )
                 euf->push();
@@ -491,7 +495,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
         if (!euf)
             throw default_exception("cannot convert to euf");
-        sat::literal lit = euf->internalize(e, sign, root);
+        sat::literal lit = euf->internalize(e, sign, root, m_is_redundant);
         if (root)
             m_result_stack.reset();
         if (lit == sat::null_literal)
@@ -516,7 +520,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
         if (!ba)
             throw default_exception("cannot convert to pb");
-        sat::literal lit = ba->internalize(t, sign, root);
+        sat::literal lit = ba->internalize(t, sign, root, m_is_redundant);
         if (root)
             m_result_stack.reset();
         else 
@@ -588,7 +592,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     };
 
-    void process(expr* n, bool is_root) {
+    void process(expr* n, bool is_root, bool redundant) {
+        flet<bool> _is_redundant(m_is_redundant, redundant);
         scoped_stack _sc(*this, is_root);
         unsigned sz = m_frame_stack.size();
         if (visit(n, is_root, false)) 
@@ -636,9 +641,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
-    sat::literal internalize(expr* n) override {
+    sat::literal internalize(expr* n, bool redundant) override {
         unsigned sz = m_result_stack.size();
-        process(n, false);
+        process(n, false, redundant);
         SASSERT(m_result_stack.size() == sz + 1);
         sat::literal result = m_result_stack.back();
         m_result_stack.pop_back();
@@ -674,7 +679,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     void process(expr * n) {
         m_result_stack.reset();
         TRACE("goal2sat", tout << mk_pp(n, m) << "\n";);
-        process(n, true);
+        process(n, true, m_is_redundant);
         CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
         SASSERT(m_result_stack.empty());
     }
@@ -782,7 +787,7 @@ struct unsupported_bool_proc {
       :blast-distinct true
 */
 bool goal2sat::has_unsupported_bool(goal const & g) {
-    return test<unsupported_bool_proc>(g);
+    return false && test<unsupported_bool_proc>(g);
 }
 
 goal2sat::goal2sat():