From 74fc8cfde79b70b3109cf94d90dbc1a22b17b2e3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Feb 2020 09:50:00 -0800 Subject: [PATCH] combine PS_THEORY with cache on/off mode Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params.cpp | 2 ++ src/smt/params/smt_params.h | 2 ++ src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_context.cpp | 15 ++++++++++++--- src/smt/smt_parallel.cpp | 10 ++++++---- 5 files changed, 23 insertions(+), 7 deletions(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index ed2e13749..5d6313e15 100644 --- a/src/smt/params/smt_params.cpp +++ b/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); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index c2fca2c10..bd5d07f1c 100644 --- a/src/smt/params/smt_params.h +++ b/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), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index afc1f61e2..123f3d6c3 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/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'), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6bb8c1c50..746b53771 100644 --- a/src/smt/smt_context.cpp +++ b/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: diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 878ed0fb6..fcbb11954 100644 --- a/src/smt/smt_parallel.cpp +++ b/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 threads(num_threads); for (unsigned i = 0; i < num_threads; ++i) { threads[i] = std::thread([&, i]() { worker_thread(i); });