split out restart

src/math/polysat/CMakeLists.txt

@@ -11,6 +11,7 @@ z3_add_component(polysat
     linear_solver.cpp
     log.cpp
     mul_ovfl_constraint.cpp
+    restart.cpp
     saturation.cpp
     search_state.cpp
     simplify.cpp

src/math/polysat/restart.cpp

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Restart
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-12
+
+  
+--*/
+#include "math/polysat/solver.h"
+#include "math/polysat/restart.h"
+#include "util/luby.h"
+
+namespace polysat {
+
+    restart::restart(solver& s):
+        s(s)
+    {}
+
+    /*
+    * Basic restart functionality.
+    * restarts make more sense when the order of variable 
+    * assignments and the values assigned to variables can be diversified.
+    */
+    bool restart::should_apply() const {
+        if (s.m_stats.m_num_conflicts - m_conflicts_at_restart < m_restart_threshold)
+            return false;
+        if (s.base_level() + 2 > s.m_level)
+            return false;
+        return true;        
+    }
+
+    void restart::operator()() {
+        ++s.m_stats.m_num_restarts;
+        s.pop_levels(s.m_level - s.base_level());
+        m_conflicts_at_restart = s.m_stats.m_num_conflicts;
+        m_restart_threshold = m_restart_init * get_luby(++m_luby_idx);
+    }
+
+}

src/math/polysat/restart.h

@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Restart
+
+Author:
+
+    Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-12
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+
+namespace polysat {
+
+    class solver;
+
+    class restart {
+        solver& s;
+        unsigned m_conflicts_at_restart = 0;
+        unsigned m_restart_threshold = 100;
+        unsigned m_restart_init = 100;
+        unsigned m_luby_idx = 0;
+
+    public:
+        restart(solver& s);
+
+        bool should_apply() const;
+
+        void operator()();
+    };
+
+}

src/math/polysat/simplify.cpp

@@ -35,7 +35,6 @@ This is a place holder for simplification.
 
   
 --*/
-#pragma once
 #include "math/polysat/solver.h"
 #include "math/polysat/simplify.h"
 

src/math/polysat/solver.cpp

@@ -20,7 +20,6 @@ Author:
 #include "math/polysat/explain.h"
 #include "math/polysat/log.h"
 #include "math/polysat/variable_elimination.h"
-#include "util/luby.h"
 
 // For development; to be removed once the linear solver works well enough
 #define ENABLE_LINEAR_SOLVER 0
@@ -35,6 +34,7 @@ namespace polysat {
         m_linear_solver(*this),
         m_conflict(*this),
         m_simplify(*this),
+        m_restart(*this),
         m_forbidden_intervals(*this),
         m_bvars(),
         m_free_pvars(m_activity),
@@ -75,7 +75,7 @@ namespace polysat {
             else if (!can_decide()) { LOG_H2("SAT"); SASSERT(verify_sat()); return l_true; }
             else if (m_constraints.should_gc()) m_constraints.gc(*this);
             else if (m_simplify.should_apply()) m_simplify();
-            else if (should_restart()) restart();
+            else if (m_restart.should_apply()) m_restart();
             else decide();
         }
         LOG_H2("UNDEF (resource limit)");
@@ -252,25 +252,7 @@ namespace polysat {
 #endif
     }
 
-    /*
-    * Basic restart functionality.
-    * restarts make more sense when the order of variable 
-    * assignments and the values assigned to variables can be diversified.
-    */
-    bool solver::should_restart() {
-        if (m_stats.m_num_conflicts - m_conflicts_at_restart < m_restart_threshold)
-            return false;
-        if (base_level() + 2 > m_level)
-            return false;
-        return true;        
-    }
 
-    void solver::restart() {
-        ++m_stats.m_num_restarts;
-        pop_levels(m_level - base_level());
-        m_conflicts_at_restart = m_stats.m_num_conflicts;
-        m_restart_threshold = m_restart_init * get_luby(++m_luby_idx);
-    }
 
     void solver::pop_levels(unsigned num_levels) {
         if (num_levels == 0)

src/math/polysat/solver.h

@@ -25,6 +25,7 @@ Author:
 #include "math/polysat/constraint.h"
 #include "math/polysat/clause_builder.h"
 #include "math/polysat/simplify.h"
+#include "math/polysat/restart.h"
 #include "math/polysat/explain.h"
 #include "math/polysat/ule_constraint.h"
 #include "math/polysat/justification.h"
@@ -61,6 +62,7 @@ namespace polysat {
         friend class conflict;
         friend class conflict_explainer;
         friend class simplify;
+        friend class restart;
         friend class explainer;
         friend class inference_engine;
         friend class forbidden_intervals;
@@ -82,6 +84,7 @@ namespace polysat {
         linear_solver            m_linear_solver;
         conflict                 m_conflict; 
         simplify                 m_simplify;
+        restart                  m_restart;
         forbidden_intervals      m_forbidden_intervals;
         bool_var_manager         m_bvars;       // Map boolean variables to constraints
         var_queue                m_free_pvars;  // free poly vars
@@ -204,12 +207,6 @@ namespace polysat {
         void backjump(unsigned new_level);
         void add_lemma(clause& lemma);
 
-        unsigned m_conflicts_at_restart = 0;
-        unsigned m_restart_threshold = 100;
-        unsigned m_restart_init = 100;
-        unsigned m_luby_idx = 0;
-        bool should_restart();
-        void restart();
 
         signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
         static void insert_constraint(signed_constraints& cs, signed_constraint c);