# kinds                                                               -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#

theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"

properties check parametric propagate presolve

rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"

typechecker "theory/strings/theory_strings_type_rules.h"

operator STRING_CONCAT 2: "string concat (N-ary)"
operator STRING_IN_REGEXP 2 "membership"
operator STRING_LENGTH 1 "string length"
operator STRING_SUBSTR 3 "string substr"
operator STRING_CHARAT 2 "string charat"
operator STRING_STRCTN 2 "string contains"
operator STRING_LT 2 "string less than"
operator STRING_LEQ 2 "string less than or equal"
operator STRING_STRIDOF 3 "string indexof"
operator STRING_STRREPL 3 "string replace"
operator STRING_STRREPLALL 3 "string replace all"
operator STRING_PREFIX 2 "string prefixof"
operator STRING_SUFFIX 2 "string suffixof"
operator STRING_ITOS 1 "integer to string"
operator STRING_STOI 1 "string to integer (total function)"
operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise"

sort STRING_TYPE \
    Cardinality::INTEGERS \
    well-founded \
        "NodeManager::currentNM()->mkConst(::CVC4::String())" \
        "util/regexp.h" \
    "String type"

sort REGEXP_TYPE \
    Cardinality::INTEGERS \
    well-founded \
        "NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \
        "util/regexp.h" \
    "RegExp type"

enumerator STRING_TYPE \
    "::CVC4::theory::strings::StringEnumerator" \
    "theory/strings/type_enumerator.h"

constant CONST_STRING \
    ::CVC4::String \
    ::CVC4::strings::StringHashFunction \
    "util/regexp.h" \
    "a string of characters"

typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule

# equal equal / less than / output
operator STRING_TO_REGEXP 1 "convert string to regexp"
operator REGEXP_CONCAT 2: "regexp concat"
operator REGEXP_UNION 2: "regexp union"
operator REGEXP_INTER 2: "regexp intersection"
operator REGEXP_STAR 1 "regexp *"
operator REGEXP_PLUS 1 "regexp +"
operator REGEXP_OPT 1 "regexp ?"
operator REGEXP_RANGE 2 "regexp range"
operator REGEXP_LOOP 2:3 "regexp loop"

operator REGEXP_EMPTY 0 "regexp empty"
operator REGEXP_SIGMA 0 "regexp all characters"

#internal
operator REGEXP_RV 1 "regexp rv (internal use only)"
typerule REGEXP_RV ::CVC4::theory::strings::RegExpRVTypeRule

#typerules
typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule
typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule

typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule

typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule
typerule STRING_LT ::CVC4::theory::strings::StringRelationTypeRule
typerule STRING_LEQ ::CVC4::theory::strings::StringRelationTypeRule
typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
typerule STRING_STRREPLALL ::CVC4::theory::strings::StringReplaceTypeRule
typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
typerule STRING_CODE ::CVC4::theory::strings::StringStrToIntTypeRule

typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule

typerule REGEXP_EMPTY ::CVC4::theory::strings::EmptyRegExpTypeRule
typerule REGEXP_SIGMA ::CVC4::theory::strings::SigmaRegExpTypeRule

endtheory