add ad-hoc debug output, add rule for incremental linearization

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

src/sat/smt/polysat/core.cpp

@@ -311,8 +311,13 @@ namespace polysat {
     }
 
     void core::viable_conflict(pvar v) {
+        if (s.inconsistent())
+            return;
         TRACE("bv", tout << "viable-conflict v" << v << "\n");
-        s.set_conflict(m_viable.explain(), "viable-conflict");
+        auto exp = m_viable.explain();
+        if (s.inconsistent())
+            verbose_stream() << "inconsistent " << exp << "\n";
+        s.set_conflict(exp, "viable-conflict");
         decay_activity();
     }
 
@@ -371,6 +376,7 @@ namespace polysat {
         else if (v == null_var && weak_eval(sc) == l_false) {
             auto ex = explain_weak_eval(sc);
             ex.push_back(dep);
+            verbose_stream() << "infeasible propagation " << ~sc << " <- " << ex << "\n";
             s.set_conflict(ex, "infeasible propagation");
         }
     }
@@ -381,6 +387,7 @@ namespace polysat {
         if (!m_viable.assign(v, value)) {
             auto deps = m_viable.explain();
             deps.push_back(dep);
+            verbose_stream() << "non-viable assignment v" << v << " == " << value << " <- " << deps << "\n";
             s.set_conflict(deps, "non-viable assignment");
             return;
         }
@@ -489,6 +496,7 @@ namespace polysat {
         else if (value != eval_value) {
             m_unsat_core = explain_weak_eval(sc);
             m_unsat_core.push_back(m_constraint_index[id.id].d);
+            verbose_stream() << "infeasible propagation " << m_unsat_core << "\n";
             s.set_conflict(m_unsat_core, "polysat-constraint-core");
             decay_activity();
         }                   
@@ -645,7 +653,7 @@ namespace polysat {
     }
 
     void core::inc_activity(pvar v) {
-        unsigned& act = m_activity[v].second;
+        unsigned& act = m_activity[v].act;
         act += m_activity_inc;
         m_var_queue.activity_increased_eh(v);
         if (act > (1 << 24))
@@ -654,7 +662,7 @@ namespace polysat {
 
     void core::rescale_activity() {
         for (auto& act : m_activity) 
-            act.second >>= 14;        
+            act.act >>= 14;        
         m_activity_inc >>= 14;
     }
 

src/sat/smt/polysat/core.h

@@ -35,11 +35,23 @@ namespace polysat {
 
 
     class core {
+        struct var_activity {
+            unsigned sz;
+            unsigned act;
+            bool operator<(var_activity const& other) const {
+                if (other.sz != sz)
+                    return sz > other.sz;
+                return act < other.act;
+            };
+            bool operator>(var_activity const& other) const {
+                return other < *this;
+            }
+        };
         class mk_add_var;
         class mk_dqueue_var;
         class mk_assign_var;
         class mk_add_watch;
-        typedef svector<std::pair<unsigned, unsigned>> activity;
+        typedef svector<var_activity> activity;
         friend class viable;
         friend class constraints;
         friend class assignment;

src/sat/smt/polysat/monomials.cpp

@@ -66,6 +66,8 @@ namespace polysat {
             return l_false;
         if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); }))
             return l_false;
+        if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); }))
+            return l_false;
 
         if (any_of(m_to_refine, [&](auto i) { return non_overflow_unit(m_monomials[i]); }))
             return l_false;
@@ -169,6 +171,23 @@ namespace polysat {
         return c.add_axiom("p = k => p * q = k * q", cs, true);
     }
 
