From 37f562882426cac5909cd1d912fab9b436ab0370 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Fri, 22 Nov 2013 13:44:12 -0800 Subject: [PATCH] Update basic spanning tree to be on par with threaded one --- src/smt/network_flow.h | 3 +-- src/smt/network_flow_def.h | 28 +++++++++++++++++++++++----- src/smt/spanning_tree.h | 1 - src/smt/spanning_tree_def.h | 23 ++++++++++++++++++----- src/smt/theory_diff_logic.h | 1 - src/smt/theory_diff_logic_def.h | 33 +++++++++++++++++++++------------ 6 files changed, 63 insertions(+), 26 deletions(-) diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index b2a5953ed..b97b9bd40 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -71,7 +71,6 @@ namespace smt { edge_id & m_enter_id; public: - pivot_rule_impl() {} pivot_rule_impl(graph & g, vector & potentials, svector & states, edge_id & enter_id) : m_graph(g), @@ -79,7 +78,7 @@ namespace smt { m_states(states), m_enter_id(enter_id) { } - bool choose_entering_edge() {return false;}; + virtual bool choose_entering_edge() = 0; }; class first_eligible_pivot : public pivot_rule_impl { diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 383740e4a..86515f432 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -40,6 +40,24 @@ namespace smt { m_graph.add_edge(e.get_target(), e.get_source(), e.get_weight(), explanation()); } } + TRACE("network_flow", { + tout << "Solving different logic optimization problem:" << std::endl; + for (unsigned i = 0; i < m_graph.get_num_nodes(); ++i) { + tout << "(declare-fun v" << i << " () Real)" << std::endl; + } + vector const & es = m_graph.get_all_edges(); + for (unsigned i = 0; i < m_graph.get_num_edges(); ++i) { + edge const & e = es[i]; + tout << "(assert (<= (- v" << e.get_source() << " v" << e.get_target() << ") " << e.get_weight() << "))" << std::endl; + }; + tout << "(maximize (+ "; + for (unsigned i = 0; i < balances.size(); ++i) { + tout << "(* " << balances[i] << " v" << i << ") "; + }; + tout << "))" << std::endl; + tout << "(optimize)" << std::endl; + };); + m_step = 0; m_tree = alloc(basic_spanning_tree, m_graph); } @@ -130,7 +148,7 @@ namespace smt { } template - bool network_flow::choose_leaving_edge() { + bool network_flow::choose_leaving_edge() { TRACE("network_flow", tout << "choose_leaving_edge...\n";); node src = m_graph.get_source(m_enter_id); node tgt = m_graph.get_target(m_enter_id); @@ -155,10 +173,10 @@ namespace smt { tout << "Found leaving edge " << m_leave_id; tout << " between node " << m_graph.get_source(m_leave_id); tout << " and node " << m_graph.get_target(m_leave_id) << " with delta = " << *m_delta << "...\n"; - }); + }); return true; } - TRACE("network_flow", tout << "Can't find a leaving edge... The problem is unbounded.\n";); + TRACE("network_flow", tout << "Can't find a leaving edge... The problem is unbounded.\n";); return false; } @@ -179,7 +197,7 @@ namespace smt { 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); + pivot = alloc(candidate_list_pivot, m_graph, m_potentials, m_states, m_enter_id); break; default: UNREACHABLE(); @@ -208,7 +226,7 @@ namespace smt { } else { m_states[m_leave_id] = m_states[m_leave_id] == LOWER ? UPPER : LOWER; - } + } } TRACE("network_flow", tout << "Found optimal solution.\n";); SASSERT(check_optimal()); diff --git a/src/smt/spanning_tree.h b/src/smt/spanning_tree.h index e9954c1d9..bce910b87 100644 --- a/src/smt/spanning_tree.h +++ b/src/smt/spanning_tree.h @@ -74,7 +74,6 @@ 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 faf45c383..5127fb2b4 100644 --- a/src/smt/spanning_tree_def.h +++ b/src/smt/spanning_tree_def.h @@ -421,8 +421,7 @@ namespace smt { template void basic_spanning_tree::initialize(svector const & tree) { m_tree_graph = alloc(graph); - m_tree.reset(); - m_tree.append(tree); + 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); @@ -464,11 +463,25 @@ namespace smt { m_tree_graph->bfs_undirected(root, m_pred, m_depth); m_tree_graph->dfs_undirected(root, m_thread); - for (node x = m_thread[root]; x != root; x = m_thread[x]) { + vector const & tree_edges = m_tree_graph->get_all_edges(); + for (unsigned i = 0; i < tree_edges.size(); ++i) { + edge const & e = tree_edges[i]; + dl_var src = e.get_source(); + dl_var tgt = e.get_target(); edge_id id; - VERIFY(m_graph.get_edge_id(x, m_pred[x], id)); - m_tree[x] = id; + VERIFY(m_graph.get_edge_id(src, tgt, id)); + SASSERT(tgt == m_pred[src] || src == m_pred[tgt]); + if (tgt == m_pred[src]) { + m_tree[src] = id; + } + else { + m_tree[tgt] = id; + } } + + node p = m_graph.get_source(enter_id); + node q = m_graph.get_target(enter_id); + m_root_t2 = p == m_pred[q] ? q : p; } } diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 9cc01e260..7f85d854f 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -192,7 +192,6 @@ namespace smt { vector m_objectives; vector m_objective_consts; vector > m_objective_assignments; - numeral m_objective_value; // Set a conflict due to a negative cycle. void set_neg_cycle_conflict(); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index b654d9c31..c45493434 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1007,9 +1007,9 @@ inf_eps_rational theory_diff_logic::maximize(theory_var v) { IF_VERBOSE(1, for (unsigned i = 0; i < objective.size(); ++i) { - verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n"; + verbose_stream() << "Coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n"; } - verbose_stream() << "free coefficient " << m_objective_consts[v] << "\n";); + verbose_stream() << "Free coefficient " << m_objective_consts[v] << "\n";); // Objective coefficients now become balances vector balances(m_graph.get_num_nodes()); @@ -1018,24 +1018,33 @@ inf_eps_rational theory_diff_logic::maximize(theory_var v) { fin_numeral balance(objective[i].second); balances[objective[i].first] = balance; } - + network_flow net_flow(m_graph, balances); bool is_optimal = net_flow.min_cost(); if (is_optimal) { - vector potentials; - m_objective_value = net_flow.get_optimal_solution(potentials, true); - std::cout << "Objective value of var " << v << ": " << m_objective_value << std::endl; - m_objective_assignments[v] = potentials; + numeral objective_value = net_flow.get_optimal_solution(m_objective_assignments[v], true) + numeral(m_objective_consts[v]); + IF_VERBOSE(1, verbose_stream() << "Optimal value of objective " << v << ": " << objective_value << std::endl;); + + DEBUG_CODE( + numeral initial_value = numeral(m_objective_consts[v]); + for (unsigned i = 0; i < objective.size(); ++i) { + initial_value += fin_numeral(objective[i].second) * m_graph.get_assignment(objective[i].first); + } + IF_VERBOSE(1, verbose_stream() << "Initial value of objective " << v << ": " << initial_value << std::endl;); + SASSERT(objective_value >= initial_value);); + + vector & current_assigments = m_objective_assignments[v]; + SASSERT(!current_assigments.empty()); TRACE("network_flow", - for (unsigned i = 0; i < potentials.size(); ++i) { - tout << "v" << i << " -> " << potentials[i] << "\n"; + for (unsigned i = 0; i < current_assigments.size(); ++i) { + tout << "v" << i << " -> " << current_assigments[i] << std::endl; }); - rational r = m_objective_value.get_rational().to_rational(); - rational i = m_objective_value.get_infinitesimal().to_rational(); + rational r = objective_value.get_rational().to_rational(); + rational i = objective_value.get_infinitesimal().to_rational(); return inf_eps_rational(inf_rational(r, i)); } else { - std::cout << "Unbounded objective" << std::endl; + IF_VERBOSE(1, verbose_stream() << "Unbounded objective" << std::endl;); return inf_eps_rational::infinity(); } }