From f0f75d525415adc8cdb309dea50353e768e32ee7 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 15 May 2018 10:42:57 -0700 Subject: [PATCH] Wire in arith-axiom-reducer --- src/muz/spacer/spacer_itp_solver.cpp | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/src/muz/spacer/spacer_itp_solver.cpp b/src/muz/spacer/spacer_itp_solver.cpp index 9c11e0c1c..187a4a30f 100644 --- a/src/muz/spacer/spacer_itp_solver.cpp +++ b/src/muz/spacer/spacer_itp_solver.cpp @@ -287,23 +287,29 @@ void itp_solver::get_itp_core (expr_ref_vector &core) verbose_stream() << "Stats before transformation:"; iuc_before.print_farkas_stats(); } - - spacer::reduce_hypotheses(pr); - spacer::reduce_hypotheses(pr); - + + theory_axiom_reducer ta_reducer(m); + proof_ref pr_without_theory_lemmas = ta_reducer.reduce(pr.get()); + if (m_print_farkas_stats) { - iuc_proof iuc_after(m, pr.get(), B); - verbose_stream() << "Stats after transformation:"; + iuc_proof iuc_mid(m, pr_without_theory_lemmas.get(), B); + verbose_stream() << "Stats after first transformation:"; + iuc_mid.print_farkas_stats(); + } + + 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(); } - STRACE("spacer.unsat_core_learner", - verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n"; - ); - // construct proof object with contains partition information - iuc_proof iuc_pr(m, pr.get(), B); + iuc_proof iuc_pr(m, pr_with_less_hypothesis, B); // configure learner unsat_core_learner learner(m, iuc_pr, m_print_farkas_stats, m_iuc_debug_proof);