From 4d8d705b3f72cb0b78c4c4e8779203e5c6e16a7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2017 08:02:24 -0800 Subject: [PATCH 1/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 2/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; } From 256a0e2d8291b722bf286a828f481f98d28fe568 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2017 12:12:26 -0800 Subject: [PATCH 3/4] move exchange par Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 9 ++++----- src/sat/sat_solver.h | 1 + 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index fff9ee6e4..376b4f8d5 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -84,7 +84,7 @@ namespace sat { VERIFY(v == mk_var(ext, dvar)); } } - unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim; + unsigned sz = src.init_trail_size(); for (unsigned i = 0; i < sz; ++i) { assign(src.m_trail[i], justification()); } @@ -774,7 +774,6 @@ namespace sat { restart(); simplify_problem(); - exchange_par(); if (check_inconsistent()) return l_false; gc(); @@ -890,9 +889,8 @@ namespace sat { */ void solver::exchange_par() { if (m_par && scope_lvl() == 0) { - unsigned sz = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; + unsigned sz = init_trail_size(); unsigned num_in = 0, num_out = 0; - SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD literal_vector in, out; for (unsigned i = m_par_limit_out; i < sz; ++i) { literal lit = m_trail[i]; @@ -2546,6 +2544,7 @@ namespace sat { void solver::pop_reinit(unsigned num_scopes) { pop(num_scopes); + exchange_par(); reinit_assumptions(); } @@ -2865,7 +2864,7 @@ namespace sat { } void solver::display_units(std::ostream & out) const { - unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; + unsigned end = init_trail_size(); for (unsigned i = 0; i < end; i++) { out << m_trail[i] << " "; } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 54b8a9bb2..f910e374f 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -223,6 +223,7 @@ namespace sat { lbool value(bool_var v) const { return static_cast(m_assignment[literal(v, false).index()]); } unsigned lvl(bool_var v) const { return m_level[v]; } unsigned lvl(literal l) const { return m_level[l.var()]; } + unsigned init_trail_size() const { return scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; } void assign(literal l, justification j) { TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";); switch (value(l)) { From 9cfd412cd0f2fbc389eaed51cc585604304f143e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2017 15:28:29 -0800 Subject: [PATCH 4/4] enable pb theory always as pb terms can be introduced during transformations. Issue #884 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 8 ++++---- src/sat/sat_simplifier.cpp | 1 - 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 46122d619..56b152caa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -570,11 +570,11 @@ namespace opt { m_opt_solver = alloc(opt_solver, m, m_params, m_fm); m_opt_solver->set_logic(m_logic); m_solver = m_opt_solver.get(); + m_opt_solver->ensure_pb(); - if (opt_params(m_params).priority() == symbol("pareto") || - (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) { - m_opt_solver->ensure_pb(); - } + //if (opt_params(m_params).priority() == symbol("pareto") || + // (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) { + //} } void context::setup_arith_solver() { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 62fb99a11..bd975115b 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -154,7 +154,6 @@ namespace sat { if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) return; - initialize(); CASSERT("sat_solver", s.check_invariant());