Move string utility file (#4164)

Moves the string file to string.h. This is required since other required utilities will soon need to be added to regexp.h.

13 files changed, 25 insertions, 32 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index dd58c74ee..809b00b04 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -961,11 +961,11 @@ install(FILES
           util/proof.h
           util/rational_cln_imp.h
           util/rational_gmp_imp.h
-          util/regexp.h
           util/resource_manager.h
           util/result.h
           util/sexpr.h
           util/statistics.h
+          util/string.h
           util/tuple.h
           util/unsafe_interrupt_exception.h
           ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h
diff --git a/src/cvc4.i b/src/cvc4.i
index f9f8f5743..9dcff7f8e 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -274,10 +274,10 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/cardinality.i"
 %include "util/hash.i"
 %include "util/proof.i"
-%include "util/regexp.i"
 %include "util/result.i"
 %include "util/sexpr.i"
 %include "util/statistics.i"
+%include "util/string.i"
 %include "util/tuple.i"
 %include "util/unsafe_interrupt_exception.i"
 
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index 58e179fbe..b9b15c6c6 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -27,7 +27,7 @@
 #include "expr/node.h"
 #include "util/bitvector.h"
 #include "util/rational.h"
-#include "util/regexp.h"
+#include "util/string.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 5b988061b..3f7abdb7c 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -37,15 +37,15 @@ operator STRING_REV 1 "string reverse"
 sort STRING_TYPE \
     Cardinality::INTEGERS \
     well-founded \
-        "NodeManager::currentNM()->mkConst(::CVC4::String())" \
-        "util/regexp.h" \
+    "NodeManager::currentNM()->mkConst(::CVC4::String())" \
+    "util/string.h" \
     "String type"
 
 sort REGEXP_TYPE \
     Cardinality::INTEGERS \
     well-founded \
-        "NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \
-        "util/regexp.h" \
+    "NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \
+    "util/string.h" \
     "RegExp type"
 
 enumerator STRING_TYPE \
@@ -55,7 +55,7 @@ enumerator STRING_TYPE \
 constant CONST_STRING \
     ::CVC4::String \
     ::CVC4::strings::StringHashFunction \
-    "util/regexp.h" \
+    "util/string.h" \
     "a string of characters"
 
 # equal equal / less than / output
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index b9dbedba5..7845b2e00 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -24,10 +24,9 @@
 #include <algorithm>
 #include <climits>
 #include "util/hash.h"
-#include "util/regexp.h"
+#include "util/string.h"
 #include "theory/theory.h"
 #include "theory/rewriter.h"
-//#include "context/cdhashmap.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index 4880af905..d18604752 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -27,7 +27,7 @@
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/solver_state.h"
-#include "util/regexp.h"
+#include "util/string.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index 7352ae5de..d24206860 100644
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -15,7 +15,7 @@
 #include "theory/strings/type_enumerator.h"
 
 #include "theory/strings/theory_strings_utils.h"
-#include "util/regexp.h"
+#include "util/string.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index dd573b68c..0faeffd99 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/strings/word.h"
 
-#include "util/regexp.h"
+#include "util/string.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 75597edac..6895dc01a 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -25,8 +25,6 @@ libcvc4_add_sources(
   proof.h
   random.cpp
   random.h
-  regexp.cpp
-  regexp.h
   resource_manager.cpp
   resource_manager.h
   result.cpp
@@ -43,6 +41,8 @@ libcvc4_add_sources(
   statistics.h
   statistics_registry.cpp
   statistics_registry.h
+  string.cpp
+  string.h
   tuple.h
   unsafe_interrupt_exception.h
   utility.cpp
diff --git a/src/util/regexp.cpp b/src/util/string.cpp
index 36ba7182b..ff522ba7b 100644
--- a/src/util/regexp.cpp
+++ b/src/util/string.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file regexp.cpp
+/*! \file string.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Tim King, Tianyi Liang, Andrew Reynolds
@@ -9,13 +9,10 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** \brief Implementation of the string data type.
  **/
 
-#include "util/regexp.h"
+#include "util/string.h"
 
 #include <algorithm>
 #include <climits>
diff --git a/src/util/regexp.h b/src/util/string.h
index 56fb969a3..032105812 100644
--- a/src/util/regexp.h
+++ b/src/util/string.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file regexp.h
+/*! \file string.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Tianyi Liang
@@ -9,16 +9,13 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** \brief The string data type.
  **/
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__REGEXP_H
-#define CVC4__REGEXP_H
+#ifndef CVC4__UTIL__STRING_H
+#define CVC4__UTIL__STRING_H
 
 #include <cstddef>
 #include <functional>
@@ -271,4 +268,4 @@ std::ostream& operator<<(std::ostream& os, const String& s) CVC4_PUBLIC;
 
 }  // namespace CVC4
 
-#endif /* CVC4__REGEXP_H */
+#endif /* CVC4__UTIL__STRING_H */
diff --git a/src/util/regexp.i b/src/util/string.i
index afc51abd7..1ded901aa 100644
--- a/src/util/regexp.i
+++ b/src/util/string.i
@@ -1,5 +1,5 @@
 %{
-#include "util/regexp.h"
+#include "util/string.h"
 %}
 
 %rename(CVC4String) String;
@@ -21,5 +21,5 @@
 %ignore CVC4::operator<<(std::ostream&, const String&);
 
 %apply int &OUTPUT { int &c };
-%include "util/regexp.h"
+%include "util/string.h"
 %clear int &c;
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
index 34e8d88c6..e1b84492c 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ b/test/unit/theory/theory_strings_skolem_cache_black.h
@@ -20,7 +20,7 @@
 #include "expr/node_manager.h"
 #include "theory/strings/skolem_cache.h"
 #include "util/rational.h"
-#include "util/regexp.h"
+#include "util/string.h"
 
 using namespace CVC4;
 using namespace CVC4::theory::strings;