na

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

src/sat/smt/intblast_solver.cpp

@@ -562,7 +562,7 @@ namespace intblast {
             unsigned lo, hi;
             expr* old_arg;
             VERIFY(bv.is_extract(e, lo, hi, old_arg));
-            expr* r = arg(0);
+            r = arg(0);
             if (lo > 0)
                 r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo)));
             break;

src/sat/smt/intblast_solver.h

@@ -66,7 +66,7 @@ namespace intblast {
         rational get_value(expr* e) const;
 
         expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
-        void set_translated(expr* e, expr* r) { m_translate.setx(e->get_id(), r); }
+        void set_translated(expr* e, expr* r) { SASSERT(r); m_translate.setx(e->get_id(), r); }
         expr* arg(unsigned i) { return m_args.get(i); }
 
         expr* umod(expr* bv_expr, unsigned i);

src/sat/smt/polysat/core.cpp

@@ -66,9 +66,15 @@ namespace polysat {
         core& c;
     public:
         mk_add_watch(core& c) : c(c) {}
-        void undo() override {
+        void undo() override {            
             auto& [sc, lit, val] = c.m_constraint_index.back();
             auto& vars = sc.vars();
+            verbose_stream() << "undo add watch " << sc << " ";
+            if (vars.size() > 0) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[0]] << ") ";
+            if (vars.size() > 1) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[1]] << ") ";
+            verbose_stream() << "\n";
+            SASSERT(vars.size() <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1);
+            SASSERT(vars.size() <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1);
             if (vars.size() > 0)
                 c.m_watch[vars[0]].pop_back();
             if (vars.size() > 1)
@@ -135,6 +141,10 @@ namespace polysat {
             add_watch(idx, vars[0]);
         if (vars.size() > 1)
             add_watch(idx, vars[1]);
+        verbose_stream() << "add watch " << sc << " " << vars << "  ";
+        if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
+        if (vars.size() > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
+        verbose_stream() << "\n";
         s.trail().push(mk_add_watch(*this));
         return idx;
     }
@@ -213,6 +223,15 @@ namespace polysat {
         m_assignment.push(v , value);
         s.trail().push(mk_assign_var(v, *this));
 
+        return; 
+        // to debug:
+        unsigned sz = m_watch[v].size();
+        for (unsigned i = 0; i < sz; ++i) {
+            auto idx = m_watch[v][i];
+            auto [sc, dep, value] = m_constraint_index[idx];
+            sc.propagate(*this, value, dep);
+        }
+
         // update the watch lists for pvars
         // remove constraints from m_watch[v] that have more than 2 free variables.
         // for entries where there is only one free variable left add to viable set 
@@ -226,15 +245,14 @@ namespace polysat {
             bool swapped = false;
             for (unsigned i = vars.size(); i-- > 2; ) {
                 if (!is_assigned(vars[i])) {
+                    verbose_stream() << "watch instead " << idx << " " << vars[i] << "instead of " << vars[0] << "\n";
                     add_watch(idx, vars[i]);
                     std::swap(vars[i], vars[0]);
                     swapped = true;
                     break;
                 }
             }
-
+           
-            sc.propagate(*this, value, dep);
-
             SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1])));
             if (swapped)
                 continue;
@@ -249,6 +267,7 @@ namespace polysat {
             m_viable.add_unitary(v1, idx);            
         }
         m_watch[v].shrink(j);
+        verbose_stream() << "new watch " << v << ": " << m_watch[v] << "\n";
     }
 
     void core::propagate_value(prop_item const& dc) {

src/sat/smt/polysat/ule_constraint.cpp

@@ -75,8 +75,6 @@ Useful lemmas:
 #include "sat/smt/polysat/constraints.h"
 #include "sat/smt/polysat/ule_constraint.h"
 
-#define LOG(_msg_) verbose_stream() << _msg_ << "\n"
-
 namespace polysat {
 
     // Simplify lhs <= rhs.

src/sat/smt/polysat_solver.cpp

@@ -138,6 +138,10 @@ namespace polysat {
         for (auto lit : lits)
             level = std::max(level, s().lvl(lit));
         auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
+        if (level == 0) {
+            ctx.set_conflict(ex);
+            return;
+        }        
         ctx.push(value_trail<bool>(m_has_lemma));
         m_has_lemma = true;
         m_lemma_level = level;
@@ -165,7 +169,8 @@ namespace polysat {
         if (!m_has_lemma)
             return l_undef;
 
-        unsigned num_scopes = s().scope_lvl() - m_lemma_level;
+        SASSERT(m_lemma_level > 0);
+        unsigned num_scopes = s().scope_lvl() - m_lemma_level - 1;
 
         NOT_IMPLEMENTED_YET();
         // s().pop_reinit(num_scopes);