From be5f93320123c198997e1a5567a1417d0f020e74 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Nov 2012 18:20:07 -0800 Subject: [PATCH] removed dead module Signed-off-by: Leonardo de Moura --- src/ast/normal_forms/cnf.cpp | 527 ---------------------------- src/ast/normal_forms/cnf.h | 141 -------- src/ast/normal_forms/cnf_params.pyg | 4 - 3 files changed, 672 deletions(-) delete mode 100644 src/ast/normal_forms/cnf.cpp delete mode 100644 src/ast/normal_forms/cnf.h delete mode 100644 src/ast/normal_forms/cnf_params.pyg diff --git a/src/ast/normal_forms/cnf.cpp b/src/ast/normal_forms/cnf.cpp deleted file mode 100644 index 2a58b16a6..000000000 --- a/src/ast/normal_forms/cnf.cpp +++ /dev/null @@ -1,527 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - cnf.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-01-23. - -Revision History: - ---*/ -#include"cnf.h" -#include"cnf_params.hpp" -#include"var_subst.h" -#include"ast_util.h" -#include"ast_pp.h" -#include"ast_ll_pp.h" - -unsigned cnf_entry::hash() const { - unsigned a = m_node->get_id(); - unsigned b = m_polarity; - unsigned c = m_in_q; - mix(a,b,c); - return c; -} - -bool cnf_entry::operator==(cnf_entry const & k) const { - return m_node == k.m_node && m_polarity == k.m_polarity && m_in_q == k.m_in_q; -} - -cnf_cache::cnf_cache(ast_manager & m): - m_manager(m) { -} - -void cnf_cache::insert(cnf_entry const & k, expr * r, proof * pr) { - SASSERT(!m_cache.contains(k)); - m_manager.inc_ref(r); - m_manager.inc_ref(pr); - m_cache.insert(k, expr_proof_pair(r, pr)); -} - -void cnf_cache::reset() { - cache::iterator it = m_cache.begin(); - cache::iterator end = m_cache.end(); - for (; it != end; ++it) { - expr_proof_pair & pair = (*it).m_value; - m_manager.dec_ref(pair.first); - m_manager.dec_ref(pair.second); - } - m_cache.reset(); -} - -void cnf::cache_result(expr * e, bool in_q, expr * r, proof * pr) { - SASSERT(r); - TRACE("cnf", tout << "caching result for: " << e->get_id() << " " << r->get_id() << "\n";); - m_cache.insert(cnf_entry(e, true, in_q), r, pr); -} - -void cnf::visit(expr * n, bool in_q, bool & visited) { - if (!is_cached(n, in_q)) { - m_todo.push_back(std::make_pair(n, in_q)); - visited = false; - } -} - -bool cnf::visit_children(expr * n, bool in_q) { - bool visited = true; - switch(n->get_kind()) { - case AST_APP: - if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_label(n)) { - unsigned j = to_app(n)->get_num_args(); - while (j > 0) { - --j; - visit(to_app(n)->get_arg(j), in_q, visited); - } - } - break; - case AST_QUANTIFIER: - visit(to_quantifier(n)->get_expr(), true, visited); - break; - default: - break; - } - return visited; -} - -void cnf::reduce1(expr * n, bool in_q) { - switch(n->get_kind()) { - case AST_APP: - if (m_manager.is_or(n)) - reduce1_or(to_app(n), in_q); - else if (m_manager.is_and(n)) - reduce1_and(to_app(n), in_q); - else if (m_manager.is_label(n)) - reduce1_label(to_app(n), in_q); - else - cache_result(n, in_q, n, 0); - break; - case AST_QUANTIFIER: - reduce1_quantifier(to_quantifier(n), in_q); - break; - default: - cache_result(n, in_q, n, 0); - break; - } -} - -void cnf::get_args(app * n, bool in_q, ptr_buffer & new_args, ptr_buffer & new_arg_prs) { - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * new_arg = 0; - proof * new_arg_pr = 0; - get_cached(n->get_arg(i), in_q, new_arg, new_arg_pr); - SASSERT(new_arg); - new_args.push_back(new_arg); - if (new_arg_pr) - new_arg_prs.push_back(new_arg_pr); - } -} - -void cnf::flat_args(func_decl * d, ptr_buffer const & args, ptr_buffer & flat_args) { - ptr_buffer::const_iterator it = args.begin(); - ptr_buffer::const_iterator end = args.end(); - for (; it != end; ++it) { - expr * arg = *it; - if (is_app_of(arg, d)) - flat_args.append(to_app(arg)->get_num_args(), to_app(arg)->get_args()); - else - flat_args.push_back(arg); - } -} - -/** - \brief Return the approximated size of distributing OR over AND on - (OR args[0] .... args[sz-1]) -*/ -approx_nat cnf::approx_result_size_for_disj(ptr_buffer const & args) { - approx_nat r(1); - ptr_buffer::const_iterator it = args.begin(); - ptr_buffer::const_iterator end = args.end(); - for (; it != end; ++it) { - expr * arg = *it; - if (m_manager.is_and(arg)) - r *= to_app(arg)->get_num_args(); - } - return r; -} - -/** - \brief Return true if it is too expensive to process the disjunction of args -*/ -inline bool cnf::is_too_expensive(approx_nat approx_result_size, ptr_buffer const & args) { - // (OR A (AND B C)) is always considered cheap. - if (args.size() == 2 && (!m_manager.is_and(args[0]) || !m_manager.is_and(args[1]))) - return false; - return !(approx_result_size < m_cnf_factor); -} - -/** - \brief Create a (positive) name for the expressions of the form (AND ...) in args. - Store the result in new_args. -*/ -void cnf::name_args(ptr_buffer const & args, expr_ref_buffer & new_args, proof_ref_buffer & new_arg_prs) { - ptr_buffer::const_iterator it = args.begin(); - ptr_buffer::const_iterator end = args.end(); - for (; it != end; ++it) { - expr * arg = *it; - if (m_manager.is_and(arg)) { - expr_ref new_def(m_manager); - proof_ref new_def_pr(m_manager); - app_ref new_arg(m_manager); - proof_ref new_arg_pr(m_manager); - - if (m_defined_names.mk_pos_name(to_app(arg), new_def, new_def_pr, new_arg, new_arg_pr)) { - m_todo_defs.push_back(new_def); - if (m_manager.proofs_enabled()) - m_todo_proofs.push_back(new_def_pr); - } - new_args.push_back(new_arg); - - if (m_manager.fine_grain_proofs()) - new_arg_prs.push_back(new_arg_pr); - else - m_coarse_proofs.push_back(new_arg_pr); - } - else - new_args.push_back(arg); - } -} - -void cnf::distribute(app * n, app * & r, proof * & pr) { - SASSERT(m_manager.is_or(n)); - buffer sz; - buffer it; - ptr_buffer new_args; - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * arg = n->get_arg(i); - it.push_back(0); - if (m_manager.is_and(arg)) - sz.push_back(to_app(arg)->get_num_args()); - else - sz.push_back(1); - } - - do { - ptr_buffer lits; - for (unsigned i = 0; i < num; i++) { - expr * arg = n->get_arg(i); - if (m_manager.is_and(arg)) { - SASSERT(it[i] < to_app(arg)->get_num_args()); - lits.push_back(to_app(arg)->get_arg(it[i])); - } - else { - SASSERT(it[i] == 0); - lits.push_back(arg); - } - } - app * n = m_manager.mk_or(lits.size(), lits.c_ptr()); - new_args.push_back(n); - } - while (product_iterator_next(sz.size(), sz.c_ptr(), it.c_ptr())); - SASSERT(!new_args.empty()); - if (new_args.size() == 1) - r = to_app(new_args[0]); - else - r = m_manager.mk_and(new_args.size(), new_args.c_ptr()); - pr = 0; - if (m_manager.fine_grain_proofs() && r != n) - pr = m_manager.mk_iff_oeq(m_manager.mk_distributivity(n, r)); -} - -void cnf::push_quant(quantifier * q, expr * & r, proof * & pr) { - SASSERT(is_forall(q)); - expr * e = q->get_expr(); - pr = 0; - if (m_manager.is_and(e)) { - expr_ref_buffer new_args(m_manager); - unsigned num = to_app(e)->get_num_args(); - for (unsigned i = 0; i < num; i++) { - quantifier_ref aux(m_manager); - aux = m_manager.update_quantifier(q, 0, 0, 0, 0, to_app(e)->get_arg(i)); - expr_ref new_arg(m_manager); - elim_unused_vars(m_manager, aux, new_arg); - new_args.push_back(new_arg); - } - r = m_manager.mk_and(new_args.size(), new_args.c_ptr()); - if (m_manager.fine_grain_proofs()) - pr = m_manager.mk_iff_oeq(m_manager.mk_push_quant(q, r)); - } - else { - r = q; - } -} - -void cnf::reduce1_or(app * n, bool in_q) { - ptr_buffer new_args; - ptr_buffer new_arg_prs; - get_args(n, in_q, new_args, new_arg_prs); - expr * r; - proof * pr = 0; - if (in_q || m_cnf_mode == CNF_OPPORTUNISTIC || m_cnf_mode == CNF_FULL) { - ptr_buffer f_args; - flat_args(n->get_decl(), new_args, f_args); - TRACE("cnf_or", for (unsigned i = 0; i < f_args.size(); i++) tout << mk_pp(f_args[i], m_manager) << "\n";); - approx_nat result_size = approx_result_size_for_disj(f_args); - TRACE("cnf_or", tout << mk_pp(n, m_manager) << "\napprox. result: " << result_size << "\n";); - if (m_cnf_mode != CNF_OPPORTUNISTIC || result_size < m_cnf_factor) { - expr_ref_buffer cheap_args(m_manager); - proof_ref_buffer cheap_args_pr(m_manager); - if (is_too_expensive(result_size, f_args)) { - name_args(f_args, cheap_args, cheap_args_pr); - } - else { - cheap_args.append(f_args.size(), f_args.c_ptr()); - } - - app_ref r1(m_manager); - r1 = m_manager.mk_or(cheap_args.size(), cheap_args.c_ptr()); - - // Proof gen support --------------------------- - // r1 is (OR cheap_args) it is only built if proofs are enabled. - // p1 is a proof for (= n r1) - proof * p1 = 0; - if (m_manager.fine_grain_proofs()) { - proof * prs[3]; - app * r[2]; - r[0] = m_manager.mk_or(new_args.size(), new_args.c_ptr()); - prs[0] = n == r[0] ? 0 : m_manager.mk_oeq_congruence(n, r[0], new_arg_prs.size(), new_arg_prs.c_ptr()); - r[1] = m_manager.mk_or(f_args.size(), f_args.c_ptr()); - prs[1] = r[0] == r[1] ? 0 : m_manager.mk_iff_oeq(m_manager.mk_rewrite(r[0], r[1])); - prs[2] = r[1] == r1 ? 0 : m_manager.mk_oeq_congruence(r[1], r1, cheap_args_pr.size(), cheap_args_pr.c_ptr()); - p1 = m_manager.mk_transitivity(3, prs); - } - // -------------------------------------------- - - expr_ref r2(m_manager); - proof_ref p2(m_manager); - m_pull.pull_quant2(r1, r2, p2); - - if (is_quantifier(r2)) { - expr * e = to_quantifier(r2)->get_expr(); - SASSERT(m_manager.is_or(e)); - app * d_r; - proof * d_pr; - distribute(to_app(e), d_r, d_pr); - quantifier_ref r3(m_manager); - r3 = m_manager.update_quantifier(to_quantifier(r2), d_r); - proof * push_pr; - push_quant(r3, r, push_pr); - if (m_manager.fine_grain_proofs()) { - // p1 is a proof of n == r1 - // p2 is a proof of r1 == r2 - p2 = p2 == 0 ? 0 : m_manager.mk_iff_oeq(p2); - proof * p3 = r2 == r3 ? 0 : m_manager.mk_oeq_quant_intro(to_quantifier(r2), r3, d_pr); - CTRACE("cnf_or", p1, tout << "p1:\n" << mk_pp(m_manager.get_fact(p1), m_manager) << "\n";); - CTRACE("cnf_or", p2, tout << "p2:\n" << mk_pp(m_manager.get_fact(p2), m_manager) << "\n";); - CTRACE("cnf_or", p3, tout << "p3:\n" << mk_pp(m_manager.get_fact(p3), m_manager) << "\n";); - TRACE("cnf_or", tout << "r2 == r3: " << (r2 == r3) << "\n" - << mk_pp(r2, m_manager) << "\n" << mk_pp(r3, m_manager) << "\n";); - pr = m_manager.mk_transitivity(p1, p2, p3, push_pr); - } - cache_result(n, in_q, r, pr); - } - else { - SASSERT(p2 == 0); - SASSERT(r1 == r2); - SASSERT(m_manager.is_or(r2)); - app * r3; - distribute(to_app(r2), r3, pr); - r = r3; - pr = m_manager.mk_transitivity(p1, pr); - cache_result(n, in_q, r, pr); - } - return; - } - } - - r = m_manager.mk_or(new_args.size(), new_args.c_ptr()); - if (m_manager.fine_grain_proofs() && n != r) - pr = m_manager.mk_oeq_congruence(n, to_app(r), new_arg_prs.size(), new_arg_prs.c_ptr()); - cache_result(n, in_q, r, pr); -} - -void cnf::reduce1_and(app * n, bool in_q) { - ptr_buffer new_args; - ptr_buffer new_arg_prs; - get_args(n, in_q, new_args, new_arg_prs); - app * r; - proof * pr = 0; - if (in_q || m_cnf_mode == CNF_OPPORTUNISTIC || m_cnf_mode == CNF_FULL) { - ptr_buffer f_args; - flat_args(n->get_decl(), new_args, f_args); - r = m_manager.mk_and(f_args.size(), f_args.c_ptr()); - if (m_manager.fine_grain_proofs() && n != r) { - app * r0 = m_manager.mk_and(new_args.size(), new_args.c_ptr()); - proof * p0 = r0 == n ? 0 : m_manager.mk_oeq_congruence(n, r0, new_arg_prs.size(), new_arg_prs.c_ptr()); - proof * p1 = r0 == r ? 0 : m_manager.mk_iff_oeq(m_manager.mk_rewrite(r0, r)); - pr = m_manager.mk_transitivity(p0, p1); - } - } - else { - r = m_manager.mk_and(new_args.size(), new_args.c_ptr()); - if (m_manager.fine_grain_proofs() && n != r) - pr = m_manager.mk_oeq_congruence(n, r, new_arg_prs.size(), new_arg_prs.c_ptr()); - } - cache_result(n, in_q, r, pr); -} - -void cnf::reduce1_label(app * n, bool in_q) { - expr * r; - proof * pr = 0; - expr * new_arg; - proof * new_arg_pr; - get_cached(n->get_arg(0), true, new_arg, new_arg_pr); - if (in_q || m_cnf_mode == CNF_FULL) { - // TODO: in the current implementation, labels are removed during CNF translation. - // This is satisfactory for Boogie, since it does not use labels inside quantifiers, - // and we only need CNF_QUANT for Superposition Calculus. - r = new_arg; - if (m_manager.fine_grain_proofs()) { - proof * p0 = m_manager.mk_iff_oeq(m_manager.mk_rewrite(n, n->get_arg(0))); - pr = m_manager.mk_transitivity(p0, new_arg_pr); - } - } - else { - r = m_manager.mk_app(n->get_decl(), new_arg); - if (m_manager.fine_grain_proofs() && n != r) - pr = m_manager.mk_oeq_congruence(n, to_app(r), 1, &new_arg_pr); - } - cache_result(n, in_q, r, pr); -} - -void cnf::reduce1_quantifier(quantifier * q, bool in_q) { - expr * new_expr; - proof * new_expr_pr; - get_cached(q->get_expr(), true, new_expr, new_expr_pr); - expr_ref r(m_manager); - proof_ref pr(m_manager); - if (m_manager.is_and(new_expr) && q->is_forall()) { - quantifier_ref q1(m_manager); - q1 = m_manager.update_quantifier(q, new_expr); - expr_ref q2(m_manager); - proof_ref p2(m_manager); - m_pull.pull_quant2(q1, q2, p2); - expr * q3; - proof * p3; - push_quant(to_quantifier(q2), q3, p3); - r = q3; - if (m_manager.fine_grain_proofs()) { - proof * p1 = q == q1 ? 0 : m_manager.mk_oeq_quant_intro(q, q1, new_expr_pr); - p2 = p2 == 0 ? 0 : m_manager.mk_iff_oeq(p2); - pr = m_manager.mk_transitivity(p1, p2, p3); - } - } - else if ((m_manager.is_or(new_expr) || is_forall(new_expr)) && q->is_forall()) { - quantifier_ref q1(m_manager); - q1 = m_manager.update_quantifier(q, new_expr); - m_pull.pull_quant2(q1, r, pr); - if (m_manager.fine_grain_proofs()) { - pr = pr == 0 ? 0 : m_manager.mk_iff_oeq(pr); - proof * p1 = q == q1 ? 0 : m_manager.mk_oeq_quant_intro(q, q1, new_expr_pr); - pr = m_manager.mk_transitivity(p1, pr); - } - } - else { - r = m_manager.update_quantifier(q, new_expr); - if (m_manager.fine_grain_proofs() && r != q) - pr = q == r ? 0 : m_manager.mk_oeq_quant_intro(q, to_quantifier(r), new_expr_pr); - } - - cache_result(q, in_q, r, pr); - TRACE("cnf_quant", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";); -} - -cnf::cnf(ast_manager & m, defined_names & n, params_ref const & params): - m_manager(m), - m_defined_names(n), - m_pull(m), - m_cache(m), - m_todo_defs(m), - m_todo_proofs(m), - m_coarse_proofs(m) { - cnf_params p(params); - m_cnf_mode = static_cast(p.mode()); - m_cnf_factor = p.factor(); -} - -cnf::~cnf() { -} - -void cnf::reduce(expr * n, expr_ref & r, proof_ref & pr) { - m_coarse_proofs.reset(); - m_todo.reset(); - m_todo.push_back(expr_bool_pair(n, false)); - while (!m_todo.empty()) { - expr_bool_pair pair = m_todo.back(); - expr * n = pair.first; - bool in_q = pair.second; - if (is_cached(n, in_q)) { - m_todo.pop_back(); - } - else if (visit_children(n, in_q)) { - m_todo.pop_back(); - reduce1(n, in_q); - } - } - expr * r2; - proof * pr2; - get_cached(n, false, r2, pr2); - r = r2; - switch (m_manager.proof_mode()) { - case PGM_DISABLED: - pr = m_manager.mk_undef_proof(); - break; - case PGM_COARSE: - remove_duplicates(m_coarse_proofs); - pr = n == r2 ? m_manager.mk_reflexivity(n) : m_manager.mk_cnf_star(n, r2, m_coarse_proofs.size(), m_coarse_proofs.c_ptr()); - break; - case PGM_FINE: - pr = pr2 == 0 ? m_manager.mk_reflexivity(n) : pr2; - break; - } -} - -void cnf::operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & pr) { - if (m_cnf_mode == CNF_DISABLED) { - r = n; - pr = m_manager.mk_reflexivity(n); - return; - } - - reset(); - reduce(n, r, pr); - for (unsigned i = 0; i < m_todo_defs.size(); i++) { - expr_ref dr(m_manager); - proof_ref dpr(m_manager); - reduce(m_todo_defs.get(i), dr, dpr); - m_result_defs.push_back(dr); - if (m_manager.proofs_enabled()) { - proof * new_pr = m_manager.mk_modus_ponens(m_todo_proofs.get(i), dpr); - m_result_def_proofs.push_back(new_pr); - } - else - m_result_def_proofs.push_back(m_manager.mk_undef_proof()); - } - std::reverse(m_result_defs.begin(), m_result_defs.end()); - new_defs.append(m_result_defs.size(), m_result_defs.c_ptr()); - std::reverse(m_result_def_proofs.begin(), m_result_def_proofs.end()); - new_def_proofs.append(m_result_def_proofs.size(), m_result_def_proofs.c_ptr()); -} - -void cnf::reset() { - m_cache.reset(); - m_todo.reset(); - m_todo_defs.reset(); - m_todo_proofs.reset(); - m_result_defs.reset(); - m_result_def_proofs.reset(); -} diff --git a/src/ast/normal_forms/cnf.h b/src/ast/normal_forms/cnf.h deleted file mode 100644 index 8aa390c48..000000000 --- a/src/ast/normal_forms/cnf.h +++ /dev/null @@ -1,141 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - cnf.h - -Abstract: - - CNF translation - -Author: - - Leonardo de Moura (leonardo) 2008-01-17. - -Revision History: - ---*/ -#ifndef _CNF_H_ -#define _CNF_H_ - -#include"pull_quant.h" -#include"nnf.h" -#include"approx_nat.h" - -/** - \brief CNF translation mode. The cheapest mode is CNF_QUANT, and - the most expensive is CNF_FULL. -*/ -enum cnf_mode { - CNF_DISABLED, /* CNF translator is disabled. - This mode is sufficient when using E-matching. - */ - CNF_QUANT, /* A subformula is put into CNF if it is inside of a - quantifier. - - This mode is sufficient when using Superposition - Calculus. - */ - CNF_OPPORTUNISTIC, /* a subformula is also put in CNF if it is cheap. */ - CNF_FULL /* Everything is put into CNF, new names are introduced - if it is too expensive. */ -}; - -/** - \brief Entry into the todo list of the CNF translator. It is also used as the key in the CNF cache. -*/ -struct cnf_entry { - expr * m_node; - bool m_polarity:1; - bool m_in_q:1; - cnf_entry():m_node(0), m_polarity(false), m_in_q(false) {} - cnf_entry(expr * n, bool p, bool in_q):m_node(n), m_polarity(p), m_in_q(in_q) {} - unsigned hash() const; - bool operator==(cnf_entry const & k) const; -}; - -/** - \brief Cache for CNF transformation. It is a mapping from (expr, polarity, in_q) -> (expr, proof) -*/ -class cnf_cache { -public: - typedef std::pair expr_proof_pair; - - typedef map, default_eq > cache; - - ast_manager & m_manager; - cache m_cache; - -public: - cnf_cache(ast_manager & m); - ~cnf_cache() { reset(); } - void insert(cnf_entry const & k, expr * r, proof * pr); - bool contains(cnf_entry const & k) const { return m_cache.contains(k); } - void get(cnf_entry const & k, expr * & r, proof * & pr) const { expr_proof_pair tmp; m_cache.find(k, tmp); r = tmp.first; pr = tmp.second; } - void reset(); -}; - -/** - \brief Functor for converting expressions into CNF. The functor can - optionally process subformulas nested in quantifiers. New names may be - introduced for subformulas that are too expensive to be put into CNF. - - NNF translation must be applied before converting to CNF. - - - To use CNF_QUANT, we must use at least NNF_QUANT - - To use CNF_OPPORTUNISTIC, we must use at least NNF_QUANT - - To use CNF_FULL, we must use NNF_FULL -*/ -class cnf { - typedef std::pair expr_bool_pair; - ast_manager & m_manager; - defined_names & m_defined_names; - pull_quant m_pull; - cnf_cache m_cache; - svector m_todo; - expr_ref_vector m_todo_defs; - proof_ref_vector m_todo_proofs; - ptr_vector m_result_defs; - ptr_vector m_result_def_proofs; - proof_ref_vector m_coarse_proofs; - - cnf_mode m_cnf_mode; - unsigned m_cnf_factor; - - void cache_result(expr * e, bool in_q, expr * r, proof * pr); - void get_cached(expr * n, bool in_q, expr * & r, proof * & pr) const { m_cache.get(cnf_entry(n, true, in_q), r, pr); } - bool is_cached(expr * n, bool in_q) const { return m_cache.contains(cnf_entry(n, true, in_q)); } - - void visit(expr * n, bool in_q, bool & visited); - bool visit_children(expr * n, bool in_q); - - void get_args(app * n, bool in_q, ptr_buffer & new_args, ptr_buffer & new_arg_prs); - void flat_args(func_decl * d, ptr_buffer const & args, ptr_buffer & flat_args); - approx_nat approx_result_size_for_disj(ptr_buffer const & args); - bool is_too_expensive(approx_nat approx_result_size, ptr_buffer const & args); - void name_args(ptr_buffer const & args, expr_ref_buffer & new_args, proof_ref_buffer & new_arg_prs); - void distribute(app * arg, app * & r, proof * & pr); - void push_quant(quantifier * q, expr * & r, proof * & pr); - void reduce1(expr * n, bool in_q); - void reduce1_or(app * n, bool in_q); - void reduce1_and(app * n, bool in_q); - void reduce1_label(app * n, bool in_q); - void reduce1_quantifier(quantifier * q, bool in_q); - - void reduce(expr * n, expr_ref & r, proof_ref & pr); -public: - cnf(ast_manager & m, defined_names & n, params_ref const & p = params_ref()); - ~cnf(); - void operator()(expr * n, // [IN] expression that should be put into CNF - expr_ref_vector & new_defs, // [OUT] new definitions - proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions - expr_ref & r, // [OUT] resultant expression - proof_ref & p // [OUT] proof for (~ n r) - ); - - void reset(); -}; - -#endif /* _CNF_H_ */ - diff --git a/src/ast/normal_forms/cnf_params.pyg b/src/ast/normal_forms/cnf_params.pyg deleted file mode 100644 index 3383f674a..000000000 --- a/src/ast/normal_forms/cnf_params.pyg +++ /dev/null @@ -1,4 +0,0 @@ -def_module_params('cnf', - export=True, - params=(('mode', UINT, 0, 'CNF translation mode: 0 - disabled, 1 - quantifiers in CNF, 2 - opportunistic, 3 - full'), - ('factor', UINT, 4, 'the maximum number of clauses that can be created when converting a subformula')))