diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-11 11:23:19 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-11 18:15:18 -0400 |
commit | c3a959b3112af83492694b8f0919381b1c467fb8 (patch) | |
tree | 62ae7f49087bfb61a439161b5bc1cb5c8c691f21 /src/theory/strings/kinds | |
parent | f49c16dd1169d3de4bbfcdca22af1269bbd0a005 (diff) |
Theory of strings.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory/strings/kinds')
-rw-r--r-- | src/theory/strings/kinds | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds new file mode 100644 index 000000000..814276a7c --- /dev/null +++ b/src/theory/strings/kinds @@ -0,0 +1,105 @@ +# 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 |