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

neatify rewriting

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-03 16:33:14 -08:00
parent d07688d80b
commit badb32f9ae
3 changed files with 24 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/pb_decl_plugin.cpp
View file

@ -129,9 +129,15 @@ app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const *
normalize(num_args, coeffs, k);
m_params.reset();
m_params.push_back(parameter(floor(m_k)));
bool all_ones = true;
for (unsigned i = 0; i < num_args; ++i) {
all_ones &= m_coeffs[i].is_one();
m_params.push_back(parameter(m_coeffs[i]));
}
if (all_ones && k.is_unsigned()) {
m_params[0] = parameter(floor(m_k).get_unsigned());
return m.mk_app(m_fid, OP_AT_MOST_K, 1, m_params.c_ptr(), num_args, args, m.mk_bool_sort());
}
return m.mk_app(m_fid, OP_PB_LE, m_params.size(), m_params.c_ptr(), num_args, args, m.mk_bool_sort());
}
@ -139,9 +145,15 @@ app * pb_util::mk_ge(unsigned num_args, rational const * coeffs, expr * const *
normalize(num_args, coeffs, k);
m_params.reset();
m_params.push_back(parameter(ceil(m_k)));
bool all_ones = true;
for (unsigned i = 0; i < num_args; ++i) {
all_ones &= m_coeffs[i].is_one();
m_params.push_back(parameter(m_coeffs[i]));
}
if (all_ones && k.is_unsigned()) {
m_params[0] = parameter(ceil(m_k).get_unsigned());
return m.mk_app(m_fid, OP_AT_LEAST_K, 1, m_params.c_ptr(), num_args, args, m.mk_bool_sort());
}
return m.mk_app(m_fid, OP_PB_GE, m_params.size(), m_params.c_ptr(), num_args, args, m.mk_bool_sort());
}

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

@ -115,14 +115,15 @@ expr_ref pb_rewriter::translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml) {
else {
tmp = a.mk_add(es.size(), es.c_ptr());
}
rational k = util.get_k(fml);
if (util.is_le(fml)) {
result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
result = a.mk_le(tmp, a.mk_numeral(k, false));
}
else if (util.is_ge(fml)) {
result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
result = a.mk_ge(tmp, a.mk_numeral(k, false));
}
else {
result = m().mk_eq(tmp, a.mk_numeral(util.get_k(fml), false));
result = m().mk_eq(tmp, a.mk_numeral(k, false));
}
}
else {
@ -265,6 +266,12 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
if (sz == 0) {
result = k.is_zero()?m.mk_true():m.mk_false();
}
else if (k.is_zero()) {
result = mk_not(m, mk_or(m, sz, m_args.c_ptr()));
}
else if (k.is_one() && all_unit && m_args.size() == 1) {
result = m_args.back();
}
else {
result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
}

4
src/tactic/arith/lia2card_tactic.cpp
View file

@ -158,7 +158,7 @@ public:
m_rw(*this),
m_pb(m),
m_todo(alloc(ptr_vector<expr>)),
m_compile_equality(false) {
m_compile_equality(true) {
m_max_ub = 100;
}
@ -168,7 +168,7 @@ public:
void updt_params(params_ref const & p) {
m_params = p;
m_compile_equality = p.get_bool("compile_equality", false);
m_compile_equality = p.get_bool("compile_equality", true);
}
expr_ref mk_bounded(expr_ref_vector& axioms, app* x, unsigned lo, unsigned hi) {