diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index bc1a18f15..3ffee518e 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -52,7 +52,7 @@ public: result.push_back(resg.get()); // report model if (g->models_enabled()) { - g->add(mk_ackermannize_bv_model_converter(m, lackr.get_info())); + resg->add(mk_ackermannize_bv_model_converter(m, lackr.get_info())); } resg->inc_depth(); diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt index 7f2a2b793..dcb13c062 100644 --- a/src/opt/CMakeLists.txt +++ b/src/opt/CMakeLists.txt @@ -4,7 +4,6 @@ z3_add_component(opt maxsmt.cpp opt_cmds.cpp opt_context.cpp - opt_lns.cpp opt_pareto.cpp opt_parse.cpp optsmt.cpp diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 61e003b90..b93149216 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -256,9 +256,6 @@ namespace opt { if (m_pareto) { return execute_pareto(); } - if (m_lns) { - return execute_lns(); - } if (m_box_index != UINT_MAX) { return execute_box(); } @@ -278,14 +275,10 @@ namespace opt { opt_params optp(m_params); symbol pri = optp.priority(); - if (pri == symbol("lns")) { - return execute_lns(); - } - display_benchmark(); - IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); - lbool is_sat = s.check_sat(0,nullptr); - TRACE("opt", tout << "initial search result: " << is_sat << "\n"; - s.display(tout);); + + IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n"); + lbool is_sat = s.check_sat(0,0); + TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); if (is_sat != l_false) { s.get_model(m_model); s.get_labels(m_labels); @@ -319,9 +312,6 @@ namespace opt { if (pri == symbol("pareto")) { is_sat = execute_pareto(); } - else if (pri == symbol("lns")) { - is_sat = execute_lns(); - } else if (pri == symbol("box")) { is_sat = execute_box(); } @@ -558,12 +548,8 @@ namespace opt { } void context::yield() { - if (m_pareto) { - m_pareto->get_model(m_model, m_labels); - } - else if (m_lns) { - m_lns->get_model(m_model, m_labels); - } + SASSERT (m_pareto); + m_pareto->get_model(m_model, m_labels); update_bound(true); update_bound(false); } @@ -582,19 +568,6 @@ namespace opt { return is_sat; } - lbool context::execute_lns() { - if (!m_lns) { - m_lns = alloc(lns, *this, m_solver.get()); - } - lbool is_sat = (*(m_lns.get()))(); - if (is_sat != l_true) { - m_lns = nullptr; - } - if (is_sat == l_true) { - yield(); - } - return l_undef; - } std::string context::reason_unknown() const { if (m.canceled()) { @@ -1041,23 +1014,6 @@ namespace opt { } } - /** - \brief retrieve literals used by the neighborhood search feature. - */ - - void context::get_lns_literals(expr_ref_vector& lits) { - for (objective & obj : m_objectives) { - switch(obj.m_type) { - case O_MAXSMT: - for (expr* f : obj.m_terms) { - lits.push_back(f); - } - break; - default: - break; - } - } - } void context::model_updated(model* md) { opt_params optp(m_params); @@ -1437,7 +1393,6 @@ namespace opt { void context::clear_state() { m_pareto = nullptr; - m_lns = nullptr; m_box_index = UINT_MAX; m_model.reset(); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index aa00cd1d3..20b0d1c71 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -27,7 +27,6 @@ Notes: #include "opt/opt_solver.h" #include "opt/opt_pareto.h" #include "opt/optsmt.h" -#include "opt/opt_lns.h" #include "opt/maxsmt.h" #include "cmd_context/cmd_context.h" @@ -148,7 +147,6 @@ namespace opt { ref m_solver; ref m_sat_solver; scoped_ptr m_pareto; - scoped_ptr m_lns; bool m_pareto1; scoped_ptr m_qmax; sref_vector m_box_models; @@ -271,8 +269,6 @@ namespace opt { void model_updated(model* mdl) override; - void get_lns_literals(expr_ref_vector& lits); - private: lbool execute(objective const& obj, bool committed, bool scoped); lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max); @@ -280,7 +276,6 @@ namespace opt { lbool execute_lex(); lbool execute_box(); lbool execute_pareto(); - lbool execute_lns(); lbool adjust_unknown(lbool r); bool scoped_lex(); bool contains_quantifiers() const; diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp deleted file mode 100644 index 0cdcf19c4..000000000 --- a/src/opt/opt_lns.cpp +++ /dev/null @@ -1,145 +0,0 @@ -/*++ -Copyright (c) 2018 Microsoft Corporation - -Module Name: - - opt_lns.cpp - -Abstract: - - Large neighborhood search default implementation - based on phase saving and assumptions - -Author: - - Nikolaj Bjorner (nbjorner) 2018-3-13 - ---*/ - -#include "ast/ast_pp.h" -#include "opt/opt_lns.h" -#include "opt/opt_context.h" - -namespace opt { - - lns::lns(context& ctx, solver* s): - m(ctx.get_manager()), - m_ctx(ctx), - m_solver(s), - m_models_trail(m), - m_atoms(m) - {} - - lns::~lns() {} - - void lns::display(std::ostream & out) const { - for (auto const& q : m_queue) { - expr_ref tmp(mk_and(q.m_assignment)); - out << q.m_index << ": " << tmp << "\n"; - } - } - - lbool lns::operator()() { - if (m_queue.empty()) { - expr_ref_vector lits(m), atoms(m); - m_ctx.get_lns_literals(lits); - for (expr* l : lits) { - expr* nl = nullptr; - if (m.is_not(l, nl)) { - m_atoms.push_back(nl); - } - else { - atoms.push_back(l); - m_atoms.push_back(l); - } - } - m_queue.push_back(queue_elem(atoms)); - m_qhead = 0; - } - - params_ref p; - p.set_uint("inprocess.max", 3ul); - m_solver->updt_params(p); - - while (m_qhead < m_queue.size()) { - obj_hashtable atoms; - for (expr* f : m_queue[m_qhead].m_assignment) { - atoms.insert(f); - } - unsigned& index = m_queue[m_qhead].m_index; - expr* lit = nullptr; - for (; index < m_atoms.size(); ++index) { - lit = m_atoms[index].get(); - if (!atoms.contains(lit) && !m_failed.contains(lit)) break; - } - if (index == m_atoms.size()) { - m_qhead++; - continue; - } - - IF_VERBOSE(2, verbose_stream() << "(opt.lns :queue " << m_qhead << " :index " << index << ")\n"); - - p.set_uint("local_search_threads", 0); - p.set_uint("unit_walk_threads", 0); - m_solver->updt_params(p); - - // recalibrate state to an initial satisfying assignment - lbool is_sat = m_solver->check_sat(m_queue[m_qhead].m_assignment); - IF_VERBOSE(2, verbose_stream() << "(opt.lns :calibrate-status " << is_sat << ")\n"); - if (!m.limit().inc()) { - return l_undef; - } - - expr_ref_vector lits(m); - lits.push_back(lit); - ++index; - - // freeze phase in both SAT solver and local search to current assignment - p.set_uint("inprocess.max", 5); - p.set_bool("phase.sticky", true); - p.set_uint("local_search_threads", 1); - p.set_uint("max_conflicts", 100000); - //p.set_uint("unit_walk_threads", 1); - m_solver->updt_params(p); - - is_sat = m_solver->check_sat(lits); - IF_VERBOSE(2, verbose_stream() << "(opt.lns :lookahead-status " << is_sat << " " << mk_pp(lit, m) << ")\n"); - if (is_sat == l_true && add_assignment()) { - return l_true; - } - if (is_sat == l_false) { - m_failed.insert(lit); - expr_ref nlit(m.mk_not(lit), m); - m_solver->assert_expr(nlit); - } - if (!m.limit().inc()) { - return l_undef; - } - } - return l_false; - } - - bool lns::add_assignment() { - model_ref mdl; - m_solver->get_model(mdl); - m_ctx.fix_model(mdl); - expr_ref tmp(m); - expr_ref_vector fmls(m); - for (expr* f : m_atoms) { - mdl->eval(f, tmp); - if (m.is_true(tmp)) { - fmls.push_back(f); - } - } - tmp = mk_and(fmls); - if (m_models.contains(tmp)) { - return false; - } - else { - m_models.insert(tmp); - m_models_trail.push_back(tmp); - return true; - } - } -} - diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h deleted file mode 100644 index 827df3081..000000000 --- a/src/opt/opt_lns.h +++ /dev/null @@ -1,68 +0,0 @@ -/*++ -Copyright (c) 2018 Microsoft Corporation - -Module Name: - - opt_lns.h - -Abstract: - - Large neighborhood seearch - -Author: - - Nikolaj Bjorner (nbjorner) 2018-3-13 - -Notes: - - ---*/ -#ifndef OPT_LNS_H_ -#define OPT_LNS_H_ - -#include "solver/solver.h" -#include "model/model.h" - -namespace opt { - - class context; - - class lns { - struct queue_elem { - expr_ref_vector m_assignment; - unsigned m_index; - queue_elem(expr_ref_vector& assign): - m_assignment(assign), - m_index(0) - {} - }; - ast_manager& m; - context& m_ctx; - ref m_solver; - model_ref m_model; - svector m_labels; - vector m_queue; - unsigned m_qhead; - expr_ref_vector m_models_trail; - expr_ref_vector m_atoms; - obj_hashtable m_models; - obj_hashtable m_failed; - - bool add_assignment(); - public: - lns(context& ctx, solver* s); - - ~lns(); - - void display(std::ostream & out) const; - - lbool operator()(); - - void get_model(model_ref& mdl, svector& labels) { - mdl = m_model; - labels = m_labels; - } - }; -} - -#endif diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 7a3c55dcc..f72bafbd8 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"), - ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box', or 'lns' (large neighborhood search)"), + ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 9cd047bf0..7ffb531be 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -110,31 +110,6 @@ namespace opt { lbool preferred_sat(expr_ref_vector const& asms, vector& cores) override; expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); } -#if 0 - virtual ~opt_solver(); - - virtual solver* translate(ast_manager& m, params_ref const& p); - virtual void updt_params(params_ref const& p); - virtual void collect_param_descrs(param_descrs & r); - virtual void collect_statistics(statistics & st) const; - virtual void assert_expr_core(expr * t); - virtual void assert_lemma(expr* t) {} - virtual void push_core(); - virtual void pop_core(unsigned n); - virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions); - virtual void get_unsat_core(ptr_vector & r); - virtual void get_model_core(model_ref & _m); - virtual proof * get_proof(); - virtual std::string reason_unknown() const; - virtual void set_reason_unknown(char const* msg); - virtual void get_labels(svector & r); - virtual void set_progress_callback(progress_callback * callback); - virtual unsigned get_num_assertions() const; - virtual expr * get_assertion(unsigned idx) const; - virtual ast_manager& get_manager() const { return m; } - virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); - virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); -#endif void set_logic(symbol const& logic); smt::theory_var add_objective(app* term); @@ -143,7 +118,7 @@ namespace opt { void maximize_objectives(expr_ref_vector& blockers); inf_eps const & saved_objective_value(unsigned obj_index); inf_eps current_objective_value(unsigned obj_index); - model* get_model(unsigned obj_index) { return m_models[obj_index]; } + model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; } bool objective_is_model_valid(unsigned obj_index) const { return m_valid_objectives[obj_index]; } diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 66174a28b..702702ef4 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -46,7 +46,7 @@ namespace opt { for (unsigned i = 0; i < src.size(); ++i) { if (src[i] >= dst[i]) { dst[i] = src[i]; - m_models.set(i, m_s->get_model(i)); + m_models.set(i, m_s->get_model_idx(i)); m_s->get_labels(m_labels); m_lower_fmls[i] = fmls[i].get(); if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already. diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index e73c2deab..8cc8560a1 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -85,6 +85,7 @@ goal::goal(goal const & src, bool): m_core_enabled(src.unsat_core_enabled()), m_inconsistent(false), m_precision(src.m_precision) { + add(src.mc()); } goal::~goal() { diff --git a/src/tactic/goal.h b/src/tactic/goal.h index 6977bb928..2d91bc67f 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -150,8 +150,8 @@ public: bool is_well_sorted() const; dependency_converter* dc() { return m_dc.get(); } - model_converter* mc() { return m_mc.get(); } - proof_converter* pc() { return inconsistent() ? proof2proof_converter(m(), pr(0)) : m_pc.get(); } + model_converter* mc() const { return m_mc.get(); } + proof_converter* pc() const { return inconsistent() ? proof2proof_converter(m(), pr(0)) : m_pc.get(); } void add(dependency_converter* d) { m_dc = dependency_converter::concat(m_dc.get(), d); } void add(model_converter* m) { m_mc = concat(m_mc.get(), m); } void add(proof_converter* p) { m_pc = concat(m_pc.get(), p); }