From 9678f58a7fedab4fc061761c58382f4023686108 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 6 Jul 2020 18:48:10 -0500 Subject: Front end support for sequences (#4690) With this PR, we now support a preliminary draft of a theory of sequences. This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them. As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term. We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++). --- src/theory/strings/word.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/theory/strings/word.cpp') diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index 35b315e35..fec567733 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -452,6 +452,15 @@ Node Word::reverse(TNode x) std::reverse(nvec.begin(), nvec.end()); return nm->mkConst(String(nvec)); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst().getSequence(); + const std::vector& vecc = sx.getVec(); + std::vector vecr(vecc.begin(), vecc.end()); + std::reverse(vecr.begin(), vecr.end()); + Sequence res(sx.getType(), vecr); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } -- cgit v1.2.3