From bdfa84c6fe135ba863093001cfedeb9c21baa432 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jan 2017 13:22:03 -0800 Subject: [PATCH 1/4] fix issues with running parallel solver: random strategy should not be a default on all solvers. Also reuse base solver Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 38 ++++++++++++++++++++++++++------------ 1 file changed, 26 insertions(+), 12 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e06ed3971..acfd79b90 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -797,29 +797,39 @@ namespace sat { lbool solver::check_par(unsigned num_lits, literal const* lits) { int num_threads = static_cast(m_config.m_num_parallel); + int num_extra_solvers = num_threads - 1; scoped_limits scoped_rlimit(rlimit()); - vector rlims(num_threads); - ptr_vector solvers(num_threads); + vector rlims(num_extra_solvers); + ptr_vector solvers(num_extra_solvers); sat::par par; - for (int i = 0; i < num_threads; ++i) { - m_params.set_uint("random_seed", i); - if (i < num_threads/2) { + symbol saved_phase = m_params.get_sym("phase", symbol("caching")); + for (int i = 0; i < num_extra_solvers; ++i) { + m_params.set_uint("random_seed", i + m_config.m_random_seed); + if (i == 1 + num_threads/2) { m_params.set_sym("phase", symbol("random")); - } + } solvers[i] = alloc(sat::solver, m_params, rlims[i], 0); solvers[i]->copy(*this); solvers[i]->set_par(&par); - scoped_rlimit.push_child(&solvers[i]->rlimit()); + scoped_rlimit.push_child(&solvers[i]->rlimit()); } + m_params.set_sym("phase", saved_phase); int finished_id = -1; std::string ex_msg; par_exception_kind ex_kind; unsigned error_code = 0; lbool result = l_undef; + flet _overwrite_thread_number(m_config.m_num_parallel, 1); #pragma omp parallel for for (int i = 0; i < num_threads; ++i) { try { - lbool r = solvers[i]->check(num_lits, lits); + lbool r = l_undef; + if (i < num_extra_solvers) { + r = solvers[i]->check(num_lits, lits); + } + else { + r = check(num_lits, lits); + } bool first = false; #pragma omp critical (par_solver) { @@ -830,14 +840,14 @@ namespace sat { } } if (first) { - if (r == l_true) { + if (r == l_true && i < num_extra_solvers) { set_model(solvers[i]->get_model()); } - else if (r == l_false) { + else if (r == l_false && i < num_extra_solvers) { m_core.reset(); m_core.append(solvers[i]->get_core()); } - for (int j = 0; j < num_threads; ++j) { + for (int j = 0; j < num_extra_solvers; ++j) { if (i != j) { rlims[j].cancel(); } @@ -857,7 +867,11 @@ namespace sat { } } } - for (int i = 0; i < num_threads; ++i) { + if (finished_id != -1 && finished_id < num_extra_solvers) { + m_stats = solvers[finished_id]->m_stats; + } + + for (int i = 0; i < num_extra_solvers; ++i) { dealloc(solvers[i]); } if (finished_id == -1) { From f015e3e4cc13f77cce3cd626b756abdd6f014236 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jan 2017 17:17:58 -0800 Subject: [PATCH 2/4] fix bug in propagation of parameters to combined solvers Signed-off-by: Nikolaj Bjorner --- src/sat/sat_config.cpp | 1 + src/sat/sat_solver.cpp | 5 +++-- src/solver/solver.h | 2 +- src/solver/solver2tactic.cpp | 1 + src/solver/tactic2solver.cpp | 2 +- 5 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index ccf538dfe..9206ea8bc 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -35,6 +35,7 @@ namespace sat { m_glue("glue"), m_glue_psm("glue_psm"), m_psm_glue("psm_glue") { + m_num_parallel = 1; updt_params(p); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index acfd79b90..fff9ee6e4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -804,7 +804,7 @@ namespace sat { sat::par par; symbol saved_phase = m_params.get_sym("phase", symbol("caching")); for (int i = 0; i < num_extra_solvers; ++i) { - m_params.set_uint("random_seed", i + m_config.m_random_seed); + m_params.set_uint("random_seed", m_rand()); if (i == 1 + num_threads/2) { m_params.set_sym("phase", symbol("random")); } @@ -813,13 +813,13 @@ namespace sat { solvers[i]->set_par(&par); scoped_rlimit.push_child(&solvers[i]->rlimit()); } + set_par(&par); m_params.set_sym("phase", saved_phase); int finished_id = -1; std::string ex_msg; par_exception_kind ex_kind; unsigned error_code = 0; lbool result = l_undef; - flet _overwrite_thread_number(m_config.m_num_parallel, 1); #pragma omp parallel for for (int i = 0; i < num_threads; ++i) { try { @@ -867,6 +867,7 @@ namespace sat { } } } + set_par(0); if (finished_id != -1 && finished_id < num_extra_solvers) { m_stats = solvers[finished_id]->m_stats; } diff --git a/src/solver/solver.h b/src/solver/solver.h index d5d9ccfd5..6b9d38f29 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -54,7 +54,7 @@ public: /** \brief Update the solver internal settings. */ - virtual void updt_params(params_ref const & p) {} + virtual void updt_params(params_ref const & p) { } /** \brief Store in \c r a description of the configuration diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 21ecdec32..1a02c97e6 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -93,6 +93,7 @@ public: {} virtual void updt_params(params_ref const & p) { + m_params.append(p); m_solver->updt_params(p); } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 34d2edd3c..150b19395 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -96,7 +96,7 @@ tactic2solver::~tactic2solver() { } void tactic2solver::updt_params(params_ref const & p) { - m_params = p; + m_params.append(p); } void tactic2solver::collect_param_descrs(param_descrs & r) { From 4d8d705b3f72cb0b78c4c4e8779203e5c6e16a7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2017 08:02:24 -0800 Subject: [PATCH 3/4] bypass combined solver when logic is set to QF_BV or QF_FD Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/smt_strategic_solver.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index d2414ec72..16e59302b 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -98,13 +98,19 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_default_tactic(m, p); } -static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { +static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { bv_rewriter rw(m); if (logic == "QF_BV" && rw.hi_div0()) return mk_inc_sat_solver(m, p); if (logic == "QF_FD") return mk_fd_solver(m, p); - return mk_smt_solver(m, p, logic); + return 0; +} + +static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { + solver* s = mk_special_solver_for_logic(m, p, logic); + if (!s) s = mk_smt_solver(m, p, logic); + return s; } class smt_strategic_solver_factory : public solver_factory { @@ -119,6 +125,8 @@ public: l = m_logic; else l = logic; + solver* s = mk_special_solver_for_logic(m, p, l); + if (s) return s; tactic * t = mk_tactic_for_logic(m, p, l); return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l), mk_solver_for_logic(m, p, l), From 40177f7bac4ab9615a32728154f6fd1fa6c8fcf9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2017 08:05:04 -0800 Subject: [PATCH 4/4] bypass combined solver when logic is set to QF_FD Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/smt_strategic_solver.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 16e59302b..a4a579ddd 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -99,17 +99,18 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const } static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { - bv_rewriter rw(m); - if (logic == "QF_BV" && rw.hi_div0()) - return mk_inc_sat_solver(m, p); if (logic == "QF_FD") return mk_fd_solver(m, p); return 0; } static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { + bv_rewriter rw(m); solver* s = mk_special_solver_for_logic(m, p, logic); - if (!s) s = mk_smt_solver(m, p, logic); + if (!s && logic == "QF_BV" && rw.hi_div0()) + s = mk_inc_sat_solver(m, p); + if (!s) + s = mk_smt_solver(m, p, logic); return s; }