diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index d1a23dcdd..a46d06245 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -181,9 +181,8 @@ def_module_params('fixedpoint', ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), ('spacer.instantiate', BOOL, True, 'instantiate quantified lemmas'), ('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_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.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.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 7af5c21fc..c9bf3c443 100644 --- a/src/muz/spacer/spacer_itp_solver.cpp +++ b/src/muz/spacer/spacer_itp_solver.cpp @@ -264,7 +264,8 @@ void itp_solver::get_itp_core (expr_ref_vector &core) proof_ref pr(m); pr = get_proof (); - if (!m_new_unsat_core) { + if (m_iuc == 0) + { // old code farkas_learner learner_old; learner_old.set_split_literals(m_split_literals); @@ -272,35 +273,40 @@ void itp_solver::get_itp_core (expr_ref_vector &core) learner_old.get_lemmas (pr, B, core); elim_proxies (core); simplify_bounds (core); // XXX potentially redundant - } else { + } + else + { // new code unsat_core_learner learner(m,m_print_farkas_stats); - if (m_farkas_plugin == 0 || m_farkas_plugin > 3) + if (m_iuc_arith == 0 || m_iuc_arith > 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) + else if (m_iuc_arith == 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) + else if (m_iuc_arith == 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) + else if(m_iuc_arith == 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) { + if (m_iuc == 2) + { unsat_core_plugin_min_cut* plugin_min_cut = alloc(unsat_core_plugin_min_cut, learner, m); learner.register_plugin(plugin_min_cut); - } else { + } + else + { unsat_core_plugin_lemma* plugin_lemma = alloc(unsat_core_plugin_lemma, learner); learner.register_plugin(plugin_lemma); } diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index 719eb3f7c..0b01f0032 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/src/muz/spacer/spacer_itp_solver.h @@ -58,9 +58,8 @@ private: expr_substitution m_elim_proxies_sub; bool m_split_literals; - bool m_new_unsat_core; - bool m_minimize_unsat_core; - unsigned m_farkas_plugin; + unsigned m_iuc; + unsigned m_iuc_arith; bool m_print_farkas_stats; bool is_proxy(expr *e, app_ref &def); @@ -69,7 +68,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, unsigned farkas_plugin, bool print_farkas_stats, bool split_literals = false) : + itp_solver(solver &solver, unsigned iuc, unsigned iuc_arith, bool print_farkas_stats, bool split_literals = false) : m(solver.get_manager()), m_solver(solver), m_proxies(m), @@ -80,9 +79,8 @@ public: m_is_proxied(false), m_elim_proxies_sub(m, false, true), m_split_literals(split_literals), - m_new_unsat_core(new_unsat_core), - m_minimize_unsat_core(minimize_unsat_core), - m_farkas_plugin(farkas_plugin), + m_iuc(iuc), + m_iuc_arith(iuc_arith), 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 1e44921f1..cf981cfeb 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_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()); + 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()); for (unsigned i = 0; i < 2; ++i) { m_contexts[i]->assert_expr(m_pm.get_background()); }