na

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

src/math/polysat/boolean.cpp

@@ -60,6 +60,26 @@ namespace polysat {
         // m_unused.push_back(var);
     }
 
+    void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) {
+        LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason);
+        assign(lit, lvl, &reason, nullptr, null_dependency);
+    }
+
+    void bool_var_manager::decide(sat::literal lit, unsigned lvl, clause* lemma) {
+        LOG("Decide literal " << lit << " @ " << lvl);
+        assign(lit, lvl, nullptr, lemma);
+    }
+
+    void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
+        LOG("Eval literal " << lit << " @ " << lvl);
+        assign(lit, lvl, nullptr, nullptr);
+    }
+
+    void bool_var_manager::asserted(sat::literal lit, unsigned lvl, unsigned dep) {
+        LOG("Asserted " << lit << " @ " << lvl);
+        assign(lit, lvl, nullptr, nullptr, dep);
+    }
+
     void bool_var_manager::assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep) {
         SASSERT(!is_assigned(lit));
         m_value[lit.index()] = l_true;

src/math/polysat/boolean.h

@@ -32,6 +32,8 @@ namespace polysat {
         var_queue                   m_free_vars;  // free Boolean variables
         vector<ptr_vector<clause>>  m_watch;      // watch list for literals into clauses
 
+        void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep = null_dependency);
+
     public:
 
         bool_var_manager(): m_free_vars(m_activity) {}
@@ -56,9 +58,7 @@ namespace polysat {
         clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_reason[var]; }
 
         clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; }
-
-        
-
+       
         ptr_vector<clause>& watch(sat::literal lit) { return m_watch[lit.index()]; }
         unsigned_vector& activity() { return m_activity; }
         bool can_decide() const { return !m_free_vars.empty(); }
@@ -69,7 +69,10 @@ namespace polysat {
         void dec_activity(sat::literal lit) { m_activity[lit.var()] /= 2; }
 
         /// Set the given literal to true
-        void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep = null_dependency);
+        void propagate(sat::literal lit, unsigned lvl, clause& reason);
+        void decide(sat::literal lit, unsigned lvl, clause* lemma);
+        void eval(sat::literal lit, unsigned lvl);
+        void asserted(sat::literal lit, unsigned lvl, unsigned dep);
         void unassign(sat::literal lit);
 
         std::ostream& display(std::ostream& out) const;

src/math/polysat/conflict.cpp

