na

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

src/math/polysat/polysat.cpp

@@ -81,8 +81,9 @@ namespace polysat {
     };
 
     
-    solver::solver(trail_stack& s): 
+    solver::solver(trail_stack& s, reslimit& lim): 
         m_trail(s),
+        m_lim(lim),
         m_bdd(1000),
         m_dep_manager(m_value_manager, m_alloc),
         m_conflict_dep(nullptr, m_dep_manager),
@@ -92,7 +93,7 @@ namespace polysat {
     solver::~solver() {}
     
     lbool solver::check_sat() { 
-        while (true) {
+        while (m_lim.inc()) {
             if (is_conflict() && at_base_level()) return l_false;
             else if (is_conflict()) resolve_conflict();
             else if (can_propagate()) propagate();
@@ -167,13 +168,19 @@ namespace polysat {
 
     void solver::assign(unsigned var, unsigned index, bool value, unsigned dep) {
         m_viable[var] &= value ? m_bdd.mk_var(index) : m_bdd.mk_nvar(index);
-        m_trail.push(vector_value_trail<p_dependency*, false>(m_vdeps, var));
+        add_viable_dep(var, mk_dep(dep));
-        m_vdeps[var] = m_dep_manager.mk_join(m_vdeps[var], m_dep_manager.mk_leaf(dep));
         if (m_viable[var].is_false()) {
             // TBD: set conflict
         }
     }
 
+    void solver::add_viable_dep(unsigned var, p_dependency* dep) {
+        if (!dep)
+            return;
+        m_trail.push(vector_value_trail<p_dependency*, false>(m_vdeps, var));
+        m_vdeps[var] = m_dep_manager.mk_join(m_vdeps[var], dep);
+    }
+
     bool solver::can_propagate() {
         return m_qhead < m_search.size() && !is_conflict();
     }
@@ -280,9 +287,11 @@ namespace polysat {
 
     void solver::push_level() {
         ++m_level;
+        m_trail.push_scope();
     }
 
     void solver::pop_levels(unsigned num_levels) {
+        m_trail.pop_scope(num_levels);        
         m_level -= num_levels;
         pop_constraints(m_constraints);
         pop_constraints(m_redundant);
@@ -304,12 +313,16 @@ namespace polysat {
     void solver::pop_assignment() {
         while (!m_search.empty() && m_justification[m_search.back()].level() > m_level) {
             auto v = m_search.back();
+            undo_var(m_search.back());
+            m_search.pop_back();
+        }
+    }
+    
+    void solver::undo_var(unsigned v) {
         m_justification[v] = justification::unassigned();
         m_free_vars.unassign_var_eh(v);
         m_cjust[v].reset();
         m_viable[v] = m_bdd.mk_true();
-            m_search.pop_back();
-        }
     }
 
     void solver::add_watch(constraint& c) {
@@ -343,20 +356,21 @@ namespace polysat {
     }
 
     void solver::decide() {
-        m_trail.push_scope();
         rational val;
-        unsigned var;
-        decide(val, var);
-    }
-
-    void solver::decide(rational & val, unsigned& var) {
         SASSERT(can_decide());
+        unsigned var = m_free_vars.next_var();
+        switch (find_viable(var, val)) {
+        case l_false:
+            set_conflict(m_cjust[var]);
+            break;
+        case l_true:
+            assign_core(var, val, justification::propagation(m_level));
+            break;
+        case l_undef:
             push_level();
-        var = m_free_vars.next_var();
-        auto viable = m_viable[var];
-        SASSERT(!viable.is_false());
-        // TBD, choose some value from viable and construct val.
             assign_core(var, val, justification::decision(m_level));
+            break;
+        }
     }
 
     void solver::assign_core(unsigned var, rational const& val, justification const& j) {
@@ -368,7 +382,7 @@ namespace polysat {
         
     /**
      * Conflict resolution.
-     * - m_conflict is a constraint infeasible in the current assignment.
+     * - m_conflict are constraints that are infeasible in the current assignment.
      * 1. walk m_search from top down until last variable in m_conflict.
      * 2. resolve constraints in m_cjust to isolate lowest degree polynomials
      *    using variable.
@@ -385,23 +399,7 @@ namespace polysat {
      * 
      */
     void solver::resolve_conflict() {
-        SASSERT(!m_conflict.empty());
+        vector<pdd> ps = init_conflict();
-        reset_marks();
-        m_conflict_level = 0;
-        m_conflict_dep = nullptr;
-        pdd p = m_conflict[0]->p();
-        for (constraint* c : m_conflict) {
-            for (auto v : c->vars())
-                set_mark(v);
-            pdd p = c->p();
-            m_conflict_level = std::max(m_conflict_level, c->level());        
-            m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep, c->dep());
-        }
-        // TBD: deal with case of multiple constaints
-        // to obtain single p or delay extracting p until resolution.
-        // 
-        m_conflict.reset();
-        unsigned new_lemma_level = 0;
         unsigned v = UINT_MAX;
         unsigned i = m_search.size();
         vector<std::pair<unsigned, rational>> sub;
@@ -418,11 +416,12 @@ namespace polysat {
                 return;
             }
             if (j.is_decision()) {
-                learn_lemma(v, p);
+                if (ps.size() == 1)
+                    learn_lemma(v, ps[0]);
                 revert_decision(i);
                 return;
             }
-            pdd r = resolve(v, p, new_lemma_level);
+            pdd r = resolve(v, ps);
             pdd rval = r.subst_val(sub);
             if (r.is_val() && rval.is_non_zero()) {
                 report_unsat();
@@ -436,12 +435,29 @@ namespace polysat {
             reset_marks();
             for (auto w : r.free_vars())
                 set_mark(w);
-            p = r;
+            ps.shrink(1);
-            m_conflict_level = new_lemma_level;
+            ps[0] = r;
         }
         report_unsat();
     }
 
+    vector<pdd> solver::init_conflict() {
+        SASSERT(!m_conflict.empty());
+        vector<pdd> ps;
+        reset_marks();
+        m_conflict_level = 0;
+        m_conflict_dep = nullptr;
+        for (auto* c : m_conflict) {
+            for (auto v : c->vars())
+                set_mark(v);
+            ps.push_back(c->p());
+            m_conflict_level = std::max(m_conflict_level, c->level());        
+            m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep, c->dep());
+        }
+        m_conflict.reset();
+        return ps;
+    }
+
     /**
      * TBD: m_conflict_dep is a justification that m_value[v] is not viable.
      * it is currently not yet being accounted for.
@@ -498,14 +514,20 @@ namespace polysat {
     void solver::revert_decision(unsigned i) {
         auto v = m_search[i];
         SASSERT(m_justification[v].is_decision());
-        add_non_viable(v, m_value[v]);
 
-        // TBD how much to backjump to be clarified
-        // everything before v is reverted, but not assignment
-        // to v. This is different from propositional CDCL
-        // where decision on v is also reverted.
         unsigned new_level = m_justification[v].level();
-        backjump(new_level);
+        if (new_level < m_level)
+            backjump(new_level + 1);        
+        while (m_search.back() != v) {
+            undo_var(m_search.back());
+            m_search.pop_back();
+        }
+        SASSERT(!m_search.empty());
+        SASSERT(m_search.back() == v);
+        m_search.pop_back();
+        add_non_viable(v, m_value[v]);
+        add_viable_dep(v, m_conflict_dep);
+        m_qhead = m_search.size();
         rational value;
         m_conflict_dep = nullptr;
         switch (find_viable(v, value)) {
@@ -523,10 +545,8 @@ namespace polysat {
     
     void solver::backjump(unsigned new_level) {
         unsigned num_levels = m_level - new_level;
-        if (num_levels > 0) {
+        if (num_levels > 0) 
             pop_levels(num_levels);        
-            m_trail.pop_scope(num_levels);        
-        }
     }
     
     /**
@@ -534,12 +554,9 @@ namespace polysat {
      * producing polynomial that isolates v to lowest degree
      * and lowest power of 2.     
      */
-    pdd solver::isolate(unsigned v) {
+    pdd solver::isolate(unsigned v, vector<pdd> const& ps) {
-        if (m_cjust[v].empty()) 
+        pdd p = ps[0];
-            return sz2pdd(m_size[v]).zero();
+        for (unsigned i = ps.size(); i-- > 1; ) {
-        auto const& cs = m_cjust[v];
-        pdd p = cs[0]->p();
-        for (unsigned i = cs.size(); i-- > 1; ) {
             // TBD reduce with respect to v
         }
         return p;
@@ -548,18 +565,17 @@ namespace polysat {
     /**
      * Return residue of superposing p and q with respect to v.
      */
-    pdd solver::resolve(unsigned v, pdd const& p, unsigned& resolve_level) {
+    pdd solver::resolve(unsigned v, vector<pdd> const& ps) {
-        resolve_level = 0;
-        auto degree = p.degree(v);
         auto const& cs = m_cjust[v];
-        pdd r = p;
+        pdd r = isolate(v, ps);
+        auto degree = r.degree(v);
         while (degree > 0) {
             for (auto * c : cs) {
                 if (degree >= c->p().degree(v)) {
                     // TODO binary resolve, update r using result
                     // add parity condition to presere falsification
                     degree = r.degree(v);
-                    resolve_level = std::max(resolve_level, c->level());
+                    m_conflict_level = std::max(m_conflict_level, c->level());
                     m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep.get(), c->dep());
                 }
             }
@@ -591,11 +607,11 @@ namespace polysat {
 
     void solver::push() {
         push_level();
-        m_scopes.push_back(m_level);
+        m_base_levels.push_back(m_level);
     }
 
     void solver::pop(unsigned num_scopes) {
-        unsigned base_level = m_scopes[m_scopes.size() - num_scopes];
+        unsigned base_level = m_base_levels[m_base_levels.size() - num_scopes];
         pop_levels(m_level - base_level - 1);
     }
 
@@ -604,7 +620,7 @@ namespace polysat {
     }
     
     unsigned solver::base_level() const {
-        return m_scopes.empty() ? 0 : m_scopes.back();
+        return m_base_levels.empty() ? 0 : m_base_levels.back();
     }
         
     std::ostream& solver::display(std::ostream& out) const {

src/math/polysat/polysat.h

@@ -19,6 +19,7 @@ Author:
 #include "util/dependency.h"
 #include "util/trail.h"
 #include "util/lbool.h"
+#include "util/rlimit.h"
 #include "util/scoped_ptr_vector.h"
 #include "util/var_queue.h"
 #include "math/dd/dd_pdd.h"
@@ -114,6 +115,7 @@ namespace polysat {
         typedef ptr_vector<constraint> constraints;
 
         trail_stack&             m_trail;
+        reslimit&                m_lim;
         scoped_ptr_vector<dd::pdd_manager> m_pdd;
         dd::bdd_manager          m_bdd;
         dep_value_manager        m_value_manager;
@@ -142,7 +144,7 @@ namespace polysat {
         unsigned                 m_qhead { 0 };
         unsigned                 m_level { 0 };
 
-        unsigned_vector          m_scopes;   // user-scopes. External clients can push/pop scope. 
+        unsigned_vector          m_base_levels;  // External clients can push/pop scope. 
 
 
         // conflict state
@@ -159,6 +161,11 @@ namespace polysat {
          */
         void add_non_viable(unsigned var, rational const& val);
 
+        /**
+         * Add dependency for variable viable range.
+         */
+        void add_viable_dep(unsigned var, p_dependency* dep);
+
         
         /**
          * Find a next viable value for varible.
@@ -206,8 +213,10 @@ namespace polysat {
 
         unsigned                 m_conflict_level { 0 };
 
-        pdd isolate(unsigned v);
+        pdd isolate(unsigned v, vector<pdd> const& ps);
-        pdd resolve(unsigned v, pdd const& p, unsigned& resolve_level);
+        pdd resolve(unsigned v, vector<pdd> const& ps);
+
+        bool can_decide() const { return !m_free_vars.empty(); }
         void decide();
 
         p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dep_manager.mk_leaf(dep); }
@@ -216,16 +225,16 @@ namespace polysat {
         bool at_base_level() const;
         unsigned base_level() const;
 
+        vector<pdd>  init_conflict();
         void resolve_conflict();            
         void backtrack(unsigned i);
         void report_unsat();
         void revert_decision(unsigned i);
         void learn_lemma(unsigned v, pdd const& p);
         void backjump(unsigned new_level);
+        void undo_var(unsigned v);
         void add_lemma(constraint* c);
 
-        bool can_decide() const { return !m_free_vars.empty(); }
-        void decide(rational & val, unsigned& var);
 
 
         bool invariant();
@@ -238,7 +247,7 @@ namespace polysat {
          * every update to the solver is going to be retractable
          * by pushing an undo action on the trail stack.
          */
-        solver(trail_stack& s);
+        solver(trail_stack& s, reslimit& lim);
 
         ~solver();
 

src/test/polysat.cpp

@@ -5,14 +5,21 @@ namespace polysat {
     // test resolve, factoring routines
     // auxiliary 
 
+    struct solver_scope {
+        reslimit lim;
+        trail_stack stack;        
+    };
+
+    struct scoped_solver : public solver_scope, public solver {
+        scoped_solver(): solver(stack, lim) {}
+    };
     
     /**
      * This one is unsat because a*a*(a*a - 1)
      * is 0 for all values of a.
      */
     static void test_eq1() {
-        trail_stack stack;
+        scoped_solver s;
-        solver s(stack);
         auto a = s.var(s.add_var(2));
         auto p = a*a*(a*a - 1) + 1;
         s.add_eq(p);
@@ -23,8 +30,7 @@ namespace polysat {
      * has solution a = 3
      */
     static void test_eq2() {
-        trail_stack stack;
+        scoped_solver s;
-        solver s(stack);
         auto a = s.var(s.add_var(2));
         auto p = a*(a-1) + 2;
         s.add_eq(p);
@@ -38,8 +44,7 @@ namespace polysat {
      * v*q > u
      */
     static void test_ineq1() {
-        trail_stack stack;
+        scoped_solver s;
-        solver s(stack);
         auto u = s.var(s.add_var(5));
         auto v = s.var(s.add_var(5));
         auto q = s.var(s.add_var(5));
@@ -57,8 +62,7 @@ namespace polysat {
      * n > r2 > 0
      */
     static void test_ineq2() {
-        trail_stack stack;
+        scoped_solver s;
-        solver s(stack);
         auto n = s.var(s.add_var(5));
         auto q1 = s.var(s.add_var(5));
         auto a = s.var(s.add_var(5));