mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

tracing code for string-integer integration

Browse source
This commit is contained in:
Murphy Berzish 2016-06-07 17:40:59 -04:00
parent 62aeff90c5
commit 513b4922ee
3 changed files with 80 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_arith.h
View file

@ -576,7 +576,19 @@ namespace smt {
return is_free(get_context().get_enode(n)->get_th_var(get_id()));
}
bool is_fixed(theory_var v) const;
void set_bound_core(theory_var v, bound * new_bound, bool upper) { m_bounds[static_cast<unsigned>(upper)][v] = new_bound; }
void set_bound_core(theory_var v, bound * new_bound, bool upper) {
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_nl_propagated_flag(unsigned old_trail_size);
void set_bound(bound * new_bound, bool upper);

41
src/smt/theory_arith_core.h
View file

@ -3223,13 +3223,50 @@ namespace smt {
bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id());
inf_numeral val;
return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r);
// rewrites for tracing purposes
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>
bool theory_arith<Ext>::get_lower(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id());
bound* b = (v == null_theory_var) ? 0 : lower(v);
bound * b;
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);
}

31
src/smt/theory_str.cpp
View file

@ -1470,6 +1470,14 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
}
}
{
rational x_lb, x_ub;
bool x_lb_p = lower_bound(x, x_lb);
bool x_ub_p = upper_bound(x, x_ub);
TRACE("t_str_detail", tout << "X [" << x_lb << ":" << x_ub << "]" << std::endl
<< "lb? " << (x_lb_p?"yes":"no") << " ub? " << (x_ub_p?"yes":"no") << std::endl;);
}
TRACE("t_str_detail", tout
<< "len(x) = " << (x_len_exists ? x_len.to_string() : "?") << std::endl
<< "len(y) = " << (y_len_exists ? y_len.to_string() : "?") << std::endl
@ -2388,21 +2396,25 @@ bool theory_str::get_value(expr* e, rational& val) const {
if (!tha) {
return false;
}
TRACE("t_str_int", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;);
expr_ref _val(m);
enode * en_e = ctx.get_enode(e);
enode * it = en_e;
do {
if (tha->get_value(it, _val)) {
// found an arithmetic term
TRACE("t_str_int", tout << "get_value[" << mk_pp(it->get_owner(), m) << "] = " << mk_pp(_val, m)
<< std::endl;);
return m_autil.is_numeral(_val, val) && val.is_int();
} else {
TRACE("t_str_int", tout << "get_value[" << mk_pp(it->get_owner(), m) << "] not found" << std::endl;);
}
it = it->get_next();
} while (it != en_e);
TRACE("t_str_int", tout << "no arithmetic values found in eqc" << std::endl;);
return false;
}
// TODO these methods currently crash the solver, find out why
bool theory_str::lower_bound(expr* _e, rational& lo) {
context& ctx = get_context();
ast_manager & m = get_manager();
@ -2460,6 +2472,19 @@ bool theory_str::get_len_value(expr* e, rational& val) {
}
else {
len = mk_strlen(c);
// debugging
TRACE("t_str_int", {
tout << mk_pp(len, m) << ":" << std::endl
<< (ctx.is_relevant(len.get()) ? "relevant" : "not relevant") << std::endl
<< (ctx.e_internalized(len) ? "internalized" : "not internalized") << std::endl
;
if (ctx.e_internalized(len)) {
enode * e_len = ctx.get_enode(len);
tout << "has " << e_len->get_num_th_vars() << " theory vars" << std::endl;
}
});
if (ctx.e_internalized(len) && get_value(len, val1)) {
val += val1;
TRACE("t_str_int", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has length " << val1 << std::endl;);
@ -3225,7 +3250,7 @@ void theory_str::init_search_eh() {
unsigned nFormulas = ctx.get_num_asserted_formulas();
for (unsigned i = 0; i < nFormulas; ++i) {
expr * ex = ctx.get_asserted_formula(i);
tout << mk_ismt2_pp(ex, m) << std::endl;
tout << mk_ismt2_pp(ex, m) << (ctx.is_relevant(ex) ? " (rel)" : " (NOT REL)") << std::endl;
}
);
/*