From 4b7fc20dcce9eefdf568937f5e2c54141c4f5c5b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 27 Mar 2020 14:04:44 -0500 Subject: [PATCH] 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. --- src/CMakeLists.txt | 2 +- src/cvc4.i | 2 +- src/theory/evaluator.h | 2 +- src/theory/strings/kinds | 10 +++++----- src/theory/strings/regexp_operation.h | 3 +-- src/theory/strings/regexp_solver.h | 2 +- src/theory/strings/type_enumerator.cpp | 2 +- src/theory/strings/word.cpp | 2 +- src/util/CMakeLists.txt | 4 ++-- src/util/{regexp.cpp => string.cpp} | 9 +++------ src/util/{regexp.h => string.h} | 13 +++++-------- src/util/{regexp.i => string.i} | 4 ++-- .../unit/theory/theory_strings_skolem_cache_black.h | 2 +- 13 files changed, 25 insertions(+), 32 deletions(-) rename src/util/{regexp.cpp => string.cpp} (98%) rename src/util/{regexp.h => string.h} (97%) rename src/util/{regexp.i => string.i} (94%) 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 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() )" \ - "util/regexp.h" \ + "NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector() )" \ + "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 #include #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 similarity index 98% rename from src/util/regexp.cpp rename to 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 #include diff --git a/src/util/regexp.h b/src/util/string.h similarity index 97% rename from src/util/regexp.h rename to 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 #include @@ -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 similarity index 94% rename from src/util/regexp.i rename to 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; -- 2.30.2