mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-07-03 09:28:27 -07:00
parent 4359d518a9 cd482c683e
commit f00264663c
1 changed files with 14 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -94,8 +94,6 @@ public:
void cleanup() override {}
private:
void checkpoint() {
if (m.canceled())
throw tactic_exception(m.limit().get_cancel_msg());
@ -148,7 +146,12 @@ private:
c.m_parents[arg->get_id()].set(n);
}
}
void operator()(expr*) {}
void operator()(var* v) {
c.m_parents.reserve(v->get_id() + 1);
}
void operator()(quantifier* q) {}
};
void collect_parents(goal_ref const& g) {
@ -167,10 +170,9 @@ private:
// 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) {
bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) {
p = m_parents[v->get_id()].get();
SASSERT(p);
if (!p) return false;
if (m_inverted.is_marked(p)) return false;
if (mc && !is_ground(p)) return false;
@ -191,11 +193,13 @@ private:
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())
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) {
@ -390,7 +394,7 @@ private:
new_sorts.push_back(srt);
}
// for each variable, collect parents,
// ensure they are in uniqe location and not under other quantifiers.
// ensure they are in unique location and not under other quantifiers.
// if they are invertible, then produce inverting expression.
//
expr_safe_replace sub(m);
@ -407,7 +411,7 @@ private:
bool has_new_var = false;
for (unsigned i = 0; i < vars.size(); ++i) {
var* v = vars[i];
if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, new_v, nullptr)) {
if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, new_v, nullptr, vars.size())) {
t.mark_inverted(p);
sub.insert(p, new_v);
new_sorts[i] = m.get_sort(new_v);