From 0ec567fe15b8e5cd60a542d2727846359b250e76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Feb 2021 15:47:40 -0800 Subject: [PATCH] integrate v2 of lns --- src/muz/spacer/spacer_iuc_solver.h | 3 + src/opt/maxres.cpp | 55 +++--- src/opt/opt_lns.cpp | 181 +++++++++++------- src/opt/opt_lns.h | 36 +++- src/opt/opt_solver.h | 5 +- src/sat/sat_solver.cpp | 11 +- src/sat/sat_solver.h | 5 +- src/sat/sat_solver/inc_sat_solver.cpp | 22 ++- src/smt/smt_kernel.h | 5 + src/smt/smt_solver.cpp | 7 +- src/solver/combined_solver.cpp | 3 + src/solver/solver.h | 8 + src/solver/solver_pool.cpp | 3 + src/solver/tactic2solver.cpp | 3 + .../fd_solver/bounded_int2bv_solver.cpp | 3 + src/tactic/fd_solver/enum2bv_solver.cpp | 3 + src/tactic/fd_solver/pb2bv_solver.cpp | 3 + src/tactic/fd_solver/smtfd_solver.cpp | 3 + 18 files changed, 254 insertions(+), 105 deletions(-) diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h index fc55d31ac..40d3ea95d 100644 --- a/src/muz/spacer/spacer_iuc_solver.h +++ b/src/muz/spacer/spacer_iuc_solver.h @@ -121,6 +121,9 @@ public: void assert_expr_core(expr *t) override { m_solver.assert_expr(t); } void assert_expr_core2(expr *t, expr *a) override { NOT_IMPLEMENTED_YET(); } void set_phase(expr* e) override { m_solver.set_phase(e); } + phase* get_phase() override { return m_solver.get_phase(); } + void set_phase(phase* p) override { m_solver.set_phase(p); } + void move_to_front(expr* e) override { m_solver.move_to_front(e); } expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); } void get_levels(ptr_vector const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); } expr_ref_vector get_trail() override { return m_solver.get_trail(); } diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 139b22ca2..7f4dbdb1e 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -83,6 +83,18 @@ private: memset(this, 0, sizeof(*this)); } }; + + struct lns_maxres : public lns_context { + maxres& i; + lns_maxres(maxres& i) :i(i) {} + ~lns_maxres() override {} + void update_model(model_ref& mdl) override { i.update_assignment(mdl); } + void relax_cores(vector const& cores) override { i.relax_cores(cores); } + rational cost(model& mdl) override { return i.cost(mdl); } + rational weight(expr* e) override { return i.m_asm2weight[e]; } + expr_ref_vector const& soft() override { return i.m_asms; } + }; + unsigned m_index; stats m_stats; expr_ref_vector m_B; @@ -95,6 +107,8 @@ private: strategy_t m_st; rational m_max_upper; model_ref m_csmodel; + lns_maxres m_lnsctx; + lns m_lns; unsigned m_correction_set_size; bool m_found_feasible_optimum; bool m_hill_climb; // prefer large weight soft clauses for cores @@ -125,6 +139,8 @@ public: m_mus(c.get_solver()), m_trail(m), m_st(st), + m_lnsctx(*this), + m_lns(s(), m_lnsctx), m_correction_set_size(0), m_found_feasible_optimum(false), m_hill_climb(true), @@ -507,9 +523,10 @@ public: void update_model(expr* def, expr* value) { SASSERT(is_uninterp_const(def)); - if (m_csmodel) { - m_csmodel->register_decl(to_app(def)->get_decl(), (*m_csmodel)(value)); - } + if (m_csmodel) + m_csmodel->register_decl(to_app(def)->get_decl(), (*m_csmodel)(value)); + if (m_model) + m_model->register_decl(to_app(def)->get_decl(), (*m_model)(value)); } void process_unsat(exprs const& core, rational w) { @@ -729,7 +746,7 @@ public: fml = m.mk_and(b_i1, cls); update_model(asum, fml); } - fml = m.mk_or(cs.size(), cs.c_ptr()); + fml = m.mk_or(cs); add(fml); } @@ -742,21 +759,13 @@ public: update_assignment(mdl); } + + void improve_model(model_ref& mdl) { if (!m_enable_lns) return; flet _disable_lns(m_enable_lns, false); - std::function update_model = [&](model_ref& mdl) { - update_assignment(mdl); - }; - std::function const&)> _relax_cores = [&](vector const& cores) { - relax_cores(cores); - }; - - lns lns(s(), update_model); - lns.set_conflicts(m_lns_conflicts); - lns.set_relax(_relax_cores); - lns.climb(mdl, m_asms); + m_lns.climb(mdl); } void relax_cores(vector const& cores) { @@ -770,6 +779,13 @@ public: process_unsat(wcores); } + rational cost(model& mdl) { + rational upper(0); + for (soft& s : m_soft) + if (!mdl.is_true(s.s)) + upper += s.weight; + return upper; + } void update_assignment(model_ref & mdl) { improve_model(mdl); @@ -787,14 +803,7 @@ public: TRACE("opt_verbose", tout << *mdl;); - rational upper(0); - - for (soft& s : m_soft) { - TRACE("opt", tout << s.s << ": " << (*mdl)(s.s) << " " << s.weight << "\n";); - if (!mdl->is_true(s.s)) { - upper += s.weight; - } - } + rational upper = cost(*mdl); if (upper > m_upper) { TRACE("opt", tout << "new upper: " << upper << " vs existing upper: " << m_upper << "\n";); diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp index 21ba939e1..f4229e81d 100644 --- a/src/opt/opt_lns.cpp +++ b/src/opt/opt_lns.cpp @@ -25,12 +25,12 @@ Author: namespace opt { - lns::lns(solver& s, std::function& update_model) + lns::lns(solver& s, lns_context& ctx) : m(s.get_manager()), s(s), + ctx(ctx), m_hardened(m), - m_soft(m), - m_update_model(update_model) + m_unprocessed(m) {} void lns::set_lns_params() { @@ -39,7 +39,7 @@ namespace opt { p.set_uint("restart.initial", 1000000); p.set_uint("max_conflicts", m_max_conflicts); p.set_uint("simplify.delay", 1000000); -// p.set_bool("gc.burst", true); + // p.set_bool("gc.burst", true); s.updt_params(p); } @@ -52,17 +52,99 @@ namespace opt { p.set_uint("gc.burst", sp.gc_burst()); } - unsigned lns::climb(model_ref& mdl, expr_ref_vector const& asms) { + unsigned lns::climb(model_ref& mdl) { + IF_VERBOSE(1, verbose_stream() << "(opt.lns :climb)\n"); m_num_improves = 0; params_ref old_p(s.get_params()); save_defaults(old_p); set_lns_params(); - setup_assumptions(mdl, asms); - unsigned num_improved = improve_linear(mdl); - // num_improved += improve_rotate(mdl, asms); + update_best_model(mdl); + for (unsigned i = 0; i < 2; ++i) + improve_bs(); + IF_VERBOSE(1, verbose_stream() << "(opt.lns :relax-cores " << m_cores.size() << ")\n"); + relax_cores(); s.updt_params(old_p); - IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n"); - return num_improved; + IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << ")\n"); + return m_num_improves; + } + + void lns::update_best_model(model_ref& mdl) { + rational cost = ctx.cost(*mdl); + if (m_best_cost.is_zero() || m_best_cost >= cost) { + m_best_cost = cost; + m_best_model = mdl; + m_best_phase = s.get_phase(); + m_best_bound = 0; + for (expr* e : ctx.soft()) + if (!mdl->is_true(e)) + m_best_bound += 1; + } + } + + void lns::apply_best_model() { + s.set_phase(m_best_phase.get()); + for (expr* e : m_unprocessed) { + s.move_to_front(e); + s.set_phase(e); + } + } + + void lns::improve_bs() { + m_unprocessed.reset(); + m_unprocessed.append(ctx.soft()); + + m_hardened.reset(); + for (expr* a : ctx.soft()) + m_is_assumption.mark(a); + shuffle(m_unprocessed.size(), m_unprocessed.c_ptr(), m_rand); + + model_ref mdl = m_best_model->copy(); + unsigned j = 0; + for (unsigned i = 0; i < m_unprocessed.size(); ++i) { + if (mdl->is_false(unprocessed(i))) { + expr_ref tmp(m_unprocessed.get(j), m); + m_unprocessed[j++] = m_unprocessed[i]; + m_unprocessed[i] = tmp; + break; + } + } + for (unsigned i = j; i < m_unprocessed.size(); ++i) { + if (mdl->is_true(unprocessed(i))) { + expr_ref tmp(m_unprocessed.get(j), m); + m_unprocessed[j++] = m_unprocessed[i]; + m_unprocessed[i] = tmp; + } + } + for (unsigned i = 0; i < 3 && !m_unprocessed.empty(); ++i) + improve_bs1(); + } + + void lns::improve_bs1() { + model_ref mdl = m_best_model->copy(); + unsigned j = 0; + for (expr* e : m_unprocessed) { + if (!m.inc()) + return; + if (mdl->is_true(e)) + m_hardened.push_back(e); + else { + apply_best_model(); + switch (improve_step(mdl, e)) { + case l_true: + m_hardened.push_back(e); + ctx.update_model(mdl); + update_best_model(mdl); + break; + case l_false: + m_hardened.push_back(m.mk_not(e)); + break; + case l_undef: + m_unprocessed[j++] = e; + break; + } + } + } + m_unprocessed.shrink(j); } struct lns::scoped_bounding { @@ -72,12 +154,13 @@ namespace opt { scoped_bounding(lns& l):m_lns(l) { if (!m_lns.m_enable_scoped_bounding) return; + if (m_lns.m_best_bound == 0) + return; m_cores_are_valid = m_lns.m_cores_are_valid; m_lns.m_cores_are_valid = false; m_lns.s.push(); pb_util pb(m_lns.m); - // TBD: bound should to be adjusted for current best solution, not number of soft constraints left. - expr_ref bound(pb.mk_at_most_k(m_lns.m_soft, m_lns.m_soft.size() - 1), m_lns.m); + expr_ref bound(pb.mk_at_most_k(m_lns.ctx.soft(), m_lns.m_best_bound - 1), m_lns.m); m_lns.s.assert_expr(bound); } ~scoped_bounding() { @@ -89,7 +172,7 @@ namespace opt { }; void lns::relax_cores() { - if (!m_cores.empty() && m_relax_cores && m_cores_are_valid) { + if (!m_cores.empty() && m_cores_are_valid) { std::sort(m_cores.begin(), m_cores.end(), [&](expr_ref_vector const& a, expr_ref_vector const& b) { return a.size() < b.size(); }); unsigned num_disjoint = 0; vector new_cores; @@ -104,43 +187,14 @@ namespace opt { new_cores.push_back(c); ++num_disjoint; } - m_relax_cores(new_cores); + IF_VERBOSE(2, verbose_stream() << "num cores: " << m_cores.size() << " new cores: " << new_cores.size() << "\n"); + ctx.relax_cores(new_cores); } m_in_core.reset(); m_is_assumption.reset(); m_cores.reset(); } - void lns::setup_assumptions(model_ref& mdl, expr_ref_vector const& asms) { - m_hardened.reset(); - m_soft.reset(); - for (expr* a : asms) { - m_is_assumption.mark(a); - if (mdl->is_true(a)) - m_hardened.push_back(a); - else - m_soft.push_back(a); - } - } - - unsigned lns::improve_rotate(model_ref& mdl, expr_ref_vector const& asms) { - unsigned num_improved = 0; - repeat: - setup_assumptions(mdl, asms); - unsigned sz = m_hardened.size(); - for (unsigned i = 0; i < sz; ++i) { - expr_ref tmp(m_hardened.get(i), m); - m_hardened[i] = m.mk_not(tmp); - unsigned reward = improve_linear(mdl); - if (reward > 1) { - num_improved += (reward - 1); - goto repeat; - } - setup_assumptions(mdl, asms); - } - return num_improved; - } - unsigned lns::improve_linear(model_ref& mdl) { scoped_bounding _scoped_bouding(*this); unsigned num_improved = 0; @@ -156,43 +210,42 @@ namespace opt { set_lns_params(); } m_max_conflicts = max_conflicts; - relax_cores(); return num_improved; } unsigned lns::improve_step(model_ref& mdl) { unsigned num_improved = 0; - for (unsigned i = 0; m.inc() && i < m_soft.size(); ++i) { - switch (improve_step(mdl, soft(i))) { + for (unsigned i = 0; m.inc() && i < m_unprocessed.size(); ++i) { + switch (improve_step(mdl, unprocessed(i))) { case l_undef: break; case l_false: - TRACE("opt", tout << "pruned " << mk_bounded_pp(soft(i), m) << "\n";); - m_hardened.push_back(m.mk_not(soft(i))); - for (unsigned k = i; k + 1 < m_soft.size(); ++k) - m_soft[k] = soft(k + 1); - m_soft.pop_back(); + TRACE("opt", tout << "pruned " << mk_bounded_pp(unprocessed(i), m) << "\n";); + m_hardened.push_back(m.mk_not(unprocessed(i))); + for (unsigned k = i; k + 1 < m_unprocessed.size(); ++k) + m_unprocessed[k] = unprocessed(k + 1); + m_unprocessed.pop_back(); --i; break; case l_true: { unsigned k = 0, offset = 0; - for (unsigned j = 0; j < m_soft.size(); ++j) { - if (mdl->is_true(soft(j))) { + for (unsigned j = 0; j < m_unprocessed.size(); ++j) { + if (mdl->is_true(unprocessed(j))) { if (j <= i) ++offset; ++m_num_improves; - TRACE("opt", tout << "improved " << mk_bounded_pp(soft(j), m) << "\n";); - m_hardened.push_back(soft(j)); + TRACE("opt", tout << "improved " << mk_bounded_pp(unprocessed(j), m) << "\n";); + m_hardened.push_back(unprocessed(j)); ++num_improved; } else { - m_soft[k++] = soft(j); + m_unprocessed[k++] = unprocessed(j); } } - m_soft.shrink(k); + m_unprocessed.shrink(k); i -= offset; - IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n"); - m_update_model(mdl); + IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_unprocessed.size() << ")\n"); + ctx.update_model(mdl); break; } } @@ -209,12 +262,12 @@ namespace opt { if (r == l_false) { expr_ref_vector core(m); s.get_unsat_core(core); - bool all_assumed = true; + bool all_assumed = true; for (expr* c : core) all_assumed &= m_is_assumption.is_marked(c); - if (all_assumed) { - m_cores.push_back(core); - } + IF_VERBOSE(2, verbose_stream() << "core " << all_assumed << " - " << core.size() << "\n"); + if (all_assumed) + m_cores.push_back(core); } return r; } diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h index 26b4c6e4a..8e16ec5c8 100644 --- a/src/opt/opt_lns.h +++ b/src/opt/opt_lns.h @@ -26,39 +26,55 @@ Author: namespace opt { + class lns_context { + public: + virtual ~lns_context() {} + virtual void update_model(model_ref& mdl) = 0; + virtual void relax_cores(vector const& cores) = 0; + virtual rational cost(model& mdl) = 0; + virtual rational weight(expr* e) = 0; + virtual expr_ref_vector const& soft() = 0; + }; + class lns { ast_manager& m; solver& s; + lns_context& ctx; + random_gen m_rand; expr_ref_vector m_hardened; - expr_ref_vector m_soft; - unsigned m_max_conflicts { 1000 }; + expr_ref_vector m_unprocessed; + unsigned m_max_conflicts { 10000 }; unsigned m_num_improves { 0 }; bool m_cores_are_valid { true }; bool m_enable_scoped_bounding { false }; + unsigned m_best_bound { 0 }; + rational m_best_cost; + model_ref m_best_model; + scoped_ptr m_best_phase; + vector m_cores; expr_mark m_in_core; expr_mark m_is_assumption; struct scoped_bounding; - std::function m_update_model; - std::function const&)> m_relax_cores; + void update_best_model(model_ref& mdl); + void improve_bs(); + void improve_bs1(); + void apply_best_model(); - expr* soft(unsigned i) const { return m_soft[i]; } + expr* unprocessed(unsigned i) const { return m_unprocessed[i]; } void set_lns_params(); void save_defaults(params_ref& p); unsigned improve_step(model_ref& mdl); lbool improve_step(model_ref& mdl, expr* e); void relax_cores(); unsigned improve_linear(model_ref& mdl); - unsigned improve_rotate(model_ref& mdl, expr_ref_vector const& asms); - void setup_assumptions(model_ref& mdl, expr_ref_vector const& asms); public: - lns(solver& s, std::function& update_model); - void set_relax(std::function const&)>& rc) { m_relax_cores = rc; } + lns(solver& s, lns_context& ctx); void set_conflicts(unsigned c) { m_max_conflicts = c; } - unsigned climb(model_ref& mdl, expr_ref_vector const& asms); + unsigned climb(model_ref& mdl); }; }; diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 396de5aea..f22a90a2f 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -110,7 +110,10 @@ namespace opt { void get_levels(ptr_vector const& vars, unsigned_vector& depth) override; expr_ref_vector get_trail() override { return m_context.get_trail(); } expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); } - void set_phase(expr* e) override { NOT_IMPLEMENTED_YET(); } + void set_phase(expr* e) override { m_context.set_phase(e); } + phase* get_phase() override { return m_context.get_phase(); } + void set_phase(phase* p) override { m_context.set_phase(p); } + void move_to_front(expr* e) override { m_context.move_to_front(e); } void set_logic(symbol const& logic); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 09588a77b..ec2b473d1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1914,7 +1914,8 @@ namespace sat { m_next_simplify = m_config.m_simplify_delay; m_min_d_tk = 1.0; m_search_lvl = 0; - m_conflicts_since_gc = 0; + if (m_learned.size() <= 2*m_clauses.size()) + m_conflicts_since_gc = 0; m_restart_next_out = 0; m_asymm_branch.init_search(); m_stopwatch.reset(); @@ -3784,6 +3785,14 @@ namespace sat { } } + void solver::move_to_front(bool_var b) { + if (b >= num_vars()) + return; + bool_var next = m_case_split_queue.min_var(); + auto next_act = m_activity[next]; + set_activity(b, next_act + 1); + } + // ----------------------- // // Iterators diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 08cd63aaf..3ed0f51d6 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -352,8 +352,9 @@ namespace sat { bool was_eliminated(bool_var v) const { return m_eliminated[v]; } void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } - void set_phase(literal l) override { m_best_phase[l.var()] = m_phase[l.var()] = !l.sign(); } - void set_phase(bool_var b, bool sign) { set_phase(literal(b, sign)); } + void set_phase(literal l) override { if (l.var() < num_vars()) m_best_phase[l.var()] = m_phase[l.var()] = !l.sign(); } + bool_var get_phase(bool_var b) { return m_phase.get(b, false); } + void move_to_front(bool_var b); unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 1dbdc3582..65a096b20 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -298,7 +298,27 @@ public: bool is_not = m.is_not(e, e); sat::bool_var b = m_map.to_bool_var(e); if (b != sat::null_bool_var) - m_solver.set_phase(b, is_not); + m_solver.set_phase(sat::literal(b, is_not)); + } + + class sat_phase : public phase, public sat::literal_vector {}; + + phase* get_phase() override { + sat_phase* p = alloc(sat_phase); + for (unsigned v = m_solver.num_vars(); v-- > 0; ) { + p->push_back(sat::literal(v, !m_solver.get_phase(v))); + } + return p; + } + void set_phase(phase* p) override { + for (auto lit : *static_cast(p)) + m_solver.set_phase(lit); + } + void move_to_front(expr* e) override { + bool is_not = m.is_not(e, e); + sat::bool_var b = m_map.to_bool_var(e); + if (b != sat::null_bool_var) + m_solver.move_to_front(b); } unsigned get_scope_level() const override { diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index cb64f7d13..5218df623 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -150,6 +150,11 @@ namespace smt { */ lbool preferred_sat(expr_ref_vector const& asms, vector& cores); + void set_phase(expr * e) { NOT_IMPLEMENTED_YET(); } + solver::phase* get_phase() { NOT_IMPLEMENTED_YET(); return nullptr; } + void set_phase(solver::phase* p) { NOT_IMPLEMENTED_YET(); } + void move_to_front(expr* e) { NOT_IMPLEMENTED_YET(); } + /** \brief Return the model associated with the last check command. */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 58a3768c4..6e600992a 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -158,9 +158,10 @@ namespace { void assert_expr_core(expr * t) override { m_context.assert_expr(t); } - void set_phase(expr* e) override { - NOT_IMPLEMENTED_YET(); - } + void set_phase(expr* e) override { m_context.set_phase(e); } + phase* get_phase() override { return m_context.get_phase(); } + void set_phase(phase* p) override { m_context.set_phase(p); } + void move_to_front(expr* e) override { m_context.move_to_front(e); } void assert_expr_core2(expr * t, expr * a) override { if (m_name2assertion.contains(a)) { diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 9369d5882..b95d2d7f8 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -136,6 +136,9 @@ public: } void set_phase(expr* e) override { m_solver1->set_phase(e); m_solver2->set_phase(e); } + solver::phase* get_phase() override { auto* p = m_solver1->get_phase(); if (!p) p = m_solver2->get_phase(); return p; } + void set_phase(solver::phase* p) override { m_solver1->set_phase(p); m_solver2->set_phase(p); } + void move_to_front(expr* e) override { m_solver1->move_to_front(e); m_solver2->move_to_front(e); } void updt_params(params_ref const & p) override { solver::updt_params(p); diff --git a/src/solver/solver.h b/src/solver/solver.h index 078d402a2..b324368b1 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -112,6 +112,14 @@ public: } virtual void set_phase(expr* e) = 0; + virtual void move_to_front(expr* e) = 0; + + class phase { public: virtual ~phase() {} }; + + virtual phase* get_phase() = 0; + + virtual void set_phase(phase* p) = 0; + void assert_expr(ptr_vector const& ts) { for (expr* e : ts) assert_expr(e); diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 997c3343d..baaf17dc6 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -69,6 +69,9 @@ public: solver* base_solver() { return m_base.get(); } void set_phase(expr* e) override { m_base->set_phase(e); } + phase* get_phase() override { return m_base->get_phase(); } + void set_phase(phase* p) override { m_base->set_phase(p); } + void move_to_front(expr* e) override { m_base->move_to_front(e); } solver* translate(ast_manager& m, params_ref const& p) override { UNREACHABLE(); return nullptr; } void updt_params(params_ref const& p) override { diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 0985478d3..06cab4462 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -80,6 +80,9 @@ public: unsigned get_num_assertions() const override; expr * get_assertion(unsigned idx) const override; void set_phase(expr* e) override { } + phase* get_phase() override { return nullptr; } + void set_phase(phase* p) override { } + void move_to_front(expr* e) override { } expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override { diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index 2df5d0003..e907abc72 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -152,6 +152,9 @@ public: void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); } void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); } void set_phase(expr* e) override { m_solver->set_phase(e); } + phase* get_phase() override { return m_solver->get_phase(); } + void set_phase(phase* p) override { m_solver->set_phase(p); } + void move_to_front(expr* e) override { m_solver->move_to_front(e); } void get_model_core(model_ref & mdl) override { m_solver->get_model(mdl); if (mdl) { diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index b922a4bf9..80e265676 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -90,6 +90,9 @@ public: void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); } void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); } void set_phase(expr* e) override { m_solver->set_phase(e); } + phase* get_phase() override { return m_solver->get_phase(); } + void set_phase(phase* p) override { m_solver->set_phase(p); } + void move_to_front(expr* e) override { m_solver->move_to_front(e); } void get_model_core(model_ref & mdl) override { m_solver->get_model(mdl); if (mdl) { diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp index b574e4789..f5d493af6 100644 --- a/src/tactic/fd_solver/pb2bv_solver.cpp +++ b/src/tactic/fd_solver/pb2bv_solver.cpp @@ -97,6 +97,9 @@ public: } } void set_phase(expr* e) override { m_solver->set_phase(e); } + phase* get_phase() override { return m_solver->get_phase(); } + void set_phase(phase* p) override { m_solver->set_phase(p); } + void move_to_front(expr* e) override { m_solver->move_to_front(e); } void get_levels(ptr_vector const& vars, unsigned_vector& depth) override { m_solver->get_levels(vars, depth); diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 7cd27cd62..8e91c2c9f 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -2032,6 +2032,9 @@ namespace smtfd { } void set_phase(expr* e) override {} + phase* get_phase() override { return nullptr; } + void set_phase(phase* p) override { } + void move_to_front(expr* e) override { } void updt_params(params_ref const & p) override { ::solver::updt_params(p);