mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
add bvsls module as backend to weighted maxsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
a26e299390
commit
3d7f208ce6
|
|
@ -431,7 +431,6 @@ protected:
|
|||
ast_manager& m_manager;
|
||||
|
||||
dlexer* m_lexer;
|
||||
ast_ref_vector m_pinned;
|
||||
region m_region;
|
||||
dl_decl_util & m_decl_util;
|
||||
arith_util m_arith;
|
||||
|
|
@ -450,7 +449,6 @@ public:
|
|||
dparser(context& ctx, ast_manager& m):
|
||||
m_context(ctx),
|
||||
m_manager(m),
|
||||
m_pinned(m),
|
||||
m_decl_util(ctx.get_decl_util()),
|
||||
m_arith(m),
|
||||
m_num_vars(0),
|
||||
|
|
@ -486,7 +484,6 @@ protected:
|
|||
void reset() {
|
||||
m_num_vars = 0;
|
||||
m_sym_idx = 0;
|
||||
m_pinned.reset();
|
||||
m_vars.reset();
|
||||
m_region.reset();
|
||||
m_path.clear();
|
||||
|
|
@ -741,7 +738,7 @@ protected:
|
|||
//
|
||||
dtoken parse_infix(dtoken tok1, char const* td, app_ref& pred) {
|
||||
symbol td1(td);
|
||||
expr* v1 = 0, *v2 = 0;
|
||||
expr_ref v1(m_manager), v2(m_manager);
|
||||
sort* s = 0;
|
||||
dtoken tok2 = m_lexer->next_token();
|
||||
if (tok2 != TK_NEQ && tok2 != TK_GT && tok2 != TK_LT && tok2 != TK_EQ) {
|
||||
|
|
@ -755,12 +752,16 @@ protected:
|
|||
symbol td2(td);
|
||||
|
||||
if (tok1 == TK_ID) {
|
||||
m_vars.find(td1.bare_str(), v1);
|
||||
expr* _v1 = 0;
|
||||
m_vars.find(td1.bare_str(), _v1);
|
||||
v1 = _v1;
|
||||
}
|
||||
if (tok3 == TK_ID) {
|
||||
m_vars.find(td2.bare_str(), v2);
|
||||
expr* _v2 = 0;
|
||||
m_vars.find(td2.bare_str(), _v2);
|
||||
v2 = _v2;
|
||||
}
|
||||
if (v1 == 0 && v2 == 0) {
|
||||
if (!v1 && !v2) {
|
||||
return unexpected(tok3, "at least one argument should be a variable");
|
||||
}
|
||||
if (v1) {
|
||||
|
|
@ -1018,10 +1019,6 @@ protected:
|
|||
}
|
||||
|
||||
void add_rule(app* head, unsigned sz, app* const* body, const bool * is_neg) {
|
||||
m_pinned.push_back(head);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
m_pinned.push_back(body[i]);
|
||||
}
|
||||
rule_manager& m = m_context.get_rule_manager();
|
||||
|
||||
if(sz==0 && m.is_fact(head)) {
|
||||
|
|
@ -1075,7 +1072,6 @@ protected:
|
|||
unsigned idx = m_context.get_constant_number(s, name);
|
||||
res = m_decl_util.mk_numeral(idx, s);
|
||||
}
|
||||
m_pinned.push_back(res);
|
||||
return res;
|
||||
}
|
||||
/**
|
||||
|
|
@ -1090,13 +1086,11 @@ protected:
|
|||
unsigned idx = m_context.get_constant_number(s, symbol(to_string(el).c_str()));
|
||||
res = m_decl_util.mk_numeral(idx, s);
|
||||
}
|
||||
m_pinned.push_back(res);
|
||||
return res;
|
||||
}
|
||||
app* mk_const(uint64 el, sort* s) {
|
||||
unsigned idx = m_context.get_constant_number(s, el);
|
||||
app * res = m_decl_util.mk_numeral(idx, s);
|
||||
m_pinned.push_back(res);
|
||||
return res;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -33,6 +33,7 @@ Notes:
|
|||
#include "qfbv_tactic.h"
|
||||
#include "card2bv_tactic.h"
|
||||
#include "tactic2solver.h"
|
||||
#include "bvsls_opt_engine.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
@ -463,11 +464,14 @@ namespace opt {
|
|||
ref<solver> m_sat_solver;
|
||||
scoped_ptr<imp> m_imp;
|
||||
smt::pb_sls m_sls;
|
||||
bvsls_opt_engine m_bvsls;
|
||||
|
||||
|
||||
imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft_constraints, vector<rational> const& weights):
|
||||
m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_print_all_models(false), m_cancel(false),
|
||||
m_solver(m, m_params, symbol("bound")),
|
||||
m_sls(m)
|
||||
m_sls(m),
|
||||
m_bvsls(m, m_params)
|
||||
{
|
||||
m_assignment.resize(m_soft.size(), false);
|
||||
}
|
||||
|
|
@ -534,6 +538,9 @@ namespace opt {
|
|||
if (m_engine == symbol("sls")) {
|
||||
return sls_solve();
|
||||
}
|
||||
if (m_engine == symbol("bvsls")) {
|
||||
return bvsls_solve();
|
||||
}
|
||||
if (m_engine == symbol::null || m_engine == symbol("wmax")) {
|
||||
return incremental_solve();
|
||||
}
|
||||
|
|
@ -687,6 +694,57 @@ namespace opt {
|
|||
return is_sat;
|
||||
}
|
||||
|
||||
lbool bvsls_solve() {
|
||||
IF_VERBOSE(1, verbose_stream() << "(bvsls solve)\n";);
|
||||
|
||||
bv_util bv(m);
|
||||
pb::card_pb_rewriter pb_rewriter(m);
|
||||
expr_ref tmp(m), objective(m), zero(m);
|
||||
expr_ref_vector es(m);
|
||||
|
||||
for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
|
||||
pb_rewriter(s.get_assertion(i), tmp);
|
||||
m_bvsls.assert_expr(tmp);
|
||||
}
|
||||
|
||||
m_lower = m_upper = rational::zero();
|
||||
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_upper += m_weights[i];
|
||||
}
|
||||
rational num = numerator(m_upper);
|
||||
rational den = denominator(m_upper);
|
||||
rational maxval = num*den;
|
||||
unsigned bv_size = maxval.get_num_bits();
|
||||
zero = bv.mk_numeral(rational(0), bv_size);
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
es.push_back(m.mk_ite(m_soft[i].get(), bv.mk_numeral(den*m_weights[i], bv_size), zero));
|
||||
}
|
||||
if (es.empty()) {
|
||||
objective = bv.mk_numeral(0, bv_size);
|
||||
}
|
||||
else {
|
||||
objective = es[0].get();
|
||||
for (unsigned i = 1; i < es.size(); ++i) {
|
||||
objective = bv.mk_bv_add(objective, es[i].get());
|
||||
}
|
||||
}
|
||||
// TBD: can we set an initial model on m_bvsls?
|
||||
bvsls_opt_engine::optimization_result res = m_bvsls.optimize(objective);
|
||||
switch(res.is_sat) {
|
||||
case l_true: {
|
||||
unsigned bv_size = 0;
|
||||
// TBD: m_bvsls.get_model(m_model);
|
||||
VERIFY(bv.is_numeral(res.optimum, m_lower, bv_size));
|
||||
break;
|
||||
}
|
||||
case l_false:
|
||||
case l_undef:
|
||||
break;
|
||||
}
|
||||
return res.is_sat;
|
||||
}
|
||||
|
||||
/**
|
||||
Iteratively increase cost until there is an assignment during
|
||||
final_check that satisfies min_cost.
|
||||
|
|
|
|||
|
|
@ -19,19 +19,12 @@ Notes:
|
|||
#include"tactical.h"
|
||||
#include"cooperate.h"
|
||||
#include"rewriter_def.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
#include"expr_substitution.h"
|
||||
#include"card2bv_tactic.h"
|
||||
#include"pb_decl_plugin.h"
|
||||
|
||||
class card2bv_rewriter {
|
||||
ast_manager& m;
|
||||
arith_util au;
|
||||
pb_util pb;
|
||||
bv_util bv;
|
||||
|
||||
unsigned get_num_bits(func_decl* f) {
|
||||
namespace pb {
|
||||
unsigned card2bv_rewriter::get_num_bits(func_decl* f) {
|
||||
rational r(0);
|
||||
unsigned sz = f->get_arity();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
|
|
@ -40,16 +33,15 @@ class card2bv_rewriter {
|
|||
r = r > pb.get_k(f)? r : pb.get_k(f);
|
||||
return r.get_num_bits();
|
||||
}
|
||||
|
||||
public:
|
||||
card2bv_rewriter(ast_manager& m):
|
||||
|
||||
card2bv_rewriter::card2bv_rewriter(ast_manager& m):
|
||||
m(m),
|
||||
au(m),
|
||||
pb(m),
|
||||
bv(m)
|
||||
{}
|
||||
|
||||
br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
|
||||
|
||||
br_status card2bv_rewriter::mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
|
||||
if (f->get_family_id() == null_family_id) {
|
||||
if (sz == 1) {
|
||||
// Expecting minimize/maximize.
|
||||
|
|
@ -84,7 +76,7 @@ public:
|
|||
break;
|
||||
}
|
||||
b = bv.mk_numeral(pb.get_k(f), bw);
|
||||
|
||||
|
||||
switch (f->get_decl_kind()) {
|
||||
case OP_AT_MOST_K:
|
||||
case OP_PB_LE:
|
||||
|
|
@ -104,8 +96,11 @@ public:
|
|||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
else if (f->get_family_id() == au.get_family_id())
|
||||
{
|
||||
// NSB: review
|
||||
// we should remove this code and rely on a layer above to deal with
|
||||
// whatever it accomplishes. It seems to break types.
|
||||
//
|
||||
else if (f->get_family_id() == au.get_family_id()) {
|
||||
if (f->get_decl_kind() == OP_ADD) {
|
||||
bool all_ite_01 = true;
|
||||
unsigned bits = 0;
|
||||
|
|
@ -122,7 +117,7 @@ public:
|
|||
else
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
||||
result = 0;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
rational val1, val2;
|
||||
|
|
@ -141,34 +136,15 @@ public:
|
|||
else
|
||||
return BR_FAILED;
|
||||
}
|
||||
};
|
||||
|
||||
struct card2bv_rewriter_cfg : public default_rewriter_cfg {
|
||||
card2bv_rewriter m_r;
|
||||
bool rewrite_patterns() const { return false; }
|
||||
bool flat_assoc(func_decl * f) const { return false; }
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
result_pr = 0;
|
||||
return m_r.mk_app_core(f, num, args, result);
|
||||
}
|
||||
card2bv_rewriter_cfg(ast_manager & m):m_r(m) {}
|
||||
};
|
||||
|
||||
template class rewriter_tpl<card2bv_rewriter_cfg>;
|
||||
|
||||
class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
|
||||
card2bv_rewriter_cfg m_cfg;
|
||||
public:
|
||||
card_pb_rewriter(ast_manager & m):
|
||||
rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
|
||||
m_cfg(m) {}
|
||||
template class rewriter_tpl<card2bv_rewriter_cfg>;
|
||||
};
|
||||
|
||||
class card2bv_tactic : public tactic {
|
||||
ast_manager & m;
|
||||
params_ref m_params;
|
||||
th_rewriter m_rw1;
|
||||
card_pb_rewriter m_rw2;
|
||||
pb::card_pb_rewriter m_rw2;
|
||||
|
||||
public:
|
||||
|
||||
|
|
|
|||
|
|
@ -20,9 +20,46 @@ Notes:
|
|||
#define _CARD2BV_TACTIC_
|
||||
|
||||
#include"params.h"
|
||||
#include"pb_decl_plugin.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"rewriter.h"
|
||||
|
||||
class ast_manager;
|
||||
class tactic;
|
||||
|
||||
namespace pb {
|
||||
|
||||
class card2bv_rewriter {
|
||||
ast_manager& m;
|
||||
arith_util au;
|
||||
pb_util pb;
|
||||
bv_util bv;
|
||||
unsigned get_num_bits(func_decl* f);
|
||||
public:
|
||||
card2bv_rewriter(ast_manager& m);
|
||||
br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result);
|
||||
};
|
||||
|
||||
struct card2bv_rewriter_cfg : public default_rewriter_cfg {
|
||||
card2bv_rewriter m_r;
|
||||
bool rewrite_patterns() const { return false; }
|
||||
bool flat_assoc(func_decl * f) const { return false; }
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
result_pr = 0;
|
||||
return m_r.mk_app_core(f, num, args, result);
|
||||
}
|
||||
card2bv_rewriter_cfg(ast_manager & m):m_r(m) {}
|
||||
};
|
||||
|
||||
class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
|
||||
card2bv_rewriter_cfg m_cfg;
|
||||
public:
|
||||
card_pb_rewriter(ast_manager & m):
|
||||
rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
|
||||
m_cfg(m) {}
|
||||
};
|
||||
};
|
||||
|
||||
tactic * mk_card2bv_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "mk_card2bv_tactic(m, p)")
|
||||
|
|
|
|||
3380
tests/chat_sls.smt2
Normal file
3380
tests/chat_sls.smt2
Normal file
File diff suppressed because it is too large
Load diff
Loading…
Reference in a new issue