From 30580a012af8ab26ed2e09786d6646a104311a61 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Dec 2015 02:38:56 -0800 Subject: [PATCH] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 +++ src/ast/seq_decl_plugin.h | 2 +- src/smt/theory_seq.cpp | 48 ++++++++++++++++++++----------- 3 files changed, 36 insertions(+), 18 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 564074ea8..a0e1bb955 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -72,6 +72,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); return mk_seq_suffix(args[0], args[1], result); case OP_SEQ_INDEX: + if (num_args == 2) { + expr_ref arg3(m_autil.mk_int(0), m()); + return mk_seq_index(args[0], args[1], arg3, result); + } SASSERT(num_args == 3); return mk_seq_index(args[0], args[1], args[2], result); case OP_SEQ_REPLACE: diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 33091ebd2..208a29c78 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -220,7 +220,7 @@ public: MATCH_TERNARY(is_extract); MATCH_BINARY(is_contains); MATCH_BINARY(is_at); - MATCH_BINARY(is_index); + MATCH_TERNARY(is_index); MATCH_TERNARY(is_replace); MATCH_BINARY(is_prefix); MATCH_BINARY(is_suffix); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fe6a0b12b..555cefff7 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -745,33 +745,47 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) { } /* - let i = Index(s, t) + let i = Index(s, t, offset) - (!contains(s, t) -> i = -1) - (s = empty -> i = 0) - (contains(s, t) & s != empty -> t = xsy) - (contains(s, t) -> tightest_prefix(s, x)) + if offset = 0: + (!contains(s, t) -> i = -1) + (s = empty -> i = 0) + (contains(s, t) & s != empty -> t = xsy) + (contains(s, t) -> tightest_prefix(s, x)) + if 0 <= offset < len(t): + t = zt' & len(z) == offset + add above constraints with t' + if offset >= len(t): + i = -1 + if offset < 0: + ? 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 fml(m), emp(m), minus_one(m), zero(m), xsy(m); - expr_ref x = mk_skolem(m_contains_left_sym, s, t); - expr_ref y = mk_skolem(m_contains_right_sym, s, t); + expr* s, *t, *offset; + rational r; + VERIFY(m_util.str.is_index(i, s, t, offset)); + expr_ref emp(m), minus_one(m), zero(m), xsy(m); minus_one = m_autil.mk_int(-1); zero = m_autil.mk_int(0); emp = m_util.str.mk_empty(m.get_sort(s)); - xsy = m_util.str.mk_concat(x,s,y); - literal cnt = mk_literal(m_util.str.mk_contains(s, t)); - literal eq_empty = mk_eq(s, emp, false); - add_axiom(cnt, mk_eq(i, minus_one, false)); - add_axiom(~eq_empty, mk_eq(i, zero, false)); - add_axiom(~cnt, eq_empty, mk_eq(t, xsy, false)); - tightest_prefix(s, x, ~cnt); + if (m_autil.is_numeral(offset, r) && r.is_zero()) { + expr_ref x = mk_skolem(m_contains_left_sym, s, t); + expr_ref y = mk_skolem(m_contains_right_sym, s, t); + xsy = m_util.str.mk_concat(x,s,y); + literal cnt = mk_literal(m_util.str.mk_contains(s, t)); + literal eq_empty = mk_eq(s, emp, false); + add_axiom(cnt, mk_eq(i, minus_one, false)); + add_axiom(~eq_empty, mk_eq(i, zero, false)); + add_axiom(~cnt, eq_empty, mk_eq(t, xsy, false)); + tightest_prefix(s, x, ~cnt); + } + else { + // TBD + } } /*