mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

fixed bug, which added too many edges between super-source and source in the case where the source was used by multiple inferences

Browse source
This commit is contained in:
Bernhard Gleiss 2017-10-12 16:05:31 +02:00 • committed by Arie Gurfinkel
parent 9b050e8d30
commit 4148ee128c
2 changed files with 15 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/muz/spacer/spacer_unsat_core_plugin.cpp
View file

@ -707,6 +707,8 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
*/ */
void unsat_core_plugin_min_cut::add_edge(proof* i, proof* j) void unsat_core_plugin_min_cut::add_edge(proof* i, proof* j)
{ {
SASSERT(i != nullptr || j != nullptr);
unsigned node_i; unsigned node_i;
unsigned node_j; unsigned node_j;
if (i == nullptr) if (i == nullptr)
@ -735,7 +737,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
m_node_to_formula[node_other] = m.get_fact(i); m_node_to_formula[node_other] = m.get_fact(i);
m_node_to_formula[node_i] = m.get_fact(i); m_node_to_formula[node_i] = m.get_fact(i);
m_min_cut.add_edge(node_other, node_i); m_min_cut.add_edge(node_other, node_i, 1);
} }
} }
@ -765,12 +767,20 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
m_node_to_formula[node_j] = m.get_fact(j); m_node_to_formula[node_j] = m.get_fact(j);
m_node_to_formula[node_other] = m.get_fact(j); m_node_to_formula[node_other] = m.get_fact(j);
m_min_cut.add_edge(node_j, node_other); m_min_cut.add_edge(node_j, node_other, 1);
} }
} }
// finally connect nodes // finally connect nodes (if there is not already a connection i -> j (only relevant if i is the supersource))
m_min_cut.add_edge(node_i, node_j); if (!(i == nullptr && m_connected_to_s.is_marked(j)))
{
m_min_cut.add_edge(node_i, node_j, 1);
}
if (i == nullptr)
{
m_connected_to_s.mark(j, true);
}
} }
/* /*

1
src/muz/spacer/spacer_unsat_core_plugin.h
View file

@ -108,6 +108,7 @@ private:
void add_edge(proof* i, proof* j); void add_edge(proof* i, proof* j);
vector<expr*> m_node_to_formula; // maps each node to the corresponding formula in the original proof vector<expr*> m_node_to_formula; // maps each node to the corresponding formula in the original proof
ast_mark m_connected_to_s; // remember which nodes have already been connected to the supersource, in order to avoid multiple edges.
min_cut m_min_cut; min_cut m_min_cut;
}; };