From 377d0600362652a0d889a7aa0c0b149b6ff7e8c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Feb 2021 18:09:40 -0800 Subject: [PATCH] move to separate axiom management Signed-off-by: Nikolaj Bjorner --- src/ast/char_decl_plugin.cpp | 10 + src/ast/char_decl_plugin.h | 11 +- src/ast/rewriter/seq_axioms.cpp | 66 +++- src/ast/rewriter/seq_axioms.h | 23 +- src/ast/rewriter/seq_rewriter.cpp | 94 +++++- src/ast/rewriter/seq_rewriter.h | 2 + src/ast/rewriter/seq_skolem.h | 2 + src/ast/seq_decl_plugin.h | 3 + src/smt/seq_axioms.cpp | 508 +----------------------------- src/smt/seq_axioms.h | 29 +- src/smt/seq_eq_solver.cpp | 74 +++-- src/smt/theory_char.cpp | 26 ++ src/smt/theory_char.h | 1 + src/smt/theory_seq.cpp | 12 +- src/smt/theory_seq.h | 4 +- src/solver/check_logic.cpp | 2 +- 16 files changed, 302 insertions(+), 565 deletions(-) diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index e348dc4bc..7e0f6d4af 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -69,6 +69,15 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_func_decl(symbol("char.to_int"), arity, domain, a.mk_int(), func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception(msg.str()); + case OP_CHAR_IS_DIGIT: + if (num_parameters != 0) + msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters; + else if (arity != 1) + msg << "incorrect number of arguments passed. Expected one character, received " << arity; + else { + return m.mk_func_decl(symbol("char.is_digit"), arity, domain, m.mk_bool_sort(), func_decl_info(m_family_id, k, 0, nullptr)); + } + m.raise_exception(msg.str()); default: UNREACHABLE(); } @@ -85,6 +94,7 @@ void char_decl_plugin::get_op_names(svector& op_names, symbol cons op_names.push_back(builtin_name("char.<=", OP_CHAR_LE)); op_names.push_back(builtin_name("Char", OP_CHAR_CONST)); op_names.push_back(builtin_name("char.to_int", OP_CHAR_TO_INT)); + op_names.push_back(builtin_name("char.is_digit", OP_CHAR_IS_DIGIT)); } void char_decl_plugin::get_sort_names(svector& sort_names, symbol const& logic) { diff --git a/src/ast/char_decl_plugin.h b/src/ast/char_decl_plugin.h index 2bbf80261..50b89306e 100644 --- a/src/ast/char_decl_plugin.h +++ b/src/ast/char_decl_plugin.h @@ -33,7 +33,8 @@ enum char_sort_kind { enum char_op_kind { OP_CHAR_CONST, OP_CHAR_LE, - OP_CHAR_TO_INT + OP_CHAR_TO_INT, + OP_CHAR_IS_DIGIT }; class char_decl_plugin : public decl_plugin { @@ -79,6 +80,8 @@ public: app* mk_to_int(expr* a) { return m_manager->mk_app(m_family_id, OP_CHAR_TO_INT, 1, &a); } + app* mk_is_digit(expr* a) { return m_manager->mk_app(m_family_id, OP_CHAR_IS_DIGIT, 1, &a); } + bool is_le(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_LE); } bool is_const_char(expr const* e, unsigned& c) const { @@ -87,6 +90,12 @@ public: bool is_to_int(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_TO_INT); } + bool is_is_digit(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_IS_DIGIT); } + + MATCH_UNARY(is_is_digit); + MATCH_UNARY(is_to_int); + MATCH_BINARY(is_le); + bool unicode() const { return m_unicode; } unsigned max_char() const { return m_unicode ? zstring::unicode_max_char() : zstring::ascii_max_char(); } unsigned num_bits() const { return m_unicode ? zstring::unicode_num_bits() : zstring::ascii_num_bits(); } diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 0aac9b529..2be078b9f 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -41,6 +41,30 @@ namespace seq { return result; } + expr_ref axioms::mk_ge_e(expr* x, expr* y) { + expr_ref ge(a.mk_ge(x, y), m); + m_rewrite(ge); + return ge; + } + + expr_ref axioms::mk_le_e(expr* x, expr* y) { + expr_ref le(a.mk_le(x, y), m); + m_rewrite(le); + return le; + } + + expr_ref axioms::mk_seq_eq(expr* a, expr* b) { + SASSERT(seq.is_seq(a) && seq.is_seq(b)); + expr_ref result(m_sk.mk_eq(a, b), m); + m_set_phase(result); + return result; + } + + + expr_ref axioms::mk_eq_empty(expr* e) { + return mk_seq_eq(seq.str.mk_empty(e->get_sort()), e); + } + expr_ref axioms::purify(expr* e) { if (!e) return expr_ref(m); @@ -48,7 +72,12 @@ namespace seq { return expr_ref(e, m); if (m.is_value(e)) return expr_ref(e, m); - expr_ref p(m); + + expr_ref p(e, m); + m_rewrite(p); + if (p == e) + return p; + expr* r = nullptr; if (m_purified.find(e, r)) p = r; @@ -152,6 +181,9 @@ namespace seq { auto s = purify(_s); auto i = purify(_i); auto l = purify(_l); + if (small_segment_axiom(e, _s, _i, _l)) + return; + if (is_tail(s, _i, _l)) { tail_axiom(e, s); return; @@ -237,11 +269,24 @@ namespace seq { return l1 == l2; } + bool axioms::small_segment_axiom(expr* s, expr* e, expr* i, expr* l) { + rational ln; + if (a.is_numeral(i, ln) && ln >= 0 && a.is_numeral(l, ln) && ln <= 5) { + expr_ref_vector es(m); + for (unsigned j = 0; j < ln; ++j) + es.push_back(seq.str.mk_at(e, a.mk_add(i, a.mk_int(j)))); + expr_ref r(seq.str.mk_concat(es, e->get_sort()), m); + add_clause(mk_seq_eq(r, s)); + return true; + } + return false; + } + + bool axioms::is_tail(expr* s, expr* i, expr* l) { rational i1; - if (!a.is_numeral(i, i1) || !i1.is_one()) { + if (!a.is_numeral(i, i1) || !i1.is_one()) return false; - } expr_ref l2(m), l1(l, m); l2 = mk_sub(mk_len(s), a.mk_int(1)); m_rewrite(l1); @@ -617,7 +662,9 @@ namespace seq { // n >= 0 => stoi(itos(n)) = n app_ref stoi(seq.str.mk_stoi(e), m); - add_clause(~ge0, mk_eq(stoi, n)); + expr_ref eq = mk_eq(stoi, n); + add_clause(~ge0, eq); + m_set_phase(eq); // itos(n) does not start with "0" when n > 0 // n = 0 or at(itos(n),0) != "0" @@ -750,17 +797,12 @@ namespace seq { } expr_ref axioms::is_digit(expr* ch) { - expr_ref isd = expr_ref(m_sk.mk_is_digit(ch), m); - expr_ref lo(seq.mk_le(seq.mk_char('0'), ch), m); - expr_ref hi(seq.mk_le(ch, seq.mk_char('9')), m); - add_clause(~lo, ~hi, isd); - add_clause(~isd, lo); - add_clause(~isd, hi); - return isd; + return expr_ref(seq.mk_char_is_digit(ch), m); } expr_ref axioms::mk_digit2int(expr* ch) { - return expr_ref(a.mk_add(seq.mk_char2int(ch), a.mk_int(-((int)'0'))), m);; + m_ensure_digits(); + return expr_ref(m_sk.mk_digit2int(ch), m); } /** diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index e3d7c17a1..f5d1df68a 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -36,6 +36,8 @@ namespace seq { expr_ref_vector m_trail; obj_map m_purified; std::function m_add_clause; + std::function m_set_phase; + std::function m_ensure_digits; expr_ref mk_len(expr* s); expr_ref mk_sub(expr* x, expr* y); @@ -43,17 +45,19 @@ namespace seq { expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(seq.str.mk_concat(e1, e2), m); } expr_ref mk_nth(expr* e, unsigned i) { return expr_ref(seq.str.mk_nth_i(e, a.mk_int(i)), m); } expr_ref mk_eq(expr* a, expr* b) { return expr_ref(m.mk_eq(a, b), m); } - expr_ref mk_seq_eq(expr* a, expr* b) { SASSERT(seq.is_seq(a) && seq.is_seq(b)); return expr_ref(m_sk.mk_eq(a, b), m); } - expr_ref mk_eq_empty(expr* e) { return expr_ref(m.mk_eq(seq.str.mk_empty(e->get_sort()), e), m); } + expr_ref mk_seq_eq(expr* a, expr* b); + expr_ref mk_eq_empty(expr* e); - expr_ref mk_ge(expr* x, unsigned n) { return expr_ref(a.mk_ge(x, a.mk_int(n)), m); } - expr_ref mk_le(expr* x, unsigned n) { return expr_ref(a.mk_le(x, a.mk_int(n)), m); } - expr_ref mk_ge(expr* x, rational const& n) { return expr_ref(a.mk_ge(x, a.mk_int(n)), m); } - expr_ref mk_le(expr* x, rational const& n) { return expr_ref(a.mk_le(x, a.mk_int(n)), m); } + expr_ref mk_ge(expr* x, int n) { return mk_ge_e(x, a.mk_int(n)); } + expr_ref mk_le(expr* x, int n) { return mk_le_e(x, a.mk_int(n)); } + expr_ref mk_ge(expr* x, rational const& n) { return mk_ge_e(x, a.mk_int(n)); } + expr_ref mk_le(expr* x, rational const& n) { return mk_le_e(x, a.mk_int(n)); } + + expr_ref mk_ge_e(expr* x, expr* y); + expr_ref mk_le_e(expr* x, expr* y); void gc_purify(); - expr_ref is_digit(expr* ch); expr_ref purify(expr* e); expr_ref mk_digit2int(expr* ch); @@ -70,6 +74,7 @@ namespace seq { void tail_axiom(expr* e, expr* s); void drop_last_axiom(expr* e, expr* s); + bool small_segment_axiom(expr* e, expr* s, expr* i, expr* l); void extract_prefix_axiom(expr* e, expr* s, expr* l); void extract_suffix_axiom(expr* e, expr* s, expr* l); void tightest_prefix(expr* s, expr* x); @@ -79,6 +84,8 @@ namespace seq { axioms(th_rewriter& rw); void set_add_clause(std::function& ac) { m_add_clause = ac; } + void set_phase(std::function& sp) { m_set_phase = sp; } + void set_ensure_digits(std::function& ed) { m_ensure_digits = ed; } void suffix_axiom(expr* n); void prefix_axiom(expr* n); @@ -102,6 +109,8 @@ namespace seq { void unroll_not_contains(expr* e); expr_ref length_limit(expr* s, unsigned k); + expr_ref is_digit(expr* ch); + }; }; diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 1449a6bbf..07f6d683b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -833,6 +833,11 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { result = m_autil.mk_add(es.size(), es.c_ptr()); return BR_REWRITE2; } + expr* x = nullptr, *y = nullptr, *z = nullptr; + if (str().is_replace(a, x, y, z) && l_true == eq_length(y, z)) { + result = str().mk_length(x); + return BR_REWRITE1; + } #if 0 expr* s = nullptr, *offset = nullptr, *length = nullptr; if (str().is_extract(a, s, offset, length)) { @@ -1147,12 +1152,23 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu return BR_REWRITE3; } + if (str().is_extract(a, a1, b1, c1) && + is_prefix(a, b, c) && is_suffix(a1, b1, c1)) { + expr_ref q(m_autil.mk_sub(c, str().mk_length(a)), m()); + std::cout << "prefix-suffix " << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n"; + std::cout << q << "\n"; + result = str().mk_substr(a1, b1, m_autil.mk_add(c1, q)); + return BR_REWRITE3; + } + + // extract(extract(a, 3, 6), 1, len(extract(a, 3, 6)) - 1) -> extract(a, 4, 5) if (str().is_extract(a, a1, b1, c1) && is_suffix(a, b, c) && m_autil.is_numeral(c1) && m_autil.is_numeral(b1)) { result = str().mk_substr(a1, m_autil.mk_add(b, b1), m_autil.mk_sub(c1, b)); return BR_REWRITE2; } + if (!constantPos) return BR_FAILED; @@ -1365,11 +1381,51 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { result = ::mk_or(ors); return BR_REWRITE_FULL; } - - + + expr_ref ra(a, m()); + if (is_unit(b) && m().is_value(b) && + reduce_by_char(ra, b, 4)) { + result = str().mk_contains(ra, b); + return BR_REWRITE1; + } return BR_FAILED; } +bool seq_rewriter::reduce_by_char(expr_ref& r, expr* ch, unsigned depth) { + expr* x = nullptr, *y = nullptr, *z = nullptr; + if (str().is_replace(r, x, y, z) && + str().is_unit(y) && m().is_value(y) && + str().is_unit(z) && m().is_value(z) && + ch != y && ch != z) { + r = x; + if (depth > 0) + reduce_by_char(r, ch, depth - 1); + return true; + } + if (depth > 0 && str().is_concat(r)) { + bool reduced = false; + expr_ref_vector args(m()); + for (expr* e : *to_app(r)) { + expr_ref tmp(e, m()); + if (reduce_by_char(tmp, ch, depth - 1)) + reduced = true; + args.push_back(tmp); + } + if (reduced) + r = str().mk_concat(args, args.get(0)->get_sort()); + return reduced; + } + if (depth > 0 && str().is_extract(r, x, y, z)) { + expr_ref tmp(x, m()); + if (reduce_by_char(tmp, ch, depth - 1)) { + r = str().mk_substr(tmp, y, z); + return true; + } + } + return false; +} + + /* * (str.at s i), constants s/i, i < 0 or i >= |s| ==> (str.at s i) = "" */ @@ -1632,6 +1688,13 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result m().mk_ite(m_autil.mk_ge(b1, zero()), m_autil.mk_add(one(), b1), minus_one())); return BR_REWRITE3; } + expr_ref ra(a, m()); + if (str().is_unit(b) && m().is_value(b) && + reduce_by_char(ra, b, 4)) { + result = str().mk_index(ra, b, c); + return BR_REWRITE1; + } + // Enhancement: walk segments of a, determine which segments must overlap, must not overlap, may overlap. return BR_FAILED; } @@ -1953,6 +2016,16 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { return BR_REWRITE2; } + unsigned len_a; + rational len_b; + if (max_length(b, len_b)) { + min_length(a, len_a); + if (len_b <= len_a) { + result = m().mk_eq(a, b); + return BR_REWRITE1; + } + } + return BR_FAILED; } @@ -2021,7 +2094,15 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { result = str().mk_suffix(a1, b); return BR_DONE; } - + unsigned len_a; + rational len_b; + if (max_length(b, len_b)) { + min_length(a, len_a); + if (len_b <= len_a) { + result = m().mk_eq(a, b); + return BR_REWRITE1; + } + } return BR_FAILED; } @@ -4590,6 +4671,13 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_pa return true; } +lbool seq_rewriter::eq_length(expr* x, expr* y) { + unsigned xl = 0, yl = 0; + if (min_length(x, xl) && min_length(y, yl)) + return xl == yl ? l_true : l_false; + return l_undef; +} + /*** \brief extract the minimal length of the sequence. Return true if the minimal length is equal to the diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c45177552..296485d73 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -289,7 +289,9 @@ class seq_rewriter { bool min_length(expr_ref_vector const& es, unsigned& len); bool min_length(expr* e, unsigned& len); bool max_length(expr* e, rational& len); + lbool eq_length(expr* x, expr* y); expr* concat_non_empty(expr_ref_vector& es); + bool reduce_by_char(expr_ref& r, expr* ch, unsigned depth); bool is_string(unsigned n, expr* const* es, zstring& s) const; diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index bf04d4a48..f7b1b46e4 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -133,6 +133,8 @@ namespace seq { a.is_unsigned(i, idx); } bool is_align(expr const* e) const { return is_skolem(symbol("seq.align.m"), e); } + bool is_align_l(expr const* e) const { return is_skolem(symbol("seq.align.l"), e); } + bool is_align_r(expr const* e) const { return is_skolem(symbol("seq.align.r"), e); } MATCH_BINARY(is_align); bool is_post(expr* e, expr*& s, expr*& start); bool is_pre(expr* e, expr*& s, expr*& i); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index be5a64adc..02015f90b 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -234,9 +234,12 @@ public: bool is_const_char(expr* e, unsigned& c) const; bool is_const_char(expr* e) const { unsigned c; return is_const_char(e, c); } bool is_char_le(expr const* e) const; + bool is_char_is_digit(expr const* e, expr*& d) const { return ch.is_is_digit(e, d); } + bool is_char_is_digit(expr const* e) const { return ch.is_is_digit(e); } bool is_char2int(expr const* e) const; app* mk_char_bit(expr* e, unsigned i); app* mk_char(unsigned ch) const; + app* mk_char_is_digit(expr* e) { return ch.mk_is_digit(e); } app* mk_le(expr* ch1, expr* ch2) const; app* mk_lt(expr* ch1, expr* ch2) const; app* mk_char2int(expr* e) { return ch.mk_to_int(e); } diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index 6d02fcf21..fee223612 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -37,7 +37,11 @@ seq_axioms::seq_axioms(theory& th, th_rewriter& r): m_digits_initialized(false) { std::function _add_clause = [&](expr_ref_vector const& c) { add_clause(c); }; + std::function _set_phase = [&](expr* e) { set_phase(e); }; + std::function _ensure_digits = [&]() { ensure_digit_axiom(); }; m_ax.set_add_clause(_add_clause); + m_ax.set_phase(_set_phase); + m_ax.set_ensure_digits(_ensure_digits); } literal seq_axioms::mk_eq(expr* a, expr* b) { @@ -68,6 +72,12 @@ literal seq_axioms::mk_literal(expr* _e) { return ctx().get_literal(e); } +void seq_axioms::set_phase(expr* e) { + literal lit = mk_literal(e); + ctx().force_phase(lit); +} + + void seq_axioms::add_clause(expr_ref_vector const& clause) { expr* a = nullptr, *b = nullptr; if (false && clause.size() == 1 && m.is_eq(clause[0], a, b)) { @@ -83,480 +93,17 @@ void seq_axioms::add_clause(expr_ref_vector const& clause) { literal lits[5] = { null_literal, null_literal, null_literal, null_literal, null_literal }; unsigned idx = 0; for (expr* e : clause) { - lits[idx++] = mk_literal(e); + literal lit = mk_literal(e); + if (lit == true_literal) + return; + if (lit != false_literal) + lits[idx++] = mk_literal(e); SASSERT(idx <= 5); } add_axiom(lits[0], lits[1], lits[2], lits[3], lits[4]); } - - -/* - encode that s is not contained in of xs1 - where s1 is all of s, except the last element. - - s = "" or s = s1*(unit c) - s = "" or !contains(x*s1, s) -*/ -void seq_axioms::tightest_prefix(expr* s, expr* x) { - literal s_eq_emp = mk_eq_empty(s); - if (seq.str.max_length(s) <= 1) { - add_axiom(s_eq_emp, ~mk_literal(seq.str.mk_contains(x, s))); - return; - } - expr_ref s1 = m_sk.mk_first(s); - expr_ref c = m_sk.mk_last(s); - expr_ref s1c = mk_concat(s1, seq.str.mk_unit(c)); - add_axiom(s_eq_emp, mk_seq_eq(s, s1c)); - add_axiom(s_eq_emp, ~mk_literal(seq.str.mk_contains(mk_concat(x, s1), s))); -} - -/* - [[str.indexof]](w, w2, i) is the smallest n such that for some some w1, w3 - - w = w1w2w3 - - i <= n = |w1| - - if [[str.contains]](w, w2) = true, |w2| > 0 and i >= 0. - - [[str.indexof]](w,w2,i) = -1 otherwise. - - - let i = Index(t, s, offset): - // index of s in t starting at offset. - - - |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1 - |t| = 0 & |s| = 0 => indexof(t,s,offset) = 0 - - offset >= len(t) => |s| = 0 or i = -1 - - len(t) != 0 & !contains(t, s) => i = -1 - - - offset = 0 & len(t) != 0 & contains(t, s) => t = xsy & i = len(x) - tightest_prefix(x, s) - - - 0 <= offset < len(t) => xy = t & - len(x) = offset & - (-1 = indexof(y, s, 0) => -1 = i) & - (indexof(y, s, 0) >= 0 => indexof(t, s, 0) + offset = i) - - offset < 0 => i = -1 - - optional lemmas: - (len(s) > len(t) -> i = -1) - (len(s) <= len(t) -> i <= len(t)-len(s)) -*/ -void seq_axioms::add_indexof_axiom(expr* i) { - expr* _s = nullptr, *_t = nullptr, *_offset = nullptr; - rational r; - VERIFY(seq.str.is_index(i, _t, _s) || - seq.str.is_index(i, _t, _s, _offset)); - expr_ref minus_one(a.mk_int(-1), m); - expr_ref zero(a.mk_int(0), m); - expr_ref xsy(m), t(_t, m), s(_s, m), offset(_offset, m); - m_rewrite(t); - m_rewrite(s); - if (offset) m_rewrite(offset); - literal cnt = mk_literal(seq.str.mk_contains(t, s)); - literal i_eq_m1 = mk_eq(i, minus_one); - literal i_eq_0 = mk_eq(i, zero); - literal s_eq_empty = mk_eq_empty(s); - literal t_eq_empty = mk_eq_empty(t); - - // |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1 - // ~contains(t,s) <=> indexof(t,s,offset) = -1 - - add_axiom(cnt, i_eq_m1); - add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1); - - if (!offset || (a.is_numeral(offset, r) && r.is_zero())) { - // |s| = 0 => indexof(t,s,0) = 0 - add_axiom(~s_eq_empty, i_eq_0); -#if 1 - expr_ref x = m_sk.mk_indexof_left(t, s); - expr_ref y = m_sk.mk_indexof_right(t, s); - xsy = mk_concat(x, s, y); - expr_ref lenx = mk_len(x); - // contains(t,s) & |s| != 0 => t = xsy & indexof(t,s,0) = |x| - add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy)); - add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx)); - add_axiom(~cnt, mk_ge(i, 0)); - tightest_prefix(s, x); -#else - // let i := indexof(t,s,0) - // contains(t, s) & |s| != 0 => ~contains(substr(t,0,i+len(s)-1), s) - // => substr(t,0,i+len(s)) = substr(t,0,i) ++ s - // - expr_ref len_s = mk_len(s); - expr_ref mone(a.mk_int(-1), m); - add_axiom(~cnt, s_eq_empty, ~mk_literal(seq.str.mk_contains(seq.str.mk_substr(t,zero,a.mk_add(i,len_s,mone)),s))); - add_axiom(~cnt, s_eq_empty, mk_seq_eq(seq.str.mk_substr(t,zero,a.mk_add(i,len_s)), - seq.str.mk_concat(seq.str.mk_substr(t,zero,i), s))); -#endif - } - else { - // offset >= len(t) => |s| = 0 or indexof(t, s, offset) = -1 - // offset > len(t) => indexof(t, s, offset) = -1 - // offset = len(t) & |s| = 0 => indexof(t, s, offset) = offset - expr_ref len_t = mk_len(t); - literal offset_ge_len = mk_ge(mk_sub(offset, len_t), 0); - literal offset_le_len = mk_le(mk_sub(offset, len_t), 0); - literal i_eq_offset = mk_eq(i, offset); - add_axiom(~offset_ge_len, s_eq_empty, i_eq_m1); - add_axiom(offset_le_len, i_eq_m1); - add_axiom(~offset_ge_len, ~offset_le_len, ~s_eq_empty, i_eq_offset); - - expr_ref x = m_sk.mk_indexof_left(t, s, offset); - expr_ref y = m_sk.mk_indexof_right(t, s, offset); - expr_ref indexof0(seq.str.mk_index(y, s, zero), m); - expr_ref offset_p_indexof0(a.mk_add(offset, indexof0), m); - literal offset_ge_0 = mk_ge(offset, 0); - - // 0 <= offset & offset < len(t) => t = xy - // 0 <= offset & offset < len(t) => len(x) = offset - // 0 <= offset & offset < len(t) & indexof(y,s,0) = -1 => -1 = i - // 0 <= offset & offset < len(t) & indexof(y,s,0) >= 0 => - // -1 = indexof(y,s,0) + offset = indexof(t, s, offset) - - add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y))); - add_axiom(~offset_ge_0, offset_ge_len, mk_eq(mk_len(x), offset)); - add_axiom(~offset_ge_0, offset_ge_len, - ~mk_eq(indexof0, minus_one), i_eq_m1); - add_axiom(~offset_ge_0, offset_ge_len, - ~mk_ge(indexof0, 0), - mk_eq(offset_p_indexof0, i)); - - // offset < 0 => -1 = i - add_axiom(offset_ge_0, i_eq_m1); - } -} - -/** - - !contains(t, s) => i = -1 - |t| = 0 => |s| = 0 or i = -1 - |t| = 0 & |s| = 0 => i = 0 - |t| != 0 & contains(t, s) => t = xsy & i = len(x) - |s| = 0 or s = s_head*s_tail - |s| = 0 or !contains(s_tail*y, s) - - */ -void seq_axioms::add_last_indexof_axiom(expr* i) { - expr* _s = nullptr, *_t = nullptr; - VERIFY(seq.str.is_last_index(i, _t, _s)); - expr_ref s(_s, m), t(_t, m); - m_rewrite(s); - m_rewrite(t); - expr_ref minus_one(a.mk_int(-1), m); - expr_ref zero(a.mk_int(0), m); - expr_ref s_head(m), s_tail(m); - expr_ref x = m_sk.mk_last_indexof_left(t, s); - expr_ref y = m_sk.mk_last_indexof_right(t, s); - m_sk.decompose(s, s_head, s_tail); - literal cnt = mk_literal(seq.str.mk_contains(t, s)); - literal cnt2 = mk_literal(seq.str.mk_contains(mk_concat(s_tail, y), s)); - literal i_eq_m1 = mk_eq(i, minus_one); - literal i_eq_0 = mk_eq(i, zero); - literal s_eq_empty = mk_eq_empty(s); - literal t_eq_empty = mk_eq_empty(t); - expr_ref xsy = mk_concat(x, s, y); - - add_axiom(cnt, i_eq_m1); - add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1); - add_axiom(~t_eq_empty, ~s_eq_empty, i_eq_0); - add_axiom(t_eq_empty, ~cnt, mk_seq_eq(t, xsy)); - add_axiom(t_eq_empty, ~cnt, mk_eq(i, mk_len(x))); - add_axiom(s_eq_empty, mk_eq(s, mk_concat(s_head, s_tail))); - add_axiom(s_eq_empty, ~cnt2); -} - -/* - let r = replace(u, s, t) - - - - if s is empty, the result is to prepend t to u; - - if s does not occur in u then the result is u. - - s = "" => r = t+u - u = "" => s = "" or r = u - ~contains(u,s) => r = u - - tightest_prefix(s, x) - contains(u, s) => r = xty & u = xsy - ~contains(u, s) => r = u - -*/ -void seq_axioms::add_replace_axiom(expr* r) { - expr* _u = nullptr, *_s = nullptr, *_t = nullptr; - VERIFY(seq.str.is_replace(r, _u, _s, _t)); - expr_ref u(_u, m), s(_s, m), t(_t, m); - m_rewrite(u); - m_rewrite(s); - m_rewrite(t); - expr_ref x = m_sk.mk_indexof_left(u, s); - expr_ref y = m_sk.mk_indexof_right(u, s); - expr_ref xty = mk_concat(x, t, y); - expr_ref xsy = mk_concat(x, s, y); - literal u_emp = mk_eq_empty(u, true); - literal s_emp = mk_eq_empty(s, true); - literal cnt = mk_literal(seq.str.mk_contains(u, s)); - add_axiom(~s_emp, mk_seq_eq(r, mk_concat(t, u))); - add_axiom(~u_emp, s_emp, mk_seq_eq(r, u)); - add_axiom(cnt, mk_seq_eq(r, u)); - add_axiom(~cnt, u_emp, s_emp, mk_seq_eq(u, xsy)); - add_axiom(~cnt, u_emp, s_emp, mk_seq_eq(r, xty)); - ctx().force_phase(cnt); - tightest_prefix(s, x); -} - - -/* - let e = at(s, i) - - 0 <= i < len(s) -> s = xey & len(x) = i & len(e) = 1 - i < 0 \/ i >= len(s) -> e = empty - -*/ -void seq_axioms::add_at_axiom(expr* e) { - TRACE("seq", tout << "at-axiom: " << ctx().get_scope_level() << " " << mk_bounded_pp(e, m) << "\n";); - expr* _s = nullptr, *_i = nullptr; - VERIFY(seq.str.is_at(e, _s, _i)); - expr_ref s(_s, m), i(_i, m); - m_rewrite(s); - m_rewrite(i); - expr_ref zero(a.mk_int(0), m); - expr_ref one(a.mk_int(1), m); - expr_ref emp(seq.str.mk_empty(e->get_sort()), m); - expr_ref len_s = mk_len(s); - literal i_ge_0 = mk_ge(i, 0); - literal i_ge_len_s = mk_ge(mk_sub(i, mk_len(s)), 0); - expr_ref len_e = mk_len(e); - - rational iv; - if (a.is_numeral(i, iv) && iv.is_unsigned()) { - expr_ref_vector es(m); - expr_ref nth(m); - unsigned k = iv.get_unsigned(); - for (unsigned j = 0; j <= k; ++j) { - es.push_back(seq.str.mk_unit(mk_nth(s, j))); - } - nth = es.back(); - es.push_back(m_sk.mk_tail(s, i)); - add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, seq.str.mk_concat(es, e->get_sort()))); - add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(nth, e)); - } - else { - expr_ref x = m_sk.mk_pre(s, i); - expr_ref y = m_sk.mk_tail(s, i); - expr_ref xey = mk_concat(x, e, y); - expr_ref len_x = mk_len(x); - add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey)); - add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x)); - } - - add_axiom(i_ge_0, mk_eq(e, emp)); - add_axiom(~i_ge_len_s, mk_eq(e, emp)); - add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e)); - add_axiom(mk_le(len_e, 1)); -} - -/** - i >= 0 i < len(s) => unit(nth_i(s, i)) = at(s, i) - nth_i(unit(nth_i(s, i)), 0) = nth_i(s, i) -*/ - -void seq_axioms::add_nth_axiom(expr* e) { - expr* s = nullptr, *i = nullptr; - rational n; - zstring str; - VERIFY(seq.str.is_nth_i(e, s, i)); - if (seq.str.is_string(s, str) && a.is_numeral(i, n) && - n.is_unsigned() && n.get_unsigned() < str.length()) { - app_ref ch(seq.str.mk_char(str[n.get_unsigned()]), m); - add_axiom(mk_eq(ch, e)); - } - else { - expr_ref zero(a.mk_int(0), m); - literal i_ge_0 = mk_ge(i, 0); - literal i_ge_len_s = mk_ge(mk_sub(i, mk_len(s)), 0); - // at(s,i) = [nth(s,i)] - expr_ref rhs(s, m); - expr_ref lhs(seq.str.mk_unit(e), m); - if (!seq.str.is_at(s) || zero != i) rhs = seq.str.mk_at(s, i); - m_rewrite(rhs); - add_axiom(~i_ge_0, i_ge_len_s, mk_eq(lhs, rhs)); - } -} - - -void seq_axioms::add_itos_axiom(expr* e) { - expr* _n = nullptr; - TRACE("seq", tout << mk_pp(e, m) << "\n";); - VERIFY(seq.str.is_itos(e, _n)); - expr_ref n(_n, m); - m_rewrite(n); - - // itos(n) = "" <=> n < 0 - expr_ref zero(a.mk_int(0), m); - literal eq1 = mk_literal(seq.str.mk_is_empty(e)); - literal ge0 = mk_ge(n, 0); - // n >= 0 => itos(n) != "" - // itos(n) = "" or n >= 0 - add_axiom(~eq1, ~ge0); - add_axiom(eq1, ge0); - add_axiom(mk_ge(mk_len(e), 0)); - - // n >= 0 => stoi(itos(n)) = n - app_ref stoi(seq.str.mk_stoi(e), m); - add_axiom(~ge0, th.mk_preferred_eq(stoi, n)); - - // itos(n) does not start with "0" when n > 0 - // n = 0 or at(itos(n),0) != "0" - // alternative: n >= 0 => itos(stoi(itos(n))) = itos(n) - expr_ref zs(seq.str.mk_string(symbol("0")), m); - m_rewrite(zs); - literal eq0 = mk_eq(n, zero); - literal at0 = mk_eq(seq.str.mk_at(e, zero), zs); - add_axiom(eq0, ~at0); - add_axiom(~eq0, mk_eq(e, zs)); -} - -/** - stoi(s) >= -1 - stoi("") = -1 - stoi(s) >= 0 => is_digit(nth(s,0)) -*/ -void seq_axioms::add_stoi_axiom(expr* e) { - TRACE("seq", tout << mk_pp(e, m) << "\n";); - literal ge0 = mk_ge(e, 0); - expr* s = nullptr; - VERIFY (seq.str.is_stoi(e, s)); - add_axiom(mk_ge(e, -1)); // stoi(s) >= -1 - add_axiom(~mk_eq_empty(s), mk_eq(e, a.mk_int(-1))); // s = "" => stoi(s) = -1 - add_axiom(~ge0, is_digit(mk_nth(s, 0))); // stoi(s) >= 0 => is_digit(nth(s,0)) - -} - -/** - - len(s) <= k => stoi(s) = stoi(s, k) - len(s) > 0, is_digit(nth(s,0)) => stoi(s, 0) = digit(nth_i(s, 0)) - len(s) > 0, ~is_digit(nth(s,0)) => stoi(s, 0) = -1 - - 0 < i, len(s) <= i => stoi(s, i) = stoi(s, i - 1) - 0 < i, len(s) > i, stoi(s, i - 1) >= 0, is_digit(nth(s, i - 1)) => stoi(s, i) = 10*stoi(s, i - 1) + digit(nth_i(s, i - 1)) - 0 < i, len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1 - 0 < i, len(s) > i, ~is_digit(nth(s, i - 1)) => stoi(s, i) = -1 - - - -Define auxiliary function with the property: - for 0 <= i < k - stoi(s, i) := stoi(extract(s, 0, i+1)) - - for 0 < i < k: - len(s) > i => stoi(s, i) := stoi(extract(s, 0, i))*10 + stoi(extract(s, i, 1)) - len(s) <= i => stoi(s, i) := stoi(extract(s, 0, i-1), i-1) - - for i <= i < k: - stoi(s) > = 0, len(s) > i => is_digit(nth(s, i)) - - */ -void seq_axioms::add_stoi_axiom(expr* e, unsigned k) { - SASSERT(k > 0); - expr* _s = nullptr; - VERIFY (seq.str.is_stoi(e, _s)); - expr_ref s(_s, m); - m_rewrite(s); - auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); }; - auto digit = [&](unsigned j) { return m_sk.mk_digit2int(mk_nth(s, j)); }; - auto is_digit_ = [&](unsigned j) { return is_digit(mk_nth(s, j)); }; - expr_ref len = mk_len(s); - literal ge0 = mk_ge(e, 0); - literal lek = mk_le(len, k); - add_axiom(~lek, mk_eq(e, stoi2(k-1))); // len(s) <= k => stoi(s) = stoi(s, k-1) - add_axiom(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0))); // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0) - add_axiom(mk_le(len, 0), is_digit_(0), mk_eq(stoi2(0), a.mk_int(-1))); // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1 - for (unsigned i = 1; i < k; ++i) { - - // len(s) <= i => stoi(s, i) = stoi(s, i - 1) - - add_axiom(~mk_le(len, i), mk_eq(stoi2(i), stoi2(i-1))); - - // len(s) > i, stoi(s, i - 1) >= 0, is_digit(nth(s, i)) => stoi(s, i) = 10*stoi(s, i - 1) + digit(i) - // len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1 - // len(s) > i, ~is_digit(nth(s, i)) => stoi(s, i) = -1 - - add_axiom(mk_le(len, i), ~mk_ge(stoi2(i-1), 0), ~is_digit_(i), mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i)))); - add_axiom(mk_le(len, i), is_digit_(i), mk_eq(stoi2(i), a.mk_int(-1))); - add_axiom(mk_le(len, i), mk_ge(stoi2(i-1), 0), mk_eq(stoi2(i), a.mk_int(-1))); - - // stoi(s) >= 0, i < len(s) => is_digit(nth(s, i)) - - add_axiom(~ge0, mk_le(len, i), is_digit_(i)); - } -} - -/** - Let s := itos(e) - - Relate values of e with len(s) where len(s) is bounded by k. - - |s| = 0 => e < 0 - - |s| <= 1 => e < 10 - |s| <= 2 => e < 100 - |s| <= 3 => e < 1000 - - |s| >= 1 => e >= 0 - |s| >= 2 => e >= 10 - |s| >= 3 => e >= 100 - - There are no constraints to ensure that the string itos(e) - contains the valid digits corresponding to e >= 0. - The validity of itos(e) is ensured by the following property: - e is either of the form stoi(s) for some s, or there is a term - stoi(itos(e)) and axiom e >= 0 => stoi(itos(e)) = e. - Then the axioms for stoi(itos(e)) ensure that the characters of - itos(e) are valid digits and the axiom stoi(itos(e)) = e ensures - these digits encode e. - The option of constraining itos(e) digits directly does not - seem appealing becaues it requires an order of quadratic number - of constraints for all possible lengths of itos(e) (e.g, log_10(e)). - -*/ - -void seq_axioms::add_itos_axiom(expr* s, unsigned k) { - expr* e = nullptr; - VERIFY(seq.str.is_itos(s, e)); - expr_ref len = mk_len(s); - add_axiom(mk_ge(e, 10), mk_le(len, 1)); - add_axiom(mk_le(e, -1), mk_ge(len, 1)); - rational lo(1); - for (unsigned i = 1; i <= k; ++i) { - lo *= rational(10); - add_axiom(mk_ge(e, lo), mk_le(len, i)); - add_axiom(mk_le(e, lo - 1), mk_ge(len, i + 1)); - } -} - -literal seq_axioms::is_digit(expr* ch) { - ensure_digit_axiom(); - literal isd = mk_literal(m_sk.mk_is_digit(ch)); - expr_ref d2i = m_sk.mk_digit2int(ch); - expr_ref _lo(seq.mk_le(seq.mk_char('0'), ch), m); - expr_ref _hi(seq.mk_le(ch, seq.mk_char('9')), m); - literal lo = mk_literal(_lo); - literal hi = mk_literal(_hi); - add_axiom(~lo, ~hi, isd); - add_axiom(~isd, lo); - add_axiom(~isd, hi); - return isd; -} - /** Bridge character digits to integers. */ @@ -573,28 +120,3 @@ void seq_axioms::ensure_digit_axiom() { } -/** - is_digit(e) <=> to_code('0') <= to_code(e) <= to_code('9') - */ -void seq_axioms::add_is_digit_axiom(expr* n) { - expr* e = nullptr; - VERIFY(seq.str.is_is_digit(n, e)); - literal is_digit = mk_literal(n); - expr_ref to_code(seq.str.mk_to_code(e), m); - literal ge0 = mk_ge(to_code, (unsigned)'0'); - literal le9 = mk_le(to_code, (unsigned)'9'); - add_axiom(~is_digit, ge0); - add_axiom(~is_digit, le9); - add_axiom(is_digit, ~ge0, ~le9); -} - - -expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) { - expr_ref bound_tracker = m_sk.mk_length_limit(s, k); - expr* s0 = nullptr; - if (seq.str.is_stoi(s, s0)) - s = s0; - literal bound_predicate = mk_le(mk_len(s), k); - add_axiom(~mk_literal(bound_tracker), bound_predicate); - return bound_tracker; -} diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index 1827e54db..0a53dcd85 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -55,9 +55,11 @@ namespace smt { void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal) { add_axiom5(l1, l2, l3, l4, l5); } - void tightest_prefix(expr* s, expr* x); void ensure_digit_axiom(); void add_clause(expr_ref_vector const& lits); + void set_phase(expr* e); + + public: seq_axioms(theory& th, th_rewriter& r); @@ -69,31 +71,32 @@ namespace smt { void add_suffix_axiom(expr* n) { m_ax.suffix_axiom(n); } void add_prefix_axiom(expr* n) { m_ax.prefix_axiom(n); } void add_extract_axiom(expr* n) { m_ax.extract_axiom(n); } - void add_indexof_axiom(expr* n); - void add_last_indexof_axiom(expr* n); - void add_replace_axiom(expr* n); - void add_at_axiom(expr* n); - void add_nth_axiom(expr* n); - void add_itos_axiom(expr* n); - void add_stoi_axiom(expr* n); - void add_stoi_axiom(expr* e, unsigned k); - void add_itos_axiom(expr* s, unsigned k); + void add_indexof_axiom(expr* n) { m_ax.indexof_axiom(n); } + void add_last_indexof_axiom(expr* n) { m_ax.last_indexof_axiom(n); } + void add_replace_axiom(expr* n) { m_ax.replace_axiom(n); } + void add_at_axiom(expr* n) { m_ax.at_axiom(n); } + void add_nth_axiom(expr* n) { m_ax.nth_axiom(n); } + void add_itos_axiom(expr* n) { m_ax.itos_axiom(n); } + void add_stoi_axiom(expr* n) { m_ax.stoi_axiom(n); } + void add_stoi_axiom(expr* e, unsigned k) { m_ax.stoi_axiom(e, k); } + void add_itos_axiom(expr* s, unsigned k) { m_ax.itos_axiom(s, k); } void add_lt_axiom(expr* n) { m_ax.lt_axiom(n); } void add_le_axiom(expr* n) { m_ax.le_axiom(n); } - void add_is_digit_axiom(expr* n); + void add_is_digit_axiom(expr* n) { m_ax.is_digit_axiom(n); } void add_str_to_code_axiom(expr* n) { m_ax.str_to_code_axiom(n); } void add_str_from_code_axiom(expr* n) { m_ax.str_from_code_axiom(n); } void add_unit_axiom(expr* n) { m_ax.unit_axiom(n); } void add_length_axiom(expr* n) { m_ax.length_axiom(n); } void unroll_not_contains(expr* n) { m_ax.unroll_not_contains(n); } - literal is_digit(expr* ch); + literal is_digit(expr* ch) { return mk_literal(m_ax.is_digit(ch)); } + expr_ref add_length_limit(expr* s, unsigned k) { return m_ax.length_limit(s, k); } + literal mk_ge(expr* e, int k) { return mk_ge_e(e, a.mk_int(k)); } literal mk_le(expr* e, int k) { return mk_le_e(e, a.mk_int(k)); } literal mk_ge(expr* e, rational const& k) { return mk_ge_e(e, a.mk_int(k)); } literal mk_le(expr* e, rational const& k) { return mk_le_e(e, a.mk_int(k)); } - expr_ref add_length_limit(expr* s, unsigned k); }; }; diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index 23bbc7350..5b931c193 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -466,20 +466,28 @@ bool theory_seq::branch_variable() { TRACE("seq", tout << "branch_quat_variable\n";); return true; } - if (branch_variable_mb()) { - TRACE("seq", tout << "branch_variable_mb\n";); - return true; - } - if (branch_variable_eq()) { - TRACE("seq", tout << "branch_variable_eq\n";); - return true; + + unsigned turn = ctx.get_random_value() % 2 == 0; + for (unsigned i = 0; i < 2; ++i, turn = !turn) { + if (turn && branch_variable_mb()) { + TRACE("seq", tout << "branch_variable_mb\n";); + return true; + } + if (!turn && branch_variable_eq()) { + TRACE("seq", tout << "branch_variable_eq\n";); + return true; + } } return false; } bool theory_seq::branch_variable_mb() { bool change = false; - for (auto const& e : m_eqs) { + unsigned sz = m_eqs.size(); + int start = ctx.get_random_value(); + for (unsigned i = 0; i < sz; ++i) { + unsigned k = (i + start) % sz; + eq const& e = m_eqs[k]; vector len1, len2; if (!is_complex(e)) { continue; @@ -860,17 +868,16 @@ bool theory_seq::branch_ternary_variable_rhs(eq const& e) { !is_ternary_eq_rhs(e.rs(), e.ls(), x, xs, y1, ys, y2)) { return false; } + if (m_sk.is_align_l(y1) || m_sk.is_align_r(y1)) + return false; rational lenX, lenY1, lenY2; - if (!get_length(x, lenX)) { + if (!get_length(x, lenX)) add_length_to_eqc(x); - } - if (!get_length(y1, lenY1)) { + if (!get_length(y1, lenY1)) add_length_to_eqc(y1); - } - if (!get_length(y2, lenY2)) { + if (!get_length(y2, lenY2)) add_length_to_eqc(y2); - } SASSERT(!xs.empty() && !ys.empty()); if (!can_align_from_lhs(xs, ys)) { @@ -882,11 +889,16 @@ bool theory_seq::branch_ternary_variable_rhs(eq const& e) { expr_ref y1ysZ = mk_concat(y1ys, Z); dependency* dep = e.dep(); - propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y2), xs.size())); - propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y1)), ys.size())); - propagate_eq(dep, x, y1ysZ, true); - propagate_eq(dep, y2, ZxsE, true); - return true; + bool propagated = false; + if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y2), xs.size()))) + propagated = true; + if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y1)), ys.size()))) + propagated = true; + if (propagate_eq(dep, x, y1ysZ, true)) + propagated = true; + if (propagate_eq(dep, y2, ZxsE, true)) + propagated = true; + return propagated; } return false; } @@ -900,17 +912,16 @@ bool theory_seq::branch_ternary_variable_lhs(eq const& e) { if (!is_ternary_eq_lhs(e.ls(), e.rs(), xs, x, y1, ys, y2) && !is_ternary_eq_lhs(e.rs(), e.ls(), xs, x, y1, ys, y2)) return false; + if (m_sk.is_align_l(y1) || m_sk.is_align_r(y1)) + return false; rational lenX, lenY1, lenY2; - if (!get_length(x, lenX)) { + if (!get_length(x, lenX)) add_length_to_eqc(x); - } - if (!get_length(y1, lenY1)) { + if (!get_length(y1, lenY1)) add_length_to_eqc(y1); - } - if (!get_length(y2, lenY2)) { + if (!get_length(y2, lenY2)) add_length_to_eqc(y2); - } SASSERT(!xs.empty() && !ys.empty()); if (!can_align_from_rhs(xs, ys)) { @@ -922,10 +933,15 @@ bool theory_seq::branch_ternary_variable_lhs(eq const& e) { expr_ref Zysy2 = mk_concat(Z, ysy2); dependency* dep = e.dep(); - propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y1), xs.size())); - propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y2)), ys.size())); - propagate_eq(dep, x, Zysy2, true); - propagate_eq(dep, y1, xsZ, true); + bool propagated = false; + if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y1), xs.size()))) + propagated = true; + if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y2)), ys.size()))) + propagated = true; + if (propagate_eq(dep, x, Zysy2, true)) + propagated = true; + if (propagate_eq(dep, y1, xsZ, true)) + propagated = true; return true; } return false; diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index f1fb4f05d..83ec9b30d 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -66,6 +66,8 @@ namespace smt { ctx.mark_as_relevant(bv); if (seq.is_char_le(term)) internalize_le(literal(bv, false), term); + if (seq.is_char_is_digit(term)) + internalize_is_digit(literal(bv, false), term); return true; } @@ -153,6 +155,30 @@ namespace smt { ctx.mk_th_axiom(get_id(), lit, ~le); } + void theory_char::internalize_is_digit(literal lit, app* term) { + expr* x = nullptr; + VERIFY(seq.is_char_is_digit(term, x)); + enode* zero = ensure_enode(seq.mk_char('0')); + enode* nine = ensure_enode(seq.mk_char('9')); + theory_var v = ctx.get_enode(x)->get_th_var(get_id()); + theory_var z = zero->get_th_var(get_id()); + theory_var n = nine->get_th_var(get_id()); + init_bits(v); + init_bits(z); + init_bits(n); + auto const& bv = get_ebits(v); + auto const& zv = get_ebits(z); + auto const& nv = get_ebits(n); + expr_ref le1(m), le2(m); + m_bb.mk_ule(bv.size(), zv.c_ptr(), bv.c_ptr(), le1); + m_bb.mk_ule(bv.size(), bv.c_ptr(), nv.c_ptr(), le2); + literal lit1 = mk_literal(le1); + literal lit2 = mk_literal(le2); + ctx.mk_th_axiom(get_id(), ~lit, lit1); + ctx.mk_th_axiom(get_id(), ~lit, lit2); + ctx.mk_th_axiom(get_id(), ~lit1, ~lit2, lit); + } + literal_vector const& theory_char::get_bits(theory_var v) { init_bits(v); return m_bits[v]; diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h index cd37732b8..511bcbd10 100644 --- a/src/smt/theory_char.h +++ b/src/smt/theory_char.h @@ -59,6 +59,7 @@ namespace smt { void new_char2int(theory_var v, expr* c); unsigned get_char_value(theory_var v); void internalize_le(literal lit, app* term); + void internalize_is_digit(literal lit, app* term); theory_var mk_var(enode* n) override; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 343411fd0..65d3be15b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -724,14 +724,17 @@ void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect -void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits, literal lit) { - if (lit == true_literal) return; - +bool theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits, literal lit) { + if (lit == true_literal) + return false; + if (ctx.get_assignment(lit) == l_true) + return false; + literal_vector lits(n, _lits); if (lit == false_literal) { set_conflict(dep, lits); - return; + return true; } ctx.mark_as_relevant(lit); enode_pair_vector eqs; @@ -750,6 +753,7 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits m_new_propagation = true; ctx.assign(lit, js); validate_assign(lit, eqs, lits); + return true; } void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 922ed59c0..1e54734ea 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -514,8 +514,8 @@ namespace smt { // asserting consequences void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; - void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, nullptr, lit); } - void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit); + bool propagate_lit(dependency* dep, literal lit) { return propagate_lit(dep, 0, nullptr, lit); } + bool propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit); bool propagate_eq(dependency* dep, enode* n1, enode* n2); bool propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs); bool propagate_eq(dependency* dep, literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs = true); diff --git a/src/solver/check_logic.cpp b/src/solver/check_logic.cpp index 3c8ddf4bf..231c21a80 100644 --- a/src/solver/check_logic.cpp +++ b/src/solver/check_logic.cpp @@ -191,7 +191,7 @@ struct check_logic::imp { m_ints = true; m_arrays = true; m_reals = true; - // m_quantifiers = false; // some QF_SLIA benchmarks are miss-classified + m_quantifiers = true; // some QF_SLIA benchmarks are miss-classified } else if (logic == "QF_FD") { m_bvs = true;