diff options
Diffstat (limited to 'src/theory/strings/kinds')
| -rw-r--r-- | src/theory/strings/kinds | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 27ffe5d26..800847ffe 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -58,12 +58,27 @@ constant CONST_STRING \ "util/string.h" \ "a string of characters" +# the type +operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements" +cardinality SEQUENCE_TYPE \ + "::CVC4::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \ + "theory/strings/theory_strings_type_rules.h" +well-founded SEQUENCE_TYPE \ + "::CVC4::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \ + "theory/strings/theory_strings_type_rules.h" +enumerator SEQUENCE_TYPE \ + "::CVC4::theory::strings::SequenceEnumerator" \ + "theory/strings/type_enumerator.h" + constant CONST_SEQUENCE \ ::CVC4::ExprSequence \ ::CVC4::ExprSequenceHashFunction \ "expr/expr_sequence.h" \ "a sequence of characters" +operator SEQ_UNIT 1 "a sequence of length one" + # equal equal / less than / output operator STRING_TO_REGEXP 1 "convert string to regexp" operator REGEXP_CONCAT 2: "regexp concat" @@ -144,4 +159,9 @@ typerule STRING_FROM_CODE "SimpleTypeRule<RString, AInteger>" typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>" typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" +### sequence specific operators + +typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule +typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule + endtheory |