mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Anh-Dung Phan 2013-12-27 11:18:25 -08:00
commit 0fabd40e49
3 changed files with 34 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_arith.h
View file

@ -855,8 +855,8 @@ namespace smt {
row m_tmp_row; row m_tmp_row;
void add_tmp_row(row & r1, numeral const & coeff, row const & r2); void add_tmp_row(row & r1, numeral const & coeff, row const & r2);
theory_var pick_var_to_leave(theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain, bool& skiped_row); theory_var pick_var_to_leave(bool has_int, theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain, bool& skiped_row);
bool is_safe_to_leave(theory_var x); bool is_safe_to_leave(theory_var x, bool& has_int);
void move_to_bound(theory_var x_i, bool inc); void move_to_bound(theory_var x_i, bool inc);
template<bool invert> template<bool invert>
void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v); void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v);

28
src/smt/theory_arith_aux.h
View file

@ -928,7 +928,7 @@ namespace smt {
*/ */
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::is_safe_to_leave(theory_var x) { bool theory_arith<Ext>::is_safe_to_leave(theory_var x, bool& has_int) {
if (get_context().is_shared(get_enode(x))) { if (get_context().is_shared(get_enode(x))) {
return false; return false;
@ -936,14 +936,16 @@ namespace smt {
column & c = m_columns[x]; column & c = m_columns[x];
typename svector<col_entry>::iterator it = c.begin_entries(); typename svector<col_entry>::iterator it = c.begin_entries();
typename svector<col_entry>::iterator end = c.end_entries(); typename svector<col_entry>::iterator end = c.end_entries();
has_int = false;
for (; it != end; ++it) { for (; it != end; ++it) {
if (it->is_dead()) continue; if (it->is_dead()) continue;
row const & r = m_rows[it->m_row_id]; row const & r = m_rows[it->m_row_id];
theory_var s = r.get_base_var(); theory_var s = r.get_base_var();
numeral const & coeff = r[it->m_row_idx].m_coeff; numeral const & coeff = r[it->m_row_idx].m_coeff;
if (s != null_theory_var && is_int(s)) has_int = true;
bool is_unsafe = (s != null_theory_var && is_int(s) && !coeff.is_int()); bool is_unsafe = (s != null_theory_var && is_int(s) && !coeff.is_int());
is_unsafe = is_unsafe || (s != null_theory_var && get_context().is_shared(get_enode(s))); is_unsafe = is_unsafe || (s != null_theory_var && get_context().is_shared(get_enode(s)));
TRACE("opt", tout << "is v" << x << " safe to leave for v" << s << "? " << (is_unsafe?"no":"yes") << "\n"; TRACE("opt", tout << "is v" << x << " safe to leave for v" << s << "? " << (is_unsafe?"no":"yes") << " " << (has_int?"int":"real") << "\n";
display_row(tout, r, true);); display_row(tout, r, true););
if (is_unsafe) return false; if (is_unsafe) return false;
} }
@ -952,7 +954,9 @@ namespace smt {
} }
template<typename Ext> template<typename Ext>
theory_var theory_arith<Ext>::pick_var_to_leave(theory_var x_j, bool inc, numeral & a_ij, inf_numeral & gain, bool& skipped_row) { theory_var theory_arith<Ext>::pick_var_to_leave(
bool has_int, theory_var x_j, bool inc,
numeral & a_ij, inf_numeral & gain, bool& skipped_row) {
TRACE("opt", tout << "selecting variable to replace v" << x_j << ", inc: " << inc << "\n";); TRACE("opt", tout << "selecting variable to replace v" << x_j << ", inc: " << inc << "\n";);
theory_var x_i = null_theory_var; theory_var x_i = null_theory_var;
inf_numeral curr_gain; inf_numeral curr_gain;
@ -982,6 +986,10 @@ namespace smt {
skipped_row = true; skipped_row = true;
continue; continue;
} }
if (!curr_gain.is_int() && has_int) {
skipped_row = true;
continue;
}
x_i = s; x_i = s;
a_ij = coeff; a_ij = coeff;
gain = curr_gain; gain = curr_gain;
@ -1294,6 +1302,7 @@ namespace smt {
#ifdef _TRACE #ifdef _TRACE
unsigned i = 0; unsigned i = 0;
#endif #endif
max_min_t result;
while (true) { while (true) {
x_j = null_theory_var; x_j = null_theory_var;
x_i = null_theory_var; x_i = null_theory_var;
@ -1307,13 +1316,14 @@ namespace smt {
SASSERT(is_non_base(curr_x_j)); SASSERT(is_non_base(curr_x_j));
curr_coeff = it->m_coeff; curr_coeff = it->m_coeff;
bool curr_inc = curr_coeff.is_pos() ? max : !max; bool curr_inc = curr_coeff.is_pos() ? max : !max;
bool has_int = false;
if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j))) if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j)))
continue; // variable cannot be used for max/min. continue; // variable cannot be used for max/min.
if (!is_safe_to_leave(curr_x_j)) { if (!is_safe_to_leave(curr_x_j, has_int)) {
skipped_row = true; skipped_row = true;
continue; continue;
} }
theory_var curr_x_i = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, curr_gain, skipped_row); theory_var curr_x_i = pick_var_to_leave(has_int, curr_x_j, curr_inc, curr_a_ij, curr_gain, skipped_row);
if (curr_x_i == null_theory_var) { if (curr_x_i == null_theory_var) {
TRACE("opt", tout << "unbounded\n";); TRACE("opt", tout << "unbounded\n";);
// we can increase/decrease curr_x_j as much as we want. // we can increase/decrease curr_x_j as much as we want.
@ -1348,7 +1358,8 @@ namespace smt {
TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";); TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";);
SASSERT(valid_row_assignment()); SASSERT(valid_row_assignment());
SASSERT(satisfy_bounds()); SASSERT(satisfy_bounds());
return skipped_row?BEST_EFFORT:OPTIMIZED; result = skipped_row?BEST_EFFORT:OPTIMIZED;
break;
} }
if (x_i == null_theory_var) { if (x_i == null_theory_var) {
@ -1367,7 +1378,8 @@ namespace smt {
SASSERT(satisfy_bounds()); SASSERT(satisfy_bounds());
continue; continue;
} }
return UNBOUNDED; result = skipped_row?BEST_EFFORT:UNBOUNDED;
break;
} }
if (!is_fixed(x_j) && is_bounded(x_j) && (upper_bound(x_j) - lower_bound(x_j) <= gain)) { if (!is_fixed(x_j) && is_bounded(x_j) && (upper_bound(x_j) - lower_bound(x_j) <= gain)) {
@ -1413,6 +1425,8 @@ namespace smt {
SASSERT(valid_row_assignment()); SASSERT(valid_row_assignment());
SASSERT(satisfy_bounds()); SASSERT(satisfy_bounds());
} }
TRACE("opt", display(tout););
return result;
} }
/** /**

15
src/smt/theory_arith_int.h
View file

@ -34,10 +34,14 @@ namespace smt {
// //
// ----------------------------------- // -----------------------------------
/** /**
\brief Move non base variables to one of its bounds. \brief Move non base variables to one of its bounds.
If the variable does not have bounds, it is integer, but it is not assigned to an integer value, then the If the variable does not have bounds, it is integer, but it is not assigned to an integer value, then the
variable is set to an integer value. variable is set to an integer value.
In mixed integer/real problems moving a real variable to a bound could cause an integer value to
have an infinitesimal. Such an assignment would disable mk_gomory_cut, and Z3 would loop.
*/ */
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::move_non_base_vars_to_bounds() { void theory_arith<Ext>::move_non_base_vars_to_bounds() {
@ -413,10 +417,10 @@ namespace smt {
for (; it != end; ++it) { for (; it != end; ++it) {
// All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed). // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed).
if (!it->is_dead() && it->m_var != b && (!at_bound(it->m_var) || !get_value(it->m_var).is_rational())) { if (!it->is_dead() && it->m_var != b && (!at_bound(it->m_var) || !get_value(it->m_var).is_rational())) {
TRACE("gomory_cut", tout << "row is gomory cut target:\n"; TRACE("gomory_cut", tout << "row is not gomory cut target:\n";
display_var(tout, it->m_var); display_var(tout, it->m_var);
tout << "at_bound: " << at_bound(it->m_var) << "\n"; tout << "at_bound: " << at_bound(it->m_var) << "\n";
tout << "infinitesimal: " << get_value(it->m_var).is_rational() << "\n";); tout << "infinitesimal: " << !get_value(it->m_var).is_rational() << "\n";);
return false; return false;
} }
} }
@ -1378,6 +1382,7 @@ namespace smt {
m_branch_cut_counter++; m_branch_cut_counter++;
// TODO: add giveup code // TODO: add giveup code
if (m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) { if (m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) {
TRACE("opt", display(tout););
move_non_base_vars_to_bounds(); move_non_base_vars_to_bounds();
if (!make_feasible()) { if (!make_feasible()) {
TRACE("arith_int", tout << "failed to move variables to bounds.\n";); TRACE("arith_int", tout << "failed to move variables to bounds.\n";);
@ -1389,7 +1394,9 @@ namespace smt {
TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";); TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";);
SASSERT(is_base(int_var)); SASSERT(is_base(int_var));
row const & r = m_rows[get_var_row(int_var)]; row const & r = m_rows[get_var_row(int_var)];
mk_gomory_cut(r); if (!mk_gomory_cut(r)) {
// silent failure
}
return FC_CONTINUE; return FC_CONTINUE;
} }
} }
@ -1399,7 +1406,7 @@ namespace smt {
} }
theory_var int_var = find_infeasible_int_base_var(); theory_var int_var = find_infeasible_int_base_var();
if (int_var != null_theory_var) { if (int_var != null_theory_var) {
TRACE("arith_int", tout << "v" << int_var << " does not have and integer assignment: " << get_value(int_var) << "\n";); TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";);
// apply branching // apply branching
branch_infeasible_int_var(int_var); branch_infeasible_int_var(int_var);
return FC_CONTINUE; return FC_CONTINUE;