Rename namespace CVC5 to cvc5. (#6258)

1 files changed, 13 insertions, 13 deletions

diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index 94c740742..cc4027aad 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -19,9 +19,9 @@
 #include "theory/strings/word.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace strings {
 
@@ -105,7 +105,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
         else if (xc.isConst())
         {
           // check for constants
-          CVC5::String s = xc.getConst<String>();
+          cvc5::String s = xc.getConst<String>();
           if (Word::isEmpty(xc))
           {
             Trace("regexp-ext-rewrite-debug") << "- ignore empty" << std::endl;
@@ -117,7 +117,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
           {
             std::vector<unsigned> ssVec;
             ssVec.push_back(t == 0 ? s.back() : s.front());
-            CVC5::String ss(ssVec);
+            cvc5::String ss(ssVec);
             if (testConstStringInRegExp(ss, 0, rc))
             {
               // strip off one character
@@ -345,7 +345,7 @@ bool RegExpEntail::isConstRegExp(TNode t)
   return true;
 }
 
-bool RegExpEntail::testConstStringInRegExp(CVC5::String& s,
+bool RegExpEntail::testConstStringInRegExp(cvc5::String& s,
                                            unsigned index_start,
                                            TNode r)
 {
@@ -358,7 +358,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC5::String& s,
   {
     case STRING_TO_REGEXP:
     {
-      CVC5::String s2 = s.substr(index_start, s.size() - index_start);
+      cvc5::String s2 = s.substr(index_start, s.size() - index_start);
       if (r[0].isConst())
       {
         return (s2 == r[0].getConst<String>());
@@ -392,7 +392,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC5::String& s,
           {
             for (vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i])
             {
-              CVC5::String t = s.substr(index_start + start, vec_k[i]);
+              cvc5::String t = s.substr(index_start + start, vec_k[i]);
               if (testConstStringInRegExp(t, 0, r[i]))
               {
                 start += vec_k[i];
@@ -457,7 +457,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC5::String& s,
       {
         for (unsigned i = s.size() - index_start; i > 0; --i)
         {
-          CVC5::String t = s.substr(index_start, i);
+          cvc5::String t = s.substr(index_start, i);
           if (testConstStringInRegExp(t, 0, r[0]))
           {
             if (index_start + i == s.size()
@@ -525,7 +525,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC5::String& s,
           uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
           for (unsigned len = s.size() - index_start; len >= 1; len--)
           {
-            CVC5::String t = s.substr(index_start, len);
+            cvc5::String t = s.substr(index_start, len);
             if (testConstStringInRegExp(t, 0, r[0]))
             {
               if (len + index_start == s.size())
@@ -534,7 +534,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC5::String& s,
               }
               else
               {
-                Node num2 = nm->mkConst(CVC5::Rational(u - 1));
+                Node num2 = nm->mkConst(cvc5::Rational(u - 1));
                 Node r2 = nm->mkNode(REGEXP_LOOP, r[0], r[1], num2);
                 if (testConstStringInRegExp(s, index_start + len, r2))
                 {
@@ -563,10 +563,10 @@ bool RegExpEntail::testConstStringInRegExp(CVC5::String& s,
           }
           for (unsigned len = 1; len <= s.size() - index_start; len++)
           {
-            CVC5::String t = s.substr(index_start, len);
+            cvc5::String t = s.substr(index_start, len);
             if (testConstStringInRegExp(t, 0, r[0]))
             {
-              Node num2 = nm->mkConst(CVC5::Rational(l - 1));
+              Node num2 = nm->mkConst(cvc5::Rational(l - 1));
               Node r2 = nm->mkNode(REGEXP_LOOP, r[0], num2, num2);
               if (testConstStringInRegExp(s, index_start + len, r2))
               {
@@ -761,4 +761,4 @@ bool RegExpEntail::regExpIncludes(Node r1, Node r2)
 
 }  // namespace strings
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5