From c5a9d81d93b9b8e5c44ee0605a66ae77a7cfc17b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 20:17:00 -0800 Subject: [PATCH] seq Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.h | 3 + src/ast/rewriter/seq_rewriter.cpp | 39 ++++--- src/ast/rewriter/seq_rewriter.h | 12 +- src/ast/seq_decl_plugin.cpp | 21 +++- src/ast/seq_decl_plugin.h | 19 ++-- src/smt/theory_seq.cpp | 183 +++++++++++++++++++++++++++--- src/smt/theory_seq.h | 13 ++- 7 files changed, 239 insertions(+), 51 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index e185b241b..252bd8ed6 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -328,6 +328,9 @@ public: app * mk_numeral(sexpr const * p, unsigned i) { return plugin().mk_numeral(p, i); } + app * mk_int(int i) { + return mk_numeral(rational(i), true); + } app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LE, arg1, arg2); } app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); } app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index f810b48cd..96e11283e 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -55,22 +55,28 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con return mk_seq_concat(args[0], args[1], result); case OP_SEQ_LENGTH: SASSERT(num_args == 1); - return mk_str_length(args[0], result); + return mk_seq_length(args[0], result); case OP_SEQ_EXTRACT: SASSERT(num_args == 3); - return mk_str_substr(args[0], args[1], args[2], result); + return mk_seq_extract(args[0], args[1], args[2], result); case OP_SEQ_CONTAINS: SASSERT(num_args == 2); - return mk_str_strctn(args[0], args[1], result); + return mk_seq_contains(args[0], args[1], result); case OP_SEQ_AT: SASSERT(num_args == 2); - return mk_str_at(args[0], args[1], result); + return mk_seq_at(args[0], args[1], result); case OP_SEQ_PREFIX: SASSERT(num_args == 2); return mk_seq_prefix(args[0], args[1], result); case OP_SEQ_SUFFIX: SASSERT(num_args == 2); return mk_seq_suffix(args[0], args[1], result); + case OP_SEQ_INDEX: + SASSERT(num_args == 3); + return mk_seq_index(args[0], args[1], args[2], result); + case OP_SEQ_REPLACE: + SASSERT(num_args == 3); + return mk_seq_replace(args[0], args[1], args[2], result); case OP_SEQ_TO_RE: return BR_FAILED; case OP_SEQ_IN_RE: @@ -78,12 +84,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STRING_CONST: return BR_FAILED; - case OP_STRING_STRIDOF: - SASSERT(num_args == 3); - return mk_str_stridof(args[0], args[1], args[2], result); - case OP_STRING_STRREPL: - SASSERT(num_args == 3); - return mk_str_strrepl(args[0], args[1], args[2], result); case OP_STRING_ITOS: SASSERT(num_args == 1); return mk_str_itos(args[0], result); @@ -101,7 +101,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case _OP_STRING_IN_REGEXP: case _OP_STRING_TO_REGEXP: case _OP_STRING_SUBSTR: - + case _OP_STRING_STRREPL: + case _OP_STRING_STRIDOF: UNREACHABLE(); } return BR_FAILED; @@ -143,7 +144,7 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { +br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { std::string b; m_es.reset(); m_util.str.get_concat(a, m_es); @@ -176,7 +177,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { return BR_FAILED; } -br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) { +br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) { std::string s; rational pos, len; if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) && @@ -188,7 +189,7 @@ br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& resul } return BR_FAILED; } -br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) { +br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { std::string c, d; if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) { result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str())); @@ -212,7 +213,7 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) { +br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { std::string c; rational r; if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) { @@ -228,7 +229,7 @@ br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) { +br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) { std::string s1, s2; rational r; bool isc1 = m_util.str.is_string(a, s1); @@ -257,15 +258,17 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu return BR_FAILED; } -br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) { +br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result) { std::string s1, s2, s3; if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) && m_util.str.is_string(c, s3)) { std::ostringstream buffer; + bool can_replace = true; for (size_t i = 0; i < s1.length(); ) { - if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) { + if (can_replace && strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) { buffer << s3; i += s2.length(); + can_replace = false; } else { buffer << s1[i]; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index d4652f614..ec1747a4b 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -35,12 +35,12 @@ class seq_rewriter { ptr_vector m_es, m_lhs, m_rhs; br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); - br_status mk_str_length(expr* a, expr_ref& result); - br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result); - br_status mk_str_strctn(expr* a, expr* b, expr_ref& result); - br_status mk_str_at(expr* a, expr* b, expr_ref& result); - br_status mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result); - br_status mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_length(expr* a, expr_ref& result); + br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_contains(expr* a, expr* b, expr_ref& result); + br_status mk_seq_at(expr* a, expr* b, expr_ref& result); + br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result); br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result); br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result); br_status mk_str_itos(expr* a, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 2946bb1bc..5639356cc 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -177,6 +177,7 @@ void seq_decl_plugin::init() { sort* reAreA[2] = { reA, reA }; sort* AA[2] = { A, A }; sort* seqAint2T[3] = { seqA, intT, intT }; + sort* seq2AintT[3] = { seqA, seqA, intT }; sort* str2T[2] = { strT, strT }; sort* str3T[3] = { strT, strT, strT }; sort* strTint2T[3] = { strT, intT, intT }; @@ -184,6 +185,7 @@ void seq_decl_plugin::init() { sort* strTreT[2] = { strT, reT }; sort* str2TintT[3] = { strT, strT, intT }; sort* seqAintT[2] = { seqA, intT }; + sort* seq3A[3] = { seqA, seqA, seqA }; m_sigs.resize(LAST_SEQ_OP); // TBD: have (par ..) construct and load parameterized signature from premable. m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); @@ -193,6 +195,8 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_CONTAINS] = alloc(psig, m, "seq.contains", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA); + m_sigs[OP_SEQ_REPLACE] = alloc(psig, m, "seq.replace", 1, 3, seq3A, strT); + m_sigs[OP_SEQ_INDEX] = alloc(psig, m, "seq.indexof", 1, 3, seq2AintT, intT); m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA); m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT); m_sigs[OP_RE_PLUS] = alloc(psig, m, "re.+", 1, 1, &reA, reA); @@ -209,8 +213,8 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT); m_sigs[OP_STRING_CONST] = 0; - m_sigs[OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); - m_sigs[OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); + m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); + m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT); m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT); m_sigs[OP_REGEXP_LOOP] = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments. @@ -347,6 +351,17 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, info.set_left_associative(); return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); } + + case OP_SEQ_REPLACE: + return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRREPL); + case _OP_STRING_STRREPL: + return mk_str_fun(k, arity, domain, range, OP_SEQ_REPLACE); + + case OP_SEQ_INDEX: + return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRIDOF); + case _OP_STRING_STRIDOF: + return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX); + case OP_SEQ_PREFIX: return mk_seq_fun(k, arity, domain, range, _OP_STRING_PREFIX); case _OP_STRING_PREFIX: @@ -387,8 +402,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case _OP_STRING_SUBSTR: return mk_str_fun(k, arity, domain, range, OP_SEQ_EXTRACT); - case OP_STRING_STRIDOF: - case OP_STRING_STRREPL: case OP_STRING_ITOS: case OP_STRING_STOI: case OP_REGEXP_LOOP: diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 0ab889c38..33091ebd2 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -39,8 +39,10 @@ enum seq_op_kind { OP_SEQ_SUFFIX, OP_SEQ_CONTAINS, OP_SEQ_EXTRACT, + OP_SEQ_REPLACE, OP_SEQ_AT, - OP_SEQ_LENGTH, + OP_SEQ_LENGTH, + OP_SEQ_INDEX, OP_SEQ_TO_RE, OP_SEQ_IN_RE, @@ -59,12 +61,11 @@ enum seq_op_kind { // string specific operators. OP_STRING_CONST, - OP_STRING_STRIDOF, // TBD generalize - OP_STRING_STRREPL, // TBD generalize OP_STRING_ITOS, OP_STRING_STOI, OP_REGEXP_LOOP, // TBD re-loop: integers as parameters or arguments? // internal only operators. Converted to SEQ variants. + _OP_STRING_STRREPL, _OP_STRING_CONCAT, _OP_STRING_LENGTH, _OP_STRING_STRCTN, @@ -74,6 +75,7 @@ enum seq_op_kind { _OP_STRING_TO_REGEXP, _OP_STRING_CHARAT, _OP_STRING_SUBSTR, + _OP_STRING_STRIDOF, _OP_SEQ_SKOLEM, LAST_SEQ_OP }; @@ -175,6 +177,9 @@ public: app* mk_string(char const* s) { return mk_string(symbol(s)); } app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); } app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); } + app* mk_concat(expr* a, expr* b, expr* c) { + return mk_concat(mk_concat(a, b), c); + } expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); } app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); } app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); } @@ -200,8 +205,8 @@ public: bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); } bool is_contains(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); } bool is_at(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_AT); } - bool is_stridof(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); } - bool is_repl(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRREPL); } + bool is_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_INDEX); } + bool is_replace(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_REPLACE); } bool is_prefix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); } bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); } bool is_itos(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_ITOS); } @@ -215,8 +220,8 @@ public: MATCH_TERNARY(is_extract); MATCH_BINARY(is_contains); MATCH_BINARY(is_at); - MATCH_BINARY(is_stridof); - MATCH_BINARY(is_repl); + MATCH_BINARY(is_index); + MATCH_TERNARY(is_replace); MATCH_BINARY(is_prefix); MATCH_BINARY(is_suffix); MATCH_UNARY(is_itos); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a09078ad6..e0ab35fea 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -465,13 +465,6 @@ bool theory_seq::simplify_and_solve_eqs() { } -final_check_status theory_seq::add_axioms() { - for (unsigned i = 0; i < get_num_vars(); ++i) { - - // add axioms for len(x) when x = a ++ b - } - return FC_DONE; -} bool theory_seq::internalize_atom(app* a, bool) { return internalize_term(a); @@ -513,8 +506,6 @@ bool theory_seq::internalize_term(app* term) { !m_util.is_skolem(term)) { set_incomplete(term); } - - // assert basic axioms return true; } @@ -667,6 +658,170 @@ void theory_seq::create_axiom(expr_ref& e) { m_axioms.push_back(e); } +/* + encode that s is not a proper prefix of xs +*/ +expr_ref theory_seq::tightest_prefix(expr* s, expr* x) { + expr_ref s1 = mk_skolem(symbol("first"), s); + expr_ref c = mk_skolem(symbol("last"), s); + expr_ref fml(m); + + fml = m.mk_and(m.mk_eq(s, m_util.str.mk_concat(s1, c)), + m.mk_eq(m_util.str.mk_length(c), m_autil.mk_int(1)), + m.mk_not(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1)))); + + return fml; +} + + +void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { + context& ctx = get_context(); + // TBD: walk use list of n1 for concat, walk use-list of n2 for length. + // instantiate length distributes over concatenation axiom. + SASSERT(n1->get_root() != n2->get_root()); + if (!m_util.is_seq(n1->get_owner())) { + return; + } + func_decl* f_len = 0; + + // TBD: extract length function for sort if it is used. + // TBD: add filter for already processed length equivalence classes + if (!f_len) { + return; + } + enode_vector::const_iterator it = ctx.begin_enodes_of(f_len); + enode_vector::const_iterator end = ctx.end_enodes_of(f_len); + bool has_concat = true; + for (; has_concat && it != end; ++it) { + if ((*it)->get_root() == n1->get_root()) { + enode* start2 = n2; + do { + if (m_util.str.is_concat(n2->get_owner())) { + has_concat = true; + add_len_concat_axiom(n2->get_owner()); + } + n2 = n2->get_next(); + } + while (n2 != start2); + } + } +} + +void theory_seq::add_len_concat_axiom(expr* c) { + // or just internalize lc and have relevancy propagation create axiom? + expr *a, *b; + expr_ref la(m), lb(m), lc(m), fml(m); + VERIFY(m_util.str.is_concat(c, a, b)); + la = m_util.str.mk_length(a); + lb = m_util.str.mk_length(b); + lc = m_util.str.mk_length(c); + fml = m.mk_eq(m_autil.mk_add(la, lb), lc); + create_axiom(fml); +} + +/* + let i = Index(s, t) + + (!contains(s, t) -> i = -1) + (contains(s, t) & s = empty -> i = 0) + (contains(s, t) & s != empty -> t = xsy & tightest_prefix(s, x)) + + optional lemmas: + (len(s) > len(t) -> i = -1) + (len(s) <= len(t) -> i <= len(t)-len(s)) +*/ +void theory_seq::add_indexof_axiom(expr* i) { + expr* s, *t; + VERIFY(m_util.str.is_index(i, s, t)); + expr_ref cnt(m), fml(m), eq_empty(m); + expr_ref x = mk_skolem(m_contains_left_sym, s, t); + expr_ref y = mk_skolem(m_contains_right_sym, s, t); + eq_empty = m.mk_eq(s, m_util.str.mk_empty(m.get_sort(s))); + cnt = m_util.str.mk_contains(s, t); + fml = m.mk_or(cnt, m.mk_eq(i, m_autil.mk_int(-1))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), m.mk_not(eq_empty), m.mk_eq(i, m_autil.mk_int(0))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), eq_empty, m.mk_eq(t, m_util.str.mk_concat(x,s,y))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), eq_empty, tightest_prefix(s, x)); + create_axiom(fml); +} + +/* + let r = replace(a, s, t) + + (contains(s, a) -> r = xty & a = xsy & tightest_prefix(s,xs)) & + (!contains(s, a) -> r = a) + +*/ +void theory_seq::add_replace_axiom(expr* r) { + expr* a, *s, *t; + VERIFY(m_util.str.is_replace(r, a, s, t)); + expr_ref cnt(m), fml(m); + cnt = m_util.str.mk_contains(s, a); + expr_ref x = mk_skolem(m_contains_left_sym, s, a); + expr_ref y = mk_skolem(m_contains_right_sym, s, a); + fml = m.mk_or(m.mk_not(cnt), m.mk_eq(a, m_util.str.mk_concat(x, s, y))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), m.mk_eq(r, m_util.str.mk_concat(x, t, y))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), tightest_prefix(s, x)); + create_axiom(fml); + fml = m.mk_or(cnt, m.mk_eq(r, a)); + create_axiom(fml); +} + +/* + let n = len(x) + + len(x) >= 0 + len(x) = 0 => x = "" + x = "" => len(x) = 0 + len(x) = rewrite(len(x)) + */ +void theory_seq::add_len_axiom(expr* n) { + expr* x; + VERIFY(m_util.str.is_length(n, x)); + expr_ref fml(m), eq1(m), eq2(m), nr(m); + eq1 = m.mk_eq(m_autil.mk_int(0), n); + eq2 = m.mk_eq(x, m_util.str.mk_empty(m.get_sort(x))); + fml = m_autil.mk_le(m_autil.mk_int(0), n); + create_axiom(fml); + fml = m.mk_or(m.mk_not(eq1), eq2); + create_axiom(fml); + fml = m.mk_or(m.mk_not(eq2), eq1); + create_axiom(fml); + nr = n; + m_rewrite(nr); + if (nr != n) { + fml = m.mk_eq(n, nr); + create_axiom(fml); + } +} + +/* + check semantics of extract. + + let e = extract(s, i, l) + + 0 <= i < len(s) -> prefix(xe,s) & len(x) = i + 0 <= i < len(s) & l >= len(s) - i -> len(e) = len(s) - i + 0 <= i < len(s) & 0 <= l < len(s) - i -> len(e) = l + 0 <= i < len(s) & l < 0 -> len(e) = 0 + i < 0 -> e = s + i >= len(s) -> e = empty +*/ + +void theory_seq::add_extract_axiom(expr* e) { + expr* s, *i, *j; + VERIFY(m_util.str.is_extract(e, s, i, j)); + expr_ref i_ge_0(m), i_le_j(m), j_lt_s(m); + + NOT_IMPLEMENTED_YET(); + +} + void theory_seq::assert_axiom(expr_ref& e) { context & ctx = get_context(); if (m.is_true(e)) return; @@ -679,7 +834,7 @@ void theory_seq::assert_axiom(expr_ref& e) { expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2) { expr* es[2] = { e1, e2 }; - return expr_ref(m_util.mk_skolem(name, 2, es, m.get_sort(e1)), m); + return expr_ref(m_util.mk_skolem(name, e2?2:1, es, m.get_sort(e1)), m); } void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { @@ -744,6 +899,9 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { m.push_back(m_lhs.back(), n1->get_owner()); m.push_back(m_rhs.back(), n2->get_owner()); m_dam.push_back(m_deps.back(), m_dm.mk_leaf(enode_pair(n1, n2))); + + new_eq_len_concat(n1, n2); + new_eq_len_concat(n2, n1); } } @@ -807,8 +965,7 @@ void theory_seq::restart_eh() { void theory_seq::relevant_eh(app* n) { if (m_util.str.is_length(n)) { - expr_ref e(m); - e = m_autil.mk_le(m_autil.mk_numeral(rational(0), true), n); - create_axiom(e); + add_len_axiom(n); } } + diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 06fb6fac0..87a6a2dc6 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -166,15 +166,22 @@ namespace smt { bool is_left_select(expr* a, expr*& b); bool is_right_select(expr* a, expr*& b); - final_check_status add_axioms(); - void assert_axiom(expr_ref& e); void create_axiom(expr_ref& e); + void add_indexof_axiom(expr* e); + void add_replace_axiom(expr* e); + void add_extract_axiom(expr* e); + void add_len_concat_axiom(expr* c); + void add_len_axiom(expr* n); + + void new_eq_len_concat(enode* n1, enode* n2); + + expr_ref tightest_prefix(expr* s, expr* x); expr_ref canonize(expr* e, enode_pair_dependency*& eqs); expr_ref expand(expr* e, enode_pair_dependency*& eqs); void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); - expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2); + expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0); void set_incomplete(app* term);