combine PS_THEORY with cache on/off mode

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

src/smt/params/smt_params.cpp

@@ -39,6 +39,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_max_conflicts = p.max_conflicts();
     m_restart_max   = p.restart_max();
     m_threads       = p.threads();
+    m_threads_max_conflicts  = p.threads_max_conflicts();
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
     m_string_solver = p.string_solver();
@@ -100,6 +101,7 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_minimize_lemmas);
     DISPLAY_PARAM(m_max_conflicts);
     DISPLAY_PARAM(m_threads);
+    DISPLAY_PARAM(m_threads_max_conflicts);
     DISPLAY_PARAM(m_simplify_clauses);
     DISPLAY_PARAM(m_tick);
     DISPLAY_PARAM(m_display_features);

src/smt/params/smt_params.h

@@ -104,6 +104,7 @@ struct smt_params : public preprocessor_params,
     unsigned         m_max_conflicts;
     unsigned         m_restart_max;
     unsigned         m_threads;
+    unsigned         m_threads_max_conflicts;
     bool             m_simplify_clauses;
     unsigned         m_tick;
     bool             m_display_features;
@@ -255,6 +256,7 @@ struct smt_params : public preprocessor_params,
         m_minimize_lemmas(true),
         m_max_conflicts(UINT_MAX),
         m_threads(1),
+        m_threads_max_conflicts(UINT_MAX),
         m_simplify_clauses(true),
         m_tick(1000),
         m_display_features(false),

src/smt/params/smt_params_helper.pyg

@@ -21,6 +21,7 @@ def_module_params(module_name='smt',
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
                           ('threads', UINT, 1, 'maximal number of parallel threads.'),
+                          ('threads.max_conflicts', UINT, 400, 'maximal number of conflicts between rounds of cubing for parallel SMT'),
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
                           ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),

src/smt/smt_context.cpp

@@ -1850,15 +1850,24 @@ namespace smt {
             else {
                 switch (m_fparams.m_phase_selection) {
                 case PS_THEORY: 
-                    if (d.is_theory_atom()) {
+                    if (m_phase_cache_on && d.m_phase_available) {
+                        is_pos = m_bdata[var].m_phase;
+                    }
+                    else if (!m_phase_cache_on && d.is_theory_atom()) {
                         theory * th = m_theories.get_plugin(d.get_theory());
                         lbool ph = th->get_phase(var);
                         if (ph != l_undef) {
                             is_pos = ph == l_true;
-                            break;
+                        }
+                        else {
+                            is_pos = m_phase_default;
                         }
                     }
-                    Z3_fallthrough;
+                    else {
+                        TRACE("phase_selection", tout << "setting to false\n";);
+                        is_pos = m_phase_default;
+                    }
+                    break;
                 case PS_CACHING:
                 case PS_CACHING_CONSERVATIVE:
                 case PS_CACHING_CONSERVATIVE2:

src/smt/smt_parallel.cpp

@@ -45,7 +45,7 @@ namespace smt {
         unsigned error_code = 0;
         bool done = false;
         unsigned num_rounds = 0;
-        unsigned max_conflicts = 400;
+        unsigned max_conflicts = ctx.get_fparams().m_threads_max_conflicts;
 
         for (unsigned i = 0; i < num_threads; ++i) {
             ast_manager* new_m = alloc(ast_manager, m, true);
@@ -87,10 +87,10 @@ namespace smt {
                 }
             }
 
+            unsigned sz = unit_trail.size();
             for (unsigned i = 0; i < num_threads; ++i) {
                 context& pctx = *pctxs[i];
                 ast_translation tr(ctx.m, pctx.m);
-                unsigned sz = unit_trail.size();
                 for (unsigned j = unit_lim[i]; j < sz; ++j) {
                     expr_ref src(ctx.m), dst(pctx.m);
                     dst = tr(unit_trail.get(j));
@@ -105,7 +105,7 @@ namespace smt {
 
         auto worker_thread = [&](int i) {
             try {
-                IF_VERBOSE(0, verbose_stream() << "thread " << i << "\n";);
+                IF_VERBOSE(1, verbose_stream() << "thread " << i << "\n";);
                 context& pctx = *pctxs[i];
                 ast_manager& pm = *pms[i];
                 expr_ref_vector lasms(pasms[i]);
@@ -146,14 +146,16 @@ namespace smt {
             catch (z3_error & err) {
                 error_code = err.error_code();
                 ex_kind = ERROR_EX;                
+                done = true;
             }
             catch (z3_exception & ex) {
                 ex_msg = ex.msg();
                 ex_kind = DEFAULT_EX;    
+                done = true;
             }
         };
 
-        while (!done) {
+        while (true) {
             vector<std::thread> threads(num_threads);
             for (unsigned i = 0; i < num_threads; ++i) {
                 threads[i] = std::thread([&, i]() { worker_thread(i); });