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

remove deprecated maxsat solvers, adjust values inline

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-14 11:55:47 -07:00
parent 770d0d58fe
commit a96fa0c555
13 changed files with 66 additions and 408 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/bcd2.cpp
View file

@ -124,7 +124,7 @@ namespace opt {
}
process_sat();
while (m_lower < m_upper) {
IF_VERBOSE(1, verbose_stream() << "(opt.bcd2 [" << m_lower << ":" << m_upper << "])\n";);
trace_bounds("bcd2");
assert_soft();
solver::scoped_push _scope2(s());
TRACE("opt", display(tout););

168
src/opt/core_maxsat.cpp
View file

@ -1,168 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
core_maxsat.h
Abstract:
Core and SAT guided MaxSAT with cardinality constraints.
Author:
Nikolaj Bjorner (nbjorner) 2013-11-9
Notes:
--*/
#include "core_maxsat.h"
#include "pb_decl_plugin.h"
#include "ast_pp.h"
#include "opt_context.h"
namespace opt {
core_maxsat::core_maxsat(context& c, expr_ref_vector& soft_constraints):
m(c.get_manager()), s(c.get_solver()),
m_lower(0), m_upper(soft_constraints.size()), m_soft(soft_constraints) {
m_answer.resize(m_soft.size(), false);
}
core_maxsat::~core_maxsat() {}
lbool core_maxsat::operator()() {
expr_ref_vector aux(m); // auxiliary variables to track soft constraints
expr_set core_vars; // variables used so far in some core
expr_set block_vars; // variables that should be blocked.
solver::scoped_push _sp(s);
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr* a = m.mk_fresh_const("p", m.mk_bool_sort());
aux.push_back(m.mk_not(a));
s.assert_expr(m.mk_or(a, m_soft[i].get()));
block_vars.insert(aux.back());
}
while (m_lower < m_upper) {
ptr_vector<expr> vars;
set2vector(block_vars, vars);
lbool is_sat = s.check_sat(vars.size(), vars.c_ptr());
switch(is_sat) {
case l_undef:
return l_undef;
case l_true: {
model_ref mdl;
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));
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(m_soft[i].get(), m) << " |-> " << ans[i] << "\n";
});
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_lower == m_upper) {
return l_true;
}
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);
break;
}
case l_false: {
ptr_vector<expr> core;
s.get_unsat_core(core);
TRACE("opt", tout << "core";
for (unsigned i = 0; i < core.size(); ++i) {
tout << mk_pp(core[i], m) << " ";
}
tout << "\n";);
for (unsigned i = 0; i < core.size(); ++i) {
core_vars.insert(get_not(core[i]));
block_vars.remove(core[i]);
}
IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
if (core.empty()) {
m_upper = m_lower;
return l_true;
}
else {
// at least one core variable is True
expr_ref fml = mk_at_most(core_vars, 0);
fml = m.mk_not(fml);
TRACE("opt", tout << "add: " << fml << "\n";);
s.assert_expr(fml);
}
--m_upper;
}
}
}
return l_true;
}
void core_maxsat::set2vector(expr_set const& set, ptr_vector<expr>& es) const {
es.reset();
expr_set::iterator it = set.begin(), end = set.end();
for (; it != end; ++it) {
es.push_back(*it);
}
}
expr_ref core_maxsat::mk_at_most(expr_set const& set, unsigned k) {
pb_util pb(m);
ptr_vector<expr> es;
set2vector(set, es);
return expr_ref(pb.mk_at_most_k(es.size(), es.c_ptr(), k), m);
}
expr* core_maxsat::get_not(expr* e) const {
expr* result = 0;
VERIFY(m.is_not(e, result));
return result;
}
rational core_maxsat::get_lower() const {
return rational(m_soft.size()-m_upper);
}
rational core_maxsat::get_upper() const {
return rational(m_soft.size()-m_lower);
}
bool core_maxsat::get_assignment(unsigned idx) const {
return m_answer[idx];
}
void core_maxsat::set_cancel(bool f) {
}
void core_maxsat::collect_statistics(statistics& st) const {
// nothing specific
}
void core_maxsat::updt_params(params_ref& p) {
// no-op
}
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;
}
}
};

