fix missing equality propagation in new bv solver

src/sat/smt/bv_internalize.cpp

@@ -290,6 +290,10 @@ namespace bv {
         TRACE("bv", tout << "add-bit: v" << v << "[" << idx << "] " << l << " " << literal2expr(l) << "@" << s().scope_lvl() << "\n";);
         SASSERT(m_num_scopes == 0);
         s().set_external(l.var());
+        euf::enode* n = bool_var2enode(l.var());
+        if (!n->is_attached_to(get_id())) 
+            mk_var(n);
+
         set_bit_eh(v, l, idx);
     }
 
@@ -307,7 +311,7 @@ namespace bv {
         SASSERT(m_bits[v][idx] == l);
         if (s().value(l) != l_undef && s().lvl(l) == 0) 
             register_true_false_bit(v, idx);
-        else if (m_bits[v].size() > 1) {
+        else {
             atom* b = mk_atom(l.var());
             if (b->m_occs)
                 find_new_diseq_axioms(*b, v, idx);

src/sat/smt/bv_solver.cpp

@@ -74,7 +74,6 @@ namespace bv {
             is_bv(v2) &&
             m_bits[v2].size() == sz &&
             get_fixed_value(v2, val2) && val1 == val2;
-
         if (!is_current)
             m_fixed_var_table.insert(key, v1);
         else if (n1->get_root() != var2enode(v2)->get_root()) {
@@ -380,6 +379,7 @@ namespace bv {
     }
 
     void solver::asserted(literal l) {
+        
         atom* a = get_bv2a(l.var());
         TRACE("bv", tout << "asserted: " << l << "\n";);
         if (a) {
@@ -530,6 +530,7 @@ namespace bv {
     }
 
     bool solver::set_root(literal l, literal r) {
+        return false;
         atom* a = get_bv2a(l.var());
         if (!a)
             return true;
@@ -624,6 +625,16 @@ namespace bv {
         return out;
     }
 
+    std::ostream& solver::display(std::ostream& out, atom const& a) const {
+        out << a.m_bv << "\n";
+        for (auto vp : a) 
+            out << vp.first << "[" << vp.second << "]\n";
+        for (auto e : a.eqs())
+            out << e.m_bv1 << " " << e.m_bv2 << "\n";
+        return out;
+    }
+
+
     void solver::collect_statistics(statistics& st) const {
         st.update("bv conflicts", m_stats.m_num_conflicts);
         st.update("bv diseqs", m_stats.m_num_diseq_static);
@@ -680,6 +691,7 @@ namespace bv {
     void solver::init_use_list(sat::ext_use_list& ul) {}
     bool solver::is_blocked(literal l, sat::ext_constraint_idx) { return false; }
     bool solver::check_model(sat::model const& m) const { return true; }
+    void solver::finalize_model(model& mdl) {}
     unsigned solver::max_var(unsigned w) const { return w; }
 
     void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {

src/sat/smt/bv_solver.h

@@ -175,6 +175,7 @@ namespace bv {
             atom* m_atom{ nullptr };
             explicit propagation_item(atom* a) : m_atom(a) {}
             explicit propagation_item(var_pos const& vp) : m_vp(vp) {}            
+            bool operator==(propagation_item const& other) const { if (m_atom) return m_atom == other.m_atom; return false; }
         };
 
 
@@ -301,6 +302,8 @@ namespace bv {
         void check_missing_propagation() const;
         void validate_atoms() const;
         
+        std::ostream& display(std::ostream& out, atom const& a) const;
+       
     public:
         solver(euf::solver& ctx, theory_id id);
         ~solver() override {}
@@ -332,6 +335,7 @@ namespace bv {
         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;
+        void finalize_model(model& mdl) override;
         unsigned max_var(unsigned w) const override;
 
         void new_eq_eh(euf::th_eq const& eq) override;

src/sat/smt/euf_model.cpp

@@ -203,9 +203,11 @@ namespace euf {
             if (!m.is_bool(e))
                 continue;
             unsigned id = n->get_root_id();
+            if (!m_values.get(id))
+                continue;
             bool tt = m.is_true(m_values.get(id));
             if (mdl.is_true(e) != tt) {
-                IF_VERBOSE(0, verbose_stream() << "Failed to evaluate " << id << " " << mk_bounded_pp(e, m) << "\n");
+                IF_VERBOSE(0, verbose_stream() << "Failed to evaluate " << id << " " << mk_bounded_pp(e, m) << " " << mdl(e) << " " << mk_bounded_pp(m_values.get(id), m) << "\n");
             }
         }
         

src/sat/smt/euf_solver.h

@@ -81,16 +81,16 @@ namespace euf {
 
         ast_manager& m;
         sat::sat_internalizer& si;
-        smt_params            m_config;
+        smt_params             m_config;
-        euf::egraph           m_egraph;
+        euf::egraph            m_egraph;
-        euf_trail_stack       m_trail;
+        euf_trail_stack        m_trail;
-        stats                 m_stats;
+        stats                  m_stats;
-        th_rewriter           m_rewriter;
+        th_rewriter            m_rewriter;
-        func_decl_ref_vector  m_unhandled_functions;
+        func_decl_ref_vector   m_unhandled_functions;
-        sat::lookahead*       m_lookahead{ nullptr };
+        sat::lookahead*        m_lookahead{ nullptr };
         ast_manager*           m_to_m;
         sat::sat_internalizer* m_to_si;
-        scoped_ptr<euf::ackerman>   m_ackerman;
+        scoped_ptr<euf::ackerman>    m_ackerman;
         scoped_ptr<sat::dual_solver> m_dual_solver;
         user::solver*          m_user_propagator{ nullptr };
         th_solver*             m_qsolver { nullptr };