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/strings/kinds | |
parent | f3d010e07f30dd658d4532a43b3813654376162d (diff) |
Remove abstract regular expression constant (#1698)
Diffstat (limited to 'src/theory/strings/kinds')
-rw-r--r-- | src/theory/strings/kinds | 9 |
1 files changed, 1 insertions, 8 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" |