fixing up missing dependencies during resolution

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

src/math/polysat/boolean.cpp

@@ -61,8 +61,8 @@ namespace polysat {
 
     void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) {
         LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason);
-        assign(kind_t::propagation, lit, lvl, &reason);
+        assign(kind_t::bool_propagation, lit, lvl, &reason);
-        SASSERT(is_propagation(lit));
+        SASSERT(is_bool_propagation(lit));
     }
 
     void bool_var_manager::decide(sat::literal lit, unsigned lvl, clause& lemma) {
@@ -79,8 +79,8 @@ namespace polysat {
 
     void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
         LOG("Eval literal " << lit << " @ " << lvl);
-        assign(kind_t::propagation, lit, lvl, nullptr);
+        assign(kind_t::value_propagation, lit, lvl, nullptr);
-        SASSERT(is_propagation(lit));
+        SASSERT(is_value_propagation(lit));
     }
 
     void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dependency dep) {

src/math/polysat/boolean.h

@@ -22,7 +22,8 @@ namespace polysat {
 
         enum class kind_t {
             unassigned,
-            propagation,
+            bool_propagation,
+            value_propagation,
             decision,
         };
 
@@ -56,15 +57,17 @@ namespace polysat {
         bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; }
         bool is_decision(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::decision; }
         bool is_decision(sat::literal lit) const { return is_decision(lit.var()); }
-        bool is_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::propagation; }
+        bool is_bool_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::bool_propagation; }
-        bool is_propagation(sat::literal lit) const { return is_propagation(lit.var()); }
+        bool is_bool_propagation(sat::literal lit) const { return is_bool_propagation(lit.var()); }
+        bool is_value_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::value_propagation; }
+        bool is_value_propagation(sat::literal lit) const { return is_value_propagation(lit.var()); }
         lbool value(sat::bool_var var) const { return value(sat::literal(var)); }
         lbool value(sat::literal lit) const { return m_value[lit.index()]; }
         bool is_true(sat::literal lit) const { return value(lit) == l_true; }
         bool is_false(sat::literal lit) const { return value(lit) == l_false; }
         unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; }
         unsigned level(sat::literal lit) const { return level(lit.var()); }
-        clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_propagation(var) ? m_clause[var] : nullptr; }
+        clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_bool_propagation(var) ? m_clause[var] : nullptr; }
         clause* reason(sat::literal lit) const { return reason(lit.var()); }
         dependency dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
 
