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.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 374c577261a5c6eff8a0330b984278ca15a94da2..cde739454c74764f1c25d76189008fba3001ed0f 100644 (file)
--- 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 aa95ef2f8213ded5ac12f0abaacd2278d854d512..9faa935e1634810a4a260ab020d1ed4dabc8dd57 100644 (file)
--- 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 (file)
index 0000000..261d000
--- /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 (file)
index 0000000..289c8b0
--- /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 */