misc bugfixes

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

src/ast/euf/euf_bv_plugin.cpp

@@ -485,6 +485,7 @@ namespace euf {
             if (n->get_root() == b->get_root() && offs == offset) {
                 while (j != UINT_MAX) {
                     auto [x, y, j2] = just[j];
+                    if (x != y)
                         consumer(x, y);
                     j = j2;
                 }

src/sat/smt/polysat/core.cpp

@@ -41,15 +41,6 @@ namespace polysat {
         void undo() {
             c.m_justification[m_var] = null_dependency;
             c.m_assignment.pop();
-        }
-    };
-
-    class core::mk_dqueue_var : public trail {
-        pvar m_var;
-        core& c;
-    public:
-        mk_dqueue_var(pvar v, core& c) : m_var(v), c(c) {}
-        void undo() {
             c.m_var_queue.unassign_var_eh(m_var);
         }
     };
@@ -171,12 +162,13 @@ namespace polysat {
     sat::check_result core::check() {
         if (m_var_queue.empty())
             return final_check();
-        m_var = m_var_queue.next_var();
+        m_var = m_var_queue.min_var();
-        s.trail().push(mk_dqueue_var(m_var, *this));
+        CTRACE("bv", is_assigned(m_var), display(tout << "v" << m_var << " is assigned\n"););
+        SASSERT(!is_assigned(m_var));
         
         switch (m_viable.find_viable(m_var, m_value)) {
         case find_t::empty:
-            TRACE("bv", tout << "check-conflict v" << m_var << "\n");
+            TRACE("bv", tout << "viable-conflict v" << m_var << "\n");
             s.set_conflict(m_viable.explain(), "viable-conflict");      
             return sat::check_result::CR_CONTINUE;
         case find_t::singleton: {
@@ -186,20 +178,21 @@ namespace polysat {
             return sat::check_result::CR_CONTINUE;
         }
         case find_t::multiple: {
-            TRACE("bv", tout << "check-multiple v" << m_var << " := " << m_value << "\n");
+            
             do {
+                try_again:
                 dependency d = null_dependency;
                 lbool value = s.add_eq_literal(m_var, m_value, d);
+                TRACE("bv", tout << "check-multiple v" << m_var << " := " << m_value << " " << value << "\n");
                 switch (value) {
                 case l_true:
                     propagate_assignment(m_var, m_value, d);
                     break;
                 case l_false:                    
                     m_value = mod(m_value + 1, rational::power_of_two(size(m_var)));
-                    continue;
+                    goto try_again;
                 default:
                     // let core assign equality.                    
-                    m_var_queue.unassign_var_eh(m_var);
                     break;
                 }
             } 
@@ -208,7 +201,6 @@ namespace polysat {
         }
         case find_t::resource_out:
             TRACE("bv", tout << "check-resource out v" << m_var << "\n");
-            m_var_queue.unassign_var_eh(m_var);
             return sat::check_result::CR_GIVEUP;
         }
         UNREACHABLE();
@@ -232,7 +224,7 @@ namespace polysat {
             auto vars = find_conflict_variables(idx);
             saturation sat(*this);
             for (auto v : vars)
-                if (sat.resolve(v, conflict_idx))
+                if (sat.resolve(v, idx))
                     return sat::check_result::CR_CONTINUE;
         }
 
@@ -288,26 +280,39 @@ namespace polysat {
         if (sc.is_eq(m_var, m_value))
             propagate_assignment(m_var, m_value, dep);
         else
-            sc.activate(*this, dep);        
+            propagate_activation(idx, sc, dep);
     }
 
     void core::add_watch(unsigned idx, unsigned var) {
         m_watch[var].push_back(idx);
     }
 
+    void core::propagate_activation(constraint_id idx, signed_constraint& sc, dependency dep) {
+        sc.activate(*this, dep);
+        pvar v = null_var;
+        for (auto w : sc.vars()) {
+            if (is_assigned(w))
+                continue;
+            if (v != null_var)
+                return;
+            v = w;
+        }
+        if (v != null_var)
+            verbose_stream() << "propagate activation " << v << " " << sc << " " << dep << "\n";
+        if (v != null_var && !m_viable.add_unitary(v, idx.id))
+            s.set_conflict(m_viable.explain(), "viable-conflict");
+    }
+
     void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
         TRACE("bv", tout << "propagate assignment v" << v << " := " << value << " " << is_assigned(v) << "\n");
         if (is_assigned(v))
             return;
-        if (m_var_queue.contains(v)) {
-            m_var_queue.del_var_eh(v);
-            s.trail().push(mk_dqueue_var(v, *this));
-        }
         
         m_values[v] = value;
         m_justification[v] = dep;   
         m_assignment.push(v , value);
         s.trail().push(mk_assign_var(v, *this));
+        m_var_queue.del_var_eh(v);
 
         // update the watch lists for pvars
         // remove constraints from m_watch[v] that have more than 2 free variables.
@@ -347,8 +352,8 @@ namespace polysat {
             if (!is_assigned(v0) || is_assigned(v1))
                 continue;
             // detect unitary, add to viable, detect conflict?
-            if (value != l_undef)
+            if (value != l_undef && !m_viable.add_unitary(v1, idx))
-                m_viable.add_unitary(v1, idx);            
+                s.set_conflict(m_viable.explain(), "viable-conflict");
         }
         SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");
         m_watch[v].shrink(j);
@@ -459,10 +464,10 @@ namespace polysat {
         out << "polysat:\n";
         for (auto const& [sc, d, value] : m_constraint_index) 
             out << sc << " " << d << " := " << value << "\n";        
-        for (unsigned i = 0; i < m_vars.size(); ++i) {
+        for (unsigned i = 0; i < m_vars.size(); ++i) 
             out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n";        
-        }
+        m_var_queue.display(out << "var queue: ") << "\n";
-        m_var_queue.display(out << "vars ") << "\n";
+        m_viable.display(out);
         return out;
     }
 

src/sat/smt/polysat/core.h

@@ -81,6 +81,7 @@ namespace polysat {
         void propagate_assignment(constraint_id idx);
         void propagate_eval(constraint_id idx);
         void propagate_assignment(pvar v, rational const& value, dependency dep);
+        void propagate_activation(constraint_id idx, signed_constraint& sc, dependency dep);
         void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
 
         void add_watch(unsigned idx, unsigned var);

src/sat/smt/polysat/fixed_bits.cpp

@@ -17,6 +17,13 @@ Author:
 
 namespace polysat {
 
+    void fixed_bits::reset() {
+        m_fixed_slices.reset();
+        m_var = null_var;
+        m_fixed.reset();
+        m_bits.reset();
+    }
+
     // reset with fixed bits information for variable v
     void fixed_bits::reset(pvar v) {
         m_fixed_slices.reset();
@@ -80,6 +87,9 @@ namespace polysat {
                     break;
                 }
             }
+
+
+            CTRACE("bv", i == sz, display(tout << "overflow\n"));
             // overflow
             if (i == sz)
                 return false;
@@ -98,6 +108,10 @@ namespace polysat {
         return result;
     }
 
+    std::ostream& fixed_bits::display(std::ostream& out) const {
+        return out << "fixed bits: v" << m_var << " " << m_fixed << "\n";
+    }
+
     /**
      * 2^k * x = 2^k * b
      * ==> x[N-k-1:0] = b[N-k-1:0]

src/sat/smt/polysat/fixed_bits.h

@@ -37,6 +37,9 @@ namespace polysat {
     public:
         fixed_bits(core& c) : c(c) {}
 
+        // reset without variable reference.
+        void reset();
+
         // reset with fixed bits information for variable v
         void reset(pvar v);
 
@@ -45,5 +48,7 @@ namespace polysat {
 
         // explain the fixed bits ranges.
         dependency_vector explain();
+
+        std::ostream& display(std::ostream& out) const;
     };
 }

src/sat/smt/polysat/ule_constraint.cpp

@@ -142,33 +142,33 @@ namespace polysat {
         }
 
         if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) {
-            LOG("-p + k <= k      -->  p <= k");
+            TRACE("bv", tout << "- p + k <= k-->  p <= k\n");
             lhs = rhs - lhs;
         }
 
         if (lhs.is_val() && !lhs.is_zero() && lhs.val() == rhs.offset()) {
-            LOG("k <= p + k       -->  p <= -k-1");
+            TRACE("bv", tout << "k <= p + k       -->  p <= -k-1\n");
             pdd k = lhs;
             lhs = rhs - lhs;
             rhs = -k - 1;
         }
 
         if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) {
-            LOG("k <= -p          -->  p-1 <= -k-1");
+            TRACE("bv", tout << "k <= -p-->  p - 1 <= -k - 1\n");
             pdd k = lhs;
             lhs = -(rhs + 1);
             rhs = -k - 1;
         }
 
         if (rhs.is_val() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) {
-            LOG("-p <= k          -->  -k-1 <= p-1");
+            TRACE("bv", tout << "-p <= k          -->  -k-1 <= p-1\n");
             pdd k = rhs;
             rhs = -(lhs + 1);
             lhs = -k - 1;
         }
 
         if (rhs.is_zero() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) {
-            LOG("-p <= 0          -->  p <= 0");
+            TRACE("bv", tout << "-p <= 0          -->  p <= 0\n");
             lhs = -lhs;
         }
         // NOTE: do not use pdd operations in conditions when comparing pdd values.
@@ -180,7 +180,7 @@ namespace polysat {
 
         // TODO: potential bug here: first call offset(), then rhs+1 has to reallocate pdd_manager::m_values, then the reference to offset is broken.
         if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) {
-            LOG("p - k <= -k - 1  -->  k <= p");
+            TRACE("bv", tout << "p - k <= -k - 1  -->  k <= p\n");
             pdd k = -(rhs + 1);
             rhs = lhs + k;
             lhs = k;
@@ -190,7 +190,7 @@ namespace polysat {
 
         // k <= 2^(N-1)*p + q + k-1  -->  k <= 2^(N-1)*p - q
         if (lhs.is_val() && rhs.leading_coefficient() == rational::power_of_two(N-1) && rhs.offset() == lhs_minus_one.val()) {
-            LOG("k <= 2^(N-1)*p + q + k-1  -->  k <= 2^(N-1)*p - q");
+            TRACE("bv", tout << "k <= 2^(N-1)*p + q + k-1  -->  k <= 2^(N-1)*p - q\n");
             rhs = (lhs - 1) - rhs;
         }
 

src/sat/smt/polysat/viable.cpp

@@ -112,6 +112,7 @@ namespace polysat {
 
         val1 = 0;
         lbool r = next_viable(val1);
+        TRACE("bv", display_state(tout); display(tout << "next viable v" << v << " " << val1 << " " << r << "\n"));
         if (r != l_true)
             return r;
 
@@ -547,10 +548,10 @@ namespace polysat {
     /*
     * Register constraint at index 'idx' as unitary in v.
     */
-    void viable::add_unitary(pvar v, unsigned idx) {
+    bool viable::add_unitary(pvar v, unsigned idx) {
 
         if (c.is_assigned(v))
-            return;
+            return true;
         auto [sc, d, value] = c.m_constraint_index[idx];
         SASSERT(value != l_undef);
         if (value == l_false)
@@ -559,29 +560,27 @@ namespace polysat {
         entry* ne = alloc_entry(v, idx);
         if (!m_forbidden_intervals.get_interval(sc, v, *ne)) {
             m_alloc.push_back(ne);
-            return;
+            return true;
         }
 
+        // verbose_stream() << "v" << v << " " << sc << " " << ne->interval << "\n";
+
         if (ne->interval.is_currently_empty()) {
             m_alloc.push_back(ne);
-            return;
+            return true;
         }        
 
-        if (ne->coeff == 1) {
+        if (ne->coeff == 1) 
             intersect(v, ne);        
-            return;
+        else if (ne->coeff == -1) 
-        }
-        else if (ne->coeff == -1) {
             insert(ne, v, m_diseq_lin, entry_kind::diseq_e);        
-            return;
-        }
         else {
             unsigned const w = c.size(v);
             unsigned const k = ne->coeff.parity(w);
             // unsigned const lo_parity = ne->interval.lo_val().parity(w);
             // unsigned const hi_parity = ne->interval.hi_val().parity(w);
 
-            display_one(std::cerr << "try to reduce entry: ", v, ne) << "\n";
+            IF_VERBOSE(1, display_one(verbose_stream() << "try to reduce entry: ", v, ne) << "\n");
 
             if (k > 0 && ne->coeff.is_power_of_two()) {
                 // reduction of coeff gives us a unit entry
@@ -640,8 +639,15 @@ namespace polysat {
             // unsigned const shared_parity = std::min(coeff_parity, std::min(lo_parity, hi_parity));
 
             insert(ne, v, m_equal_lin, entry_kind::equal_e);
-            return;
         }
+        if (ne->interval.is_full()) {
+            m_explain.reset();
+            m_explain.push_back(ne);
+            m_fixed_bits.reset();
+            m_var = v;
+            return false;
+        }
+        return true;
     }
 
     void viable::ensure_var(pvar v) {
@@ -890,6 +896,14 @@ namespace polysat {
         return out;
     }
 
+    std::ostream& viable::display_state(std::ostream& out) const {
+        out << "v" << m_var << ": ";
+        for (auto const& slice : m_overlaps)
+            out << slice.v << " ";
+        out << "\n";
+        return out;
+    }
+
       /*
      * Lower bounds are strictly ascending.
      * Intervals don't contain each-other (since lower bounds are ascending, it suffices to check containment in one direction).

src/sat/smt/polysat/viable.h

@@ -132,6 +132,7 @@ namespace polysat {
         fixed_bits      m_fixed_bits;
         offset_slices   m_overlaps;
         void init_overlaps(pvar v);
+        std::ostream& display_state(std::ostream& out) const;
 
     public:
         viable(core& c);
@@ -151,7 +152,7 @@ namespace polysat {
         /*
         * Register constraint at index 'idx' as unitary in v.
         */
-        void add_unitary(pvar v, unsigned idx);
+        bool add_unitary(pvar v, unsigned idx);
 
         /*
         * Ensure data-structures tracking variable v.

src/sat/smt/polysat_egraph.cpp

@@ -117,6 +117,7 @@ namespace polysat {
     void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function<void(euf::enode*, euf::enode*)>& consume_eq) {
         euf::theory_var v = m_pddvar2var[pv];
         euf::theory_var w = m_pddvar2var[pw];
+        verbose_stream() << "explain " << ctx.bpp(var2enode(v)) << " " << ctx.bpp(var2enode(w)) << "\n";
         m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq);
     }
 

src/sat/smt/polysat_model.cpp

@@ -73,10 +73,10 @@ namespace polysat {
     }
 
     std::ostream& solver::display(std::ostream& out) const {
-        m_core.display(out);
         for (unsigned v = 0; v < get_num_vars(); ++v)
             if (m_var2pdd_valid.get(v, false))
                 out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
+        m_core.display(out);
         m_intblast.display(out);
         return out;
     }

src/sat/smt/polysat_solver.cpp

@@ -113,14 +113,11 @@ namespace polysat {
         if (ctx.use_drat() && hint_info)
             hint = mk_proof_hint(hint_info);
         auto ex = euf::th_explain::conflict(*this, lits, eqs, hint);
-
+        TRACE("bv", ex->display(tout << "conflict: ") << "\n"; s().display(tout));
         ctx.set_conflict(ex);
     }
 
-    std::pair<sat::literal_vector, euf::enode_pair_vector> solver::explain_deps(dependency_vector const& deps) {
+    void solver::explain_dep(dependency const& d, euf::enode_pair_vector& eqs, sat::literal_vector& core) {
-        sat::literal_vector core;
-        euf::enode_pair_vector eqs;
-        for (auto d : deps) {
         if (d.is_bool_var()) {
             auto bv = d.bool_var();
             auto lit = sat::literal(bv, s().value(bv) == l_false);
@@ -148,6 +145,14 @@ namespace polysat {
             eqs.push_back(euf::enode_pair(n1, n2));
         }
     }
+
+    std::pair<sat::literal_vector, euf::enode_pair_vector> solver::explain_deps(dependency_vector const& deps) {
+        sat::literal_vector core;
+        euf::enode_pair_vector eqs;
+        for (auto d : deps) 
+            explain_dep(d, eqs, core);
+
+        
         IF_VERBOSE(10,
             for (auto lit : core)
                 verbose_stream() << "    " << lit << ":  " << mk_ismt2_pp(literal2expr(lit), m) << " " << s().value(lit) << "\n";
@@ -236,44 +241,16 @@ namespace polysat {
     unsigned solver::level(dependency const& d) {
         if (d.is_bool_var())
             return s().lvl(d.bool_var());
-        else if (d.is_eq()) {
-            auto [v1, v2] = d.eq();
         sat::literal_vector lits;
-            ctx.get_eq_antecedents(var2enode(v1), var2enode(v2), lits);
+        euf::enode_pair_vector eqs;
+        explain_dep(d, eqs, lits);
+        for (auto [n1, n2] : eqs)
+            ctx.get_eq_antecedents(n1, n2, lits);
         unsigned level = 0;
         for (auto lit : lits)
             level = std::max(level, s().lvl(lit));
         return level;
     }
-        else if (d.is_offset_claim()) {
-            auto const& offs = d.offset();
-            sat::literal_vector lits;
-            std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
-                ctx.get_eq_antecedents(a, b, lits);                
-                };
-            explain_slice(offs.v, offs.w, offs.offset, consume);
-            unsigned level = 0;
-            for (auto lit : lits)
-                level = std::max(level, s().lvl(lit));
-            return level;
-        }
-        else if (d.is_fixed_claim()) {
-            auto const& f = d.fixed();
-            sat::literal_vector lits;
-            std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
-                ctx.get_eq_antecedents(a, b, lits);
-                };
-            explain_fixed(f.v, f.lo, f.hi, f.value, consume);
-            unsigned level = 0;
-            for (auto lit : lits)
-                level = std::max(level, s().lvl(lit));
-            return level;
-        }
-        else {
-            SASSERT(d.is_axiom());
-            return 0;
-        }
-    }
 
     void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps, char const* hint_info) {
         TRACE("bv", tout << "propagate " << d << " " << sign << "\n");
@@ -311,41 +288,21 @@ namespace polysat {
 
     bool solver::add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant) {
         sat::literal_vector lits;
+        euf::enode_pair_vector eqs;
         for (auto it = begin; it != end; ++it) {
             auto const& e = *it;
             if (std::holds_alternative<dependency>(e)) {
                 auto d = *std::get_if<dependency>(&e);
                 SASSERT(!d.is_null());
-                if (d.is_bool_var()) {
+                explain_dep(d, eqs, lits);
-                    auto bv = d.bool_var();
-                    auto lit = sat::literal(bv, s().value(bv) == l_false);
-                    lits.push_back(~lit);
-                }
-                else if (d.is_eq()) {
-                    auto [v1, v2] = d.eq();
-                    lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2)));
-                }
-                else if (d.is_offset_claim()) {
-                    auto const& o = d.offset();
-                    std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
-                        lits.push_back(~eq_internalize(a, b));
-                    };
-                    explain_slice(o.v, o.w, o.offset, consume);
-                }
-                else if (d.is_fixed_claim()) {
-                    auto const& f = d.fixed();
-                    std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
-                        lits.push_back(~eq_internalize(a, b));
-                    };
-                    explain_fixed(f.v, f.lo, f.hi, f.value, consume);
-                }
-                else {
-                    SASSERT(d.is_axiom());
-                }
             }
             else if (std::holds_alternative<signed_constraint>(e))
-                lits.push_back(ctx.mk_literal(constraint2expr(*std::get_if<signed_constraint>(&e))));
+                lits.push_back(~ctx.mk_literal(constraint2expr(*std::get_if<signed_constraint>(&e))));
         }
+        for (auto [n1, n2] : eqs)
+            ctx.get_eq_antecedents(n1, n2, lits);
+        for (auto& lit : lits)
+            lit.neg();
         for (auto lit : lits)
             if (s().value(lit) == l_true)
                 return false;

src/sat/smt/polysat_solver.h

@@ -193,6 +193,9 @@ namespace polysat {
             return add_axiom(name, clause.begin(), clause.end(), redundant);
         }
 
+
+        void explain_dep(dependency const& d, euf::enode_pair_vector& eqs, sat::literal_vector& lits);
+
         std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);
 
         expr_ref constraint2expr(signed_constraint const& sc);