diff --git a/lib/ast.cpp b/lib/ast.cpp index bfb4a09b4..8e878165c 100644 --- a/lib/ast.cpp +++ b/lib/ast.cpp @@ -1370,10 +1370,11 @@ void ast_manager::copy_families_plugins(ast_manager const & from) { decl_plugin * new_p = from.get_plugin(fid)->mk_fresh(); register_plugin(fid, new_p); SASSERT(new_p->get_family_id() == fid); + SASSERT(has_plugin(fid)); } SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid)); SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name)); - SASSERT(from.has_plugin(fid) == has_plugin(fid)); + SASSERT(!from.has_plugin(fid) || has_plugin(fid)); } } diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index 2cfc2af2d..dac877d02 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -1354,16 +1354,18 @@ namespace pdr { m_core_generalizers.push_back(alloc(core_multi_generalizer, *this)); } if (m_params.get_bool(":use-farkas", true) && !is_bool(rules)) { - // TBD: - m.toggle_proof_mode(PGM_FINE); - m_fparams.m_proof_mode = PGM_FINE; - m_fparams.m_arith_bound_prop = BP_NONE; - m_fparams.m_arith_auto_config_simplex = true; - m_fparams.m_arith_propagate_eqs = false; - m_fparams.m_arith_eager_eq_axioms = false; - m_fparams.m_arith_eq_bounds = false; - - // m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams)); + if (m_params.get_bool(":use-proofs", true)) { + m.toggle_proof_mode(PGM_FINE); + m_fparams.m_proof_mode = PGM_FINE; + m_fparams.m_arith_bound_prop = BP_NONE; + m_fparams.m_arith_auto_config_simplex = true; + m_fparams.m_arith_propagate_eqs = false; + m_fparams.m_arith_eager_eq_axioms = false; + m_fparams.m_arith_eq_bounds = false; + } + else { + m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams)); + } } if (m_params.get_bool(":use-farkas-properties", false)) { m_core_generalizers.push_back(alloc(core_farkas_properties_generalizer, *this)); diff --git a/lib/pdr_farkas_learner.cpp b/lib/pdr_farkas_learner.cpp index 0f1df172f..e7b0bca33 100644 --- a/lib/pdr_farkas_learner.cpp +++ b/lib/pdr_farkas_learner.cpp @@ -512,12 +512,10 @@ namespace pdr { for_each_expr(collect_proc, *it); } - proof_ref tmp(root, m); - proof_utils::reduce_hypotheses(tmp); - IF_VERBOSE(2, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(tmp, m) << "\n";); - proof_ref pr(root, m); - permute_unit_resolution(pr); + proof_utils::reduce_hypotheses(pr); + IF_VERBOSE(2, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(pr, m) << "\n";); + proof_utils::permute_unit_resolution(pr); ptr_vector hyprefs; obj_map hypmap; @@ -751,94 +749,6 @@ namespace pdr { } } - // permute unit resolution over Theory lemmas to track premises. - void farkas_learner::permute_unit_resolution(proof_ref& pr) { - expr_ref_vector refs(pr.get_manager()); - obj_map cache; - permute_unit_resolution(refs, cache, pr); - } - - void farkas_learner::permute_unit_resolution(expr_ref_vector& refs, obj_map& cache, proof_ref& pr) { - ast_manager& m = pr.get_manager(); - proof* pr2 = 0; - proof_ref_vector parents(m); - proof_ref prNew(pr); - if (cache.find(pr, pr2)) { - pr = pr2; - return; - } - - for (unsigned i = 0; i < m.get_num_parents(pr); ++i) { - prNew = m.get_parent(pr, i); - permute_unit_resolution(refs, cache, prNew); - parents.push_back(prNew); - } - - prNew = pr; - if (pr->get_decl_kind() == PR_UNIT_RESOLUTION && - parents[0]->get_decl_kind() == PR_TH_LEMMA) { - /* - Unit resolution: - T1: (or l_1 ... l_n l_1' ... l_m') - T2: (not l_1) - ... - T(n+1): (not l_n) - [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') - Th lemma: - T1: (not l_1) - ... - Tn: (not l_n) - [th-lemma T1 ... Tn]: (or l_{n+1} ... l_m) - - Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom. - - Implement conversion: - - T1 |- not l_1 ... Tn |- not l_n - ------------------------------- TH_LEMMA - (or k_1 .. k_m j_1 ... j_m) S1 |- not k_1 ... Sm |- not k_m - -------------------------------------------------------------- UNIT_RESOLUTION - (or j_1 .. j_m) - - - |-> - - T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m - ---------------------------------------------------------------- TH_LEMMA - (or j_1 .. j_m) - - */ - proof_ref_vector premises(m); - proof* thLemma = parents[0].get(); - for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) { - premises.push_back(m.get_parent(thLemma, i)); - } - for (unsigned i = 1; i < parents.size(); ++i) { - premises.push_back(parents[i].get()); - } - parameter const* params = thLemma->get_decl()->get_parameters(); - unsigned num_params = thLemma->get_decl()->get_num_parameters(); - SASSERT(params[0].is_symbol()); - family_id tid = m.get_family_id(params[0].get_symbol()); - SASSERT(tid != null_family_id); - prNew = m.mk_th_lemma(tid, m.get_fact(pr), - premises.size(), premises.c_ptr(), num_params-1, params+1); - } - else { - ptr_vector args; - for (unsigned i = 0; i < parents.size(); ++i) { - args.push_back(parents[i].get()); - } - if (m.has_fact(pr)) { - args.push_back(m.get_fact(pr)); - } - prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr()); - } - - cache.insert(pr, prNew); - refs.push_back(prNew); - pr = prNew; - } bool farkas_learner::is_farkas_lemma(ast_manager& m, expr* e) { app * a; diff --git a/lib/pdr_farkas_learner.h b/lib/pdr_farkas_learner.h index 5ee4625c4..c0303777c 100644 --- a/lib/pdr_farkas_learner.h +++ b/lib/pdr_farkas_learner.h @@ -69,10 +69,6 @@ class farkas_learner { void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, expr_ref_vector& lemmas); - void permute_unit_resolution(proof_ref& pr); - - void permute_unit_resolution(expr_ref_vector& refs, obj_map& cache, proof_ref& pr); - bool is_pure_expr(func_decl_set const& symbs, expr* e) const; static void test(); diff --git a/lib/proof_utils.cpp b/lib/proof_utils.cpp index 35e49c4e1..6143e6746 100644 --- a/lib/proof_utils.cpp +++ b/lib/proof_utils.cpp @@ -196,19 +196,18 @@ public: } m_hypmap.insert(result, new_hyps); m_hyprefs.push_back(new_hyps); - TRACE("proof_utils", - { + TRACE("proof_utils", tout << "New lemma: " << mk_pp(m.get_fact(p), m) << "\n==>\n" << mk_pp(m.get_fact(result), m) << "\n"; if (hyps) { - expr_set::iterator it = hyps->begin(), end = hyps->end(); + expr_set::iterator it = hyps->begin(); + expr_set::iterator end = hyps->end(); for (; it != end; ++it) { tout << "Hypothesis: " << mk_pp(*it, m) << "\n"; } - } - }); - } + }); + break; } case PR_UNIT_RESOLUTION: { @@ -387,3 +386,94 @@ bool proof_utils::is_closed(ast_manager& m, proof* p) { proof_is_closed checker(m); return checker(p); } + + +static void permute_unit_resolution(expr_ref_vector& refs, obj_map& cache, proof_ref& pr) { + ast_manager& m = pr.get_manager(); + proof* pr2 = 0; + proof_ref_vector parents(m); + proof_ref prNew(pr); + if (cache.find(pr, pr2)) { + pr = pr2; + return; + } + + for (unsigned i = 0; i < m.get_num_parents(pr); ++i) { + prNew = m.get_parent(pr, i); + permute_unit_resolution(refs, cache, prNew); + parents.push_back(prNew); + } + + prNew = pr; + if (pr->get_decl_kind() == PR_UNIT_RESOLUTION && + parents[0]->get_decl_kind() == PR_TH_LEMMA) { + /* + Unit resolution: + T1: (or l_1 ... l_n l_1' ... l_m') + T2: (not l_1) + ... + T(n+1): (not l_n) + [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') + Th lemma: + T1: (not l_1) + ... + Tn: (not l_n) + [th-lemma T1 ... Tn]: (or l_{n+1} ... l_m) + + Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom. + + Implement conversion: + + T1 |- not l_1 ... Tn |- not l_n + ------------------------------- TH_LEMMA + (or k_1 .. k_m j_1 ... j_m) S1 |- not k_1 ... Sm |- not k_m + -------------------------------------------------------------- UNIT_RESOLUTION + (or j_1 .. j_m) + + + |-> + + T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m + ---------------------------------------------------------------- TH_LEMMA + (or j_1 .. j_m) + + */ + proof_ref_vector premises(m); + proof* thLemma = parents[0].get(); + for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) { + premises.push_back(m.get_parent(thLemma, i)); + } + for (unsigned i = 1; i < parents.size(); ++i) { + premises.push_back(parents[i].get()); + } + parameter const* params = thLemma->get_decl()->get_parameters(); + unsigned num_params = thLemma->get_decl()->get_num_parameters(); + SASSERT(params[0].is_symbol()); + family_id tid = m.get_family_id(params[0].get_symbol()); + SASSERT(tid != null_family_id); + prNew = m.mk_th_lemma(tid, m.get_fact(pr), + premises.size(), premises.c_ptr(), num_params-1, params+1); + } + else { + ptr_vector args; + for (unsigned i = 0; i < parents.size(); ++i) { + args.push_back(parents[i].get()); + } + if (m.has_fact(pr)) { + args.push_back(m.get_fact(pr)); + } + prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr()); + } + + cache.insert(pr, prNew); + refs.push_back(prNew); + pr = prNew; +} + + +// permute unit resolution over Theory lemmas to track premises. +void proof_utils::permute_unit_resolution(proof_ref& pr) { + expr_ref_vector refs(pr.get_manager()); + obj_map cache; + ::permute_unit_resolution(refs, cache, pr); +} diff --git a/lib/proof_utils.h b/lib/proof_utils.h index 10a73f388..a193f6821 100644 --- a/lib/proof_utils.h +++ b/lib/proof_utils.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Utilities for proofs. + Utilities for transforming proofs. Author: @@ -31,6 +31,11 @@ public: */ static bool is_closed(ast_manager& m, proof* p); + /** + \brief Permute unit resolution rule with th-lemma + */ + static void permute_unit_resolution(proof_ref& pr); + }; #endif _PROOF_UTILS_H_