+    // p * q = p => q = 1 or p = 0
+    bool monomials::mul1_inverse(monomial const& mon) {
+        for (unsigned j = mon.size(); j-- > 0; ) {
+            auto const& arg_val = mon.arg_vals[j];
+            if (arg_val == mon.val) {
+                auto const& p = mon.args[j];
+                pdd qs = c.value(rational(1), mon.num_bits());
+                for (unsigned k = mon.size(); k-- > 0; ) 
+                    if (k != j)
+                        qs *= mon.arg_vals[k];                
+                c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), C.eq(qs, 1), C.eq(p) }, true);
+                return true;
+            }
+        }
+        return false;
+    }
+
     // parity p >= i => parity p * q >= i
     bool monomials::parity(monomial const& mon) {       
         unsigned parity_val = get_parity(mon.val, mon.num_bits());

src/sat/smt/polysat/monomials.h

@@ -49,6 +49,7 @@ namespace polysat {
         bool mul0(monomial const& mon);
         bool mul1(monomial const& mon);
         bool mulp2(monomial const& mon);
+        bool mul1_inverse(monomial const& mon);
         bool mul(monomial const& mon, std::function<bool(rational const&)> const& p);
         bool parity(monomial const& mon);
         bool non_overflow_monotone(monomial const& mon);

src/sat/smt/polysat/viable.cpp

@@ -555,6 +555,8 @@ namespace polysat {
         auto last = m_explain.back();
         auto after = last;
 
+        if (c.inconsistent())
+            verbose_stream() << "inconistent explain\n";
         TRACE("bv", display_explain(tout));
 
         auto unmark = [&]() {
@@ -564,13 +566,20 @@ namespace polysat {
 
         auto explain_entry = [&](entry* e) {
             auto index = e->constraint_index;
+            if (c.inconsistent())
+                return;
             if (e->marked)
                 return;
             e->marked = true;
             if (m_var != e->var)
                 result.push_back(offset_claim(m_var, { e->var, 0 }));
-            for (auto const& sc : e->side_cond)
+            for (auto const& sc : e->side_cond) {
-                result.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
+                auto d = c.propagate(sc, c.explain_weak_eval(sc));
+                if (c.inconsistent()) {
+                    verbose_stream() << "inconsistent " << d << " " << sc << "\n";
+                }
+                result.push_back(d);
+            }
             result.append(e->deps);
             if (!index.is_null())
                 result.push_back(c.get_dependency(index));
@@ -600,7 +609,11 @@ namespace polysat {
             explain_entry(first.e);
             // add constraint that there is only a single viable value.         
             auto sc = cs.eq(last.e->interval.hi() + 1, first.e->interval.lo());
-            result.push_back(c.propagate(sc, c.explain_weak_eval(sc)));            
+            auto exp = c.propagate(sc, c.explain_weak_eval(sc));
+            if (c.inconsistent()) {
+                verbose_stream() << "inconsistent " << sc << " " << exp << "\n";
+            }
+            result.push_back(exp);            
         }
         if (m_explain_kind == explain_t::assignment) {
             // there is just one entry
@@ -608,6 +621,8 @@ namespace polysat {
             explain_entry(last.e);
         }
         unmark();
+        if (c.inconsistent())
+            verbose_stream() << "inconistent after explain\n";
         return result;
     }
 
@@ -691,6 +706,8 @@ namespace polysat {
             t.reset(lo.manager());
             t = c.value(mod(e.value, rational::power_of_two(aw)), aw);
             // verbose_stream() << "after " << t << "\n";
+            if (c.inconsistent())
+                verbose_stream() << "inconsistent overlap " << sc << " " << "\n";
         }
 
         if (abw < aw) 
@@ -700,6 +717,12 @@ namespace polysat {
         SASSERT(!sc.is_always_false());
         if (!sc.is_always_true())
             deps.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
+        if (c.inconsistent()) {
+            verbose_stream() << "inconsistent ult " << sc << " " << "\n";
+            verbose_stream() << "before bw " << ebw << " " << bw << " " << *e.e << "\nafter  bw " << abw << " " << aw << " " << *after.e << "\n";
+            display(verbose_stream());
+            // UNREACHABLE();
+        }
     }
 
     /*

src/sat/smt/polysat_solver.cpp

@@ -260,6 +260,9 @@ namespace polysat {
             hint = mk_proof_hint(hint_info, core, eqs);
             core.pop_back();
         }
+        if (s().value(lit) == l_false) {
+            verbose_stream() << "contradictory propagation " << sc << " <- " << deps << "\n";
+        }
         auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint);     
         validate_propagate(lit, core, eqs);
         ctx.propagate(lit, ex);