levels/crit

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

src/math/polysat/clause.cpp

@@ -17,9 +17,8 @@ Author:
 
 namespace polysat {
 
-    clause_ref clause::from_unit(signed_constraint c, p_dependency_ref d) {
+    clause_ref clause::from_unit(unsigned lvl, signed_constraint c, p_dependency_ref d) {
         SASSERT(c->has_bvar());
-        unsigned const lvl = 0; // level from literal?
         sat::literal_vector lits;
         lits.push_back(c.blit());
         return clause::from_literals(lvl, std::move(d), std::move(lits));

src/math/polysat/clause.h

@@ -56,7 +56,7 @@ namespace polysat {
         void inc_ref() { m_ref_count++; }
         void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
 
-        static clause_ref from_unit(signed_constraint c, p_dependency_ref d);
+        static clause_ref from_unit(unsigned lvl, signed_constraint c, p_dependency_ref d);
         static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals);
 
         p_dependency* dep() const { return m_dep; }

src/math/polysat/clause_builder.cpp

@@ -53,6 +53,7 @@ namespace polysat {
         SASSERT(c->has_bvar());
         if (c->unit_clause()) {
             add_dependency(c->unit_dep());
+            m_level = std::max(m_level, c->unit_clause()->level());
             return;
         }       
         m_literals.push_back(c.blit());

src/math/polysat/saturation.cpp

@@ -62,18 +62,19 @@ namespace polysat {
     * Propagate c. It is added to reason and core all other literals in reason are false in current stack.
     * The lemmas outlines in the rules are valid and therefore c is implied.
     */
-    bool inf_saturate::propagate(conflict_core& core, signed_constraint& c, clause_builder& reason) {        
+    bool inf_saturate::propagate(conflict_core& core, inequality const& crit, signed_constraint& c, clause_builder& reason) {        
         if (c.is_currently_true(s()))
             return false;
         core.insert(c);
         reason.push(c);
+        // TODO core.erase(crit.as_signed_constraint());
         s().propagate_bool(c.blit(), reason.build().get());
         return true;
     }
 
-    bool inf_saturate::propagate(conflict_core& core, bool is_strict, pdd const& lhs, pdd const& rhs, clause_builder& reason) {
+    bool inf_saturate::propagate(conflict_core& core, inequality const& crit, bool is_strict, pdd const& lhs, pdd const& rhs, clause_builder& reason) {
         signed_constraint c = ineq(is_strict, lhs, rhs);
-        return propagate(core, c, reason);
+        return propagate(core, crit, c, reason);
     }
 
     /// Add premises for Ω*(x, y)
@@ -267,7 +268,7 @@ namespace polysat {
             reason.push(cm().eq(x - x.manager().mk_val(rational(0))));
         reason.push(~c.as_signed_constraint());
         push_omega(reason, x, y);        
-        return propagate(core, c.is_strict, y, z, reason);
+        return propagate(core, c, c.is_strict, y, z, reason);
     }
 
     /// [y] z' <= y /\ zx > yx  ==>  Ω*(x,y) \/ zx > z'x
@@ -287,7 +288,7 @@ namespace polysat {
         reason.push(~yx_l_zx.as_signed_constraint());
         push_omega(reason, x, y);
         // z'x <= zx
-        return propagate(core, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, reason);
+        return propagate(core, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, reason);
     }
 
     bool inf_saturate::try_ugt_y(pvar v, conflict_core& core, inequality const& c) {
@@ -330,7 +331,7 @@ namespace polysat {
         reason.push(~x_l_z.as_signed_constraint());
         reason.push(~y_l_ax.as_signed_constraint());
         push_omega(reason, a, z);
-        return propagate(core, x_l_z.is_strict || y_l_ax.is_strict, y, a * z, reason);
+        return propagate(core, y_l_ax, x_l_z.is_strict || y_l_ax.is_strict, y, a * z, reason);
     }
 
 
@@ -360,7 +361,7 @@ namespace polysat {
         reason.push(~d.as_signed_constraint());
         push_omega(reason, x, y_prime);
         // yx <= y'x
-        return propagate(core, c.is_strict || d.is_strict, y * x, y_prime * x, reason);
+        return propagate(core, d, c.is_strict || d.is_strict, y * x, y_prime * x, reason);
     }
 
 

src/math/polysat/saturation.h

@@ -41,8 +41,8 @@ namespace polysat {
         void push_omega(clause_builder& reason, pdd const& x, pdd const& y);
         void push_omega_bisect(clause_builder& reason, pdd const& x, rational x_max, pdd const& y, rational y_max);
         signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
-        bool propagate(conflict_core& core, signed_constraint& c, clause_builder& reason);
+        bool propagate(conflict_core& core, inequality const& crit, signed_constraint& c, clause_builder& reason);
-        bool propagate(conflict_core& core, bool strict, pdd const& lhs, pdd const& rhs, clause_builder& reason);
+        bool propagate(conflict_core& core, inequality const& crit, bool strict, pdd const& lhs, pdd const& rhs, clause_builder& reason);
 
         bool try_ugt_x(pvar v, conflict_core& core, inequality const& c);
 

src/math/polysat/solver.cpp

@@ -145,7 +145,7 @@ namespace polysat {
         SASSERT(c);
         SASSERT(activate || dep != null_dependency);  // if we don't activate the constraint, we need the dependency to access it again later.
         m_constraints.ensure_bvar(c.get());
-        clause* unit = m_constraints.store(clause::from_unit(c, mk_dep_ref(dep)));
+        clause* unit = m_constraints.store(clause::from_unit(m_level, c, mk_dep_ref(dep)));
         c->set_unit_clause(unit);
         if (dep != null_dependency)
             m_constraints.register_external(c.get());