mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 06:03:23 +00:00
remove unused code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
fadcac8f6d
commit
c7063631e1
4 changed files with 0 additions and 346 deletions
|
|
@ -2,7 +2,6 @@ z3_add_component(opt
|
||||||
SOURCES
|
SOURCES
|
||||||
maxres.cpp
|
maxres.cpp
|
||||||
maxsmt.cpp
|
maxsmt.cpp
|
||||||
mss.cpp
|
|
||||||
opt_cmds.cpp
|
opt_cmds.cpp
|
||||||
opt_context.cpp
|
opt_context.cpp
|
||||||
opt_pareto.cpp
|
opt_pareto.cpp
|
||||||
|
|
|
||||||
|
|
@ -57,7 +57,6 @@ Notes:
|
||||||
#include "opt/maxres.h"
|
#include "opt/maxres.h"
|
||||||
#include "ast/ast_pp.h"
|
#include "ast/ast_pp.h"
|
||||||
#include "solver/mus.h"
|
#include "solver/mus.h"
|
||||||
#include "opt/mss.h"
|
|
||||||
#include "sat/sat_solver/inc_sat_solver.h"
|
#include "sat/sat_solver/inc_sat_solver.h"
|
||||||
#include "opt/opt_context.h"
|
#include "opt/opt_context.h"
|
||||||
#include "ast/pb_decl_plugin.h"
|
#include "ast/pb_decl_plugin.h"
|
||||||
|
|
@ -90,7 +89,6 @@ private:
|
||||||
obj_map<expr, rational> m_asm2weight;
|
obj_map<expr, rational> m_asm2weight;
|
||||||
ptr_vector<expr> m_new_core;
|
ptr_vector<expr> m_new_core;
|
||||||
mus m_mus;
|
mus m_mus;
|
||||||
mss m_mss;
|
|
||||||
expr_ref_vector m_trail;
|
expr_ref_vector m_trail;
|
||||||
strategy_t m_st;
|
strategy_t m_st;
|
||||||
rational m_max_upper;
|
rational m_max_upper;
|
||||||
|
|
@ -121,7 +119,6 @@ public:
|
||||||
m_index(index),
|
m_index(index),
|
||||||
m_B(m), m_asms(m), m_defs(m),
|
m_B(m), m_asms(m), m_defs(m),
|
||||||
m_mus(c.get_solver()),
|
m_mus(c.get_solver()),
|
||||||
m_mss(c.get_solver(), m),
|
|
||||||
m_trail(m),
|
m_trail(m),
|
||||||
m_st(st),
|
m_st(st),
|
||||||
m_correction_set_size(0),
|
m_correction_set_size(0),
|
||||||
|
|
|
||||||
285
src/opt/mss.cpp
285
src/opt/mss.cpp
|
|
@ -1,285 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2014 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
mss.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
MSS/MCS extraction.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2014-2-8
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#include "solver/solver.h"
|
|
||||||
#include "opt/mss.h"
|
|
||||||
#include "ast/ast_pp.h"
|
|
||||||
#include "model/model_smt2_pp.h"
|
|
||||||
|
|
||||||
namespace opt {
|
|
||||||
|
|
||||||
|
|
||||||
mss::mss(solver& s, ast_manager& m): m_s(s), m(m) {
|
|
||||||
}
|
|
||||||
|
|
||||||
mss::~mss() {
|
|
||||||
}
|
|
||||||
|
|
||||||
bool mss::check_result() {
|
|
||||||
lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
|
|
||||||
if (is_sat == l_undef) return true;
|
|
||||||
SASSERT(m_mss.empty() || is_sat == l_true);
|
|
||||||
if (is_sat == l_false) return false;
|
|
||||||
expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
m_mss.push_back(*it);
|
|
||||||
is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
|
|
||||||
m_mss.pop_back();
|
|
||||||
if (is_sat == l_undef) return true;
|
|
||||||
SASSERT(is_sat == l_false);
|
|
||||||
if (is_sat == l_true) return false;
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
void mss::initialize(exprs& literals) {
|
|
||||||
expr* n;
|
|
||||||
expr_set lits, core_lits;
|
|
||||||
for (unsigned i = 0; i < literals.size(); ++i) {
|
|
||||||
n = literals[i];
|
|
||||||
lits.insert(n);
|
|
||||||
m.is_not(n, n);
|
|
||||||
if (!is_uninterp_const(n)) {
|
|
||||||
throw default_exception("arguments have to be uninterpreted literals");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
exprs rest_core;
|
|
||||||
expr_ref tmp(m);
|
|
||||||
//
|
|
||||||
// the last core is a dummy core. It contains literals that
|
|
||||||
// did not occur in previous cores and did not evaluate to true
|
|
||||||
// in the current model.
|
|
||||||
//
|
|
||||||
for (unsigned i = 0; i < m_cores.size(); ++i) {
|
|
||||||
exprs const& core = m_cores[i];
|
|
||||||
for (unsigned j = 0; j < core.size(); ++j) {
|
|
||||||
expr* n = core[j];
|
|
||||||
if (!core_lits.contains(n)) {
|
|
||||||
core_lits.insert(n);
|
|
||||||
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
|
|
||||||
add_mss(n);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_todo.push_back(n);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < literals.size(); ++i) {
|
|
||||||
expr* n = literals[i];
|
|
||||||
if (!core_lits.contains(n)) {
|
|
||||||
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
|
|
||||||
m_mss.push_back(n);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
rest_core.push_back(n);
|
|
||||||
core_lits.insert(n);
|
|
||||||
m_todo.push_back(n);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
m_cores.push_back(rest_core);
|
|
||||||
}
|
|
||||||
|
|
||||||
void mss::add_mss(expr* n) {
|
|
||||||
if (!m_mss_set.contains(n)) {
|
|
||||||
m_mss_set.insert(n);
|
|
||||||
m_mss.push_back(n);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void mss::update_core(exprs& core) {
|
|
||||||
unsigned j = 0;
|
|
||||||
for (unsigned i = 0; i < core.size(); ++i) {
|
|
||||||
expr* n = core[i];
|
|
||||||
if (!m_mss_set.contains(n)) {
|
|
||||||
if (i != j) {
|
|
||||||
core[j] = core[i];
|
|
||||||
}
|
|
||||||
++j;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
core.resize(j);
|
|
||||||
}
|
|
||||||
|
|
||||||
void mss::update_mss() {
|
|
||||||
expr_ref tmp(m);
|
|
||||||
unsigned j = 0;
|
|
||||||
for (unsigned i = 0; i < m_todo.size(); ++i) {
|
|
||||||
expr* n = m_todo[i];
|
|
||||||
SASSERT(!m_mss_set.contains(n));
|
|
||||||
if (m_mcs.contains(n)) {
|
|
||||||
continue; // remove from cores.
|
|
||||||
}
|
|
||||||
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
|
|
||||||
add_mss(n);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
if (j != i) {
|
|
||||||
m_todo[j] = m_todo[i];
|
|
||||||
}
|
|
||||||
++j;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
m_todo.resize(j);
|
|
||||||
}
|
|
||||||
|
|
||||||
lbool mss::operator()(model* initial_model, vector<exprs> const& _cores, exprs& literals, exprs& mcs) {
|
|
||||||
m_mss.reset();
|
|
||||||
m_todo.reset();
|
|
||||||
m_model = initial_model;
|
|
||||||
m_cores.reset();
|
|
||||||
SASSERT(m_model);
|
|
||||||
m_cores.append(_cores);
|
|
||||||
initialize(literals);
|
|
||||||
TRACE("opt",
|
|
||||||
display_vec(tout << "lits: ", literals.size(), literals.c_ptr());
|
|
||||||
display(tout););
|
|
||||||
lbool is_sat = l_true;
|
|
||||||
for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) {
|
|
||||||
bool has_mcs = false;
|
|
||||||
bool is_last = i + 1 < m_cores.size();
|
|
||||||
SASSERT(check_invariant());
|
|
||||||
update_core(m_cores[i]); // remove members of mss
|
|
||||||
is_sat = process_core(1, m_cores[i], has_mcs, is_last);
|
|
||||||
}
|
|
||||||
if (is_sat == l_true) {
|
|
||||||
SASSERT(check_invariant());
|
|
||||||
TRACE("opt", display(tout););
|
|
||||||
literals.reset();
|
|
||||||
literals.append(m_mss);
|
|
||||||
mcs.reset();
|
|
||||||
expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
mcs.push_back(*it);
|
|
||||||
}
|
|
||||||
SASSERT(check_result());
|
|
||||||
}
|
|
||||||
m_mcs.reset();
|
|
||||||
m_mss_set.reset();
|
|
||||||
IF_VERBOSE(2, display_vec(verbose_stream() << "mcs: ", mcs.size(), mcs.c_ptr()););
|
|
||||||
return is_sat;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
//
|
|
||||||
// at least one literal in core is false in current model.
|
|
||||||
// pick literals in core that are not yet in mss.
|
|
||||||
//
|
|
||||||
lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) {
|
|
||||||
SASSERT(sz > 0);
|
|
||||||
if (core.empty()) {
|
|
||||||
return l_true;
|
|
||||||
}
|
|
||||||
if (m.canceled()) {
|
|
||||||
return l_undef;
|
|
||||||
}
|
|
||||||
if (sz == 1 && core.size() == 1 && is_last && !has_mcs) {
|
|
||||||
// there has to be at least one false
|
|
||||||
// literal in the core.
|
|
||||||
TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";);
|
|
||||||
m_mcs.insert(core[0]);
|
|
||||||
return l_true;
|
|
||||||
}
|
|
||||||
sz = std::min(sz, core.size());
|
|
||||||
TRACE("opt", display_vec(tout << "process (total " << core.size() << ") :", sz, core.c_ptr()););
|
|
||||||
unsigned sz_save = m_mss.size();
|
|
||||||
m_mss.append(sz, core.c_ptr());
|
|
||||||
lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
|
|
||||||
IF_VERBOSE(3, display_vec(verbose_stream() << "mss: ", m_mss.size(), m_mss.c_ptr()););
|
|
||||||
m_mss.resize(sz_save);
|
|
||||||
switch (is_sat) {
|
|
||||||
case l_true:
|
|
||||||
m_s.get_model(m_model);
|
|
||||||
update_mss();
|
|
||||||
DEBUG_CODE(
|
|
||||||
for (unsigned i = 0; i < sz; ++i) {
|
|
||||||
SASSERT(m_mss_set.contains(core[i]));
|
|
||||||
});
|
|
||||||
update_core(core);
|
|
||||||
return process_core(2*sz, core, has_mcs, is_last);
|
|
||||||
case l_false:
|
|
||||||
if (sz == 1) {
|
|
||||||
has_mcs = true;
|
|
||||||
m_mcs.insert(core[0]);
|
|
||||||
core[0] = core.back();
|
|
||||||
core.pop_back();
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
exprs core2;
|
|
||||||
core2.append(core.size()-sz, core.c_ptr()+sz);
|
|
||||||
core.resize(sz);
|
|
||||||
is_sat = process_core(sz, core2, has_mcs, false);
|
|
||||||
if (is_sat != l_true) {
|
|
||||||
return is_sat;
|
|
||||||
}
|
|
||||||
update_core(core);
|
|
||||||
}
|
|
||||||
return process_core(1, core, has_mcs, is_last);
|
|
||||||
case l_undef:
|
|
||||||
return l_undef;
|
|
||||||
}
|
|
||||||
|
|
||||||
return l_true;
|
|
||||||
}
|
|
||||||
|
|
||||||
void mss::display_vec(std::ostream& out, unsigned sz, expr* const* args) const {
|
|
||||||
for (unsigned i = 0; i < sz; ++i) {
|
|
||||||
out << mk_pp(args[i], m) << " ";
|
|
||||||
}
|
|
||||||
out << "\n";
|
|
||||||
}
|
|
||||||
|
|
||||||
void mss::display(std::ostream& out) const {
|
|
||||||
for (unsigned i = 0; i < m_cores.size(); ++i) {
|
|
||||||
display_vec(out << "core: ", m_cores[i].size(), m_cores[i].c_ptr());
|
|
||||||
}
|
|
||||||
expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
|
|
||||||
out << "mcs:\n";
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
out << mk_pp(*it, m) << "\n";
|
|
||||||
}
|
|
||||||
out << "\n";
|
|
||||||
out << "mss:\n";
|
|
||||||
for (unsigned i = 0; i < m_mss.size(); ++i) {
|
|
||||||
out << mk_pp(m_mss[i], m) << "\n";
|
|
||||||
}
|
|
||||||
out << "\n";
|
|
||||||
if (m_model) {
|
|
||||||
model_smt2_pp(out, m, *(m_model.get()), 0);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
bool mss::check_invariant() const {
|
|
||||||
if (!m_model) return true;
|
|
||||||
expr_ref tmp(m);
|
|
||||||
for (unsigned i = 0; i < m_mss.size(); ++i) {
|
|
||||||
expr* n = m_mss[i];
|
|
||||||
if (!m_model->eval(n, tmp)) return true;
|
|
||||||
CTRACE("opt", !m.is_true(tmp), tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
|
|
||||||
SASSERT(!m.is_false(tmp));
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -1,57 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2014 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
mss.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Maximal satisfying subset/minimal correction sets: MSS/MCS
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2014-2-8
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#ifndef MSS_H_
|
|
||||||
#define MSS_H_
|
|
||||||
|
|
||||||
namespace opt {
|
|
||||||
class mss {
|
|
||||||
solver& m_s;
|
|
||||||
ast_manager& m;
|
|
||||||
typedef ptr_vector<expr> exprs;
|
|
||||||
typedef obj_hashtable<expr> expr_set;
|
|
||||||
exprs m_mss;
|
|
||||||
expr_set m_mcs;
|
|
||||||
expr_set m_mss_set;
|
|
||||||
vector<exprs> m_cores;
|
|
||||||
exprs m_todo;
|
|
||||||
model_ref m_model;
|
|
||||||
public:
|
|
||||||
mss(solver& s, ast_manager& m);
|
|
||||||
~mss();
|
|
||||||
|
|
||||||
lbool operator()(model* initial_model, vector<exprs> const& cores, exprs& literals, exprs& mcs);
|
|
||||||
|
|
||||||
|
|
||||||
void get_model(model_ref& mdl) { mdl = m_model; }
|
|
||||||
|
|
||||||
private:
|
|
||||||
void initialize(exprs& literals);
|
|
||||||
bool check_result();
|
|
||||||
void add_mss(expr* n);
|
|
||||||
void update_mss();
|
|
||||||
void update_core(exprs& core);
|
|
||||||
lbool process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last);
|
|
||||||
void display(std::ostream& out) const;
|
|
||||||
void display_vec(std::ostream& out, unsigned sz, expr* const* args) const;
|
|
||||||
bool check_invariant() const;
|
|
||||||
};
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
#endif
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue