mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 18:15:32 +00:00
Code Activity

removing dependency on simplifier in pattern_inference

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-23 12:17:30 -07:00
parent e5826b957f
commit 655b3d9c19
8 changed files with 861 additions and 167 deletions
Download patch file Download diff file Expand all files Collapse all files

98
src/ast/macros/macro_manager.cpp
View file

@ -298,104 +298,6 @@ struct macro_manager::macro_expander_rw : public rewriter_tpl<macro_manager::mac
{}
};
macro_manager::macro_expander::macro_expander(ast_manager & m, macro_manager & mm):
simplifier(m),
m_macro_manager(mm) {
// REMARK: theory simplifier should not be used by macro_expander...
// is_arith_macro rewrites a quantifer such as:
// forall (x Int) (= (+ x (+ (f x) 1)) 2)
// into
// forall (x Int) (= (f x) (+ 1 (* -1 x)))
// The goal is to make simple macro detection detect the arith macro.
// The arith simplifier will undo this transformation.
// borrow_plugins(s);
enable_ac_support(false);
}
macro_manager::macro_expander::~macro_expander() {
// release_plugins();
}
void macro_manager::macro_expander::reduce1_quantifier(quantifier * q) {
simplifier::reduce1_quantifier(q);
// If a macro was expanded in a pattern, we must erase it since it may not be a valid pattern anymore.
// The MAM assumes valid patterns, and it crashes if invalid patterns are provided.
// For example, it will crash if the pattern does not contain all variables.
//
// Alternative solution: use pattern_validation to check if the pattern is still valid.
// I'm not sure if this is a good solution, since the pattern may be meaningless after the macro expansion.
// So, I'm just erasing them.
expr * new_q_expr = 0;
proof * new_q_pr = 0;
get_cached(q, new_q_expr, new_q_pr);
if (!is_quantifier(new_q_expr))
return;
quantifier * new_q = to_quantifier(new_q_expr);
bool erase_patterns = false;
if (q->get_num_patterns() != new_q->get_num_patterns() ||
q->get_num_no_patterns() != new_q->get_num_no_patterns()) {
erase_patterns = true;
}
else {
for (unsigned i = 0; !erase_patterns && i < q->get_num_patterns(); i++) {
if (q->get_pattern(i) != new_q->get_pattern(i))
erase_patterns = true;
}
for (unsigned i = 0; !erase_patterns && i < q->get_num_no_patterns(); i++) {
if (q->get_no_pattern(i) != new_q->get_no_pattern(i))
erase_patterns = true;
}
}
if (erase_patterns) {
ast_manager & m = get_manager();
expr * new_new_q = m.update_quantifier(new_q, 0, 0, 0, 0, new_q->get_expr());
// we can use the same proof since new_new_q and new_q are identical modulo patterns/annotations
cache_result(q, new_new_q, new_q_pr);
}
}
bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref & p) {
if (!is_app(_n))
return false;
app * n = to_app(_n);
quantifier * q = 0;
func_decl * d = n->get_decl();
TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
if (m_macro_manager.m_decl2macro.find(d, q)) {
TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
app * head = 0;
expr * def = 0;
m_macro_manager.get_head_def(q, d, head, def);
unsigned num = n->get_num_args();
SASSERT(head && def);
ptr_buffer<expr> subst_args;
subst_args.resize(num, 0);
for (unsigned i = 0; i < num; i++) {
var * v = to_var(head->get_arg(i));
SASSERT(v->get_idx() < num);
unsigned nidx = num - v->get_idx() - 1;
SASSERT(subst_args[nidx] == 0);
subst_args[nidx] = n->get_arg(i);
}
var_subst s(m);
s(def, num, subst_args.c_ptr(), r);
if (m.proofs_enabled()) {
expr_ref instance(m);
s(q->get_expr(), num, subst_args.c_ptr(), instance);
proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr());
proof * q_pr = 0;
m_macro_manager.m_decl2macro_pr.find(d, q_pr);
SASSERT(q_pr != 0);
proof * prs[2] = { qi_pr, q_pr };
p = m.mk_unit_resolution(2, prs);
}
else {
p = 0;
}
return true;
}
return false;
}
void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr) {
if (has_macros()) {

11
src/ast/macros/macro_manager.h
View file

@ -60,17 +60,6 @@ class macro_manager {
struct macro_expander_cfg;
struct macro_expander_rw;
class macro_expander : public simplifier {
protected:
macro_manager & m_macro_manager;
virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
virtual void reduce1_quantifier(quantifier * q);
public:
macro_expander(ast_manager & m, macro_manager & mm);
~macro_expander();
};
friend class macro_expander;
public:
macro_manager(ast_manager & m);
~macro_manager();