regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609)

This renames kinds REGEXP_EMPTY to REGEXP_NONE and REGEXP_SIGMA to
REGEXP_ALLCHAR to match their SMT-LIB representation (re.none,
re.allchar). It further renames api::Solver::mkRegexpEmpty() to
mkRegexpNone and api::Solver::mkRegexpSigma to mkRegexpAllchar.

22 files changed, 134 insertions, 124 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 9684c29c5..797d2e473 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -349,8 +349,8 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {REGEXP_RANGE, cvc5::Kind::REGEXP_RANGE},
     {REGEXP_REPEAT, cvc5::Kind::REGEXP_REPEAT},
     {REGEXP_LOOP, cvc5::Kind::REGEXP_LOOP},
-    {REGEXP_EMPTY, cvc5::Kind::REGEXP_EMPTY},
-    {REGEXP_SIGMA, cvc5::Kind::REGEXP_SIGMA},
+    {REGEXP_NONE, cvc5::Kind::REGEXP_NONE},
+    {REGEXP_ALLCHAR, cvc5::Kind::REGEXP_ALLCHAR},
     {REGEXP_COMPLEMENT, cvc5::Kind::REGEXP_COMPLEMENT},
     // maps to the same kind as the string versions
     {SEQ_CONCAT, cvc5::Kind::STRING_CONCAT},
@@ -661,8 +661,8 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT},
         {cvc5::Kind::REGEXP_LOOP, REGEXP_LOOP},
         {cvc5::Kind::REGEXP_LOOP_OP, REGEXP_LOOP},
-        {cvc5::Kind::REGEXP_EMPTY, REGEXP_EMPTY},
-        {cvc5::Kind::REGEXP_SIGMA, REGEXP_SIGMA},
+        {cvc5::Kind::REGEXP_NONE, REGEXP_NONE},
+        {cvc5::Kind::REGEXP_ALLCHAR, REGEXP_ALLCHAR},
         {cvc5::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT},
         {cvc5::Kind::CONST_SEQUENCE, CONST_SEQUENCE},
         {cvc5::Kind::SEQ_UNIT, SEQ_UNIT},
@@ -5103,14 +5103,14 @@ Sort Solver::mkTupleSortHelper(const std::vector<Sort>& sorts) const
 
 Term Solver::mkTermFromKind(Kind kind) const
 {
-  CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY
-                                   || kind == REGEXP_SIGMA || kind == SEP_EMP,
+  CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_NONE
+                                   || kind == REGEXP_ALLCHAR || kind == SEP_EMP,
                                kind)
-      << "PI, REGEXP_EMPTY, REGEXP_SIGMA or SEP_EMP";
+      << "PI, REGEXP_NONE, REGEXP_ALLCHAR or SEP_EMP";
   //////// all checks before this line
   Node res;
   cvc5::Kind k = extToIntKind(kind);
-  if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
+  if (kind == REGEXP_NONE || kind == REGEXP_ALLCHAR)
   {
     Assert(isDefinedIntKind(k));
     res = d_nodeMgr->mkNode(k, std::vector<Node>());
@@ -5796,24 +5796,24 @@ Term Solver::mkReal(int64_t num, int64_t den) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkRegexpEmpty() const
+Term Solver::mkRegexpNone() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   Node res =
-      d_nodeMgr->mkNode(cvc5::kind::REGEXP_EMPTY, std::vector<cvc5::Node>());
+      d_nodeMgr->mkNode(cvc5::kind::REGEXP_NONE, std::vector<cvc5::Node>());
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkRegexpSigma() const
+Term Solver::mkRegexpAllchar() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   Node res =
-      d_nodeMgr->mkNode(cvc5::kind::REGEXP_SIGMA, std::vector<cvc5::Node>());
+      d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALLCHAR, std::vector<cvc5::Node>());
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
   ////////
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 1ecf8715b..5b0cc0b45 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3443,16 +3443,16 @@ class CVC5_EXPORT Solver
   Term mkReal(int64_t num, int64_t den) const;
 
   /**
-   * Create a regular expression empty term.
+   * Create a regular expression none (re.none) term.
    * @return the empty term
    */
