reconnect saturation

src/math/polysat/conflict.cpp

@@ -69,14 +69,34 @@ namespace polysat {
         }
     };
 
+
+    class conflict_resolver {
+        inf_saturate m_saturate;
+
+    public:
+        conflict_resolver(solver& s)
+            : m_saturate(s)
+        {}
+
+        bool try_resolve_value(pvar v, conflict& core) {
+            if (m_saturate.perform(v, core))
+                return true;
+            return false;
+        }
+    };
+
+
     conflict::conflict(solver& s) : s(s) {
         // TODO: m_log_conflicts is always false even if "polysat.log_conflicts=true" is given on the command line
         if (true || s.get_config().m_log_conflicts)
             m_logger = alloc(file_inference_logger, s);
         else
             m_logger = alloc(dummy_inference_logger);
+        m_resolver = alloc(conflict_resolver, s);
     }
 
+    conflict::~conflict() {}
+
     inference_logger& conflict::logger() {
         return *m_logger;
     }
@@ -355,7 +375,8 @@ namespace polysat {
         }
         logger().log(inf_resolve_value(s, v));
 
-        // TODO: call conflict resolution plugins here; "return true" if successful
+        if (m_resolver->try_resolve_value(v, *this))
+            return true;
 
         // No conflict resolution plugin succeeded => give up and bail out
         set_bailout();

src/math/polysat/conflict.h

@@ -100,6 +100,7 @@ namespace polysat {
 
     class solver;
     class conflict_iterator;
+    class conflict_resolver;
 
     enum class conflict_kind_t {
         // standard conflict resolution
@@ -120,6 +121,7 @@ namespace polysat {
     class conflict {
         solver& s;
         scoped_ptr<inference_logger> m_logger;
+        scoped_ptr<conflict_resolver> m_resolver;
 
         // current conflict core consists of m_literals and m_vars
         indexed_uint_set m_literals;        // set of boolean literals in the conflict
@@ -139,6 +141,7 @@ namespace polysat {
 
     public:
         conflict(solver& s);
+        ~conflict();
 
         inference_logger& logger();
 

src/math/polysat/saturation.cpp

@@ -1,4 +1,3 @@
-#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -103,8 +102,9 @@ namespace polysat {
             core.insert(d);
         if (c.bvalue(s) != l_false)  // conflict is due to the evaluation of c, so it depends on the variable values
             core.insert_vars(c);
-        core.insert(~c);       
-        core.log_inference(inf_name);
+        core.insert(~c);
+        core.set_backjump();
+        core.logger().log(inf_name);
         LOG("Core " << core);
         return true;        
     }
@@ -487,4 +487,3 @@ namespace polysat {
     }
 
 }
-#endif

src/math/polysat/saturation.h

@@ -1,4 +1,3 @@
-#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -18,7 +17,6 @@ Author:
 namespace polysat {
 
     class solver;
-    class constraint_manager;
 
     class inference_engine {
         friend class conflict;
@@ -111,4 +109,3 @@ namespace polysat {
      */
 
 }
-#endif

src/math/polysat/solver.cpp

@@ -681,12 +681,12 @@ namespace polysat {
         SASSERT(lemma);
         LOG("Lemma: " << *lemma);
         for (sat::literal lit : *lemma) {
-            LOG("   Literal " << lit << " is: " << lit_pp(*this, lit));
+            LOG("   " << lit_pp(*this, lit));
             SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this));
         }
 
         // find second-highest level of the literals in the lemma
-        unsigned max_level = 0;  // could be simplified if we're sure that always max_level == m_level
+        unsigned max_level = 0;
         unsigned jump_level = 0;
         for (auto lit : *lemma) {
             if (!m_bvars.is_assigned(lit))
@@ -699,7 +699,6 @@ namespace polysat {
                 jump_level = lit_level;
             }
         }
-        SASSERT(max_level == m_level);  // not required; see comment on max_level
 
         jump_level = std::max(jump_level, base_level());