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

src/math/polysat/clause.h

@@ -34,7 +34,7 @@ namespace polysat {
 
         unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
         unsigned m_level;
-        unsigned m_next_guess = 0;  // next guess for enumerative backtracking
+        pvar m_justified_var = null_var;  // The variable that was restricted by learning this lemma.
         p_dependency_ref m_dep;
         sat::literal_vector m_literals;
 
@@ -62,6 +62,9 @@ namespace polysat {
         p_dependency* dep() const { return m_dep; }
         unsigned level() const { return m_level; }
 
+        pvar justified_var() const { return m_justified_var; }
+        void set_justified_var(pvar v) { SASSERT(m_justified_var == null_var); m_justified_var = v; }
+
         bool empty() const { return m_literals.empty(); }
         unsigned size() const { return m_literals.size(); }
         sat::literal operator[](unsigned idx) const { return m_literals[idx]; }
@@ -73,11 +76,6 @@ namespace polysat {
         bool is_always_false(solver& s) const;
         bool is_currently_false(solver& s) const;
 
-        unsigned next_guess() {
-            SASSERT(m_next_guess < size());
-            return m_next_guess++;
-        }
-
         std::ostream& display(std::ostream& out) const;
     };
 

src/math/polysat/clause_builder.cpp

@@ -55,13 +55,4 @@ namespace polysat {
         m_literals.push_back(c.blit());
     }
 
-    // void clause_builder::push_new_constraint(signed_constraint c) {
-    //     SASSERT(c);
-    //     if (c.is_always_false())
-    //         return;
-    //     m_level = std::max(m_level, c->level());
-    //     m_literals.push_back(c.blit());
-    //     m_new_constraints.push_back(c.get());
-    // }
-
 }

src/math/polysat/conflict_core.cpp

@@ -65,6 +65,7 @@ namespace polysat {
 
     void conflict_core::insert(signed_constraint c) {
         SASSERT(!empty());  // should use set() to enter conflict state
+        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())

src/math/polysat/solver.cpp

@@ -576,6 +576,7 @@ namespace polysat {
             return;
         SASSERT(lemma->size() > 0);
         SASSERT(m_conflict_level <= m_justification[v].level());  // ???
+        lemma->set_justified_var(v);
         clause* cl = lemma.get();
         add_lemma(std::move(lemma));
         if (cl->size() == 1) {
@@ -589,7 +590,6 @@ namespace polysat {
             sat::literal lit = decide_bool(*cl);
             SASSERT(lit != sat::null_literal);
             signed_constraint c = m_constraints.lookup(lit);
-            push_cjust(v, c);   // TODO: Ok, this works for the first guess. but what if we update the guess later?? the next guess should then be part of cjust[v] instead.
         }
     }
 
@@ -622,6 +622,9 @@ namespace polysat {
         }
         LOG_V("num_choices: " << num_choices);
 
+        signed_constraint c = m_constraints.lookup(choice);
+        push_cjust(lemma.justified_var(), c);
+
         if (num_choices == 0) {
             // This case may happen when all undefined literals are false under the current variable assignment.
             // TODO: The question is whether such lemmas should be generated? Check test_monot() for such a case.
@@ -709,7 +712,6 @@ namespace polysat {
         m_conflict.reset();
 
         bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit);
-        // bool contains_lit = std::any_of(reason_builder->begin(), reason_builder->end(), [lit](auto reason_lit) { return reason_lit == ~lit; });
         if (!contains_lit) {
             // At this point, we do not have ~lit in the reason.
             // For now, we simply add it (thus weakening the reason)
@@ -893,18 +895,6 @@ namespace polysat {
         return m_base_levels.empty() ? 0 : m_base_levels.back();
     }
 
-    // bool solver::active_at_base_level(sat::bool_var bvar) const {
-    //     // NOTE: this active_at_base_level is actually not what we want!!!
-    //     //          first of all, it might not really be a base level: could be a non-base level between previous base levels.
-    //     //          in that case, how do we determine the right dependencies???
-    //     //          secondly, we are interested in "unit clauses", not as much whether we assigned something on the base level...
-    //     //          TODO: however, propagating stuff at the base level... need to be careful with dependencies there... might need to turn all base-level propagations into unit clauses...
-    //     VERIFY(false);
-    //     // bool res = m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level();
-    //     // SASSERT_EQ(res, !!m_constraints.lookup(bvar)->unit_clause());
-    //     // return res;
-    // }
-
     bool solver::try_eval(pdd const& p, rational& out_value) const {
         pdd r = p.subst_val(assignment());
         if (r.is_val())