-  Term mkRegexpEmpty() const;
+  Term mkRegexpNone() const;
 
   /**
-   * Create a regular expression sigma term.
+   * Create a regular expression allchar (re.allchar) term.
    * @return the sigma term
    */
-  Term mkRegexpSigma() const;
+  Term mkRegexpAllchar() const;
 
   /**
    * Create a constant representing an empty set of the given sort.
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 57941aa5f..162ec24e7 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -3016,25 +3016,25 @@ enum Kind : int32_t
    */
   REGEXP_LOOP,
   /**
-   * Regexp empty.
+   * Regexp none.
    *
    * Parameters: none
    *
    * Create with:
-   *   - `Solver::mkRegexpEmpty() const`
+   *   - `Solver::mkRegexpNone() const`
    *   - `Solver::mkTerm(Kind kind) const`
    */
-  REGEXP_EMPTY,
+  REGEXP_NONE,
   /**
    * Regexp all characters.
    *
    * Parameters: none
    *
    * Create with:
-   *   - `Solver::mkRegexpSigma() const`
+   *   - `Solver::mkRegexpAllchar() const`
    *   - `Solver::mkTerm(Kind kind) const`
    */
-  REGEXP_SIGMA,
+  REGEXP_ALLCHAR,
   /**
    * Regexp complement.
    *
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 0479dce3d..09ad66f5b 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -854,25 +854,25 @@ public class Solver implements IPointer, AutoCloseable
    * Create a regular expression empty term.
    * @return the empty term
    */
-  public Term mkRegexpEmpty()
+  public Term mkRegexpNone()
   {
-    long termPointer = mkRegexpEmpty(pointer);
+    long termPointer = mkRegexpNone(pointer);
     return new Term(this, termPointer);
   }
 
-  private native long mkRegexpEmpty(long pointer);
+  private native long mkRegexpNone(long pointer);
 
   /**
    * Create a regular expression sigma term.
    * @return the sigma term
    */
-  public Term mkRegexpSigma()
+  public Term mkRegexpAllchar()
   {
-    long termPointer = mkRegexpSigma(pointer);
+    long termPointer = mkRegexpAllchar(pointer);
     return new Term(this, termPointer);
   }
 
-  private native long mkRegexpSigma(long pointer);
+  private native long mkRegexpAllchar(long pointer);
 
   /**
    * Create a constant representing an empty set of the given sort.
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index cb4d58591..a3ce49f4e 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -977,30 +977,30 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkReal__JJJ(
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkRegexpEmpty
+ * Method:    mkRegexpNone
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpEmpty(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpNone(
     JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->mkRegexpEmpty());
+  Term* retPointer = new Term(solver->mkRegexpNone());
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkRegexpSigma
+ * Method:    mkRegexpAllchar
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpSigma(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpAllchar(
     JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->mkRegexpSigma());
+  Term* retPointer = new Term(solver->mkRegexpAllchar());
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index a2c238985..baee5899e 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -215,8 +215,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkInteger(const uint64_t i) except +
         Term mkInteger(const string& s) except +
         Term mkReal(const string& s) except +
-        Term mkRegexpEmpty() except +
-        Term mkRegexpSigma() except +
+        Term mkRegexpNone() except +
+        Term mkRegexpAllchar() except +
         Term mkEmptySet(Sort s) except +
         Term mkEmptyBag(Sort s) except +
         Term mkSepEmp() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 05138e9bc..9e1aeaca1 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1130,22 +1130,22 @@ cdef class Solver:
             term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
         return term
 
-    def mkRegexpEmpty(self):
+    def mkRegexpNone(self):
         """Create a regular expression empty term.
 
         :return: the empty term
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkRegexpEmpty()
+        term.cterm = self.csolver.mkRegexpNone()
         return term
 
-    def mkRegexpSigma(self):
+    def mkRegexpAllchar(self):
         """Create a regular expression sigma term.
 
         :return: the sigma term
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkRegexpSigma()
+        term.cterm = self.csolver.mkRegexpAllchar()
         return term
 
     def mkEmptySet(self, Sort s):
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d0c607a4b..1208a0e03 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -394,7 +394,7 @@ class NodeManager
    * - We can avoid creating a temporary vector in some cases, e.g., when we
    *   want to create a node with a fixed, large number of children
    * - It makes sure that calls to `mkNode` that braced-init-lists work as
-   *   expected, e.g., mkNode(REGEXP_EMPTY, {}) will call this overload instead
+   *   expected, e.g., mkNode(REGEXP_NONE, {}) will call this overload instead
    *   of creating a node with a null node as a child.
    */
   Node mkNode(Kind kind, std::initializer_list<TNode> children);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b86c564d0..7add605c5 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -147,7 +147,7 @@ void Smt2::addDatatypesOperators()
 void Smt2::addStringOperators() {
   defineVar(
       "re.all",
-      getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma()));
+      getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpAllchar()));
   addOperator(api::STRING_CONCAT, "str.++");
   addOperator(api::STRING_LENGTH, "str.len");
   addOperator(api::STRING_SUBSTR, "str.substr");
