# kinds [for strings theory]
#

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

properties check parametric propagate

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"

operator STRING_IN_REGEXP 2 "membership"

operator STRING_LENGTH 1 "string length"

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

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()->mkConst(::CVC4::RegExp())" \
        "util/regexp.h" \
    "RegExp type"

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

#enumerator REGEXP_TYPE \
#    "::CVC4::theory::strings::RegExpEnumerator" \
#    "theory/strings/type_enumerator.h"

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

constant CONST_REGEXP \
    ::CVC4::RegExp \
    ::CVC4::RegExpHashFunction \
    "util/regexp.h" \
    "a regular expression"

typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule

# equal equal / less than / output
operator STRING_TO_REGEXP 1 "convert string to regexp"
operator REGEXP_CONCAT 2: "regexp concat"
operator REGEXP_OR 2: "regexp or"
operator REGEXP_INTER 2: "regexp intersection"
operator REGEXP_STAR 1 "regexp *"
operator REGEXP_PLUS 1 "regexp +"
operator REGEXP_OPT 1 "regexp ?"

#constant REGEXP_EMPTY \
#	::CVC4::RegExp \
#	::CVC4::RegExpHashFunction \
#	"util/string.h" \
#	"a regexp contains nothing"

#constant REGEXP_ALL \
#	::CVC4::RegExp \
#	::CVC4::RegExpHashFunction \
#	"util/string.h" \
#	"a regexp contains all strings"

#constant REGEXP_SIGMA \
#	::CVC4::RegExp \
#	::CVC4::RegExpHashFunction \
#	"util/string.h" \
#	"a regexp contains an arbitrary charactor"

typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
typerule REGEXP_OR ::CVC4::theory::strings::RegExpOrTypeRule
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 STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule


typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule

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

endtheory