n/a

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

src/sat/smt/euf_solver.cpp

@@ -23,6 +23,7 @@ Author:
 #include "sat/smt/bv_solver.h"
 #include "sat/smt/intblast_solver.h"
 #include "sat/smt/polysat_solver.h"
+#include "sat/smt/intblast_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/array_solver.h"
 #include "sat/smt/arith_solver.h"

src/sat/smt/intblast_solver.h

@@ -109,7 +109,7 @@ namespace intblast {
         void translate_quantifier(quantifier* q);
         void translate_var(var* v);
 
-        void ensure_args(app* e);
+        void ensure_translated(expr* e);
         void internalize_bv(app* e);
 
         unsigned m_vars_qhead = 0;

src/sat/smt/polysat/constraints.h

@@ -31,12 +31,15 @@ namespace polysat {
 
     class constraint {
         unsigned_vector     m_vars;
+        unsigned            m_num_watch = 0;
     public:
         virtual ~constraint() {}
         unsigned_vector& vars() { return m_vars; }
         unsigned_vector const& vars() const { return m_vars; }
         unsigned var(unsigned idx) const { return m_vars[idx]; }
         bool contains_var(pvar v) const { return m_vars.contains(v); }
+        unsigned num_watch() const { return m_num_watch;  }
+        void set_num_watch(unsigned n) { SASSERT(n <= 2);  m_num_watch = n; }
         virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual lbool eval() const = 0;
@@ -63,6 +66,8 @@ namespace polysat {
         unsigned_vector const& vars() const { return m_constraint->vars(); }
         unsigned var(unsigned idx) const { return m_constraint->var(idx); }
         bool contains_var(pvar v) const { return m_constraint->contains_var(v); }
+        unsigned num_watch() const { return m_constraint->num_watch(); }
+        void set_num_watch(unsigned n) { m_constraint->set_num_watch(n); }
         void activate(core& c, dependency const& d) { m_constraint->activate(c, m_sign, d); }
         void propagate(core& c, lbool value, dependency const& d) { m_constraint->propagate(c, value, d); }
         bool is_always_true() const { return eval() == l_true; }

src/sat/smt/polysat/core.cpp

@@ -74,11 +74,13 @@ namespace polysat {
             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);
+            unsigned n = sc.num_watch();
-            SASSERT(vars.size() <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1);
+            SASSERT(n <= vars.size());
-            if (vars.size() > 0)
+            SASSERT(n <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1);
+            SASSERT(n <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1);
+            if (n > 0)
                 c.m_watch[vars[0]].pop_back();
-            if (vars.size() > 1)
+            if (n > 1)
                 c.m_watch[vars[1]].pop_back();
             c.m_constraint_index.pop_back();
         }
@@ -138,9 +140,10 @@ namespace polysat {
         for (; i < sz && j < 2; ++i)
             if (!is_assigned(vars[i]))
                 std::swap(vars[i], vars[j++]);
-        if (vars.size() > 0)
+        sc.set_num_watch(i);
+        if (i > 0)
             add_watch(idx, vars[0]);
-        if (vars.size() > 1)
+        if (i > 1)
             add_watch(idx, vars[1]);
         IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << "  ";
                     if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
@@ -225,19 +228,12 @@ namespace polysat {
         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 
-        unsigned j = 0;
+        unsigned j = 0, sz = m_watch[v].size();
-        for (auto idx : m_watch[v]) {
+        for (unsigned k = 0; k < sz; ++k) {
+            auto idx = m_watch[v][k];
             auto [sc, dep, value] = m_constraint_index[idx];
             auto& vars = sc.vars();
             if (vars[0] != v)
@@ -253,6 +249,11 @@ namespace polysat {
                     break;
                 }
             }
+
+            // this can create fresh literals and update m_watch, but
+            // will not update m_watch[v] (other than copy constructor for m_watch)
+            // because v has been assigned a value.
+            sc.propagate(*this, value, dep);
            
             SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1])));
             if (swapped)
@@ -267,6 +268,7 @@ namespace polysat {
             // detect unitary, add to viable, detect conflict?
             m_viable.add_unitary(v1, idx);            
         }
+        SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");
         m_watch[v].shrink(j);
         verbose_stream() << "new watch " << v << ": " << m_watch[v] << "\n";
     }