@@ -636,8 +636,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     defineType("RegLan", d_solver->getRegExpSort(), true, true);
     defineType("Int", d_solver->getIntegerSort(), true, true);
 
-    defineVar("re.none", d_solver->mkRegexpEmpty());
-    defineVar("re.allchar", d_solver->mkRegexpSigma());
+    defineVar("re.none", d_solver->mkRegexpNone());
+    defineVar("re.allchar", d_solver->mkRegexpAllchar());
 
     // Boolean is a placeholder
     defineVar("seq.empty",
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 231390504..5d4387658 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1178,8 +1178,8 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::STRING_STOI: return "str.to_int";
   case kind::STRING_IN_REGEXP: return "str.in_re";
   case kind::STRING_TO_REGEXP: return "str.to_re";
-  case kind::REGEXP_EMPTY: return "re.none";
-  case kind::REGEXP_SIGMA: return "re.allchar";
+  case kind::REGEXP_NONE: return "re.none";
+  case kind::REGEXP_ALLCHAR: return "re.allchar";
   case kind::REGEXP_CONCAT: return "re.++";
   case kind::REGEXP_UNION: return "re.union";
   case kind::REGEXP_INTER: return "re.inter";
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 9faa935e1..d23e44cee 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -48,7 +48,7 @@ sort STRING_TYPE \
 sort REGEXP_TYPE \
     Cardinality::INTEGERS \
     well-founded \
-    "NodeManager::currentNM()->mkNode(REGEXP_EMPTY)" \
+    "NodeManager::currentNM()->mkNode(REGEXP_NONE)" \
     "util/string.h" \
     "RegExp type"
 
@@ -103,8 +103,8 @@ operator REGEXP_OPT 1 "regexp ?"
 operator REGEXP_RANGE 2 "regexp range"
 operator REGEXP_COMPLEMENT 1 "regexp complement"
 
-operator REGEXP_EMPTY 0 "regexp empty"
-operator REGEXP_SIGMA 0 "regexp all characters"
+operator REGEXP_NONE 0 "regexp empty"
+operator REGEXP_ALLCHAR 0 "regexp all characters"
 
 constant REGEXP_REPEAT_OP \
   struct \
@@ -143,8 +143,8 @@ typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp>"
 typerule REGEXP_COMPLEMENT "SimpleTypeRule<RRegExp, ARegExp>"
 typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>"
 typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
-typerule REGEXP_EMPTY "SimpleTypeRule<RRegExp>"
-typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>"
+typerule REGEXP_NONE "SimpleTypeRule<RRegExp>"
+typerule REGEXP_ALLCHAR "SimpleTypeRule<RRegExp>"
 
 ### operators that apply to both strings and sequences
 
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index b3dc309d5..d5b7606f2 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -121,7 +121,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
     if (fl.isNull())
     {
       if (!hasPivotIndex && c.getKind() == REGEXP_STAR
-          && c[0].getKind() == REGEXP_SIGMA)
+          && c[0].getKind() == REGEXP_ALLCHAR)
       {
         hasPivotIndex = true;
         pivotIndex = i;
@@ -167,7 +167,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
         // We do not need to include memberships of the form
         //   (str.substr x n 1) in re.allchar
         // since we know that by construction, n < len( x ).
-        if (re[i].getKind() != REGEXP_SIGMA)
+        if (re[i].getKind() != REGEXP_ALLCHAR)
         {
           Node currMem = nm->mkNode(STRING_IN_REGEXP, curr, re[i]);
           conc.push_back(currMem);
@@ -212,13 +212,13 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       gap_minsize.push_back(0);
       gap_exact.push_back(true);
     }
-    else if (c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_SIGMA)
+    else if (c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_ALLCHAR)
     {
       // found a gap of any size
       onlySigmasAndConsts = true;
       gap_exact[gap_exact.size() - 1] = false;
     }
-    else if (c.getKind() == REGEXP_SIGMA)
+    else if (c.getKind() == REGEXP_ALLCHAR)
     {
       // add one to the minimum size of the gap
       onlySigmasAndConsts = true;
@@ -565,7 +565,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
   for (const Node& r : disj)
   {
     Assert(r.getKind() != REGEXP_UNION);
-    Assert(r.getKind() != REGEXP_SIGMA);
+    Assert(r.getKind() != REGEXP_ALLCHAR);
     lenOnePeriod = false;
     // lenOnePeriod is true if this regular expression is a single character
     // regular expression
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index be1646403..530f34455 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -116,7 +116,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
             mchildren.pop_back();
             do_next = true;
           }
-          else if (rc.getKind() == REGEXP_RANGE || rc.getKind() == REGEXP_SIGMA)
+          else if (rc.getKind() == REGEXP_RANGE
+                   || rc.getKind() == REGEXP_ALLCHAR)
           {
             if (!isConstRegExp(rc))
             {
@@ -513,11 +514,11 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s,
         return true;
       }
     }
-    case REGEXP_EMPTY:
+    case REGEXP_NONE:
     {
       return false;
     }
-    case REGEXP_SIGMA:
+    case REGEXP_ALLCHAR:
     {
       if (s.size() == index_start + 1)
       {
@@ -654,7 +655,7 @@ Node RegExpEntail::getFixedLengthForRegexp(Node n)
       return ret;
     }
   }
-  else if (n.getKind() == REGEXP_SIGMA || n.getKind() == REGEXP_RANGE)
+  else if (n.getKind() == REGEXP_ALLCHAR || n.getKind() == REGEXP_RANGE)
   {
     return nm->mkConst(Rational(1));
   }
@@ -710,7 +711,7 @@ bool RegExpEntail::regExpIncludes(Node r1, Node r2)
     return false;
   }
   NodeManager* nm = NodeManager::currentNM();
-  Node sigma = nm->mkNode(REGEXP_SIGMA, std::vector<Node>{});
+  Node sigma = nm->mkNode(REGEXP_ALLCHAR, std::vector<Node>{});
   Node sigmaStar = nm->mkNode(REGEXP_STAR, sigma);
 
   std::vector<Node> v1, v2;
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 81ac75c84..fff512f98 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -35,11 +35,11 @@ RegExpOpr::RegExpOpr(Env& env, SkolemCache* sc)
     : EnvObj(env),
       d_true(NodeManager::currentNM()->mkConst(true)),
       d_false(NodeManager::currentNM()->mkConst(false)),
-      d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_EMPTY,
+      d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_NONE,
                                                      std::vector<Node>{})),
       d_zero(NodeManager::currentNM()->mkConst(::cvc5::Rational(0))),
       d_one(NodeManager::currentNM()->mkConst(::cvc5::Rational(1))),
