mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Update diff logic optimization

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-22 18:15:34 -08:00
parent 37f5628824
commit b35088f7e5
3 changed files with 29 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/network_flow.h
View file

@ -54,7 +54,6 @@ namespace smt {
enum edge_state {
LOWER = 1,
BASIS = 0,
UPPER = -1
};
typedef dl_var node;

29
src/smt/network_flow_def.h
View file

@ -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<node> 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<typename Ext>
bool network_flow<Ext>::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);
}
}

16
src/smt/theory_diff_logic_def.h
View file

@ -1031,7 +1031,8 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::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<numeral> & current_assigments = m_objective_assignments[v];
SASSERT(!current_assigments.empty());
@ -1092,11 +1093,17 @@ expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const
vector<numeral> 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<Ext>::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());