local updates

Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>

src/sat/sat_config.cpp

@@ -72,6 +72,7 @@ namespace sat {
         m_restart_initial = p.restart_initial();
         m_restart_factor  = p.restart_factor();
         m_restart_max     = p.restart_max();
+        m_inprocess_max   = p.inprocess_max();
 
         m_random_freq     = p.random_freq();
         m_random_seed     = p.random_seed();
@@ -183,6 +184,7 @@ namespace sat {
             throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
         }
         m_dimacs_display  = p.dimacs_display();
+        m_dimacs_inprocess_display  = p.dimacs_inprocess_display();
     }
 
     void config::collect_param_descrs(param_descrs & r) {

src/sat/sat_config.h

@@ -73,6 +73,7 @@ namespace sat {
         unsigned           m_restart_initial;
         double             m_restart_factor; // for geometric case
         unsigned           m_restart_max;
+        unsigned           m_inprocess_max;
         double             m_random_freq;
         unsigned           m_random_seed;
         unsigned           m_burst_search;
@@ -106,6 +107,7 @@ namespace sat {
         bool               m_drat_check;
 
         bool               m_dimacs_display;
+        bool               m_dimacs_inprocess_display;
 
         symbol             m_always_true;
         symbol             m_always_false;

src/sat/sat_params.pyg

@@ -9,6 +9,7 @@ def_module_params('sat',
                           ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
                           ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
+                          ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'),
                           ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
                           ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'),
                           ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
@@ -40,5 +41,6 @@ def_module_params('sat',
                           ('lookahead_search', BOOL, False, 'use lookahead solver'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
                           ('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, hs (Heule Schur), heuleu (Heule Unit), or unit'),
-                          ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving')))
+                          ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'),
+                          ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))
 

src/sat/sat_simplifier.cpp

@@ -73,7 +73,7 @@ namespace sat {
     inline bool simplifier::is_external(bool_var v) const { 
         return 
             s.is_assumption(v) ||
-            (s.is_external(v) && 
+            (s.is_external(v) && s.m_ext &&
              (!m_ext_use_list.get(literal(v, false)).empty() ||
               !m_ext_use_list.get(literal(v, true)).empty()));
     }

src/sat/sat_solver.cpp

@@ -62,6 +62,7 @@ namespace sat {
         m_conflicts_since_init    = 0;
         m_next_simplify           = 0;
         m_num_checkpoints         = 0;
+        m_simplifications         = 0;
     }
 
     solver::~solver() {
@@ -797,7 +798,6 @@ namespace sat {
                     keep = m_ext->propagate(l, it->get_ext_constraint_idx());
                     if (m_inconsistent) {
                         if (!keep) {
-                            std::cout << "CONFLICT - but throw away current watch literal\n";
                             ++it;
                         }
                         CONFLICT_CLEANUP();
@@ -925,6 +925,17 @@ namespace sat {
                     IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);
                     return l_undef;
                 }
+                if (m_config.m_inprocess_max <= m_simplifications) {
+                    m_reason_unknown = "sat.max.inprocess";
+                    IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-inprocess\")\n";);
+                    if (m_config.m_dimacs_inprocess_display) {
+                        display_dimacs(std::cout);
+                        for (unsigned i = 0; i < num_lits; ++lits) {
+                            std::cout << dimacs_lit(lits[i]) << " 0\n";
+                        }
+                    }
+                    return l_undef;
+                }
 
             }
         }
@@ -1411,7 +1422,8 @@ namespace sat {
         if (m_conflicts_since_init < m_next_simplify) {
             return;
         }
-        IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";);
+        m_simplifications++;
+        IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";);
 
         TRACE("sat", tout << "simplify\n";);
 
@@ -1424,11 +1436,11 @@ namespace sat {
 
         m_scc();
         CASSERT("sat_simplify_bug", check_invariant());
-
+        
         m_simplifier(false);
         CASSERT("sat_simplify_bug", check_invariant());
         CASSERT("sat_missed_prop", check_missed_propagation());
-
+        
         if (!m_learned.empty()) {
             m_simplifier(true);
             CASSERT("sat_missed_prop", check_missed_propagation());

src/sat/sat_solver.h

@@ -367,6 +367,7 @@ namespace sat {
         unsigned m_conflicts_since_init;
         unsigned m_restarts;
         unsigned m_conflicts_since_restart;
+        unsigned m_simplifications;
         unsigned m_restart_threshold;
         unsigned m_luby_idx;
         unsigned m_conflicts_since_gc;