-      d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA,
+      d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_ALLCHAR,
                                                std::vector<Node>{})),
       d_sigma_star(
           NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)),
@@ -84,7 +84,7 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r)
         d_constCache[cur] =
             tmp.isConst() ? RE_C_CONRETE_CONSTANT : RE_C_VARIABLE;
       }
-      else if (ck == REGEXP_SIGMA || ck == REGEXP_RANGE)
+      else if (ck == REGEXP_ALLCHAR || ck == REGEXP_RANGE)
       {
         d_constCache[cur] = RE_C_CONSTANT;
       }
@@ -136,8 +136,8 @@ int RegExpOpr::delta( Node r, Node &exp ) {
   Kind k = r.getKind();
   switch (k)
   {
-    case REGEXP_EMPTY:
-    case REGEXP_SIGMA:
+    case REGEXP_NONE:
+    case REGEXP_ALLCHAR:
     case REGEXP_RANGE:
     {
       // does not contain empty string
@@ -295,11 +295,13 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
     d_deriv_cache[dv] = p;
   } else {
     switch( r.getKind() ) {
-      case kind::REGEXP_EMPTY: {
+      case kind::REGEXP_NONE:
+      {
         ret = 2;
         break;
       }
-      case kind::REGEXP_SIGMA: {
+      case kind::REGEXP_ALLCHAR:
+      {
         retNode = d_emptySingleton;
         break;
       }
@@ -550,11 +552,13 @@ Node RegExpOpr::derivativeSingle(Node r, cvc5::String c)
   } else {
     Kind k = r.getKind();
     switch( k ) {
-      case kind::REGEXP_EMPTY: {
+      case kind::REGEXP_NONE:
+      {
         retNode = d_emptyRegexp;
         break;
       }
-      case kind::REGEXP_SIGMA: {
+      case kind::REGEXP_ALLCHAR:
+      {
         retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
         break;
       }
@@ -719,7 +723,8 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
     SetNodes vset;
     Kind k = r.getKind();
     switch( k ) {
-      case kind::REGEXP_EMPTY: {
+      case kind::REGEXP_NONE:
+      {
         break;
       }
       case kind::REGEXP_RANGE: {
@@ -792,7 +797,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
         firstChars(r[0], cset, vset);
         break;
       }
-      case kind::REGEXP_SIGMA:
+      case kind::REGEXP_ALLCHAR:
       case kind::REGEXP_COMPLEMENT:
       default: {
         // we do not expect to call this function on regular expressions that
@@ -1198,7 +1203,7 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
     r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr1);
     r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr2);
   }
-  else if (nk == STRING_TO_REGEXP || nk == REGEXP_SIGMA || nk == REGEXP_RANGE
+  else if (nk == STRING_TO_REGEXP || nk == REGEXP_ALLCHAR || nk == REGEXP_RANGE
            || nk == REGEXP_COMPLEMENT || nk == REGEXP_LOOP)
   {
     // this leaves n unchanged
@@ -1466,11 +1471,13 @@ std::string RegExpOpr::mkString( Node r ) {
   } else {
     int k = r.getKind();
     switch( k ) {
-      case kind::REGEXP_EMPTY: {
+      case kind::REGEXP_NONE:
+      {
         retStr += "\\E";
         break;
       }
-      case kind::REGEXP_SIGMA: {
+      case kind::REGEXP_ALLCHAR:
+      {
         retStr += ".";
         break;
       }
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 050ec594a..04de0ea44 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -52,7 +52,7 @@ RegExpSolver::RegExpSolver(Env& env,
       d_regexp_opr(env, tr.getSkolemCache())
 {
   d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::String(""));
-  d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY);
+  d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_NONE);
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
@@ -656,8 +656,8 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
   Node ret = r;
   switch (r.getKind())
   {
-    case REGEXP_EMPTY:
-    case REGEXP_SIGMA:
+    case REGEXP_NONE:
+    case REGEXP_ALLCHAR:
     case REGEXP_RANGE: break;
     case STRING_TO_REGEXP:
     {
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 783e258fa..babf260fc 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -789,10 +789,10 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node)
       changed = true;
       emptyRe = c;
     }
-    else if (c.getKind() == REGEXP_EMPTY)
+    else if (c.getKind() == REGEXP_NONE)
     {
       // re.++( ..., empty, ... ) ---> empty
-      Node ret = nm->mkNode(REGEXP_EMPTY);
+      Node ret = nm->mkNode(REGEXP_NONE);
       return returnRewrite(node, ret, Rewrite::RE_CONCAT_EMPTY);
     }
     else
@@ -868,7 +868,7 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node)
         {
           curr = Node::null();
         }
-        else if (curr[0].getKind() == REGEXP_SIGMA)
+        else if (curr[0].getKind() == REGEXP_ALLCHAR)
         {
           Assert(!lastAllStar);
           lastAllStar = true;
@@ -932,7 +932,7 @@ Node SequencesRewriter::rewriteStarRegExp(TNode node)
     // ("")* ---> ""
     return returnRewrite(node, node[0], Rewrite::RE_STAR_EMPTY_STRING);
   }
-  else if (node[0].getKind() == REGEXP_EMPTY)
+  else if (node[0].getKind() == REGEXP_NONE)
   {
     // (empty)* ---> ""
     retNode = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")));
@@ -992,7 +992,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
         }
       }
     }
-    else if (ni.getKind() == REGEXP_EMPTY)
+    else if (ni.getKind() == REGEXP_NONE)
     {
       if (nk == REGEXP_INTER)
       {
@@ -1000,7 +1000,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
       }
       // otherwise, can ignore
     }
-    else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_SIGMA)
+    else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_ALLCHAR)
     {
       if (nk == REGEXP_UNION)
       {
@@ -1032,11 +1032,11 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
         Node retNode;
         if (nk == REGEXP_INTER)
         {
-          retNode = nm->mkNode(kind::REGEXP_EMPTY);
+          retNode = nm->mkNode(kind::REGEXP_NONE);
         }
         else
         {
-          retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA));
+          retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR));
         }
         return returnRewrite(node, retNode, Rewrite::RE_ANDOR_INC_CONFLICT);
       }
@@ -1047,11 +1047,11 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
   {
     if (nk == REGEXP_INTER)
     {
-      retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA));
+      retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR));
     }
     else
     {
-      retNode = nm->mkNode(kind::REGEXP_EMPTY);
+      retNode = nm->mkNode(kind::REGEXP_NONE);
     }
   }
   else
@@ -1091,7 +1091,7 @@ Node SequencesRewriter::rewriteLoopRegExp(TNode node)
   if (u < l)
   {
     std::vector<Node> nvec;
-    retNode = nm->mkNode(REGEXP_EMPTY, nvec);
+    retNode = nm->mkNode(REGEXP_NONE, nvec);
   }
   else if (u == l)
   {
@@ -1184,7 +1184,7 @@ Node SequencesRewriter::rewriteRangeRegExp(TNode node)
   if (ch[0] > ch[1])
   {
     // re.range( "B", "A" ) ---> re.none
-    Node retNode = nm->mkNode(REGEXP_EMPTY);
+    Node retNode = nm->mkNode(REGEXP_NONE);
     return returnRewrite(node, retNode, Rewrite::RE_RANGE_EMPTY);
   }
   return node;
@@ -1199,7 +1199,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
   TypeNode stype = x.getType();
   TypeNode rtype = r.getType();
 
-  if(r.getKind() == kind::REGEXP_EMPTY) 
+  if (r.getKind() == kind::REGEXP_NONE)
   {
     Node retNode = NodeManager::currentNM()->mkConst(false);
     return returnRewrite(node, retNode, Rewrite::RE_IN_EMPTY);
@@ -1212,7 +1212,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
     Node retNode = NodeManager::currentNM()->mkConst(test);
     return returnRewrite(node, retNode, Rewrite::RE_IN_EVAL);
   }
-  else if (r.getKind() == kind::REGEXP_SIGMA)
+  else if (r.getKind() == kind::REGEXP_ALLCHAR)
   {
     Node one = nm->mkConst(Rational(1));
     Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x));
@@ -1260,7 +1260,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
         }
       }
     }
