Merge remote-tracking branch 'origin/polysat' into polysat

src/math/polysat/boolean.cpp

@@ -85,8 +85,8 @@ namespace polysat {
 
     void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dependency dep) {
         LOG("Asserted " << lit << " @ " << lvl);
-        assign(kind_t::decision, lit, lvl, nullptr, dep);
-        SASSERT(is_decision(lit));
+        assign(dep == null_dependency ? kind_t::decision : kind_t::assumption, lit, lvl, nullptr, dep);
+        SASSERT(is_decision(lit) || is_assumption(lit));
     }
 
     void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep) {

src/math/polysat/boolean.h

@@ -24,6 +24,7 @@ namespace polysat {
             unassigned,
             bool_propagation,
             value_propagation,
+            assumption,
             decision,
         };
 
@@ -57,6 +58,8 @@ namespace polysat {
         bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; }
         bool is_decision(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::decision; }
         bool is_decision(sat::literal lit) const { return is_decision(lit.var()); }
+        bool is_assumption(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::assumption; }
+        bool is_assumption(sat::literal lit) const { return is_assumption(lit.var()); }
         bool is_bool_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::bool_propagation; }
         bool is_bool_propagation(sat::literal lit) const { return is_bool_propagation(lit.var()); }
         bool is_value_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::value_propagation; }

src/math/polysat/conflict.cpp

@@ -50,7 +50,8 @@ namespace polysat {
         if (!m_vars.empty())
             out << " vars";
         for (auto v : m_vars)
-            out << " v" << v;
+            if (is_pmarked(v))
+                out << " v" << v;
         return out;
     }
 
@@ -328,7 +329,14 @@ namespace polysat {
         auto const& j = s.m_justification[v];
 
         s.inc_activity(v); 
-        
+
+#if 0
+        if (j.is_decision() && m_vars.contains(v)) {
+            set_bailout();
+            return false;
+        }
+#endif
+   
         m_vars.remove(v);
 
         if (j.is_propagation()) {
@@ -343,32 +351,38 @@ namespace polysat {
             }        
         }
 
+        LOG("try-explain v" << v);
         if (try_explain(v))
             return true;
 
         // No value resolution method was successful => fall back to saturation and variable elimination
         while (s.inc()) {
+            LOG("try-eliminate v" << v);
             // TODO: as a last resort, substitute v by m_value[v]?
             if (try_eliminate(v))
                 return true;
             if (!try_saturate(v))
                 break;
         }
+        LOG("bailout v" << v);
         set_bailout();
         if (s.is_assigned(v) && j.is_decision())
             m_vars.insert(v);
         return false;
     }
 
-    bool conflict::try_eliminate(pvar v) {       
+    bool conflict::try_eliminate(pvar v) {    
+        LOG("try v" << v << " contains " << m_vars.contains(v));
+        if (m_vars.contains(v))
+            return false;
         bool has_v = false;
         for (auto c : *this)
-            has_v |= c->is_var_dependent() && c->contains_var(v);
+            has_v |= c->contains_var(v);
         if (!has_v)
             return true;
         for (auto* engine : ve_engines)
-            if (engine->perform(s, v, *this))
-                return true;
+            if (engine->perform(s, v, *this)) 
+                return true;            
         return false;
     }
 

src/math/polysat/solver.cpp

@@ -557,14 +557,14 @@ namespace polysat {
                 LOG("Literal " << lit << " is " << lit2cnstr(lit));
                 if (!m_conflict.is_bmarked(var))
                     continue;
-                if (m_bvars.level(var) <= base_level())  
-                    continue;
                 LOG("Conflict: " << m_conflict);
-                if (m_bvars.is_decision(var)) {
+                if (m_bvars.is_assumption(var))
+                    continue;
+                else if (m_bvars.is_decision(var)) {
                     revert_bool_decision(lit);
                     return;
                 }
-                if (m_bvars.is_bool_propagation(var))
+                else if (m_bvars.is_bool_propagation(var))
                     m_conflict.resolve(lit, *m_bvars.reason(lit));
                 else
                     m_conflict.resolve_with_assignment(lit, m_bvars.level(lit));
@@ -603,19 +603,6 @@ namespace polysat {
         }
         m_activity_inc >>= 14;
     }
-
-
-#if 0
-    /** Conflict resolution case where boolean literal 'lit' is on top of the stack 
-    *   NOTE: boolean resolution should work normally even in bailout mode.
-    */
-    void solver::resolve_bool(sat::literal lit) {       
-        SASSERT(m_bvars.is_bool_propagation(lit));
-        clause const& other = *m_bvars.reason(lit);
-        LOG_H3("resolve_bool: " << lit << " " << show_deref(&other));
-        m_conflict.resolve(lit, *other);        
-    }
-#endif
     
     void solver::report_unsat() {
         backjump(base_level());
@@ -785,7 +772,7 @@ namespace polysat {
     }
 
     unsigned solver::level(sat::literal lit0, clause const& cl) {
-        unsigned lvl = base_level();
+        unsigned lvl = 0;
         for (auto lit : cl) {
             if (lit == lit0)
                 continue;