include disequality expansion for non-unit case.

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

src/ast/rewriter/bit_blaster/bit_blaster.cpp

@@ -28,7 +28,7 @@ bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool
     m_rw(rw) {
 }
 
-static void sort_args(expr * & l1, expr * & l2, expr * & l3) {
+void bit_blaster_cfg::sort_args(expr * & l1, expr * & l2, expr * & l3) {
     expr * args[3] = {l1, l2, l3};
     // ast_lt_proc is based on the AST ids. So, it is a total order on AST nodes.
     // No need for stable_sort
@@ -41,7 +41,7 @@ void bit_blaster_cfg::mk_xor3(expr * l1, expr * l2, expr * l3, expr_ref & r) {
     TRACE("xor3", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id(););
     sort_args(l1, l2, l3);
     TRACE("xor3_sorted", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id(););
-    if (m_params.m_bb_ext_gates) {
+    if (m_ext_gates || m_params.m_bb_ext_gates) {
         if (l1 == l2)
             r = l3;
         else if (l1 == l3)
@@ -80,7 +80,7 @@ void bit_blaster_cfg::mk_carry(expr * l1, expr * l2, expr * l3, expr_ref & r) {
     TRACE("carry", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id(););
     sort_args(l1, l2, l3);
     TRACE("carry_sorted", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id(););
-    if (m_params.m_bb_ext_gates) {
+    if (m_ext_gates || m_params.m_bb_ext_gates) {
         if ((m().is_false(l1) && m().is_false(l2)) ||
             (m().is_false(l1) && m().is_false(l3)) ||
             (m().is_false(l2) && m().is_false(l3)))

src/ast/rewriter/bit_blaster/bit_blaster.h

@@ -31,35 +31,39 @@ protected:
     bv_util                  &  m_util;
     bit_blaster_params const &  m_params;
     bool_rewriter            &  m_rw;
+    bool                        m_ext_gates = false;
+    void sort(expr*& a, expr*& b) { if (a->get_id() > b->get_id()) std::swap(a, b); }
+    void sort_args(expr*& l1, expr*& l2, expr*& l3);
 public:
     bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw);
 
     ast_manager & m() const { return m_util.get_manager(); }
     numeral power(unsigned n) const { return rational::power_of_two(n); }
-    void mk_xor(expr * a, expr * b, expr_ref & r) { m_rw.mk_xor(a, b, r); }
+    void mk_xor(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_xor(a, b, r); }
     void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r);
     void mk_carry(expr * a, expr * b, expr * c, expr_ref & r);
-    void mk_iff(expr * a, expr * b, expr_ref & r) { m_rw.mk_iff(a, b, r); }
+    void mk_iff(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_iff(a, b, r); }
-    void mk_and(expr * a, expr * b, expr_ref & r) { m_rw.mk_and(a, b, r); }
+    void mk_and(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_and(a, b, r); }
-    void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_and(a, b, c, r); }
+    void mk_and(expr* a, expr* b, expr* c, expr_ref& r) { sort_args(a, b, c); m_rw.mk_and(a, b, c, r); }
     void mk_and(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_and(sz, args, r); }
     void mk_ge2(expr* a, expr* b, expr* c, expr_ref& r) { m_rw.mk_ge2(a, b, c, r); }
-    void mk_or(expr * a, expr * b, expr_ref & r) { m_rw.mk_or(a, b, r); }
+    void mk_or(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_or(a, b, r); }
-    void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_or(a, b, c, r); }
+    void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { sort_args(a, b, c); m_rw.mk_or(a, b, c, r); }
     void mk_or(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_or(sz, args, r); }
     void mk_not(expr * a, expr_ref & r) { m_rw.mk_not(a, r); }
     void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rw.mk_ite(c, t, e, r); }
-    void mk_nand(expr * a, expr * b, expr_ref & r) { m_rw.mk_nand(a, b, r); }
+    void mk_nand(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_nand(a, b, r); }
-    void mk_nor(expr * a, expr * b, expr_ref & r) { m_rw.mk_nor(a, b, r); }
+    void mk_nor(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_nor(a, b, r); }
 };
 
-class bit_blaster : public bit_blaster_tpl<bit_blaster_cfg> {
+class bit_blaster : public bit_blaster_tpl<bit_blaster_cfg> {    
     bv_util                 m_util;
     bool_rewriter           m_rw;
 public:
     bit_blaster(ast_manager & m, bit_blaster_params const & params);
     bit_blaster_params const & get_params() const { return this->m_params; }
     void set_flat_and_or(bool f) { m_rw.set_flat_and_or(f); }
+    void set_ext_gates(bool f) { m_ext_gates = f; }
 };
 
 

src/sat/smt/bv_solver.cpp

@@ -56,6 +56,7 @@ namespace bv {
         m_bb(m, get_config()),
         m_find(*this) {
         m_bb.set_flat_and_or(false);
+        m_bb.set_ext_gates(true);
     }
 
     bool solver::is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) {
@@ -267,7 +268,7 @@ namespace bv {
                 ++num_undef;
                 undef_idx = -static_cast<int>(i + 1);
             }
-            if (num_undef > 1)
+            if (num_undef > 1 && false)
                 return;
         }
         if (num_undef == 0)
@@ -533,12 +534,10 @@ namespace bv {
     }
 
     bool solver::unit_propagate() {
-        if (m_prop_queue_head == m_prop_queue.size())
+        if (m_prop_queue.empty())
             return false;
-        force_push();
+        for (unsigned i = 0; i < m_prop_queue.size() && !s().inconsistent(); ++i) {
-        ctx.push(value_trail<unsigned>(m_prop_queue_head));
+            auto const p = m_prop_queue[i];
-        for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
-            auto const p = m_prop_queue[m_prop_queue_head];
             if (p.m_atom) {
                 for (auto vp : *p.m_atom)
                     propagate_bits(vp);
@@ -548,6 +547,7 @@ namespace bv {
             else 
                 propagate_bits(p.m_vp);            
         }
+        m_prop_queue.reset();
         // check_missing_propagation();
         return true;
     }
@@ -587,6 +587,8 @@ namespace bv {
         if (m_wpos[v1] == idx)
             find_wpos(v1);
 
+        bool is_fixed = s().value(m_bits[v1][m_wpos[v1]]) != l_undef;
+
         literal bit1 = m_bits[v1][idx];
         lbool   val = s().value(bit1);
         TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_expr_id() << "[" << idx << "] = " << val << "\n";);
@@ -613,7 +615,7 @@ namespace bv {
             if (!assign_bit(bit2, v1, v2, idx, bit1, false))
                 break;
         }
-        if (s().value(m_bits[v1][m_wpos[v1]]) != l_undef)
+        if (!is_fixed && s().value(m_bits[v1][m_wpos[v1]]) != l_undef)
             find_wpos(v1);
 
         return num_assigned > 0;
@@ -626,7 +628,7 @@ namespace bv {
     */
     sat::check_result solver::check() {
         force_push();
-        SASSERT(m_prop_queue.size() == m_prop_queue_head);
+        SASSERT(m_prop_queue.empty());
         bool ok = true;
         svector<std::pair<expr*, internalize_mode>> delay;
         for (auto kv : m_delay_internalize)
@@ -651,22 +653,19 @@ namespace bv {
     }
 
     void solver::push_core() {
-        TRACE("bv", tout << "push: " << get_num_vars() << "@" << m_prop_queue_lim.size() << "\n";);
+        TRACE("bv", tout << "push: " << get_num_vars() << "@" << m_prop_queue.size() << "\n";);
         th_euf_solver::push_core();
-        m_prop_queue_lim.push_back(m_prop_queue.size());
     }
 
     void solver::pop_core(unsigned n) {
         SASSERT(m_num_scopes == 0);
-        unsigned old_sz = m_prop_queue_lim.size() - n;
-        m_prop_queue.shrink(m_prop_queue_lim[old_sz]);
-        m_prop_queue_lim.shrink(old_sz);
         th_euf_solver::pop_core(n);
-        old_sz = get_num_vars();        
+        unsigned old_sz = get_num_vars();        
         m_bits.shrink(old_sz);
         m_wpos.shrink(old_sz);
         m_zero_one_bits.shrink(old_sz);
-        TRACE("bv", tout << "num vars " << old_sz << "@" << m_prop_queue_lim.size() << "\n";);
+        m_prop_queue.reset();
+        TRACE("bv", tout << "num vars " << old_sz << "\n";);
     }
 
     void solver::simplify() {
@@ -886,12 +885,14 @@ namespace bv {
 
     void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
 
+
         TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";);
 
         if (!merge_zero_one_bits(r1, r2)) {
             TRACE("bv", tout << "conflict detected\n";);
             return; // conflict was detected
         }
+        m_prop_queue.reset();
         SASSERT(m_bits[v1].size() == m_bits[v2].size());
         unsigned sz = m_bits[v1].size();
         if (sz == 1)
@@ -982,8 +983,9 @@ namespace bv {
             force_push();
             if (a)
                 for (auto curr : *a)
-                    if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx) 
+                    if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx) {
-                        m_prop_queue.push_back(propagation_item(curr));  
+                        m_prop_queue.push_back(propagation_item(curr));
+                    }
             return true;
         }
     }

src/sat/smt/bv_solver.h

@@ -234,8 +234,6 @@ namespace bv {
         mutable vector<rational>   m_power2;
         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;
         euf::enode_vector          m_bv2ints;
         obj_map<app, lazy_mul*>   m_lazymul;

src/sat/smt/euf_internalize.cpp

@@ -155,9 +155,7 @@ namespace euf {
         if (lit.sign()) {
             v = si.add_bool_var(e);
             s().set_external(v);
-            s().set_eliminated(v, false);
+            s().set_eliminated(v, false);            
-            set_bool_var2expr(v, e);
-            m_var_trail.push_back(v);
             sat::literal lit2 = literal(v, false);
             th_proof_hint* ph1 = nullptr, * ph2 = nullptr;
             if (use_drat()) {
@@ -185,7 +183,6 @@ namespace euf {
             return lit;
         }
 
-
         set_bool_var2expr(v, e);      
         enode* n = m_egraph.find(e);
         if (!n)