From b35088f7e53e2a0f15f4e565e88a68d328d80b27 Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Fri, 22 Nov 2013 18:15:34 -0800 Subject: [PATCH] Update diff logic optimization --- src/smt/network_flow.h | 1 - src/smt/network_flow_def.h | 29 +++++++++++++++++------------ src/smt/theory_diff_logic_def.h | 16 ++++++++++++---- 3 files changed, 29 insertions(+), 17 deletions(-) diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index b97b9bd40..6e6fcaee0 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -54,7 +54,6 @@ namespace smt { enum edge_state { LOWER = 1, BASIS = 0, - UPPER = -1 }; typedef dl_var node; diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 86515f432..c5038222e 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -114,11 +114,17 @@ namespace smt { node src = m_graph.get_source(m_enter_id); node tgt = m_graph.get_target(m_enter_id); numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(m_enter_id); - numeral change = m_tree->in_subtree_t2(tgt) ? cost : -cost; - node start = m_graph.get_source(m_leave_id); - if (!m_tree->in_subtree_t2(start)) { - start = m_graph.get_target(m_leave_id);; + numeral change; + node start; + if (m_tree->in_subtree_t2(tgt)) { + change = cost; + start = tgt; } + else { + change = -cost; + start = src; + } + SASSERT(m_tree->in_subtree_t2(start)); TRACE("network_flow", tout << "update_potentials of T_" << start << " with change = " << change << "...\n";); svector descendants; m_tree->get_descendants(start, descendants); @@ -185,7 +191,6 @@ namespace smt { m_tree->update(m_enter_id, m_leave_id); } - // FIXME: should declare pivot as a pivot_rule_impl and refactor template bool network_flow::choose_entering_edge(pivot_rule pr) { pivot_rule_impl * pivot; @@ -218,14 +223,11 @@ namespace smt { SASSERT(edge_in_tree(m_leave_id)); SASSERT(!edge_in_tree(m_enter_id)); m_states[m_enter_id] = BASIS; - m_states[m_leave_id] = (m_flows[m_leave_id].is_zero()) ? LOWER : UPPER; + m_states[m_leave_id] = LOWER; update_spanning_tree(); update_potentials(); TRACE("network_flow", tout << "Spanning tree:\n" << display_spanning_tree();); SASSERT(check_well_formed()); - } - else { - m_states[m_leave_id] = m_states[m_leave_id] == LOWER ? UPPER : LOWER; } } TRACE("network_flow", tout << "Found optimal solution.\n";); @@ -241,7 +243,7 @@ namespace smt { for (unsigned i = 0; i < num_edges; ++i) { if (m_states[i] == BASIS) { - objective_value += m_graph.get_weight(i).get_rational() * m_flows[i]; + objective_value += m_flows[i].get_rational() * m_graph.get_weight(i); } } result.reset(); @@ -273,7 +275,10 @@ namespace smt { unsigned num_edges = m_graph.get_num_edges(); for (unsigned i = 0; i < num_edges; ++i) { if (m_states[i] == BASIS) { - SASSERT(m_potentials[m_graph.get_source(i)] - m_potentials[m_graph.get_target(i)] == m_graph.get_weight(i)); + dl_var src = m_graph.get_source(i); + dl_var tgt = m_graph.get_target(i); + numeral weight = m_graph.get_weight(i); + SASSERT(m_potentials[src] - m_potentials[tgt] == weight); } } @@ -286,7 +291,7 @@ namespace smt { unsigned num_edges = m_graph.get_num_edges(); for (unsigned i = 0; i < num_edges; ++i) { if (m_states[i] == BASIS) { - total_cost += m_graph.get_weight(i).get_rational() * m_flows[i]; + total_cost += m_flows[i].get_rational() * m_graph.get_weight(i); } } diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index c45493434..d0cef90cf 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1031,7 +1031,8 @@ inf_eps_rational theory_diff_logic::maximize(theory_var v) { 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);); + // FIXME: Network Simplex lose precisions when handling infinitesimals + SASSERT(objective_value >= initial_value.get_rational());); vector & current_assigments = m_objective_assignments[v]; SASSERT(!current_assigments.empty()); @@ -1092,11 +1093,17 @@ expr* theory_diff_logic::block_lower_bound(theory_var v, inf_rational const vector const & ns = m_objective_assignments[v]; inf_rational val; rational r, s; - for (unsigned i = 0; i < t.size(); ++i) { + rational r0 = ns[0].get_rational().to_rational(); + rational s0 = ns[0].get_infinitesimal().to_rational(); + app * x; + app * x0 = get_enode(t[0].first)->get_owner(); + // Assert improved bounds for x_i - x_0 + for (unsigned i = 1; i < t.size(); ++i) { r = ns[i].get_rational().to_rational(); s = ns[i].get_infinitesimal().to_rational(); - val = inf_rational(r, s); - f = get_enode(t[i].first)->get_owner(); + val = inf_rational(r - r0, s - s0); + x = get_enode(t[i].first)->get_owner(); + f = m_util.mk_sub(x, x0); e = m_util.mk_numeral(val.get_rational(), m.get_sort(f)); if (t[i].second.is_neg() && val.get_infinitesimal().is_pos()) { disj.push_back(m_util.mk_le(f, e)); @@ -1111,6 +1118,7 @@ expr* theory_diff_logic::block_lower_bound(theory_var v, inf_rational const disj.push_back(m_util.mk_gt(f, e)); } else { + UNREACHABLE(); } } return m.mk_or(disj.size(), disj.c_ptr());