From fba995294d8b288643c09b3cb1a5f3fabbc48343 Mon Sep 17 00:00:00 2001 From: Bernhard Gleiss Date: Thu, 12 Oct 2017 17:01:30 +0200 Subject: [PATCH] refactored options regarding farkas lemma handling --- src/muz/base/fixedpoint_params.pyg | 3 +-- src/muz/spacer/spacer_itp_solver.cpp | 34 +++++++++++++++------------ src/muz/spacer/spacer_itp_solver.h | 8 +++---- src/muz/spacer/spacer_prop_solver.cpp | 4 ++-- 4 files changed, 25 insertions(+), 24 deletions(-) diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 94c5a8989..d1a23dcdd 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -183,8 +183,7 @@ def_module_params('fixedpoint', ('spacer.qlemmas', BOOL, True, 'allow quantified lemmas in frames'), ('spacer.new_unsat_core', BOOL, True, 'use the new implementation of unsat-core-generation'), ('spacer.minimize_unsat_core', BOOL, False, 'compute unsat-core by min-cut'), - ('spacer.farkas_optimized', BOOL, True, 'use the optimized farkas plugin, which performs gaussian elimination'), - ('spacer.farkas_a_const', BOOL, True, 'if the unoptimized farkas plugin is used, use the constants from A while constructing unsat_cores'), + ('spacer.farkas_plugin', UINT, 2, '0 = use unoptimized Farkas plugin, 1 = use unoptimized Farkas plugin with flipped polarity, 2 = use Gaussian elimination ideas, 3 = use additive IUC plugin'), ('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 cf481f179..7af5c21fc 100644 --- a/src/muz/spacer/spacer_itp_solver.cpp +++ b/src/muz/spacer/spacer_itp_solver.cpp @@ -276,23 +276,27 @@ void itp_solver::get_itp_core (expr_ref_vector &core) // new code unsat_core_learner learner(m,m_print_farkas_stats); - if (m_farkas_optimized) { - if (true) // TODO: proper options - { - unsat_core_plugin_farkas_lemma_optimized* plugin_farkas_lemma_optimized = alloc(unsat_core_plugin_farkas_lemma_optimized, learner,m); - learner.register_plugin(plugin_farkas_lemma_optimized); - } - else - { - unsat_core_plugin_farkas_lemma_bounded* plugin_farkas_lemma_bounded = alloc(unsat_core_plugin_farkas_lemma_bounded, learner,m); - learner.register_plugin(plugin_farkas_lemma_bounded); - } - - } else { - unsat_core_plugin_farkas_lemma* plugin_farkas_lemma = alloc(unsat_core_plugin_farkas_lemma, learner, m_split_literals, m_farkas_a_const); + if (m_farkas_plugin == 0 || m_farkas_plugin > 3) + { + unsat_core_plugin_farkas_lemma* plugin_farkas_lemma = alloc(unsat_core_plugin_farkas_lemma, learner, m_split_literals, false); learner.register_plugin(plugin_farkas_lemma); } - + else if (m_farkas_plugin == 1) + { + unsat_core_plugin_farkas_lemma* plugin_farkas_lemma = alloc(unsat_core_plugin_farkas_lemma, learner, m_split_literals, true); + learner.register_plugin(plugin_farkas_lemma); + } + else if (m_farkas_plugin == 2) + { + unsat_core_plugin_farkas_lemma_optimized* plugin_farkas_lemma_optimized = alloc(unsat_core_plugin_farkas_lemma_optimized, learner,m); + learner.register_plugin(plugin_farkas_lemma_optimized); + } + else if(m_farkas_plugin == 3) + { + unsat_core_plugin_farkas_lemma_bounded* plugin_farkas_lemma_bounded = alloc(unsat_core_plugin_farkas_lemma_bounded, learner,m); + learner.register_plugin(plugin_farkas_lemma_bounded); + } + if (m_minimize_unsat_core) { unsat_core_plugin_min_cut* plugin_min_cut = alloc(unsat_core_plugin_min_cut, learner, m); learner.register_plugin(plugin_min_cut); diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index 4245332d2..719eb3f7c 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/src/muz/spacer/spacer_itp_solver.h @@ -60,8 +60,7 @@ private: bool m_split_literals; bool m_new_unsat_core; bool m_minimize_unsat_core; - bool m_farkas_optimized; - bool m_farkas_a_const; + unsigned m_farkas_plugin; bool m_print_farkas_stats; bool is_proxy(expr *e, app_ref &def); @@ -70,7 +69,7 @@ private: app* fresh_proxy(); void elim_proxies(expr_ref_vector &v); public: - itp_solver(solver &solver, bool new_unsat_core, bool minimize_unsat_core, bool farkas_optimized, bool farkas_a_const, bool print_farkas_stats, bool split_literals = false) : + itp_solver(solver &solver, bool new_unsat_core, bool minimize_unsat_core, unsigned farkas_plugin, bool print_farkas_stats, bool split_literals = false) : m(solver.get_manager()), m_solver(solver), m_proxies(m), @@ -83,8 +82,7 @@ public: m_split_literals(split_literals), m_new_unsat_core(new_unsat_core), m_minimize_unsat_core(minimize_unsat_core), - m_farkas_optimized(farkas_optimized), - m_farkas_a_const(farkas_a_const), + m_farkas_plugin(farkas_plugin), m_print_farkas_stats(print_farkas_stats) {} diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 239e8d7f0..1e44921f1 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_new_unsat_core(), p.spacer_minimize_unsat_core(), p.spacer_farkas_optimized(), p.spacer_farkas_a_const(), p.spacer_print_farkas_stats(), p.spacer_split_farkas_literals()); - m_contexts[1] = alloc(spacer::itp_solver, *(m_solvers[1]), p.spacer_new_unsat_core(), p.spacer_minimize_unsat_core(), p.spacer_farkas_optimized(), p.spacer_farkas_a_const(), p.spacer_split_farkas_literals()); + m_contexts[0] = alloc(spacer::itp_solver, *(m_solvers[0]), p.spacer_new_unsat_core(), p.spacer_minimize_unsat_core(), p.spacer_farkas_plugin(), p.spacer_print_farkas_stats(), p.spacer_split_farkas_literals()); + m_contexts[1] = alloc(spacer::itp_solver, *(m_solvers[1]), p.spacer_new_unsat_core(), p.spacer_minimize_unsat_core(), p.spacer_farkas_plugin(), p.spacer_print_farkas_stats(), p.spacer_split_farkas_literals()); for (unsigned i = 0; i < 2; ++i) { m_contexts[i]->assert_expr(m_pm.get_background()); }