diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 7bc430244..6e58d31bb 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -961,7 +961,6 @@ public: for (; it != end; ++it) { edge_id e_id = *it; edge & e = m_edges[e_id]; - if (!e.is_enabled()) continue; SASSERT(e.get_source() == current); dl_var neighbour = e.get_target(); neighbours.push_back(neighbour); @@ -972,7 +971,6 @@ public: for (; it != end; ++it) { edge_id e_id = *it; edge & e = m_edges[e_id]; - if (!e.is_enabled()) continue; SASSERT(e.get_target() == current); dl_var neighbour = e.get_source(); neighbours.push_back(neighbour); @@ -982,27 +980,41 @@ public: void dfs_undirected(dl_var start, svector & threads) { threads.reset(); threads.resize(get_num_nodes()); - uint_set visited; + uint_set discovered, explored; svector nodes; + discovered.insert(start); nodes.push_back(start); dl_var prev = -1; while(!nodes.empty()) { dl_var current = nodes.back(); - nodes.pop_back(); - visited.insert(current); - if (prev != -1) + 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 neighbours; get_neighbours_undirected(current, neighbours); + SASSERT(!neighbours.empty()); + bool found = false; for (unsigned i = 0; i < neighbours.size(); ++i) { + dl_var next = neighbours[i]; DEBUG_CODE( edge_id id; - SASSERT(prev == -1 || get_edge_id(prev, current, id) || get_edge_id(current, prev, id));); - if (!visited.contains(neighbours[i])) { - nodes.push_back(neighbours[i]); + SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id));); + if (!discovered.contains(next) && !explored.contains(next)) { + discovered.insert(next); + nodes.push_back(next); + found = true; + break; } - } + } + SASSERT(!nodes.empty()); + if (!found) { + explored.insert(current); + nodes.pop_back(); + } } threads[prev] = start; } @@ -1022,8 +1034,10 @@ public: SASSERT(visited.contains(current)); svector neighbours; get_neighbours_undirected(current, neighbours); + SASSERT(!neighbours.empty()); 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( edge_id id; SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id));); diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index d845c671a..b2a5953ed 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -82,7 +82,7 @@ namespace smt { bool choose_entering_edge() {return false;}; }; - class first_eligible_pivot : pivot_rule_impl { + class first_eligible_pivot : public pivot_rule_impl { private: edge_id m_next_edge; @@ -117,7 +117,7 @@ namespace smt { }; }; - class best_eligible_pivot : pivot_rule_impl { + class best_eligible_pivot : public pivot_rule_impl { public: best_eligible_pivot(graph & g, vector & potentials, svector & states, edge_id & enter_id) : @@ -152,7 +152,7 @@ namespace smt { }; }; - class candidate_list_pivot : pivot_rule_impl { + class candidate_list_pivot : public pivot_rule_impl { private: edge_id m_next_edge; svector m_candidates; diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 7af1a87ff..383740e4a 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -170,18 +170,21 @@ namespace smt { // FIXME: should declare pivot as a pivot_rule_impl and refactor template bool network_flow::choose_entering_edge(pivot_rule pr) { - if (pr == FIRST_ELIGIBLE) { - first_eligible_pivot pivot(m_graph, m_potentials, m_states, m_enter_id); - return pivot.choose_entering_edge(); + pivot_rule_impl * pivot; + switch (pr) { + case FIRST_ELIGIBLE: + pivot = alloc(first_eligible_pivot, m_graph, m_potentials, m_states, m_enter_id); + break; + case BEST_ELIGIBLE: + pivot = alloc(best_eligible_pivot, m_graph, m_potentials, m_states, m_enter_id); + break; + case CANDIDATE_LIST: + pivot = alloc(best_eligible_pivot, m_graph, m_potentials, m_states, m_enter_id); + break; + default: + UNREACHABLE(); } - else if (pr == BEST_ELIGIBLE) { - best_eligible_pivot pivot(m_graph, m_potentials, m_states, m_enter_id); - return pivot.choose_entering_edge(); - } - else { - candidate_list_pivot pivot(m_graph, m_potentials, m_states, m_enter_id); - return pivot.choose_entering_edge(); - } + return pivot->choose_entering_edge(); } // Minimize cost flows diff --git a/src/smt/spanning_tree.h b/src/smt/spanning_tree.h index bce910b87..e9954c1d9 100644 --- a/src/smt/spanning_tree.h +++ b/src/smt/spanning_tree.h @@ -74,6 +74,7 @@ namespace smt { private: graph * m_tree_graph; + public: basic_spanning_tree(graph & g); void initialize(svector const & tree); diff --git a/src/smt/spanning_tree_def.h b/src/smt/spanning_tree_def.h index 32b971c45..6697c8969 100644 --- a/src/smt/spanning_tree_def.h +++ b/src/smt/spanning_tree_def.h @@ -420,14 +420,15 @@ namespace smt { template void basic_spanning_tree::initialize(svector const & tree) { - unsigned num_nodes = m_graph.get_num_nodes(); m_tree_graph = alloc(graph); + m_tree = tree; + unsigned num_nodes = m_graph.get_num_nodes(); for (unsigned i = 0; i < num_nodes; ++i) { m_tree_graph->init_var(i); } vector const & es = m_graph.get_all_edges(); - svector::const_iterator it = tree.begin(), end = tree.end(); + svector::const_iterator it = m_tree.begin(), end = m_tree.end(); for(; it != end; ++it) { edge const & e = es[*it]; m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation()); @@ -440,8 +441,7 @@ namespace smt { template void basic_spanning_tree::update(edge_id enter_id, edge_id leave_id) { - if (m_tree_graph) - dealloc(m_tree_graph); + if (m_tree_graph) dealloc(m_tree_graph); m_tree_graph = alloc(graph); unsigned num_nodes = m_graph.get_num_nodes(); for (unsigned i = 0; i < num_nodes; ++i) {