From 25fad153d11736393c4c5baa80854622dd1139a3 Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Mon, 23 Oct 2017 15:39:59 +0200 Subject: [PATCH] added option fixedpoint.spacer.iuc.debug_proof to debug proof which is used for generation of iuc --- src/muz/base/fixedpoint_params.pyg | 1 + src/muz/spacer/spacer_itp_solver.cpp | 2 +- src/muz/spacer/spacer_itp_solver.h | 7 ++-- src/muz/spacer/spacer_prop_solver.cpp | 4 +-- src/muz/spacer/spacer_unsat_core_learner.cpp | 35 +++++++++++++++----- src/muz/spacer/spacer_unsat_core_learner.h | 3 +- 6 files changed, 36 insertions(+), 16 deletions(-) diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index a46d06245..f0f4e0881 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -186,6 +186,7 @@ def_module_params('fixedpoint', ('spacer.lemma_sanity_check', BOOL, False, 'check during generalization whether lemma is actually correct'), ('spacer.reuse_pobs', BOOL, True, 'reuse POBs'), ('spacer.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut'), + ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes'), ('spacer.simplify_pob', BOOL, False, 'simplify POBs by removing redundant constraints') )) diff --git a/src/muz/spacer/spacer_itp_solver.cpp b/src/muz/spacer/spacer_itp_solver.cpp index c9bf3c443..9cccdf43c 100644 --- a/src/muz/spacer/spacer_itp_solver.cpp +++ b/src/muz/spacer/spacer_itp_solver.cpp @@ -277,7 +277,7 @@ void itp_solver::get_itp_core (expr_ref_vector &core) else { // new code - unsat_core_learner learner(m,m_print_farkas_stats); + unsat_core_learner learner(m, m_print_farkas_stats, m_iuc_debug_proof); if (m_iuc_arith == 0 || m_iuc_arith > 3) { diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index 0b01f0032..5e5c2d39e 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/src/muz/spacer/spacer_itp_solver.h @@ -61,14 +61,14 @@ private: unsigned m_iuc; unsigned m_iuc_arith; bool m_print_farkas_stats; - + bool m_iuc_debug_proof; bool is_proxy(expr *e, app_ref &def); void undo_proxies_in_core(ptr_vector &v); app* mk_proxy(expr *v); app* fresh_proxy(); void elim_proxies(expr_ref_vector &v); public: - itp_solver(solver &solver, unsigned iuc, unsigned iuc_arith, bool print_farkas_stats, bool split_literals = false) : + itp_solver(solver &solver, unsigned iuc, unsigned iuc_arith, bool print_farkas_stats, bool iuc_debug_proof, bool split_literals = false) : m(solver.get_manager()), m_solver(solver), m_proxies(m), @@ -81,7 +81,8 @@ public: m_split_literals(split_literals), m_iuc(iuc), m_iuc_arith(iuc_arith), - m_print_farkas_stats(print_farkas_stats) + m_print_farkas_stats(print_farkas_stats), + m_iuc_debug_proof(iuc_debug_proof) {} ~itp_solver() override {} diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index cf981cfeb..60deac214 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -60,8 +60,8 @@ prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const& m_solvers[1] = pm.mk_fresh2(); m_fparams[1] = &pm.fparams2(); - m_contexts[0] = alloc(spacer::itp_solver, *(m_solvers[0]), p.spacer_iuc(), p.spacer_iuc_arith(), p.spacer_print_farkas_stats(), p.spacer_split_farkas_literals()); - m_contexts[1] = alloc(spacer::itp_solver, *(m_solvers[1]), p.spacer_iuc(), p.spacer_iuc_arith(), p.spacer_print_farkas_stats(), p.spacer_split_farkas_literals()); + m_contexts[0] = alloc(spacer::itp_solver, *(m_solvers[0]), p.spacer_iuc(), p.spacer_iuc_arith(), p.spacer_print_farkas_stats(), p.spacer_iuc_debug_proof(), p.spacer_split_farkas_literals()); + m_contexts[1] = alloc(spacer::itp_solver, *(m_solvers[1]), p.spacer_iuc(), p.spacer_iuc_arith(), p.spacer_print_farkas_stats(), p.spacer_iuc_debug_proof(), p.spacer_split_farkas_literals()); for (unsigned i = 0; i < 2; ++i) { m_contexts[i]->assert_expr(m_pm.get_background()); } diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index cf1eb979f..4adf67209 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/src/muz/spacer/spacer_unsat_core_learner.cpp @@ -174,13 +174,11 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e verbose_stream() << "\nThis proof contains " << farkas_counter << " Farkas lemmas. " << farkas_counter2 << " Farkas lemmas participate in the lowest cut\n"; } - - bool debug_proof = false; - if(debug_proof) + if(m_iuc_debug_proof) { // print proof for debugging - verbose_stream() << "\n\nProof:\n"; + verbose_stream() << "Proof:\n"; std::unordered_map id_to_small_id; unsigned counter = 0; @@ -223,8 +221,23 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e verbose_stream() << "hypothesis"; break; default: - verbose_stream() << "unknown axiom-type"; - break; + if (currentNode->get_decl_kind() == PR_TH_LEMMA) + { + verbose_stream() << "th_axiom"; + func_decl* d = currentNode->get_decl(); + symbol sym; + if (d->get_num_parameters() >= 2 && // the Farkas coefficients are saved in the parameters of step + d->get_parameter(0).is_symbol(sym) && sym == "arith" && // the first two parameters are "arith", "farkas", + d->get_parameter(1).is_symbol(sym) && sym == "farkas") + { + verbose_stream() << "(farkas)"; + } + } + else + { + verbose_stream() << "unknown axiom-type"; + break; + } } } else @@ -269,17 +282,21 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e } } - if (currentNode->get_decl_kind() == PR_TH_LEMMA || (is_a_marked(currentNode) && is_b_marked(currentNode)) || is_h_marked(currentNode) || (!is_a_marked(currentNode) && !is_b_marked(currentNode))) +// if (currentNode->get_decl_kind() == PR_TH_LEMMA || (is_a_marked(currentNode) && is_b_marked(currentNode)) || is_h_marked(currentNode) || (!is_a_marked(currentNode) && !is_b_marked(currentNode))) + if (false) { - verbose_stream() << std::endl; + verbose_stream() << "\n"; } else { - verbose_stream() << ": " << mk_pp(m.get_fact(currentNode), m) << std::endl; + verbose_stream() << ": " << mk_pp(m.get_fact(currentNode), m) << "\n"; } ++counter; } } + + verbose_stream() << std::endl; + // move all lemmas into vector for (expr* const* it = m_unsat_core.begin(); it != m_unsat_core.end(); ++it) { diff --git a/src/muz/spacer/spacer_unsat_core_learner.h b/src/muz/spacer/spacer_unsat_core_learner.h index 2f04a9e06..4b5ca981d 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.h +++ b/src/muz/spacer/spacer_unsat_core_learner.h @@ -31,7 +31,7 @@ namespace spacer { typedef obj_hashtable expr_set; public: - unsat_core_learner(ast_manager& m, bool print_farkas_stats = false) : m(m), m_unsat_core(m), m_print_farkas_stats(print_farkas_stats) {}; + unsat_core_learner(ast_manager& m, bool print_farkas_stats = false, bool iuc_debug_proof = false) : m(m), m_unsat_core(m), m_print_farkas_stats(print_farkas_stats), m_iuc_debug_proof(iuc_debug_proof) {}; virtual ~unsat_core_learner(); ast_manager& m; @@ -102,6 +102,7 @@ namespace spacer { void finalize(); bool m_print_farkas_stats; + bool m_iuc_debug_proof; }; }