diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/kinds | 2 | ||||
-rw-r--r-- | src/theory/strings/rewrites.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/rewrites.h | 3 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 13 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.h | 5 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 49 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 8 |
8 files changed, 63 insertions, 30 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 020cedb30..427e2e4e6 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -84,6 +84,7 @@ constant CONST_SEQUENCE \ operator SEQ_UNIT 1 "a sequence of length one" operator SEQ_NTH 2 "The nth element of a sequence" +operator SEQ_NTH_TOTAL 2 "The nth element of a sequence (internal, for responses to expand definitions only)" # equal equal / less than / output operator STRING_TO_REGEXP 1 "convert string to regexp" @@ -171,5 +172,6 @@ typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule typerule SEQ_NTH ::CVC4::theory::strings::SeqNthTypeRule +typerule SEQ_NTH_TOTAL ::CVC4::theory::strings::SeqNthTypeRule endtheory diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index a32e5bc9e..dca793049 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -210,7 +210,8 @@ const char* toString(Rewrite r) case Rewrite::LEN_SEQ_UNIT: return "LEN_SEQ_UNIT"; case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM"; case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL"; - case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL"; + case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL"; + case Rewrite::SEQ_NTH_TOTAL_OOB: return "SEQ_NTH_TOTAL_OOB"; default: return "?"; } } diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index f9824405b..a450ae7f6 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -213,7 +213,8 @@ enum class Rewrite : uint32_t LEN_SEQ_UNIT, CHARAT_ELIM, SEQ_UNIT_EVAL, - SEQ_NTH_EVAL + SEQ_NTH_EVAL, + SEQ_NTH_TOTAL_OOB }; /** diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 2cefe6b09..1382ab0f9 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1491,7 +1491,7 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewriteSeqUnit(node); } - else if (nk == SEQ_NTH) + else if (nk == SEQ_NTH || nk == SEQ_NTH_TOTAL) { retNode = rewriteSeqNth(node); } @@ -1516,7 +1516,7 @@ RewriteResponse SequencesRewriter::preRewrite(TNode node) Node SequencesRewriter::rewriteSeqNth(Node node) { - Assert(node.getKind() == SEQ_NTH); + Assert(node.getKind() == SEQ_NTH || node.getKind() == SEQ_NTH_TOTAL); Node ret; Node s = node[0]; Node i = node[1]; @@ -1530,6 +1530,12 @@ Node SequencesRewriter::rewriteSeqNth(Node node) ret = elements[pos]; return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL); } + else if (node.getKind() == SEQ_NTH_TOTAL) + { + // return arbitrary term + Node ret = s.getType().getSequenceElementType().mkGroundValue(); + return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB); + } else { return node; diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index a1e04071b..f5f2dfd35 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -130,6 +130,19 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn, return mkTypedSkolemCached(tn, a, Node::null(), id, c); } +Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c) +{ + Assert(seqType.isSequence()); + NodeManager* nm = NodeManager::currentNM(); + std::vector<TypeNode> argTypes; + argTypes.push_back(seqType); + argTypes.push_back(nm->integerType()); + TypeNode elemType = seqType.getSequenceElementType(); + TypeNode ufType = nm->mkFunctionType(argTypes, elemType); + return mkTypedSkolemCached( + ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, c); +} + Node SkolemCache::mkSkolem(const char* c) { // TODO: eliminate this diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 0a6dd367f..fa76afebd 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -159,6 +159,11 @@ class SkolemCache TypeNode tn, Node a, Node b, SkolemId id, const char* c); /** Same as mkTypedSkolemCached above for (a,[null],id) */ Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c); + /** + * Specific version for seq.nth, used for cases where the index is out of + * range for sequence type seqType. + */ + Node mkSkolemSeqNth(TypeNode seqType, const char* c); /** Returns a (uncached) skolem of type string with name c */ Node mkSkolem(const char* c); /** Returns true if n is a skolem allocated by this class */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8ce8e0ecb..8915fcd02 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -570,23 +570,21 @@ TrustNode TheoryStrings::expandDefinition(Node node) { Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; - if (node.getKind() == STRING_FROM_CODE) + if (node.getKind() == kind::SEQ_NTH) { - // str.from_code(t) ---> - // witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "") NodeManager* nm = NodeManager::currentNM(); - Node t = node[0]; - Node card = nm->mkConst(Rational(utils::getAlphabetCardinality())); - Node cond = - nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card)); - Node k = nm->mkBoundVar(nm->stringType()); - Node bvl = nm->mkNode(BOUND_VAR_LIST, k); - Node emp = Word::mkEmptyWord(node.getType()); - Node ret = nm->mkNode( - WITNESS, - bvl, - nm->mkNode( - ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); + SkolemCache* sc = d_termReg.getSkolemCache(); + Node s = node[0]; + Node n = node[1]; + // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n)) + Node cond = nm->mkNode(AND, + nm->mkNode(LEQ, d_zero, n), + nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s))); + Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n); + Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf"); + Node u = nm->mkNode(APPLY_UF, uf, s, n); + Node ret = nm->mkNode(ITE, cond, ss, u); + Trace("strings-exp-def") << "...return " << ret << std::endl; return TrustNode::mkTrustRewrite(node, ret, nullptr); } return TrustNode::null(); @@ -1006,11 +1004,24 @@ void TheoryStrings::checkRegisterTermsNormalForms() TrustNode TheoryStrings::ppRewrite(TNode atom) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; - // first, see if we need to expand definitions - TrustNode texp = expandDefinition(atom); - if (!texp.isNull()) + if (atom.getKind() == STRING_FROM_CODE) { - return texp; + // str.from_code(t) ---> + // witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "") + NodeManager* nm = NodeManager::currentNM(); + Node t = atom[0]; + Node card = nm->mkConst(Rational(utils::getAlphabetCardinality())); + Node cond = + nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card)); + Node k = nm->mkBoundVar(nm->stringType()); + Node bvl = nm->mkNode(BOUND_VAR_LIST, k); + Node emp = Word::mkEmptyWord(atom.getType()); + Node ret = nm->mkNode( + WITNESS, + bvl, + nm->mkNode( + ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); + return TrustNode::mkTrustRewrite(atom, ret, nullptr); } TrustNode ret; Node atomRet = atom; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 87ab533f4..81cca34af 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -444,13 +444,7 @@ Node StringsPreprocess::reduce(Node t, Node b1 = nm->mkNode(AND, b11, b12, b13); // nodes for the case where `seq.nth` is undefined. - std::vector<TypeNode> argTypes; - argTypes.push_back(s.getType()); - argTypes.push_back(nm->integerType()); - TypeNode elemType = s.getType().getSequenceElementType(); - TypeNode ufType = nm->mkFunctionType(argTypes, elemType); - Node uf = sc->mkTypedSkolemCached( - ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, "Uf"); + Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf"); Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n)); // the full ite, split on definedness of `seq.nth` |