src/theory/strings/kinds

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