bugfixes

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

src/math/dd/dd_pdd.cpp

@@ -1860,6 +1860,22 @@ namespace dd {
         return (*this) * rational::power_of_two(n);
     }
 
+    bool pdd::has_unit(pdd& x, pdd& rest) const {
+        if (is_val())
+            return false;
+        pdd r = *this;
+        while (!r.is_val()) {
+            if (r.hi().is_one()) {
+                x = m->mk_var(r.var());
+                rest = *this - x;
+                return true;
+            }
+            r = r.lo();
+        }
+        return false;
+    }
+
+
     /**
      * \brief substitute variable v by r.
      * This base line implementation is simplistic and does not use operator caching.

src/math/dd/dd_pdd.h

@@ -441,6 +441,7 @@ namespace dd {
         bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); }
         bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); }
         bool is_binary() const { return m->is_binary(root); }
+        bool has_unit(pdd& x, pdd& rest) const; 
         bool is_monomial() const { return m->is_monomial(root); }
         bool is_univariate() const { return m->is_univariate(root); }
         bool is_univariate_in(unsigned v) const { return m->is_univariate_in(root, v); }

src/math/lp/int_solver.cpp

@@ -950,14 +950,16 @@ namespace lp {
             bool feas = _check_feasible();
             lra.pop(1);
 
-            if (settings().get_cancel_flag())
+            if (!feas) {
-                return lia_move::undef;
+                for (auto const& cut : cuts)
-
+                    if (!is_small_cut(cut))
-            if (!feas)
+                        add_cut(cut);
-                return lia_move::conflict;
+            }            
-            
         }
 
+        if (settings().get_cancel_flag())
+            return lia_move::undef;
+
         if (!_check_feasible())
             return lia_move::conflict;
         

src/sat/smt/polysat/core.cpp

@@ -343,9 +343,7 @@ namespace polysat {
     }
 
     void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
-        TRACE("bv", tout << "propagate assignment v" << v << " := " << value << " " << is_assigned(v) << "\n");
+        TRACE("bv", tout << "propagate assignment v" << v << " := " << value << "\n");
-        if (is_assigned(v))
-            return;
         
         m_values[v] = value;
         m_justification[v] = dep;   
@@ -404,14 +402,14 @@ namespace polysat {
     */
     void core::propagate_eval(constraint_id idx) {
         auto [sc, d, value] = m_constraint_index[idx.id];
-        if (value != l_undef)
-            return;
         switch (eval(sc)) {
         case l_false:
-            s.propagate(d, true, explain_eval(sc), "eval-propagate");
+            if (value != l_false)
+                s.propagate(d, true, explain_eval(sc), "eval-propagate");
             break;
         case l_true:
-            s.propagate(d, false, explain_eval(sc), "eval-propagate");
+            if (value != l_true)
+                s.propagate(d, false, explain_eval(sc), "eval-propagate");
             break;
         default:
             break;

src/sat/smt/polysat/umul_ovfl_constraint.cpp

@@ -69,9 +69,7 @@ namespace polysat {
     }
 
     lbool umul_ovfl_constraint::eval(assignment const& a) const {
-        auto r = eval(a.apply_to(p()), a.apply_to(q()));
+        return eval(a.apply_to(p()), a.apply_to(q()));
-        CTRACE("bv", r != l_undef, tout << "eval: " << *this << " := " << r << "\n";);
-        return r;
     }
 
     void umul_ovfl_constraint::activate(core& c, bool sign, dependency const& dep) {

src/sat/smt/polysat/viable.cpp

@@ -110,7 +110,7 @@ namespace polysat {
         bool start_at0 = val1 == 0;        
         
         lbool r = next_viable(val1);
-        TRACE("bv", display_state(tout); display(tout << "next viable v" << v << " " << val1 << " " << r << "\n"));
+        TRACE("bv", display_state(tout); display(tout << "next viable v" << v << " " << val1 << " " << r << " " << start_at0 << "\n"));
         if (r == l_false && !start_at0) {
             val1 = 0;
             r = next_viable(val1);
@@ -225,6 +225,8 @@ namespace polysat {
 
         while (true) {                
             auto e = find_overlap(val1, layer.entries);
+            TRACE("bv", tout << "next v" << w << " for value " << val1 << "\n";
+                  if (e) tout << e->interval << " " << e->interval.is_full() << "\n"; else tout << "no overlap\n";);
             if (!e) 
                 break;            
             // TODO check if admitted: layer.entries = e;
@@ -232,10 +234,10 @@ namespace polysat {
             if (e->interval.is_full())
                 return l_false;            
             auto hi = e->interval.hi_val();
-            if (hi < e->interval.lo_val())   
-                wrapped = true;
             if (wrapped && start <= hi)
                 return l_false;            
+            if (hi < e->interval.lo_val())   
+                wrapped = true;
             val1 = hi;
             SASSERT(val1 < p2b);
         }
@@ -530,11 +532,13 @@ namespace polysat {
             if (m_var != e->var)
                 result.push_back(offset_claim(m_var, {e->var, 0}));
             seen.insert(index.id);
+            for (auto const& sc : e->side_cond)               
+                result.push_back(c.propagate(sc, c.explain_eval(sc)));            
             auto const& [sc, d, value] = c.m_constraint_index[index.id];
-            result.push_back(d);
+            result.push_back(d);            
-            result.append(c.explain_eval(sc));
         }
         result.append(m_fixed_bits.explain());
+        TRACE("bv", tout << "viable-explain v" << m_var << " - " << result.size() << "\n");
         return result;
     }
 
@@ -579,7 +583,7 @@ namespace polysat {
             unsigned const k = ne->coeff.parity(w);
             SASSERT(k > 0);
 
-            IF_VERBOSE(3, display_one(verbose_stream() << "try to reduce entry: ", v, ne) << "\n");
+            IF_VERBOSE(13, display_one(verbose_stream() << "try to reduce entry: ", v, ne) << "\n");
 
             // reduction of coeff gives us a unit entry
             //
@@ -618,8 +622,8 @@ namespace polysat {
                     ne->side_cond.push_back(cs.eq(lo_eq));
             }
             else {
-                new_lo += 1;
                 new_lo = machine_div2k(new_lo, k);
+                new_lo += 1;
                 if (!lo_eq.is_val() || lo_eq.is_zero())
                     ne->side_cond.push_back(~cs.eq(lo_eq));
             }
@@ -631,18 +635,16 @@ namespace polysat {
                     ne->side_cond.push_back(cs.eq(hi_eq));
             }
             else {
-                new_hi += 1;
                 new_hi = machine_div2k(new_hi, k);
+                new_hi += 1;
                 if (!hi_eq.is_val() || hi_eq.is_zero())
                     ne->side_cond.push_back(~cs.eq(hi_eq));
             }
             
-            // we have to update also the pdd bounds accordingly, but it seems not worth introducing new variables for this eagerly
-            //      new_lo = lo[:k]  etc.
             
             if (new_lo == new_hi) {
+                IF_VERBOSE(0, verbose_stream() << "Check: always true " << "x*" << ne->coeff << " not in " << ne->interval << " " << new_hi << "\n");
                 // empty
-                verbose_stream() << "always true " << "x*" << ne->coeff << " not in " << ne->interval << "\n";
                 m_alloc.push_back(ne);
                 return true;
             }

src/sat/smt/polysat_solver.cpp

@@ -124,7 +124,9 @@ namespace polysat {
         if (ctx.use_drat() && hint_info)
             hint = mk_proof_hint(hint_info, lits, eqs);
         auto ex = euf::th_explain::conflict(*this, lits, eqs, hint);
-        TRACE("bv", ex->display(tout << "conflict: ") << "\n"; s().display(tout));
+        TRACE("bv", tout << "conflict: " << lits << " ";
+        for (auto [a, b] : eqs) tout << ctx.bpp(a) << " == " << ctx.bpp(b) << " "; 
+        tout << "\n"; s().display(tout));
         validate_conflict(lits, eqs);
         ctx.set_conflict(ex);
     }
@@ -166,10 +168,11 @@ namespace polysat {
 
         
         IF_VERBOSE(10,
+            verbose_stream() << "explain\n";
             for (auto lit : core)
                 verbose_stream() << "    " << lit << ":  " << mk_ismt2_pp(literal2expr(lit), m) << " " << s().value(lit) << "\n";
-        for (auto const& [n1, n2] : eqs)
+            for (auto const& [n1, n2] : eqs)
-            verbose_stream() << "    " << ctx.bpp(n1) << "  ==  " << ctx.bpp(n2) << "\n";);
+                verbose_stream() << "    " << ctx.bpp(n1) << "  ==  " << ctx.bpp(n2) << "\n";);
         DEBUG_CODE({
             for (auto lit : core)
                 SASSERT(s().value(lit) == l_true);
@@ -381,16 +384,25 @@ namespace polysat {
         expr_ref result(m);
         switch (sc.op()) {
         case ckind_t::ule_t: {
+            
             auto p = sc.to_ule().lhs();
             auto q = sc.to_ule().rhs();
-            auto l = pdd2expr(p);
+            pdd x = p, r = p;
-            auto h = pdd2expr(q);
+            if (q.is_zero() && p.has_unit(x, r)) {
-            if (p == q)
+                auto l = pdd2expr(x);
-                result = m.mk_true();
+                auto h = pdd2expr(-r);
-            else if (q.is_zero())
                 result = m.mk_eq(l, h);
-            else
+            }
-                result = bv.mk_ule(l, h);
+            else {
+                auto l = pdd2expr(p);
+                auto h = pdd2expr(q);
+                if (p == q)
+                    result = m.mk_true();
+                else if (q.is_zero())
+                    result = m.mk_eq(l, h);
+                else
+                    result = bv.mk_ule(l, h);
+            }
             if (sc.sign())
                 result = m.mk_not(result);
             return result;           
@@ -419,12 +431,14 @@ namespace polysat {
             return expr_ref(n, m);
         }
         auto v = var2enode(m_pddvar2var[p.var()]);
-        expr* r = v->get_expr();
+        expr_ref r(m);
+        r = v->get_expr();
         if (!p.hi().is_one())
             r = bv.mk_bv_mul(r, pdd2expr(p.hi()));
         if (!p.lo().is_zero())
             r = bv.mk_bv_add(r, pdd2expr(p.lo()));
-        return expr_ref(r, m);
+        ctx.get_rewriter()(r);
+        return r;
     }
 
     expr* solver::proof_hint::get_hint(euf::solver& s) const {