Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

src/math/polysat/conflict_core.cpp

@@ -16,11 +16,6 @@ Notes:
 
  TODO: try a final core reduction step or other core minimization
 
-TODO: fallback lemma is redundant:
-      The core lemma uses m_vars and m_conflict directly instead of walking the stack.
-      It should be an invariant that the core is false (the negation of the core is valid modulo assertions).
-      The fallback lemma prunes at least the last value assignment.
-
 TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core.
       (works currently if x is unassigned; for other cases we would need extra info from constraint::is_currently_false)
 
@@ -209,41 +204,9 @@ namespace polysat {
         s().propagate_bool_at(active_level, c.blit(), cl);
     }
 
-    /** Create fallback lemma that excludes the current search state */
+    clause_builder conflict_core::build_core_lemma() {
-    /**
-    * revisit: can prune literals further by slicing base on cone of influence
-    * based on marked literals/variables on the stack. Only decisions that affect
-    * marked items need to be included.
-    */
-    clause_builder conflict_core::build_fallback_lemma(unsigned lvl) {
-        LOG_H3("Creating fallback lemma for level " << lvl);
-        LOG_V("m_search: " << s().m_search);
-        clause_builder lemma(s());
-        unsigned todo = lvl;
-        unsigned i = 0;
-        while (todo > 0) {
-            auto const& item = s().m_search[i++];
-            if (!s().is_decision(item))
-                continue;
-            LOG_V("Adding: " << item);
-            if (item.is_assignment()) {
-                pvar v = item.var();
-                auto c = ~s().eq(s().var(v), s().get_value(v));
-                cm().ensure_bvar(c.get());
-                lemma.push(c.blit());
-            } else {
-                sat::literal lit = item.lit();
-                lemma.push(~lit);
-            }
-            --todo;
-        }
-        return lemma;
-    }
-
-    clause_builder conflict_core::build_core_lemma(unsigned model_level) {
         LOG_H3("Build lemma from core");
         LOG("core: " << *this);
-        LOG("model_level: " << model_level);
         clause_builder lemma(s());
 
         for (auto c : m_constraints) {
@@ -258,8 +221,6 @@ namespace polysat {
             SASSERT(s().is_assigned(v));  // note that we may have added too many variables: e.g., y disappears in x*y if x=0
             if (!s().is_assigned(v))
                 continue;
-            if (s().get_level(v) > model_level)
-                continue;
             auto diseq = ~s().eq(s().var(v), s().get_value(v));
             cm().ensure_bvar(diseq.get());
             lemma.push(diseq);
@@ -268,13 +229,11 @@ namespace polysat {
         return lemma;
     }
 
-    clause_builder conflict_core::build_lemma(unsigned reverted_level) {
+    clause_builder conflict_core::build_lemma() {
-        if (!is_bailout())
+        if (m_bailout_lemma)
-            return build_core_lemma(reverted_level);
-        else if (m_bailout_lemma)
             return *std::move(m_bailout_lemma);
         else
-            return build_fallback_lemma(reverted_level);
+            return build_core_lemma();
     }
 
     bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
@@ -298,18 +257,23 @@ namespace polysat {
         for (auto c : cjust_v) 
             insert(c);        
 
-        for (auto* engine : ex_engines)
+        if (!is_bailout()) {
-            if (engine->try_explain(v, *this))
+            for (auto* engine : ex_engines)
-                return true;
+                if (engine->try_explain(v, *this))
+                    return true;
 
-        // No value resolution method was successful => fall back to saturation and variable elimination
+            // No value resolution method was successful => fall back to saturation and variable elimination
-        while (s().inc()) { 
+            while (s().inc()) { 
-            // TODO: as a last resort, substitute v by m_value[v]?
+                // TODO: as a last resort, substitute v by m_value[v]?
-            if (try_eliminate(v))
+                if (try_eliminate(v))
-                return true;
+                    return true;
-            if (!try_saturate(v))
+                if (!try_saturate(v))
-                break;
+                    break;
+            }
+
+            set_bailout();
         }
+
         m_vars.insert(v);
         return false;
     }

src/math/polysat/conflict_core.h

@@ -68,7 +68,7 @@ namespace polysat {
         pvar conflict_var() const { return m_conflict_var; }
 
         bool is_bailout() const { return m_bailout; }
-        void set_bailout() { SASSERT(!is_bailout()); m_bailout = true; }
+        void set_bailout() { SASSERT(!is_bailout()); m_bailout = true; s().m_stats.m_num_bailouts++; }
 
         bool empty() const {
             return m_constraints.empty() && m_vars.empty() && m_literals.empty() && m_conflict_var == null_var;
@@ -105,9 +105,8 @@ namespace polysat {
         bool resolve_value(pvar v, vector<signed_constraint> const& cjust_v);
 
         /** Convert the core into a lemma to be learned. */
-        clause_builder build_lemma(unsigned reverted_level);
+        clause_builder build_lemma();
-        clause_builder build_core_lemma(unsigned model_level);
+        clause_builder build_core_lemma();
-        clause_builder build_fallback_lemma(unsigned lvl);
 
         bool try_eliminate(pvar v);
         bool try_saturate(pvar v);

src/math/polysat/solver.cpp

@@ -495,18 +495,7 @@ namespace polysat {
 
     /** Conflict resolution case where propagation 'v := ...' is on top of the stack */
     void solver::resolve_value(pvar v) {
-        if (m_conflict.is_bailout()) {
+        m_conflict.resolve_value(v, m_cjust[v]);
-            for (auto c : m_cjust[v])
-                m_conflict.insert(c);
-            return;
-        }
-
-        // Value Resolution
-        if (!m_conflict.resolve_value(v, m_cjust[v])) {
-            // Failed to resolve => bail out
-            ++m_stats.m_num_bailouts;
-            m_conflict.set_bailout();
-        }
     }
 
     /** Conflict resolution case where boolean literal 'lit' is on top of the stack */
@@ -600,12 +589,11 @@ namespace polysat {
         rational val = m_value[v];
         LOG_H3("Reverting decision: pvar " << v << " := " << val);
         SASSERT(m_justification[v].is_decision());
-        unsigned const lvl = m_justification[v].level();
 
-        clause_ref lemma = m_conflict.build_lemma(lvl).build();
+        clause_ref lemma = m_conflict.build_lemma().build();
         m_conflict.reset();
 
-        backjump(lvl - 1);
+        backjump(m_justification[v].level() - 1);
 
         // The justification for this restriction is the guessed constraint from the lemma.
         // cjust[v] will be updated accordingly by decide_bool.
@@ -653,9 +641,8 @@ namespace polysat {
         // - propagation of L' from L
         //      (L')^{L' \/ ¬L \/ ...}
         //      again L is in core, unless we core-reduced it away
-        unsigned const lvl = m_bvars.level(var);
 
-        clause_builder reason_builder = m_conflict.build_lemma(lvl);
+        clause_builder reason_builder = m_conflict.build_lemma();
         m_conflict.reset();
 
         bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit);
@@ -679,7 +666,7 @@ namespace polysat {
         clause* lemma = m_bvars.lemma(var);  // need to grab this while 'lit' is still assigned
         SASSERT(lemma);
 
-        backjump(lvl - 1);
+        backjump(m_bvars.level(var) - 1);
 
         add_lemma(reason);
         propagate_bool(~lit, reason.get());