-    if (r[0].getKind() == kind::REGEXP_SIGMA)
+    if (r[0].getKind() == kind::REGEXP_ALLCHAR)
     {
       Node retNode = NodeManager::currentNM()->mkConst(true);
       return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA_STAR);
@@ -1277,12 +1277,12 @@ Node SequencesRewriter::rewriteMembership(TNode node)
     for (size_t i = 0; i < nchildren; i++)
     {
       Node rc = r[i];
-      Assert(rc.getKind() != kind::REGEXP_EMPTY);
-      if (rc.getKind() == kind::REGEXP_SIGMA)
+      Assert(rc.getKind() != kind::REGEXP_NONE);
+      if (rc.getKind() == kind::REGEXP_ALLCHAR)
       {
         allSigmaMinSize++;
       }
-      else if (rc.getKind() == REGEXP_STAR && rc[0].getKind() == REGEXP_SIGMA)
+      else if (rc.getKind() == REGEXP_STAR && rc[0].getKind() == REGEXP_ALLCHAR)
       {
         allSigmaStrict = false;
       }
@@ -3245,7 +3245,7 @@ std::pair<size_t, size_t> SequencesRewriter::firstMatch(Node n, Node r)
   Assert(r.getType().isRegExp());
   NodeManager* nm = NodeManager::currentNM();
 
-  Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA));
+  Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR));
   Node re = nm->mkNode(REGEXP_CONCAT, r, sigmaStar);
   String s = n.getConst<String>();
 
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 9ab65f6ec..59bb0755c 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -285,7 +285,7 @@ bool isConstantLike(Node n) { return n.isConst() || n.getKind() == SEQ_UNIT; }
 bool isUnboundedWildcard(const std::vector<Node>& rs, size_t start)
 {
   size_t i = start;
-  while (i < rs.size() && rs[i].getKind() == REGEXP_SIGMA)
+  while (i < rs.size() && rs[i].getKind() == REGEXP_ALLCHAR)
   {
     i++;
   }
@@ -295,7 +295,7 @@ bool isUnboundedWildcard(const std::vector<Node>& rs, size_t start)
     return false;
   }
 
