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

fixes to maxsmt

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-14 16:06:03 +02:00
parent 5f72325e99
commit ac893e907f
11 changed files with 124 additions and 113 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
src/opt/core_maxsat.cpp
View file

@ -21,11 +21,10 @@ Notes:
#include "ast_pp.h"
namespace opt {
core_maxsat::core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints):
m(m), s(s), m_soft(soft_constraints), m_answer(m) {
m_upper = m_soft.size();
m(m), s(s), m_lower(0), m_upper(soft_constraints.size()), m_soft(soft_constraints) {
m_answer.resize(m_soft.size(), false);
}
core_maxsat::~core_maxsat() {}
@ -41,7 +40,7 @@ namespace opt {
s.assert_expr(m.mk_or(a, m_soft[i].get()));
block_vars.insert(aux.back());
}
while (m_answer.size() < m_upper) {
while (m_lower < m_upper) {
ptr_vector<expr> vars;
set2vector(block_vars, vars);
lbool is_sat = s.check_sat(vars.size(), vars.c_ptr());
@ -51,31 +50,31 @@ namespace opt {
return l_undef;
case l_true: {
model_ref mdl;
expr_ref_vector ans(m);
svector<bool> ans;
unsigned new_lower = 0;
s.get_model(mdl);
for (unsigned i = 0; i < aux.size(); ++i) {
expr_ref val(m);
VERIFY(mdl->eval(m_soft[i].get(), val));
if (m.is_true(val)) {
ans.push_back(m_soft[i].get());
}
ans.push_back(m.is_true(val));
if (ans.back()) ++new_lower;
}
TRACE("opt", tout << "sat\n";
for (unsigned i = 0; i < ans.size(); ++i) {
tout << mk_pp(ans[i].get(), m) << "\n";
tout << mk_pp(m_soft[i].get(), m) << " |-> " << ans[i] << "\n";
});
IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat with lower bound: " << ans.size() << "\n";);
if (ans.size() > m_answer.size()) {
IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat with lower bound: " << new_lower << "\n";);
if (new_lower > m_lower) {
m_answer.reset();
m_answer.append(ans);
m_model = mdl.get();
m_lower = new_lower;
}
if (m_answer.size() == m_upper) {
if (m_lower == m_upper) {
return l_true;
}
SASSERT(m_soft.size() >= m_answer.size()+1);
unsigned k = m_soft.size()-m_answer.size()-1;
SASSERT(m_soft.size() >= new_lower+1);
unsigned k = m_soft.size()-new_lower-1;
expr_ref fml = mk_at_most(core_vars, k);
TRACE("opt", tout << "add: " << fml << "\n";);
s.assert_expr(fml);
@ -95,7 +94,7 @@ namespace opt {
}
IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
if (core.empty()) {
m_upper = m_answer.size();
m_upper = m_lower;
return l_true;
}
else {
@ -134,16 +133,13 @@ namespace opt {
}
rational core_maxsat::get_lower() const {
return rational(m_answer.size());
return rational(m_soft.size()-m_upper);
}
rational core_maxsat::get_upper() const {
return rational(m_upper);
return rational(m_soft.size()-m_lower);
}
rational core_maxsat::get_value() const {
return get_lower();
}
expr_ref_vector core_maxsat::get_assignment() const {
return m_answer;
bool core_maxsat::get_assignment(unsigned idx) const {
return m_answer[idx];
}
void core_maxsat::set_cancel(bool f) {
@ -153,6 +149,14 @@ namespace opt {
}
void core_maxsat::get_model(model_ref& mdl) {
mdl = m_model.get();
if (!mdl) {
SASSERT(m_upper == 0);
lbool is_sat = s.check_sat(0, 0);
if (is_sat == l_true) {
s.get_model(m_model);
}
mdl = m_model;
}
}

6
src/opt/core_maxsat.h
View file

@ -29,8 +29,9 @@ namespace opt {
ast_manager& m;
solver& s;
expr_ref_vector m_soft;
expr_ref_vector m_answer;
svector<bool> m_answer;
unsigned m_upper;
unsigned m_lower;
model_ref m_model;
public:
core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints);
@ -38,8 +39,7 @@ namespace opt {
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 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& mdl);

87
src/opt/fu_malik.cpp
View file

@ -49,7 +49,7 @@ namespace opt {
expr_ref_vector m_soft;
expr_ref_vector m_orig_soft;
expr_ref_vector m_aux;
expr_ref_vector m_assignment;
svector<bool> m_assignment;
unsigned m_upper;
unsigned m_lower;
model_ref m_model;
@ -63,12 +63,12 @@ namespace opt {
m_soft(soft),
m_orig_soft(soft),
m_aux(m),
m_assignment(m),
m_upper(0),
m_lower(0),
m_use_new_bv_solver(false)
{
m_upper = m_soft.size() + 1;
m_assignment.resize(m_soft.size(), false);
}
solver& s() { return *m_s; }
@ -286,44 +286,44 @@ namespace opt {
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
lbool operator()() {
lbool is_sat = l_true;
if (m_soft.empty()) {
return is_sat;
}
set_solver();
lbool is_sat = s().check_sat(0,0);
if (!m_soft.empty() && is_sat == l_true) {
solver::scoped_push _sp(s());
expr_ref tmp(m);
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_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
m_opt_solver.mc().insert(to_app(m_aux.back())->get_decl());
tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
s().assert_expr(tmp);
}
lbool is_sat = l_true;
do {
is_sat = step();
--m_upper;
}
while (is_sat == l_false);
if (is_sat == l_true) {
// Get a list satisfying m_soft
s().get_model(m_model);
m_lower = m_upper;
m_assignment.reset();
for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_orig_soft[i].get(), val));
if (m.is_true(val)) {
m_assignment.push_back(m_orig_soft[i].get());
}
}
TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";);
solver::scoped_push _sp(s());
expr_ref tmp(m);
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_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
m_opt_solver.mc().insert(to_app(m_aux.back())->get_decl());
tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
s().assert_expr(tmp);
}
do {
is_sat = step();
--m_upper;
}
while (is_sat == l_false);
if (is_sat == l_true) {
// Get a list satisfying m_soft
s().get_model(m_model);
m_lower = m_upper;
m_assignment.reset();
for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_orig_soft[i].get(), val));
m_assignment.push_back(m.is_true(val));
}
TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";);
}
// We are done and soft_constraints has
// been updated with the max-sat assignment.
@ -347,16 +347,13 @@ namespace opt {
return (*m_imp)();
}
rational fu_malik::get_lower() const {
return rational(m_imp->m_lower);
return rational(m_imp->m_soft.size()-m_imp->m_upper);
}
rational fu_malik::get_upper() const {
return rational(m_imp->m_upper);
return rational(m_imp->m_soft.size()-m_imp->m_lower);
}
rational fu_malik::get_value() const {
return rational(m_imp->m_assignment.size());
}
expr_ref_vector fu_malik::get_assignment() const {
return m_imp->m_assignment;
bool fu_malik::get_assignment(unsigned idx) const {
return m_imp->m_assignment[idx];
}
void fu_malik::set_cancel(bool f) {
// no-op

3
src/opt/fu_malik.h
View file

@ -38,8 +38,7 @@ namespace opt {
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 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);

41
src/opt/maxsmt.cpp
View file

@ -28,14 +28,12 @@ namespace opt {
lbool maxsmt::operator()(opt_solver& s) {
lbool is_sat;
m_answer.reset();
m_msolver = 0;
m_s = &s;
if (m_soft_constraints.empty()) {
TRACE("opt", tout << "no constraints\n";);
m_msolver = 0;
is_sat = s.check_sat(0, 0);
m_answer.reset();
}
else if (is_maxsat_problem(m_weights)) {
if (m_maxsat_engine == symbol("core_maxsat")) {
@ -51,7 +49,6 @@ namespace opt {
if (m_msolver) {
is_sat = (*m_msolver)();
m_answer.append(m_msolver->get_assignment());
if (is_sat == l_true) {
m_msolver->get_model(m_model);
}
@ -75,16 +72,14 @@ namespace opt {
return is_sat;
}
expr_ref_vector maxsmt::get_assignment() const {
return m_answer;
}
rational maxsmt::get_value() const {
bool maxsmt::get_assignment(unsigned idx) const {
if (m_msolver) {
return m_msolver->get_value();
return m_msolver->get_assignment(idx);
}
return m_upper;
}
else {
return true;
}
}
rational maxsmt::get_lower() const {
rational r = m_lower;
@ -114,15 +109,29 @@ namespace opt {
void maxsmt::commit_assignment() {
SASSERT(m_s);
for (unsigned i = 0; i < m_answer.size(); ++i) {
m_s->assert_expr(m_answer[i].get());
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
expr_ref tmp(m);
tmp = m_soft_constraints[i].get();
if (get_assignment(i)) {
m_s->assert_expr(tmp);
}
else {
tmp = m.mk_not(tmp);
m_s->assert_expr(tmp);
}
}
}
void maxsmt::display_answer(std::ostream& out) const {
for (unsigned i = 0; i < m_answer.size(); ++i) {
out << mk_pp(m_answer[i], m) << "\n";
}
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
out << mk_pp(m_soft_constraints[i], m);
if (get_assignment(i)) {
out << " |-> true\n";
}
else {
out << " |-> false\n";
}
}
}
void maxsmt::set_cancel(bool f) {

5
src/opt/maxsmt.h
View file

@ -30,8 +30,7 @@ namespace opt {
virtual lbool operator()() = 0;
virtual rational get_lower() const = 0;
virtual rational get_upper() const = 0;
virtual rational get_value() const = 0;
virtual expr_ref_vector get_assignment() const = 0;
virtual bool get_assignment(unsigned index) const = 0;
virtual void set_cancel(bool f) = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual void get_model(model_ref& mdl) = 0;
@ -80,7 +79,7 @@ namespace opt {
rational get_upper() const;
void update_lower(rational const& r);
void get_model(model_ref& mdl);
expr_ref_vector get_assignment() const;
bool get_assignment(unsigned index) const;
void display_answer(std::ostream& out) const;
void collect_statistics(statistics& st) const;

10
src/opt/opt_context.cpp
View file

@ -54,6 +54,7 @@ namespace opt {
maxsmt* ms;
if (!m_maxsmts.find(id, ms)) {
ms = alloc(maxsmt, m);
ms->updt_params(m_params);
m_maxsmts.insert(id, ms);
m_objectives.push_back(objective(m, id));
m_indices.insert(id, m_objectives.size() - 1);
@ -352,6 +353,7 @@ namespace opt {
obj.m_weights.append(weights);
SASSERT(!m_maxsmts.contains(id));
maxsmt* ms = alloc(maxsmt, m);
ms->updt_params(m_params);
m_maxsmts.insert(id, ms);
m_indices.insert(id, index);
}
@ -730,8 +732,14 @@ namespace opt {
}
break;
}
case O_MAXSMT:
case O_MAXSMT: {
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));
SASSERT(ms.get_assignment(i) == (m.mk_true() == val));
}
break;
}
}
}
}

7
src/opt/optsmt.cpp
View file

@ -296,9 +296,6 @@ namespace opt {
return is_sat;
}
inf_eps optsmt::get_value(unsigned i) const {
return get_lower(i);
}
inf_eps optsmt::get_lower(unsigned i) const {
return m_is_max[i]?m_lower[i]:-m_lower[i];
@ -325,7 +322,7 @@ namespace opt {
std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const {
bool is_max = m_is_max[i];
inf_eps val = get_value(i);
inf_eps val = get_lower(i);
expr_ref obj(m_objs[i], m);
if (!is_max) {
arith_util a(m);
@ -344,7 +341,7 @@ namespace opt {
<< ":" << get_upper(i) << "]" << std::endl;
}
else {
display_objective(out, i) << " |-> " << get_value(i) << std::endl;
display_objective(out, i) << " |-> " << get_lower(i) << std::endl;
}
}
}

1
src/opt/optsmt.h
View file

@ -58,7 +58,6 @@ namespace opt {
unsigned get_num_objectives() const { return m_objs.size(); }
void commit_assignment(unsigned index);
inf_eps get_value(unsigned index) const;
inf_eps get_lower(unsigned index) const;
inf_eps get_upper(unsigned index) const;
void get_model(model_ref& mdl);

24
src/opt/weighted_maxsat.cpp
View file

@ -46,15 +46,16 @@ namespace smt {
/**
\brief return the complement of variables that are currently assigned.
*/
void get_assignment(expr_ref_vector& result) {
void get_assignment(svector<bool>& result) {
result.reset();
std::sort(m_cost_save.begin(), m_cost_save.end());
for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
if (j < m_cost_save.size() && m_cost_save[j] == i) {
result.push_back(false);
++j;
}
else {
result.push_back(m_fmls[i].get());
result.push_back(true);
}
}
}
@ -282,15 +283,17 @@ namespace opt {
ast_manager& m;
opt_solver& s;
expr_ref_vector m_soft;
expr_ref_vector m_assignment;
svector<bool> m_assignment;
vector<rational> m_weights;
rational m_upper;
rational m_lower;
model_ref m_model;
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)
{}
m(m), s(s), m_soft(soft_constraints), m_weights(weights)
{
m_assignment.resize(m_soft.size(), false);
}
~imp() {}
smt::theory_weighted_maxsat* get_theory() const {
@ -333,9 +336,9 @@ namespace opt {
wth.assert_weighted(m_soft[i].get(), m_weights[i]);
}
result = s.check_sat_core(0,0);
SASSERT(result != l_true);
wth.get_assignment(m_assignment);
if (!m_assignment.empty() && result == l_false) {
if (result == l_false) {
result = l_true;
}
}
@ -382,11 +385,8 @@ namespace opt {
rational wmaxsmt::get_upper() const {
return m_imp->get_upper();
}
rational wmaxsmt::get_value() const {
return m_imp->get_upper();
}
expr_ref_vector wmaxsmt::get_assignment() const {
return m_imp->m_assignment;
bool wmaxsmt::get_assignment(unsigned idx) const {
return m_imp->m_assignment[idx];
}
void wmaxsmt::set_cancel(bool f) {
// no-op

3
src/opt/weighted_maxsat.h
View file

@ -36,8 +36,7 @@ namespace opt {
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 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& mdl);