summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/strings/kinds2
-rw-r--r--src/theory/strings/rewrites.cpp3
-rw-r--r--src/theory/strings/rewrites.h3
-rw-r--r--src/theory/strings/sequences_rewriter.cpp10
-rw-r--r--src/theory/strings/skolem_cache.cpp13
-rw-r--r--src/theory/strings/skolem_cache.h5
-rw-r--r--src/theory/strings/theory_strings.cpp49
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp8
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`
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback