mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

improved options for IUC computation

Browse source
This commit is contained in:
Bernhard Gleiss 2017-10-12 17:31:39 +02:00 • committed by Arie Gurfinkel
parent fba995294d
commit 00a99f01b4
4 changed files with 23 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -181,9 +181,8 @@ def_module_params('fixedpoint',
('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'),
('spacer.instantiate', BOOL, True, 'instantiate quantified lemmas'), ('spacer.instantiate', BOOL, True, 'instantiate quantified lemmas'),
('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.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.minimize_unsat_core', BOOL, False, 'compute unsat-core by min-cut'), ('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.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.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'),

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

@ -264,7 +264,8 @@ void itp_solver::get_itp_core (expr_ref_vector &core)
proof_ref pr(m); proof_ref pr(m);
pr = get_proof (); pr = get_proof ();
if (!m_new_unsat_core) { if (m_iuc == 0)
{
// old code // old code
farkas_learner learner_old; farkas_learner learner_old;
learner_old.set_split_literals(m_split_literals); 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); learner_old.get_lemmas (pr, B, core);
elim_proxies (core); elim_proxies (core);
simplify_bounds (core); // XXX potentially redundant simplify_bounds (core); // XXX potentially redundant
} else { }
else
{
// 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_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); 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); 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); 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); 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); 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); 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); 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); 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); 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);
} else { }
else
{
unsat_core_plugin_lemma* plugin_lemma = alloc(unsat_core_plugin_lemma, learner); unsat_core_plugin_lemma* plugin_lemma = alloc(unsat_core_plugin_lemma, learner);
learner.register_plugin(plugin_lemma); learner.register_plugin(plugin_lemma);
} }

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

@ -58,9 +58,8 @@ private:
expr_substitution m_elim_proxies_sub; expr_substitution m_elim_proxies_sub;
bool m_split_literals; bool m_split_literals;
bool m_new_unsat_core; unsigned m_iuc;
bool m_minimize_unsat_core; unsigned m_iuc_arith;
unsigned m_farkas_plugin;
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);
@ -69,7 +68,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, 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.get_manager()),
m_solver(solver), m_solver(solver),
m_proxies(m), m_proxies(m),
@ -80,9 +79,8 @@ public:
m_is_proxied(false), m_is_proxied(false),
m_elim_proxies_sub(m, false, true), m_elim_proxies_sub(m, false, true),
m_split_literals(split_literals), m_split_literals(split_literals),
m_new_unsat_core(new_unsat_core), m_iuc(iuc),
m_minimize_unsat_core(minimize_unsat_core), m_iuc_arith(iuc_arith),
m_farkas_plugin(farkas_plugin),
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_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_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_iuc(), p.spacer_iuc_arith(), 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()); }