mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

remove lns code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-25 18:32:16 -07:00
parent a79400a01b
commit c4ff5c7ac7
6 changed files with 3 additions and 266 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/opt/opt_context.cpp
View file

@ -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();
}