diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b197c5131..4ef6efd11 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -30,7 +30,7 @@ def init_project_def(): # Simplifier module will be deleted in the future. # It has been replaced with rewriter module. add_lib('simplifier', ['rewriter', 'front_end_params'], 'ast/simplifier') - add_lib('normal_forms', ['rewriter', 'simplifier'], 'ast/normal_forms') + add_lib('normal_forms', ['rewriter', 'front_end_params'], 'ast/normal_forms') add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core') add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic') add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith') @@ -41,7 +41,7 @@ def init_project_def(): add_lib('cmd_context', ['solver', 'rewriter']) add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds') add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') - add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern') + add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern') add_lib('macros', ['simplifier', 'front_end_params'], 'ast/macros') add_lib('proof_checker', ['rewriter', 'front_end_params'], 'ast/proof_checker') add_lib('bit_blaster', ['rewriter', 'simplifier', 'front_end_params'], 'ast/rewriter/bit_blaster') diff --git a/src/ast/normal_forms/cnf.cpp b/src/ast/normal_forms/cnf.cpp index f43b85154..d454c7f00 100644 --- a/src/ast/normal_forms/cnf.cpp +++ b/src/ast/normal_forms/cnf.cpp @@ -16,8 +16,9 @@ Author: Revision History: --*/ - #include"cnf.h" +#include"var_subst.h" +#include"ast_util.h" #include"ast_pp.h" #include"ast_ll_pp.h" diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index fa531c73a..5158439a7 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -17,369 +17,372 @@ Notes: --*/ #include"pull_quant.h" +#include"var_subst.h" +#include"rewriter_def.h" #include"ast_pp.h" -#include"for_each_expr.h" -void pull_quant::pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) { - ptr_buffer var_sorts; - buffer var_names; - symbol qid; - int w = INT_MAX; - - // The input formula is in Skolem normal form... - // So all children are forall (positive context) or exists (negative context). - // Remark: (AND a1 ...) may be represented (NOT (OR (NOT a1) ...))) - // So, when pulling a quantifier over a NOT, it becomes an exists. +struct pull_quant::imp { - if (m_manager.is_not(d)) { - SASSERT(num_children == 1); - expr * child = children[0]; - if (is_quantifier(child)) { - quantifier * q = to_quantifier(child); - expr * body = q->get_expr(); - result = m_manager.update_quantifier(q, !q->is_forall(), m_manager.mk_not(body)); + struct rw_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + shift_vars m_shift; + + rw_cfg(ast_manager & m): + m_manager(m), + m_shift(m) { } - else { - result = m_manager.mk_not(child); - } - return; - } - bool found_quantifier = false; - bool forall_children; - - for (unsigned i = 0; i < num_children; i++) { - expr * child = children[i]; - if (is_quantifier(child)) { + bool pull_quant1_core(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) { + ptr_buffer var_sorts; + buffer var_names; + symbol qid; + int w = INT_MAX; - if (!found_quantifier) { - found_quantifier = true; - forall_children = is_forall(child); - } - else { - // Since the initial formula was in SNF, all children must be EXISTS or FORALL. - SASSERT(forall_children == is_forall(child)); + // The input formula is in Skolem normal form... + // So all children are forall (positive context) or exists (negative context). + // Remark: (AND a1 ...) may be represented (NOT (OR (NOT a1) ...))) + // So, when pulling a quantifier over a NOT, it becomes an exists. + + if (m_manager.is_not(d)) { + SASSERT(num_children == 1); + expr * child = children[0]; + if (is_quantifier(child)) { + quantifier * q = to_quantifier(child); + expr * body = q->get_expr(); + result = m_manager.update_quantifier(q, !q->is_forall(), m_manager.mk_not(body)); + return true; + } + else { + return false; + } } - quantifier * nested_q = to_quantifier(child); - if (var_sorts.empty()) { - // use the qid of one of the nested quantifiers. - qid = nested_q->get_qid(); + bool found_quantifier = false; + bool forall_children; + + for (unsigned i = 0; i < num_children; i++) { + expr * child = children[i]; + if (is_quantifier(child)) { + + if (!found_quantifier) { + found_quantifier = true; + forall_children = is_forall(child); + } + else { + // Since the initial formula was in SNF, all children must be EXISTS or FORALL. + SASSERT(forall_children == is_forall(child)); + } + + quantifier * nested_q = to_quantifier(child); + if (var_sorts.empty()) { + // use the qid of one of the nested quantifiers. + qid = nested_q->get_qid(); + } + w = std::min(w, nested_q->get_weight()); + unsigned j = nested_q->get_num_decls(); + while (j > 0) { + --j; + var_sorts.push_back(nested_q->get_decl_sort(j)); + symbol s = nested_q->get_decl_name(j); + if (std::find(var_names.begin(), var_names.end(), s) != var_names.end()) + var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? 0 : s.bare_str())); + else + var_names.push_back(s); + } + } } - w = std::min(w, nested_q->get_weight()); - unsigned j = nested_q->get_num_decls(); - while (j > 0) { - --j; - var_sorts.push_back(nested_q->get_decl_sort(j)); - symbol s = nested_q->get_decl_name(j); - if (std::find(var_names.begin(), var_names.end(), s) != var_names.end()) - var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? 0 : s.bare_str())); - else - var_names.push_back(s); - } - } - } - - if (!var_sorts.empty()) { - SASSERT(found_quantifier); - // adjust the variable ids in formulas in new_children - expr_ref_buffer new_adjusted_children(m_manager); - expr_ref adjusted_child(m_manager); - unsigned num_decls = var_sorts.size(); - unsigned shift_amount = 0; - TRACE("pull_quant", tout << "Result num decls:" << num_decls << "\n";); - for (unsigned i = 0; i < num_children; i++) { - expr * child = children[i]; - if (!is_quantifier(child)) { - // increment the free variables in child by num_decls because - // child will be in the scope of num_decls bound variables. - m_shift(child, num_decls, adjusted_child); - TRACE("pull_quant", tout << "shifted by: " << num_decls << "\n" << - mk_pp(child, m_manager) << "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";); + + if (!var_sorts.empty()) { + SASSERT(found_quantifier); + // adjust the variable ids in formulas in new_children + expr_ref_buffer new_adjusted_children(m_manager); + expr_ref adjusted_child(m_manager); + unsigned num_decls = var_sorts.size(); + unsigned shift_amount = 0; + TRACE("pull_quant", tout << "Result num decls:" << num_decls << "\n";); + for (unsigned i = 0; i < num_children; i++) { + expr * child = children[i]; + if (!is_quantifier(child)) { + // increment the free variables in child by num_decls because + // child will be in the scope of num_decls bound variables. + m_shift(child, num_decls, adjusted_child); + TRACE("pull_quant", tout << "shifted by: " << num_decls << "\n" << + mk_pp(child, m_manager) << "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";); + } + else { + quantifier * nested_q = to_quantifier(child); + SASSERT(num_decls >= nested_q->get_num_decls()); + // Assume nested_q is of the form + // forall xs. P(xs, ys) + // where xs (ys) represents the set of bound (free) variables. + // + // - the index of the variables xs must be increased by shift_amount. + // That is, the number of new bound variables that will precede the bound + // variables xs. + // + // - the index of the variables ys must be increased by num_decls - nested_q->get_num_decls. + // That is, the total number of new bound variables that will be in the scope + // of nested_q->get_expr(). + m_shift(nested_q->get_expr(), + nested_q->get_num_decls(), // bound for shift1/shift2 + num_decls - nested_q->get_num_decls(), // shift1 (shift by this ammount if var idx >= bound) + shift_amount, // shift2 (shift by this ammount if var idx < bound) + adjusted_child); + TRACE("pull_quant", tout << "shifted bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount << + " shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) << + "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";); + shift_amount += nested_q->get_num_decls(); + } + new_adjusted_children.push_back(adjusted_child); + } + + // Remark: patterns are ignored. + // This is ok, since this functor is used in one of the following cases: + // + // 1) Superposition calculus is being used, so the + // patterns are useless. + // + // 2) No patterns were provided, and the functor is used + // to increase the effectiveness of the pattern inference + // procedure. + // + // 3) MBQI + std::reverse(var_sorts.begin(), var_sorts.end()); + std::reverse(var_names.begin(), var_names.end()); + result = m_manager.mk_quantifier(forall_children, + var_sorts.size(), + var_sorts.c_ptr(), + var_names.c_ptr(), + m_manager.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()), + w, + qid); + return true; } else { - quantifier * nested_q = to_quantifier(child); - SASSERT(num_decls >= nested_q->get_num_decls()); - // Assume nested_q is of the form - // forall xs. P(xs, ys) - // where xs (ys) represents the set of bound (free) variables. - // - // - the index of the variables xs must be increased by shift_amount. - // That is, the number of new bound variables that will precede the bound - // variables xs. - // - // - the index of the variables ys must be increased by num_decls - nested_q->get_num_decls. - // That is, the total number of new bound variables that will be in the scope - // of nested_q->get_expr(). - m_shift(nested_q->get_expr(), - nested_q->get_num_decls(), // bound for shift1/shift2 - num_decls - nested_q->get_num_decls(), // shift1 (shift by this ammount if var idx >= bound) - shift_amount, // shift2 (shift by this ammount if var idx < bound) - adjusted_child); - TRACE("pull_quant", tout << "shifted bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount << - " shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) << - "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";); - shift_amount += nested_q->get_num_decls(); + SASSERT(!found_quantifier); + return false; } - new_adjusted_children.push_back(adjusted_child); } - // Remark: patterns are ignored. - // This is ok, since this functor is used in one of the following cases: - // - // 1) Superposition calculus is being used, so the - // patterns are useless. - // - // 2) No patterns were provided, and the functor is used - // to increase the effectiveness of the pattern inference - // procedure. - // - // 3) MBQI - std::reverse(var_sorts.begin(), var_sorts.end()); - std::reverse(var_names.begin(), var_names.end()); - result = m_manager.mk_quantifier(forall_children, - var_sorts.size(), + void pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) { + if (!pull_quant1_core(d, num_children, children, result)) { + result = m_manager.mk_app(d, num_children, children); + } + } + + + void pull_quant1_core(quantifier * q, expr * new_expr, expr_ref & result) { + // The original formula was in SNF, so the original quantifiers must be universal. + SASSERT(is_forall(q)); + SASSERT(is_forall(new_expr)); + quantifier * nested_q = to_quantifier(new_expr); + ptr_buffer var_sorts; + buffer var_names; + var_sorts.append(q->get_num_decls(), const_cast(q->get_decl_sorts())); + var_sorts.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_sorts())); + var_names.append(q->get_num_decls(), const_cast(q->get_decl_names())); + var_names.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_names())); + // Remark: patterns are ignored. + // See comment in reduce1_app + result = m_manager.mk_forall(var_sorts.size(), var_sorts.c_ptr(), var_names.c_ptr(), - m_manager.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()), - w, - qid); - } - else { - SASSERT(!found_quantifier); - result = m_manager.mk_app(d, num_children, children); - } -} - -void pull_quant::pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) { - // The original formula was in SNF, so the original quantifiers must be universal. - SASSERT(is_forall(q)); - if (is_forall(new_expr)) { - quantifier * nested_q = to_quantifier(new_expr); - ptr_buffer var_sorts; - buffer var_names; - var_sorts.append(q->get_num_decls(), const_cast(q->get_decl_sorts())); - var_sorts.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_sorts())); - var_names.append(q->get_num_decls(), const_cast(q->get_decl_names())); - var_names.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_names())); - // Remark: patterns are ignored. - // See comment in reduce1_app - result = m_manager.mk_forall(var_sorts.size(), - var_sorts.c_ptr(), - var_names.c_ptr(), - nested_q->get_expr(), - std::min(q->get_weight(), nested_q->get_weight()), - q->get_qid()); - } - else { - SASSERT(!is_quantifier(new_expr)); - result = m_manager.update_quantifier(q, new_expr); - } -} - -void pull_quant::pull_quant1(expr * n, expr_ref & result) { - if (is_app(n)) - pull_quant1(to_app(n)->get_decl(), to_app(n)->get_num_args(), to_app(n)->get_args(), result); - else if (is_quantifier(n)) - pull_quant1(to_quantifier(n), to_quantifier(n)->get_expr(), result); - else - result = n; -} - -// Code for proof generation... -void pull_quant::pull_quant2(expr * n, expr_ref & r, proof_ref & pr) { - pr = 0; - if (is_app(n)) { - expr_ref_buffer new_args(m_manager); - expr_ref new_arg(m_manager); - ptr_buffer proofs; - unsigned num = to_app(n)->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * arg = to_app(n)->get_arg(i); - pull_quant1(arg , new_arg); - new_args.push_back(new_arg); - if (new_arg != arg) - proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg))); + nested_q->get_expr(), + std::min(q->get_weight(), nested_q->get_weight()), + q->get_qid()); } - pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r); - if (m_manager.fine_grain_proofs()) { - app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr()); - proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr()); - proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r)); - pr = m_manager.mk_transitivity(p1, p2); - } - } - else if (is_quantifier(n)) { - expr_ref new_expr(m_manager); - pull_quant1(to_quantifier(n)->get_expr(), new_expr); - pull_quant1(to_quantifier(n), new_expr, r); - if (m_manager.fine_grain_proofs()) { - quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr); - proof * p1 = 0; - if (n != q1) { - proof * p0 = m_manager.mk_pull_quant(to_quantifier(n)->get_expr(), to_quantifier(new_expr)); - p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0); + + void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) { + // The original formula was in SNF, so the original quantifiers must be universal. + SASSERT(is_forall(q)); + if (is_forall(new_expr)) { + pull_quant1_core(q, new_expr, result); } - proof * p2 = q1 == r ? 0 : m_manager.mk_pull_quant(q1, to_quantifier(r)); - pr = m_manager.mk_transitivity(p1, p2); - } - } - else { - r = n; - } -} - -bool pull_quant::visit_children(expr * n) { - bool visited = true; - unsigned j; - switch(n->get_kind()) { - case AST_APP: - // This transformation is also applied after the formula - // has been converted into a SNF using only OR and NOT. - if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_not(n)) { - j = to_app(n)->get_num_args(); - while (j > 0) { - --j; - visit(to_app(n)->get_arg(j), visited); - } - } - else { - // This class assumes the formula is in skolem normal form. - SASSERT(!has_quantifiers(n)); - } - break; - case AST_QUANTIFIER: - if (to_quantifier(n)->is_forall()) - visit(to_quantifier(n)->get_expr(), visited); - break; - default: - break; - } - return visited; -} - -void pull_quant::reduce1(expr * n) { - switch(n->get_kind()) { - case AST_APP: - reduce1_app(to_app(n)); - break; - case AST_VAR: - cache_result(n, n, 0); - break; - case AST_QUANTIFIER: - reduce1_quantifier(to_quantifier(n)); - break; - default: - UNREACHABLE(); - break; - } -} - -void pull_quant::reduce1_app(app * n) { - if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_not(n)) { - ptr_buffer new_children; - ptr_buffer new_children_proofs; - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * new_child = 0; - proof * new_child_pr = 0; - get_cached(n->get_arg(i), new_child, new_child_pr); - new_children.push_back(new_child); - if (new_child_pr) { - new_children_proofs.push_back(new_child_pr); + else { + SASSERT(!is_quantifier(new_expr)); + result = m_manager.update_quantifier(q, new_expr); } } - expr_ref r(m_manager); - pull_quant1(n->get_decl(), new_children.size(), new_children.c_ptr(), r); - proof * pr = 0; - if (m_manager.fine_grain_proofs()) { - app * n_prime = m_manager.mk_app(n->get_decl(), new_children.size(), new_children.c_ptr()); - TRACE("proof_bug", tout << mk_pp(n, m_manager) << "\n"; - tout << mk_pp(n_prime, m_manager) << "\n";); - proof * p1 = n == n_prime ? 0 : m_manager.mk_congruence(n, n_prime, - new_children_proofs.size(), new_children_proofs.c_ptr()); - proof * p2 = n_prime == r ? 0 : m_manager.mk_pull_quant(n_prime, to_quantifier(r)); - pr = m_manager.mk_transitivity(p1, p2); + void pull_quant1(expr * n, expr_ref & result) { + if (is_app(n)) + pull_quant1(to_app(n)->get_decl(), to_app(n)->get_num_args(), to_app(n)->get_args(), result); + else if (is_quantifier(n)) + pull_quant1(to_quantifier(n), to_quantifier(n)->get_expr(), result); + else + result = n; + } + + // Code for proof generation... + void pull_quant2(expr * n, expr_ref & r, proof_ref & pr) { + pr = 0; + if (is_app(n)) { + expr_ref_buffer new_args(m_manager); + expr_ref new_arg(m_manager); + ptr_buffer proofs; + unsigned num = to_app(n)->get_num_args(); + for (unsigned i = 0; i < num; i++) { + expr * arg = to_app(n)->get_arg(i); + pull_quant1(arg , new_arg); + new_args.push_back(new_arg); + if (new_arg != arg) + proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg))); + } + pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r); + if (m_manager.fine_grain_proofs()) { + app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr()); + proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr()); + proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r)); + pr = m_manager.mk_transitivity(p1, p2); + } + } + else if (is_quantifier(n)) { + expr_ref new_expr(m_manager); + pull_quant1(to_quantifier(n)->get_expr(), new_expr); + pull_quant1(to_quantifier(n), new_expr, r); + if (m_manager.fine_grain_proofs()) { + quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr); + proof * p1 = 0; + if (n != q1) { + proof * p0 = m_manager.mk_pull_quant(to_quantifier(n)->get_expr(), to_quantifier(new_expr)); + p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0); + } + proof * p2 = q1 == r ? 0 : m_manager.mk_pull_quant(q1, to_quantifier(r)); + pr = m_manager.mk_transitivity(p1, p2); + } + } + else { + r = n; + } } - cache_result(n, r, pr); - return; - } - TRACE("proof_bug", tout << mk_pp(n, m_manager) << "\n";); - cache_result(n, n, 0); -} -void pull_quant::reduce1_quantifier(quantifier * q) { - if (q->is_forall()) { - expr * new_expr; - proof * new_expr_pr; - get_cached(q->get_expr(), new_expr, new_expr_pr); - expr_ref r(m_manager); - pull_quant1(q, new_expr, r); - proof * pr = 0; - if (m_manager.fine_grain_proofs()) { - quantifier * q_prime = m_manager.update_quantifier(q, new_expr); - proof * p1 = q == q_prime ? 0 : m_manager.mk_quant_intro(q, q_prime, new_expr_pr); - proof * p2 = q_prime == r ? 0 : m_manager.mk_pull_quant(q_prime, to_quantifier(r)); - pr = m_manager.mk_transitivity(p1, p2); + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + if (!m_manager.is_or(f) && !m_manager.is_and(f) && !m_manager.is_not(f)) + return BR_FAILED; + + if (!pull_quant1_core(f, num, args, result)) + return BR_FAILED; + + if (m_manager.proofs_enabled()) { + result_pr = m_manager.mk_pull_quant(m_manager.mk_app(f, num, args), + to_quantifier(result.get())); + } + return BR_DONE; } - cache_result(q, r, pr); - return; - } - // should be unreachable, right? - UNREACHABLE(); - cache_result(q, q, 0); -} + + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + + if (old_q->is_exists()) { + UNREACHABLE(); + return false; + } + + if (!is_forall(new_body)) + return false; + + pull_quant1_core(old_q, new_body, result); + if (m_manager.proofs_enabled()) + result_pr = m_manager.mk_pull_quant(old_q, to_quantifier(result.get())); + return true; + } + }; + + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + rw(ast_manager & m): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m) { + } + }; -pull_quant::pull_quant(ast_manager & m): - base_simplifier(m), - m_shift(m) { + rw m_rw; + + imp(ast_manager & m): + m_rw(m) { + } + + void operator()(expr * n, expr_ref & r, proof_ref & p) { + m_rw(n, r, p); + } +}; + +pull_quant::pull_quant(ast_manager & m) { + m_imp = alloc(imp, m); +} + +pull_quant::~pull_quant() { + dealloc(m_imp); } void pull_quant::operator()(expr * n, expr_ref & r, proof_ref & p) { - flush_cache(); - m_todo.push_back(n); - while (!m_todo.empty()) { - expr * n = m_todo.back(); - if (is_cached(n)) - m_todo.pop_back(); - else if (visit_children(n)) { - m_todo.pop_back(); - reduce1(n); + (*m_imp)(n, r, p); +} + +void pull_quant::reset() { + m_imp->m_rw.reset(); +} + +void pull_quant::pull_quant2(expr * n, expr_ref & r, proof_ref & pr) { + m_imp->m_rw.cfg().pull_quant2(n, r, pr); +} + +struct pull_nested_quant::imp { + + struct rw_cfg : public default_rewriter_cfg { + pull_quant m_pull; + expr_ref m_r; + proof_ref m_pr; + + rw_cfg(ast_manager & m):m_pull(m), m_r(m), m_pr(m) {} + + bool get_subst(expr * s, expr * & t, proof * & t_pr) { + if (!is_quantifier(s)) + return false; + m_pull(to_quantifier(s), m_r, m_pr); + t = m_r.get(); + t_pr = m_pr.get(); + return true; } - } - - expr * result; - proof * result_proof; - get_cached(n, result, result_proof); + }; - r = result; + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + rw(ast_manager & m): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m) { + } + }; - switch (m_manager.proof_mode()) { - case PGM_DISABLED: - p = m_manager.mk_undef_proof(); - break; - case PGM_COARSE: - if (result == n) - p = m_manager.mk_reflexivity(n); - else - p = m_manager.mk_pull_quant_star(n, to_quantifier(result)); - break; - case PGM_FINE: - SASSERT(result_proof || result == n); - p = result_proof ? result_proof : m_manager.mk_reflexivity(n); - break; + rw m_rw; + + imp(ast_manager & m): + m_rw(m) { } + + void operator()(expr * n, expr_ref & r, proof_ref & p) { + m_rw(n, r, p); + } +}; + +pull_nested_quant::pull_nested_quant(ast_manager & m) { + m_imp = alloc(imp, m); } -bool pull_nested_quant::visit_quantifier(quantifier * q) { - // do not recurse. - return true; +pull_nested_quant::~pull_nested_quant() { + dealloc(m_imp); } -void pull_nested_quant::reduce1_quantifier(quantifier * q) { - expr_ref r(m_manager); - proof_ref pr(m_manager); - m_pull(q, r, pr); - cache_result(q, r, pr); +void pull_nested_quant::operator()(expr * n, expr_ref & r, proof_ref & p) { + (*m_imp)(n, r, p); } + +void pull_nested_quant::reset() { + m_imp->m_rw.reset(); +} + + diff --git a/src/ast/normal_forms/pull_quant.h b/src/ast/normal_forms/pull_quant.h index e9b2b5c65..071fb0dbe 100644 --- a/src/ast/normal_forms/pull_quant.h +++ b/src/ast/normal_forms/pull_quant.h @@ -19,8 +19,7 @@ Notes: #ifndef _PULL_QUANT_H_ #define _PULL_QUANT_H_ -#include"simplifier.h" -#include"var_subst.h" +#include"ast.h" /** \brief Pull nested quantifiers in a formula. @@ -32,22 +31,14 @@ Notes: \remark If pull_quant(F) is a quantifier then its weight is Min{weight(Q') | Q' is a quantifier nested in F} */ -class pull_quant : public base_simplifier { -protected: - shift_vars m_shift; - bool visit_children(expr * n); - void reduce1(expr *); - void reduce1_app(app * n); - void reduce1_quantifier(quantifier * q); - +class pull_quant { + struct imp; + imp * m_imp; public: pull_quant(ast_manager & m); - virtual ~pull_quant() {} + ~pull_quant(); void operator()(expr * n, expr_ref & r, proof_ref & p); - void reset() { flush_cache(); } - void pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result); - void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result); - void pull_quant1(expr * n, expr_ref & result); + void reset(); void pull_quant2(expr * n, expr_ref & r, proof_ref & pr); }; @@ -55,13 +46,14 @@ public: \brief After applying this transformation the formula will not contain nested quantifiers. */ -class pull_nested_quant : public simplifier { - pull_quant m_pull; - virtual bool visit_quantifier(quantifier * q); - virtual void reduce1_quantifier(quantifier * q); +class pull_nested_quant { + struct imp; + imp * m_imp; public: - pull_nested_quant(ast_manager & m):simplifier(m), m_pull(m) { enable_ac_support(false); } - virtual ~pull_nested_quant() {} + pull_nested_quant(ast_manager & m); + ~pull_nested_quant(); + void operator()(expr * n, expr_ref & r, proof_ref & p); + void reset(); }; #endif /* _PULL_QUANT_H_ */