update core generation to be partial, update maxres to use current model too

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

src/opt/inc_sat_solver.cpp

@@ -367,8 +367,12 @@ private:
 
     void extract_model() {
         TRACE("sat", tout << "retrieve model\n";);
-        model_ref md = alloc(model, m);
         sat::model const & ll_m = m_solver.get_model();
+        if (ll_m.empty()) {
+            m_model = 0;
+            return;
+        }
+        model_ref md = alloc(model, m);
         atom2bool_var::iterator it  = m_map.begin();
         atom2bool_var::iterator end = m_map.end();
         for (; it != end; ++it) {

src/opt/maxres.cpp

@@ -156,7 +156,7 @@ public:
     lbool mus_solver() {
         init();
         init_local();
-        while (true) {
+        while (m_lower < m_upper) {
             TRACE("opt", 
                   display_vec(tout, m_asms.size(), m_asms.c_ptr());
                   s().display(tout);
@@ -167,6 +167,7 @@ public:
             if (m_cancel) {
                 return l_undef;
             }
+            model_ref mdl;
             switch (is_sat) {
             case l_true: 
                 found_optimum();
@@ -174,6 +175,7 @@ public:
             case l_false:
                 is_sat = process_unsat();
                 if (is_sat != l_true) return is_sat;
+                get_mus_model(mdl);
                 break;
             case l_undef:
                 return l_undef;
@@ -359,14 +361,16 @@ public:
             // likewise, if the cores are too big, don't block the cores.
             //
 
-            process_unsat(cores);
 
             exprs cs;
             get_current_correction_set(cs);
             unsigned max_core = max_core_size(cores);
-            if (cs.size() <= std::max(max_core, m_max_correction_set_size)) {
+            if (!cs.empty() && cs.size() < max_core) {
                 process_sat(cs);                        
             }
+            else {
+                process_unsat(cores);                
+            }
         }
         
         m_lower = m_upper;
@@ -465,6 +469,7 @@ public:
                 cs.push_back(m_asms[i].get());
             }
         }
+        IF_VERBOSE(2, verbose_stream() << "(opt.maxres correction set size: " << cs.size() << ")\n";);
         TRACE("opt", display_vec(tout << "new correction set: ", cs.size(), cs.c_ptr()););
     }
 
@@ -554,7 +559,7 @@ public:
         if (m_c.sat_enabled()) {
             // SAT solver core extracts some model 
             // during unsat core computation.
-            s().get_model(mdl);            
+            s().get_model(mdl);
         }
         else {
             w = m_mus.get_best_model(mdl);

src/opt/opt_context.cpp

@@ -451,7 +451,7 @@ namespace opt {
             m_maxsat_engine != symbol("sls")) {
             return;
         }
-        m_params.set_bool("minimize_core", true);
+        m_params.set_bool("minimize_core_partial", true);
         m_sat_solver = mk_inc_sat_solver(m, m_params);
         unsigned sz = get_solver().get_num_assertions();
         for (unsigned i = 0; i < sz; ++i) {

src/sat/sat_config.cpp

@@ -105,6 +105,7 @@ namespace sat {
         }
         m_minimize_lemmas = p.minimize_lemmas();
         m_minimize_core   = p.minimize_core();
+        m_minimize_core_partial   = p.minimize_core_partial();
         m_optimize_model  = p.optimize_model();
         m_dyn_sub_res     = p.dyn_sub_res();
     }

src/sat/sat_config.h

@@ -69,6 +69,7 @@ namespace sat {
         bool               m_minimize_lemmas;
         bool               m_dyn_sub_res;
         bool               m_minimize_core;
+        bool               m_minimize_core_partial;
         bool               m_optimize_model;
 
 

src/sat/sat_mus.cpp

@@ -41,7 +41,9 @@ namespace sat {
     }
 
     lbool mus::operator()() {
+        bool minimize_partial = s.m_config.m_minimize_core_partial;
         flet<bool> _disable_min(s.m_config.m_minimize_core, false);
+        flet<bool> _disable_min_partial(s.m_config.m_minimize_core_partial, false);
         flet<bool> _disable_opt(s.m_config.m_optimize_model, false);
         flet<bool> _is_active(m_is_active, true);
         TRACE("sat", tout << "old core: " << s.get_core() << "\n";);
@@ -58,7 +60,7 @@ namespace sat {
                 --i;
             }
         }
-
+        unsigned delta_time  = 0;
         while (!core.empty()) {
             IF_VERBOSE(2, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
             TRACE("sat", 
@@ -69,6 +71,11 @@ namespace sat {
                 set_core();
                 return l_undef;
             }
+            if (minimize_partial && delta_time > 4) {
+                break;
+            }
+            unsigned num_literals = core.size() + mus.size();
+
             literal lit = core.back();
             core.pop_back();
             unsigned sz = mus.size();
@@ -99,14 +106,6 @@ namespace sat {
                 if (new_core.contains(~lit)) {
                     mus.resize(sz);
                     break;
-#if 0
-                    mus.pop_back();
-                    is_sat = s.check(mus.size(), mus.c_ptr());
-                    SASSERT(is_sat != l_true);
-                    if (is_sat != l_false) {
-                        return l_undef;
-                    }
-#endif 
                 }
                 mus.resize(sz);
                 TRACE("sat", tout << "new core: " << new_core << "\n";);
@@ -119,6 +118,14 @@ namespace sat {
                 }
                 break;
             }
+
+            unsigned new_num_literals = core.size() + mus.size();
+            if (new_num_literals == num_literals) {
+                delta_time++;
+            }
+            else {
+                delta_time = 0;
+            }
         }
         TRACE("sat", tout << "new core: " << mus << "\n";);
         set_core();

src/sat/sat_params.pyg

@@ -19,5 +19,6 @@ def_module_params('sat',
                           ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
                           ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
                           ('minimize_core', BOOL, False, 'minimize computed core'),
+                          ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

src/sat/sat_solver.cpp

@@ -1730,7 +1730,7 @@ namespace sat {
             idx--;
         }        
         reset_unmark(old_size);
-        if (m_config.m_minimize_core) {
+        if (m_config.m_minimize_core || m_config.m_minimize_core_partial) {
             // TBD: 
             // apply optional clause minimization by detecting subsumed literals.
             // initial experiment suggests it has no effect.

src/smt/theory_arith_core.h

@@ -938,7 +938,7 @@ namespace smt {
                     m_new_atoms.pop_back();
                     --i;
                 }
-            }
+            }            
             ptr_vector<atom> occs(m_var_occs[v]);
 
             std::sort(atoms.begin(), atoms.end(), compare_atoms());