mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

working on incremtal PB theory

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-01-13 10:12:45 -08:00
parent 1f7c994e43
commit 236b2d2ff3
12 changed files with 1419 additions and 912 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/ast/pb_decl_plugin.cpp
View file

@ -23,7 +23,8 @@ pb_decl_plugin::pb_decl_plugin():
m_at_most_sym("at-most"),
m_at_least_sym("at-least"),
m_pble_sym("pble"),
m_pbge_sym("pbge")
m_pbge_sym("pbge"),
m_pbeq_sym("pbeq")
{}
func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -41,6 +42,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
case OP_AT_MOST_K: sym = m_at_most_sym; break;
case OP_PB_LE: sym = m_pble_sym; break;
case OP_PB_GE: sym = m_pbge_sym; break;
case OP_PB_EQ: sym = m_pbeq_sym; break;
default: break;
}
switch(k) {
@ -53,7 +55,8 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
}
case OP_PB_GE:
case OP_PB_LE: {
case OP_PB_LE:
case OP_PB_EQ: {
if (num_parameters != 1 + arity) {
m.raise_exception("function expects arity+1 rational parameters");
}
@ -74,7 +77,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
}
else {
m.raise_exception("function 'pble' expects arity+1 integer parameters");
m.raise_exception("functions 'pble/pbge/pbeq' expect arity+1 integer parameters");
}
}
func_decl_info info(m_family_id, k, num_parameters, params.c_ptr());
@ -89,8 +92,10 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
if (logic == symbol::null) {
op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE));
op_names.push_back(builtin_name(m_pbeq_sym.bare_str(), OP_PB_EQ));
}
}
@ -112,6 +117,15 @@ app * pb_util::mk_ge(unsigned num_args, rational const * coeffs, expr * const *
return m.mk_app(m_fid, OP_PB_GE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
}
app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
vector<parameter> params;
params.push_back(parameter(k));
for (unsigned i = 0; i < num_args; ++i) {
params.push_back(parameter(coeffs[i]));
}
return m.mk_app(m_fid, OP_PB_EQ, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
}
app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
@ -123,7 +137,7 @@ bool pb_util::is_at_most_k(func_decl *a) const {
return is_decl_of(a, m_fid, OP_AT_MOST_K);
}
bool pb_util::is_at_most_k(app *a, rational& k) const {
bool pb_util::is_at_most_k(expr *a, rational& k) const {
if (is_at_most_k(a)) {
k = get_k(a);
return true;
@ -133,7 +147,6 @@ bool pb_util::is_at_most_k(app *a, rational& k) const {
}
}
app * pb_util::mk_at_least_k(unsigned num_args, expr * const * args, unsigned k) {
parameter param(k);
return m.mk_app(m_fid, OP_AT_LEAST_K, 1, &param, num_args, args, m.mk_bool_sort());
@ -143,7 +156,7 @@ bool pb_util::is_at_least_k(func_decl *a) const {
return is_decl_of(a, m_fid, OP_AT_LEAST_K);
}
bool pb_util::is_at_least_k(app *a, rational& k) const {
bool pb_util::is_at_least_k(expr *a, rational& k) const {
if (is_at_least_k(a)) {
k = get_k(a);
return true;
@ -159,7 +172,7 @@ rational pb_util::get_k(func_decl *a) const {
return to_rational(p);
}
else {
SASSERT(is_le(a) || is_ge(a));
SASSERT(is_le(a) || is_ge(a) || is_eq(a));
return to_rational(p);
}
}
@ -169,7 +182,7 @@ bool pb_util::is_le(func_decl *a) const {
return is_decl_of(a, m_fid, OP_PB_LE);
}
bool pb_util::is_le(app* a, rational& k) const {
bool pb_util::is_le(expr* a, rational& k) const {
if (is_le(a)) {
k = get_k(a);
return true;
@ -183,7 +196,7 @@ bool pb_util::is_ge(func_decl *a) const {
return is_decl_of(a, m_fid, OP_PB_GE);
}
bool pb_util::is_ge(app* a, rational& k) const {
bool pb_util::is_ge(expr* a, rational& k) const {
if (is_ge(a)) {
k = get_k(a);
return true;
@ -193,11 +206,26 @@ bool pb_util::is_ge(app* a, rational& k) const {
}
}
bool pb_util::is_eq(func_decl *a) const {
return is_decl_of(a, m_fid, OP_PB_EQ);
}
bool pb_util::is_eq(expr* a, rational& k) const {
if (is_eq(a)) {
k = get_k(a);
return true;
}
else {
return false;
}
}
rational pb_util::get_coeff(func_decl* a, unsigned index) const {
if (is_at_most_k(a) || is_at_least_k(a)) {
return rational::one();
}
SASSERT(is_le(a) || is_ge(a));
SASSERT(is_le(a) || is_ge(a) || is_eq(a));
SASSERT(1 + index < a->get_num_parameters());
return to_rational(a->get_parameter(index + 1));
}

16
src/ast/pb_decl_plugin.h
View file

@ -34,6 +34,7 @@ enum pb_op_kind {
OP_AT_LEAST_K, // at least K Booleans are true.
OP_PB_LE, // pseudo-Boolean <= (generalizes at_most_k)
OP_PB_GE, // pseudo-Boolean >=
OP_PB_EQ, // equality
LAST_PB_OP
};
@ -43,10 +44,12 @@ class pb_decl_plugin : public decl_plugin {
symbol m_at_least_sym;
symbol m_pble_sym;
symbol m_pbge_sym;
symbol m_pbeq_sym;
func_decl * mk_at_most(unsigned arity, unsigned k);
func_decl * mk_at_least(unsigned arity, unsigned k);
func_decl * mk_le(unsigned arity, rational const* coeffs, int k);
func_decl * mk_ge(unsigned arity, rational const* coeffs, int k);
func_decl * mk_eq(unsigned arity, rational const* coeffs, int k);
public:
pb_decl_plugin();
virtual ~pb_decl_plugin() {}
@ -82,22 +85,27 @@ public:
app * mk_at_least_k(unsigned num_args, expr * const * args, unsigned k);
app * mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
app * mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
bool is_at_most_k(func_decl *a) const;
bool is_at_most_k(expr *a) const { return is_app(a) && is_at_most_k(to_app(a)->get_decl()); }
bool is_at_most_k(app *a, rational& k) const;
bool is_at_most_k(expr *a, rational& k) const;
bool is_at_least_k(func_decl *a) const;
bool is_at_least_k(expr *a) const { return is_app(a) && is_at_least_k(to_app(a)->get_decl()); }
bool is_at_least_k(app *a, rational& k) const;
bool is_at_least_k(expr *a, rational& k) const;
rational get_k(func_decl *a) const;
rational get_k(expr *a) const { return get_k(to_app(a)->get_decl()); }
bool is_le(func_decl *a) const;
bool is_le(expr *a) const { return is_app(a) && is_le(to_app(a)->get_decl()); }
bool is_le(app* a, rational& k) const;
bool is_le(expr* a, rational& k) const;
bool is_ge(func_decl* a) const;
bool is_ge(expr* a) const { return is_app(a) && is_ge(to_app(a)->get_decl()); }
bool is_ge(app* a, rational& k) const;
bool is_ge(expr* a, rational& k) const;
rational get_coeff(expr* a, unsigned index) const { return get_coeff(to_app(a)->get_decl(), index); }
rational get_coeff(func_decl* a, unsigned index) const;
bool is_eq(func_decl* f) const;
bool is_eq(expr* e) const { return is_app(e) && is_eq(to_app(e)->get_decl()); }
bool is_eq(expr* e, rational& k) const;
private:
rational to_rational(parameter const& p) const;
};

15
src/ast/rewriter/pb_rewriter.cpp
View file

@ -102,19 +102,21 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
break;
case OP_AT_LEAST_K:
case OP_PB_GE:
case OP_PB_EQ:
break;
default:
UNREACHABLE();
return BR_FAILED;
}
bool is_eq = f->get_decl_kind() == OP_PB_EQ;
pb_ast_rewriter_util pbu(m);
pb_rewriter_util<pb_ast_rewriter_util> util(pbu);
util.unique(vec, k);
lbool is_sat = util.normalize(vec, k);
util.prune(vec, k);
util.unique(vec, k, is_eq);
lbool is_sat = util.normalize(vec, k, is_eq);
util.prune(vec, k, is_eq);
switch (is_sat) {
case l_true:
result = m.mk_true();
@ -129,7 +131,12 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
m_args.push_back(vec[i].first);
m_coeffs.push_back(vec[i].second);
}
result = m_util.mk_ge(vec.size(), m_coeffs.c_ptr(), m_args.c_ptr(), k);
if (is_eq) {
result = m_util.mk_eq(vec.size(), m_coeffs.c_ptr(), m_args.c_ptr(), k);
}
else {
result = m_util.mk_ge(vec.size(), m_coeffs.c_ptr(), m_args.c_ptr(), k);
}
break;
}
TRACE("pb",

8
src/ast/rewriter/pb_rewriter.h
View file

@ -28,12 +28,12 @@ Notes:
template<typename PBU>
class pb_rewriter_util {
PBU& m_util;
void display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k);
void display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
public:
pb_rewriter_util(PBU& u) : m_util(u) {}
void unique(typename PBU::args_t& args, typename PBU::numeral& k);
lbool normalize(typename PBU::args_t& args, typename PBU::numeral& k);
void prune(typename PBU::args_t& args, typename PBU::numeral& k);
void unique(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
lbool normalize(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
void prune(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
};
/**

54
src/ast/rewriter/pb_rewriter_def.h
View file

@ -23,20 +23,20 @@ Notes:
template<typename PBU>
void pb_rewriter_util<PBU>::display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k) {
void pb_rewriter_util<PBU>::display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
for (unsigned i = 0; i < args.size(); ++i) {
out << args[i].second << " * ";
m_util.display(out, args[i].first);
out << " ";
if (i+1 < args.size()) out << "+ ";
}
out << " >= " << k << "\n";
out << (is_eq?" = ":" >= ") << k << "\n";
}
template<typename PBU>
void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::numeral& k) {
void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
TRACE("pb_verbose", display(tout << "pre-unique:", args, k););
TRACE("pb_verbose", display(tout << "pre-unique:", args, k, is_eq););
for (unsigned i = 0; i < args.size(); ++i) {
if (m_util.is_negated(args[i].first)) {
args[i].first = m_util.negate(args[i].first);
@ -85,19 +85,19 @@ void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::num
}
}
args.resize(i);
TRACE("pb_verbose", display(tout << "post-unique:", args, k););
TRACE("pb_verbose", display(tout << "post-unique:", args, k, is_eq););
}
template<typename PBU>
lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU::numeral& k) {
TRACE("pb_verbose", display(tout << "pre-normalize:", args, k););
lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
TRACE("pb_verbose", display(tout << "pre-normalize:", args, k, is_eq););
DEBUG_CODE(
bool found = false;
for (unsigned i = 0; !found && i < args.size(); ++i) {
found = args[i].second.is_zero();
}
if (found) display(verbose_stream(), args, k);
if (found) display(verbose_stream(), args, k, is_eq);
SASSERT(!found););
//
@ -121,17 +121,29 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
sum += args[i].second;
}
// detect tautologies:
if (k <= PBU::numeral::zero()) {
if (!is_eq && k <= PBU::numeral::zero()) {
args.reset();
k = PBU::numeral::zero();
return l_true;
}
if (is_eq && k.is_zero() && args.empty()) {
return l_true;
}
// detect infeasible constraints:
if (sum < k) {
args.reset();
k = PBU::numeral::one();
return l_false;
}
if (is_eq && k == sum) {
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = PBU::numeral::one();
}
k = PBU::numeral::one();
return l_undef;
}
bool all_int = true;
for (unsigned i = 0; all_int && i < args.size(); ++i) {
@ -150,6 +162,11 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
args[i].second *= d;
}
}
if (is_eq) {
TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
return l_undef;
}
// Ensure the largest coefficient is not larger than k:
sum = PBU::numeral::zero();
@ -193,7 +210,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
}
else if (g > PBU::numeral::one()) {
IF_VERBOSE(3, verbose_stream() << "cut " << g << "\n";
display(verbose_stream(), args, k);
display(verbose_stream(), args, k, is_eq);
);
//
@ -241,7 +258,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
PBU::numeral n1 = floor(n0);
PBU::numeral n2 = ceil(k/min) - PBU::numeral::one();
if (n1 == n2 && !n0.is_int()) {
IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k););
IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k, is_eq););
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = PBU::numeral::one();
@ -249,13 +266,15 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
k = n1 + PBU::numeral::one();
}
}
TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
return l_undef;
}
template<typename PBU>
void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::numeral& k) {
void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
if (is_eq) {
return;
}
PBU::numeral nlt(0);
unsigned occ = 0;
for (unsigned i = 0; nlt < k && i < args.size(); ++i) {
@ -264,8 +283,7 @@ void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::nume
++occ;
}
}
if (0 < occ && nlt < k) {
if (0 < occ && nlt < k) {
for (unsigned i = 0; i < args.size(); ++i) {
if (args[i].second < k) {
args[i] = args.back();
@ -273,8 +291,8 @@ void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::nume
--i;
}
}
unique(args, k);
normalize(args, k);
unique(args, k, is_eq);
normalize(args, k, is_eq);
}
}