From c4ff5c7ac7b6f3542242a1533a6f52b5c2e1fa23 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 25 Mar 2018 18:32:16 -0700
Subject: [PATCH] remove lns code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/CMakeLists.txt | 1 -
src/opt/opt_context.cpp | 48 +------------
src/opt/opt_context.h | 5 --
src/opt/opt_lns.cpp | 145 ----------------------------------------
src/opt/opt_lns.h | 68 -------------------
src/opt/opt_params.pyg | 2 +-
6 files changed, 3 insertions(+), 266 deletions(-)
delete mode 100644 src/opt/opt_lns.cpp
delete mode 100644 src/opt/opt_lns.h
diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt
index 3f1d8253c..28a14be2e 100644
--- a/src/opt/CMakeLists.txt
+++ b/src/opt/CMakeLists.txt
@@ -5,7 +5,6 @@ z3_add_component(opt
mss.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 33aaa0b27..0793e5c53 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -254,9 +254,6 @@ namespace opt {
if (m_pareto) {
return execute_pareto();
}
- if (m_lns) {
- return execute_lns();
- }
if (m_box_index != UINT_MAX) {
return execute_box();
}
@@ -276,9 +273,6 @@ namespace opt {
opt_params optp(m_params);
symbol pri = optp.priority();
- if (pri == symbol("lns")) {
- return execute_lns();
- }
IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n");
lbool is_sat = s.check_sat(0,0);
@@ -311,9 +305,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();
}
@@ -536,12 +527,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);
}
@@ -560,19 +547,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()) {
@@ -1020,23 +994,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;
- }
- }
- }
bool context::verify_model(unsigned index, model* md, rational const& _v) {
rational r;
@@ -1401,7 +1358,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 9f55d5ca1..abc6268dd 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"
@@ -147,7 +146,6 @@ namespace opt {
ref<solver> m_solver;
ref<solver> m_sat_solver;
scoped_ptr<pareto_base> m_pareto;
- scoped_ptr<lns> m_lns;
scoped_ptr<qe::qmax> m_qmax;
sref_vector<model> m_box_models;
unsigned m_box_index;
@@ -234,8 +232,6 @@ namespace opt {
virtual bool verify_model(unsigned id, model* mdl, rational const& v);
- 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);
@@ -243,7 +239,6 @@ namespace opt {
lbool execute_lex();
lbool execute_box();
lbool execute_pareto();
- lbool execute_lns();
lbool adjust_unknown(lbool r);
bool scoped_lex();
expr_ref to_expr(inf_eps const& n);
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<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;
- }
- }
-}
-
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<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
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 21845d38a..911b0a694 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'),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),