mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

remove trace code from theory_arith

Browse source
This commit is contained in:
Murphy Berzish 2017-05-02 15:39:15 -04:00
parent 0862949e66
commit e6d527c5d5
2 changed files with 3 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_arith.h
View file

@ -577,19 +577,7 @@ namespace smt {
return is_free(get_context().get_enode(n)->get_th_var(get_id())); return is_free(get_context().get_enode(n)->get_th_var(get_id()));
} }
bool is_fixed(theory_var v) const; bool is_fixed(theory_var v) const;
void set_bound_core(theory_var v, bound * new_bound, bool upper) { void set_bound_core(theory_var v, bound * new_bound, bool upper) { m_bounds[static_cast<unsigned>(upper)][v] = new_bound; }
TRACE("t_str_int",
tout << "setting " << (upper ? "upper" : "lower") << " bound ";
if (new_bound) {
tout << new_bound->get_value();
} else {
tout << "(NULL)";
}
tout << " for theory var v#" << v;
tout << std::endl;
);
m_bounds[static_cast<unsigned>(upper)][v] = new_bound;
}
void restore_bound(theory_var v, bound * new_bound, bool upper) { set_bound_core(v, new_bound, upper); } void restore_bound(theory_var v, bound * new_bound, bool upper) { set_bound_core(v, new_bound, upper); }
void restore_nl_propagated_flag(unsigned old_trail_size); void restore_nl_propagated_flag(unsigned old_trail_size);
void set_bound(bound * new_bound, bool upper); void set_bound(bound * new_bound, bool upper);

41
src/smt/theory_arith_core.h
View file

@ -3263,50 +3263,13 @@ namespace smt {
bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) { bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id()); theory_var v = n->get_th_var(get_id());
inf_numeral val; inf_numeral val;
// rewrites for tracing purposes return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r);
if (v == null_theory_var) {
TRACE("t_str_int", tout << "WARNING: enode " << mk_pp(n->get_owner(), get_manager())
<< " attached to null theory var" << std::endl;
);
return false;
} else {
val = get_value(v);
TRACE("t_str_int", tout << "enode " << mk_pp(n->get_owner(), get_manager())
<< " attached to theory var v#" << v
<< ", has val = " << val
<< std::endl;
);
if (!is_int(v) || val.is_int()) {
return to_expr(val, is_int(v), r);
} else {
return false;
}
}
// return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r);
} }
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::get_lower(enode * n, expr_ref & r) { bool theory_arith<Ext>::get_lower(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id()); theory_var v = n->get_th_var(get_id());
bound * b; bound * b = (v == null_theory_var) ? 0 : lower(v);
if (v == null_theory_var) {
TRACE("t_str_int", tout << "WARNING: enode " << mk_pp(n->get_owner(), get_manager())
<< " attached to null theory var" << std::endl;
);
b = 0;
} else {
b = lower(v);
TRACE("t_str_int",
tout << "enode " << mk_pp(n->get_owner(), get_manager())
<< " attached to theory var v#" << v
<< std::endl;
if (b) {
tout << "lower bound = " << b->get_value() << std::endl;
} else {
tout << "WARNING: b = NULL" << std::endl;
}
);
}
return b && to_expr(b->get_value(), is_int(v), r); return b && to_expr(b->get_value(), is_int(v), r);
} }