@@ -161,7 +161,7 @@ namespace polysat {
         clause_ref lemma = c_lemma.build();
         cm().store(lemma.get(), s);
         if (s.m_bvars.value(c.blit()) == l_undef)
-            s.assign_bool(s.level(*lemma), c.blit(), lemma.get(), nullptr);
+            s.assign_propagate(c.blit(), *lemma);
     }
 
     void conflict::remove(signed_constraint c) {
@@ -178,6 +178,14 @@ namespace polysat {
         insert(c_new, c_new_premises);
     }
 
+
+    bool conflict::contains(signed_constraint c) {
+        if (c->has_bvar())
+            return m_literals.contains(c.blit().index());
+        else
+            return m_constraints.contains(c);
+    }
+
     void conflict::set_bailout() {
         SASSERT(!is_bailout());
         m_bailout = true;
@@ -237,11 +245,11 @@ namespace polysat {
         for (unsigned v : m_vars) {
             if (!is_pmarked(v))
                 continue;
-            auto diseq = ~s.eq(s.var(v), s.get_value(v));
-            cm().ensure_bvar(diseq.get());
-            if (diseq.bvalue(s) == l_undef) 
-                s.assign_bool(s.get_level(v), ~diseq.blit(), nullptr, nullptr);            
-            lemma.push(diseq);
+            auto eq = s.eq(s.var(v), s.get_value(v));
+            cm().ensure_bvar(eq.get());
+            if (eq.bvalue(s) == l_undef) 
+                s.assign_eval(s.get_level(v), eq.blit());            
+            lemma.push(~eq);
         }        
 
         return lemma;

src/math/polysat/conflict.h

@@ -93,6 +93,8 @@ namespace polysat {
 
         void keep(signed_constraint c);
 
+        bool contains(signed_constraint c);
+
         /** Perform boolean resolution with the clause upon variable 'var'.
          * Precondition: core/clause contain complementary 'var'-literals.
          */

src/math/polysat/constraint.cpp

@@ -104,7 +104,7 @@ namespace polysat {
         if (first) 
             s.set_conflict(cl);        
         else 
-            s.assign_bool(s.level(cl), cl[0], &cl, nullptr);
+            s.assign_propagate(cl[0], cl);
     }
 
     void constraint_manager::unwatch(clause& cl) {

src/math/polysat/saturation.cpp

@@ -70,11 +70,17 @@ namespace polysat {
         SASSERT(!crit1.is_currently_true(s));
 
         LOG("critical " << m_rule << " " << crit1);
-        LOG("consequent " << c << " value: " << c.bvalue(s));
+        LOG("consequent " << c << " value: " << c.bvalue(s) << " " << c.is_currently_false(s) << " " << core.contains(~c));
 
+
+        // ensure new core is a conflict
         if (!c.is_currently_false(s) && c.bvalue(s) != l_false)
             return false;
 
+        // avoid loops
+        if (core.contains(~c))
+            return false;
+
         core.reset();
         for (auto d : m_new_constraints)
             core.insert(d);
@@ -272,12 +278,12 @@ namespace polysat {
      *  [x] zx > yx  ==>  Ω*(x,y) \/ z > y
      *  [x] yx <= zx  ==>  Ω*(x,y) \/ y <= z \/ x = 0
      */
-    bool inf_saturate::try_ugt_x(pvar v, conflict& core, inequality const& c) {
+    bool inf_saturate::try_ugt_x(pvar v, conflict& core, inequality const& xy_l_xz) {
         set_rule("zx <= yx");
         pdd x = s.var(v);
         pdd y = x;
         pdd z = x;
-        if (!is_xY_l_xZ(v, c, y, z))
+        if (!is_xY_l_xZ(v, xy_l_xz, y, z))
             return false;
         if (!is_non_overflow(x, y))
             return false;
@@ -288,40 +294,37 @@ namespace polysat {
         if (!c.is_strict)
             m_new_constraints.push_back(~s.eq(x));
         push_omega(x, y);
-        return propagate(core, c, c, c.is_strict, y, z);
+        return propagate(core, xy_l_xz, xy_l_xz, xy_l_xz.is_strict, y, z);
     }
 
     /// [y] z' <= y /\ zx > yx  ==>  Ω*(x,y) \/ zx > z'x
     /// [y] z' <= y /\ yx <= zx  ==>  Ω*(x,y) \/ z'x <= zx
     bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& le_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) {
-        pdd const y = s.var(v);
-
         SASSERT(is_l_v(v, le_y));
         SASSERT(verify_Xy_l_XZ(v, yx_l_zx, x, z));
+        pdd const y = s.var(v);
         if (!is_non_overflow(x, y))
-            return false;
-          
+            return false;          
         pdd const& z_prime = le_y.lhs;
         m_new_constraints.reset();
         push_omega(x, y);
-        // z'x <= zx
         return propagate(core, le_y, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x);
     }
 
-    bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& c) {
-        set_rule("z' <= y & yx <= zx");
-        if (!is_l_v(v, c))
-            return false;
+    bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& yx_l_zx) {
+        set_rule("[y] z' <= y & yx <= zx");
         pdd x = s.var(v);
         pdd z = x;
+        if (!is_Xy_l_XZ(v, yx_l_zx, x, z))
+            return false;
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
             auto dd = s.lit2cnstr(si.lit());
             if (!dd->is_ule())
                 continue;
-            auto d = dd.as_inequality();
-            if (is_Xy_l_XZ(v, d, x, z) && try_ugt_y(v, core, c, d, x, z))
+            auto le_y = dd.as_inequality();
+            if (is_l_v(v, le_y) && try_ugt_y(v, core, le_y, yx_l_zx, x, z))
                 return true;
         }
         return false;
@@ -330,30 +333,26 @@ namespace polysat {
 
     /// [x]  y <= ax /\ x <= z  (non-overflow case)
     ///     ==>   Ω*(a, z)  \/  y <= az
-    bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c) {
-        set_rule("y <= ax & x <= z");
+    bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& y_l_ax) {
+        set_rule("[x] y <= ax & x <= z");
         pdd y = s.var(x);
         pdd a = y;
-        if (!is_Y_l_Ax(x, c, a, y))
+        if (!is_Y_l_Ax(x, y_l_ax, a, y))
             return false;
-
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
             auto dd = s.lit2cnstr(si.lit());
             if (!dd->is_ule())
                 continue;
-            if (dd.is_currently_true(s))
-                continue;
-            auto d = dd.as_inequality();
-            if (is_g_v(x, d) && try_y_l_ax_and_x_l_z(x, core, c, d, a, y))
+            auto x_l_z = dd.as_inequality();
+            if (is_g_v(x, x_l_z) && try_y_l_ax_and_x_l_z(x, core, y_l_ax, x_l_z, a, y))
                 return true;
         }
         return false;
     }
 
     bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& y_l_ax, inequality const& x_l_z,  pdd const& a, pdd const& y) {
-
         SASSERT(is_g_v(x, x_l_z));
         SASSERT(verify_Y_l_Ax(x, y_l_ax, a, y));
         pdd z = x_l_z.rhs;
@@ -361,28 +360,26 @@ namespace polysat {
             return false;
         m_new_constraints.reset();       
         push_omega(a, z);
-        return propagate(core, x_l_z, y_l_ax, x_l_z.is_strict || y_l_ax.is_strict, y, a * z);
+        return propagate(core, y_l_ax, x_l_z, x_l_z.is_strict || y_l_ax.is_strict, y, a * z);
     }
 
 
     /// [z] z <= y' /\ zx > yx  ==>  Ω*(x,y') \/ y'x > yx
     /// [z] z <= y' /\ yx <= zx  ==>  Ω*(x,y') \/ yx <= y'x
-    bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& c) {
-        set_rule("ugt_z");
-        if (!is_g_v(z, c))
-            return false;
+    bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& yx_l_zx) {
+        set_rule("[z] z <= y' /\ zx > yx");
         pdd y = s.var(z);
         pdd x = y;
+        if (!is_YX_l_zX(z, yx_l_zx, x, y))
+            return false;
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
             auto dd = s.lit2cnstr(si.lit());
             if (!dd->is_ule())
                 continue;
-            if (!dd.is_currently_false(s))
-                continue;
-            auto d = dd.as_inequality();
-            if (is_YX_l_zX(z, d, x, y) && try_ugt_z(z, core, c, d, x, y))
+            auto z_l_y = dd.as_inequality();
+            if (is_g_v(z, z_l_y) && try_ugt_z(z, core, z_l_y, yx_l_zx, x, y))
                 return true;
         }
         return false;
@@ -408,7 +405,7 @@ namespace polysat {
     //     ==> value(p) <= p => value(p) < q
 
     bool inf_saturate::try_tangent(pvar v, conflict& core, inequality const& c) {   
-        set_rule("tangent");
+        set_rule("[x] p(x) <= q(x) where value(p) > value(q)");
         if (c.is_strict)
             return false;
         if (!c.src->contains_var(v))

src/math/polysat/solver.cpp

@@ -126,7 +126,7 @@ namespace polysat {
             set_conflict(c /*, dep */);
             return;
         }
-        m_bvars.assign(lit, m_level, nullptr, nullptr, dep);
+        m_bvars.asserted(lit, m_level, dep);
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);
 
@@ -206,7 +206,7 @@ namespace polysat {
         if (m_bvars.is_false(cl[idx]))
             set_conflict(cl);
         else
-            assign_bool(level(cl), cl[idx], &cl, nullptr);
+            assign_propagate(cl[idx], cl);
         return false;
     }
 
@@ -539,7 +539,11 @@ namespace polysat {
                 break;
             case l_undef:
                 num_choices++;                
-                if (!lit2cnstr(lit).is_currently_false(*this)) 
+                if (lit2cnstr(lit).is_currently_false(*this)) {
+                    unsigned level = m_level; // TODO
+                    assign_eval(level, lit);
+                }
+                else
                     choice = lit;
                 break;
             }
@@ -558,9 +562,9 @@ namespace polysat {
         push_cjust(lemma.justified_var(), c);
 
         if (num_choices == 1)
-            assign_bool(level(lemma), choice, &lemma, nullptr);
+            assign_propagate(choice, lemma);
         else 
-            assign_bool(m_level, choice, nullptr, &lemma);
+            assign_decision(choice, &lemma);
     }
 
     /**
@@ -597,48 +601,31 @@ namespace polysat {
             return m_bvars.is_decision(item.lit().var());
     }
 
+    // Current situation: we have a decision for boolean literal L on top of the stack, and a conflict core.
+    //
+    // In a CDCL solver, this means ~L is in the lemma (actually, as the asserting literal). We drop the decision and replace it by the propagation (~L)^lemma.
+    //
+    // - we know L must be false
+    // - if L isn't in the core, we can still add it (weakening the lemma) to obtain "core => ~L"
+    // - then we can add the propagation (~L)^lemma and continue with the next guess
+
+    // Note that if we arrive at this point, the variables in L are "relevant" to the conflict (otherwise we would have skipped L).
+    // So the subsequent steps must have contained one of these:
+    // - propagation of some variable v from L (and maybe other constraints)
+    //      (v := val)^{L, ...}
+    //      this means L is in core, unless we core-reduced it away
+    // - propagation of L' from L
+    //      (L')^{L' \/ ¬L \/ ...}
+    //      again L is in core, unless we core-reduced it away
+
     void solver::revert_bool_decision(sat::literal lit) {
         sat::bool_var const var = lit.var();
         LOG_H3("Reverting boolean decision: " << lit << " " << m_conflict);
         SASSERT(m_bvars.is_decision(var));
 
-        // Current situation: we have a decision for boolean literal L on top of the stack, and a conflict core.
-        //
-        // In a CDCL solver, this means ~L is in the lemma (actually, as the asserting literal). We drop the decision and replace it by the propagation (~L)^lemma.
-        //
-        // - we know L must be false
-        // - if L isn't in the core, we can still add it (weakening the lemma) to obtain "core => ~L"
-        // - then we can add the propagation (~L)^lemma and continue with the next guess
-
-        // Note that if we arrive at this point, the variables in L are "relevant" to the conflict (otherwise we would have skipped L).
-        // So the subsequent steps must have contained one of these:
-        // - propagation of some variable v from L (and maybe other constraints)
-        //      (v := val)^{L, ...}
-        //      this means L is in core, unless we core-reduced it away
-        // - propagation of L' from L
-        //      (L')^{L' \/ ¬L \/ ...}
-        //      again L is in core, unless we core-reduced it away
-
-        clause_builder reason_builder = m_conflict.build_lemma();
-        
+        clause_builder reason_builder = m_conflict.build_lemma();        
 
         SASSERT(std::find(reason_builder.begin(), reason_builder.end(), ~lit));
-#if 0
-        if (!contains_lit) {
-            // At this point, we do not have ~lit in the reason.
-            // For now, we simply add it (thus weakening the reason)
-            //
-            // Alternative (to be considered later):
-            // - 'reason' itself (without ~L) would already be an explanation for ~L
-            // - however if it doesn't contain ~L, it breaks the boolean resolution invariant
-            // - would need to check what we can gain by relaxing that invariant
-            // - drawback: might have to bail out at boolean resolution
-            // Also: maybe we can skip ~L in some cases? but in that case it shouldn't be marked.
-            //
-            std::cout << "ADD extra " << ~lit << "\n";
-            reason_builder.push(~lit);
-        }
-#endif
         clause_ref reason = reason_builder.build();
 
         if (reason->empty()) {
@@ -666,7 +653,7 @@ namespace polysat {
         SASSERT(!can_propagate());
         SASSERT(!is_conflict());
         push_level();        
-        assign_bool(m_level, lit, nullptr, lemma);
+        assign_decision(lit, lemma);
     }
 
     unsigned solver::level(clause const& cl) {
@@ -679,15 +666,20 @@ namespace polysat {
         return lvl;
     }
 
-    /// Assign a boolean literal and put it on the search stack
-    void solver::assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma) {
-        SASSERT(!m_bvars.is_true(lit));
-        if (reason)
-            LOG("Propagate literal " << lit << " @ " << level << " by " << *reason);
-        else
-            LOG("Decide literal " << lit << " @ " << m_level);
-        
-        m_bvars.assign(lit, level, reason, lemma);
+    void solver::assign_propagate(sat::literal lit, clause& reason) {
+        m_bvars.propagate(lit, level(reason), reason);
+        m_trail.push_back(trail_instr_t::assign_bool_i);
+        m_search.push_boolean(lit);
+    }
+
+    void solver::assign_decision(sat::literal lit, clause* lemma) {
+        m_bvars.decide(lit, m_level, lemma);
+        m_trail.push_back(trail_instr_t::assign_bool_i);
+        m_search.push_boolean(lit);
+    }
+
+    void solver::assign_eval(unsigned level, sat::literal lit) {
+        m_bvars.eval(lit, level);
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);
     }

src/math/polysat/solver.h

@@ -145,7 +145,9 @@ namespace polysat {
         void push_level();
         void pop_levels(unsigned num_levels);
 
-        void assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma);
+        void assign_propagate(sat::literal lit, clause& reason);
+        void assign_decision(sat::literal lit, clause* lemma);
+        void assign_eval(unsigned level, sat::literal lit);
         void activate_constraint(signed_constraint c);
         void deactivate_constraint(signed_constraint c);
         void decide_bool(clause& lemma);