Propagate value assignments discovered by the slicing e-graph

src/math/polysat/conflict.cpp

@@ -468,9 +468,9 @@ namespace polysat {
         m_resolver->infer_lemmas_for_value(v, *this);
     }
 
-    void conflict::resolve_value(pvar v) {
+    void conflict::resolve_value_by_viable(pvar v) {
         SASSERT(contains_pvar(v));
-        SASSERT(s.m_justification[v].is_propagation());
+        SASSERT(s.m_justification[v].is_propagation_by_viable());
 
         s.inc_activity(v);
 
@@ -489,6 +489,26 @@ namespace polysat {
         revert_pvar(v);
     }
 
+    void conflict::resolve_value_by_slicing(pvar v) {
+        SASSERT(contains_pvar(v));
+        SASSERT(s.m_justification[v].is_propagation_by_slicing());
+
+        s.inc_activity(v);
+
+        m_vars.remove(v);
+        s.m_slicing.explain_value(v,
+            [this](sat::literal lit) {
+                insert_or_replace(s.lit2cnstr(lit));
+            },
+            [this](pvar w) {
+                SASSERT(s.is_assigned(w));
+                m_vars.insert(w);
+            });
+        // logger().log(inf_resolve_value(s, v)); TODO
+
+        revert_pvar(v);
+    }
+
     clause_ref conflict::build_lemma() {
         LOG_H3("Build lemma from core");
         LOG("core: " << *this);
@@ -619,8 +639,8 @@ namespace polysat {
                 todo_vars.pop_back();
                 IF_VERBOSE(11, verbose_stream() << "Handling v" << v << "\n";);
 
-                SASSERT(s.m_justification[v].is_propagation());  // no decisions at base level
+                auto const& j = s.m_justification[v];
-
+                if (j.is_propagation_by_viable()) {
                     for (signed_constraint c : s.m_viable.get_constraints(v))
                         enqueue_constraint(c);
                     for (auto const& i : s.m_viable.units(v)) {
@@ -628,6 +648,14 @@ namespace polysat {
                         enqueue_constraint(s.eq(i.hi(), i.hi_val()));
                     }
                 }
+                else if (j.is_propagation_by_slicing()) {
+                    s.m_slicing.explain_value(v, enqueue_lit, enqueue_var);
+                }
+                else {
+                    // no decisions at base level
+                    UNREACHABLE();
+                }
+            }
             while (!todo_lits.empty()) {
                 sat::literal const lit = todo_lits.back();
                 todo_lits.pop_back();
@@ -670,7 +698,7 @@ namespace polysat {
     std::ostream& conflict::display(std::ostream& out) const {
         out << "lvl " << m_level;
         if (!m_dep.is_null())
-            out << "dep " << m_dep;
+            out << " dep " << m_dep;
         char const* sep = " ";
         for (auto c : *this)
             out << sep << c->bvar2string() << " " << c, sep = " ; ";

src/math/polysat/conflict.h

@@ -191,7 +191,9 @@ namespace polysat {
         void resolve_evaluated(sat::literal lit);
 
         /** Perform resolution with "v = value <- ..." */
-        void resolve_value(pvar v);
+        void resolve_value_by_viable(pvar v);
+
+        void resolve_value_by_slicing(pvar v);
 
         /** Revert variable assignment, add auxiliary lemmas for the reverted variable */
         void revert_pvar(pvar v);

src/math/polysat/justification.cpp

@@ -8,7 +8,7 @@ Module Name:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Jakob Rath 2021-04-06
 
 --*/
 
@@ -22,8 +22,10 @@ namespace polysat {
             return out << "unassigned";
         case justification_k::decision:
             return out << "decision @ " << level();
-        case justification_k::propagation:
+        case justification_k::propagation_by_viable:
-            return out << "propagation @ " << level();
+            return out << "propagation by viable @ " << level();
+        case justification_k::propagation_by_slicing:
+            return out << "propagation by slicing @ " << level();
         }
         UNREACHABLE();
         return out;

src/math/polysat/justification.h

@@ -8,7 +8,7 @@ Module Name:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Jakob Rath 2021-04-06
 
 --*/
 #pragma once
@@ -21,7 +21,12 @@ namespace polysat {
     /**
      * Justification kind for a variable assignment.
      */
-    enum justification_k { unassigned, decision, propagation };
+    enum class justification_k {
+        unassigned,
+        decision,
+        propagation_by_viable,
+        propagation_by_slicing,
+    };
 
     class justification {
         justification_k m_kind;
@@ -31,10 +36,12 @@ namespace polysat {
         justification(): m_kind(justification_k::unassigned) {}
         static justification unassigned() { return justification(justification_k::unassigned, 0); }
         static justification decision(unsigned lvl) { return justification(justification_k::decision, lvl); }
-        static justification propagation(unsigned lvl) { return justification(justification_k::propagation, lvl); }
+        static justification propagation_by_viable(unsigned lvl) { return justification(justification_k::propagation_by_viable, lvl); }
+        static justification propagation_by_slicing(unsigned lvl) { return justification(justification_k::propagation_by_slicing, lvl); }
         bool is_decision() const { return m_kind == justification_k::decision; }
         bool is_unassigned() const { return m_kind == justification_k::unassigned; }
-        bool is_propagation() const { return m_kind == justification_k::propagation; }
+        bool is_propagation_by_viable() const { return m_kind == justification_k::propagation_by_viable; }
+        bool is_propagation_by_slicing() const { return m_kind == justification_k::propagation_by_slicing; }
         justification_k kind() const { return m_kind; }
         unsigned level() const { /* SASSERT(!is_unassigned()); */ return m_level; }   // TODO: check why this assertion triggers...
         std::ostream& display(std::ostream& out) const;

src/math/polysat/search_state.cpp

@@ -30,8 +30,10 @@ namespace polysat {
             switch (j.kind()) {
             case justification_k::decision:
                 return out << " by decision";
-            case justification_k::propagation:
+            case justification_k::propagation_by_viable:
                 return out << " by " << viable::var_pp(s.m_viable, var);
+            case justification_k::propagation_by_slicing:
+                return out << " by slicing (detailed output is TODO)";
             case justification_k::unassigned:
                 return out << " unassigned";
             }

src/math/polysat/slicing.cpp

@@ -718,6 +718,35 @@ namespace polysat {
         return cb.build();
     }
 
+    void slicing::explain_value(pvar v, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {
+        SASSERT(m_solver.m_justification[v].is_propagation_by_slicing());
+        SASSERT(invariant());
+        SASSERT(m_marked_lits.empty());
+
+        enode* sv = var2slice(v);
+        enode* rv = sv->get_root();
+        SASSERT(is_value(rv));  // by convention, value slices are always the root; and this method may only be called if v is equivalent to a value in the egraph.
+
+        SASSERT(m_tmp_deps.empty());
+        explain_equal(sv, rv, m_tmp_deps);
+
+        for (void* dp : m_tmp_deps) {
+            dep_t const d = dep_t::decode(dp);
+            if (d.is_null())
+                continue;
+            if (d.is_lit())
+                on_lit(d.lit());
+            else {
+                SASSERT(d.is_value());
+                if (get_dep_lit(d) == sat::null_literal)
+                    on_var(get_dep_var(d));
+                else
+                    on_lit(get_dep_lit(d));
+            }
+        }
+        m_tmp_deps.reset();
+    }
+
     bool slicing::find_range_in_ancestor(enode* s, enode* a, unsigned& out_hi, unsigned& out_lo) {
         out_hi = width(s) - 1;
         out_lo = 0;
@@ -747,10 +776,12 @@ namespace polysat {
                 pvar const v = slice2var(n);
                 if (v == null_var)
                     continue;
+                if (m_solver.is_assigned(v))
+                    continue;
                 LOG("on_merge: v" << v << " := " << get_value(root));
-                // TODO: notify solver about value
+                m_solver.assign_propagate_by_slicing(v, get_value(root));
                 // TODO: congruence? what if all base slices of a variable are equivalent to values?
-                //          -> could track, for each slice, how many of its base slices are (not) equivalent to values. (update on split and merge)
+                //          -> could track, for each variable, how many of its base slices are (not) equivalent to values. (update on split and merge)
             }
         }
     }

src/math/polysat/slicing.h

@@ -313,6 +313,9 @@ namespace polysat {
         /** Extract conflict clause */
         clause_ref build_conflict_clause();
 
+        /** Explain why slicing has propagated the value assignment for v */
+        void explain_value(pvar v, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
+
         /** For a given variable v, find the set of variables w such that w = v[|w|:0]. */
         void collect_simple_overlaps(pvar v, pvar_vector& out);
 

src/math/polysat/solver.cpp

@@ -863,7 +863,7 @@ namespace polysat {
             // The fallback solver currently does not detect propagations, because we would need to handle justifications differently.
             // However, this case may still occur if during viable::intersect, we run into the refinement budget,
             // but here, we continue refinement and actually succeed until propagation.
-            assign_propagate(v, val);
+            assign_propagate_by_viable(v, val);
             return;
         case find_t::multiple:
             j = justification::decision(m_level + 1);
@@ -882,11 +882,7 @@ namespace polysat {
         assign_core(v, val, j);
     }
 
-    void solver::assign_propagate(pvar v, rational const& val) {
+    void solver::assign_propagate_by_viable(pvar v, rational const& val) {
-        LOG("Propagation: " << assignment_pp(*this, v, val));
-        SASSERT(!is_assigned(v));
-        SASSERT(m_viable.is_viable(v, val));
-        m_free_pvars.del_var_eh(v);
         // NOTE:
         // The propagation v := val might depend on a lower level than the current level (m_level).
         // This can happen if the constraints that cause the propagation have been bool-propagated at an earlier level,
@@ -901,14 +897,23 @@ namespace polysat {
                 if (is_assigned(w))  // TODO: question of which variables are relevant. e.g., v1 > v0 implies v1 > 0 without dependency on v0. maybe add a lemma v1 > v0 --> v1 > 0 on the top level to reduce false variable dependencies? instead of handling such special cases separately everywhere.
                     lvl = std::max(lvl, get_level(w));
         }
-        // NOTE: we do not have to check the univariate solver here.
+        assign_propagate(v, val, justification::propagation_by_viable(lvl));
-        //       Since we propagate, this means at most the single value 'val' is viable.
-        //       If it is not actually viable, the propagation loop will find out and enter the conflict state.
-        //       (However, if we do check here, we might find the conflict earlier. Might be worth a try.)
-        assign_core(v, val, justification::propagation(lvl));
     }
 
-    void solver::assign_core(pvar v, rational const& val, justification const& j) {
+    void solver::assign_propagate_by_slicing(pvar v, rational const& val) {
+        unsigned lvl = m_level;  // TODO: can the actual level be lower?
+        assign_propagate(v, val, justification::propagation_by_slicing(lvl));
+    }
+
+    void solver::assign_propagate(pvar v, rational const& val, justification j) {
+        LOG("Propagation: " << assignment_pp(*this, v, val));
+        SASSERT(!is_assigned(v));
+        SASSERT(j.is_propagation_by_viable() || j.is_propagation_by_slicing());
+        m_free_pvars.del_var_eh(v);
+        assign_core(v, val, j);
+    }
+
+    void solver::assign_core(pvar v, rational const& val, justification j) {
         VERIFY(!is_assigned(v));
         if (j.is_decision())
             ++m_stats.m_num_decisions;
@@ -916,7 +921,7 @@ namespace polysat {
             ++m_stats.m_num_propagations;
         LOG(assignment_pp(*this, v, val) << " by " << j);
         SASSERT(m_viable.is_viable(v, val));
-        SASSERT(j.is_decision() || j.is_propagation());
+        SASSERT(j.is_decision() || j.is_propagation_by_viable() || j.is_propagation_by_slicing());
         SASSERT(j.level() <= m_level);
         SASSERT(!is_assigned(v));
         SASSERT(all_of(get_assignment(), [v](auto p) { return p.first != v; }));
@@ -956,8 +961,13 @@ namespace polysat {
                     revert_decision(v);
                     return;
                 }
-                SASSERT(j.is_propagation());
+                if (j.is_propagation_by_viable())
-                m_conflict.resolve_value(v);
+                    m_conflict.resolve_value_by_viable(v);
+                else if (j.is_propagation_by_slicing())
+                    m_conflict.resolve_value_by_slicing(v);
+                else {
+                    UNREACHABLE();
+                }
             }
             else {
                 // Resolve over boolean literal
@@ -1102,6 +1112,7 @@ namespace polysat {
             appraise_lemma(lemmas.back());
         }
         if (!best_lemma) {
+            verbose_stream() << "ERROR: no best_lemma\n";
             display(verbose_stream());
             verbose_stream() << "conflict: " << m_conflict << "\n";
             verbose_stream() << "no lemma\n";
@@ -1110,7 +1121,6 @@ namespace polysat {
                 for (sat::literal lit : *cl)
                     verbose_stream() << "    " << lit_pp(*this, lit) << "\n";
             }
-            
         }
         SASSERT(best_score < lemma_score::max());
         VERIFY(best_lemma);
@@ -1581,9 +1591,11 @@ namespace polysat {
                 pvar v = item.var();
                 auto const& j = m_justification[v];
                 out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level() << " ";
-                if (j.is_propagation())
+                if (j.is_propagation_by_viable())
                     for (auto const& c : m_viable.get_constraints(v))
                         out << c << " ";
+                if (j.is_propagation_by_slicing())
+                    out << "by slicing (detailed output is TODO)";
                 out << "\n";
             }
             else {

src/math/polysat/solver.h

@@ -262,8 +262,10 @@ namespace polysat {
         void activate_constraint(signed_constraint c);
         unsigned level(sat::literal lit, clause const& cl);
 
-        void assign_propagate(pvar v, rational const& val);
+        void assign_propagate_by_viable(pvar v, rational const& val);
-        void assign_core(pvar v, rational const& val, justification const& j);
+        void assign_propagate_by_slicing(pvar v, rational const& val);
+        void assign_propagate(pvar v, rational const& val, justification j);
+        void assign_core(pvar v, rational const& val, justification j);
         bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
         bool is_decision(pvar v) const { return m_justification[v].is_decision(); }
 

src/math/polysat/types.h

@@ -67,8 +67,12 @@ namespace polysat {
     inline bool operator!=(dependency const& d1, dependency const& d2) { return d1.val() != d2.val(); }
 
     inline std::ostream& operator<<(std::ostream& out, dependency const& d) {
-        out << "dep(" << d.val() << ")";
+        out << "dep(";
-        return out;
+        if (d.is_null())
+            out << "<null>";
+        else
+            out << d.val();
+        return out << ")";
     }
 
 }

src/math/polysat/viable.cpp

@@ -227,7 +227,7 @@ namespace polysat {
             s.try_assign_eval(s.eq(i.lo(), i.lo_val()));
             s.try_assign_eval(s.eq(i.hi(), i.hi_val()));
         }
-        s.assign_propagate(v, val);
+        s.assign_propagate_by_viable(v, val);
     }
 
     bool viable::intersect(pvar v, signed_constraint const& c) {