From 3da3b4178637533989d2ef021a7d9a7cdedaa7ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Feb 2020 19:22:28 -0800 Subject: [PATCH] ensure parallel mode works under push/pop Signed-off-by: Nikolaj Bjorner --- src/math/lp/lp_bound_propagator.cpp | 7 +++++++ src/smt/smt_context.cpp | 7 ++++--- src/smt/smt_context.h | 2 +- src/smt/smt_parallel.cpp | 8 ++++---- 4 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp index 2242d63e5..98ecda018 100644 --- a/src/math/lp/lp_bound_propagator.cpp +++ b/src/math/lp/lp_bound_propagator.cpp @@ -22,6 +22,9 @@ void lp_bound_propagator::try_add_bound(mpq const& v, unsigned j, bool is_low, b if (strict) kind = static_cast(kind / 2); +// static unsigned s_count = 0, a_count = 0; +// ++a_count; +// if ((a_count % 100000) == 0) std::cout << s_count << " / " << a_count << "\n"; if (!bound_is_interesting(j, kind, v)) return; unsigned k; // index to ibounds @@ -29,10 +32,12 @@ void lp_bound_propagator::try_add_bound(mpq const& v, unsigned j, bool is_low, b if (try_get_value(m_improved_lower_bounds, j, k)) { auto & found_bound = m_ibounds[k]; if (v > found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { +// ++s_count; found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); TRACE("try_add_bound", m_lar_solver.print_implied_bound(found_bound, tout);); } } else { +// ++s_count; m_improved_lower_bounds[j] = m_ibounds.size(); m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); TRACE("try_add_bound", m_lar_solver.print_implied_bound(m_ibounds.back(), tout);); @@ -41,10 +46,12 @@ void lp_bound_propagator::try_add_bound(mpq const& v, unsigned j, bool is_low, b if (try_get_value(m_improved_upper_bounds, j, k)) { auto & found_bound = m_ibounds[k]; if (v < found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict)) { +// ++s_count; found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); TRACE("try_add_bound", m_lar_solver.print_implied_bound(found_bound, tout);); } } else { +// ++s_count; m_improved_upper_bounds[j] = m_ibounds.size(); m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); TRACE("try_add_bound", m_lar_solver.print_implied_bound(m_ibounds.back(), tout);); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index d0dcf6e50..35c05cb15 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -155,15 +155,16 @@ namespace smt { return std::min(m_relevancy_lvl, m_fparams.m_relevancy_lvl); } - void context::copy(context& src_ctx, context& dst_ctx) { + void context::copy(context& src_ctx, context& dst_ctx, bool override_base) { ast_manager& dst_m = dst_ctx.get_manager(); ast_manager& src_m = src_ctx.get_manager(); src_ctx.pop_to_base_lvl(); - if (src_ctx.m_base_lvl > 0) { + if (!override_base && src_ctx.m_base_lvl > 0) { + INVOKE_DEBUGGER(); throw default_exception("Cloning contexts within a user-scope is not allowed"); } - SASSERT(src_ctx.m_base_lvl == 0); + SASSERT(src_ctx.m_base_lvl == 0 || override_base); ast_translation tr(src_m, dst_m, false); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 29b84f5c3..f25ff52e2 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1539,7 +1539,7 @@ namespace smt { */ context * mk_fresh(symbol const * l = nullptr, smt_params * smtp = nullptr, params_ref const & p = params_ref()); - static void copy(context& src, context& dst); + static void copy(context& src, context& dst, bool override_base = false); /** \brief Translate context to use new manager m. diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 82579e858..f19fafa37 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -33,9 +33,9 @@ namespace smt { unsigned thread_max_conflicts = ctx.get_fparams().m_threads_max_conflicts; unsigned max_conflicts = ctx.get_fparams().m_max_conflicts; -#if 0 - // TBD: try first sequential with a low conflict budget to make super easy problems cheap - ctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, 20); +#if 1 + // try first sequential with a low conflict budget to make super easy problems cheap + ctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, 40u); result = ctx.check(asms.size(), asms.c_ptr()); if (result != l_undef || ctx.m_num_conflicts < max_conflicts) { return result; @@ -65,7 +65,7 @@ namespace smt { pms.push_back(new_m); pctxs.push_back(alloc(context, *new_m, ctx.get_fparams(), ctx.get_params())); context& new_ctx = *pctxs.back(); - context::copy(ctx, new_ctx); + context::copy(ctx, new_ctx, true); new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed); ast_translation tr(*new_m, m); pasms.push_back(tr(asms));