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.

1 files changed, 75 insertions, 0 deletions

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 */