mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

adding options to maxres for experiments, include option to pretty print module parameters in smt2 style

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-30 11:46:29 -07:00
parent b45b2872d8
commit 83a7d1a658
14 changed files with 249 additions and 131 deletions
Download patch file Download diff file Expand all files Collapse all files

185
src/opt/maxres.cpp
View file

@ -62,6 +62,7 @@ Notes:
#include "inc_sat_solver.h"
#include "opt_context.h"
#include "pb_decl_plugin.h"
#include "opt_params.hpp"
using namespace opt;
@ -85,9 +86,14 @@ private:
expr_ref_vector m_trail;
strategy_t m_st;
rational m_max_upper;
bool m_hill_climb;
bool m_all_cores;
bool m_add_upper_bound_block;
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.
unsigned m_max_core_size; // max core size per round.
bool m_maximize_assignment; // maximize assignment to find MCS
unsigned m_max_correction_set_size;// maximal set of correction set that is tolerated.
bool m_wmax; // Block upper bound using wmax
// this option is disabled if SAT core is used.
typedef ptr_vector<expr> exprs;
@ -102,8 +108,11 @@ public:
m_trail(m),
m_st(st),
m_hill_climb(true),
m_all_cores(false),
m_add_upper_bound_block(false)
m_add_upper_bound_block(false),
m_max_num_cores(UINT_MAX),
m_max_core_size(3),
m_maximize_assignment(false),
m_max_correction_set_size(3)
{
}
@ -201,14 +210,11 @@ public:
return l_true;
case l_true:
SASSERT(cores.empty() || mcs.empty());
for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
is_sat = process_unsat(cores[i]);
for (unsigned i = 0; i < cores.size(); ++i) {
process_unsat(cores[i]);
}
if (is_sat == l_true && cores.empty()) {
is_sat = process_sat(mcs);
}
if (is_sat != l_true) {
return is_sat;
if (cores.empty()) {
process_sat(mcs);
}
break;
}
@ -233,8 +239,8 @@ public:
mcs.reset();
s().get_model(mdl);
update_assignment(mdl.get());
is_sat = get_mss(cores, mss, mcs);
is_sat = get_mss(mdl.get(), cores, mss, mcs);
switch (is_sat) {
case l_undef:
return l_undef;
@ -242,11 +248,8 @@ public:
m_lower = m_upper;
return l_true;
case l_true: {
is_sat = process_sat(mcs);
if (is_sat != l_true) {
return is_sat;
}
update_mss_model();
process_sat(mcs);
get_mss_model();
break;
}
}
@ -281,12 +284,15 @@ public:
What are the corner cases:
- suppose that cost of cores adds up to current upper bound.
-> it means that each core is a unit (?)
TBD:
- Block upper bound using wmax or pb constraint, or in case of
unweighted constraints using incremental tricks.
- Throttle when correction set gets added based on its size.
Suppose correction set is huge. Do we really need it?
*/
lbool mus_mss2_solver() {
// m_all_cores = true;
// m_add_upper_bound_block = true;
bool maximize_assignment = false;
init();
init_local();
sls();
@ -321,42 +327,46 @@ public:
SASSERT((is_sat == l_true) == !cores.empty());
if (cores.empty()) {
break;
}
}
//
// There is a best model,
// retrieve it from the previous
// core calls.
// There is a best model, retrieve
// it from the previous core calls.
//
update_mus_model();
model_ref mdl;
get_mus_model(mdl);
//
// Extend the current model to a (maximal)
// assignment extracting the ss and cs.
// ss - satisfying subset
// cs - correction set (complement of ss).
//
if (maximize_assignment) {
if (m_maximize_assignment && mdl.get()) {
exprs ss, cs;
// TBD: current model has to evaluate all auxiliary predicates.
is_sat = get_mss(cores, ss, cs);
is_sat = get_mss(mdl.get(), cores, ss, cs);
if (is_sat != l_true) return is_sat;
update_mss_model();
get_mss_model();
}
//
// block the hard constraints corresponding to the cores.
// block the soft constraints corresponding to the cs
// obtained from the current best model.
//
// TBD: model must be updated with definitions for the
// fresh variables.
//
is_sat = process_unsat(cores);
if (is_sat != l_true) return is_sat;
//
// TBD: throttle blocking on correction sets if they are too big.
// likewise, if the cores are too big, don't block the cores.
//
process_unsat(cores);
exprs cs;
get_current_correction_set(cs);
is_sat = process_sat(cs);
if (is_sat != l_true) return is_sat;
unsigned max_core = max_core_size(cores);
if (cs.size() <= std::max(max_core, m_max_correction_set_size)) {
process_sat(cs);
}
}
m_lower = m_upper;
@ -404,8 +414,15 @@ public:
if (is_sat != l_true) {
break;
}
if (core.empty()) {
cores.reset();
return l_false;
}
cores.push_back(core);
if (!m_all_cores && core.size() >= 3) {
if (core.size() >= m_max_core_size) {
break;
}
if (cores.size() >= m_max_num_cores) {
break;
}
remove_soft(core, asms);
@ -442,7 +459,6 @@ public:
}
void get_current_correction_set(exprs& cs) {
TRACE("opt", display_vec(tout << "old correction set: ", cs.size(), cs.c_ptr()););
cs.reset();
for (unsigned i = 0; i < m_asms.size(); ++i) {
if (!is_true(m_asms[i].get())) {
@ -482,13 +498,12 @@ public:
return index;
}
lbool process_sat(exprs const& corr_set) {
void process_sat(exprs const& corr_set) {
expr_ref fml(m), tmp(m);
TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
remove_core(corr_set);
rational w = split_core(corr_set);
cs_max_resolve(corr_set, w);
return l_true;
}
lbool process_unsat() {
@ -501,19 +516,26 @@ public:
return l_false;
}
else {
return process_unsat(cores);
process_unsat(cores);
return l_true;
}
}
lbool process_unsat(vector<exprs>& cores) {
lbool is_sat = l_true;
for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
is_sat = process_unsat(cores[i]);
unsigned max_core_size(vector<exprs> const& cores) {
unsigned result = 0;
for (unsigned i = 0; i < cores.size(); ++i) {
result = std::max(cores[i].size(), result);
}
return result;
}
void process_unsat(vector<exprs> const& cores) {
for (unsigned i = 0; i < cores.size(); ++i) {
process_unsat(cores[i]);
}
return is_sat;
}
lbool process_unsat(exprs const& core) {
void process_unsat(exprs const& core) {
expr_ref fml(m);
remove_core(core);
SASSERT(!core.empty());
@ -524,31 +546,35 @@ public:
s().assert_expr(fml);
m_lower += w;
IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
return l_true;
}
void update_mus_model() {
if (!m_c.sat_enabled()) {
model_ref mdl;
rational w = m_mus.get_best_model(mdl);
if (mdl.get() && w < m_upper) {
update_assignment(mdl.get());
}
void get_mus_model(model_ref& mdl) {
rational w(0);
if (m_c.sat_enabled()) {
// SAT solver core extracts some model
// during unsat core computation.
s().get_model(mdl);
}
else {
w = m_mus.get_best_model(mdl);
}
if (mdl.get() && w < m_upper) {
update_assignment(mdl.get());
}
}
void update_mss_model() {
void get_mss_model() {
model_ref mdl;
m_mss.get_model(mdl); // last model is best way to reduce search space.
update_assignment(mdl.get());
}
lbool get_mss(vector<exprs> const& cores, exprs& literals, exprs& mcs) {
lbool get_mss(model* mdl, vector<exprs> const& cores, exprs& literals, exprs& mcs) {
literals.reset();
mcs.reset();
literals.append(m_asms.size(), m_asms.c_ptr());
set_mus(false);
lbool is_sat = m_mss(m_model.get(), cores, literals, mcs);
lbool is_sat = m_mss(mdl, cores, literals, mcs);
set_mus(true);
return is_sat;
}
@ -735,7 +761,7 @@ public:
if (is_sat != l_true) {
return is_sat;
}
update_mss_model();
get_mss_model();
if (!cores.empty() && mcs.size() > cores.back().size()) {
mcs.reset();
}
@ -804,16 +830,19 @@ public:
IF_VERBOSE(1, verbose_stream() <<
"(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
if (m_add_upper_bound_block) {
pb_util u(m);
expr_ref_vector nsoft(m);
expr_ref fml(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
nsoft.push_back(m.mk_not(m_soft[i].get()));
}
fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
s().assert_expr(fml);
}
add_upper_bound_block();
}
void add_upper_bound_block() {
if (!m_add_upper_bound_block) return;
pb_util u(m);
expr_ref_vector nsoft(m);
expr_ref fml(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
nsoft.push_back(m.mk_not(m_soft[i].get()));
}
fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
s().assert_expr(fml);
}
bool is_true(expr* e) {
@ -845,6 +874,19 @@ public:
m_mus.set_cancel(f);
}
virtual void updt_params(params_ref& p) {
maxsmt_solver_base::updt_params(p);
opt_params _p(p);
m_hill_climb = _p.maxres_hill_climb();
m_add_upper_bound_block = _p.maxres_add_upper_bound_block();
m_max_num_cores = _p.maxres_max_num_cores();
m_max_core_size = _p.maxres_max_core_size();
m_maximize_assignment = _p.maxres_maximize_assignment();
m_max_correction_set_size = _p.maxres_max_correction_set_size();
m_wmax = _p.maxres_wmax();
}
void init_local() {
m_upper.reset();
m_lower.reset();
@ -853,6 +895,7 @@ public:
add_soft(m_soft[i].get(), m_weights[i]);
}
m_max_upper = m_upper;
add_upper_bound_block();
}
void verify_assignment() {

36
src/opt/maxsmt.cpp
View file

@ -30,6 +30,7 @@ Notes:
#include "ast_pp.h"
#include "uint_set.h"
#include "opt_context.h"
#include "theory_wmaxsat.h"
namespace opt {
@ -108,6 +109,40 @@ namespace opt {
return result;
}
smt::theory_wmaxsat* maxsmt_solver_base::get_wmax_theory() const {
smt::theory_id th_id = m.get_family_id("weighted_maxsat");
smt::theory* th = m_c.smt_context().get_theory(th_id);
if (th) {
return dynamic_cast<smt::theory_wmaxsat*>(th);
}
else {
return 0;
}
}
smt::theory_wmaxsat* maxsmt_solver_base::ensure_wmax_theory() {
smt::theory_wmaxsat* wth = get_wmax_theory();
if (wth) {
wth->reset_local();
}
else {
wth = alloc(smt::theory_wmaxsat, m, m_c.fm());
m_c.smt_context().register_plugin(wth);
}
return wth;
}
maxsmt_solver_base::scoped_ensure_theory::scoped_ensure_theory(maxsmt_solver_base& s) {
m_wth = s.ensure_wmax_theory();
}
maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() {
//m_wth->reset();
}
smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
maxsmt::maxsmt(context& c):
m_s(c.get_solver()), m(c.get_manager()), m_c(c), m_cancel(false),
m_soft_constraints(m), m_answer(m) {}
@ -160,6 +195,7 @@ namespace opt {
}
if (m_msolver) {
m_msolver->updt_params(m_params);
is_sat = (*m_msolver)();
if (is_sat != l_false) {
m_msolver->get_model(m_model);

15
src/opt/maxsmt.h
View file

@ -24,6 +24,9 @@ Notes:
#include"solver.h"
#include"filter_model_converter.h"
#include"statistics.h"
#include"smt_context.h"
#include"smt_theory.h"
#include"theory_wmaxsat.h"
namespace opt {
@ -82,6 +85,18 @@ namespace opt {
expr* mk_not(expr* e);
void set_mus(bool f);
app* mk_fresh_bool(char const* name);
class smt::theory_wmaxsat* get_wmax_theory() const;
smt::theory_wmaxsat* ensure_wmax_theory();
class scoped_ensure_theory {
smt::theory_wmaxsat* m_wth;
public:
scoped_ensure_theory(maxsmt_solver_base& s);
~scoped_ensure_theory();
smt::theory_wmaxsat& operator()();
};
protected:
void enable_sls(expr_ref_vector const& soft, weights_t& ws);
void set_enable_sls(bool f);

5
src/opt/opt_context.cpp
View file

@ -1157,6 +1157,11 @@ namespace opt {
break;
}
}
param_descrs descrs;
collect_param_descrs(descrs);
m_params.display_smt2(out, "opt", descrs);
out << "(check-sat)\n";
return out.str();
}

9
src/opt/opt_params.pyg
View file

@ -10,7 +10,14 @@ def_module_params('opt',
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'),
('elim_01', BOOL, True, 'eliminate 01 variables'),
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)')
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'),
('maxres.max_core_size', UINT, 3, 'break batch of generated cores if size reaches this number'),
('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'),
('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'),
('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds')
))

54
src/opt/wmax.cpp
View file

@ -26,59 +26,15 @@ Notes:
#include "opt_context.h"
namespace opt {
class maxsmt_solver_wbase : public maxsmt_solver_base {
smt::context& ctx;
public:
maxsmt_solver_wbase(context& c,
vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft), ctx(c.smt_context()) {}
~maxsmt_solver_wbase() {}
class scoped_ensure_theory {
smt::theory_wmaxsat* m_wth;
public:
scoped_ensure_theory(maxsmt_solver_wbase& s) {
m_wth = s.ensure_theory();
}
~scoped_ensure_theory() {
m_wth->reset();
}
smt::theory_wmaxsat& operator()() { return *m_wth; }
};
smt::theory_wmaxsat* ensure_theory() {
smt::theory_wmaxsat* wth = get_theory();
if (wth) {
wth->reset();
}
else {
wth = alloc(smt::theory_wmaxsat, m, m_c.fm());
ctx.register_plugin(wth);
}
return wth;
}
smt::theory_wmaxsat* get_theory() const {
smt::theory_id th_id = m.get_family_id("weighted_maxsat");
smt::theory* th = ctx.get_theory(th_id);
if (th) {
return dynamic_cast<smt::theory_wmaxsat*>(th);
}
else {
return 0;
}
}
};
// ----------------------------------------------------------
// weighted max-sat using a custom theory solver for max-sat.
// NB. it is quite similar to pseudo-Boolean propagation.
class wmax : public maxsmt_solver_wbase {
class wmax : public maxsmt_solver_base {
public:
wmax(context& c,
vector<rational> const& ws, expr_ref_vector const& soft):
maxsmt_solver_wbase(c, ws, soft) {}
wmax(context& c, weights_t& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft) {}
virtual ~wmax() {}
lbool operator()() {
@ -90,7 +46,6 @@ namespace opt {
for (unsigned i = 0; i < m_soft.size(); ++i) {
wth().assert_weighted(m_soft[i].get(), m_weights[i]);
}
solver::scoped_push _s2(s());
while (l_true == is_sat) {
is_sat = s().check_sat(0,0);
if (m_cancel) {
@ -122,8 +77,7 @@ namespace opt {
}
};
maxsmt_solver_base* mk_wmax(context& c,
vector<rational> const& ws, expr_ref_vector const& soft) {
maxsmt_solver_base* mk_wmax(context& c, weights_t& ws, expr_ref_vector const& soft) {
return alloc(wmax, c, ws, soft);
}

3
src/opt/wmax.h
View file

@ -23,8 +23,7 @@ Notes:
#include "maxsmt.h"
namespace opt {
maxsmt_solver_base* mk_wmax(context& c,
vector<rational> const& ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_wmax(context& c, weights_t & ws, expr_ref_vector const& soft);
}
#endif

4
src/sat/sat_mus.cpp
View file

@ -31,6 +31,7 @@ namespace sat {
void mus::reset() {
m_core.reset();
m_mus.reset();
m_model.reset();
}
void mus::set_core() {
@ -88,6 +89,9 @@ namespace sat {
if (!core.empty()) {
// mr(); // TBD: measure
}
if (m_model.empty()) {
m_model.append(s.m_model);
}
break;
}
case l_false:

3
src/sat/sat_mus.h
View file

@ -24,6 +24,8 @@ namespace sat {
literal_vector m_core;
literal_vector m_mus;
bool m_is_active;
model m_model; // model obtained during minimal unsat core
solver& s;
public:
@ -31,6 +33,7 @@ namespace sat {
~mus();
lbool operator()();
bool is_active() const { return m_is_active; }
model const& get_model() const { return m_model; }
private:
lbool mus2();
void mr();

2
src/sat/sat_solver.cpp
View file

@ -1736,6 +1736,8 @@ namespace sat {
// initial experiment suggests it has no effect.
m_mus(); // ignore return value on cancelation.
m_model.reset();
m_model.append(m_mus.get_model());
}
}

4
src/smt/theory_wmaxsat.cpp
View file

@ -164,6 +164,10 @@ final_check_status theory_wmaxsat::final_check_eh() {
void theory_wmaxsat::reset_eh() {
theory::reset_eh();
reset_local();
}
void theory_wmaxsat::reset_local() {
m_vars.reset();
m_fmls.reset();
m_rweights.reset();

9
src/smt/theory_wmaxsat.h
View file

@ -17,6 +17,9 @@ Notes:
--*/
#ifndef _THEORY_WMAXSAT_H_
#define _THEORY_WMAXSAT_H_
#include "smt_theory.h"
#include "smt_clause.h"
#include "filter_model_converter.h"
@ -84,9 +87,7 @@ namespace smt {
virtual bool build_models() const {
return false;
}
void reset() {
reset_eh();
}
void reset_local();
virtual void reset_eh();
virtual theory * mk_fresh(context * new_ctx) { return 0; }
virtual bool internalize_atom(app * atom, bool gate_ctx) { return false; }
@ -123,3 +124,5 @@ namespace smt {
};
};
#endif

50
src/util/params.cpp
View file

@ -347,11 +347,11 @@ public:
out << "(params";
svector<params::entry>::const_iterator it = m_entries.begin();
svector<params::entry>::const_iterator end = m_entries.end();
for (; it != end; ++it) {
out << " " << it->first;
for (; it != end; ++it) {
out << " " << it->first;
switch (it->second.m_kind) {
case CPK_BOOL:
out << " " << it->second.m_bool_value;
out << " " << (it->second.m_bool_value?"true":"false");
break;
case CPK_UINT:
out << " " <<it->second.m_uint_value;
@ -376,6 +376,41 @@ public:
out << ")";
}
void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const {
svector<params::entry>::const_iterator it = m_entries.begin();
svector<params::entry>::const_iterator end = m_entries.end();
for (; it != end; ++it) {
if (!descrs.contains(it->first)) continue;
out << "(set-option :";
out << module << ".";
out << it->first;
switch (it->second.m_kind) {
case CPK_BOOL:
out << " " << (it->second.m_bool_value?"true":"false");
break;
case CPK_UINT:
out << " " <<it->second.m_uint_value;
break;
case CPK_DOUBLE:
out << " " << it->second.m_double_value;
break;
case CPK_NUMERAL:
out << " " << *(it->second.m_rat_value);
break;
case CPK_SYMBOL:
out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
break;
case CPK_STRING:
out << " " << it->second.m_str_value;
break;
default:
UNREACHABLE();
break;
}
out << ")\n";
}
}
void display(std::ostream & out, symbol const & k) const {
svector<params::entry>::const_iterator it = m_entries.begin();
svector<params::entry>::const_iterator end = m_entries.end();
@ -423,10 +458,17 @@ params_ref::params_ref(params_ref const & p):
void params_ref::display(std::ostream & out) const {
if (m_params)
m_params->display(out);
else
else
out << "(params)";
}
void params_ref::display_smt2(std::ostream& out, char const* module, param_descrs& descrs) const {
if (m_params)
m_params->display_smt2(out, module, descrs);
}
void params_ref::display(std::ostream & out, char const * k) const {
display(out, symbol(k));
}

1
src/util/params.h
View file

@ -90,6 +90,7 @@ public:
void set_sym(char const * k, symbol const & v);
void display(std::ostream & out) const;
void display_smt2(std::ostream& out, char const* module, param_descrs& module_desc) const;
void validate(param_descrs const & p) const;