introduce user-push/pop

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

src/math/polysat/polysat.cpp

@@ -63,7 +63,7 @@ namespace polysat {
     lbool solver::check_sat() { 
         while (true) {
             if (is_conflict() && m_level == 0) return l_false;
-            else if (is_conflict()) resolve_conflict_core();
+            else if (is_conflict()) resolve_conflict();
             else if (can_propagate()) propagate();
             else if (!can_decide()) return l_true;
             else decide();
@@ -348,7 +348,7 @@ namespace polysat {
      * 6. Otherwise, add accumulated constraints to explanation for the next viable solution, prune
      *    viable solutions by excluding the previous guess.
      */
-    unsigned solver::resolve_conflict() {
+    void solver::resolve_conflict() {
         SASSERT(m_conflict);
         constraint& c = *m_conflict;
         m_conflict = nullptr;
@@ -368,12 +368,15 @@ namespace polysat {
                 continue;
             pdd r = resolve(v, p);
             pdd rval = r.subst_val(sub);
-            if (!rval.is_non_zero())
+            if (!rval.is_non_zero()) {
-                goto backtrack;
+                backtrack();
+                return;
+            }
             if (r.is_val()) {
-                SASSERT(!r.is_zero());
                 // TBD: UNSAT, set conflict
-                return i;
+                SASSERT(!r.is_zero());
+                // learn_lemma(r, deps);
+                return;
             }
             justification& j = m_justification[v];
             if (j.is_decision()) {
@@ -381,30 +384,43 @@ namespace polysat {
                 // propagate if new value is given uniquely
                 // set conflict if viable set is empty
                 // adding r and reverting last decision.
-                break;                
+                // m_search.size() - i;
+                return;
             }
             SASSERT(j.is_propagation());
+            reset_marks();
             for (auto w : r.free_vars())
                 set_mark(w);
             p = r;
         }
         UNREACHABLE();
+    }
 
-    backtrack:
+    void solver::backtrack() {
+        unsigned i = m_search.size();
         do {
-            v = m_search[i];
+            auto v = m_search[i];
             justification& j = m_justification[v];
             if (j.is_decision()) {
                 // TBD: flip last decision.
+                // subtract value from viable
+                // m_viable[v] -= m_value[v];
+                if (m_viable[v].is_false()) 
+                    continue;
+                // 
+                // pop levels to i
+                // choose a new value for v as a decision.
+                // 
             }
         }
         while (i-- > 0);
 
-        return 0;
+        // unsat
+        // r = 1;        
+        // learn_and_backjump(r, m_search.size());        
     }
 
-    void solver::resolve_conflict_core() {
+    void solver::learn_and_backjump(pdd const& lemma, unsigned new_level) {
-        unsigned new_level = resolve_conflict();
         unsigned num_levels = m_level - new_level;
         SASSERT(num_levels > 0);
         pop_levels(num_levels);
@@ -413,6 +429,7 @@ namespace polysat {
     }
 
 
+    
     /**
      * resolve polynomials associated with unit propagating on v
      * producing polynomial that isolates v to lowest degree
@@ -431,6 +448,10 @@ namespace polysat {
     
     /**
      * Return residue of superposing p and q with respect to v.
+     * 
+     * TBD: should also collect dependencies (deps)
+     * and maximal level of constraints so learned lemma
+     * is given the appropriate level.
      */
     pdd solver::resolve(unsigned v, pdd const& p) {
         auto degree = p.degree(v);
@@ -457,16 +478,18 @@ namespace polysat {
         m_marks.fill(0);        
     }
 
-    bool solver::can_learn() {
+    void solver::push() {
-        return false;
+        push_level();
+        m_scopes.push_back(m_level);
     }
 
-    void solver::learn(constraint& c, unsigned_vector& deps) {
+    void solver::pop(unsigned num_scopes) {
-
+        unsigned base_level = m_scopes[m_scopes.size() - num_scopes];
+        pop_levels(m_level - base_level - 1);
     }
 
-    void solver::learn(vector<constraint>& cs, unsigned_vector& deps) {
+    bool solver::at_base_level() const {
-
+        return m_level == 0 || (!m_scopes.empty() && m_level == m_scopes.back());
     }
         
     std::ostream& solver::display(std::ostream& out) const {

src/math/polysat/polysat.h

@@ -120,6 +120,8 @@ namespace polysat {
         unsigned                 m_qhead { 0 };
         unsigned                 m_level { 0 };
 
+        unsigned_vector          m_scopes;   // user-scopes. External clients can push/pop scope
+
 
         // conflict state
         constraint* m_conflict { nullptr };
@@ -169,7 +171,16 @@ namespace polysat {
         pdd isolate(unsigned v);
         pdd resolve(unsigned v, pdd const& p);
         void decide();
-        void resolve_conflict_core();            
+
+        bool is_conflict() const { return nullptr != m_conflict; }
+        bool at_base_level() const;
+
+        void resolve_conflict();            
+        void backtrack();
+        void learn_and_backjump(pdd const& lemma, unsigned new_level);
+
+        bool can_decide() const { return !m_free_vars.empty(); }
+        void decide(rational & val, unsigned& var);
 
 
         bool invariant();
@@ -223,19 +234,8 @@ namespace polysat {
         bool can_propagate();
         void propagate();
 
-        bool can_decide() const { return !m_free_vars.empty(); }
+        void push();
-        void decide(rational & val, unsigned& var);
+        void pop(unsigned num_scopes);
-
-        bool is_conflict() const { return nullptr != m_conflict; }
-        /**
-         * Return number of scopes to backtrack and core in the shape of dependencies
-         * TBD: External vs. internal mode may need different signatures.
-         */
-        unsigned resolve_conflict();            
-        
-        bool can_learn();
-        void learn(constraint& c, unsigned_vector& deps); 
-        void learn(vector<constraint>& cs, unsigned_vector& deps); 
        
         std::ostream& display(std::ostream& out) const;