mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
iuc code cleanup
This commit is contained in:
Arie Gurfinkel
parent
9c9d0d0840
commit
58dc5451e1
|
|
@ -36,28 +36,27 @@ void unsat_core_learner::register_plugin(unsat_core_plugin* plugin) {
|
|||
}
|
||||
|
||||
void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
|
||||
// traverse proof
|
||||
proof_post_order it(m_pr.get(), m);
|
||||
while (it.hasNext()) {
|
||||
proof* currentNode = it.next();
|
||||
proof* curr = it.next();
|
||||
|
||||
if (m.get_num_parents(currentNode) > 0) {
|
||||
bool need_to_mark_closed = true;
|
||||
bool done = is_closed(curr);
|
||||
if (done) continue;
|
||||
|
||||
for (proof* premise : m.get_parents(currentNode)) {
|
||||
need_to_mark_closed &= (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise));
|
||||
}
|
||||
|
||||
// save result
|
||||
m_closed.mark(currentNode, need_to_mark_closed);
|
||||
if (m.get_num_parents(curr) > 0) {
|
||||
done = true;
|
||||
for (proof* p : m.get_parents(curr)) done &= !is_b_open(p);
|
||||
set_closed(curr, done);
|
||||
}
|
||||
|
||||
// we have now collected all necessary information, so we can visit the node
|
||||
// if the node mixes A-reasoning and B-reasoning and contains non-closed premises
|
||||
if (m_pr.is_a_marked(currentNode) &&
|
||||
m_pr.is_b_marked(currentNode) &&
|
||||
!m_closed.is_marked(currentNode)) {
|
||||
compute_partial_core(currentNode); // then we need to compute a partial core
|
||||
// we have now collected all necessary information,
|
||||
// so we can visit the node
|
||||
// if the node mixes A-reasoning and B-reasoning
|
||||
// and contains non-closed premises
|
||||
if (!done) {
|
||||
if (m_pr.is_a_marked(curr) && m_pr.is_b_marked(curr)) {
|
||||
compute_partial_core(curr);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -74,7 +73,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
|
|||
|
||||
void unsat_core_learner::compute_partial_core(proof* step) {
|
||||
for (unsat_core_plugin* plugin : m_plugins) {
|
||||
if (m_closed.is_marked(step)) break;
|
||||
if (is_closed(step)) break;
|
||||
plugin->compute_partial_core(step);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@ Revision History:
|
|||
#include "ast/ast.h"
|
||||
#include "muz/spacer/spacer_util.h"
|
||||
#include "muz/spacer/spacer_proof_utils.h"
|
||||
#include "muz/spacer/spacer_iuc_proof.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
|
|
@ -31,13 +32,25 @@ namespace spacer {
|
|||
class unsat_core_learner {
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
|
||||
ast_manager& m;
|
||||
iuc_proof& m_pr;
|
||||
|
||||
ptr_vector<unsat_core_plugin> m_plugins;
|
||||
ast_mark m_closed;
|
||||
|
||||
expr_ref_vector m_unsat_core;
|
||||
|
||||
public:
|
||||
unsat_core_learner(ast_manager& m, iuc_proof& pr) :
|
||||
m(m), m_pr(pr), m_unsat_core(m) {};
|
||||
virtual ~unsat_core_learner();
|
||||
|
||||
ast_manager& m;
|
||||
iuc_proof& m_pr;
|
||||
ast_manager& get_manager() {return m;}
|
||||
|
||||
bool is_a(proof *pr) {return m_pr.is_a_marked(pr);}
|
||||
bool is_b(proof *pr) {return m_pr.is_b_marked(pr);}
|
||||
bool is_h(proof *pr) {return m_pr.is_h_marked(pr);}
|
||||
bool is_b_pure(proof *pr) { return m_pr.is_b_pure(pr);}
|
||||
|
||||
/*
|
||||
* register a plugin for computation of partial unsat cores
|
||||
|
|
@ -67,14 +80,6 @@ namespace spacer {
|
|||
void add_lemma_to_core(expr* lemma);
|
||||
|
||||
private:
|
||||
ptr_vector<unsat_core_plugin> m_plugins;
|
||||
ast_mark m_closed;
|
||||
|
||||
/*
|
||||
* collects the lemmas of the unsat-core
|
||||
* will at the end be inserted into unsat_core.
|
||||
*/
|
||||
expr_ref_vector m_unsat_core;
|
||||
|
||||
/*
|
||||
* computes partial core for step by delegating computation to plugins
|
||||
|
|
|
|||
|
|
@ -34,27 +34,25 @@ Revision History:
|
|||
|
||||
namespace spacer {
|
||||
|
||||
unsat_core_plugin::unsat_core_plugin(unsat_core_learner& learner):
|
||||
m(learner.m), m_learner(learner) {};
|
||||
unsat_core_plugin::unsat_core_plugin(unsat_core_learner& ctx):
|
||||
m(ctx.get_manager()), m_ctx(ctx) {};
|
||||
|
||||
void unsat_core_plugin_lemma::compute_partial_core(proof* step) {
|
||||
SASSERT(m_learner.m_pr.is_a_marked(step));
|
||||
SASSERT(m_learner.m_pr.is_b_marked(step));
|
||||
SASSERT(m_ctx.is_a(step));
|
||||
SASSERT(m_ctx.is_b(step));
|
||||
|
||||
for (proof* premise : m.get_parents(step)) {
|
||||
|
||||
if (m_learner.is_b_open (premise)) {
|
||||
for (auto* p : m.get_parents(step)) {
|
||||
if (m_ctx.is_b_open (p)) {
|
||||
// by IH, premises that are AB marked are already closed
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(premise));
|
||||
add_lowest_split_to_core(premise);
|
||||
SASSERT(!m_ctx.is_a(p));
|
||||
add_lowest_split_to_core(p);
|
||||
}
|
||||
}
|
||||
m_learner.set_closed(step, true);
|
||||
m_ctx.set_closed(step, true);
|
||||
}
|
||||
|
||||
void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const
|
||||
{
|
||||
SASSERT(m_learner.is_b_open(step));
|
||||
void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const {
|
||||
SASSERT(m_ctx.is_b_open(step));
|
||||
|
||||
ptr_buffer<proof> todo;
|
||||
todo.push_back(step);
|
||||
|
|
@ -64,44 +62,45 @@ namespace spacer {
|
|||
todo.pop_back();
|
||||
|
||||
// if current step hasn't been processed,
|
||||
if (!m_learner.is_closed(pf)) {
|
||||
m_learner.set_closed(pf, true);
|
||||
if (!m_ctx.is_closed(pf)) {
|
||||
m_ctx.set_closed(pf, true);
|
||||
// the step is b-marked and not closed.
|
||||
// by I.H. the step must be already visited
|
||||
// so if it is also a-marked, it must be closed
|
||||
SASSERT(m_learner.m_pr.is_b_marked(pf));
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(pf));
|
||||
SASSERT(m_ctx.is_b(pf));
|
||||
SASSERT(!m_ctx.is_a(pf));
|
||||
|
||||
// the current step needs to be interpolated:
|
||||
expr* fact = m.get_fact(pf);
|
||||
// if we trust the current step and we are able to use it
|
||||
if (m_learner.m_pr.is_b_pure (pf) &&
|
||||
(m.is_asserted(pf) || is_literal(m, fact))) {
|
||||
if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || is_literal(m, fact))) {
|
||||
// just add it to the core
|
||||
m_learner.add_lemma_to_core(fact);
|
||||
m_ctx.add_lemma_to_core(fact);
|
||||
}
|
||||
// otherwise recurse on premises
|
||||
else {
|
||||
for (proof* premise : m.get_parents(pf))
|
||||
if (m_learner.is_b_open(premise))
|
||||
if (m_ctx.is_b_open(premise))
|
||||
todo.push_back(premise);
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step)
|
||||
{
|
||||
SASSERT(m_learner.m_pr.is_a_marked(step));
|
||||
SASSERT(m_learner.m_pr.is_b_marked(step));
|
||||
/***
|
||||
* FARKAS
|
||||
*/
|
||||
void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step) {
|
||||
SASSERT(m_ctx.is_a(step));
|
||||
SASSERT(m_ctx.is_b(step));
|
||||
// XXX this assertion should be true so there is no need to check for it
|
||||
SASSERT (!m_learner.is_closed (step));
|
||||
SASSERT (!m_ctx.is_closed (step));
|
||||
func_decl* d = step->get_decl();
|
||||
symbol sym;
|
||||
if (!m_learner.is_closed(step) && // if step is not already interpolated
|
||||
is_farkas_lemma(m, step)) {
|
||||
TRACE("spacer.farkas",
|
||||
tout << "looking at: " << mk_pp(step, m) << "\n";);
|
||||
if (!m_ctx.is_closed(step) && is_farkas_lemma(m, step)) {
|
||||
// weaker check : d->get_num_parameters() >= m.get_num_parents(step) + 2
|
||||
|
||||
SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
|
||||
|
|
@ -136,24 +135,24 @@ namespace spacer {
|
|||
parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient
|
||||
|
||||
TRACE("spacer.farkas",
|
||||
tout << "Farkas input: "<< "\n";
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * prem = m.get_parent(step, i);
|
||||
rational coef = params[i].get_rational();
|
||||
bool b_pure = m_learner.m_pr.is_b_pure (prem);
|
||||
tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
|
||||
}
|
||||
);
|
||||
tout << "Farkas input: "<< "\n";
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * prem = m.get_parent(step, i);
|
||||
rational coef = params[i].get_rational();
|
||||
bool b_pure = m_ctx.is_b_pure (prem);
|
||||
tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
bool can_be_closed = true;
|
||||
bool done = true;
|
||||
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * premise = m.get_parent(step, i);
|
||||
|
||||
if (m_learner.is_b_open (premise)) {
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(premise));
|
||||
if (m_ctx.is_b_open (premise)) {
|
||||
SASSERT(!m_ctx.is_a(premise));
|
||||
|
||||
if (m_learner.m_pr.is_b_pure (premise)) {
|
||||
if (m_ctx.is_b_pure (premise)) {
|
||||
if (!m_use_constant_from_a) {
|
||||
rational coefficient = params[i].get_rational();
|
||||
coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
|
||||
|
|
@ -161,7 +160,7 @@ namespace spacer {
|
|||
}
|
||||
else {
|
||||
// -- mixed premise, won't be able to close this proof step
|
||||
can_be_closed = false;
|
||||
done = false;
|
||||
|
||||
if (m_use_constant_from_a) {
|
||||
rational coefficient = params[i].get_rational();
|
||||
|
|
@ -177,6 +176,7 @@ namespace spacer {
|
|||
}
|
||||
}
|
||||
|
||||
// TBD: factor into another method
|
||||
if (m_use_constant_from_a) {
|
||||
params += m.get_num_parents(step); // point to the first Farkas coefficient, which corresponds to a formula in the conclusion
|
||||
|
||||
|
|
@ -208,11 +208,9 @@ namespace spacer {
|
|||
// only if all b-premises can be used directly, add the farkas core and close the step
|
||||
// AG: this decision needs to be re-evaluated. If the proof cannot be closed, literals above
|
||||
// AG: it will go into the core. However, it does not mean that this literal should/could not be added.
|
||||
if (can_be_closed) {
|
||||
m_learner.set_closed(step, true);
|
||||
expr_ref res = compute_linear_combination(coeff_lits);
|
||||
m_learner.add_lemma_to_core(res);
|
||||
}
|
||||
m_ctx.set_closed(step, done);
|
||||
expr_ref res = compute_linear_combination(coeff_lits);
|
||||
m_ctx.add_lemma_to_core(res);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -236,12 +234,12 @@ namespace spacer {
|
|||
|
||||
void unsat_core_plugin_farkas_lemma_optimized::compute_partial_core(proof* step)
|
||||
{
|
||||
SASSERT(m_learner.m_pr.is_a_marked(step));
|
||||
SASSERT(m_learner.m_pr.is_b_marked(step));
|
||||
SASSERT(m_ctx.is_a(step));
|
||||
SASSERT(m_ctx.is_b(step));
|
||||
|
||||
func_decl* d = step->get_decl();
|
||||
symbol sym;
|
||||
if (!m_learner.is_closed(step) && // if step is not already interpolated
|
||||
if (!m_ctx.is_closed(step) && // if step is not already interpolated
|
||||
is_farkas_lemma(m, step)) {
|
||||
SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
|
||||
SASSERT(m.has_fact(step));
|
||||
|
|
@ -250,25 +248,25 @@ namespace spacer {
|
|||
|
||||
parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient
|
||||
|
||||
STRACE("spacer.farkas",
|
||||
verbose_stream() << "Farkas input: "<< "\n";
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * prem = m.get_parent(step, i);
|
||||
rational coef = params[i].get_rational();
|
||||
bool b_pure = m_learner.m_pr.is_b_pure (prem);
|
||||
verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m_learner.m) << "\n";
|
||||
}
|
||||
);
|
||||
TRACE("spacer.farkas",
|
||||
tout << "Farkas input: "<< "\n";
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * prem = m.get_parent(step, i);
|
||||
rational coef = params[i].get_rational();
|
||||
bool b_pure = m_ctx.is_b_pure (prem);
|
||||
tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
bool can_be_closed = true;
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * premise = m.get_parent(step, i);
|
||||
|
||||
if (m_learner.m_pr.is_b_marked(premise) && !m_learner.is_closed(premise))
|
||||
if (m_ctx.is_b(premise) && !m_ctx.is_closed(premise))
|
||||
{
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(premise));
|
||||
SASSERT(!m_ctx.is_a(premise));
|
||||
|
||||
if (m_learner.m_pr.is_b_pure(premise))
|
||||
if (m_ctx.is_b_pure(premise))
|
||||
{
|
||||
rational coefficient = params[i].get_rational();
|
||||
linear_combination.push_back
|
||||
|
|
@ -284,7 +282,7 @@ namespace spacer {
|
|||
// only if all b-premises can be used directly, close the step and add linear combinations for later processing
|
||||
if (can_be_closed)
|
||||
{
|
||||
m_learner.set_closed(step, true);
|
||||
m_ctx.set_closed(step, true);
|
||||
if (!linear_combination.empty())
|
||||
{
|
||||
m_linear_combinations.push_back(linear_combination);
|
||||
|
|
@ -350,7 +348,7 @@ namespace spacer {
|
|||
SASSERT(!coeff_lits.empty());
|
||||
expr_ref linear_combination = compute_linear_combination(coeff_lits);
|
||||
|
||||
m_learner.add_lemma_to_core(linear_combination);
|
||||
m_ctx.add_lemma_to_core(linear_combination);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -481,7 +479,7 @@ namespace spacer {
|
|||
SASSERT(!coeff_lits.empty()); // since then previous outer loop would have found solution already
|
||||
expr_ref linear_combination = compute_linear_combination(coeff_lits);
|
||||
|
||||
m_learner.add_lemma_to_core(linear_combination);
|
||||
m_ctx.add_lemma_to_core(linear_combination);
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
|
@ -505,10 +503,10 @@ namespace spacer {
|
|||
{
|
||||
ptr_vector<proof> todo;
|
||||
|
||||
SASSERT(m_learner.m_pr.is_a_marked(step));
|
||||
SASSERT(m_learner.m_pr.is_b_marked(step));
|
||||
SASSERT(m_ctx.is_a(step));
|
||||
SASSERT(m_ctx.is_b(step));
|
||||
SASSERT(m.get_num_parents(step) > 0);
|
||||
SASSERT(!m_learner.is_closed(step));
|
||||
SASSERT(!m_ctx.is_closed(step));
|
||||
todo.push_back(step);
|
||||
|
||||
while (!todo.empty())
|
||||
|
|
@ -517,7 +515,7 @@ namespace spacer {
|
|||
todo.pop_back();
|
||||
|
||||
// if we need to deal with the node and if we haven't added the corresponding edges so far
|
||||
if (!m_learner.is_closed(current) && !m_visited.is_marked(current))
|
||||
if (!m_ctx.is_closed(current) && !m_visited.is_marked(current))
|
||||
{
|
||||
// compute smallest subproof rooted in current, which has only good edges
|
||||
// add an edge from current to each leaf of that subproof
|
||||
|
|
@ -528,7 +526,7 @@ namespace spacer {
|
|||
|
||||
}
|
||||
}
|
||||
m_learner.set_closed(step, true);
|
||||
m_ctx.set_closed(step, true);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -539,7 +537,7 @@ namespace spacer {
|
|||
ptr_buffer<proof> todo_subproof;
|
||||
|
||||
for (proof* premise : m.get_parents(step)) {
|
||||
if (m_learner.m_pr.is_b_marked(premise)) {
|
||||
if (m_ctx.is_b(premise)) {
|
||||
todo_subproof.push_back(premise);
|
||||
}
|
||||
}
|
||||
|
|
@ -549,21 +547,21 @@ namespace spacer {
|
|||
todo_subproof.pop_back();
|
||||
|
||||
// if we need to deal with the node
|
||||
if (!m_learner.is_closed(current))
|
||||
if (!m_ctx.is_closed(current))
|
||||
{
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(current)); // by I.H. the step must be already visited
|
||||
SASSERT(!m_ctx.is_a(current)); // by I.H. the step must be already visited
|
||||
|
||||
// and the current step needs to be interpolated:
|
||||
if (m_learner.m_pr.is_b_marked(current))
|
||||
if (m_ctx.is_b(current))
|
||||
{
|
||||
// if we trust the current step and we are able to use it
|
||||
if (m_learner.m_pr.is_b_pure (current) &&
|
||||
if (m_ctx.is_b_pure (current) &&
|
||||
(m.is_asserted(current) ||
|
||||
is_literal(m, m.get_fact(current))))
|
||||
{
|
||||
// we found a leaf of the subproof, so
|
||||
// 1) we add corresponding edges
|
||||
if (m_learner.m_pr.is_a_marked(step))
|
||||
if (m_ctx.is_a(step))
|
||||
{
|
||||
add_edge(nullptr, current); // current is sink
|
||||
}
|
||||
|
|
@ -685,7 +683,7 @@ namespace spacer {
|
|||
m_min_cut.compute_min_cut(cut_nodes);
|
||||
|
||||
for (unsigned cut_node : cut_nodes) {
|
||||
m_learner.add_lemma_to_core(m_node_to_formula[cut_node]);
|
||||
m_ctx.add_lemma_to_core(m_node_to_formula[cut_node]);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -35,14 +35,14 @@ namespace spacer {
|
|||
virtual ~unsat_core_plugin() {};
|
||||
virtual void compute_partial_core(proof* step) = 0;
|
||||
virtual void finalize(){};
|
||||
|
||||
unsat_core_learner& m_learner;
|
||||
|
||||
unsat_core_learner& m_ctx;
|
||||
};
|
||||
|
||||
class unsat_core_plugin_lemma : public unsat_core_plugin {
|
||||
class unsat_core_plugin_lemma : public unsat_core_plugin {
|
||||
public:
|
||||
unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){};
|
||||
void compute_partial_core(proof* step) override;
|
||||
unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){};
|
||||
void compute_partial_core(proof* step) override;
|
||||
private:
|
||||
void add_lowest_split_to_core(proof* step) const;
|
||||
};
|
||||
|
|
@ -54,7 +54,7 @@ namespace spacer {
|
|||
bool use_constant_from_a=true) :
|
||||
unsat_core_plugin(learner),
|
||||
m_split_literals(split_literals),
|
||||
m_use_constant_from_a(use_constant_from_a) {};
|
||||
m_use_constant_from_a(use_constant_from_a) {};
|
||||
void compute_partial_core(proof* step) override;
|
||||
private:
|
||||
bool m_split_literals;
|
||||
|
|
@ -64,8 +64,8 @@ namespace spacer {
|
|||
*/
|
||||
expr_ref compute_linear_combination(const coeff_lits_t& coeff_lits);
|
||||
};
|
||||
|
||||
class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin {
|
||||
|
||||
class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin {
|
||||
public:
|
||||
unsat_core_plugin_farkas_lemma_optimized(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner) {};
|
||||
void compute_partial_core(proof* step) override;
|
||||
|
|
|
|||
Loading…
Reference in a new issue