Skip to content

Commit

Permalink
add quasi macro detection
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jan 7, 2023
1 parent 25112e4 commit 95cb06d
Show file tree
Hide file tree
Showing 3 changed files with 170 additions and 5 deletions.
168 changes: 164 additions & 4 deletions src/ast/simplifiers/eliminate_predicates.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,8 @@ bool eliminate_predicates::can_be_macro_head(expr* _head, unsigned num_bound) {
return false;
if (f->is_associative())
return false;
if (!is_uninterp(f))
return false;
uint_set indices;
for (expr* arg : *head) {
if (!is_var(arg))
Expand Down Expand Up @@ -146,8 +148,14 @@ bool eliminate_predicates::can_be_quasi_macro_head(expr* _head, unsigned num_bou
return false;
if (f->is_associative())
return false;
if (!is_uninterp(f))
return false;
uint_set indices;
for (expr* arg : *head) {
if (occurs(f, arg))
return false;
if (!is_macro_safe(arg))
return false;
if (!is_var(arg))
continue;
unsigned idx = to_var(arg)->get_idx();
Expand All @@ -161,6 +169,49 @@ bool eliminate_predicates::can_be_quasi_macro_head(expr* _head, unsigned num_bou
}


//
// (= (f x y (+ x y)) s), where x y are all bound variables.
// then replace (f x y z) by (if (= z (+ x y)) s (f' x y z))
//

void eliminate_predicates::insert_quasi_macro(app* head, expr* body, clause const& cl) {
expr_ref _body(body, m);
uint_set indices;
expr_ref_vector args(m), eqs(m);
var_ref new_var(m);
app_ref lhs(m), rhs(m);
func_decl_ref f1(m);
sort_ref_vector sorts(m);
svector<symbol> names;

unsigned num_decls = cl.m_bound.size();
func_decl* f = head->get_decl();

for (expr* arg : *head) {
sorts.push_back(arg->get_sort());
names.push_back(symbol(std::string("x") + std::to_string(args.size())));
if (is_var(arg)) {
unsigned idx = to_var(arg)->get_idx();
if (!indices.contains(idx)) {
indices.insert(idx);
args.push_back(arg);
continue;
}
}
new_var = m.mk_var(eqs.size() + num_decls, arg->get_sort());
args.push_back(new_var);
eqs.push_back(m.mk_eq(arg, new_var));
}

// forall vars . f(args) = if eqs then body else f'(args)
f1 = m.mk_fresh_func_decl(f->get_name(), symbol::null, sorts.size(), sorts.data(), f->get_range());
lhs = m.mk_app(f, args);
rhs = m.mk_ite(mk_and(eqs), body, m.mk_app(f1, args));
insert_macro(lhs, rhs, cl.m_dep);
}



expr_ref eliminate_predicates::bind_free_variables_in_def(clause& cl, app* head, expr* def) {
unsigned num_bound = cl.m_bound.size();
if (head->get_num_args() == num_bound)
Expand Down Expand Up @@ -208,7 +259,7 @@ bool eliminate_predicates::try_find_binary_definition(func_decl* p, app_ref& hea
};

for (auto* cl : m_use_list.get(p, false)) {
if (cl->m_alive && cl->m_literals.size() == 2) {
if (cl->m_alive && cl->size() == 2) {
auto const& [atom1, sign1] = cl->m_literals[0];
auto const& [atom2, sign2] = cl->m_literals[1];
add_def(*cl, atom1, sign1, atom2, sign2);
Expand Down Expand Up @@ -242,7 +293,7 @@ bool eliminate_predicates::try_find_binary_definition(func_decl* p, app_ref& hea
};

for (auto* cl : m_use_list.get(p, true)) {
if (cl->m_alive && cl->m_literals.size() == 2) {
if (cl->m_alive && cl->size() == 2) {
if (is_def(0, 1, *cl))
return true;
if (is_def(1, 0, *cl))
Expand Down Expand Up @@ -507,10 +558,45 @@ void eliminate_predicates::try_find_macro(clause& cl) {
//

//
// To review: quasi-macros
// quasi-macros
// (= (f x y (+ x y)) s), where x y are all bound variables.
// then replace (f x y z) by (if (= z (+ x y)) s (f' x y))
// then replace (f x y z) by (if (= z (+ x y)) s (f' x y z))
//
auto can_be_qdef = [&](expr* _x, expr* y) {
if (!is_app(_x))
return false;
app* x = to_app(_x);
return
can_be_quasi_macro_head(x, cl.m_bound.size()) &&
is_macro_safe(y) &&
!occurs(x->get_decl(), y);
};

if (cl.is_unit() && m.is_eq(cl.atom(0), x, y)) {
if (!cl.sign(0) && can_be_qdef(x, y)) {
insert_quasi_macro(to_app(x), y, cl);
return;
}
else if (!cl.sign(0) && can_be_qdef(y, x)) {
insert_quasi_macro(to_app(y), x, cl);
return;
}
else if (cl.sign(0) && m.is_bool(y) && can_be_qdef(x, y)) {
insert_quasi_macro(to_app(x), m.mk_not(y), cl);
return;
}
else if (cl.sign(0) && m.is_bool(y) && can_be_qdef(y, x)) {
insert_quasi_macro(to_app(y), m.mk_not(x), cl);
return;
}
}
if (cl.is_unit()) {
expr* body = cl.sign(0) ? m.mk_false() : m.mk_true();
if (can_be_qdef(cl.atom(0), body)) {
insert_quasi_macro(to_app(x), body, cl);
return;
}
}
}


Expand Down Expand Up @@ -791,6 +877,11 @@ eliminate_predicates::clause* eliminate_predicates::init_clause(expr* f, expr_de
bool sign = m.is_not(lit, lit);
cl->m_literals.push_back({ expr_ref(lit, m), sign });
}

// extend macro detection to exploit bijective functions?
// f(+ x 1) = g(x) -> f(x) = g(- x 1)
// init_injective(*cl);
// init_surjective(*cl);
return cl;
}

Expand All @@ -811,6 +902,73 @@ void eliminate_predicates::init_clauses() {
process_to_exclude(m_disable_elimination);
}

/**
* Ad hoc recognize surjectivity axioms
* - exists y . f(y) = x
*/
void eliminate_predicates::init_surjective(clause const& cl) {
if (!cl.is_unit())
return;
if (cl.sign(0))
return;
if (!is_exists(cl.atom(0)))
return;
}

/**
* Ad hoc recognize injectivity axioms
* - f(x) = f(y) => x = y
*/
void eliminate_predicates::init_injective(clause const& cl) {
if (cl.size() != 2)
return;
if (cl.m_bound.size() != 2)
return;
if (cl.sign(0) == cl.sign(1))
return;
expr* a = cl.atom(0), *b = cl.atom(1);
if (!cl.sign(0) && cl.sign(1))
std::swap(a, b);
expr* x, *y, *fx, *fy;
if (!m.is_eq(a, fx, fy))
return;
if (!m.is_eq(b, x, y))
return;

auto is_fx = [&](expr* _fx, func_decl*& f, unsigned& idx) {
if (!is_app(_fx))
return false;
app* fx = to_app(_fx);
if (fx->get_num_args() != 1)
return false;
if (!is_var(fx->get_arg(0)))
return false;
f = fx->get_decl();
idx = to_var(fx->get_arg(0))->get_idx();
return true;
};
func_decl* f1, *f2;
unsigned idx1, idx2;
if (!is_fx(fx, f1, idx1))
return;
if (!is_fx(fy, f2, idx2))
return;
if (idx1 == idx2 || f1 != f2)
return;

auto check_var = [&](expr* x, unsigned& idx) {
if (!is_var(x))
return false;
idx = to_var(x)->get_idx();
return true;
};
if (!check_var(x, idx1) || !check_var(y, idx2))
return;
if (idx1 == idx2)
return;
m_is_injective.mark(f1, true);
}

/**
* Convert clauses to m_fmls
*/
Expand Down Expand Up @@ -838,6 +996,8 @@ void eliminate_predicates::reset() {
m_to_exclude.reset();
m_disable_elimination.reset();
m_is_macro.reset();
m_is_injective.reset();
m_is_surjective.reset();
for (auto const& [k, v] : m_macros)
dealloc(v);
m_macros.reset();
Expand Down
5 changes: 5 additions & 0 deletions src/ast/simplifiers/eliminate_predicates.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ class eliminate_predicates : public dependent_expr_simplifier {

std::ostream& display(std::ostream& out) const;

unsigned size() const { return m_literals.size(); }
expr* atom(unsigned i) const { return m_literals[i].first; }
bool sign(unsigned i) const { return m_literals[i].second; }
bool is_unit() const { return m_literals.size() == 1; }
Expand Down Expand Up @@ -91,6 +92,7 @@ class eliminate_predicates : public dependent_expr_simplifier {
ast_mark m_disable_elimination, m_predicate_decls, m_is_macro;
ptr_vector<func_decl> m_predicates;
ptr_vector<expr> m_to_exclude;
ast_mark m_is_injective, m_is_surjective;
stats m_stats;
use_list m_use_list;
der_rewriter m_der;
Expand All @@ -101,6 +103,8 @@ class eliminate_predicates : public dependent_expr_simplifier {

clause* init_clause(unsigned i);
clause* init_clause(expr* f, expr_dependency* d, unsigned i);
void init_injective(clause const& cl);
void init_surjective(clause const& cl);
clause* resolve(func_decl* p, clause& pos, clause& neg);
void add_use_list(clause& cl);

Expand All @@ -109,6 +113,7 @@ class eliminate_predicates : public dependent_expr_simplifier {
void insert_macro(app* head, expr* def, expr_dependency* dep);
expr_ref bind_free_variables_in_def(clause& cl, app* head, expr* def);
bool can_be_macro_head(expr* head, unsigned num_bound);
void insert_quasi_macro(app* head, expr* body, clause const& cl);
bool can_be_quasi_macro_head(expr* head, unsigned num_bound);
bool is_macro_safe(expr* e);
void try_find_macro(clause& cl);
Expand Down
2 changes: 1 addition & 1 deletion src/tactic/arith/degree_shift_tactic.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ Then, replace $x^n$ with a new fresh variable $y$.
```z3
(declare-const x Real)
(declare-const y Real)
(assert (> (+ (* x x x 4) (* x x 3) 0)))
(assert (> (+ (* x x x 4) (* x x 3)) 0))
(assert (= (* x x) (* y y)))
(apply degree-shift)
```
Expand Down

0 comments on commit 95cb06d

Please sign in to comment.