mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

tuning pb/max

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-06 04:01:10 -07:00
parent 7ade3f2c04
commit d2db8007d8
9 changed files with 79 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/ast/pb_decl_plugin.cpp
View file

@ -126,6 +126,40 @@ app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const *
return m.mk_app(m_fid, OP_PB_EQ, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
}
// ax + by < k
// <=>
// -ax - by >= -k + 1
// <=>
// a(1-x) + b(1-y) >= -k + a + b + 1
app * pb_util::mk_lt(unsigned num_args, rational const * _coeffs, expr * const * _args, rational const& _k) {
vector<rational> coeffs;
rational k(_k);
expr_ref_vector args(m);
expr* f;
rational d(denominator(k));
for (unsigned i = 0; i < num_args; ++i) {
coeffs.push_back(_coeffs[i]);
d = lcm(d, denominator(coeffs[i]));
if (m.is_not(_args[i], f)) {
args.push_back(f);
}
else {
args.push_back(m.mk_not(f));
}
}
if (!d.is_one()) {
k *= d;
for (unsigned i = 0; i < num_args; ++i) {
coeffs[i] *= d;
}
}
k.neg();
k += rational::one();
for (unsigned i = 0; i < num_args; ++i) {
k += coeffs[i];
}
return mk_ge(num_args, coeffs.c_ptr(), args.c_ptr(), k);
}
app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {

3
src/ast/pb_decl_plugin.h
View file

@ -86,6 +86,7 @@ public:
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);
app * mk_lt(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(expr *a, rational& k) const;
@ -106,6 +107,8 @@ public:
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;
};