merge

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

src/math/polysat/conflict_core.cpp

@@ -80,7 +80,7 @@ namespace polysat {
 
     void conflict_core::insert(signed_constraint c) {
         SASSERT(!empty());  // should use set() to enter conflict state
-        LOG("inserting:" << c);
+        LOG("inserting: " << c);
         // Skip trivial constraints
         // (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology)
         if (c.is_always_true())
@@ -156,7 +156,10 @@ namespace polysat {
         auto& premises = it->m_value;
         clause_builder c_lemma(*m_solver);
         for (auto premise : premises) {
+            cm().ensure_bvar(premise.get());
+            // keep(premise);
             handle_saturation_premises(premise);
+            SASSERT(premise->has_bvar());
             c_lemma.push(~premise.blit());
             active_level = std::max(active_level, m_solver->m_bvars.level(premise.blit()));
         }

src/math/polysat/search_state.h

@@ -74,4 +74,60 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); }
 
+
+    // Go backwards over the search_state
+    class search_iterator {
+
+        search_state*   m_search;
+
+        unsigned current;
+        unsigned first;
+
+        struct idx_range {
+            unsigned current;
+            unsigned first;  // highest index + 1
+        };
+        vector<idx_range>     m_index_stack;
+
+    public:
+        search_iterator(search_state& search):
+            m_search(&search) {
+            first = m_search->size();
+            current = first;  // we start one before the beginning, then it also works for empty m_search
+        }
+
+        search_item const& operator*() const {
+            return (*m_search)[current];
+        }
+
+        unsigned last() {
+            return m_index_stack.empty() ? 0 : m_index_stack.back().first;
+        }
+
+        bool next() {
+            if (current > last()) {
+                --current;
+                return true;
+            }
+            else {
+                SASSERT(current == last());
+                if (m_index_stack.empty())
+                    return false;
+                current = m_index_stack.back().current;
+                first = m_index_stack.back().first;
+                m_index_stack.pop_back();
+                return true;
+            }
+        }
+
+        // to be called after all saturations for a step are done
+        void push_block() {
+            if (first != m_search->size()) {
+                m_index_stack.push_back({current, first});
+                first = m_search->size();
+                current = first - 1;
+            }
+        }
+    };
+
 }

src/math/polysat/solver.cpp

@@ -446,6 +446,8 @@ namespace polysat {
         LOG_H2("Resolve conflict");
         LOG("\n" << *this);
         LOG("search state: " << m_search);
+        for (pvar v = 0; v < m_cjust.size(); ++v)
+            LOG("cjust[v" << v << "]: " << m_cjust[v]);
         ++m_stats.m_num_conflicts;
 
         SASSERT(is_conflict());
@@ -461,9 +463,10 @@ namespace polysat {
             set_marks(m_conflict);
         }
 
-        for (unsigned i = m_search.size(); i-- > 0; ) {
+        search_iterator search_it(m_search);
+        while (search_it.next()) {
             LOG("Conflict: " << m_conflict);
-            auto const& item = m_search[i];
+            auto const& item = *search_it;
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
@@ -620,17 +623,9 @@ namespace polysat {
 
         backjump(lvl - 1);
 
-        // TODO: we need to decide_bool on the clause (learn_lemma takes care of this).
-        //       if the lemma was asserting, then this will propagate the last literal. otherwise we do the enumerative guessing as normal.
-        //       we need to exclude the current value of v. narrowing of the guessed constraint *should* take care of it but we cannot count on that.
-
-        // TODO: what do we add as 'cjust' for this restriction? the guessed
-        // constraint from the lemma should be the right choice. but, how to
-        // carry this over when the guess is reverted? need to remember the
-        // variable 'v' somewhere on the lemma.
-        // the restriction v /= val can live before the guess... (probably should ensure that the guess stays close to the current position in the stack to prevent confusion...)
+        // The justification for this restriction is the guessed constraint from the lemma.
+        // cjust[v] will be updated accordingly by decide_bool.
         m_viable.add_non_viable(v, val);
-
         learn_lemma(v, std::move(lemma));
 
         if (is_conflict()) {
@@ -779,8 +774,13 @@ namespace polysat {
         if (!lemma)
             return;
         LOG("Lemma: " << show_deref(lemma));
-        for (sat::literal l : *lemma)
-            LOG("   Literal " << l << " is: " << m_constraints.lookup(l));
+        for (sat::literal lit : *lemma) {
+            LOG("   Literal " << lit << " is: " << m_constraints.lookup(lit));
+            // TODO: fully evaluated constraints must be put onto the stack as propagations.
+            signed_constraint c = m_constraints.lookup(lit);
+            SASSERT(m_bvars.is_assigned(lit) && !c.is_currently_false(*this));
+            SASSERT(m_bvars.is_assigned(lit) && !c.is_currently_true(*this));
+        }
         SASSERT(lemma->size() > 0);
         clause* cl = m_constraints.store(std::move(lemma));
         m_redundant_clauses.push_back(cl);

src/math/polysat/ule_constraint.cpp

@@ -110,8 +110,11 @@ namespace polysat {
     bool ule_constraint::is_currently_true(solver& s, bool is_positive) {
         auto p = lhs().subst_val(s.assignment());
         auto q = rhs().subst_val(s.assignment());
-        if (is_positive)
+        if (is_positive) {
+            if (p.is_zero())
+                return true;
             return p.is_val() && q.is_val() && p.val() <= q.val();
+        }
         else 
             return p.is_val() && q.is_val() && p.val() > q.val();
     }