mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

checked ite-expressions as shared for bounds detection

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-23 19:59:33 +02:00
parent 3ba2e712b2
commit ffc3a36dcb
4 changed files with 35 additions and 244 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/muz/rel/dl_product_relation.cpp
View file

@ -956,20 +956,17 @@ namespace datalog {
void product_relation::ensure_correct_kind() { void product_relation::ensure_correct_kind() {
unsigned rel_cnt = m_relations.size(); unsigned rel_cnt = m_relations.size();
//the rel_cnt==0 part makes us to update the kind also when the relation is newly created //the rel_cnt==0 part makes us to update the kind also when the relation is newly created
bool spec_changed = rel_cnt!=m_spec.size() || rel_cnt==0; bool spec_changed = rel_cnt != m_spec.size() || rel_cnt==0;
if(spec_changed) { if (spec_changed) {
m_spec.resize(rel_cnt); m_spec.resize(rel_cnt);
} }
for(unsigned i=0;i<rel_cnt; i++) { for (unsigned i = 0; i < rel_cnt; i++) {
family_id rkind=m_relations[i]->get_kind(); family_id rkind = m_relations[i]->get_kind();
if(spec_changed || m_spec[i]!=rkind) { spec_changed |= (m_spec[i] != rkind);
spec_changed = true; m_spec[i] = rkind;
m_spec[i]=rkind;
}
} }
if(spec_changed) { if (spec_changed) {
family_id new_kind = get_plugin().get_relation_kind(*this); set_kind(get_plugin().get_relation_kind(*this));
set_kind(new_kind);
} }
} }
@ -978,7 +975,7 @@ namespace datalog {
func_decl* p = 0; func_decl* p = 0;
const relation_signature & sig = get_signature(); const relation_signature & sig = get_signature();
family_id new_kind = get_plugin().get_relation_kind(sig, spec); family_id new_kind = get_plugin().get_relation_kind(sig, spec);
if(new_kind==get_kind()) { if(new_kind == get_kind()) {
return; return;
} }
@ -1001,7 +998,7 @@ namespace datalog {
} }
} }
if(!irel) { if(!irel) {
if(old_sz==0 && m_default_empty) { if(old_sz == 0 && m_default_empty) {
//The relation didn't contain any inner relations but it was empty, //The relation didn't contain any inner relations but it was empty,
//so we make the newly added relations empty as well. //so we make the newly added relations empty as well.
irel = get_manager().mk_empty_relation(sig, new_kind); irel = get_manager().mk_empty_relation(sig, new_kind);
@ -1018,7 +1015,7 @@ namespace datalog {
set_kind(new_kind); set_kind(new_kind);
DEBUG_CODE( DEBUG_CODE(
ensure_correct_kind(); ensure_correct_kind();
SASSERT(get_kind()==new_kind); SASSERT(get_kind() == new_kind);
); );
} }

6
src/smt/smt_context.cpp
View file

@ -3879,9 +3879,13 @@ namespace smt {
bool context::is_shared(enode * n) const { bool context::is_shared(enode * n) const {
n = n->get_root(); n = n->get_root();
unsigned num_th_vars = n->get_num_th_vars(); unsigned num_th_vars = n->get_num_th_vars();
if (m_manager.is_ite(n->get_owner())) {
return true;
}
switch (num_th_vars) { switch (num_th_vars) {
case 0: case 0: {
return false; return false;
}
case 1: { case 1: {
if (m_qmanager->is_shared(n)) if (m_qmanager->is_shared(n))
return true; return true;

6
src/smt/theory_arith.h
View file

@ -879,22 +879,20 @@ namespace smt {
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(bool has_int, 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 inc, bool& has_int, bool& is_shared); bool is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& is_shared);
bool 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);
enum max_min_t { UNBOUNDED, AT_BOUND, OPTIMIZED, BEST_EFFORT}; enum max_min_t { UNBOUNDED, AT_BOUND, OPTIMIZED, BEST_EFFORT};
max_min_t max_min(theory_var v, bool max, bool& has_shared); max_min_t max_min(theory_var v, bool max, bool& has_shared);
max_min_t max_min_orig(row & r, bool max, bool& has_shared);
bool max_min(svector<theory_var> const & vars); bool max_min(svector<theory_var> const & vars);
max_min_t max_min_new(row& r, bool max, bool& has_shared); max_min_t max_min(row& r, bool max, bool& has_shared);
bool unbounded_gain(inf_numeral const & max_gain) const; bool unbounded_gain(inf_numeral const & max_gain) const;
bool safe_gain(inf_numeral const& min_gain, inf_numeral const & max_gain) const; bool safe_gain(inf_numeral const& min_gain, inf_numeral const & max_gain) const;
void normalize_gain(numeral const& divisor, inf_numeral & max_gain) const; void normalize_gain(numeral const& divisor, inf_numeral & max_gain) const;
void init_gains(theory_var x, bool inc, inf_numeral& min_gain, inf_numeral& max_gain); void init_gains(theory_var x, bool inc, inf_numeral& min_gain, inf_numeral& max_gain);
bool update_gains(bool inc, theory_var x_i, numeral const& a_ij, bool update_gains(bool inc, theory_var x_i, numeral const& a_ij,
inf_numeral& min_gain, inf_numeral& max_gain); inf_numeral& min_gain, inf_numeral& max_gain);
bool move_to_bound_new(theory_var x_i, bool inc, unsigned& best_efforts, bool& has_shared); bool move_to_bound(theory_var x_i, bool inc, unsigned& best_efforts, bool& has_shared);
bool pick_var_to_leave( bool pick_var_to_leave(
theory_var x_j, bool inc, numeral & a_ij, theory_var x_j, bool inc, numeral & a_ij,
inf_numeral& min_gain, inf_numeral& max_gain, inf_numeral& min_gain, inf_numeral& max_gain,

242
src/smt/theory_arith_aux.h
View file

@ -961,6 +961,7 @@ namespace smt {
bool theory_arith<Ext>::is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& shared) { bool theory_arith<Ext>::is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& shared) {
context& ctx = get_context(); context& ctx = get_context();
ast_manager& m = get_manager();
shared |= ctx.is_shared(get_enode(x)); shared |= ctx.is_shared(get_enode(x));
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();
@ -1355,154 +1356,6 @@ namespace smt {
} }
/**
\brief Maximize (Minimize) the given temporary row.
Return true if succeeded.
*/
template<typename Ext>
typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min_orig(row & r, bool max, bool& has_shared) {
m_stats.m_max_min++;
bool skipped_row = false;
has_shared = false;
SASSERT(valid_assignment());
theory_var x_i = null_theory_var;
theory_var x_j = null_theory_var;
bool inc = false;
numeral a_ij, curr_a_ij, coeff, curr_coeff;
inf_numeral gain, curr_gain;
#ifdef _TRACE
unsigned i = 0;
#endif
max_min_t result;
while (true) {
x_j = null_theory_var;
x_i = null_theory_var;
gain.reset();
TRACE("opt", tout << "i: " << i << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout); i++;);
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead()) {
theory_var curr_x_j = it->m_var;
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, curr_inc, has_int, has_shared)) {
skipped_row = true;
continue;
}
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.
x_i = null_theory_var; // unbounded
x_j = curr_x_j;
inc = curr_inc;
break;
}
else if (curr_gain > gain) {
x_i = curr_x_i;
x_j = curr_x_j;
a_ij = curr_a_ij;
coeff = curr_coeff;
gain = curr_gain;
inc = curr_inc;
}
else if (curr_gain.is_zero() && (x_i == null_theory_var || curr_x_i < x_i)) {
x_i = curr_x_i;
x_j = curr_x_j;
a_ij = curr_a_ij;
coeff = curr_coeff;
gain = curr_gain;
inc = curr_inc;
// continue
}
}
}
TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << gain << "\n";
tout << "skipped row: " << (skipped_row?"yes":"no") << "\n";
display(tout););
if (x_j == null_theory_var) {
TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";);
SASSERT(valid_assignment());
result = skipped_row?BEST_EFFORT:OPTIMIZED;
break;
}
if (x_i == null_theory_var) {
// can increase/decrease x_j as much as we want.
if (inc && upper(x_j) && !skipped_row) {
update_value(x_j, upper_bound(x_j) - get_value(x_j));
TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
SASSERT(valid_assignment());
continue;
}
if (!inc && lower(x_j) && !skipped_row) {
update_value(x_j, lower_bound(x_j) - get_value(x_j));
TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";);
SASSERT(valid_assignment());
continue;
}
result = skipped_row?BEST_EFFORT:UNBOUNDED;
break;
}
if (!is_fixed(x_j) && is_bounded(x_j) && !skipped_row && (upper_bound(x_j) - lower_bound(x_j) <= gain)) {
// can increase/decrease x_j up to upper/lower bound.
if (inc) {
update_value(x_j, upper_bound(x_j) - get_value(x_j));
TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
}
else {
update_value(x_j, lower_bound(x_j) - get_value(x_j));
TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";);
}
SASSERT(valid_assignment());
continue;
}
TRACE("opt", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n";
if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " ";
if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " ";
tout << "value x_i: " << get_value(x_i) << "\n";
if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " ";
if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " ";
tout << "value x_j: " << get_value(x_j) << "\n";
);
pivot<true>(x_i, x_j, a_ij, false);
SASSERT(is_non_base(x_i));
SASSERT(is_base(x_j));
bool move_xi_to_lower;
if (inc)
move_xi_to_lower = a_ij.is_pos();
else
move_xi_to_lower = a_ij.is_neg();
if (!move_to_bound(x_i, move_xi_to_lower)) {
result = BEST_EFFORT;
break;
}
row & r2 = m_rows[get_var_row(x_j)];
coeff.neg();
add_tmp_row(r, coeff, r2);
SASSERT(r.get_idx_of(x_j) == -1);
SASSERT(valid_assignment());
}
TRACE("opt", display(tout););
return result;
}
/** /**
\brief Select tightest variable x_i to pivot with x_j. The goal \brief Select tightest variable x_i to pivot with x_j. The goal
is to select a x_i such that the value of x_j is increased is to select a x_i such that the value of x_j is increased
@ -1698,13 +1551,14 @@ namespace smt {
Return true if succeeded. Return true if succeeded.
*/ */
template<typename Ext> template<typename Ext>
typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min_new( typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min(
row & r, row & r,
bool max, bool max,
bool& has_shared) { bool& has_shared) {
m_stats.m_max_min++; m_stats.m_max_min++;
unsigned best_efforts = 0; unsigned best_efforts = 0;
bool inc = false; bool inc = false;
context& ctx = get_context();
SASSERT(valid_assignment()); SASSERT(valid_assignment());
@ -1715,7 +1569,7 @@ namespace smt {
#endif #endif
max_min_t result = OPTIMIZED; max_min_t result = OPTIMIZED;
has_shared = false; has_shared = false;
unsigned max_efforts = 10 + (get_context().get_random_value() % 20); unsigned max_efforts = 10 + (ctx.get_random_value() % 20);
while (best_efforts < max_efforts) { while (best_efforts < max_efforts) {
theory_var x_j = null_theory_var; theory_var x_j = null_theory_var;
theory_var x_i = null_theory_var; theory_var x_i = null_theory_var;
@ -1806,8 +1660,13 @@ namespace smt {
SASSERT(valid_assignment()); SASSERT(valid_assignment());
continue; continue;
} }
SASSERT(unbounded_gain(max_gain)); if (ctx.is_shared(get_enode(x_j))) {
best_efforts = 0; ++best_efforts;
}
else {
SASSERT(unbounded_gain(max_gain));
best_efforts = 0;
}
result = UNBOUNDED; result = UNBOUNDED;
break; break;
} }
@ -1841,8 +1700,10 @@ namespace smt {
SASSERT(is_base(x_j)); SASSERT(is_base(x_j));
bool inc_xi = inc?a_ij.is_neg():a_ij.is_pos(); bool inc_xi = inc?a_ij.is_neg():a_ij.is_pos();
if (!move_to_bound_new(x_i, inc_xi, best_efforts, has_shared)) { if (!move_to_bound(x_i, inc_xi, best_efforts, has_shared)) {
// break; TRACE("opt", tout << "can't move bound fully\n";);
// break; // break;
} }
row & r2 = m_rows[get_var_row(x_j)]; row & r2 = m_rows[get_var_row(x_j)];
@ -1863,7 +1724,7 @@ namespace smt {
*/ */
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::move_to_bound_new( bool theory_arith<Ext>::move_to_bound(
theory_var x_i, // variable to move theory_var x_i, // variable to move
bool inc, // increment variable or decrement bool inc, // increment variable or decrement
unsigned& best_efforts, // is bound move a best effort? unsigned& best_efforts, // is bound move a best effort?
@ -1900,75 +1761,6 @@ namespace smt {
return result; return result;
} }
/**
Move the variable x_i maximally towards its bound as long as
bounds of other variables are not violated.
Returns false if an integer bound was truncated and no
progress was made.
*/
template<typename Ext>
bool theory_arith<Ext>::move_to_bound(theory_var x_i, bool move_to_lower) {
inf_numeral delta, delta_abs;
numeral lc(1);
if (move_to_lower) {
delta = lower_bound(x_i) - get_value(x_i);
SASSERT(!delta.is_pos());
}
else {
delta = upper_bound(x_i) - get_value(x_i);
SASSERT(!delta.is_neg());
}
TRACE("opt", tout << "Original delta: " << delta << "\n";);
delta_abs = abs(delta);
//
// Decrease absolute value of delta according to bounds on rows where x_i is used.
//
column & c = m_columns[x_i];
typename svector<col_entry>::iterator it = c.begin_entries();
typename svector<col_entry>::iterator end = c.end_entries();
for (; it != end && delta_abs.is_pos(); ++it) {
if (it->is_dead()) continue;
row & r = m_rows[it->m_row_id];
theory_var s = r.get_base_var();
if (s != null_theory_var && !is_quasi_base(s)) {
numeral const & coeff = r[it->m_row_idx].m_coeff;
SASSERT(!coeff.is_zero());
bool inc_s = coeff.is_pos() ? move_to_lower : !move_to_lower; // NSB: review this..
bound * b = get_bound(s, inc_s);
if (b) {
inf_numeral delta2 = abs((get_value(s) - b->get_value())/coeff);
if (delta2 < delta_abs) {
delta_abs = delta2;
}
}
if (is_int(x_i)) {
lc = lcm(lc, denominator(abs(coeff)));
}
}
}
bool truncated = false;
if (is_int(x_i)) {
inf_numeral tmp = delta_abs/lc;
truncated = !tmp.is_int();
delta_abs = lc*floor(tmp);
}
if (move_to_lower) {
delta = -delta_abs;
}
else {
delta = delta_abs;
}
TRACE("opt", tout << "Safe delta: " << delta << "\n";);
update_value(x_i, delta);
return !truncated || !delta.is_zero();
}
/** /**
\brief Add an entry to a temporary row. \brief Add an entry to a temporary row.
@ -2012,7 +1804,7 @@ namespace smt {
add_tmp_row_entry<true>(m_tmp_row, it->m_coeff, it->m_var); add_tmp_row_entry<true>(m_tmp_row, it->m_coeff, it->m_var);
} }
} }
max_min_t r = max_min_new(m_tmp_row, max, has_shared); max_min_t r = max_min(m_tmp_row, max, has_shared);
if (r == OPTIMIZED) { if (r == OPTIMIZED) {
TRACE("opt", tout << mk_pp(e, get_manager()) << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n"; TRACE("opt", tout << mk_pp(e, get_manager()) << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n";
display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row);); display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row););