mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

Normalize diff logic's optimal assignments

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-25 00:30:15 +01:00
parent cc3d65e544
commit fff3a1aae5
2 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/network_flow_def.h
View file

@ -50,9 +50,10 @@ namespace smt {
edge const & e = es[i]; edge const & e = es[i];
tout << "(assert (<= (- v" << e.get_source() << " v" << e.get_target() << ") " << e.get_weight() << "))" << std::endl; tout << "(assert (<= (- v" << e.get_source() << " v" << e.get_target() << ") " << e.get_weight() << "))" << std::endl;
}; };
tout << "(maximize (+ "; tout << "(assert (= v0 0))" << std::endl;
tout << "(maximize (+";
for (unsigned i = 0; i < balances.size(); ++i) { for (unsigned i = 0; i < balances.size(); ++i) {
tout << "(* " << balances[i] << " v" << i << ") "; tout << " (* " << balances[i] << " v" << i << ")";
}; };
tout << "))" << std::endl; tout << "))" << std::endl;
tout << "(optimize)" << std::endl; tout << "(optimize)" << std::endl;

12
src/smt/theory_diff_logic_def.h
View file

@ -1015,10 +1015,16 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
// Objective coefficients now become balances // Objective coefficients now become balances
vector<fin_numeral> balances(m_graph.get_num_nodes()); vector<fin_numeral> balances(m_graph.get_num_nodes());
balances.fill(fin_numeral::zero()); balances.fill(fin_numeral::zero());
fin_numeral sum = fin_numeral::zero();
for (unsigned i = 0; i < objective.size(); ++i) { for (unsigned i = 0; i < objective.size(); ++i) {
fin_numeral balance(objective[i].second); fin_numeral balance(objective[i].second);
balances[objective[i].first] = balance; balances[objective[i].first] = balance;
sum += balance;
} }
// HACK: assume that v0 is always value 0
if (balances[0].is_zero()) {
balances[0] = -sum;
}
network_flow<GExt> net_flow(m_graph, balances); network_flow<GExt> net_flow(m_graph, balances);
bool is_optimal = net_flow.min_cost(); bool is_optimal = net_flow.min_cost();
@ -1034,9 +1040,13 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
IF_VERBOSE(1, verbose_stream() << "Initial value of objective " << v << ": " << initial_value << std::endl;); IF_VERBOSE(1, verbose_stream() << "Initial value of objective " << v << ": " << initial_value << std::endl;);
// FIXME: Network Simplex lose precisions when handling infinitesimals // FIXME: Network Simplex lose precisions when handling infinitesimals
SASSERT(objective_value >= initial_value.get_rational());); SASSERT(objective_value >= initial_value.get_rational()););
vector<numeral> & current_assigments = m_objective_assignments[v]; vector<numeral> & current_assigments = m_objective_assignments[v];
SASSERT(!current_assigments.empty()); SASSERT(!current_assigments.empty());
// Normalize optimal assignments so that v0 is fixed to 0
for (unsigned i = 1; i < current_assigments.size(); ++i) {
current_assigments[i] -= current_assigments[0];
}
ast_manager& m = get_manager(); ast_manager& m = get_manager();
IF_VERBOSE(1, IF_VERBOSE(1,
verbose_stream() << "Optimal assigment:" << std::endl; verbose_stream() << "Optimal assigment:" << std::endl;