@@ -84,7 +87,6 @@ namespace polysat {
         void propagate(sat::literal lit, unsigned lvl, clause& reason);
         void decide(sat::literal lit, unsigned lvl, clause& lemma);
         void decide(sat::literal lit, unsigned lvl);
-
         void eval(sat::literal lit, unsigned lvl);
         void asserted(sat::literal lit, unsigned lvl, dependency dep);
         void unassign(sat::literal lit);
@@ -94,7 +96,8 @@ namespace polysat {
         friend std::ostream& operator<<(std::ostream& out, kind_t const& k) {
             switch (k) {
             case kind_t::unassigned: return out << "unassigned"; 
-            case kind_t::propagation: return out << "propagation"; 
+            case kind_t::bool_propagation: return out << "bool propagation"; 
+            case kind_t::value_propagation: return out << "value propagation"; 
             case kind_t::decision: return out << "decision"; 
             default: UNREACHABLE(); return out;
             }

src/math/polysat/conflict.cpp

@@ -70,7 +70,7 @@ namespace polysat {
     * The core is then the conjuction of this constraint and assigned variables.
     */
     void conflict::set(signed_constraint c) {
-        LOG("Conflict: " << c);
+        LOG("Conflict: " << c << " " << c.bvalue(s));
         SASSERT(empty());
         if (c.bvalue(s) == l_false) {
             auto* cl = s.m_bvars.reason(c.blit().var());
@@ -209,7 +209,7 @@ namespace polysat {
         SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
         
         remove_literal(lit);        
-        unset_mark(s.lit2cnstr(lit));        
+        unset_bmark(s.lit2cnstr(lit));         
         for (sat::literal lit2 : cl)
             if (lit2 != lit)
                 insert(s.lit2cnstr(~lit2));
@@ -228,11 +228,12 @@ namespace polysat {
         remove_literal(lit);
         signed_constraint c = s.lit2cnstr(lit);
         unset_mark(c);
-        for (pvar v : c->vars())
+        for (pvar v : c->vars()) {
             if (s.is_assigned(v) && s.get_level(v) <= lvl) {
-                m_vars.insert(v);  // TODO: check this
+                m_vars.insert(v);  
                 inc_pref(v);
             }
+        }
     }
 
     /** 
@@ -330,9 +331,19 @@ namespace polysat {
         
         m_vars.remove(v);
 
-        if (j.is_propagation()) 
+        // TODO: side-conditions depend on variable assignments
-            for (auto const& c : s.m_viable.get_constraints(v))
+        // we need to track these when the side conditions are used
-                insert(c);        
+        // or we need to propagate the side-conditions if they are not set.
+        // 
+        if (j.is_propagation()) {
+            for (auto const& c : s.m_viable.get_constraints(v)) {
+                if (!c->has_bvar()) {
+                    cm().ensure_bvar(c.get());
+                    s.assign_eval(c.blit());
+                }
+                insert(c);
+            }        
+        }
 
         if (try_explain(v))
             return true;
@@ -392,17 +403,26 @@ namespace polysat {
         }
     }
 
-    void conflict::unset_mark(signed_constraint c) {
+    /**
+     * unset marking on the constraint, but keep variable dependencies.
+     */
+    void conflict::unset_bmark(signed_constraint c) {
         if (!c->is_marked())
             return;
         c->unset_mark();
         if (c->has_bvar())
             unset_bmark(c->bvar());
-        if (c->is_var_dependent()) {
+    }
-            c->unset_var_dependent();
+
-            for (auto v : c->vars())
+    void conflict::unset_mark(signed_constraint c) {
-                dec_pref(v);
+        if (!c->is_marked())
-        }
+            return;
+        unset_bmark(c);
+        if (!c->is_var_dependent()) 
+            return;
+        c->unset_var_dependent();
+        for (auto v : c->vars())
+            dec_pref(v);        
     }
 
     void conflict::inc_pref(pvar v) {

src/math/polysat/conflict.h

@@ -45,6 +45,7 @@ namespace polysat {
 
         void set_mark(signed_constraint c);
         void unset_mark(signed_constraint c);
+        void unset_bmark(signed_constraint c);
 
         bool contains_literal(sat::literal lit) const;
         void insert_literal(sat::literal lit);

src/math/polysat/solver.cpp

@@ -561,8 +561,10 @@ namespace polysat {
                     revert_bool_decision(lit);
                     return;
                 }
-                SASSERT(m_bvars.is_propagation(var));
+                if (m_bvars.is_bool_propagation(var))
-                resolve_bool(lit);
+                    m_conflict.resolve(lit, *m_bvars.reason(lit));
+                else
+                    m_conflict.resolve_with_assignment(lit, m_bvars.level(lit));
             }
         }
         // here we build conflict clause if it has free variables.
@@ -600,18 +602,17 @@ namespace polysat {
     }
 
 
+#if 0
     /** Conflict resolution case where boolean literal 'lit' is on top of the stack 
     *   NOTE: boolean resolution should work normally even in bailout mode.
     */
     void solver::resolve_bool(sat::literal lit) {       
-        SASSERT(m_bvars.is_propagation(lit));
+        SASSERT(m_bvars.is_bool_propagation(lit));
-        clause const* other = m_bvars.reason(lit);
+        clause const& other = *m_bvars.reason(lit);
-        LOG_H3("resolve_bool: " << lit << " " << show_deref(other));
+        LOG_H3("resolve_bool: " << lit << " " << show_deref(&other));
-        if (other)
+        m_conflict.resolve(lit, *other);        
-            m_conflict.resolve(lit, *other);
-        else
-            m_conflict.resolve_with_assignment(lit, m_bvars.level(lit));
     }
+#endif
     
     void solver::report_unsat() {
         backjump(base_level());
@@ -620,6 +621,7 @@ namespace polysat {
 
     void solver::unsat_core(dependency_vector& deps) {
         deps.reset();
+        LOG("conflict" << m_conflict);
         for (auto c : m_conflict) {
             auto d = m_bvars.dep(c.blit());
             if (d != null_dependency)

src/math/polysat/viable.h

@@ -122,18 +122,24 @@ namespace polysat {
         class iterator {
             entry* curr = nullptr;
             bool   visited = false;
+            unsigned idx = 0;
         public:
             iterator(entry* curr, bool visited) : 
                 curr(curr), visited(visited || !curr) {}
 
             iterator& operator++() {
-                visited = true;
+                if (idx < curr->side_cond.size()) 
-                curr = curr->next();
+                    ++idx;
+                else {
+                    idx = 0;
+                    visited = true;
+                    curr = curr->next();
+                }
                 return *this;
             }
 
             signed_constraint& operator*() { 
-                return curr->src; 
+                return idx < curr->side_cond.size() ? curr->side_cond[idx] : curr->src;
             }
 
             bool operator==(iterator const& other) const {