diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 74903baf1..65d89e420 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -182,7 +182,8 @@ def_module_params('fixedpoint', ('spacer.instantiate', BOOL, True, 'instantiate quantified lemmas'), ('spacer.qlemmas', BOOL, True, 'allow quantified lemmas in frames'), ('spacer.iuc', UINT, 1, '0 = use old implementation of unsat-core-generation, 1 = use new implementation of IUC generation, 2 = use new implementation of IUC + min-cut optimization'), - ('spacer.iuc.arith', UINT, 2, '0 = use simple Farkas plugin, 1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation), 2 = use Gaussian elimination optimization, 3 = use additive IUC plugin'), + ('spacer.iuc.arith', UINT, 2, '0 = use simple Farkas plugin, 1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation), 2 = use Gaussian elimination optimization, 3 = use additive IUC plugin'), + ('spacer.old_hyp_reducer', BOOL, False, 'use old hyp reducer instead of new implementation, for debugging only'), ('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'), diff --git a/src/muz/spacer/spacer_itp_solver.cpp b/src/muz/spacer/spacer_itp_solver.cpp index 187a4a30f..35e06f9a2 100644 --- a/src/muz/spacer/spacer_itp_solver.cpp +++ b/src/muz/spacer/spacer_itp_solver.cpp @@ -19,6 +19,7 @@ Notes: #include"muz/spacer/spacer_itp_solver.h" #include"ast/ast.h" #include"muz/spacer/spacer_util.h" +#include"muz/base/proof_utils.h" #include"muz/spacer/spacer_farkas_learner.h" #include"ast/rewriter/expr_replacer.h" #include"muz/spacer/spacer_unsat_core_learner.h" @@ -277,39 +278,56 @@ void itp_solver::get_itp_core (expr_ref_vector &core) } else { + proof_ref res(get_proof(),m); + // new code - // preprocess proof in order to get a proof which is better suited for unsat-core-extraction - proof_ref pr(get_proof(), m); - - if (m_print_farkas_stats) + if (m_old_hyp_reducer) { - iuc_proof iuc_before(m, pr.get(), B); - verbose_stream() << "Stats before transformation:"; - iuc_before.print_farkas_stats(); + // preprocess proof in order to get a proof which is better suited for unsat-core-extraction + if (m_print_farkas_stats) + { + iuc_proof iuc_before(m, res.get(), B); + verbose_stream() << "\nStats before transformation:"; + iuc_before.print_farkas_stats(); + } + + proof_utils::reduce_hypotheses(res); + proof_utils::permute_unit_resolution(res); + + if (m_print_farkas_stats) + { + iuc_proof iuc_after(m, res.get(), B); + verbose_stream() << "Stats after transformation:"; + iuc_after.print_farkas_stats(); + } } - - theory_axiom_reducer ta_reducer(m); - proof_ref pr_without_theory_lemmas = ta_reducer.reduce(pr.get()); - - if (m_print_farkas_stats) + else { - iuc_proof iuc_mid(m, pr_without_theory_lemmas.get(), B); - verbose_stream() << "Stats after first transformation:"; - iuc_mid.print_farkas_stats(); + // preprocess proof in order to get a proof which is better suited for unsat-core-extraction + if (m_print_farkas_stats) + { + iuc_proof iuc_before(m, res.get(), B); + verbose_stream() << "\nStats before transformation:"; + iuc_before.print_farkas_stats(); + } + + theory_axiom_reducer ta_reducer(m); + proof_ref pr_without_theory_lemmas = ta_reducer.reduce(res.get()); + + hypothesis_reducer hyp_reducer(m); + proof_ref pr_with_less_hypothesis = hyp_reducer.reduce(pr_without_theory_lemmas); + + if (m_print_farkas_stats) + { + iuc_proof iuc_after(m, pr_with_less_hypothesis.get(), B); + verbose_stream() << "Stats after transformation:"; + iuc_after.print_farkas_stats(); + } + res = pr_with_less_hypothesis; } - - hypothesis_reducer hyp_reducer(m); - proof_ref pr_with_less_hypothesis = hyp_reducer.reduce(pr_without_theory_lemmas); - - if (m_print_farkas_stats) - { - iuc_proof iuc_after(m, pr_with_less_hypothesis.get(), B); - verbose_stream() << "Stats after second transformation:"; - iuc_after.print_farkas_stats(); - } - + // construct proof object with contains partition information - iuc_proof iuc_pr(m, pr_with_less_hypothesis, B); + iuc_proof iuc_pr(m, res, B); // configure learner unsat_core_learner learner(m, iuc_pr, m_print_farkas_stats, m_iuc_debug_proof); diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index 5e5c2d39e..6f6a2bf8f 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/src/muz/spacer/spacer_itp_solver.h @@ -62,13 +62,14 @@ private: unsigned m_iuc_arith; bool m_print_farkas_stats; bool m_iuc_debug_proof; + bool m_old_hyp_reducer; 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 iuc_debug_proof, bool split_literals = false) : + itp_solver(solver &solver, unsigned iuc, unsigned iuc_arith, bool print_farkas_stats, bool iuc_debug_proof, bool old_hyp_reducer, bool split_literals = false) : m(solver.get_manager()), m_solver(solver), m_proxies(m), @@ -82,7 +83,8 @@ public: m_iuc(iuc), m_iuc_arith(iuc_arith), m_print_farkas_stats(print_farkas_stats), - m_iuc_debug_proof(iuc_debug_proof) + m_iuc_debug_proof(iuc_debug_proof), + m_old_hyp_reducer(old_hyp_reducer) {} ~itp_solver() override {} diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 60deac214..03c9b858b 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_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()); + 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_old_hyp_reducer(), 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_old_hyp_reducer(), p.spacer_split_farkas_literals()); for (unsigned i = 0; i < 2; ++i) { m_contexts[i]->assert_expr(m_pm.get_background()); }