From 19bb55e396d0414e61cdc496ec8d32d08eb9d8a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Aug 2017 10:22:36 -0700 Subject: [PATCH] recognize theory_i_arith to fix #1200 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 103 ++++++++++++++++++++++++++++----------- src/util/scoped_vector.h | 4 +- 2 files changed, 76 insertions(+), 31 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 14ee3b073..1d3ab47bb 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -18,6 +18,7 @@ Revision History: --*/ +#include #include "smt/proto_model/value_factory.h" #include "smt/smt_context.h" #include "smt/smt_model_generator.h" @@ -275,7 +276,22 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << ">>int_string\n";); return FC_CONTINUE; } - if (reduce_length_eq() || branch_unit_variable() || branch_binary_variable() || branch_variable_mb() || branch_variable()) { + if (reduce_length_eq()) { + ++m_stats.m_branch_variable; + TRACE("seq", tout << ">>reduce length\n";); + return FC_CONTINUE; + } + if (branch_unit_variable()) { + ++m_stats.m_branch_variable; + TRACE("seq", tout << ">>branch_unit_variable\n";); + return FC_CONTINUE; + } + if (branch_binary_variable() || branch_variable_mb()) { + ++m_stats.m_branch_variable; + TRACE("seq", tout << ">>branch_variable\n";); + return FC_CONTINUE; + } + if (branch_variable()) { ++m_stats.m_branch_variable; TRACE("seq", tout << ">>branch_variable\n";); return FC_CONTINUE; @@ -318,10 +334,9 @@ bool theory_seq::reduce_length_eq() { } bool theory_seq::branch_binary_variable() { - unsigned sz = m_eqs.size(); - for (unsigned i = 0; i < sz; ++i) { - eq const& e = m_eqs[i]; + for (eq const& e : m_eqs) { if (branch_binary_variable(e)) { + TRACE("seq", display_equation(tout, e);); return true; } } @@ -399,19 +414,21 @@ bool theory_seq::branch_binary_variable(eq const& e) { } bool theory_seq::branch_unit_variable() { - unsigned sz = m_eqs.size(); - for (unsigned i = 0; i < sz; ++i) { - eq const& e = m_eqs[i]; + bool result = false; + for (eq const& e : m_eqs) { if (is_unit_eq(e.ls(), e.rs())) { branch_unit_variable(e.dep(), e.ls()[0], e.rs()); - return true; + result = true; + break; } else if (is_unit_eq(e.rs(), e.ls())) { branch_unit_variable(e.dep(), e.rs()[0], e.ls()); - return true; + result = true; + break; } } - return false; + CTRACE("seq", result, "branch unit variable";); + return result; } /** @@ -434,17 +451,20 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector context& ctx = get_context(); rational lenX; if (!get_length(X, lenX)) { + TRACE("seq", tout << "enforce length on " << mk_pp(X, m) << "\n";); enforce_length(ensure_enode(X)); return; } if (lenX > rational(units.size())) { expr_ref le(m_autil.mk_le(m_util.str.mk_length(X), m_autil.mk_int(units.size())), m); + TRACE("seq", tout << "propagate length on " << mk_pp(X, m) << "\n";); propagate_lit(dep, 0, 0, mk_literal(le)); return; } SASSERT(lenX.is_unsigned()); unsigned lX = lenX.get_unsigned(); if (lX == 0) { + TRACE("seq", tout << "set empty length " << mk_pp(X, m) << "\n";); set_empty(X); } else { @@ -454,8 +474,10 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector literal_vector lits; lits.push_back(lit); propagate_eq(dep, lits, X, R, true); + TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";); } else { + TRACE("seq", tout << "set phase " << mk_pp(X, m) << "\n";); ctx.mark_as_relevant(lit); ctx.force_phase(lit); } @@ -494,9 +516,11 @@ bool theory_seq::branch_variable_mb() { } if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) { TRACE("seq", tout << "split lengths\n";); - return true; + change = true; + break; } } + TRACE("seq", tout << "branch_variable_mb\n";); return change; } @@ -651,6 +675,7 @@ bool theory_seq::branch_variable() { eq const& e = m_eqs[k]; if (branch_variable(e)) { + TRACE("seq", tout << "branch variable\n";); return true; } @@ -1577,6 +1602,7 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con len2 += len; } if (len1 == len2 && 0 < j && j < rs.size() && reduce_length(1, j, true, ls, rs, deps)) { + TRACE("seq", tout << "l equal\n";); return true; } } @@ -1586,6 +1612,7 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con len2 += len; } if (len1 == len2 && 0 < j && j < ls.size() && reduce_length(j, 1, true, ls, rs, deps)) { + TRACE("seq", tout << "r equal\n";); return true; } } @@ -1595,6 +1622,7 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con len2 += len; } if (len1 == len2 && 0 < j && j < rs.size() && reduce_length(ls.size()-1, rs.size()-j, false, ls, rs, deps)) { + TRACE("seq", tout << "l suffix equal\n";); return true; } } @@ -1604,6 +1632,7 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con len2 += len; } if (len1 == len2 && 0 < j && j < ls.size() && reduce_length(ls.size()-j, rs.size()-1, false, ls, rs, deps)) { + TRACE("seq", tout << "r suffix equal\n";); return true; } } @@ -1641,6 +1670,7 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect deps = mk_join(deps, lit); m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps)); propagate_eq(deps, lits, l, r, true); + TRACE("seq", tout << "propagate eq\nlhs: " << lhs << "\nrhs: " << rhs << "\n";); return true; } else { @@ -2510,8 +2540,8 @@ void theory_seq::display_nc(std::ostream& out, nc const& nc) const { } void theory_seq::display_equations(std::ostream& out) const { - for (unsigned i = 0; i < m_eqs.size(); ++i) { - display_equation(out, m_eqs[i]); + for (eq const& e : m_eqs) { + display_equation(out, e); } } @@ -2522,10 +2552,10 @@ void theory_seq::display_equation(std::ostream& out, eq const& e) const { void theory_seq::display_disequations(std::ostream& out) const { bool first = true; - for (unsigned i = 0; i < m_nqs.size(); ++i) { + for (ne const& n : m_nqs) { if (first) out << "Disequations:\n"; first = false; - display_disequation(out, m_nqs[i]); + display_disequation(out, n); } } @@ -3406,24 +3436,32 @@ enode* theory_seq::ensure_enode(expr* e) { return n; } -static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) { +template +static T* get_th_arith(context& ctx, theory_id afid, expr* e) { theory* th = ctx.get_theory(afid); if (th && ctx.e_internalized(e)) { - return dynamic_cast(th); + return dynamic_cast(th); } else { return 0; } } +static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v) { + theory_mi_arith* tha = get_th_arith(ctx, afid, e); + if (tha) return tha->get_value(ctx.get_enode(e), v); + theory_i_arith* thi = get_th_arith(ctx, afid, e); + if (thi) return thi->get_value(ctx.get_enode(e), v); + TRACE("seq", tout << "no arithmetic theory\n";); + return false; +} + bool theory_seq::get_num_value(expr* e, rational& val) const { context& ctx = get_context(); - theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); expr_ref _val(m); - if (!tha) return false; enode* next = ctx.get_enode(e), *n = next; do { - if (tha->get_value(next, _val) && m_autil.is_numeral(_val, val) && val.is_int()) { + if (get_arith_value(ctx, m_autil.get_family_id(), next->get_owner(), _val) && m_autil.is_numeral(_val, val) && val.is_int()) { return true; } next = next->get_next(); @@ -3435,27 +3473,31 @@ bool theory_seq::get_num_value(expr* e, rational& val) const { bool theory_seq::lower_bound(expr* _e, rational& lo) const { context& ctx = get_context(); expr_ref e(m_util.str.mk_length(_e), m); - theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); expr_ref _lo(m); - if (!tha || !tha->get_lower(ctx.get_enode(e), _lo)) return false; + theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); + if (tha && !tha->get_lower(ctx.get_enode(e), _lo)) return false; + if (!tha) { + theory_i_arith* thi = get_th_arith(ctx, m_autil.get_family_id(), e); + if (!thi || !thi->get_lower(ctx.get_enode(e), _lo)) return false; + } return m_autil.is_numeral(_lo, lo) && lo.is_int(); } bool theory_seq::upper_bound(expr* _e, rational& hi) const { context& ctx = get_context(); expr_ref e(m_util.str.mk_length(_e), m); - theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); + theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); expr_ref _hi(m); - if (!tha || !tha->get_upper(ctx.get_enode(e), _hi)) return false; + if (tha && !tha->get_upper(ctx.get_enode(e), _hi)) return false; + if (!tha) { + theory_i_arith* thi = get_th_arith(ctx, m_autil.get_family_id(), e); + if (!thi || !thi->get_upper(ctx.get_enode(e), _hi)) return false; + } return m_autil.is_numeral(_hi, hi) && hi.is_int(); } bool theory_seq::get_length(expr* e, rational& val) const { context& ctx = get_context(); - theory* th = ctx.get_theory(m_autil.get_family_id()); - if (!th) return false; - theory_mi_arith* tha = dynamic_cast(th); - if (!tha) return false; rational val1; expr_ref len(m), len_val(m); expr* e1 = 0, *e2 = 0; @@ -3480,20 +3522,23 @@ bool theory_seq::get_length(expr* e, rational& val) const { val += rational(s.length()); } else if (!has_length(c)) { + TRACE("seq", tout << "literal has no length " << mk_pp(c, m) << "\n";); return false; } else { len = m_util.str.mk_length(c); if (ctx.e_internalized(len) && - tha->get_value(ctx.get_enode(len), len_val) && + get_arith_value(ctx, m_autil.get_family_id(), len, len_val) && m_autil.is_numeral(len_val, val1)) { val += val1; } else { + TRACE("seq", tout << "length has not been internalized " << mk_pp(c, m) << "\n";); return false; } } } + CTRACE("seq", !val.is_int(), "length is not an integer\n";); return val.is_int(); } diff --git a/src/util/scoped_vector.h b/src/util/scoped_vector.h index d4c5301e6..5935ab6fa 100644 --- a/src/util/scoped_vector.h +++ b/src/util/scoped_vector.h @@ -113,8 +113,8 @@ public: } }; - iterator begin() { return iterator(*this, 0); } - iterator end() { return iterator(*this, m_size); } + iterator begin() const { return iterator(*this, 0); } + iterator end() const { return iterator(*this, m_size); } void push_back(T const& t) { set_index(m_size, m_elems.size());