-  return rs[i].getKind() == REGEXP_STAR && rs[i][0].getKind() == REGEXP_SIGMA;
+  return rs[i].getKind() == REGEXP_STAR && rs[i][0].getKind() == REGEXP_ALLCHAR;
 }
 
 bool isSimpleRegExp(Node r)
@@ -313,8 +313,9 @@ bool isSimpleRegExp(Node r)
         return false;
       }
     }
-    else if (n.getKind() != REGEXP_SIGMA
-             && (n.getKind() != REGEXP_STAR || n[0].getKind() != REGEXP_SIGMA))
+    else if (n.getKind() != REGEXP_ALLCHAR
+             && (n.getKind() != REGEXP_STAR
+                 || n[0].getKind() != REGEXP_ALLCHAR))
     {
       return false;
     }
@@ -376,7 +377,7 @@ bool isStringKind(Kind k)
 
 bool isRegExpKind(Kind k)
 {
-  return k == REGEXP_EMPTY || k == REGEXP_SIGMA || k == STRING_TO_REGEXP
+  return k == REGEXP_NONE || k == REGEXP_ALLCHAR || k == STRING_TO_REGEXP
          || k == REGEXP_CONCAT || k == REGEXP_UNION || k == REGEXP_INTER
          || k == REGEXP_STAR || k == REGEXP_PLUS || k == REGEXP_OPT
          || k == REGEXP_RANGE || k == REGEXP_LOOP || k == REGEXP_RV
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index c7398aa3b..71ab17465 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -646,13 +646,13 @@ def test_mk_real(solver):
 def test_mk_regexp_empty(solver):
     strSort = solver.getStringSort()
     s = solver.mkConst(strSort, "s")
-    solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpEmpty())
+    solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone())
 
 
 def test_mk_regexp_sigma(solver):
     strSort = solver.getStringSort()
     s = solver.mkConst(strSort, "s")
