diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 39f991c72..7e594abe5 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -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(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(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); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 95c7fdfad..1ce56ffe8 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3223,13 +3223,50 @@ namespace smt { bool theory_arith::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 bool theory_arith::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); } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index eb64aae5d..3b59961a3 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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; } ); /*