mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

added option fixedpoint.spacer.iuc.debug_proof to debug proof which is used for generation of iuc

Browse source
This commit is contained in:
Bernhard Gleiss 2017-10-23 15:39:59 +02:00 committed by Arie Gurfinkel
parent c3a66217e1
commit 25fad153d1
6 changed files with 36 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -186,6 +186,7 @@ def_module_params('fixedpoint',
('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'),
('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes'),
('spacer.simplify_pob', BOOL, False, 'simplify POBs by removing redundant constraints')
))

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

@ -277,7 +277,7 @@ void itp_solver::get_itp_core (expr_ref_vector &core)
else
{
// new code
unsat_core_learner learner(m,m_print_farkas_stats);
unsat_core_learner learner(m, m_print_farkas_stats, m_iuc_debug_proof);
if (m_iuc_arith == 0 || m_iuc_arith > 3)
{

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

@ -61,14 +61,14 @@ private:
unsigned m_iuc;
unsigned m_iuc_arith;
bool m_print_farkas_stats;
bool m_iuc_debug_proof;
bool is_proxy(expr *e, app_ref &def);
void undo_proxies_in_core(ptr_vector<expr> &v);
app* mk_proxy(expr *v);
app* fresh_proxy();
void elim_proxies(expr_ref_vector &v);
public:
itp_solver(solver &solver, unsigned iuc, unsigned iuc_arith, bool print_farkas_stats, bool split_literals = false) :
itp_solver(solver &solver, unsigned iuc, unsigned iuc_arith, bool print_farkas_stats, bool iuc_debug_proof, bool split_literals = false) :
m(solver.get_manager()),
m_solver(solver),
m_proxies(m),
@ -81,7 +81,8 @@ public:
m_split_literals(split_literals),
m_iuc(iuc),
m_iuc_arith(iuc_arith),
m_print_farkas_stats(print_farkas_stats)
m_print_farkas_stats(print_farkas_stats),
m_iuc_debug_proof(iuc_debug_proof)
{}
~itp_solver() override {}

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_fparams[1] = &pm.fparams2();
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());
m_contexts[0] = alloc(spacer::itp_solver, *(m_solvers[0]), p.spacer_iuc(), p.spacer_iuc_arith(), p.spacer_print_farkas_stats(), p.spacer_iuc_debug_proof(), 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_iuc_debug_proof(), p.spacer_split_farkas_literals());
for (unsigned i = 0; i < 2; ++i)
{ m_contexts[i]->assert_expr(m_pm.get_background()); }

35
src/muz/spacer/spacer_unsat_core_learner.cpp
View file

@ -174,13 +174,11 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
verbose_stream() << "\nThis proof contains " << farkas_counter << " Farkas lemmas. " << farkas_counter2 << " Farkas lemmas participate in the lowest cut\n";
}
bool debug_proof = false;
if(debug_proof)
if(m_iuc_debug_proof)
{
// print proof for debugging
verbose_stream() << "\n\nProof:\n";
verbose_stream() << "Proof:\n";
std::unordered_map<unsigned, unsigned> id_to_small_id;
unsigned counter = 0;
@ -223,8 +221,23 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
verbose_stream() << "hypothesis";
break;
default:
verbose_stream() << "unknown axiom-type";
break;
if (currentNode->get_decl_kind() == PR_TH_LEMMA)
{
verbose_stream() << "th_axiom";
func_decl* d = currentNode->get_decl();
symbol sym;
if (d->get_num_parameters() >= 2 && // the Farkas coefficients are saved in the parameters of step
d->get_parameter(0).is_symbol(sym) && sym == "arith" && // the first two parameters are "arith", "farkas",
d->get_parameter(1).is_symbol(sym) && sym == "farkas")
{
verbose_stream() << "(farkas)";
}
}
else
{
verbose_stream() << "unknown axiom-type";
break;
}
}
}
else
@ -269,17 +282,21 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
}
}
if (currentNode->get_decl_kind() == PR_TH_LEMMA || (is_a_marked(currentNode) && is_b_marked(currentNode)) || is_h_marked(currentNode) || (!is_a_marked(currentNode) && !is_b_marked(currentNode)))
// if (currentNode->get_decl_kind() == PR_TH_LEMMA || (is_a_marked(currentNode) && is_b_marked(currentNode)) || is_h_marked(currentNode) || (!is_a_marked(currentNode) && !is_b_marked(currentNode)))
if (false)
{
verbose_stream() << std::endl;
verbose_stream() << "\n";
}
else
{
verbose_stream() << ": " << mk_pp(m.get_fact(currentNode), m) << std::endl;
verbose_stream() << ": " << mk_pp(m.get_fact(currentNode), m) << "\n";
}
++counter;
}
}
verbose_stream() << std::endl;
// move all lemmas into vector
for (expr* const* it = m_unsat_core.begin(); it != m_unsat_core.end(); ++it)
{

3
src/muz/spacer/spacer_unsat_core_learner.h
View file

@ -31,7 +31,7 @@ namespace spacer {
typedef obj_hashtable<expr> expr_set;
public:
unsat_core_learner(ast_manager& m, bool print_farkas_stats = false) : m(m), m_unsat_core(m), m_print_farkas_stats(print_farkas_stats) {};
unsat_core_learner(ast_manager& m, bool print_farkas_stats = false, bool iuc_debug_proof = false) : m(m), m_unsat_core(m), m_print_farkas_stats(print_farkas_stats), m_iuc_debug_proof(iuc_debug_proof) {};
virtual ~unsat_core_learner();
ast_manager& m;
@ -102,6 +102,7 @@ namespace spacer {
void finalize();
bool m_print_farkas_stats;
bool m_iuc_debug_proof;
};
}