-    solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpSigma())
+    solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar())
 
 
 def test_mk_sep_emp(solver):
@@ -690,8 +690,8 @@ def test_mk_term(solver):
 
     # mkTerm(Kind kind) const
     solver.mkPi()
-    solver.mkTerm(kinds.RegexpEmpty)
-    solver.mkTerm(kinds.RegexpSigma)
+    solver.mkTerm(kinds.RegexpNone)
+    solver.mkTerm(kinds.RegexpAllchar)
     with pytest.raises(RuntimeError):
         solver.mkTerm(kinds.ConstBV)
 
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 2f134b6bf..161854421 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -632,18 +632,18 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkReal(val4, val4));
   }
 
-  @Test void mkRegexpEmpty()
+  @Test void mkRegexpNone()
   {
     Sort strSort = d_solver.getStringSort();
     Term s = d_solver.mkConst(strSort, "s");
-    assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+    assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone()));
   }
 
-  @Test void mkRegexpSigma()
+  @Test void mkRegexpAllchar()
   {
     Sort strSort = d_solver.getStringSort();
     Term s = d_solver.mkConst(strSort, "s");
-    assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+    assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar()));
   }
 
   @Test void mkSepEmp()
@@ -683,8 +683,8 @@ class SolverTest
 
     // mkTerm(Kind kind) const
     assertDoesNotThrow(() -> d_solver.mkTerm(PI));
