mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
remove lns
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
commit
a81a8de975
|
@ -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();
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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();
|
||||
}
|
||||
|
|
|
@ -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<solver> m_solver;
|
||||
ref<solver> m_sat_solver;
|
||||
scoped_ptr<pareto_base> m_pareto;
|
||||
scoped_ptr<lns> m_lns;
|
||||
bool m_pareto1;
|
||||
scoped_ptr<qe::qmax> m_qmax;
|
||||
sref_vector<model> 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;
|
||||
|
|
|
@ -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<expr> 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;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -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<solver> m_solver;
|
||||
model_ref m_model;
|
||||
svector<symbol> m_labels;
|
||||
vector<queue_elem> m_queue;
|
||||
unsigned m_qhead;
|
||||
expr_ref_vector m_models_trail;
|
||||
expr_ref_vector m_atoms;
|
||||
obj_hashtable<expr> m_models;
|
||||
obj_hashtable<expr> 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<symbol>& labels) {
|
||||
mdl = m_model;
|
||||
labels = m_labels;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
|
@ -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)'),
|
||||
|
|
|
@ -110,31 +110,6 @@ namespace opt {
|
|||
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_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<expr> & 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<symbol> & 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<expr_ref_vector>& mutexes);
|
||||
virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_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];
|
||||
}
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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() {
|
||||
|
|
|
@ -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); }
|
||||
|
|
Loading…
Reference in a new issue