mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

Block lower bound of difference logic objectives

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-01 08:05:29 +01:00
parent 87141f4cb3
commit 736d43c084
3 changed files with 37 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/network_flow_def.h
View file

@ -308,7 +308,7 @@ namespace smt {
m_thread[z] = y; m_thread[z] = y;
n = q; n = q;
last = m_final[q]; last = m_final[q];
while (n != last) { while (n != last && n != -1) {
m_depth[n] += 1 + m_depth[p]; m_depth[n] += 1 + m_depth[p];
n = m_pred[n]; n = m_pred[n];
} }
@ -495,7 +495,7 @@ namespace smt {
// m_pred is predecessor link // m_pred is predecessor link
// m_depth depth counting from a root note. // m_depth depth counting from a root note.
// m_graph // m_graph
#if 0
node root = m_pred.size()-1; node root = m_pred.size()-1;
for (unsigned i = 0; i < m_upwards.size(); ++i) { for (unsigned i = 0; i < m_upwards.size(); ++i) {
if (m_upwards[i]) { if (m_upwards[i]) {
@ -509,8 +509,7 @@ namespace smt {
// m_thread forms a spanning tree over [0..root] // m_thread forms a spanning tree over [0..root]
// union-find structure: // union-find structure:
svector<int> roots(root+1, -1); svector<int> roots(root+1, -1);
#if 0
for (unsigned i = 0; i < m_thread.size(); ++i) { for (unsigned i = 0; i < m_thread.size(); ++i) {
if (m_states[i] == BASIS) { if (m_states[i] == BASIS) {
node x = m_thread[i]; node x = m_thread[i];

5
src/smt/theory_diff_logic.h
View file

@ -189,8 +189,9 @@ namespace smt {
// For optimization purpose // For optimization purpose
typedef vector <std::pair<theory_var, rational> > objective_term; typedef vector <std::pair<theory_var, rational> > objective_term;
vector<objective_term> m_objectives; vector<objective_term> m_objectives;
vector<rational> m_objective_consts; vector<rational> m_objective_consts;
vector<vector<numeral> > m_objective_assignments;
numeral m_objective_value; numeral m_objective_value;
// Set a conflict due to a negative cycle. // Set a conflict due to a negative cycle.

34
src/smt/theory_diff_logic_def.h
View file

@ -778,6 +778,7 @@ void theory_diff_logic<Ext>::reset_eh() {
m_non_diff_logic_exprs = false; m_non_diff_logic_exprs = false;
m_objectives .reset(); m_objectives .reset();
m_objective_consts.reset(); m_objective_consts.reset();
m_objective_assignments.reset();
theory::reset_eh(); theory::reset_eh();
} }
@ -1023,7 +1024,7 @@ bool theory_diff_logic<Ext>::maximize(theory_var v) {
vector<numeral> potentials; vector<numeral> potentials;
m_objective_value = net_flow.get_optimal_solution(potentials, true); m_objective_value = net_flow.get_optimal_solution(potentials, true);
std::cout << "Objective value of var " << v << ": " << m_objective_value << std::endl; std::cout << "Objective value of var " << v << ": " << m_objective_value << std::endl;
// TODO: return the model of the optimal solution from potentials m_objective_assignments[v] = potentials;
TRACE("network_flow", TRACE("network_flow",
for (unsigned i = 0; i < potentials.size(); ++i) { for (unsigned i = 0; i < potentials.size(); ++i) {
tout << "v" << i << " -> " << potentials[i] << "\n"; tout << "v" << i << " -> " << potentials[i] << "\n";
@ -1041,9 +1042,11 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
objective_term objective; objective_term objective;
theory_var result = m_objectives.size(); theory_var result = m_objectives.size();
rational q(1), r(0); rational q(1), r(0);
vector<numeral> vr;
if (internalize_objective(term, q, r, objective)) { if (internalize_objective(term, q, r, objective)) {
m_objectives.push_back(objective); m_objectives.push_back(objective);
m_objective_consts.push_back(r); m_objective_consts.push_back(r);
m_objective_assignments.push_back(vr);
} }
else { else {
result = null_theory_var; result = null_theory_var;
@ -1063,7 +1066,6 @@ expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const
ast_manager& m = get_manager(); ast_manager& m = get_manager();
objective_term const& t = m_objectives[v]; objective_term const& t = m_objectives[v];
expr_ref e(m), f(m), f2(m); expr_ref e(m), f(m), f2(m);
// hacky implementation for now.
if (t.size() == 1 && t[0].second.is_one()) { if (t.size() == 1 && t[0].second.is_one()) {
f = get_enode(t[0].first)->get_owner(); f = get_enode(t[0].first)->get_owner();
} }
@ -1081,8 +1083,34 @@ expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const
f = m_util.mk_sub(f, f2); f = m_util.mk_sub(f, f2);
} }
else { else {
NOT_IMPLEMENTED_YET(); expr_ref_vector disj(m);
vector<numeral> const & ns = m_objective_assignments[v];
inf_rational val;
rational r, s;
for (unsigned i = 0; 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();
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));
}
else if (t[i].second.is_neg()) {
disj.push_back(m_util.mk_lt(f, e));
}
else if (t[i].second.is_pos() && val.get_infinitesimal().is_neg()) {
disj.push_back(m_util.mk_ge(f, e));
}
else if (t[i].second.is_pos()) {
disj.push_back(m_util.mk_gt(f, e));
}
else {
}
}
return m.mk_or(disj.size(), disj.c_ptr());
} }
inf_rational new_val = val - inf_rational(m_objective_consts[v]); inf_rational new_val = val - inf_rational(m_objective_consts[v]);
e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f)); e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f));