-    assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_EMPTY));
-    assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_SIGMA));
+    assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_NONE));
+    assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_ALLCHAR));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(CONST_BITVECTOR));
 
     // mkTerm(Kind kind, Term child) const
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index ab47ae90b..79a4aa63e 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -592,20 +592,20 @@ TEST_F(TestApiBlackSolver, mkReal)
   ASSERT_NO_THROW(d_solver.mkReal(val4, val4));
 }
 
-TEST_F(TestApiBlackSolver, mkRegexpEmpty)
+TEST_F(TestApiBlackSolver, mkRegexpNone)
 {
   Sort strSort = d_solver.getStringSort();
   Term s = d_solver.mkConst(strSort, "s");
   ASSERT_NO_THROW(
-      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone()));
 }
 
-TEST_F(TestApiBlackSolver, mkRegexpSigma)
+TEST_F(TestApiBlackSolver, mkRegexpAllchar)
 {
   Sort strSort = d_solver.getStringSort();
   Term s = d_solver.mkConst(strSort, "s");
   ASSERT_NO_THROW(
-      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar()));
 }
 
 TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); }
@@ -643,8 +643,8 @@ TEST_F(TestApiBlackSolver, mkTerm)
 
   // mkTerm(Kind kind) const
   ASSERT_NO_THROW(d_solver.mkTerm(PI));
-  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_EMPTY));
-  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_SIGMA));
+  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE));
+  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR));
   ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC5ApiException);
 
   // mkTerm(Kind kind, Term child) const
diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp
index c6b921542..8d3a672f7 100644
--- a/test/unit/theory/regexp_operation_black.cpp
+++ b/test/unit/theory/regexp_operation_black.cpp
@@ -61,7 +61,7 @@ class TestTheoryBlackRegexpOperation : public TestSmt
 
 TEST_F(TestTheoryBlackRegexpOperation, basic)
 {
-  Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA);
+  Node sigma = d_nodeManager->mkNode(REGEXP_ALLCHAR);
   Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma);
   Node a = d_nodeManager->mkNode(STRING_TO_REGEXP,
                                  d_nodeManager->mkConst(String("a")));
@@ -88,7 +88,7 @@ TEST_F(TestTheoryBlackRegexpOperation, basic)
 
 TEST_F(TestTheoryBlackRegexpOperation, star_wildcards)
 {
-  Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA);
+  Node sigma = d_nodeManager->mkNode(REGEXP_ALLCHAR);
   Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma);
   Node a = d_nodeManager->mkNode(STRING_TO_REGEXP,
                                  d_nodeManager->mkConst(String("a")));
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index bcac315a7..165479b78 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -713,7 +713,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re)
 
   std::vector<Node> emptyVec;
   Node sigStar = d_nodeManager->mkNode(
-      kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec));
+      kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, emptyVec));
   Node foo = d_nodeManager->mkConst(String("FOO"));
   Node a = d_nodeManager->mkConst(String("A"));
   Node b = d_nodeManager->mkConst(String("B"));
@@ -833,7 +833,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all)
 
   std::vector<Node> emptyVec;
   Node sigStar = d_nodeManager->mkNode(
-      kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec));
+      kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, emptyVec));
   Node foo = d_nodeManager->mkConst(String("FOO"));
   Node a = d_nodeManager->mkConst(String("A"));
   Node b = d_nodeManager->mkConst(String("B"));
@@ -1796,7 +1796,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership)
     // (str.contains x "ABC")
     Node sig_star = d_nodeManager->mkNode(
         kind::REGEXP_STAR,
-        d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty));
+        d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, vec_empty));
     Node lhs = d_nodeManager->mkNode(
         kind::STRING_IN_REGEXP,
         x,
@@ -1814,7 +1814,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership)
     // (str.contains x "ABC")
     Node sig_star = d_nodeManager->mkNode(
         kind::REGEXP_STAR,
-        d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty));
+        d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, vec_empty));
     Node lhs = d_nodeManager->mkNode(
         kind::STRING_IN_REGEXP,
         x,
@@ -1832,7 +1832,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_regexp_concat)
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node allStar = d_nodeManager->mkNode(
-      kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyArgs));
+      kind::REGEXP_STAR,
+      d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, emptyArgs));
   Node xReg = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, x);
   Node yReg = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, y);