55
src/opt/core_maxsat.h
View file

@ -1,55 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
core_maxsat.h
Abstract:
Core and SAT guided MaxSAT with cardinality constraints.
Author:
Nikolaj Bjorner (nbjorner) 2013-11-9
Notes:
--*/
#ifndef _OPT_CORE_MAXSAT_H_
#define _OPT_CORE_MAXSAT_H_
#include "solver.h"
#include "maxsmt.h"
namespace opt {
class core_maxsat : public maxsmt_solver {
typedef obj_hashtable<expr> expr_set;
ast_manager& m;
solver& s;
expr_ref_vector m_soft;
svector<bool> m_answer;
unsigned m_upper;
unsigned m_lower;
model_ref m_model;
public:
core_maxsat(context& c, expr_ref_vector& soft_constraints);
virtual ~core_maxsat();
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& mdl);
virtual void updt_params(params_ref& p);
private:
void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
expr_ref mk_at_most(expr_set const& set, unsigned k);
expr* get_not(expr* e) const;
};
};
#endif

3
src/opt/maxhs.cpp
View file

@ -111,8 +111,7 @@ namespace opt {
seed2assumptions();
while (m_lower < m_upper) {
++m_stats.m_num_iterations;
IF_VERBOSE(1, verbose_stream() <<
"(opt.maxhs [" << m_lower << ":" << m_upper << "])\n";);
trace_bounds("maxhs");
TRACE("opt", tout << "(maxhs [" << m_lower << ":" << m_upper << "])\n";);
if (m_cancel) {
return l_undef;

7
src/opt/maxres.cpp
View file

@ -193,7 +193,7 @@ public:
exprs mcs;
lbool is_sat = l_true;
while (m_lower < m_upper && is_sat == l_true) {
IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
trace_bounds("maxres");
if (m_cancel) {
return l_undef;
}
@ -512,7 +512,7 @@ public:
fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
s().assert_expr(fml);
m_lower += w;
IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
trace_bounds("maxres");
}
bool get_mus_model(model_ref& mdl) {
@ -789,8 +789,7 @@ public:
}
m_upper = upper;
// verify_assignment();
IF_VERBOSE(1, verbose_stream() <<
"(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
trace_bounds("maxres");
add_upper_bound_block();
}

31
src/opt/maxsmt.cpp
View file

@ -20,11 +20,9 @@ Notes:
#include <typeinfo>
#include "maxsmt.h"
#include "fu_malik.h"
#include "core_maxsat.h"
#include "maxres.h"
#include "maxhs.h"
#include "bcd2.h"
#include "pbmax.h"
#include "wmax.h"
#include "maxsls.h"
#include "ast_pp.h"
@ -140,6 +138,13 @@ namespace opt {
}
smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
void maxsmt_solver_base::trace_bounds(char const * solver) {
IF_VERBOSE(1,
rational l = m_adjust_value(m_lower);
rational u = m_adjust_value(m_upper);
if (l > u) std::swap(l, u);
verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);
}
@ -167,9 +172,6 @@ namespace opt {
else if (maxsat_engine == symbol("mss-maxres")) {
m_msolver = mk_mss_maxres(m_c, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("pbmax")) {
m_msolver = mk_pbmax(m_c, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("bcd2")) {
m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints);
}
@ -180,9 +182,6 @@ namespace opt {
// NB: this is experimental one-round version of SLS
m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
}
else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("core_maxsat")) {
m_msolver = alloc(core_maxsat, m_c, 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);
}
@ -196,6 +195,7 @@ namespace opt {
if (m_msolver) {
m_msolver->updt_params(m_params);
m_msolver->set_adjust_value(m_adjust_value);
is_sat = (*m_msolver)();
if (is_sat != l_false) {
m_msolver->get_model(m_model);
@ -245,7 +245,7 @@ namespace opt {
rational q = m_msolver->get_lower();
if (q > r) r = q;
}
return r;
return m_adjust_value(r);
}
rational maxsmt::get_upper() const {
@ -254,17 +254,16 @@ namespace opt {
rational q = m_msolver->get_upper();
if (q < r) r = q;
}
return r;
return m_adjust_value(r);
}
void maxsmt::update_lower(rational const& r, bool override) {
if (m_lower > r || override) m_lower = r;
void maxsmt::update_lower(rational const& r) {
if (m_lower > r) m_lower = r;
}
void maxsmt::update_upper(rational const& r, bool override) {
if (m_upper < r || override) m_upper = r;
}
void maxsmt::update_upper(rational const& r) {
if (m_upper < r) m_upper = r;
}
void maxsmt::get_model(model_ref& mdl) {
mdl = m_model.get();

13
src/opt/maxsmt.h
View file

@ -27,6 +27,7 @@ Notes:
#include"smt_context.h"
#include"smt_theory.h"
#include"theory_wmaxsat.h"
#include"opt_solver.h"
namespace opt {
@ -35,6 +36,8 @@ namespace opt {
class context;
class maxsmt_solver {
protected:
adjust_value m_adjust_value;
public:
virtual ~maxsmt_solver() {}
virtual lbool operator()() = 0;
@ -45,6 +48,7 @@ namespace opt {
virtual void collect_statistics(statistics& st) const = 0;
virtual void get_model(model_ref& mdl) = 0;
virtual void updt_params(params_ref& p) = 0;
void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
};
@ -100,6 +104,7 @@ namespace opt {
protected:
void enable_sls(expr_ref_vector const& soft, weights_t& ws);
void set_enable_sls(bool f);
void trace_bounds(char const* solver);
};
@ -119,6 +124,7 @@ namespace opt {
vector<rational> m_weights;
rational m_lower;
rational m_upper;
adjust_value m_adjust_value;
model_ref m_model;
params_ref m_params;
public:
@ -127,15 +133,16 @@ namespace opt {
void set_cancel(bool f);
void updt_params(params_ref& p);
void add(expr* f, rational const& w);
void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
unsigned size() const { return m_soft_constraints.size(); }
expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
rational weight(unsigned idx) const { return m_weights[idx]; }
void commit_assignment();
rational get_value() const;
rational get_lower() const;
rational get_upper() const;
void update_lower(rational const& r, bool override);
void update_upper(rational const& r, bool override);
rational get_upper() const;
void update_lower(rational const& r);
void update_upper(rational const& r);
void get_model(model_ref& mdl);
bool get_assignment(unsigned index) const;
void display_answer(std::ostream& out) const;

42
src/opt/opt_context.cpp
View file

@ -218,7 +218,7 @@ namespace opt {
IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";);
s.get_model(m_model);
m_optsmt.setup(*m_opt_solver.get());
update_lower(true);
update_lower();
switch (m_objectives.size()) {
case 0:
return is_sat;
@ -293,7 +293,7 @@ namespace opt {
return r;
}
if (r == l_true && i + 1 < m_objectives.size()) {
update_lower(true);
update_lower();
}
}
DEBUG_CODE(if (r == l_true) validate_lex(););
@ -398,8 +398,8 @@ namespace opt {
void context::yield() {
m_pareto->get_model(m_model);
update_bound(true, true);
update_bound(true, false);
update_bound(true);
update_bound(false);
}
lbool context::execute_pareto() {
@ -763,8 +763,9 @@ namespace opt {
SASSERT(obj.m_id == id);
obj.m_terms.reset();
obj.m_terms.append(terms);
obj.m_adjust_bound.set_offset(offset);
obj.m_adjust_bound.set_negate(neg);
obj.m_adjust_value.set_offset(offset);
obj.m_adjust_value.set_negate(neg);
m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value);
TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";);
}
else if (is_maximize(fml, tr, orig_term, index)) {
@ -772,6 +773,7 @@ namespace opt {
}
else if (is_minimize(fml, tr, orig_term, index)) {
m_objectives[index].m_term = tr;
m_objectives[index].m_adjust_value.set_negate(true);
}
else {
m_hard_constraints.push_back(fml);
@ -826,15 +828,16 @@ namespace opt {
}
}
void context::update_bound(bool override, bool is_lower) {
void context::update_bound(bool is_lower) {
expr_ref val(m);
bool override = true;
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
rational r;
switch(obj.m_type) {
case O_MINIMIZE:
if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
inf_eps val = obj.m_adjust_bound.neg_add(r);
inf_eps val = inf_eps(obj.m_adjust_value(r));
if (is_lower) {
m_optsmt.update_lower(obj.m_index, val, override);
}
@ -845,7 +848,7 @@ namespace opt {
break;
case O_MAXIMIZE:
if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
inf_eps val = obj.m_adjust_bound.neg_add(r);
inf_eps val = inf_eps(obj.m_adjust_value(r));
if (is_lower) {
m_optsmt.update_lower(obj.m_index, val, override);
}
@ -868,10 +871,10 @@ namespace opt {
}
if (ok) {
if (is_lower) {
m_maxsmts.find(obj.m_id)->update_upper(r, override);
m_maxsmts.find(obj.m_id)->update_upper(r);
}
else {
m_maxsmts.find(obj.m_id)->update_lower(r, override);
m_maxsmts.find(obj.m_id)->update_lower(r);
}
}
break;
@ -918,14 +921,12 @@ namespace opt {
}
objective const& obj = m_objectives[idx];
switch(obj.m_type) {
case O_MAXSMT: {
rational r = m_maxsmts.find(obj.m_id)->get_lower();
return obj.m_adjust_bound.neg_add(r);
}
case O_MAXSMT:
return inf_eps(m_maxsmts.find(obj.m_id)->get_lower());
case O_MINIMIZE:
return -m_optsmt.get_upper(obj.m_index);
return obj.m_adjust_value(m_optsmt.get_upper(obj.m_index));
case O_MAXIMIZE:
return m_optsmt.get_lower(obj.m_index);
return obj.m_adjust_value(m_optsmt.get_lower(obj.m_index));
default:
UNREACHABLE();
return inf_eps();
@ -939,12 +940,11 @@ namespace opt {
objective const& obj = m_objectives[idx];
switch(obj.m_type) {
case O_MAXSMT:
return obj.m_adjust_bound.neg_add(m_maxsmts.find(obj.m_id)->get_upper());
// TBD: adjust bound
return inf_eps(m_maxsmts.find(obj.m_id)->get_upper());
case O_MINIMIZE:
return -m_optsmt.get_lower(obj.m_index);
return obj.m_adjust_value(m_optsmt.get_lower(obj.m_index));
case O_MAXIMIZE:
return m_optsmt.get_upper(obj.m_index);
return obj.m_adjust_value(m_optsmt.get_upper(obj.m_index));
default:
UNREACHABLE();
return inf_eps();

8
src/opt/opt_context.h
View file

@ -51,7 +51,7 @@ namespace opt {
app_ref m_term; // for maximize, minimize term
expr_ref_vector m_terms; // for maxsmt
vector<rational> m_weights; // for maxsmt
bound_adjustment m_adjust_bound;
adjust_value m_adjust_value;
symbol m_id; // for maxsmt
unsigned m_index; // for maximize/minimize index
@ -63,7 +63,7 @@ namespace opt {
m_index(idx)
{
if (!is_max) {
m_adjust_bound.set_negate(true);
m_adjust_value.set_negate(true);
}
}
@ -212,8 +212,8 @@ namespace opt {
void from_fmls(expr_ref_vector const& fmls);
void simplify_fmls(expr_ref_vector& fmls);
void update_lower(bool override) { update_bound(override, true); }
void update_bound(bool override, bool is_lower);
void update_lower() { update_bound(true); }
void update_bound(bool is_lower);
inf_eps get_lower_as_num(unsigned idx);
inf_eps get_upper_as_num(unsigned idx);

19
src/opt/opt_solver.h
View file

@ -36,30 +36,31 @@ namespace opt {
typedef inf_eps_rational<inf_rational> inf_eps;
// Adjust bound bound |-> (m_negate?-1:1)*(m_offset + bound)
class bound_adjustment {
// Adjust bound bound |-> m_offset + (m_negate?-1:1)*bound
class adjust_value {
rational m_offset;
bool m_negate;
public:
bound_adjustment(rational const& offset, bool neg):
adjust_value(rational const& offset, bool neg):
m_offset(offset),
m_negate(neg)
{}
bound_adjustment(): m_offset(0), m_negate(false) {}
adjust_value(): m_offset(0), m_negate(false) {}
void set_offset(rational const& o) { m_offset = o; }
void set_negate(bool neg) { m_negate = neg; }
rational const& get_offset() const { return m_offset; }
bool get_negate() { return m_negate; }
inf_eps add_neg(rational const& r) const {
rational result = r + m_offset;
inf_eps operator()(inf_eps const& r) const {
inf_eps result = r;
if (m_negate) result.neg();
return inf_eps(result);
result += m_offset;
return result;
}
inf_eps neg_add(rational const& r) const {
rational operator()(rational const& r) const {
rational result = r;
if (m_negate) result.neg();
result += m_offset;
return inf_eps(result);
return result;
}
};

95
src/opt/pbmax.cpp
View file

@ -1,95 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
pbmax.cpp
Abstract:
pb based MaxSAT.
Author:
Nikolaj Bjorner (nbjorner) 2014-4-17
Notes:
--*/
#include "pbmax.h"
#include "pb_decl_plugin.h"
#include "uint_set.h"
#include "ast_pp.h"
#include "model_smt2_pp.h"
namespace opt {
// ----------------------------------
// incrementally add pseudo-boolean
// lower bounds.
class pbmax : public maxsmt_solver_base {
public:
pbmax(context& c, weights_t& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft) {
}
virtual ~pbmax() {}
lbool operator()() {
TRACE("opt", s().display(tout); tout << "\n";
for (unsigned i = 0; i < m_soft.size(); ++i) {
tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n";
}
);
pb_util u(m);
expr_ref fml(m), val(m);
app_ref b(m);
expr_ref_vector nsoft(m);
init();
for (unsigned i = 0; i < m_soft.size(); ++i) {
nsoft.push_back(mk_not(m_soft[i].get()));
}
lbool is_sat = l_true;
while (l_true == is_sat) {
TRACE("opt", s().display(tout<<"looping\n");
model_smt2_pp(tout << "\n", m, *(m_model.get()), 0););
m_upper.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
VERIFY(m_model->eval(nsoft[i].get(), val));
m_assignment[i] = !m.is_true(val);
if (!m_assignment[i]) {
m_upper += m_weights[i];
}
}
IF_VERBOSE(1, verbose_stream() << "(opt.pb [" << m_lower << ":" << m_upper << "])\n";);
TRACE("opt", tout << "new upper: " << m_upper << "\n";);
fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
solver::scoped_push _scope2(s());
s().assert_expr(fml);
is_sat = s().check_sat(0,0);
if (m_cancel) {
is_sat = l_undef;
}
if (is_sat == l_true) {
s().get_model(m_model);
}
}
if (is_sat == l_false) {
is_sat = l_true;
m_lower = m_upper;
}
TRACE("opt", tout << "lower: " << m_lower << "\n";);
return is_sat;
}
};
maxsmt_solver_base* mk_pbmax(
context & c, weights_t& ws, expr_ref_vector const& soft) {
return alloc(pbmax, c, ws, soft);
}
}

29
src/opt/pbmax.h
View file

@ -1,29 +0,0 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
pbmax.h
Abstract:
MaxSAT based on pb theory.
Author:
Nikolaj Bjorner (nbjorner) 2014-4-17
Notes:
--*/
#ifndef _PBMAX_H_
#define _PBMAX_H_
#include "maxsmt.h"
namespace opt {
maxsmt_solver_base* mk_pbmax(context& c, weights_t& ws, expr_ref_vector const& soft);
}
#endif

2
src/opt/wmax.cpp
View file

@ -59,7 +59,7 @@ namespace opt {
s().assert_expr(fml);
was_sat = true;
}
IF_VERBOSE(1, verbose_stream() << "(opt.wmax [" << m_lower << ":" << m_upper << "])\n";);
trace_bounds("wmax");
}
if (was_sat) {
wth().get_assignment(m_assignment);