additional bit-vector propagators (#4695)

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/euf/euf_egraph.cpp

@@ -573,30 +573,30 @@ namespace euf {
 
     std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
         out << n->get_expr_id() << " := ";
-        if (!n->is_root()) 
-            out << "[" << n->get_root()->get_expr_id() << "] ";
         expr* f = n->get_expr();
         if (is_app(f))
-            out << mk_bounded_pp(f, m, 1);
+            out << mk_bounded_pp(f, m, 1) << " ";
         else if (is_quantifier(f))
-            out << "q:" << f->get_id();
+            out << "q:" << f->get_id() << " ";
         else
-            out << "v:" << f->get_id();
-        out << "\n";
+            out << "v:" << f->get_id() << " ";
+        if (!n->is_root()) 
+            out << "[r " << n->get_root()->get_expr_id() << "] ";
         if (!n->m_parents.empty()) {
-            out << "    parents ";
+            out << "[p";
             for (enode* p : enode_parents(n))
-                out << p->get_expr_id() << " ";
-            out << "\n";
+                out << " " << p->get_expr_id();
+            out << "] ";
         }
         if (n->has_th_vars()) {
-            out << "    theories ";
+            out << "[t";
             for (auto v : enode_th_vars(n))
-                out << v.get_id() << ":" << v.get_var() << " ";
-            out << "\n";
+                out << " " << v.get_id() << ":" << v.get_var();
+            out << "] ";
         }
         if (n->m_target && m_display_justification)
-            n->m_justification.display(out << "    = " << n->m_target->get_expr_id() << " j: ", m_display_justification) << "\n";
+            n->m_justification.display(out << "[j " << n->m_target->get_expr_id() << " ", m_display_justification) << "] ";
+        out << "\n";
         return out;
     }
 

src/sat/sat_probing.cpp

@@ -237,6 +237,7 @@ namespace sat {
         if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit)
             m_cached_bins.finalize();
 
+        flet<bool> _probing(m_active, true);
         report rpt(*this);
         bool r    = true;
         m_counter = 0;

src/sat/sat_probing.h

@@ -31,7 +31,7 @@ namespace sat {
         unsigned        m_stopped_at;  // where did it stop
         literal_set     m_assigned;    // literals assigned in the first branch
         literal_vector  m_to_assert;
-
+        bool            m_active { false };
         // counters
         int             m_counter;       // track cost
 
@@ -78,6 +78,7 @@ namespace sat {
 
         void collect_statistics(statistics & st) const;
         void reset_statistics();
+        bool active() const { return m_active; }
 
         // return the literals implied by l.
         // return 0, if the cache is not available

src/sat/sat_solver.cpp

@@ -1934,12 +1934,24 @@ namespace sat {
         }
         log_stats();
         m_simplifications++;
-        IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";);
 
         TRACE("sat", tout << "simplify\n";);
 
         pop(scope_lvl());
-
+        struct report {
+            solver&   s;
+            stopwatch m_watch;
+            report(solver& s):s(s) { 
+                m_watch.start(); 
+                s.log_stats();
+                IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << s.m_simplifications << ")\n";);
+            }
+            ~report() { 
+                m_watch.stop(); 
+                s.log_stats();
+            }
+        };
+        report _rprt(*this);
         SASSERT(at_base_lvl());
 
         m_cleaner(m_config.m_force_cleanup);
@@ -3943,9 +3955,8 @@ namespace sat {
             break;
         }
         case justification::EXT_JUSTIFICATION:
-            if (m_ext) {
-                m_ext->display_justification(out << " ", js.get_ext_justification_idx());
-            }
+            if (m_ext) 
+                m_ext->display_justification(out, js.get_ext_justification_idx());            
             break;
         default:
             break;

src/sat/sat_solver.h

@@ -662,6 +662,7 @@ namespace sat {
     public:
         void set_should_simplify() { m_next_simplify = m_conflicts_since_init; }
         bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit;  }
+        bool is_probing() const { return m_probing.active(); }
 
     public:
         void user_push() override;

src/sat/smt/bv_ackerman.cpp

@@ -110,7 +110,7 @@ namespace bv {
         }
 
         if (glue < max_glue) 
-            v.m_glue = 2*glue <= sz ? 0 : glue;
+            v.m_glue = (sz > 6 && 2*glue <= sz) ? 0 : glue;
     }
 
     void ackerman::remove(vv* p) {

src/sat/smt/bv_internalize.cpp

@@ -42,6 +42,16 @@ namespace bv {
         }
     };
 
+    class solver::add_eq_occurs_trail : public trail<euf::solver> {
+        solver::bit_atom* m_atom;
+    public:
+        add_eq_occurs_trail(solver::bit_atom* a) :m_atom(a) {}
+        void undo(euf::solver& euf) override {
+            SASSERT(m_atom->m_eqs);
+            m_atom->m_eqs = m_atom->m_eqs->m_next;
+        }
+    };    
+
     class solver::mk_atom_trail : public trail<euf::solver> {
         solver& th;
         sat::bool_var m_var;
@@ -242,31 +252,30 @@ namespace bv {
     }
 
     solver::bit_atom* solver::mk_bit_atom(sat::bool_var bv) {
-        bit_atom* b = new (get_region()) bit_atom();
-        insert_bv2a(bv, b);
-        ctx.push(mk_atom_trail(bv, *this));
-        return b;
+        atom* a = get_bv2a(bv);
+        if (a) 
+            return a->is_bit() ? &a->to_bit() : nullptr;
+        else {
+            bit_atom* b = new (get_region()) bit_atom();
+            insert_bv2a(bv, b);
+            ctx.push(mk_atom_trail(bv, *this));
+            return b;
+        }
     }
 
     void solver::set_bit_eh(theory_var v, literal l, unsigned idx) {
         SASSERT(m_bits[v][idx] == l);
         if (s().value(l) != l_undef && s().lvl(l) == 0) 
             register_true_false_bit(v, idx);
         else {
-            atom* a = get_bv2a(l.var());
-            if (a && !a->is_bit()) 
-                ;
-            else if (a) {
-                bit_atom* b = &a->to_bit();
-                find_new_diseq_axioms(*b, v, idx);
-                ctx.push(add_var_pos_trail(b));
+            bit_atom* b = mk_bit_atom(l.var());
+            if (b) {
+                if (b->m_occs)
+                    find_new_diseq_axioms(*b, v, idx);
+                if (!b->is_fresh()) 
+                    ctx.push(add_var_pos_trail(b));                
                 b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
             }
-            else {
-                bit_atom* b = mk_bit_atom(l.var());
-                SASSERT(!b->m_occs);
-                b->m_occs = new (get_region()) var_pos_occ(v, idx);
-            }
         }
     }
 
@@ -570,12 +579,34 @@ namespace bv {
         }
     }
 
+    void solver::eq_internalized(euf::enode* n) {
+        SASSERT(m.is_eq(n->get_expr()));
+        theory_var v1 = n->get_arg(0)->get_th_var(get_id());
+        theory_var v2 = n->get_arg(1)->get_th_var(get_id());
+        SASSERT(v1 != euf::null_theory_var);
+        SASSERT(v2 != euf::null_theory_var);
+        unsigned sz = m_bits[v1].size();
+        for (unsigned i = 0; i < sz; ++i) {
+            eq_internalized(m_bits[v1][i].var(), i, v1, v2, n);
+            eq_internalized(m_bits[v2][i].var(), i, v2, v1, n);
+        }
+    }
+
+    void solver::eq_internalized(sat::bool_var b, unsigned idx, theory_var v1, theory_var v2, euf::enode* n) {
+        bit_atom* a = mk_bit_atom(b);
+        if (a) {
+            if (!a->is_fresh()) 
+                ctx.push(add_eq_occurs_trail(a));
+            a->m_eqs = new (get_region()) eq_occurs(idx, v1, v2, n, a->m_eqs);
+        }
+    }
+
     void solver::assert_ackerman(theory_var v1, theory_var v2) {
         if (v1 == v2)
             return;
         if (v1 > v2)
             std::swap(v1, v2);
-        flet<bool> _red(m_is_redundant, true);        
+        flet<bool> _red(m_is_redundant, true);
         ++m_stats.m_ackerman;
         expr* o1 = var2expr(v1);
         expr* o2 = var2expr(v2);
@@ -584,6 +615,7 @@ namespace bv {
         unsigned sz = m_bits[v1].size();
         TRACE("bv", tout << "ackerman-eq: " << s().scope_lvl() << " " << oe << "\n";);
         literal_vector eqs;
+        eqs.push_back(oeq);
         for (unsigned i = 0; i < sz; ++i) {
             literal l1 = m_bits[v1][i];
             literal l2 = m_bits[v2][i];
@@ -592,14 +624,10 @@ namespace bv {
             e2 = bv.mk_bit2bool(o2, i);
             expr_ref e = mk_eq(e1, e2);
             literal eq = ctx.internalize(e, false, false, m_is_redundant);
-            add_clause(l1, ~l2, ~eq);
-            add_clause(~l1, l2, ~eq);
-            add_clause(l1, l2, eq);
-            add_clause(~l1, ~l2, eq);
             add_clause(eq, ~oeq);
             eqs.push_back(~eq);
         }
-        eqs.push_back(oeq);
+        TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);
         s().add_clause(eqs.size(), eqs.c_ptr(), sat::status::th(m_is_redundant, get_id()));
     }
 }

src/sat/smt/bv_invariant.cpp

@@ -16,6 +16,7 @@ Module Name:
 --*/
 
 #include "sat/smt/bv_solver.h"
+#include "sat/smt/euf_solver.h"
 
 namespace bv {
 
@@ -32,6 +33,27 @@ namespace bv {
         }
     }
 
+    void solver::check_missing_propagation() const {
+        for (euf::enode* n : ctx.get_egraph().nodes()) {
+            expr* e = n->get_expr(), *a = nullptr, *b = nullptr;
+            if (m.is_eq(e, a, b) && bv.is_bv(a) && s().value(expr2literal(e)) == l_undef) {
+                theory_var v1 = n->get_arg(0)->get_th_var(get_id());
+                theory_var v2 = n->get_arg(1)->get_th_var(get_id());
+                SASSERT(v1 != euf::null_theory_var);
+                SASSERT(v2 != euf::null_theory_var);
+                unsigned sz = m_bits[v1].size();
+                for (unsigned i = 0; i < sz; ++i) {
+                    lbool val1 = s().value(m_bits[v1][i]);
+                    lbool val2 = s().value(m_bits[v2][i]);
+                    if (val1 != l_undef && val2 != l_undef && val1 != val2) {
+                        IF_VERBOSE(0, verbose_stream() << "missing " << mk_bounded_pp(e, m) << "\n");
+                        break;
+                    }
+                }
+            }
+        }
+    }
+
     /**
         \brief Check whether m_zero_one_bits is an accurate summary of the bits in the
         equivalence class rooted by v.