mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

Debug undirected dfs and bfs

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-22 08:58:17 +01:00
parent 3b2dd47cd4
commit 7bc7a61a40
2 changed files with 31 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

57
src/smt/diff_logic.h
View file

@ -956,8 +956,8 @@ public:
void get_neighbours_undirected(dl_var current, svector<dl_var> & neighbours) { void get_neighbours_undirected(dl_var current, svector<dl_var> & neighbours) {
neighbours.reset(); neighbours.reset();
edge_id_vector & edges = m_out_edges[current]; edge_id_vector & out_edges = m_out_edges[current];
typename edge_id_vector::iterator it = edges.begin(), end = edges.end(); typename edge_id_vector::iterator it = out_edges.begin(), end = out_edges.end();
for (; it != end; ++it) { for (; it != end; ++it) {
edge_id e_id = *it; edge_id e_id = *it;
edge & e = m_edges[e_id]; edge & e = m_edges[e_id];
@ -965,11 +965,10 @@ public:
dl_var neighbour = e.get_target(); dl_var neighbour = e.get_target();
neighbours.push_back(neighbour); neighbours.push_back(neighbour);
} }
edges = m_in_edges[current]; edge_id_vector & in_edges = m_in_edges[current];
it = edges.begin(); typename edge_id_vector::iterator it2 = in_edges.begin(), end2 = in_edges.end();
end = edges.end(); for (; it2 != end2; ++it2) {
for (; it != end; ++it) { edge_id e_id = *it2;
edge_id e_id = *it;
edge & e = m_edges[e_id]; edge & e = m_edges[e_id];
SASSERT(e.get_target() == current); SASSERT(e.get_target() == current);
dl_var neighbour = e.get_source(); dl_var neighbour = e.get_source();
@ -984,31 +983,28 @@ public:
svector<dl_var> nodes; svector<dl_var> nodes;
discovered.insert(start); discovered.insert(start);
nodes.push_back(start); nodes.push_back(start);
dl_var prev = -1; dl_var prev = start;
while(!nodes.empty()) { while(!nodes.empty()) {
dl_var current = nodes.back(); dl_var current = nodes.back();
SASSERT(discovered.contains(current) && !explored.contains(current)); SASSERT(discovered.contains(current) && !explored.contains(current));
std::cout << "thread[" << prev << "] --> " << current << std::endl;
if (prev != -1) {
threads[prev] = current;
std::cout << "thread[" << prev << "] --> " << current << std::endl;
}
prev = current;
svector<dl_var> neighbours; svector<dl_var> neighbours;
get_neighbours_undirected(current, neighbours); get_neighbours_undirected(current, neighbours);
SASSERT(!neighbours.empty()); SASSERT(!neighbours.empty());
bool found = false; bool found = false;
for (unsigned i = 0; i < neighbours.size(); ++i) { for (unsigned i = 0; i < neighbours.size(); ++i) {
dl_var next = neighbours[i]; dl_var next = neighbours[i];
DEBUG_CODE( DEBUG_CODE(
edge_id id; edge_id id;
SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id));); SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id)););
if (!discovered.contains(next) && !explored.contains(next)) { if (!discovered.contains(next) && !explored.contains(next)) {
TRACE("diff_logic", tout << "thread[" << prev << "] --> " << next << std::endl;);
threads[prev] = next;
prev = next;
discovered.insert(next); discovered.insert(next);
nodes.push_back(next); nodes.push_back(next);
found = true; found = true;
break; break;
} }
} }
SASSERT(!nodes.empty()); SASSERT(!nodes.empty());
if (!found) { if (!found) {
@ -1022,6 +1018,7 @@ public:
void bfs_undirected(dl_var start, svector<dl_var> & parents, svector<dl_var> & depths) { void bfs_undirected(dl_var start, svector<dl_var> & parents, svector<dl_var> & depths) {
parents.reset(); parents.reset();
parents.resize(get_num_nodes()); parents.resize(get_num_nodes());
parents[start] = -1;
depths.reset(); depths.reset();
depths.resize(get_num_nodes()); depths.resize(get_num_nodes());
uint_set visited; uint_set visited;
@ -1037,16 +1034,16 @@ public:
SASSERT(!neighbours.empty()); SASSERT(!neighbours.empty());
for (unsigned i = 0; i < neighbours.size(); ++i) { for (unsigned i = 0; i < neighbours.size(); ++i) {
dl_var next = neighbours[i]; dl_var next = neighbours[i];
std::cout << "parents[" << next << "] --> " << current << std::endl; DEBUG_CODE(
DEBUG_CODE( edge_id id;
edge_id id; SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id)););
SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id));); if (!visited.contains(next)) {
if (!visited.contains(next)) { TRACE("diff_logic", tout << "parents[" << next << "] --> " << current << std::endl;);
parents[next] = current; parents[next] = current;
depths[next] = depths[current] + 1; depths[next] = depths[current] + 1;
visited.insert(next); visited.insert(next);
nodes.push_front(next); nodes.push_front(next);
} }
} }
} }
} }

6
src/smt/spanning_tree_def.h
View file

@ -421,7 +421,8 @@ namespace smt {
template<typename Ext> template<typename Ext>
void basic_spanning_tree<Ext>::initialize(svector<edge_id> const & tree) { void basic_spanning_tree<Ext>::initialize(svector<edge_id> const & tree) {
m_tree_graph = alloc(graph); m_tree_graph = alloc(graph);
m_tree = tree; m_tree.reset();
m_tree.append(tree);
unsigned num_nodes = m_graph.get_num_nodes(); unsigned num_nodes = m_graph.get_num_nodes();
for (unsigned i = 0; i < num_nodes; ++i) { for (unsigned i = 0; i < num_nodes; ++i) {
m_tree_graph->init_var(i); m_tree_graph->init_var(i);
@ -456,7 +457,8 @@ namespace smt {
m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation()); m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation());
} }
} }
m_tree_graph->add_edge(m_graph.get_source(enter_id), m_graph.get_target(enter_id), m_graph.get_weight(enter_id), explanation()); edge const & e = es[enter_id];
m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation());
node root = num_nodes - 1; node root = num_nodes - 1;
m_tree_graph->bfs_undirected(root, m_pred, m_depth); m_tree_graph->bfs_undirected(root, m_pred, m_depth);