mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix lexicographic product for MaxSMT

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-01 13:49:23 -07:00
parent 0914748184
commit 0b1c180808
10 changed files with 96 additions and 130 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/opt/bcd2.cpp
View file

@ -187,7 +187,7 @@ namespace opt {
expr_ref fml(m);
expr* r = m_soft_aux[i].get();
m_soft2index.insert(r, i);
fml = m.mk_or(r, m_soft[i].get());
fml = m.mk_or(r, m_soft[i]);
m_soft_constraints.push_back(fml);
m_asm_set.insert(r);
SASSERT(m_weights[i].is_int());
@ -233,7 +233,7 @@ namespace opt {
new_assignment.reset();
s().get_model(model);
for (unsigned i = 0; i < m_soft.size(); ++i) {
VERIFY(model->eval(m_soft[i].get(), val));
VERIFY(model->eval(m_soft[i], val));
new_assignment.push_back(m.is_true(val));
if (!new_assignment[i]) {
new_upper += m_weights[i];
@ -393,7 +393,7 @@ namespace opt {
out << "[" << c.m_lower << ":" << c.m_mid << ":" << c.m_upper << "]\n";
}
for (unsigned i = 0; i < m_soft.size(); ++i) {
out << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n";
out << mk_pp(m_soft[i], m) << " " << m_weights[i] << "\n";
}
}
};

104
src/opt/fu_malik.cpp
View file

@ -43,34 +43,24 @@ Notes:
*/
namespace opt {
struct fu_malik::imp {
ast_manager& m;
solver& m_s;
class fu_malik : public maxsmt_solver_base {
filter_model_converter& m_fm;
expr_ref_vector m_soft;
expr_ref_vector m_orig_soft;
expr_ref_vector m_aux_soft;
expr_ref_vector m_aux;
svector<bool> m_assignment;
unsigned m_upper;
unsigned m_lower;
model_ref m_model;
imp(context& c, expr_ref_vector const& soft):
m(c.get_manager()),
m_s(c.get_solver()),
public:
fu_malik(context& c, weights_t& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft),
m_fm(c.fm()),
m_soft(soft),
m_orig_soft(soft),
m_aux(m),
m_upper(0),
m_lower(0)
m_aux_soft(soft),
m_aux(m)
{
m_upper = m_soft.size() + 1;
m_assignment.resize(m_soft.size(), false);
m_upper = rational(m_aux_soft.size() + 1);
m_lower.reset();
m_assignment.resize(m_aux_soft.size(), false);
}
solver& s() { return m_s; }
/**
\brief One step of the Fu&Malik algorithm.
@ -96,9 +86,8 @@ namespace opt {
}
}
void collect_statistics(statistics& st) const {
st.update("opt-fm-num-steps", m_soft.size() + 2 - m_upper);
st.update("opt-fm-num-steps", m_aux_soft.size() + 2 - m_upper.get_unsigned());
}
void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const {
@ -115,9 +104,9 @@ namespace opt {
}
lbool step() {
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper << ")\n";);
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_aux_soft.size() + 2 - m_upper.get_unsigned() << ")\n";);
expr_ref_vector assumptions(m), block_vars(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
assumptions.push_back(m.mk_not(m_aux[i].get()));
}
lbool is_sat = s().check_sat(assumptions.size(), assumptions.c_ptr());
@ -131,7 +120,7 @@ namespace opt {
SASSERT(!core.empty());
// Update soft-constraints and aux_vars
for (unsigned i = 0; i < m_soft.size(); ++i) {
for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
bool found = false;
for (unsigned j = 0; !found && j < core.size(); ++j) {
@ -145,14 +134,14 @@ namespace opt {
m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort());
m_fm.insert(block_var->get_decl());
m_fm.insert(to_app(m_aux[i].get())->get_decl());
m_soft[i] = m.mk_or(m_soft[i].get(), block_var);
m_aux_soft[i] = m.mk_or(m_aux_soft[i].get(), block_var);
block_vars.push_back(block_var);
tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
tmp = m.mk_or(m_aux_soft[i].get(), m_aux[i].get());
s().assert_expr(tmp);
}
SASSERT (!block_vars.empty());
assert_at_most_one(block_vars);
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_soft.size() - block_vars.size() << ")\n";);
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_aux_soft.size() - block_vars.size() << ")\n";);
return l_false;
}
@ -181,9 +170,9 @@ namespace opt {
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
lbool operator()() {
virtual lbool operator()() {
lbool is_sat = l_true;
if (m_soft.empty()) {
if (m_aux_soft.empty()) {
return is_sat;
}
solver::scoped_push _sp(s());
@ -191,14 +180,14 @@ namespace opt {
TRACE("opt",
tout << "soft constraints:\n";
for (unsigned i = 0; i < m_soft.size(); ++i) {
tout << mk_pp(m_soft[i].get(), m) << "\n";
for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
tout << mk_pp(m_aux_soft[i].get(), m) << "\n";
});
for (unsigned i = 0; i < m_soft.size(); ++i) {
for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
m_fm.insert(to_app(m_aux.back())->get_decl());
tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
tmp = m.mk_or(m_aux_soft[i].get(), m_aux[i].get());
s().assert_expr(tmp);
}
@ -209,13 +198,13 @@ namespace opt {
while (is_sat == l_false);
if (is_sat == l_true) {
// Get a list satisfying m_soft
// Get a list satisfying m_aux_soft
s().get_model(m_model);
m_lower = m_upper;
m_assignment.reset();
for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_orig_soft[i].get(), val));
VERIFY(m_model->eval(m_soft[i], val));
TRACE("opt", tout << val << "\n";);
m_assignment.push_back(m.is_true(val));
}
@ -227,43 +216,22 @@ namespace opt {
return is_sat;
}
void get_model(model_ref& mdl) {
virtual void get_model(model_ref& mdl) {
mdl = m_model.get();
}
virtual rational get_lower() const {
return rational(m_aux_soft.size())-m_upper;
}
virtual rational get_upper() const {
return rational(m_aux_soft.size())-m_lower;
}
};
fu_malik::fu_malik(context& c, expr_ref_vector& soft_constraints) {
m_imp = alloc(imp, c, soft_constraints);
}
fu_malik::~fu_malik() {
dealloc(m_imp);
}
lbool fu_malik::operator()() {
return (*m_imp)();
}
rational fu_malik::get_lower() const {
return rational(m_imp->m_soft.size()-m_imp->m_upper);
}
rational fu_malik::get_upper() const {
return rational(m_imp->m_soft.size()-m_imp->m_lower);
}
bool fu_malik::get_assignment(unsigned idx) const {
return m_imp->m_assignment[idx];
}
void fu_malik::set_cancel(bool f) {
// no-op
}
void fu_malik::collect_statistics(statistics& st) const {
m_imp->collect_statistics(st);
}
void fu_malik::get_model(model_ref& m) {
m_imp->get_model(m);
maxsmt_solver_base* mk_fu_malik(context& c, weights_t & ws, expr_ref_vector const& soft) {
return alloc(fu_malik, c, ws, soft);
}
void fu_malik::updt_params(params_ref& p) {
// no-op
}
};

17
src/opt/fu_malik.h
View file

@ -29,21 +29,8 @@ Notes:
namespace opt {
class fu_malik : public maxsmt_solver {
struct imp;
imp* m_imp;
public:
fu_malik(context& c, expr_ref_vector& soft_constraints);
virtual ~fu_malik();
virtual lbool operator()();
virtual rational get_lower() const;
virtual rational get_upper() const;
virtual bool get_assignment(unsigned idx) const;
virtual void set_cancel(bool f);
virtual void collect_statistics(statistics& st) const;
virtual void get_model(model_ref& m);
virtual void updt_params(params_ref& p);
};
maxsmt_solver_base* mk_fu_malik(context& c, weights_t & ws, expr_ref_vector const& soft);
};

8
src/opt/maxhs.cpp
View file

@ -162,7 +162,7 @@ namespace opt {
m_aux2index.reset();
m_core_activity.reset();
for (unsigned i = 0; i < sz; ++i) {
bool tt = is_true(m_model, m_soft[i].get());
bool tt = is_true(m_model, m_soft[i]);
m_seed.push_back(tt);
m_aux. push_back(mk_fresh(m.mk_bool_sort()));
m_aux_active.push_back(false);
@ -380,7 +380,7 @@ namespace opt {
if (m_seed[i]) {
// already an assumption
}
else if (is_true(mdl, m_soft[i].get())) {
else if (is_true(mdl, m_soft[i])) {
m_seed[i] = true;
m_asms.push_back(m_aux[i].get());
}
@ -420,7 +420,7 @@ namespace opt {
}
DEBUG_CODE(
for (unsigned i = 0; i < num_soft(); ++i) {
SASSERT(is_true(mdl, m_soft[i].get()) == m_seed[i]);
SASSERT(is_true(mdl, m_soft[i]) == m_seed[i]);
});
return true;
@ -545,7 +545,7 @@ namespace opt {
void ensure_active(unsigned i) {
if (!is_active(i)) {
expr_ref fml(m);
fml = m.mk_implies(m_aux[i].get(), m_soft[i].get());
fml = m.mk_implies(m_aux[i].get(), m_soft[i]);
s().assert_expr(fml);
m_aux_active[i] = true;
}

32
src/opt/maxres.cpp
View file

@ -84,6 +84,7 @@ private:
expr_ref_vector m_trail;
strategy_t m_st;
rational m_max_upper;
bool m_found_feasible_optimum;
bool m_hill_climb; // prefer large weight soft clauses for cores
bool m_add_upper_bound_block; // restrict upper bound with constraint
unsigned m_max_num_cores; // max number of cores per round.
@ -105,6 +106,7 @@ public:
m_mss(c.get_solver(), m),
m_trail(m),
m_st(st),
m_found_feasible_optimum(false),
m_hill_climb(true),
m_add_upper_bound_block(false),
m_max_num_cores(UINT_MAX),
@ -122,6 +124,8 @@ public:
(m.is_not(l, l) && is_uninterp_const(l));
}
void add_soft(expr* e, rational const& w) {
TRACE("opt", tout << mk_pp(e, m) << "\n";);
expr_ref asum(m), fml(m);
@ -372,13 +376,14 @@ public:
SASSERT(is_true(m_asms[i].get()));
});
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_assignment[i] = is_true(m_soft[i].get());
m_assignment[i] = is_true(m_soft[i]);
}
m_upper = m_lower;
m_found_feasible_optimum = true;
}
lbool operator()() {
virtual lbool operator()() {
switch(m_st) {
case s_mus:
return mus_solver();
@ -781,7 +786,7 @@ public:
rational upper(0);
expr_ref tmp(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr* n = m_soft[i].get();
expr* n = m_soft[i];
VERIFY(mdl->eval(n, tmp));
if (!m.is_true(tmp)) {
upper += m_weights[i];
@ -796,7 +801,7 @@ public:
m_model = mdl;
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_assignment[i] = is_true(m_soft[i].get());
m_assignment[i] = is_true(m_soft[i]);
}
m_upper = upper;
// verify_assignment();
@ -811,7 +816,7 @@ public:
expr_ref_vector nsoft(m);
expr_ref fml(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
nsoft.push_back(mk_not(m, m_soft[i].get()));
nsoft.push_back(mk_not(m, m_soft[i]));
}
fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
s().assert_expr(fml);
@ -864,12 +869,25 @@ public:
m_lower.reset();
m_trail.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
add_soft(m_soft[i].get(), m_weights[i]);
add_soft(m_soft[i], m_weights[i]);
}
m_max_upper = m_upper;
m_found_feasible_optimum = false;
add_upper_bound_block();
}
virtual void commit_assignment() {
if (m_found_feasible_optimum) {
TRACE("opt", tout << "Committing feasible solution\n";);
for (unsigned i = 0; i < m_asms.size(); ++i) {
s().assert_expr(m_asms[i].get());
}
}
else {
maxsmt_solver_base::commit_assignment();
}
}
void verify_assignment() {
IF_VERBOSE(0, verbose_stream() << "verify assignment\n";);
ref<solver> sat_solver = mk_inc_sat_solver(m, m_params);
@ -878,7 +896,7 @@ public:
}
expr_ref n(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
n = m_soft[i].get();
n = m_soft[i];
if (!m_assignment[i]) {
n = mk_not(m, n);
}

2
src/opt/maxsls.cpp
View file

@ -41,7 +41,7 @@ namespace opt {
m_upper.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr_ref tmp(m);
m_model->eval(m_soft[i].get(), tmp, true);
m_model->eval(m_soft[i], tmp, true);
m_assignment[i] = m.is_true(tmp);
if (!m_assignment[i]) {
m_upper += m_weights[i];

42
src/opt/maxsmt.cpp
View file

@ -30,6 +30,7 @@ Notes:
#include "opt_context.h"
#include "theory_wmaxsat.h"
#include "ast_util.h"
#include "pb_decl_plugin.h"
namespace opt {
@ -38,12 +39,13 @@ namespace opt {
context& c, vector<rational> const& ws, expr_ref_vector const& soft):
m(c.get_manager()),
m_c(c),
m_cancel(false), m_soft(m),
m_cancel(false),
m_soft(soft),
m_weights(ws),
m_assertions(m) {
c.get_base_model(m_model);
SASSERT(m_model);
updt_params(c.params());
init_soft(ws, soft);
}
void maxsmt_solver_base::updt_params(params_ref& p) {
@ -54,11 +56,17 @@ namespace opt {
return m_c.get_solver();
}
void maxsmt_solver_base::init_soft(vector<rational> const& weights, expr_ref_vector const& soft) {
m_weights.reset();
m_soft.reset();
m_weights.append(weights);
m_soft.append(soft);
void maxsmt_solver_base::commit_assignment() {
expr_ref tmp(m);
rational k(0);
for (unsigned i = 0; i < m_soft.size(); ++i) {
if (get_assignment(i)) {
k += m_weights[i];
}
}
pb_util pb(m);
tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k);
s().assert_expr(tmp);
}
void maxsmt_solver_base::init() {
@ -67,7 +75,7 @@ namespace opt {
m_assignment.reset();
for (unsigned i = 0; i < m_weights.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_soft[i].get(), val));
VERIFY(m_model->eval(m_soft[i], val));
m_assignment.push_back(m.is_true(val));
if (!m_assignment.back()) {
m_upper += m_weights[i];
@ -178,7 +186,7 @@ namespace opt {
m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
}
else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("fu_malik")) {
m_msolver = alloc(fu_malik, m_c, m_soft_constraints);
m_msolver = mk_fu_malik(m_c, m_weights, m_soft_constraints);
}
else {
if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
@ -217,12 +225,6 @@ namespace opt {
// TBD: have to use a different solver
// because we don't push local scope any longer.
return;
solver::scoped_push _sp(s());
commit_assignment();
if (l_true != s().check_sat(0,0)) {
IF_VERBOSE(0, verbose_stream() << "could not verify assignment\n";);
UNREACHABLE();
}
}
bool maxsmt::get_assignment(unsigned idx) const {
@ -265,14 +267,8 @@ namespace opt {
}
void maxsmt::commit_assignment() {
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
expr_ref tmp(m);
tmp = m_soft_constraints[i].get();
if (!get_assignment(i)) {
tmp = mk_not(m, tmp);
}
TRACE("opt", tout << "committing: " << tmp << "\n";);
s().assert_expr(tmp);
if (m_msolver) {
m_msolver->commit_assignment();
}
}

8
src/opt/maxsmt.h
View file

@ -61,9 +61,9 @@ namespace opt {
ast_manager& m;
context& m_c;
volatile bool m_cancel;
expr_ref_vector m_soft;
expr_ref_vector m_assertions;
const expr_ref_vector m_soft;
vector<rational> m_weights;
expr_ref_vector m_assertions;
rational m_lower;
rational m_upper;
model_ref m_model;
@ -80,9 +80,9 @@ namespace opt {
virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); }
virtual void collect_statistics(statistics& st) const { }
virtual void get_model(model_ref& mdl) { mdl = m_model.get(); }
virtual void commit_assignment();
void set_model() { s().get_model(m_model); }
virtual void updt_params(params_ref& p);
virtual void init_soft(weights_t& weights, expr_ref_vector const& soft);
solver& s();
void init();
void set_mus(bool f);
@ -114,7 +114,7 @@ namespace opt {
class maxsmt {
ast_manager& m;
context& m_c;
scoped_ptr<maxsmt_solver> m_msolver;
scoped_ptr<maxsmt_solver_base> m_msolver;
volatile bool m_cancel;
expr_ref_vector m_soft_constraints;
expr_ref_vector m_answer;

5
src/opt/opt_context.cpp
View file

@ -1204,10 +1204,7 @@ namespace opt {
maxsmt& ms = *m_maxsmts.find(obj.m_id);
for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
VERIFY(m_model->eval(obj.m_terms[i], val));
CTRACE("opt",ms.get_assignment(i) != (m.mk_true() == val),
tout << mk_pp(obj.m_terms[i], m) << " evaluates to " << val << "\n";
model_smt2_pp(tout, m, *m_model, 0););
SASSERT(ms.get_assignment(i) == (m.mk_true() == val));
// TBD: check that optimal was not changed.
}
break;
}

2
src/opt/wmax.cpp
View file

@ -43,7 +43,7 @@ namespace opt {
lbool is_sat = l_true;
bool was_sat = false;
for (unsigned i = 0; i < m_soft.size(); ++i) {
wth().assert_weighted(m_soft[i].get(), m_weights[i]);
wth().assert_weighted(m_soft[i], m_weights[i]);
}
while (l_true == is_sat) {
is_sat = s().check_sat(0,0);