src/theory/strings/kinds

   1 # kinds                                                               -*- sh -*-
   2 #
   3 # For documentation on this file format, please refer to
   4 # src/theory/builtin/kinds.
   5 #
   6
   7 theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
   8
   9 properties check parametric propagate getNextDecisionRequest presolve
  10
  11 rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"
  12
  13 typechecker "theory/strings/theory_strings_type_rules.h"
  14
  15 operator STRING_CONCAT 2: "string concat (N-ary)"
  16 operator STRING_IN_REGEXP 2 "membership"
  17 operator STRING_LENGTH 1 "string length"
  18 operator STRING_SUBSTR 3 "string substr (user symbol)"
  19 operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)"
  20 operator STRING_CHARAT 2 "string charat (user symbol)"
  21 operator STRING_STRCTN 2 "string contains"
  22 operator STRING_STRIDOF 3 "string indexof"
  23 operator STRING_STRREPL 3 "string replace"
  24 operator STRING_PREFIX 2 "string prefixof"
  25 operator STRING_SUFFIX 2 "string suffixof"
  26 operator STRING_ITOS 1 "integer to string"
  27 operator STRING_STOI 1 "string to integer (total function)"
  28 operator STRING_U16TOS 1 "uint16 to string"
  29 operator STRING_STOU16 1 "string to uint16"
  30 operator STRING_U32TOS 1 "uint32 to string"
  31 operator STRING_STOU32 1 "string to uint32"
  32
  33 #sort CHAR_TYPE \
  34 #    Cardinality::INTEGERS \
  35 #    well-founded \
  36 #        "NodeManager::currentNM()->mkConst(::CVC4::String())" \
  37 #        "util/regexp.h" \
  38 #    "String type"
  39
  40 sort STRING_TYPE \
  41     Cardinality::INTEGERS \
  42     well-founded \
  43         "NodeManager::currentNM()->mkConst(::CVC4::String())" \
  44         "util/regexp.h" \
  45     "String type"
  46
  47 sort REGEXP_TYPE \
  48     Cardinality::INTEGERS \
  49     well-founded \
  50         "NodeManager::currentNM()->mkConst(::CVC4::RegExp())" \
  51         "util/regexp.h" \
  52     "RegExp type"
  53
  54 enumerator STRING_TYPE \
  55     "::CVC4::theory::strings::StringEnumerator" \
  56     "theory/strings/type_enumerator.h"
  57
  58 #enumerator REGEXP_TYPE \
  59 #    "::CVC4::theory::strings::RegExpEnumerator" \
  60 #    "theory/strings/type_enumerator.h"
  61
  62 constant CONST_STRING \
  63     ::CVC4::String \
  64     ::CVC4::strings::StringHashFunction \
  65     "util/regexp.h" \
  66     "a string of characters"
  67
  68 constant CONST_REGEXP \
  69     ::CVC4::RegExp \
  70     ::CVC4::RegExpHashFunction \
  71     "util/regexp.h" \
  72     "a regular expression"
  73
  74 typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
  75 typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule
  76
  77 # equal equal / less than / output
  78 operator STRING_TO_REGEXP 1 "convert string to regexp"
  79 operator REGEXP_CONCAT 2: "regexp concat"
  80 operator REGEXP_UNION 2: "regexp union"
  81 operator REGEXP_INTER 2: "regexp intersection"
  82 operator REGEXP_STAR 1 "regexp *"
  83 operator REGEXP_PLUS 1 "regexp +"
  84 operator REGEXP_OPT 1 "regexp ?"
  85 operator REGEXP_RANGE 2 "regexp range"
  86 operator REGEXP_LOOP 2:3 "regexp loop"
  87
  88 operator REGEXP_EMPTY 0 "regexp empty"
  89 operator REGEXP_SIGMA 0 "regexp all characters"
  90
  91 #internal
  92 operator REGEXP_RV 1 "regexp rv (internal use only)"
  93 typerule REGEXP_RV ::CVC4::theory::strings::RegExpRVTypeRule
  94
  95 #typerules
  96 typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
  97 typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule
  98 typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
  99 typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
 100 typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
 101 typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
 102 typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
 103 typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule
 104
 105 typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 106
 107 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
 108 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
 109 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
 110 typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule
 111 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
 112 typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
 113 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
 114 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
 115 typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
 116 typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
 117 typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
 118 typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
 119 typerule STRING_U16TOS ::CVC4::theory::strings::StringIntToStrTypeRule
 120 typerule STRING_STOU16 ::CVC4::theory::strings::StringStrToIntTypeRule
 121 typerule STRING_U32TOS ::CVC4::theory::strings::StringIntToStrTypeRule
 122 typerule STRING_STOU32 ::CVC4::theory::strings::StringStrToIntTypeRule
 123
 124 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 125
 126 typerule REGEXP_EMPTY ::CVC4::theory::strings::EmptyRegExpTypeRule
 127 typerule REGEXP_SIGMA ::CVC4::theory::strings::SigmaRegExpTypeRule
 128
 129 endtheory