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