diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-06 18:48:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-06 18:48:10 -0500 |
commit | 9678f58a7fedab4fc061761c58382f4023686108 (patch) | |
tree | 5ccc2e13b00a32a2e8fa87604b4a2f3a92b12e7e /src/expr/expr_manager_template.cpp | |
parent | ae0bfbdacfec8b2d21b10cbc4955305f49a62a54 (diff) |
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.++).
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index d499b8bb7..d69dc73f9 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -661,6 +661,14 @@ SetType ExprManager::mkSetType(Type elementType) const { return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode)))); } +SequenceType ExprManager::mkSequenceType(Type elementType) const +{ + NodeManagerScope nms(d_nodeManager); + return SequenceType(Type( + d_nodeManager, + new TypeNode(d_nodeManager->mkSequenceType(*elementType.d_typeNode)))); +} + DatatypeType ExprManager::mkDatatypeType(Datatype& datatype, uint32_t flags) { // Not worth a special implementation; this doesn't need to be fast |