mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

refactored options regarding farkas lemma handling

Browse source
This commit is contained in:
Bernhard Gleiss 2017-10-12 17:01:30 +02:00 • committed by Arie Gurfinkel
parent 56fcb8e6fd
commit fba995294d
4 changed files with 25 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/base/fixedpoint_params.pyg
View file

@ -183,8 +183,7 @@ def_module_params('fixedpoint',
('spacer.qlemmas', BOOL, True, 'allow quantified lemmas in frames'), ('spacer.qlemmas', BOOL, True, 'allow quantified lemmas in frames'),
('spacer.new_unsat_core', BOOL, True, 'use the new implementation of unsat-core-generation'), ('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.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_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.farkas_a_const', BOOL, True, 'if the unoptimized farkas plugin is used, use the constants from A while constructing unsat_cores'),
('spacer.lemma_sanity_check', BOOL, False, 'check during generalization whether lemma is actually correct'), ('spacer.lemma_sanity_check', BOOL, False, 'check during generalization whether lemma is actually correct'),
('spacer.reuse_pobs', BOOL, True, 'reuse POBs'), ('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.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut'),

34
src/muz/spacer/spacer_itp_solver.cpp
View file

@ -276,23 +276,27 @@ void itp_solver::get_itp_core (expr_ref_vector &core)
// new code // new code
unsat_core_learner learner(m,m_print_farkas_stats); unsat_core_learner learner(m,m_print_farkas_stats);
if (m_farkas_optimized) { if (m_farkas_plugin == 0 || m_farkas_plugin > 3)
if (true) // TODO: proper options {
{ unsat_core_plugin_farkas_lemma* plugin_farkas_lemma = alloc(unsat_core_plugin_farkas_lemma, learner, m_split_literals, false);
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);
learner.register_plugin(plugin_farkas_lemma); 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) { if (m_minimize_unsat_core) {
unsat_core_plugin_min_cut* plugin_min_cut = alloc(unsat_core_plugin_min_cut, learner, m); unsat_core_plugin_min_cut* plugin_min_cut = alloc(unsat_core_plugin_min_cut, learner, m);
learner.register_plugin(plugin_min_cut); learner.register_plugin(plugin_min_cut);

8
src/muz/spacer/spacer_itp_solver.h
View file

@ -60,8 +60,7 @@ private:
bool m_split_literals; bool m_split_literals;
bool m_new_unsat_core; bool m_new_unsat_core;
bool m_minimize_unsat_core; bool m_minimize_unsat_core;
bool m_farkas_optimized; unsigned m_farkas_plugin;
bool m_farkas_a_const;
bool m_print_farkas_stats; bool m_print_farkas_stats;
bool is_proxy(expr *e, app_ref &def); bool is_proxy(expr *e, app_ref &def);
@ -70,7 +69,7 @@ private:
app* fresh_proxy(); app* fresh_proxy();
void elim_proxies(expr_ref_vector &v); void elim_proxies(expr_ref_vector &v);
public: 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.get_manager()),
m_solver(solver), m_solver(solver),
m_proxies(m), m_proxies(m),
@ -83,8 +82,7 @@ public:
m_split_literals(split_literals), m_split_literals(split_literals),
m_new_unsat_core(new_unsat_core), m_new_unsat_core(new_unsat_core),
m_minimize_unsat_core(minimize_unsat_core), m_minimize_unsat_core(minimize_unsat_core),
m_farkas_optimized(farkas_optimized), m_farkas_plugin(farkas_plugin),
m_farkas_a_const(farkas_a_const),
m_print_farkas_stats(print_farkas_stats) m_print_farkas_stats(print_farkas_stats)
{} {}

4
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -60,8 +60,8 @@ prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const&
m_solvers[1] = pm.mk_fresh2(); m_solvers[1] = pm.mk_fresh2();
m_fparams[1] = &pm.fparams2(); 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[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_optimized(), p.spacer_farkas_a_const(), 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) for (unsigned i = 0; i < 2; ++i)
{ m_contexts[i]->assert_expr(m_pm.get_background()); } { m_contexts[i]->assert_expr(m_pm.get_background()); }