diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/theory/strings/kinds | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/theory/strings/kinds')
-rw-r--r-- | src/theory/strings/kinds | 70 |
1 files changed, 35 insertions, 35 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 427e2e4e6..6f366d6d7 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -4,11 +4,11 @@ # src/theory/builtin/kinds. # -theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h" +theory THEORY_STRINGS ::CVC5::theory::strings::TheoryStrings "theory/strings/theory_strings.h" properties check parametric presolve -rewriter ::CVC4::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h" +rewriter ::CVC5::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h" typechecker "theory/strings/theory_strings_type_rules.h" @@ -42,7 +42,7 @@ operator STRING_REV 1 "string reverse" sort STRING_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkConst(::CVC4::String())" \ + "NodeManager::currentNM()->mkConst(::CVC5::String())" \ "util/string.h" \ "String type" @@ -54,31 +54,31 @@ sort REGEXP_TYPE \ "RegExp type" enumerator STRING_TYPE \ - "::CVC4::theory::strings::StringEnumerator" \ + "::CVC5::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" constant CONST_STRING \ - ::CVC4::String \ - ::CVC4::strings::StringHashFunction \ + ::CVC5::String \ + ::CVC5::strings::StringHashFunction \ "util/string.h" \ "a string of characters" # the type operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements" cardinality SEQUENCE_TYPE \ - "::CVC4::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \ + "::CVC5::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \ "theory/strings/theory_strings_type_rules.h" well-founded SEQUENCE_TYPE \ - "::CVC4::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \ + "::CVC5::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \ + "::CVC5::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \ "theory/strings/theory_strings_type_rules.h" enumerator SEQUENCE_TYPE \ - "::CVC4::theory::strings::SequenceEnumerator" \ + "::CVC5::theory::strings::SequenceEnumerator" \ "theory/strings/type_enumerator.h" constant CONST_SEQUENCE \ - ::CVC4::Sequence \ - ::CVC4::SequenceHashFunction \ + ::CVC5::Sequence \ + ::CVC5::SequenceHashFunction \ "expr/sequence.h" \ "a sequence of characters" @@ -102,17 +102,17 @@ operator REGEXP_EMPTY 0 "regexp empty" operator REGEXP_SIGMA 0 "regexp all characters" constant REGEXP_REPEAT_OP \ - ::CVC4::RegExpRepeat \ - ::CVC4::RegExpRepeatHashFunction \ + ::CVC5::RegExpRepeat \ + ::CVC5::RegExpRepeatHashFunction \ "util/regexp.h" \ - "operator for regular expression repeat; payload is an instance of the CVC4::RegExpRepeat class" + "operator for regular expression repeat; payload is an instance of the CVC5::RegExpRepeat class" parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term" constant REGEXP_LOOP_OP \ - ::CVC4::RegExpLoop \ - ::CVC4::RegExpLoopHashFunction \ + ::CVC5::RegExpLoop \ + ::CVC5::RegExpLoopHashFunction \ "util/regexp.h" \ - "operator for regular expression loop; payload is an instance of the CVC4::RegExpLoop class" + "operator for regular expression loop; payload is an instance of the CVC5::RegExpLoop class" parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term" #internal @@ -128,7 +128,7 @@ typerule REGEXP_DIFF "SimpleTypeRuleVar<RRegExp, ARegExp>" typerule REGEXP_STAR "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_PLUS "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>" -typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule +typerule REGEXP_RANGE ::CVC5::theory::strings::RegExpRangeTypeRule typerule REGEXP_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>" typerule REGEXP_REPEAT "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_LOOP_OP "SimpleTypeRule<RBuiltinOperator>" @@ -141,18 +141,18 @@ typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>" ### operators that apply to both strings and sequences -typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule -typerule STRING_LENGTH ::CVC4::theory::strings::StringStrToIntTypeRule -typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule -typerule STRING_UPDATE ::CVC4::theory::strings::StringUpdateTypeRule -typerule STRING_CHARAT ::CVC4::theory::strings::StringAtTypeRule -typerule STRING_STRCTN ::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::StringStrToBoolTypeRule -typerule STRING_SUFFIX ::CVC4::theory::strings::StringStrToBoolTypeRule -typerule STRING_REV ::CVC4::theory::strings::StringStrToStrTypeRule +typerule STRING_CONCAT ::CVC5::theory::strings::StringConcatTypeRule +typerule STRING_LENGTH ::CVC5::theory::strings::StringStrToIntTypeRule +typerule STRING_SUBSTR ::CVC5::theory::strings::StringSubstrTypeRule +typerule STRING_UPDATE ::CVC5::theory::strings::StringUpdateTypeRule +typerule STRING_CHARAT ::CVC5::theory::strings::StringAtTypeRule +typerule STRING_STRCTN ::CVC5::theory::strings::StringRelationTypeRule +typerule STRING_STRIDOF ::CVC5::theory::strings::StringIndexOfTypeRule +typerule STRING_STRREPL ::CVC5::theory::strings::StringReplaceTypeRule +typerule STRING_STRREPLALL ::CVC5::theory::strings::StringReplaceTypeRule +typerule STRING_PREFIX ::CVC5::theory::strings::StringStrToBoolTypeRule +typerule STRING_SUFFIX ::CVC5::theory::strings::StringStrToBoolTypeRule +typerule STRING_REV ::CVC5::theory::strings::StringStrToStrTypeRule ### string specific operators @@ -169,9 +169,9 @@ typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" ### sequence specific operators -typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule -typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule -typerule SEQ_NTH ::CVC4::theory::strings::SeqNthTypeRule -typerule SEQ_NTH_TOTAL ::CVC4::theory::strings::SeqNthTypeRule +typerule CONST_SEQUENCE ::CVC5::theory::strings::ConstSequenceTypeRule +typerule SEQ_UNIT ::CVC5::theory::strings::SeqUnitTypeRule +typerule SEQ_NTH ::CVC5::theory::strings::SeqNthTypeRule +typerule SEQ_NTH_TOTAL ::CVC5::theory::strings::SeqNthTypeRule endtheory |