na

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

src/sat/smt/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(sat_smt
     atom2bool_var.cpp
     ba_internalize.cpp
     ba_solver.cpp
+    bv_internalize.cpp
     xor_solver.cpp
     euf_ackerman.cpp
     euf_internalize.cpp

src/sat/smt/ba_solver.cpp

@@ -360,7 +360,7 @@ namespace sat {
         }
         if (p.k() == 1 && p.lit() == null_literal) {
             literal_vector lits(p.literals());
-            s().mk_clause(lits.size(), lits.c_ptr(), status::ba(p.learned()));
+            s().mk_clause(lits.size(), lits.c_ptr(), status::th(p.learned(), get_id()));
             IF_VERBOSE(100, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
             remove_constraint(p, "implies clause");
         }
@@ -412,7 +412,7 @@ namespace sat {
 
             if (k == 1 && p.lit() == null_literal) {
                 literal_vector lits(sz, p.literals().c_ptr());
-                s().mk_clause(sz, lits.c_ptr(), status::ba(p.learned()));
+                s().mk_clause(sz, lits.c_ptr(), status::th(p.learned(), get_id()));
                 remove_constraint(p, "is clause");
                 return;
             }
@@ -795,7 +795,7 @@ namespace sat {
 
         else if (k == 1 && p.lit() == null_literal) {
             literal_vector lits(sz, p.literals().c_ptr());
-            s().mk_clause(sz, lits.c_ptr(), status::ba(p.learned()));
+            s().mk_clause(sz, lits.c_ptr(), status::th(p.learned(), get_id()));
             remove_constraint(p, "recompiled to clause");
             return;
         }
@@ -1598,7 +1598,7 @@ namespace sat {
         TRACE("ba", tout << m_lemma << "\n";);
 
         if (get_config().m_drat && m_solver) {
-            s().m_drat.add(m_lemma, sat::status::ba(true));
+            s().m_drat.add(m_lemma, sat::status::th(true, get_id()));
         }
 
         s().m_lemma.reset();
@@ -1750,7 +1750,7 @@ namespace sat {
     ba_solver::constraint* ba_solver::add_at_least(literal lit, literal_vector const& lits, unsigned k, bool learned) {
         if (k == 1 && lit == null_literal) {
             literal_vector _lits(lits);
-            s().mk_clause(_lits.size(), _lits.c_ptr(), status::ba(learned));
+            s().mk_clause(_lits.size(), _lits.c_ptr(), status::th(learned, get_id()));
             return nullptr;
         }
         if (!learned && clausify(lit, lits.size(), lits.c_ptr(), k)) {
@@ -2140,7 +2140,7 @@ namespace sat {
             for (literal lit : r) 
                 lits.push_back(~lit);
             lits.push_back(l);
-            s().m_drat.add(lits, sat::status::ba(true));
+            s().m_drat.add(lits, sat::status::th(true, get_id()));
         }
     }
 
@@ -2899,7 +2899,7 @@ namespace sat {
 
         if (k == 1 && c.lit() == null_literal) {
             literal_vector lits(sz, c.literals().c_ptr());
-            s().mk_clause(sz, lits.c_ptr(), sat::status::ba(c.learned()));
+            s().mk_clause(sz, lits.c_ptr(), sat::status::th(c.learned(), get_id()));
             remove_constraint(c, "recompiled to clause");
             return;
         }
@@ -2907,27 +2907,27 @@ namespace sat {
         if (sz == 0) {
             if (c.lit() == null_literal) {
                 if (k > 0) {
-                    s().mk_clause(0, nullptr, status::ba_asserted());
+                    s().mk_clause(0, nullptr, status::th(false, get_id()));
                 }
             }
             else if (k > 0) {
                 literal lit = ~c.lit();
-                s().mk_clause(1, &lit, status::ba(c.learned()));
+                s().mk_clause(1, &lit, status::th(c.learned(), get_id()));
             }
             else {
                 literal lit = c.lit();
-                s().mk_clause(1, &lit, status::ba(c.learned()));
+                s().mk_clause(1, &lit, status::th(c.learned(), get_id()));
             }
             remove_constraint(c, "recompiled to clause");
             return;
         }
         if (all_units && sz < k) {
             if (c.lit() == null_literal) {
-                s().mk_clause(0, nullptr, status::ba(c.learned()));
+                s().mk_clause(0, nullptr, status::th(c.learned(), get_id()));
             }
             else {
                 literal lit = ~c.lit();
-                s().mk_clause(1, &lit, status::ba(c.learned()));
+                s().mk_clause(1, &lit, status::th(c.learned(), get_id()));
             }
             remove_constraint(c, "recompiled to clause");
             return;            

src/sat/smt/bv_internalize.cpp

@@ -0,0 +1,75 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    bv_internalize.cpp
+
+Abstract:
+
+    Internalize utilities for bit-vector solver plugin.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-30
+
+--*/
+
+#include "sat/smt/bv_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/sat_th.h"
+#include "tactic/tactic_exception.h"
+
+namespace bv {
+
+    euf::theory_var solver::mk_var(euf::enode* n) {
+        theory_var r  = euf::th_euf_solver::mk_var(n);
+        m_find.mk_var();
+        m_bits.push_back(sat::literal_vector());
+        m_wpos.push_back(0);
+        m_zero_one_bits.push_back(zero_one_bits());        
+        ctx.attach_th_var(n, this, r);
+        return r;
+    }
+
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
+        flet<bool> _is_learned(m_is_redundant, learned);
+        sat::scoped_stack _sc(m_stack);
+        unsigned sz = m_stack.size();
+        visit(e);
+        while (m_stack.size() > sz) {
+        loop:
+            if (!m.inc())
+                throw tactic_exception(m.limit().get_cancel_msg());
+            sat::eframe & fr = m_stack.back();
+            expr* e = fr.m_e;
+            if (visited(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++;
+                visit(arg);
+                if (!visited(arg))
+                    goto loop;
+            }
+            visit(e);
+            SASSERT(visited(e));
+            m_stack.pop_back();
+        }        
+        SASSERT(visited(e));
+        return sat::null_literal;
+    }
+
+    bool solver::visit(expr* e) {
+        return false;
+    }
+
+    bool solver::visited(expr* e) {
+        return false;
+    }
+
+}

src/sat/smt/bv_solver.h

@@ -0,0 +1,147 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    bv_solver.h
+
+Abstract:
+
+    Theory plugin for bit-vectors
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-30
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_th.h"
+
+namespace bv {
+
+    class solver : public euf::th_euf_solver {
+        typedef rational numeral;
+        typedef euf::theory_var theory_var;
+        typedef euf::theory_id theory_id;
+        typedef sat::literal literal;
+        typedef sat::bool_var bool_var;
+        typedef sat::literal_vector literal_vector;
+        typedef svector<euf::theory_var> vars;
+        typedef std::pair<numeral, unsigned> value_sort_pair;
+        typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
+        typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
+        typedef union_find<solver>  th_union_find;
+
+        /**
+           \brief Structure used to store the position of a bitvector variable that
+           contains the true_literal/false_literal.
+           
+           Remark: the implementation assumes that bitvector variables containing
+           complementary bits are never merged. I assert a disequality (not (= x y))
+           whenever x and y contain complementary bits. However, this is too expensive
+           when the bit is the true_literal or false_literal. The number of disequalities
+           is too big. To avoid this problem, each equivalence class has a set
+           of its true_literal and false_literal bits in the form of svector<zero_one_bit>.
+           
+           Before merging two classes we just check if the merge is valid by traversing these
+           vectors.
+        */
+        struct zero_one_bit {
+            theory_var m_owner;    //!< variable that owns the bit: useful for backtracking
+            unsigned   m_idx:31;
+            unsigned   m_is_true:1;
+            zero_one_bit(theory_var v = euf::null_theory_var, unsigned idx = UINT_MAX, bool is_true = false):
+                m_owner(v), m_idx(idx), m_is_true(is_true) {}
+        };
+
+        typedef svector<zero_one_bit> zero_one_bits;
+
+        class atom {
+        public:
+            virtual ~atom() {}
+            virtual bool is_bit() const = 0;
+        };
+
+        struct var_pos_occ {
+            theory_var    m_var;
+            unsigned      m_idx;
+            var_pos_occ * m_next;
+            var_pos_occ(theory_var v = euf::null_theory_var, unsigned idx = 0, var_pos_occ * next = nullptr):m_var(v), m_idx(idx), m_next(next) {}
+        };
+
+        struct bit_atom : public atom {
+            var_pos_occ * m_occs;
+            bit_atom():m_occs(nullptr) {}
+            ~bit_atom() override {}
+            bool is_bit() const override { return true; }
+        };
+
+        struct le_atom : public atom {
+            literal    m_var;
+            literal    m_def;
+            le_atom(literal v, literal d):m_var(v), m_def(d) {}
+            ~le_atom() override {}
+            bool is_bit() const override { return false; }
+        };
+
+        euf::solver&             ctx;
+        bv_util                  m_util;
+        arith_util               m_autil;
+//        bit_blaster              m_bb;
+        th_union_find            m_find;
+        vector<literal_vector>   m_bits;     // per var, the bits of a given variable.
+        ptr_vector<expr>         m_bits_expr;
+        svector<unsigned>        m_wpos;     // per var, watch position for fixed variable detection. 
+        vector<zero_one_bits>    m_zero_one_bits; // per var, see comment in the struct zero_one_bit
+//        bool_var2atom            m_bool_var2atom;
+        sat::solver* m_solver;
+        svector<sat::eframe>     m_stack;
+        bool                     m_is_redundant{ false };
+
+        bool visit(expr* e);
+        bool visited(expr* e);
+    public:
+        solver(euf::solver& ctx);
+        ~solver() override {}
+        void set_solver(sat::solver* s) override { m_solver = s; }
+        void set_lookahead(sat::lookahead* s) override { }
+        void init_search() override {}
+        double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;
+        bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override;
+        bool is_external(bool_var v) override;
+        bool propagate(literal l, sat::ext_constraint_idx idx) override;
+        void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r) override;
+        void asserted(literal l) override;
+        sat::check_result check() override;
+        void push() override;
+        void pop(unsigned n) override;
+        void pre_simplify() override;
+        void simplify() override;
+        void clauses_modifed() override;
+        lbool get_phase(bool_var v) 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;
+        void collect_statistics(statistics& st) const override;
+        extension* copy(sat::solver* s) override;       
+        void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}
+        void gc() override {}
+        void pop_reinit() override;
+        bool validate() override;
+        void init_use_list(sat::ext_use_list& ul) override;
+        bool is_blocked(literal l, sat::ext_constraint_idx) override;
+        bool check_model(sat::model const& m) const override;
+        unsigned max_var(unsigned w) const override;
+
+        bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
+                        std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override { return false; }
+
+        bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override { return false; }
+        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
+        euf::theory_var mk_var(euf::enode* n) override;
+
+    };
+
+
+}

src/sat/smt/euf_ackerman.cpp

@@ -194,7 +194,7 @@ namespace euf {
         }
         expr_ref eq(m.mk_eq(a, b), m);
         lits.push_back(s.internalize(eq, false, false, true));
-        s.s().mk_clause(lits, sat::status::euf(true));
+        s.s().mk_clause(lits, sat::status::th(true, m.get_basic_family_id()));
     }
 
     void ackerman::add_eq(expr* a, expr* b, expr* c) {
@@ -205,6 +205,6 @@ namespace euf {
         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, sat::status::euf(true));
+        s.s().mk_clause(3, lits, sat::status::th(true, m.get_basic_family_id()));
     }
 }

src/sat/smt/euf_internalize.cpp

@@ -103,8 +103,8 @@ namespace euf {
         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, sat::status::euf(false));
-            s().mk_clause(lit, ~lit2, sat::status::euf(false));
+            s().mk_clause(~lit, lit2, sat::status::th(false, m.get_basic_family_id()));
+            s().mk_clause(lit, ~lit2, sat::status::th(false, m.get_basic_family_id()));
             lit = lit2;
         }
         sat::bool_var v = lit.var();
@@ -132,7 +132,7 @@ namespace euf {
         if (sz <= 1)
             return;
 
-        sat::status st = sat::status::euf(m_is_redundant);
+        sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
         static const unsigned distinct_max_args = 32;
         if (sz <= distinct_max_args) {
             sat::literal_vector lits;
@@ -175,7 +175,7 @@ namespace euf {
         SASSERT(m.is_distinct(e));
         static const unsigned distinct_max_args = 32;
         unsigned sz = e->get_num_args();
-        sat::status st = sat::status::euf(m_is_redundant);
+        sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
         if (sz <= 1) {
             s().mk_clause(0, nullptr, st);
             return;
@@ -209,7 +209,7 @@ namespace euf {
 
     void solver::axiomatize_basic(enode* n) {
         expr* e = n->get_owner();
-        sat::status st = sat::status::euf(m_is_redundant);
+        sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
         if (m.is_ite(e)) {        
             app* a = to_app(e);
             expr* c = a->get_arg(0);

src/sat/smt/euf_proof.cpp

@@ -49,7 +49,7 @@ namespace euf {
             for (literal lit : r) lits.push_back(~lit);
             if (l != sat::null_literal)
                 lits.push_back(l);
-            s().get_drat().add(lits, sat::status::euf(true));
+            s().get_drat().add(lits, sat::status::th(true, m.get_basic_family_id()));
         }
     }
 

src/sat/smt/euf_solver.cpp

@@ -27,6 +27,8 @@ namespace euf {
     void solver::updt_params(params_ref const& p) {
         m_config.updt_params(p);
         m_drat = m_solver && m_solver->get_config().m_drat;
+        if (m_drat) 
+            m_solver->get_drat().add_theory(m.get_basic_family_id(), symbol("euf"));
     }
 
     /**
@@ -59,6 +61,8 @@ namespace euf {
         pb_util pb(m);
         if (pb.get_family_id() == fid) {
             ext = alloc(sat::ba_solver, *this, fid);
+            if (m_drat)
+                m_solver->get_drat().add_theory(fid, symbol("ba"));
         }
         if (ext) {
             ext->set_solver(m_solver);

src/sat/smt/euf_solver.h

@@ -219,6 +219,8 @@ namespace euf {
 
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
+        void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()); }
+
         void update_model(model_ref& mdl);
 
         func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }       

src/sat/smt/sat_th.h

@@ -84,7 +84,6 @@ namespace euf {
         */
         virtual bool is_shared(theory_var v) const { return false; }
 
-
     };
 
     class th_euf_solver : public th_solver {