mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-10-31 18:51:28 -07:00
commit ae3a69b32e
2 changed files with 27 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/network_flow.h
View file

@ -85,7 +85,7 @@ namespace smt {
edge_id m_entering_edge; edge_id m_entering_edge;
edge_id m_leaving_edge; edge_id m_leaving_edge;
node m_join_node; node m_join_node;
numeral m_delta; optional<numeral> m_delta;
bool m_in_edge_dir; bool m_in_edge_dir;
unsigned m_step; unsigned m_step;

60
src/smt/network_flow_def.h
View file

@ -161,7 +161,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
void network_flow<Ext>::update_flows() { void network_flow<Ext>::update_flows() {
TRACE("network_flow", tout << "update_flows...\n";); TRACE("network_flow", tout << "update_flows...\n";);
numeral val = fin_numeral(m_states[m_entering_edge]) * m_delta; numeral val = fin_numeral(m_states[m_entering_edge]) * (*m_delta);
m_flows[m_entering_edge] += val; m_flows[m_entering_edge] += val;
node source = m_graph.get_source(m_entering_edge); node source = m_graph.get_source(m_entering_edge);
for (unsigned u = source; u != m_join_node; u = m_pred[u]) { for (unsigned u = source; u != m_join_node; u = m_pred[u]) {
@ -225,16 +225,13 @@ namespace smt {
// Found first common ancestor of source and target // Found first common ancestor of source and target
m_join_node = u; m_join_node = u;
TRACE("network_flow", tout << "Found join node " << m_join_node << std::endl;); TRACE("network_flow", tout << "Found join node " << m_join_node << std::endl;);
// FIXME: need to get truly infinite value m_delta.set_invalid();
numeral infty = numeral(INT_MAX);
m_delta = infty;
node src, tgt; node src, tgt;
// Send flows along the path from source to the ancestor // Send flows along the path from source to the ancestor
for (unsigned u = source; u != m_join_node; u = m_pred[u]) { for (unsigned u = source; u != m_join_node; u = m_pred[u]) {
edge_id e_id = get_edge_id(u, m_pred[u]); edge_id e_id = get_edge_id(u, m_pred[u]);
numeral d = m_upwards[u] ? m_flows[e_id] : infty; if (m_upwards[u] && (!m_delta || m_flows[e_id] < *m_delta)) {
if (d < m_delta) { m_delta = m_flows[e_id];
m_delta = d;
src = u; src = u;
tgt = m_pred[u]; tgt = m_pred[u];
m_in_edge_dir = true; m_in_edge_dir = true;
@ -244,16 +241,15 @@ namespace smt {
// Send flows along the path from target to the ancestor // Send flows along the path from target to the ancestor
for (unsigned u = target; u != m_join_node; u = m_pred[u]) { for (unsigned u = target; u != m_join_node; u = m_pred[u]) {
edge_id e_id = get_edge_id(u, m_pred[u]); edge_id e_id = get_edge_id(u, m_pred[u]);
numeral d = m_upwards[u] ? infty : m_flows[e_id]; if (!m_upwards[u] && (!m_delta || m_flows[e_id] <= *m_delta)) {
if (d <= m_delta) { m_delta = m_flows[e_id];
m_delta = d;
src = u; src = u;
tgt = m_pred[u]; tgt = m_pred[u];
m_in_edge_dir = false; m_in_edge_dir = false;
} }
} }
if (m_delta < infty) { if (m_delta) {
m_leaving_edge = get_edge_id(src, tgt); m_leaving_edge = get_edge_id(src, tgt);
TRACE("network_flow", { TRACE("network_flow", {
tout << "Found leaving edge " << m_leaving_edge; tout << "Found leaving edge " << m_leaving_edge;
@ -296,22 +292,14 @@ namespace smt {
// Update m_pred (for nodes in the stem from q to v) // Update m_pred (for nodes in the stem from q to v)
node n = q; node n = q;
node last = m_pred[v]; node last = m_pred[v];
node parent = p; node prev = p;
while (n != last) { while (n != last && n != -1) {
node next = m_pred[n]; node next = m_pred[n];
m_pred[n] = parent; m_pred[n] = prev;
parent = n; m_upwards[n] = !m_upwards[prev];
prev = n;
n = next; n = next;
} }
n = v;
while (n != q && n != -1) {
node next = m_pred[n];
if (next != -1) {
m_upwards[n] = !m_upwards[next];
}
n = next;
}
m_upwards[q] = true;
TRACE("network_flow", tout << "Graft T_q and T_r'\n";); TRACE("network_flow", tout << "Graft T_q and T_r'\n";);
@ -340,7 +328,7 @@ namespace smt {
node theta = m_thread[m_final[v]]; node theta = m_thread[m_final[v]];
gamma = m_thread[m_final[v]]; gamma = m_thread[m_final[v]];
// REVIEW: check f(u) is not in T_v // Check that f(u) is not in T_v
node delta = m_final[u] != m_final[v] ? m_final[u] : phi; node delta = m_final[u] != m_final[v] ? m_final[u] : phi;
n = u; n = u;
last = m_pred[gamma]; last = m_pred[gamma];
@ -356,10 +344,9 @@ namespace smt {
TRACE("network_flow", tout << "Reroot T_v at q\n";); TRACE("network_flow", tout << "Reroot T_v at q\n";);
node n = v; node n = v;
m_thread[m_final[q]] = n;
last = q; last = q;
node alpha1, alpha2 = -1; node alpha1, alpha2;
unsigned count = 0; node prev = q;
while (n != last && n != -1) { while (n != last && n != -1) {
// Find all immediate successors of n // Find all immediate successors of n
node t1 = m_thread[n]; node t1 = m_thread[n];
@ -379,18 +366,15 @@ namespace smt {
} }
m_thread[n] = alpha1; m_thread[n] = alpha1;
m_thread[m_final[alpha1]] = alpha2; m_thread[m_final[alpha1]] = alpha2;
// Decrease depth of all children in the subtree m_thread[m_final[alpha2]] = prev;
++count; prev = n;
int d = m_depth[n] - count;
for (node m = m_thread[n]; m != m_final[n]; m = m_thread[m]) {
m_depth[m] -= d;
}
n = m_pred[n]; n = m_pred[n];
m_thread[m_final[alpha2]] = n;
}
if (alpha2 != -1) {
m_thread[m_final[alpha2]] = v;
} }
m_thread[m_final[q]] = prev;
}
for (node n = m_thread[v]; m_pred[n] != -1; n = m_pred[n]) {
m_depth[n] = m_depth[m_pred[n]] + 1;
} }
for (unsigned i = 0; i < m_thread.size(); ++i) { for (unsigned i = 0; i < m_thread.size(); ++i) {