mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

make max-smt solvers generic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-08 18:22:07 -08:00
parent 9f53a4aa18
commit c6c7093a4c
4 changed files with 188 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

102
src/opt/fu_malik.cpp
View file

@ -35,19 +35,20 @@ Notes:
*/
namespace opt {
class fu_malik {
struct fu_malik::imp {
ast_manager& m;
solver& s;
expr_ref_vector m_soft;
expr_ref_vector m_aux;
expr_ref_vector m_assignment;
public:
fu_malik(ast_manager& m, solver& s, expr_ref_vector const& soft):
imp(ast_manager& m, solver& s, expr_ref_vector const& soft):
m(m),
s(s),
m_soft(soft),
m_aux(m)
m_aux(m),
m_assignment(m)
{
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
@ -106,8 +107,6 @@ namespace opt {
return l_false;
}
private:
void assert_at_most_one(expr_ref_vector const& block_vars) {
expr_ref has_one(m), has_zero(m), at_most_one(m);
mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, has_zero);
@ -131,46 +130,71 @@ namespace opt {
}
}
};
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints) {
ast_manager& m = soft_constraints.get_manager();
lbool is_sat = s.check_sat(0,0);
if (!soft_constraints.empty() && is_sat == l_true) {
s.push();
fu_malik fm(m, s, soft_constraints);
lbool is_sat = l_true;
do {
is_sat = fm.step();
}
while (is_sat == l_false);
if (is_sat == l_true) {
// Get a list of satisfying soft_constraints
model_ref model;
s.get_model(model);
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
lbool operator()() {
lbool is_sat = s.check_sat(0,0);
if (!m_soft.empty() && is_sat == l_true) {
opt_solver::scoped_push _sp(s);
expr_ref_vector result(m);
for (unsigned i = 0; i < soft_constraints.size(); ++i) {
expr_ref val(m);
VERIFY(model->eval(soft_constraints[i].get(), val));
if (!m.is_false(val)) {
result.push_back(soft_constraints[i].get());
lbool is_sat = l_true;
do {
is_sat = step();
}
while (is_sat == l_false);
if (is_sat == l_true) {
// Get a list of satisfying m_soft
model_ref model;
s.get_model(model);
m_assignment.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr_ref val(m);
VERIFY(model->eval(m_soft[i].get(), val));
if (m.is_true(val)) {
m_assignment.push_back(m_soft[i].get());
}
}
}
soft_constraints.reset();
soft_constraints.append(result);
}
s.pop(1);
// We are done and soft_constraints has
// been updated with the max-sat assignment.
return is_sat;
}
// We are done and soft_constraints has
// been updated with the max-sat assignment.
return is_sat;
};
fu_malik::fu_malik(ast_manager& m, solver& s, expr_ref_vector& soft_constraints) {
m_imp = alloc(imp, m, s, soft_constraints);
}
fu_malik::~fu_malik() {
dealloc(m_imp);
}
lbool fu_malik::operator()() {
return (*m_imp)();
}
rational fu_malik::get_lower() const {
NOT_IMPLEMENTED_YET();
return rational(0);
}
rational fu_malik::get_upper() const {
NOT_IMPLEMENTED_YET();
return rational(m_imp->m_soft.size());
}
rational fu_malik::get_value() const {
NOT_IMPLEMENTED_YET();
return rational(m_imp->m_assignment.size());
}
expr_ref_vector fu_malik::get_assignment() const {
return m_imp->m_assignment;
}
void fu_malik::set_cancel(bool f) {
// no-op
}
};

16
src/opt/fu_malik.h
View file

@ -20,6 +20,7 @@ Notes:
#define _OPT_FU_MALIK_H_
#include "solver.h"
#include "maxsmt.h"
namespace opt {
/**
@ -27,8 +28,21 @@ namespace opt {
Returns a maximal satisfying subset of soft_constraints
that are still consistent with the solver state.
*/
class fu_malik : public maxsmt_solver {
struct imp;
imp* m_imp;
public:
fu_malik(ast_manager& m, solver& s, expr_ref_vector& soft_constraints);
virtual ~fu_malik();
virtual lbool operator()();
virtual rational get_lower() const;
virtual rational get_upper() const;
virtual rational get_value() const;
virtual expr_ref_vector get_assignment() const;
virtual void set_cancel(bool f);
};
lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints);
};
#endif

127
src/opt/weighted_maxsat.cpp
View file

@ -151,11 +151,9 @@ namespace smt {
virtual final_check_status final_check_eh() {
if (block(true)) {
return FC_CONTINUE;
}
else {
return FC_DONE;
}
return FC_CONTINUE;
}
virtual bool use_diseqs() const {
@ -203,6 +201,9 @@ namespace smt {
};
bool block(bool is_final) {
if (m_vars.empty()) {
return true;
}
ast_manager& m = get_manager();
context& ctx = get_context();
literal_vector lits;
@ -218,6 +219,11 @@ namespace smt {
lits.push_back(~literal(m_min_cost_bv));
}
IF_VERBOSE(2, verbose_stream() << "block: " << m_costs.size() << " " << lits.size() << " " << m_min_cost << "\n";);
IF_VERBOSE(2, for (unsigned i = 0; i < lits.size(); ++i) {
verbose_stream() << lits[i] << " ";
}
verbose_stream() << "\n";
);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
if (is_final && m_cost < m_min_cost) {
@ -225,7 +231,7 @@ namespace smt {
m_cost_save.reset();
m_cost_save.append(m_costs);
}
return !lits.empty();
return false;
}
};
@ -259,42 +265,101 @@ namespace opt {
return result;
}
struct wmaxsmt::imp {
ast_manager& m;
opt_solver& s;
expr_ref_vector m_soft;
expr_ref_vector m_assignment;
rational m_lower;
rational m_upper;
rational m_value;
vector<rational> m_weights;
imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights):
m(m), s(s), m_soft(soft_constraints), m_assignment(m), m_weights(weights)
{}
~imp() {}
smt::theory_weighted_maxsat& ensure_theory() {
smt::context& ctx = s.get_context();
smt::theory_id th_id = m.get_family_id("weighted_maxsat");
smt::theory* th = ctx.get_theory(th_id);
smt::theory_weighted_maxsat* wth;
if (th) {
wth = dynamic_cast<smt::theory_weighted_maxsat*>(th);
wth->reset();
}
else {
wth = alloc(smt::theory_weighted_maxsat, m);
ctx.register_plugin(wth);
}
return *wth;
}
/**
Takes solver with hard constraints added.
Returns a maximal satisfying subset of weighted soft_constraints
that are still consistent with the solver state.
*/
lbool weighted_maxsat(opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
ast_manager& m = soft_constraints.get_manager();
smt::context& ctx = s.get_context();
smt::theory_id th_id = m.get_family_id("weighted_maxsat");
smt::theory* th = ctx.get_theory(th_id);
smt::theory_weighted_maxsat* wth;
if (th) {
wth = dynamic_cast<smt::theory_weighted_maxsat*>(th);
wth->reset();
}
else {
wth = alloc(smt::theory_weighted_maxsat, m);
ctx.register_plugin(wth);
}
opt_solver::scoped_push _s(s);
for (unsigned i = 0; i < soft_constraints.size(); ++i) {
wth->assert_weighted(soft_constraints[i].get(), weights[i]);
}
#if 0
lbool result = s.check_sat_core(0,0);
lbool operator()() {
smt::theory_weighted_maxsat& wth = ensure_theory();
lbool result;
{
opt_solver::scoped_push _s(s);
for (unsigned i = 0; i < m_soft.size(); ++i) {
wth.assert_weighted(m_soft[i].get(), m_weights[i]);
}
#if 1
result = s.check_sat_core(0,0);
#else
lbool result = iterative_weighted_maxsat(s, *wth);
result = iterative_weighted_maxsat(s, *wth);
#endif
wth.get_assignment(m_assignment);
if (!m_assignment.empty() && result == l_false) {
result = l_true;
}
}
wth.reset();
return result;
}
};
wth->get_assignment(soft_constraints);
if (!soft_constraints.empty() && result == l_false) {
result = l_true;
}
return result;
wmaxsmt::wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
m_imp = alloc(imp, m, s, soft_constraints, weights);
}
wmaxsmt::~wmaxsmt() {
dealloc(m_imp);
}
lbool wmaxsmt::operator()() {
return (*m_imp)();
}
rational wmaxsmt::get_lower() const {
NOT_IMPLEMENTED_YET();
return m_imp->m_lower;
}
rational wmaxsmt::get_upper() const {
NOT_IMPLEMENTED_YET();
return m_imp->m_upper;
}
rational wmaxsmt::get_value() const {
NOT_IMPLEMENTED_YET();
return m_imp->m_value;
}
expr_ref_vector wmaxsmt::get_assignment() const {
return m_imp->m_assignment;
}
void wmaxsmt::set_cancel(bool f) {
// no-op
}
};

16
src/opt/weighted_maxsat.h
View file

@ -19,6 +19,7 @@ Notes:
#define _OPT_WEIGHTED_MAX_SAT_H_
#include "opt_solver.h"
#include "maxsmt.h"
namespace opt {
/**
@ -26,8 +27,19 @@ namespace opt {
Returns a maximal satisfying subset of weighted soft_constraints
that are still consistent with the solver state.
*/
lbool weighted_maxsat(opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights);
class wmaxsmt : public maxsmt_solver {
struct imp;
imp* m_imp;
public:
wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights);
~wmaxsmt();
virtual lbool operator()();
virtual rational get_lower() const;
virtual rational get_upper() const;
virtual rational get_value() const;
virtual expr_ref_vector get_assignment() const;
virtual void set_cancel(bool f);
};
};
#endif