mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

invertible_tactic: add partial support for shifts

Browse source
This commit is contained in:
Nuno Lopes 2018-07-02 18:29:34 +01:00
parent 648a531950
commit a73d030321
2 changed files with 48 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/bv_decl_plugin.h
View file

@ -354,6 +354,8 @@ public:
MATCH_BINARY(is_bv_mul);
MATCH_BINARY(is_bv_sle);
MATCH_BINARY(is_bv_ule);
MATCH_BINARY(is_bv_ashr);
MATCH_BINARY(is_bv_lshr);
MATCH_BINARY(is_bv_shl);
MATCH_BINARY(is_bv_urem);
MATCH_BINARY(is_bv_srem);

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

@ -30,7 +30,9 @@ Notes:
#include "tactic/core/reduce_invertible_tactic.h"
#include "tactic/core/collect_occs.h"
#include "tactic/generic_model_converter.h"
#include <cstdint>
namespace {
class reduce_invertible_tactic : public tactic {
ast_manager& m;
bv_util m_bv;
@ -60,7 +62,8 @@ public:
generic_model_converter_ref mc;
occs(*g, vars);
expr_safe_replace sub(m);
expr_ref p(m), new_v(m);
expr_ref new_v(m);
expr * p;
for (expr* v : vars) {
if (is_invertible(v, p, new_v, &mc)) {
mark_inverted(p);
@ -75,8 +78,8 @@ public:
expr_ref f_new(m);
sub(f, f_new);
rw(f_new, f_new);
proof_ref new_pr(m);
if (f == f_new) continue;
proof_ref new_pr(m);
if (g->proofs_enabled()) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
@ -120,11 +123,20 @@ private:
}
}
// store up to two parents of expression.
// store one parent of expression, or null if multiple
struct parents {
parents(): m_p1(nullptr), m_p2(nullptr) {}
expr* m_p1;
expr* m_p2;
parents(): m_p(0) {}
uintptr_t m_p;
void set(expr * e) {
SASSERT((uintptr_t)e != 1);
if (!m_p) m_p = (uintptr_t)e;
else m_p = 1;
}
expr * get() const {
return m_p == 1 ? nullptr : (expr*)m_p;
}
};
svector<parents> m_parents;
struct parent_collector {
@ -132,9 +144,8 @@ private:
parent_collector(reduce_invertible_tactic& c):c(c) {}
void operator()(app* n) {
for (expr* arg : *n) {
c.m_parents.reserve(arg->get_id() + 1, parents());
parents& p = c.m_parents[arg->get_id()];
if (!p.m_p1) p.m_p1 = n; else p.m_p2 = n;
c.m_parents.reserve(arg->get_id() + 1);
c.m_parents[arg->get_id()].set(n);
}
}
void operator()(expr*) {}
@ -156,11 +167,13 @@ private:
// TBD: could be made to be recursive, by walking multiple layers of parents.
bool is_invertible(expr* v, expr_ref& p, expr_ref& new_v, generic_model_converter_ref* mc) {
p = m_parents[v->get_id()].m_p1;
if (m_parents[v->get_id()].m_p2 || !p) return false;
bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc) {
p = m_parents[v->get_id()].get();
SASSERT(p);
if (m_inverted.is_marked(p)) return false;
if (mc && !is_ground(p)) return false;
if (m_bv.is_bv_add(p)) {
if (mc) {
ensure_mc(mc);
@ -175,6 +188,24 @@ private:
new_v = v;
return true;
}
expr *a, *b;
// shift(a, b), where both a,b are single use. Set b = 0 and return a
// FIXME: needs to check that both variables are grounded by same quantifier
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())
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)) {
@ -365,7 +396,8 @@ private:
expr_safe_replace sub(m);
t.m_parents.reset();
t.m_inverted.reset();
expr_ref p(m), new_v(m);
expr_ref new_v(m);
expr * p;
{
parent_collector proc(t);
@ -409,11 +441,9 @@ private:
rewriter_tpl<reduce_q_rw_cfg>(t.m, false, m_cfg),
m_cfg(t) {}
};
};
}
tactic * mk_reduce_invertible_tactic(ast_manager & m, params_ref const &) {
return alloc(reduce_invertible_tactic, m);
}