mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

invertible_tactic: add support for a few more operations that produce full domain

Browse source
This commit is contained in:
Nuno Lopes 2018-07-04 11:59:01 +01:00
parent e622022bf9
commit 53e582ba22
1 changed files with 77 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

107
src/tactic/core/reduce_invertible_tactic.cpp
View file

@ -168,6 +168,69 @@ private:
if (mc && !(*mc)) *mc = alloc(generic_model_converter, m, "reduce-invertible");
}
bool is_full_domain_var(expr* v, const rational*& model) {
auto f = is_app(v) ? to_app(v)->get_decl() : nullptr;
if (!f || f->get_family_id() != m_bv.get_family_id() || f->get_arity() == 0)
return false;
switch (f->get_decl_kind()) {
case OP_BADD:
case OP_BSUB:
case OP_BSHL:
case OP_BASHR:
case OP_BLSHR:
case OP_BOR:
model = &rational::zero();
return true;
case OP_BAND:
model = &rational::minus_one();
return true;
case OP_BMUL:
case OP_BSDIV:
case OP_BSDIV0:
case OP_BSDIV_I:
case OP_BUDIV:
case OP_BUDIV0:
case OP_BUDIV_I:
model = &rational::one();
return true;
default:
return false;
}
}
bool rewrite_unconstr(expr* v, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var) {
const rational* mdl;
if (!is_full_domain_var(v, mdl))
return false;
app* a = to_app(v);
expr* fst_arg = a->get_arg(0);
bool fst_is_var = is_var(fst_arg);
for (unsigned i = 0, n = a->get_num_args(); i != n; ++i) {
auto arg = a->get_arg(i);
if (!m_parents[arg->get_id()].get() || is_var(arg) != fst_is_var)
return false;
if (fst_is_var && to_var(arg)->get_idx() >= max_var)
return false;
}
if (mc) {
ensure_mc(mc);
expr_ref num(m_bv.mk_numeral(*mdl, get_sort(fst_arg)), m);
for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) {
(*mc)->add(a->get_arg(i), num);
}
}
new_v = fst_arg;
return true;
}
// TBD: could be made to be recursive, by walking multiple layers of parents.
bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) {
@ -176,6 +239,20 @@ private:
if (m_inverted.is_marked(p)) return false;
if (mc && !is_ground(p)) return false;
if (m_bv.is_bv_xor(p) ||
m_bv.is_bv_not(p) ||
m_bv.is_bv_neg(p)) {
if (mc) {
ensure_mc(mc);
(*mc)->add(v, p);
}
new_v = v;
return true;
}
if (rewrite_unconstr(p, new_v, mc, max_var))
return true;
if (m_bv.is_bv_add(p)) {
if (mc) {
ensure_mc(mc);
@ -191,25 +268,6 @@ private:
return true;
}
expr *a, *b;
// shift(a, b), where both a,b are single use. Set b = 0 and return a
if (m_bv.is_bv_shl(p, a, b) ||
m_bv.is_bv_ashr(p, a, b) ||
m_bv.is_bv_lshr(p, a, b)) {
if (!m_parents[(v == a ? b : a)->get_id()].get() || is_var(a) != is_var(b))
return false;
if (is_var(a) && to_var(v == a ? b : a)->get_idx() >= max_var)
return false;
if (mc) {
ensure_mc(mc);
(*mc)->add(b, m_bv.mk_numeral(rational::zero(), get_sort(b)));
}
new_v = a;
return true;
}
if (m_bv.is_bv_mul(p)) {
expr_ref rest(m);
for (expr* arg : *to_app(p)) {
@ -264,20 +322,9 @@ private:
}
return true;
}
if (m_bv.is_bv_xor(p)) {
if (mc) {
ensure_mc(mc);
(*mc)->add(v, p);
}
new_v = v;
return true;
}
if (m_bv.is_bv_sub(p)) {
// TBD
}
if (m_bv.is_bv_neg(p)) {
// TBD
}
if (m_bv.is_bv_udivi(p)) {
// TBD
}