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

debug looping behavior

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-27 07:50:25 -08:00
parent 58f8181a74
commit 32762b54a7
3 changed files with 34 additions and 13 deletions
Show stats 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;
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);
bool is_safe_to_leave(theory_var x);
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& has_int);
void move_to_bound(theory_var x_i, bool inc);
template<bool invert>
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>
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))) {
return false;
@ -936,14 +936,16 @@ namespace smt {
column & c = m_columns[x];
typename svector<col_entry>::iterator it = c.begin_entries();
typename svector<col_entry>::iterator end = c.end_entries();
has_int = false;
for (; it != end; ++it) {
if (it->is_dead()) continue;
row const & r = m_rows[it->m_row_id];
theory_var s = r.get_base_var();
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());
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););
if (is_unsafe) return false;
}
@ -952,7 +954,9 @@ namespace smt {
}
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";);
theory_var x_i = null_theory_var;
inf_numeral curr_gain;
@ -982,6 +986,10 @@ namespace smt {
skipped_row = true;
continue;
}
if (!curr_gain.is_int() && has_int) {
skipped_row = true;
continue;
}
x_i = s;
a_ij = coeff;
gain = curr_gain;
@ -1294,6 +1302,7 @@ namespace smt {
#ifdef _TRACE
unsigned i = 0;
#endif
max_min_t result;
while (true) {
x_j = null_theory_var;
x_i = null_theory_var;
@ -1307,13 +1316,14 @@ namespace smt {
SASSERT(is_non_base(curr_x_j));
curr_coeff = it->m_coeff;
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)))
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;
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) {
TRACE("opt", tout << "unbounded\n";);
// 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";);
SASSERT(valid_row_assignment());
SASSERT(satisfy_bounds());
return skipped_row?BEST_EFFORT:OPTIMIZED;
result = skipped_row?BEST_EFFORT:OPTIMIZED;
break;
}
if (x_i == null_theory_var) {
@ -1367,7 +1378,8 @@ namespace smt {
SASSERT(satisfy_bounds());
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)) {
@ -1413,6 +1425,8 @@ namespace smt {
SASSERT(valid_row_assignment());
SASSERT(satisfy_bounds());
}
TRACE("opt", display(tout););
return result;
}
/**

15
src/smt/theory_arith_int.h
View file

@ -33,11 +33,15 @@ namespace smt {
// Integrality
//
// -----------------------------------
/**
\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
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>
void theory_arith<Ext>::move_non_base_vars_to_bounds() {
@ -413,10 +417,10 @@ namespace smt {
for (; it != end; ++it) {
// 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())) {
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);
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;
}
}
@ -1378,6 +1382,7 @@ namespace smt {
m_branch_cut_counter++;
// TODO: add giveup code
if (m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) {
TRACE("opt", display(tout););
move_non_base_vars_to_bounds();
if (!make_feasible()) {
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";);
SASSERT(is_base(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;
}
}
@ -1399,7 +1406,7 @@ namespace smt {
}
theory_var int_var = find_infeasible_int_base_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
branch_infeasible_int_var(int_var);
return FC_CONTINUE;