mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

add outline of object invariant

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-31 17:21:10 -07:00
parent a66a14dbf0
commit cfac32c57d
2 changed files with 69 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/network_flow.h
View file

@ -112,6 +112,8 @@ namespace smt {
std::string display_spanning_tree();
bool check_well_formed();
public:
network_flow(graph & g, vector<fin_numeral> const & balances);

67
src/smt/network_flow_def.h
View file

@ -133,6 +133,7 @@ namespace smt {
tout << pp_vector("Potentials", m_potentials) << pp_vector("Flows", m_flows);
});
TRACE("network_flow", tout << "Spanning tree:\n" << display_spanning_tree(););
SASSERT(check_well_formed());
}
template<typename Ext>
@ -395,6 +396,7 @@ namespace smt {
for (unsigned i = 0; i < m_thread.size(); ++i) {
m_rev_thread[m_thread[i]] = i;
}
SASSERT(check_well_formed());
TRACE("network_flow", {
tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread);
@ -439,6 +441,7 @@ namespace smt {
bool network_flow<Ext>::min_cost() {
initialize();
while (choose_entering_edge()) {
SASSERT(check_well_formed());
bool bounded = choose_leaving_edge();
if (!bounded) return false;
update_flows();
@ -477,6 +480,70 @@ namespace smt {
}
return m_objective_value;
}
static unsigned find(svector<int>& roots, unsigned x) {
unsigned old_x = x;
while (roots[x] >= 0) {
x = roots[x];
}
roots[old_x] = x;
return x;
}
static void merge(svector<int>& roots, unsigned x, unsigned y) {
x = find(roots, x);
y = find(roots, y);
SASSERT(roots[x] < 0 && roots[y] < 0);
if (x == y) {
return;
}
if (roots[x] > roots[y]) {
std::swap(x, y);
}
SASSERT(roots[x] <= roots[y]);
roots[y] = x;
roots[x] += roots[y];
}
template<typename Ext>
bool network_flow<Ext>::check_well_formed() {
// m_thread is depth-first stack
// m_pred is predecessor link
// m_depth depth counting from a root note.
// m_graph
node root = m_pred.size()-1;
for (unsigned i = 0; i < m_upwards.size(); ++i) {
if (m_upwards[i]) {
node p = m_pred[i];
edge_id e = get_edge_id(i, p);
// we are either the root or the predecessor points up.
SASSERT(p == root || m_upwards[p]);
}
}
// m_thread forms a spanning tree over [0..root]
// union-find structure:
svector<int> roots(root+1, -1);
#if 0
for (unsigned i = 0; i < m_thread.size(); ++i) {
if (m_states[i] == BASIS) {
node x = m_thread[i];
node y = i;
// we are now going to check the edge between x and y:
SASSERT(find(roots, x) != find(roots, y));
merge(roots, x, y);
}
else {
// ? LOWER, UPPER
}
}
#endif
return true;
}
}
#endif