diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-19 19:24:32 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-20 00:24:32 +0000 |
commit | fc9c1005a398c537bdb491d1b161f3e316b68b5e (patch) | |
tree | 6a3a4abfc06e43a9e9749e68eeb5539cfb85c758 | |
parent | a96ed1538245b2ce2cd8a8084e0288d07071ca23 (diff) |
Add basic regular expression type enumerator (#7416)
The lack of a type enumerator for regular expressions makes certain things impossible e.g. sygus-based sampling for RE queries.
It is trivial to support a basic RE enumerator that takes singleton languages of strings. This commit adds this utility as the type enumerator for RE.
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/theory/strings/kinds | 4 | ||||
-rw-r--r-- | src/theory/strings/regexp_enumerator.cpp | 49 | ||||
-rw-r--r-- | src/theory/strings/regexp_enumerator.h | 59 |
4 files changed, 114 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 374c57726..cde739454 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1081,6 +1081,8 @@ libcvc5_add_sources( theory/strings/normal_form.h theory/strings/proof_checker.cpp theory/strings/proof_checker.h + theory/strings/regexp_enumerator.cpp + theory/strings/regexp_enumerator.h theory/strings/regexp_elim.cpp theory/strings/regexp_elim.h theory/strings/regexp_entail.cpp diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index aa95ef2f8..9faa935e1 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -56,6 +56,10 @@ enumerator STRING_TYPE \ "::cvc5::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" +enumerator REGEXP_TYPE \ + "::cvc5::theory::strings::RegExpEnumerator" \ + "theory/strings/regexp_enumerator.h" + constant CONST_STRING \ class \ String \ diff --git a/src/theory/strings/regexp_enumerator.cpp b/src/theory/strings/regexp_enumerator.cpp new file mode 100644 index 000000000..261d0008e --- /dev/null +++ b/src/theory/strings/regexp_enumerator.cpp @@ -0,0 +1,49 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of enumerator for regular expressions. + */ + +#include "theory/strings/regexp_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +RegExpEnumerator::RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep) + : TypeEnumeratorBase<RegExpEnumerator>(type), d_senum(type, tep) +{ +} + +RegExpEnumerator::RegExpEnumerator(const RegExpEnumerator& enumerator) + : TypeEnumeratorBase<RegExpEnumerator>(enumerator.getType()), + d_senum(enumerator.d_senum) +{ +} + +Node RegExpEnumerator::operator*() +{ + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::STRING_TO_REGEXP, *d_senum); +} + +RegExpEnumerator& RegExpEnumerator::operator++() +{ + ++d_senum; + return *this; +} + +bool RegExpEnumerator::isFinished() { return d_senum.isFinished(); } + +} // namespace strings +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/strings/regexp_enumerator.h b/src/theory/strings/regexp_enumerator.h new file mode 100644 index 000000000..289c8b046 --- /dev/null +++ b/src/theory/strings/regexp_enumerator.h @@ -0,0 +1,59 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Enumerators for regular expressions. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H +#define CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H + +#include <vector> + +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/strings/type_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +/** + * Simple regular expression enumerator, generates only singleton language + * regular expressions from a string enumeration, in other words: + * (str.to_re s1) ... (str.to_re sn) .... + * where s1 ... sn ... is the enumeration for strings. + */ +class RegExpEnumerator : public TypeEnumeratorBase<RegExpEnumerator> +{ + public: + RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr); + RegExpEnumerator(const RegExpEnumerator& enumerator); + ~RegExpEnumerator() {} + /** get the current term */ + Node operator*() override; + /** increment */ + RegExpEnumerator& operator++() override; + /** is this enumerator finished? */ + bool isFinished() override; + + private: + /** underlying string enumerator */ + StringEnumerator d_senum; +}; + +} // namespace strings +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H */ |