diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-30 13:10:54 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-30 13:10:54 -0500 |
| commit | ba659fb1b8bc2f110616ec113892f63f210a5ebb (patch) | |
| tree | 9beaf9be94879a75f4c2cadf8289664b53cc1d1b /src/theory/strings/sequences_rewriter.h | |
| parent | da165b9cbee366d4e77716617f2e2c794da9bd46 (diff) | |
Add the sequence type (#4539)
This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.
The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.
Diffstat (limited to 'src/theory/strings/sequences_rewriter.h')
| -rw-r--r-- | src/theory/strings/sequences_rewriter.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 56b74f536..490dd8b3c 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -224,6 +224,12 @@ class SequencesRewriter : public TheoryRewriter * Returns the rewritten form of node. */ Node rewriteStringToCode(Node node); + /** rewrite seq.unit + * This is the entry point for post-rewriting terms n of the form + * seq.unit( t ) + * Returns the rewritten form of node. + */ + Node rewriteSeqUnit(Node node); /** length preserving rewrite * |