wip

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/explain.cpp

@@ -35,6 +35,7 @@ namespace polysat {
             // (this condition might be too strict, but we use it for now to prevent looping)
             if (b.degree(v) <= r.degree(v))
                 return {};
+            SASSERT(r.degree(v) < b.degree(v));
             unsigned const lvl = std::max(c1->level(), c2->level());
             signed_constraint c = cm().eq(lvl, r);
             LOG("resolved: " << c << "        currently false? " << c.is_currently_false(s()));

src/math/polysat/solver.cpp

@@ -455,6 +455,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());
@@ -629,17 +631,9 @@ namespace polysat {
 
         backjump(lvl - 1);
 
-        // TODO: we need to decide_bool on the clause (learn_lemma takes care of this).
+        // The justification for this restriction is the guessed constraint from the lemma.
-        //       if the lemma was asserting, then this will propagate the last literal. otherwise we do the enumerative guessing as normal.
+        // cjust[v] will be updated accordingly by decide_bool.
-        //       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...)
         m_viable.add_non_viable(v, val);
-
         learn_lemma(v, std::move(lemma));
 
         if (is_conflict()) {
@@ -788,8 +782,13 @@ namespace polysat {
         if (!lemma)
             return;
         LOG("Lemma: " << show_deref(lemma));
-        for (sat::literal l : *lemma)
+        for (sat::literal lit : *lemma) {
-            LOG("   Literal " << l << " is: " << m_constraints.lookup(l));
+            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();
     }