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

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-08-25 15:23:25 +01:00
parent 36dd2b6530
commit 3e0926fb82
1 changed files with 37 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

74
src/ast/macros/quasi_macros.cpp
View file

@ -31,7 +31,7 @@ quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s)
m_new_qsorts(m) { m_new_qsorts(m) {
} }
quasi_macros::~quasi_macros() { quasi_macros::~quasi_macros() {
} }
void quasi_macros::find_occurrences(expr * e) { void quasi_macros::find_occurrences(expr * e) {
@ -41,7 +41,7 @@ void quasi_macros::find_occurrences(expr * e) {
// we remember whether we have seen an expr once, or more than once; // we remember whether we have seen an expr once, or more than once;
// when we see it the second time, we don't have to visit it another time, // when we see it the second time, we don't have to visit it another time,
// as we are only interested in finding unique function applications. // as we are only interested in finding unique function applications.
m_visited_once.reset(); m_visited_once.reset();
m_visited_more.reset(); m_visited_more.reset();
@ -64,8 +64,8 @@ void quasi_macros::find_occurrences(expr * e) {
if (is_non_ground_uninterp(cur)) { if (is_non_ground_uninterp(cur)) {
func_decl * f = to_app(cur)->get_decl(); func_decl * f = to_app(cur)->get_decl();
m_occurrences.insert_if_not_there(f, 0); m_occurrences.insert_if_not_there(f, 0);
occurrences_map::iterator it = m_occurrences.find_iterator(f); occurrences_map::iterator it = m_occurrences.find_iterator(f);
it->m_value++; it->m_value++;
} }
j = to_app(cur)->get_num_args(); j = to_app(cur)->get_num_args();
while (j) while (j)
@ -84,16 +84,16 @@ bool quasi_macros::is_unique(func_decl * f) const {
return m_occurrences.find(f) == 1; return m_occurrences.find(f) == 1;
} }
struct var_dep_proc { struct var_dep_proc {
bit_vector m_bitset; bit_vector m_bitset;
public: public:
var_dep_proc(quantifier * q) { m_bitset.resize(q->get_num_decls(), false); } var_dep_proc(quantifier * q) { m_bitset.resize(q->get_num_decls(), false); }
void operator()(var * n) { m_bitset.set(n->get_idx(), true); } void operator()(var * n) { m_bitset.set(n->get_idx(), true); }
void operator()(quantifier * n) {} void operator()(quantifier * n) {}
void operator()(app * n) {} void operator()(app * n) {}
bool all_used(void) { bool all_used(void) {
for (unsigned i = 0; i < m_bitset.size() ; i++) for (unsigned i = 0; i < m_bitset.size() ; i++)
if (!m_bitset.get(i)) if (!m_bitset.get(i))
return false; return false;
return true; return true;
} }
@ -101,7 +101,7 @@ public:
bool quasi_macros::fully_depends_on(app * a, quantifier * q) const { bool quasi_macros::fully_depends_on(app * a, quantifier * q) const {
// CMW: This checks whether all variables in q are used _somewhere_ deep down in the children of a // CMW: This checks whether all variables in q are used _somewhere_ deep down in the children of a
/* var_dep_proc proc(q); /* var_dep_proc proc(q);
for_each_expr(proc, a); for_each_expr(proc, a);
return proc.all_used(); */ return proc.all_used(); */
@ -116,14 +116,14 @@ bool quasi_macros::fully_depends_on(app * a, quantifier * q) const {
} }
for (unsigned i = 0; i < bitset.size() ; i++) { for (unsigned i = 0; i < bitset.size() ; i++) {
if (!bitset.get(i)) if (!bitset.get(i))
return false; return false;
} }
return true; return true;
} }
bool quasi_macros::depends_on(expr * e, func_decl * f) const { bool quasi_macros::depends_on(expr * e, func_decl * f) const {
ptr_vector<expr> todo; ptr_vector<expr> todo;
expr_mark visited; expr_mark visited;
todo.push_back(e); todo.push_back(e);
@ -133,12 +133,12 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const {
if (visited.is_marked(cur)) if (visited.is_marked(cur))
continue; continue;
if (is_app(cur)) { if (is_app(cur)) {
app * a = to_app(cur); app * a = to_app(cur);
if (a->get_decl() == f) if (a->get_decl() == f)
return true; return true;
unsigned j = a->get_num_args(); unsigned j = a->get_num_args();
while (j>0) while (j>0)
todo.push_back(a->get_arg(--j)); todo.push_back(a->get_arg(--j));
@ -151,7 +151,7 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const {
bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const { bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
// Our definition of a quasi-macro: // Our definition of a quasi-macro:
// Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted, // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
// f[X] contains all universally quantified variables, and f does not occur in T[X]. // f[X] contains all universally quantified variables, and f does not occur in T[X].
TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;); TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;);
@ -165,14 +165,14 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) && if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
!depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) { !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
a = to_app(lhs); a = to_app(lhs);
t = rhs; t = rhs;
return true; return true;
} else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) && } else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
!depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) { !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
a = to_app(rhs); a = to_app(rhs);
t = lhs; t = lhs;
return true; return true;
} }
} else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) && } else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) &&
is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false
a = to_app(to_app(qe)->get_arg(0)); a = to_app(to_app(qe)->get_arg(0));
@ -189,7 +189,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
} }
void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro) { void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro) {
m_new_var_names.reset(); m_new_var_names.reset();
m_new_vars.reset(); m_new_vars.reset();
m_new_qsorts.reset(); m_new_qsorts.reset();
m_new_eqs.reset(); m_new_eqs.reset();
@ -197,19 +197,19 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
func_decl * f = a->get_decl(); func_decl * f = a->get_decl();
// CMW: we rely on the fact that all variables in q appear at least once as // CMW: we rely on the fact that all variables in q appear at least once as
// a direct argument of `a'. // a direct argument of `a'.
bit_vector v_seen; bit_vector v_seen;
v_seen.resize(q->get_num_decls(), false); v_seen.resize(q->get_num_decls(), false);
for (unsigned i = 0 ; i < a->get_num_args() ; i++) { for (unsigned i = 0 ; i < a->get_num_args() ; i++) {
if (!is_var(a->get_arg(i)) || if (!is_var(a->get_arg(i)) ||
v_seen.get(to_var(a->get_arg(i))->get_idx())) { v_seen.get(to_var(a->get_arg(i))->get_idx())) {
unsigned inx = m_new_var_names.size(); unsigned inx = m_new_var_names.size();
m_new_name.str(""); m_new_name.str("");
m_new_name << "X" << inx; m_new_name << "X" << inx;
m_new_var_names.push_back(symbol(m_new_name.str().c_str())); m_new_var_names.push_back(symbol(m_new_name.str().c_str()));
m_new_qsorts.push_back(f->get_domain()[i]); m_new_qsorts.push_back(f->get_domain()[i]);
m_new_vars.push_back(m_manager.mk_var(inx + q->get_num_decls(), f->get_domain()[i])); m_new_vars.push_back(m_manager.mk_var(inx + q->get_num_decls(), f->get_domain()[i]));
m_new_eqs.push_back(m_manager.mk_eq(m_new_vars.back(), a->get_arg(i))); m_new_eqs.push_back(m_manager.mk_eq(m_new_vars.back(), a->get_arg(i)));
} else { } else {
@ -228,13 +228,13 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
new_var_names_rev.push_back(m_new_var_names.get(i)); new_var_names_rev.push_back(m_new_var_names.get(i));
new_qsorts_rev.push_back(m_new_qsorts.get(i)); new_qsorts_rev.push_back(m_new_qsorts.get(i));
} }
// We want to keep all the old variables [already reversed] // We want to keep all the old variables [already reversed]
for (unsigned i = 0 ; i < q->get_num_decls() ; i++) { for (unsigned i = 0 ; i < q->get_num_decls() ; i++) {
new_var_names_rev.push_back(q->get_decl_name(i)); new_var_names_rev.push_back(q->get_decl_name(i));
new_qsorts_rev.push_back(q->get_decl_sort(i)); new_qsorts_rev.push_back(q->get_decl_sort(i));
} }
// Macro := Forall m_new_vars . appl = ITE( m_new_eqs, t, f_else) // Macro := Forall m_new_vars . appl = ITE( m_new_eqs, t, f_else)
app_ref appl(m_manager); app_ref appl(m_manager);
@ -251,28 +251,28 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
eq = m_manager.mk_eq(appl, ite); eq = m_manager.mk_eq(appl, ite);
macro = m_manager.mk_quantifier(true, new_var_names_rev.size(), macro = m_manager.mk_quantifier(true, new_var_names_rev.size(),
new_qsorts_rev.c_ptr(), new_var_names_rev.c_ptr(), eq); new_qsorts_rev.c_ptr(), new_var_names_rev.c_ptr(), eq);
} }
bool quasi_macros::find_macros(unsigned n, expr * const * exprs) { bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl; TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl;
for (unsigned i = 0 ; i < n ; i++) for (unsigned i = 0 ; i < n ; i++)
tout << i << ": " << mk_pp(exprs[i], m_manager) << std::endl; ); tout << i << ": " << mk_pp(exprs[i], m_manager) << std::endl; );
bool res = false; bool res = false;
m_occurrences.reset(); m_occurrences.reset();
// Find out how many non-ground appearences for each uninterpreted function there are
// Find out how many non-ground appearences for each uninterpreted function there are
for ( unsigned i = 0 ; i < n ; i++ ) for ( unsigned i = 0 ; i < n ; i++ )
find_occurrences(exprs[i]); find_occurrences(exprs[i]);
TRACE("quasi_macros", tout << "Occurrences: " << std::endl; TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
for (occurrences_map::iterator it = m_occurrences.begin(); for (occurrences_map::iterator it = m_occurrences.begin();
it != m_occurrences.end(); it != m_occurrences.end();
it++) it++)
tout << it->m_key->get_name() << ": " << it->m_value << std::endl; ); tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
// Find all macros // Find all macros
for ( unsigned i = 0 ; i < n ; i++ ) { for ( unsigned i = 0 ; i < n ; i++ ) {
app_ref a(m_manager); app_ref a(m_manager);
@ -293,7 +293,7 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
return res; return res;
} }
void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
for ( unsigned i = 0 ; i < n ; i++ ) { for ( unsigned i = 0 ; i < n ; i++ ) {
expr_ref r(m_manager), rs(m_manager); expr_ref r(m_manager), rs(m_manager);
proof_ref pr(m_manager), ps(m_manager); proof_ref pr(m_manager), ps(m_manager);
@ -301,7 +301,7 @@ void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const
m_macro_manager.expand_macros(exprs[i], p, r, pr); m_macro_manager.expand_macros(exprs[i], p, r, pr);
m_simplifier(r, rs, ps); m_simplifier(r, rs, ps);
new_exprs.push_back(rs); new_exprs.push_back(rs);
new_prs.push_back(ps); new_prs.push_back(ps);
} }
} }
@ -313,9 +313,9 @@ bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const *
// just copy them over // just copy them over
for ( unsigned i = 0 ; i < n ; i++ ) { for ( unsigned i = 0 ; i < n ; i++ ) {
new_exprs.push_back(exprs[i]); new_exprs.push_back(exprs[i]);
if (m_manager.proofs_enabled()) if (m_manager.proofs_enabled())
new_prs.push_back(prs[i]); new_prs.push_back(prs[i]);
} }
return false; return false;
} }
} }