Support indexed operators re.loop and re.^ (#4167)

Towards support for the strings standard.

This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices).

This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions.

Also fixes #4161.

4 files changed, 146 insertions, 0 deletions

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 6895dc01a..eba5fb8c9 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -29,6 +29,8 @@ libcvc4_add_sources(
   resource_manager.h
   result.cpp
   result.h
+  regexp.cpp
+  regexp.h
   safe_print.cpp
   safe_print.h
   sampler.cpp
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
new file mode 100644
index 000000000..ca6547134
--- /dev/null
+++ b/src/util/regexp.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file regexp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Implementation of data structures for regular expression operators.
+ **/
+
+#include "util/regexp.h"
+
+#include <ostream>
+
+namespace CVC4 {
+
+RegExpRepeat::RegExpRepeat(uint32_t repeatAmount) : d_repeatAmount(repeatAmount) {}
+
+bool RegExpRepeat::operator==(const RegExpRepeat& r) const
+{
+  return d_repeatAmount == r.d_repeatAmount;
+}
+
+RegExpLoop::RegExpLoop(uint32_t l, uint32_t h) : d_loopMinOcc(l), d_loopMaxOcc(h) {}
+
+bool RegExpLoop::operator==(const RegExpLoop& r) const
+{
+  return d_loopMinOcc == r.d_loopMinOcc
+          && d_loopMaxOcc == r.d_loopMaxOcc;
+}
+  
+size_t RegExpRepeatHashFunction::operator()(const RegExpRepeat& r) const
+{
+  return r.d_repeatAmount;
+}
+
+size_t RegExpLoopHashFunction::operator()(const RegExpLoop& r) const
+{
+  return r.d_loopMinOcc + r.d_loopMaxOcc;
+}
+
+std::ostream& operator<<(std::ostream& os, const RegExpRepeat& r)
+{
+  return os << r.d_repeatAmount;
+}
+
+std::ostream& operator<<(std::ostream& os, const RegExpLoop& r)
+{
+  return os << "[" << r.d_loopMinOcc << ".." << r.d_loopMaxOcc << "]";
+}
+
+}  // namespace CVC4
+
diff --git a/src/util/regexp.h b/src/util/regexp.h
new file mode 100644
index 000000000..aaba9e4db
--- /dev/null
+++ b/src/util/regexp.h
@@ -0,0 +1,75 @@
+/*********************                                                        */
+/*! \file regexp.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Data structures for regular expression operators.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__UTIL__REGEXP_H
+#define CVC4__UTIL__REGEXP_H
+
+#include <cstdint>
+#include <iosfwd>
+
+namespace CVC4 {
+
+struct CVC4_PUBLIC RegExpRepeat
+{
+  RegExpRepeat(uint32_t repeatAmount);
+
+  bool operator==(const RegExpRepeat& r) const;
+  /** The amount of repetitions of the regular expression */
+  uint32_t d_repeatAmount;
+};
+
+struct CVC4_PUBLIC RegExpLoop
+{
+  RegExpLoop(uint32_t l, uint32_t h);
+
+  bool operator==(const RegExpLoop& r) const;
+  /** The minimum number of repetitions of the regular expression */
+  uint32_t d_loopMinOcc;
+  /** The maximum number of repetitions of the regular expression */
+  uint32_t d_loopMaxOcc;
+};
+
+/* -----------------------------------------------------------------------
+ ** Hash Function structs
+ * ----------------------------------------------------------------------- */
+
+/*
+ * Hash function for the RegExpRepeat constants.
+ */
+struct CVC4_PUBLIC RegExpRepeatHashFunction
+{
+  size_t operator()(const RegExpRepeat& r) const;
+};
+
+/**
+ * Hash function for the RegExpLoop objects.
+ */
+struct CVC4_PUBLIC RegExpLoopHashFunction
+{
+  size_t operator()(const RegExpLoop& r) const;
+};
+
+/* -----------------------------------------------------------------------
+ ** Output stream
+ * ----------------------------------------------------------------------- */
+
+std::ostream& operator<<(std::ostream& os, const RegExpRepeat& bv) CVC4_PUBLIC;
+
+std::ostream& operator<<(std::ostream& os, const RegExpLoop& bv) CVC4_PUBLIC;
+
+}  // namespace CVC4
+
+#endif /* CVC4__UTIL__REGEXP_H */
diff --git a/src/util/regexp.i b/src/util/regexp.i
new file mode 100644
index 000000000..775e778f7
--- /dev/null
+++ b/src/util/regexp.i
@@ -0,0 +1,12 @@
+%{
+#include "util/regexp.h"
+%}
+
+%rename(equals) CVC4::RegExpRepeat::operator==(const RegExpRepeat&) const;
+
+%rename(equals) CVC4::RegExpLoop::operator==(const RegExpLoop&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const RegExpRepeat&);
+%ignore CVC4::operator<<(std::ostream&, const RegExpLoop&);
+
+%include "util/regexp.h"