From 6195ed7c662f2ff02f0975091ec3ec1f31f16ddd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Nov 2012 18:16:02 -0800 Subject: [PATCH] checkpoint Signed-off-by: Leonardo de Moura --- scripts/mk_project.py | 2 +- src/ast/normal_forms/cnf.cpp | 19 ++-- src/ast/normal_forms/cnf.h | 26 +++++- src/ast/normal_forms/cnf_params.pyg | 4 + src/ast/normal_forms/nnf.cpp | 101 +++++++++++---------- src/ast/normal_forms/nnf.h | 2 - src/ast/normal_forms/nnf_params.pyg | 8 ++ src/front_end_params/cnf_params.cpp | 26 ------ src/front_end_params/cnf_params.h | 56 ------------ src/front_end_params/nnf_params.cpp | 26 ------ src/front_end_params/nnf_params.h | 74 --------------- src/front_end_params/preprocessor_params.h | 6 +- src/front_end_params/smt_params.cpp | 1 - src/front_end_params/smt_params.h | 2 - src/smt/asserted_formulas.cpp | 82 ++++------------- src/smt/smt_context.h | 4 - src/smt/smt_internalizer.cpp | 7 +- 17 files changed, 120 insertions(+), 326 deletions(-) create mode 100644 src/ast/normal_forms/cnf_params.pyg create mode 100644 src/ast/normal_forms/nnf_params.pyg delete mode 100644 src/front_end_params/cnf_params.cpp delete mode 100644 src/front_end_params/cnf_params.h delete mode 100644 src/front_end_params/nnf_params.cpp delete mode 100644 src/front_end_params/nnf_params.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6fff2abba..27120c89d 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -18,6 +18,7 @@ def init_project_def(): add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter') + add_lib('normal_forms', ['rewriter'], 'ast/normal_forms') add_lib('model', ['rewriter']) add_lib('tactic', ['ast', 'model']) add_lib('substitution', ['ast'], 'ast/substitution') @@ -30,7 +31,6 @@ 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', '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') diff --git a/src/ast/normal_forms/cnf.cpp b/src/ast/normal_forms/cnf.cpp index d454c7f00..2a58b16a6 100644 --- a/src/ast/normal_forms/cnf.cpp +++ b/src/ast/normal_forms/cnf.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include"cnf.h" +#include"cnf_params.hpp" #include"var_subst.h" #include"ast_util.h" #include"ast_pp.h" @@ -159,7 +160,7 @@ inline bool cnf::is_too_expensive(approx_nat approx_result_size, 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_params.m_cnf_mode != CNF_OPPORTUNISTIC || result_size < m_params.m_cnf_factor) { + 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)) { @@ -354,7 +355,7 @@ void cnf::reduce1_and(app * n, bool in_q) { get_args(n, in_q, new_args, new_arg_prs); app * r; proof * pr = 0; - if (in_q || m_params.m_cnf_mode == CNF_OPPORTUNISTIC || m_params.m_cnf_mode == CNF_FULL) { + 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()); @@ -379,7 +380,7 @@ void cnf::reduce1_label(app * n, bool in_q) { expr * new_arg; proof * new_arg_pr; get_cached(n->get_arg(0), true, new_arg, new_arg_pr); - if (in_q || m_params.m_cnf_mode == CNF_FULL) { + 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. @@ -439,8 +440,7 @@ void cnf::reduce1_quantifier(quantifier * q, bool in_q) { TRACE("cnf_quant", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";); } -cnf::cnf(ast_manager & m, defined_names & n, cnf_params & params): - m_params(params), +cnf::cnf(ast_manager & m, defined_names & n, params_ref const & params): m_manager(m), m_defined_names(n), m_pull(m), @@ -448,6 +448,9 @@ cnf::cnf(ast_manager & m, defined_names & n, cnf_params & params): 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() { @@ -488,7 +491,7 @@ void cnf::reduce(expr * n, expr_ref & r, proof_ref & pr) { } void cnf::operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & pr) { - if (m_params.m_cnf_mode == CNF_DISABLED) { + if (m_cnf_mode == CNF_DISABLED) { r = n; pr = m_manager.mk_reflexivity(n); return; diff --git a/src/ast/normal_forms/cnf.h b/src/ast/normal_forms/cnf.h index 60c2d2410..8aa390c48 100644 --- a/src/ast/normal_forms/cnf.h +++ b/src/ast/normal_forms/cnf.h @@ -19,11 +19,29 @@ Revision History: #ifndef _CNF_H_ #define _CNF_H_ -#include"cnf_params.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. */ @@ -71,7 +89,6 @@ public: */ class cnf { typedef std::pair expr_bool_pair; - cnf_params & m_params; ast_manager & m_manager; defined_names & m_defined_names; pull_quant m_pull; @@ -83,6 +100,9 @@ class cnf { 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)); } @@ -105,7 +125,7 @@ class cnf { void reduce(expr * n, expr_ref & r, proof_ref & pr); public: - cnf(ast_manager & m, defined_names & n, cnf_params & params); + 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 diff --git a/src/ast/normal_forms/cnf_params.pyg b/src/ast/normal_forms/cnf_params.pyg new file mode 100644 index 000000000..3383f674a --- /dev/null +++ b/src/ast/normal_forms/cnf_params.pyg @@ -0,0 +1,4 @@ +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'))) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index d525fa167..8e0065071 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -18,6 +18,7 @@ Notes: --*/ #include"nnf.h" +#include"nnf_params.hpp" #include"warning.h" #include"used_vars.h" #include"well_sorted.h" @@ -29,6 +30,40 @@ Notes: #include"ast_smt2_pp.h" +/** + \brief NNF translation mode. The cheapest mode is NNF_SKOLEM, and + the most expensive is NNF_FULL. +*/ +enum nnf_mode { + NNF_SKOLEM, /* A subformula is put into NNF only if it contains + quantifiers or labels. The result of the + transformation will be in skolem normal form. + If a formula is too expensive to be put into NNF, + then nested quantifiers and labels are renamed. + + This mode is sufficient when using E-matching. + */ + NNF_QUANT, /* A subformula is put into NNF if it contains + quantifiers, labels, or is in the scope of a + quantifier. The result of the transformation will be + in skolem normal form, and the body of quantifiers + will be in NNF. If a ground formula is too expensive to + be put into NNF, then nested quantifiers and labels + are renamed. + + This mode is sufficient when using Superposition + Calculus. + + Remark: If the problem does not contain quantifiers, + then NNF_QUANT is identical to NNF_SKOLEM. + */ + NNF_OPPORTUNISTIC, /* Similar to NNF_QUANT, but a subformula is + also put into NNF, if it is + cheap. Otherwise, the nested quantifiers and + labels are renamed. */ + NNF_FULL /* Everything is put into NNF. */ +}; + class skolemizer { typedef act_cache cache; @@ -113,20 +148,16 @@ class skolemizer { } public: - skolemizer(ast_manager & m, params_ref const & p): + skolemizer(ast_manager & m): m_manager(m), m_sk_hack("sk_hack"), + m_sk_hack_enabled(false), m_cache(m), m_cache_pr(m) { - updt_params(p); } - void updt_params(params_ref const & p) { - m_sk_hack_enabled = p.get_bool("sk_hack", false); - } - - static void get_param_descrs(param_descrs & r) { - r.insert("sk_hack", CPK_BOOL, "(default: false) hack for VCC"); + void set_sk_hack(bool f) { + m_sk_hack_enabled = f; } ast_manager & m() const { return m_manager; } @@ -220,8 +251,6 @@ struct nnf::imp { name_exprs * m_name_nested_formulas; name_exprs * m_name_quant; - symbol m_skolem; - volatile bool m_cancel; unsigned long long m_max_memory; // in bytes @@ -231,10 +260,9 @@ struct nnf::imp { m_todo_defs(m), m_todo_proofs(m), m_result_pr_stack(m), - m_skolemizer(m, p), - m_skolem("skolem"), + m_skolemizer(m), m_cancel(false) { - updt_local_params(p); + updt_params(p); for (unsigned i = 0; i < 4; i++) { m_cache[i] = alloc(act_cache, m); if (m.proofs_enabled()) @@ -258,14 +286,10 @@ struct nnf::imp { del_name_exprs(m_name_quant); } - void updt_params(params_ref const & p) { - updt_local_params(p); - m_skolemizer.updt_params(p); - } - - void updt_local_params(params_ref const & p) { - symbol mode_sym = p.get_sym("mode", m_skolem); - if (mode_sym == m_skolem) + void updt_params(params_ref const & _p) { + nnf_params p(_p); + symbol mode_sym = p.mode(); + if (mode_sym == "skolem") m_mode = NNF_SKOLEM; else if (mode_sym == "full") m_mode = NNF_FULL; @@ -273,23 +297,17 @@ struct nnf::imp { m_mode = NNF_QUANT; else throw nnf_params_exception("invalid NNF mode"); + + TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";); - TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << p << "\n";); - - m_ignore_labels = p.get_bool("ignore_labels", false); - m_skolemize = p.get_bool("skolemize", true); - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_ignore_labels = p.ignore_labels(); + m_skolemize = p.skolemize(); + m_max_memory = megabytes_to_bytes(p.max_memory()); + m_skolemizer.set_sk_hack(p.sk_hack()); } static void get_param_descrs(param_descrs & r) { - insert_max_memory(r); - r.insert("mode", CPK_SYMBOL, - "(default: skolem) NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full"); - r.insert("ignore_labels", CPK_BOOL, - "(default: false) remove/ignore labels in the input formula, this option is ignored if proofs are enabled"); - r.insert("skolemize", CPK_BOOL, - "(default: true) skolemize (existential force) quantifiers"); - skolemizer::get_param_descrs(r); + nnf_params::collect_param_descrs(r); } void reset() { @@ -881,21 +899,6 @@ nnf::nnf(ast_manager & m, defined_names & n, params_ref const & p) { m_imp = alloc(imp, m, n, p); } -nnf::nnf(ast_manager & m, defined_names & n, nnf_params & np) { - params_ref p; - if (np.m_nnf_mode == NNF_FULL) - p.set_sym("mode", symbol("full")); - else if (np.m_nnf_mode == NNF_QUANT) - p.set_sym("mode", symbol("quantifiers")); - - if (np.m_nnf_ignore_labels) - p.set_bool("ignore_labels", true); - - if (np.m_nnf_sk_hack) - p.set_bool("sk_hack", true); - m_imp = alloc(imp, m, n, p); -} - nnf::~nnf() { dealloc(m_imp); } diff --git a/src/ast/normal_forms/nnf.h b/src/ast/normal_forms/nnf.h index 96807afc0..e8296e933 100644 --- a/src/ast/normal_forms/nnf.h +++ b/src/ast/normal_forms/nnf.h @@ -21,7 +21,6 @@ Notes: #define _NNF_H_ #include"ast.h" -#include"nnf_params.h" #include"params.h" #include"defined_names.h" @@ -30,7 +29,6 @@ class nnf { imp * m_imp; public: nnf(ast_manager & m, defined_names & n, params_ref const & p = params_ref()); - nnf(ast_manager & m, defined_names & n, nnf_params & params); // for backward compatibility ~nnf(); void operator()(expr * n, // [IN] expression that should be put into NNF diff --git a/src/ast/normal_forms/nnf_params.pyg b/src/ast/normal_forms/nnf_params.pyg new file mode 100644 index 000000000..6fab28f11 --- /dev/null +++ b/src/ast/normal_forms/nnf_params.pyg @@ -0,0 +1,8 @@ +def_module_params('nnf', + export=True, + params=(max_memory_param(), + ('sk_hack', BOOL, False, 'hack for VCC'), + ('mode', SYMBOL, 'skolem', + 'NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full'), + ('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled'), + ('skolemize', BOOL, True, 'skolemize (existential force) quantifiers'))) diff --git a/src/front_end_params/cnf_params.cpp b/src/front_end_params/cnf_params.cpp deleted file mode 100644 index fffd698a6..000000000 --- a/src/front_end_params/cnf_params.cpp +++ /dev/null @@ -1,26 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - cnf_params.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-01-23. - -Revision History: - ---*/ - -#include"cnf_params.h" - -void cnf_params::register_params(ini_params & p) { - p.register_unsigned_param("cnf_factor", m_cnf_factor, "the maximum number of clauses that can be created when converting a subformula"); - p.register_int_param("cnf_mode", 0, 3, reinterpret_cast(m_cnf_mode), "CNF translation mode: 0 - disabled, 1 - quantifiers in CNF, 2 - 0 + opportunistic, 3 - full"); -} - diff --git a/src/front_end_params/cnf_params.h b/src/front_end_params/cnf_params.h deleted file mode 100644 index f694e1716..000000000 --- a/src/front_end_params/cnf_params.h +++ /dev/null @@ -1,56 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - cnf_params.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-01-23. - -Revision History: - ---*/ -#ifndef _CNF_PARAMS_H_ -#define _CNF_PARAMS_H_ - -#include"ini_file.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. */ -}; - -struct cnf_params { - cnf_mode m_cnf_mode; - unsigned m_cnf_factor; - cnf_params(): - m_cnf_mode(CNF_DISABLED), - m_cnf_factor(4) { - } - - void register_params(ini_params & p); -}; - - -#endif /* _CNF_PARAMS_H_ */ - diff --git a/src/front_end_params/nnf_params.cpp b/src/front_end_params/nnf_params.cpp deleted file mode 100644 index 351997f98..000000000 --- a/src/front_end_params/nnf_params.cpp +++ /dev/null @@ -1,26 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - nnf_params.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-01-14. - -Revision History: - ---*/ -#include"nnf_params.h" - -void nnf_params::register_params(ini_params & p) { - p.register_unsigned_param("nnf_factor", m_nnf_factor, "the maximum growth factor during NNF translation (auxiliary definitions are introduced if the threshold is reached)"); - p.register_int_param("nnf_mode", 0, 3, reinterpret_cast(m_nnf_mode), "NNF translation mode: 0 - skolem normal form, 1 - 0 + quantifiers in NNF, 2 - 1 + opportunistic, 3 - full"); - p.register_bool_param("nnf_ignore_labels", m_nnf_ignore_labels, "remove/ignore labels in the input formula, this option is ignored if proofs are enabled"); - p.register_bool_param("nnf_sk_hack", m_nnf_sk_hack, "hack for VCC"); -} diff --git a/src/front_end_params/nnf_params.h b/src/front_end_params/nnf_params.h deleted file mode 100644 index f759a93ac..000000000 --- a/src/front_end_params/nnf_params.h +++ /dev/null @@ -1,74 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - nnf_params.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-01-14. - -Revision History: - ---*/ -#ifndef _NNF_PARAMS_H_ -#define _NNF_PARAMS_H_ - -#include"ini_file.h" - -/** - \brief NNF translation mode. The cheapest mode is NNF_SKOLEM, and - the most expensive is NNF_FULL. -*/ -enum nnf_mode { - NNF_SKOLEM, /* A subformula is put into NNF only if it contains - quantifiers or labels. The result of the - transformation will be in skolem normal form. - If a formula is too expensive to be put into NNF, - then nested quantifiers and labels are renamed. - - This mode is sufficient when using E-matching. - */ - NNF_QUANT, /* A subformula is put into NNF if it contains - quantifiers, labels, or is in the scope of a - quantifier. The result of the transformation will be - in skolem normal form, and the body of quantifiers - will be in NNF. If a ground formula is too expensive to - be put into NNF, then nested quantifiers and labels - are renamed. - - This mode is sufficient when using Superposition - Calculus. - - Remark: If the problem does not contain quantifiers, - then NNF_QUANT is identical to NNF_SKOLEM. - */ - NNF_OPPORTUNISTIC, /* Similar to NNF_QUANT, but a subformula is - also put into NNF, if it is - cheap. Otherwise, the nested quantifiers and - labels are renamed. */ - NNF_FULL /* Everything is put into NNF. */ -}; - -struct nnf_params { - nnf_mode m_nnf_mode; - unsigned m_nnf_factor; - bool m_nnf_ignore_labels; - bool m_nnf_sk_hack; - nnf_params(): - m_nnf_mode(NNF_SKOLEM), - m_nnf_factor(4), - m_nnf_ignore_labels(false), - m_nnf_sk_hack(false) { - } - - void register_params(ini_params & p); -}; - -#endif /* _NNF_PARAMS_H_ */ - diff --git a/src/front_end_params/preprocessor_params.h b/src/front_end_params/preprocessor_params.h index 89bd01b48..00466bc02 100644 --- a/src/front_end_params/preprocessor_params.h +++ b/src/front_end_params/preprocessor_params.h @@ -19,8 +19,6 @@ Revision History: #ifndef _PREPROCESSOR_PARAMS_H_ #define _PREPROCESSOR_PARAMS_H_ -#include"nnf_params.h" -#include"cnf_params.h" #include"pattern_inference_params.h" #include"bit_blaster_params.h" #include"bv_simplifier_params.h" @@ -31,7 +29,7 @@ enum lift_ite_kind { LI_FULL }; -struct preprocessor_params : public nnf_params, public cnf_params, public pattern_inference_params, +struct preprocessor_params : public pattern_inference_params, public bit_blaster_params, public bv_simplifier_params { lift_ite_kind m_lift_ite; lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms @@ -79,8 +77,6 @@ public: } void register_params(ini_params & p) { - nnf_params::register_params(p); - cnf_params::register_params(p); pattern_inference_params::register_params(p); bit_blaster_params::register_params(p); bv_simplifier_params::register_params(p); diff --git a/src/front_end_params/smt_params.cpp b/src/front_end_params/smt_params.cpp index 14db6020a..74e279ff8 100644 --- a/src/front_end_params/smt_params.cpp +++ b/src/front_end_params/smt_params.cpp @@ -31,7 +31,6 @@ void smt_params::register_params(ini_params & p) { p.register_bool_param("display_proof", m_display_proof); p.register_bool_param("display_dot_proof", m_display_dot_proof); p.register_bool_param("display_unsat_core", m_display_unsat_core); - p.register_bool_param("internalizer_nnf", m_internalizer_nnf); p.register_bool_param("eq_propagation", m_eq_propagation); p.register_bool_param("bin_clauses", m_binary_clause_opt); p.register_unsigned_param("relevancy", m_relevancy_lvl, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant", true); diff --git a/src/front_end_params/smt_params.h b/src/front_end_params/smt_params.h index 20a150c64..5c62c49e3 100644 --- a/src/front_end_params/smt_params.h +++ b/src/front_end_params/smt_params.h @@ -72,7 +72,6 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith bool m_display_dot_proof; bool m_display_unsat_core; bool m_check_proof; - bool m_internalizer_nnf; bool m_eq_propagation; bool m_binary_clause_opt; unsigned m_relevancy_lvl; @@ -193,7 +192,6 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith m_display_dot_proof(false), m_display_unsat_core(false), m_check_proof(false), - m_internalizer_nnf(false), m_eq_propagation(true), m_binary_clause_opt(true), m_relevancy_lvl(2), diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 15b49ee32..c548eca94 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -25,12 +25,12 @@ Revision History: #include"bv_simplifier_plugin.h" #include"for_each_expr.h" #include"well_sorted.h" +#include"pull_quant.h" #include"pull_ite_tree.h" #include"push_app_ite.h" #include"elim_term_ite.h" #include"pattern_inference.h" #include"nnf.h" -#include"cnf.h" #include"bv_elim.h" #include"inj_axiom.h" #include"der.h" @@ -86,22 +86,6 @@ void asserted_formulas::setup() { if (m_params.m_relevancy_lvl == 0) m_params.m_relevancy_lemma = false; - - switch (m_params.m_cnf_mode) { - case CNF_QUANT: - if (m_params.m_nnf_mode == NNF_SKOLEM) - m_params.m_nnf_mode = NNF_QUANT; - break; - case CNF_OPPORTUNISTIC: - if (m_params.m_nnf_mode == NNF_SKOLEM) - m_params.m_nnf_mode = NNF_QUANT; - break; - case CNF_FULL: - m_params.m_nnf_mode = NNF_FULL; - break; - default: - break; - } } void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp) { @@ -439,13 +423,10 @@ void asserted_formulas::apply_quasi_macros() { } void asserted_formulas::nnf_cnf() { - IF_IVERBOSE(10, verbose_stream() << "applying nnf&cnf...\n";); - nnf apply_nnf(m_manager, m_defined_names, m_params); - cnf apply_cnf(m_manager, m_defined_names, m_params); + IF_IVERBOSE(10, verbose_stream() << "applying nnf...\n";); + nnf apply_nnf(m_manager, m_defined_names); expr_ref_vector new_exprs(m_manager); proof_ref_vector new_prs(m_manager); - expr_ref_vector cnf_todo(m_manager); - proof_ref_vector cnf_todo_prs(m_manager); expr_ref_vector push_todo(m_manager); proof_ref_vector push_todo_prs(m_manager); @@ -456,60 +437,33 @@ void asserted_formulas::nnf_cnf() { expr * n = m_asserted_formulas.get(i); TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m_manager) << "\n";); proof * pr = m_asserted_formula_prs.get(i, 0); - cnf_todo.reset(); - cnf_todo_prs.reset(); expr_ref r1(m_manager); proof_ref pr1(m_manager); CASSERT("well_sorted",is_well_sorted(m_manager, n)); - apply_nnf(n, cnf_todo, cnf_todo_prs, r1, pr1); + apply_nnf(n, push_todo, push_todo_prs, r1, pr1); CASSERT("well_sorted",is_well_sorted(m_manager, r1)); pr = m_manager.mk_modus_ponens(pr, pr1); - cnf_todo.push_back(r1); - cnf_todo_prs.push_back(pr); + push_todo.push_back(r1); + push_todo_prs.push_back(pr); if (canceled()) { return; } - - unsigned sz1 = cnf_todo.size(); - for (unsigned j = 0; j < sz1; j++) { - push_todo.reset(); - push_todo_prs.reset(); - + unsigned sz2 = push_todo.size(); + for (unsigned k = 0; k < sz2; k++) { + expr * n = push_todo.get(k); + proof * pr = 0; + m_simplifier(n, r1, pr1); + CASSERT("well_sorted",is_well_sorted(m_manager, r1)); if (canceled()) { return; } - - expr * n = cnf_todo.get(j); - proof * pr = m_manager.proofs_enabled() ? cnf_todo_prs.get(j) : 0; - - CASSERT("well_sorted",is_well_sorted(m_manager, n)); - apply_cnf(n, push_todo, push_todo_prs, r1, pr1); - CASSERT("well_sorted",is_well_sorted(m_manager, r1)); - - push_todo.push_back(r1); - - if (m_manager.proofs_enabled()) { - pr = m_manager.mk_modus_ponens(pr, pr1); - push_todo_prs.push_back(pr); - } - - unsigned sz2 = push_todo.size(); - for (unsigned k = 0; k < sz2; k++) { - expr * n = push_todo.get(k); - proof * pr = 0; - m_simplifier(n, r1, pr1); - CASSERT("well_sorted",is_well_sorted(m_manager, r1)); - if (canceled()) { - return; - } - - if (m_manager.proofs_enabled()) - pr = m_manager.mk_modus_ponens(push_todo_prs.get(k), pr1); - else - pr = 0; - push_assertion(r1, pr, new_exprs, new_prs); - } + + if (m_manager.proofs_enabled()) + pr = m_manager.mk_modus_ponens(push_todo_prs.get(k), pr1); + else + pr = 0; + push_assertion(r1, pr, new_exprs, new_prs); } } swap_asserted_formulas(new_exprs, new_prs); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index b44d42fc8..132718e9a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -654,10 +654,6 @@ namespace smt { protected: unsigned m_generation; //!< temporary variable used during internalization - bool expand_pos_def_only() const { - return m_fparams.m_nnf_mode == NNF_FULL && m_fparams.m_internalizer_nnf; - } - public: bool binary_clause_opt_enabled() const { return !m_manager.proofs_enabled() && m_fparams.m_binary_clause_opt; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 86b1641bc..0cfe5b1de 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1566,9 +1566,7 @@ namespace smt { mk_gate_clause(~l, l_arg); buffer.push_back(~l_arg); } - if (!expand_pos_def_only()) { - mk_gate_clause(buffer.size(), buffer.c_ptr()); - } + mk_gate_clause(buffer.size(), buffer.c_ptr()); } void context::mk_or_cnstr(app * n) { @@ -1578,8 +1576,7 @@ namespace smt { unsigned num_args = n->get_num_args(); for (unsigned i = 0; i < num_args; i++) { literal l_arg = get_literal(n->get_arg(i)); - if (!expand_pos_def_only()) - mk_gate_clause(l, ~l_arg); + mk_gate_clause(l, ~l_arg); buffer.push_back(l_arg); } mk_gate_clause(buffer.size(), buffer.c_ptr());