diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-23 15:23:00 -0500 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-03-23 13:23:00 -0700 |
| commit | d13b2981520e3d39039e8eb2c3c844de473a1e7c (patch) | |
| tree | 7be3fe248f9d009a71e1470e5d63641c4b33c5a4 /src/theory | |
| parent | f3d010e07f30dd658d4532a43b3813654376162d (diff) | |
Remove abstract regular expression constant (#1698)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/strings/kinds | 9 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 8 |
2 files changed, 1 insertions, 16 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 3a5fd59e9..15dd5b423 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -42,7 +42,7 @@ sort STRING_TYPE \ sort REGEXP_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkConst(::CVC4::RegExp())" \ + "NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \ "util/regexp.h" \ "RegExp type" @@ -60,14 +60,7 @@ constant CONST_STRING \ "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" diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 176398776..da1b71fff 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -235,14 +235,6 @@ public: } }; -class RegExpConstantTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - return nodeManager->regExpType(); - } -}; - class RegExpConcatTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) |