Enumeration for String rewrites (#4173)

In preparation for string proof infrastructure.

This introduces an enumeration type to track string rewrites.

It also makes inference printing more consistent.

8 files changed, 552 insertions, 161 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 760c3fba7..2ea305bc7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -684,6 +684,8 @@ libcvc4_add_sources(
   theory/strings/regexp_operation.h
   theory/strings/regexp_solver.cpp
   theory/strings/regexp_solver.h
+  theory/strings/rewrites.cpp
+  theory/strings/rewrites.h
   theory/strings/sequences_rewriter.cpp
   theory/strings/sequences_rewriter.h
   theory/strings/sequences_stats.cpp
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index cdf764aa8..3b4a6b857 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -22,18 +22,18 @@ const char* toString(Inference i)
 {
   switch (i)
   {
-    case Inference::N_ENDPOINT_EMP: return "N_EndpointEmp";
-    case Inference::N_UNIFY: return "N_Unify";
-    case Inference::N_ENDPOINT_EQ: return "N_EndpointEq";
-    case Inference::N_CONST: return "N_Const";
-    case Inference::INFER_EMP: return "Infer-Emp";
-    case Inference::SSPLIT_CST_PROP: return "S-Split(CST-P)-prop";
-    case Inference::SSPLIT_VAR_PROP: return "S-Split(VAR)-prop";
-    case Inference::LEN_SPLIT: return "Len-Split(Len)";
-    case Inference::LEN_SPLIT_EMP: return "Len-Split(Emp)";
-    case Inference::SSPLIT_CST: return "S-Split(CST-P)";
-    case Inference::SSPLIT_VAR: return "S-Split(VAR)";
-    case Inference::FLOOP: return "F-Loop";
+    case Inference::N_ENDPOINT_EMP: return "N_ENDPOINT_EMP";
+    case Inference::N_UNIFY: return "N_UNIFY";
+    case Inference::N_ENDPOINT_EQ: return "N_ENDPOINT_EQ";
+    case Inference::N_CONST: return "N_CONST";
+    case Inference::INFER_EMP: return "INFER_EMP";
+    case Inference::SSPLIT_CST_PROP: return "SSPLIT_CST_PROP";
+    case Inference::SSPLIT_VAR_PROP: return "SSPLIT_VAR_PROP";
+    case Inference::LEN_SPLIT: return "LEN_SPLIT";
+    case Inference::LEN_SPLIT_EMP: return "LEN_SPLIT_EMP";
+    case Inference::SSPLIT_CST: return "SSPLIT_CST";
+    case Inference::SSPLIT_VAR: return "SSPLIT_VAR";
+    case Inference::FLOOP: return "FLOOP";
     default: return "?";
   }
 }
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index cfabe5c51..e13a5a2ff 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -196,4 +196,4 @@ class InferInfo
 }  // namespace theory
 }  // namespace CVC4
 
-#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
+#endif /* CVC4__THEORY__STRINGS__INFER_INFO_H */
diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
new file mode 100644
index 000000000..5bc62b6e4
--- /dev/null
+++ b/src/theory/strings/rewrites.cpp
@@ -0,0 +1,185 @@
+/*********************                                                        */
+/*! \file rewrites.cpp
+ ** \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 Implementation of inference information utility.
+ **/
+
+#include "theory/strings/rewrites.h"
+
+#include <iostream>
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+const char* toString(Rewrite r)
+{
+  switch (r)
+  {
+    case Rewrite::CTN_COMPONENT: return "CTN_COMPONENT";
+    case Rewrite::CTN_CONCAT_CHAR: return "CTN_CONCAT_CHAR";
+    case Rewrite::CTN_CONST: return "CTN_CONST";
+    case Rewrite::CTN_EQ: return "CTN_EQ";
+    case Rewrite::CTN_LEN_INEQ: return "CTN_LEN_INEQ";
+    case Rewrite::CTN_LEN_INEQ_NSTRICT: return "CTN_LEN_INEQ_NSTRICT";
+    case Rewrite::CTN_LHS_EMPTYSTR: return "CTN_LHS_EMPTYSTR";
+    case Rewrite::CTN_MSET_NSS: return "CTN_MSET_NSS";
+    case Rewrite::CTN_NCONST_CTN_CONCAT: return "CTN_NCONST_CTN_CONCAT";
+    case Rewrite::CTN_REPL: return "CTN_REPL";
+    case Rewrite::CTN_REPL_CHAR: return "CTN_REPL_CHAR";
+    case Rewrite::CTN_REPL_CNSTS_TO_CTN: return "CTN_REPL_CNSTS_TO_CTN";
+    case Rewrite::CTN_REPL_EMPTY: return "CTN_REPL_EMPTY";
+    case Rewrite::CTN_REPL_LEN_ONE_TO_CTN: return "CTN_REPL_LEN_ONE_TO_CTN";
+    case Rewrite::CTN_REPL_SELF: return "CTN_REPL_SELF";
+    case Rewrite::CTN_REPL_SIMP_REPL: return "CTN_REPL_SIMP_REPL";
+    case Rewrite::CTN_REPL_TO_CTN: return "CTN_REPL_TO_CTN";
+    case Rewrite::CTN_REPL_TO_CTN_DISJ: return "CTN_REPL_TO_CTN_DISJ";
+    case Rewrite::CTN_RHS_EMPTYSTR: return "CTN_RHS_EMPTYSTR";
+    case Rewrite::CTN_RPL_NON_CTN: return "CTN_RPL_NON_CTN";
+    case Rewrite::CTN_SPLIT: return "CTN_SPLIT";
+    case Rewrite::CTN_SPLIT_ONES: return "CTN_SPLIT_ONES";
+    case Rewrite::CTN_STRIP_ENDPT: return "CTN_STRIP_ENDPT";
+    case Rewrite::CTN_SUBSTR: return "CTN_SUBSTR";
+    case Rewrite::EQ_LEN_DEQ: return "EQ_LEN_DEQ";
+    case Rewrite::EQ_NCTN: return "EQ_NCTN";
+    case Rewrite::EQ_NFIX: return "EQ_NFIX";
+    case Rewrite::FROM_CODE_EVAL: return "FROM_CODE_EVAL";
+    case Rewrite::IDOF_DEF_CTN: return "IDOF_DEF_CTN";
+    case Rewrite::IDOF_EMP_IDOF: return "IDOF_EMP_IDOF";
+    case Rewrite::IDOF_EQ_CST_START: return "IDOF_EQ_CST_START";
+    case Rewrite::IDOF_EQ_NORM: return "IDOF_EQ_NORM";
+    case Rewrite::IDOF_EQ_NSTART: return "IDOF_EQ_NSTART";
+    case Rewrite::IDOF_FIND: return "IDOF_FIND";
+    case Rewrite::IDOF_LEN: return "IDOF_LEN";
+    case Rewrite::IDOF_MAX: return "IDOF_MAX";
+    case Rewrite::IDOF_NCTN: return "IDOF_NCTN";
+    case Rewrite::IDOF_NEG: return "IDOF_NEG";
+    case Rewrite::IDOF_NFIND: return "IDOF_NFIND";
+    case Rewrite::IDOF_NORM_PREFIX: return "IDOF_NORM_PREFIX";
+    case Rewrite::IDOF_PULL_ENDPT: return "IDOF_PULL_ENDPT";
+    case Rewrite::IDOF_STRIP_CNST_ENDPTS: return "IDOF_STRIP_CNST_ENDPTS";
+    case Rewrite::IDOF_STRIP_SYM_LEN: return "IDOF_STRIP_SYM_LEN";
+    case Rewrite::ITOS_EVAL: return "ITOS_EVAL";
+    case Rewrite::RE_AND_EMPTY: return "RE_AND_EMPTY";
+    case Rewrite::RE_ANDOR_FLATTEN: return "RE_ANDOR_FLATTEN";
+    case Rewrite::RE_CHAR_IN_STR_STAR: return "RE_CHAR_IN_STR_STAR";
+    case Rewrite::RE_CONCAT: return "RE_CONCAT";
+    case Rewrite::RE_CONCAT_FLATTEN: return "RE_CONCAT_FLATTEN";
+    case Rewrite::RE_CONCAT_OPT: return "RE_CONCAT_OPT";
+    case Rewrite::RE_CONCAT_PURE_ALLCHAR: return "RE_CONCAT_PURE_ALLCHAR";
+    case Rewrite::RE_CONCAT_TO_CONTAINS: return "RE_CONCAT_TO_CONTAINS";
+    case Rewrite::RE_EMPTY_IN_STR_STAR: return "RE_EMPTY_IN_STR_STAR";
+    case Rewrite::RE_IN_DIST_CHAR_STAR: return "RE_IN_DIST_CHAR_STAR";
+    case Rewrite::RE_IN_SIGMA_STAR: return "RE_IN_SIGMA_STAR";
+    case Rewrite::RE_LOOP: return "RE_LOOP";
+    case Rewrite::RE_LOOP_STAR: return "RE_LOOP_STAR";
+    case Rewrite::RE_OR_ALL: return "RE_OR_ALL";
+    case Rewrite::RE_SIMPLE_CONSUME: return "RE_SIMPLE_CONSUME";
+    case Rewrite::RE_STAR_EMPTY: return "RE_STAR_EMPTY";
+    case Rewrite::RE_STAR_EMPTY_STRING: return "RE_STAR_EMPTY_STRING";
+    case Rewrite::RE_STAR_NESTED_STAR: return "RE_STAR_NESTED_STAR";
+    case Rewrite::RE_STAR_UNION: return "RE_STAR_UNION";
+    case Rewrite::REPL_CHAR_NCONTRIB_FIND: return "REPL_CHAR_NCONTRIB_FIND";
+    case Rewrite::REPL_DUAL_REPL_ITE: return "REPL_DUAL_REPL_ITE";
+    case Rewrite::REPL_REPL_SHORT_CIRCUIT: return "REPL_REPL_SHORT_CIRCUIT";
+    case Rewrite::REPL_REPL2_INV: return "REPL_REPL2_INV";
+    case Rewrite::REPL_REPL2_INV_ID: return "REPL_REPL2_INV_ID";
+    case Rewrite::REPL_REPL3_INV: return "REPL_REPL3_INV";
+    case Rewrite::REPL_REPL3_INV_ID: return "REPL_REPL3_INV_ID";
+    case Rewrite::REPL_SUBST_IDX: return "REPL_SUBST_IDX";
+    case Rewrite::REPLALL_CONST: return "REPLALL_CONST";
+    case Rewrite::REPLALL_EMPTY_FIND: return "REPLALL_EMPTY_FIND";
+    case Rewrite::RPL_CCTN: return "RPL_CCTN";
+    case Rewrite::RPL_CCTN_RPL: return "RPL_CCTN_RPL";
+    case Rewrite::RPL_CNTS_SUBSTS: return "RPL_CNTS_SUBSTS";
+    case Rewrite::RPL_CONST_FIND: return "RPL_CONST_FIND";
+    case Rewrite::RPL_CONST_NFIND: return "RPL_CONST_NFIND";
+    case Rewrite::RPL_EMP_CNTS_SUBSTS: return "RPL_EMP_CNTS_SUBSTS";
+    case Rewrite::RPL_ID: return "RPL_ID";
+    case Rewrite::RPL_NCTN: return "RPL_NCTN";
+    case Rewrite::RPL_PULL_ENDPT: return "RPL_PULL_ENDPT";
+    case Rewrite::RPL_REPLACE: return "RPL_REPLACE";
+    case Rewrite::RPL_RPL_EMPTY: return "RPL_RPL_EMPTY";
+    case Rewrite::RPL_RPL_LEN_ID: return "RPL_RPL_LEN_ID";
+    case Rewrite::RPL_X_Y_X_SIMP: return "RPL_X_Y_X_SIMP";
+    case Rewrite::SPLIT_EQ: return "SPLIT_EQ";
+    case Rewrite::SPLIT_EQ_STRIP_L: return "SPLIT_EQ_STRIP_L";
+    case Rewrite::SPLIT_EQ_STRIP_R: return "SPLIT_EQ_STRIP_R";
+    case Rewrite::SS_COMBINE: return "SS_COMBINE";
+    case Rewrite::SS_CONST_END_OOB: return "SS_CONST_END_OOB";
+    case Rewrite::SS_CONST_LEN_MAX_OOB: return "SS_CONST_LEN_MAX_OOB";
+    case Rewrite::SS_CONST_LEN_NON_POS: return "SS_CONST_LEN_NON_POS";
+    case Rewrite::SS_CONST_SS: return "SS_CONST_SS";
+    case Rewrite::SS_CONST_START_MAX_OOB: return "SS_CONST_START_MAX_OOB";
+    case Rewrite::SS_CONST_START_NEG: return "SS_CONST_START_NEG";
+    case Rewrite::SS_CONST_START_OOB: return "SS_CONST_START_OOB";
+    case Rewrite::SS_EMPTYSTR: return "SS_EMPTYSTR";
+    case Rewrite::SS_END_PT_NORM: return "SS_END_PT_NORM";
+    case Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S:
+      return "SS_GEQ_ZERO_START_ENTAILS_EMP_S";
+    case Rewrite::SS_LEN_INCLUDE: return "SS_LEN_INCLUDE";
+    case Rewrite::SS_LEN_NON_POS: return "SS_LEN_NON_POS";
+    case Rewrite::SS_LEN_ONE_Z_Z: return "SS_LEN_ONE_Z_Z";
+    case Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB:
+      return "SS_NON_ZERO_LEN_ENTAILS_OOB";
+    case Rewrite::SS_START_ENTAILS_ZERO_LEN: return "SS_START_ENTAILS_ZERO_LEN";
+    case Rewrite::SS_START_GEQ_LEN: return "SS_START_GEQ_LEN";
+    case Rewrite::SS_START_NEG: return "SS_START_NEG";
+    case Rewrite::SS_STRIP_END_PT: return "SS_STRIP_END_PT";
+    case Rewrite::SS_STRIP_START_PT: return "SS_STRIP_START_PT";
+    case Rewrite::STOI_CONCAT_NONNUM: return "STOI_CONCAT_NONNUM";
+    case Rewrite::STOI_EVAL: return "STOI_EVAL";
+    case Rewrite::STR_CONV_CONST: return "STR_CONV_CONST";
+    case Rewrite::STR_CONV_IDEM: return "STR_CONV_IDEM";
+    case Rewrite::STR_CONV_ITOS: return "STR_CONV_ITOS";
+    case Rewrite::STR_CONV_MINSCOPE_CONCAT: return "STR_CONV_MINSCOPE_CONCAT";
+    case Rewrite::STR_EMP_REPL_EMP: return "STR_EMP_REPL_EMP";
+    case Rewrite::STR_EMP_REPL_EMP_R: return "STR_EMP_REPL_EMP_R";
+    case Rewrite::STR_EMP_REPL_X_Y_X: return "STR_EMP_REPL_X_Y_X";
+    case Rewrite::STR_EMP_SUBSTR_ELIM: return "STR_EMP_SUBSTR_ELIM";
+    case Rewrite::STR_EMP_SUBSTR_LEQ_LEN: return "STR_EMP_SUBSTR_LEQ_LEN";
+    case Rewrite::STR_EMP_SUBSTR_LEQ_Z: return "STR_EMP_SUBSTR_LEQ_Z";
+    case Rewrite::STR_EQ_CONJ_LEN_ENTAIL: return "STR_EQ_CONJ_LEN_ENTAIL";
+    case Rewrite::STR_EQ_CONST_NHOMOG: return "STR_EQ_CONST_NHOMOG";
+    case Rewrite::STR_EQ_HOMOG_CONST: return "STR_EQ_HOMOG_CONST";
+    case Rewrite::STR_EQ_REPL_EMP: return "STR_EQ_REPL_EMP";
+    case Rewrite::STR_EQ_REPL_NOT_CTN: return "STR_EQ_REPL_NOT_CTN";
+    case Rewrite::STR_EQ_REPL_TO_DIS: return "STR_EQ_REPL_TO_DIS";
+    case Rewrite::STR_EQ_REPL_TO_EQ: return "STR_EQ_REPL_TO_EQ";
+    case Rewrite::STR_EQ_UNIFY: return "STR_EQ_UNIFY";
+    case Rewrite::STR_LEQ_CPREFIX: return "STR_LEQ_CPREFIX";
+    case Rewrite::STR_LEQ_EMPTY: return "STR_LEQ_EMPTY";
+    case Rewrite::STR_LEQ_EVAL: return "STR_LEQ_EVAL";
+    case Rewrite::STR_LEQ_ID: return "STR_LEQ_ID";
+    case Rewrite::STR_REV_CONST: return "STR_REV_CONST";
+    case Rewrite::STR_REV_IDEM: return "STR_REV_IDEM";
+    case Rewrite::STR_REV_MINSCOPE_CONCAT: return "STR_REV_MINSCOPE_CONCAT";
+    case Rewrite::SUBSTR_REPL_SWAP: return "SUBSTR_REPL_SWAP";
+    case Rewrite::SUF_PREFIX_CONST: return "SUF_PREFIX_CONST";
+    case Rewrite::SUF_PREFIX_CTN: return "SUF_PREFIX_CTN";
+    case Rewrite::SUF_PREFIX_EMPTY: return "SUF_PREFIX_EMPTY";
+    case Rewrite::SUF_PREFIX_EMPTY_CONST: return "SUF_PREFIX_EMPTY_CONST";
+    case Rewrite::SUF_PREFIX_EQ: return "SUF_PREFIX_EQ";
+    case Rewrite::SUF_PREFIX_TO_EQS: return "SUF_PREFIX_TO_EQS";
+    case Rewrite::TO_CODE_EVAL: return "TO_CODE_EVAL";
+    default: return "?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, Rewrite r)
+{
+  out << toString(r);
+  return out;
+}
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
new file mode 100644
index 000000000..91d52197c
--- /dev/null
+++ b/src/theory/strings/rewrites.h
@@ -0,0 +1,202 @@
+/*********************                                                        */
+/*! \file rewrites.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 Type for rewrites for strings.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__REWRITES_H
+#define CVC4__THEORY__STRINGS__REWRITES_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+/** Types of rewrites used by strings
+ *
+ * This rewrites are documented where they are used in the rewriter.
+ */
+enum class Rewrite : uint32_t
+{
+  CTN_COMPONENT,
+  CTN_CONCAT_CHAR,
+  CTN_CONST,
+  CTN_EQ,
+  CTN_LEN_INEQ,
+  CTN_LEN_INEQ_NSTRICT,
+  CTN_LHS_EMPTYSTR,
+  CTN_MSET_NSS,
+  CTN_NCONST_CTN_CONCAT,
+  CTN_REPL,
+  CTN_REPL_CHAR,
+  CTN_REPL_CNSTS_TO_CTN,
+  CTN_REPL_EMPTY,
+  CTN_REPL_LEN_ONE_TO_CTN,
+  CTN_REPL_SELF,
+  CTN_REPL_SIMP_REPL,
+  CTN_REPL_TO_CTN,
+  CTN_REPL_TO_CTN_DISJ,
+  CTN_RHS_EMPTYSTR,
+  CTN_RPL_NON_CTN,
+  CTN_SPLIT,
+  CTN_SPLIT_ONES,
+  CTN_STRIP_ENDPT,
+  CTN_SUBSTR,
+  EQ_LEN_DEQ,
+  EQ_NCTN,
+  EQ_NFIX,
+  FROM_CODE_EVAL,
+  IDOF_DEF_CTN,
+  IDOF_EMP_IDOF,
+  IDOF_EQ_CST_START,
+  IDOF_EQ_NORM,
+  IDOF_EQ_NSTART,
+  IDOF_FIND,
+  IDOF_LEN,
+  IDOF_MAX,
+  IDOF_NCTN,
+  IDOF_NEG,
+  IDOF_NFIND,
+  IDOF_NORM_PREFIX,
+  IDOF_PULL_ENDPT,
+  IDOF_STRIP_CNST_ENDPTS,
+  IDOF_STRIP_SYM_LEN,
+  ITOS_EVAL,
+  RE_AND_EMPTY,
+  RE_ANDOR_FLATTEN,
+  RE_CHAR_IN_STR_STAR,
+  RE_CONCAT,
+  RE_CONCAT_FLATTEN,
+  RE_CONCAT_OPT,
+  RE_CONCAT_PURE_ALLCHAR,
+  RE_CONCAT_TO_CONTAINS,
+  RE_EMPTY_IN_STR_STAR,
+  RE_IN_DIST_CHAR_STAR,
+  RE_IN_SIGMA_STAR,
+  RE_LOOP,
+  RE_LOOP_STAR,
+  RE_OR_ALL,
+  RE_SIMPLE_CONSUME,
+  RE_STAR_EMPTY,
+  RE_STAR_EMPTY_STRING,
+  RE_STAR_NESTED_STAR,
+  RE_STAR_UNION,
+  REPL_CHAR_NCONTRIB_FIND,
+  REPL_DUAL_REPL_ITE,
+  REPL_REPL_SHORT_CIRCUIT,
+  REPL_REPL2_INV,
+  REPL_REPL2_INV_ID,
+  REPL_REPL3_INV,
+  REPL_REPL3_INV_ID,
+  REPL_SUBST_IDX,
+  REPLALL_CONST,
+  REPLALL_EMPTY_FIND,
+  RPL_CCTN,
+  RPL_CCTN_RPL,
+  RPL_CNTS_SUBSTS,
+  RPL_CONST_FIND,
+  RPL_CONST_NFIND,
+  RPL_EMP_CNTS_SUBSTS,
+  RPL_ID,
+  RPL_NCTN,
+  RPL_PULL_ENDPT,
+  RPL_REPLACE,
+  RPL_RPL_EMPTY,
+  RPL_RPL_LEN_ID,
+  RPL_X_Y_X_SIMP,
+  SPLIT_EQ,
+  SPLIT_EQ_STRIP_L,
+  SPLIT_EQ_STRIP_R,
+  SS_COMBINE,
+  SS_CONST_END_OOB,
+  SS_CONST_LEN_MAX_OOB,
+  SS_CONST_LEN_NON_POS,
+  SS_CONST_SS,
+  SS_CONST_START_MAX_OOB,
+  SS_CONST_START_NEG,
+  SS_CONST_START_OOB,
+  SS_EMPTYSTR,
+  SS_END_PT_NORM,
+  SS_GEQ_ZERO_START_ENTAILS_EMP_S,
+  SS_LEN_INCLUDE,
+  SS_LEN_NON_POS,
+  SS_LEN_ONE_Z_Z,
+  SS_NON_ZERO_LEN_ENTAILS_OOB,
+  SS_START_ENTAILS_ZERO_LEN,
+  SS_START_GEQ_LEN,
+  SS_START_NEG,
+  SS_STRIP_END_PT,
+  SS_STRIP_START_PT,
+  STOI_CONCAT_NONNUM,
+  STOI_EVAL,
+  STR_CONV_CONST,
+  STR_CONV_IDEM,
+  STR_CONV_ITOS,
+  STR_CONV_MINSCOPE_CONCAT,
+  STR_EMP_REPL_EMP,
+  STR_EMP_REPL_EMP_R,
+  STR_EMP_REPL_X_Y_X,
+  STR_EMP_SUBSTR_ELIM,
+  STR_EMP_SUBSTR_LEQ_LEN,
+  STR_EMP_SUBSTR_LEQ_Z,
+  STR_EQ_CONJ_LEN_ENTAIL,
+  STR_EQ_CONST_NHOMOG,
+  STR_EQ_HOMOG_CONST,
+  STR_EQ_REPL_EMP,
+  STR_EQ_REPL_NOT_CTN,
+  STR_EQ_REPL_TO_DIS,
+  STR_EQ_REPL_TO_EQ,
+  STR_EQ_UNIFY,
+  STR_LEQ_CPREFIX,
+  STR_LEQ_EMPTY,
+  STR_LEQ_EVAL,
+  STR_LEQ_ID,
+  STR_REV_CONST,
+  STR_REV_IDEM,
+  STR_REV_MINSCOPE_CONCAT,
+  SUBSTR_REPL_SWAP,
+  SUF_PREFIX_CONST,
+  SUF_PREFIX_CTN,
+  SUF_PREFIX_EMPTY,
+  SUF_PREFIX_EMPTY_CONST,
+  SUF_PREFIX_EQ,
+  SUF_PREFIX_TO_EQS,
+  TO_CODE_EVAL
+};
+
+/**
+ * Converts an rewrite to a string. Note: This function is also used in
+ * `safe_print()`. Changing this functions name or signature will result in
+ * `safe_print()` printing "<unsupported>" instead of the proper strings for
+ * the enum values.
+ *
+ * @param r The rewrite
+ * @return The name of the rewrite
+ */
+const char* toString(Rewrite r);
+
+/**
+ * Writes an rewrite name to a stream.
+ *
+ * @param out The stream to write to
+ * @param r The rewrite to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, Rewrite r);
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__REWRITES_H */
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index b0940b7e1..861d99135 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -328,7 +328,7 @@ Node SequencesRewriter::rewriteEquality(Node node)
     {
       if (!ctn.getConst<bool>())
       {
-        return returnRewrite(node, ctn, "eq-nctn");
+        return returnRewrite(node, ctn, Rewrite::EQ_NCTN);
       }
       else
       {
@@ -347,7 +347,7 @@ Node SequencesRewriter::rewriteEquality(Node node)
   len_eq = Rewriter::rewrite(len_eq);
   if (len_eq.isConst() && !len_eq.getConst<bool>())
   {
-    return returnRewrite(node, len_eq, "eq-len-deq");
+    return returnRewrite(node, len_eq, Rewrite::EQ_LEN_DEQ);
   }
 
   std::vector<Node> c[2];
@@ -375,7 +375,7 @@ Node SequencesRewriter::rewriteEquality(Node node)
         if (!isSameFix)
         {
           Node ret = NodeManager::currentNM()->mkConst(false);
-          return returnRewrite(node, ret, "eq-nfix");
+          return returnRewrite(node, ret, Rewrite::EQ_NFIX);
         }
       }
       if (c[0][index1] != c[1][index2])
@@ -465,7 +465,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
     Node s1 = utils::mkConcat(c[0], stype);
     Node s2 = utils::mkConcat(c[1], stype);
     new_ret = s1.eqNode(s2);
-    node = returnRewrite(node, new_ret, "str-eq-unify");
+    node = returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY);
   }
 
   // ------- homogeneous constants
@@ -505,7 +505,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
                 // this conflict just in case.
                 new_ret = nm->mkConst(false);
                 return returnRewrite(
-                    node, new_ret, "string-eq-const-conflict-non-homog");
+                    node, new_ret, Rewrite::STR_EQ_CONST_NHOMOG);
               }
               numHChars[j]++;
             }
@@ -540,7 +540,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
         //  "AA" = y ++ x ---> "AA" = x ++ y if x < y
         //  "AAA" = y ++ "A" ++ z ---> "AA" = y ++ z
         new_ret = lhs.eqNode(ss);
-        node = returnRewrite(node, new_ret, "str-eq-homog-const");
+        node = returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST);
       }
     }
   }
@@ -558,7 +558,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
         if (ne[0] == ne[2])
         {
           Node ret = nm->mkNode(EQUAL, ne[0], empty);
-          return returnRewrite(node, ret, "str-emp-repl-x-y-x");
+          return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_X_Y_X);
         }
 
         // (= "" (str.replace x y "A")) ---> (and (= x "") (not (= y "")))
@@ -568,14 +568,14 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
               nm->mkNode(AND,
                          nm->mkNode(EQUAL, ne[0], empty),
                          nm->mkNode(NOT, nm->mkNode(EQUAL, ne[1], empty)));
-          return returnRewrite(node, ret, "str-emp-repl-emp");
+          return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
         }
 
         // (= "" (str.replace x "A" "")) ---> (str.prefix x "A")
         if (checkEntailLengthOne(ne[1]) && ne[2] == empty)
         {
           Node ret = nm->mkNode(STRING_PREFIX, ne[0], ne[1]);
-          return returnRewrite(node, ret, "str-emp-repl-emp");
+          return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
         }
       }
       else if (ne.getKind() == STRING_SUBSTR)
@@ -588,20 +588,20 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
           if (ne[1] == zero)
           {
             Node ret = nm->mkNode(EQUAL, ne[0], empty);
-            return returnRewrite(node, ret, "str-emp-substr-leq-len");
+            return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_LEN);
           }
 
           // (= "" (str.substr x n m)) ---> (<= (str.len x) n)
           // if n >= 0 and m > 0
           Node ret = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, ne[0]), ne[1]);
-          return returnRewrite(node, ret, "str-emp-substr-leq-len");
+          return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_LEN);
         }
 
         // (= "" (str.substr "A" 0 z)) ---> (<= z 0)
         if (checkEntailNonEmpty(ne[0]) && ne[1] == zero)
         {
           Node ret = nm->mkNode(LEQ, ne[2], zero);
-          return returnRewrite(node, ret, "str-emp-substr-leq-z");
+          return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_Z);
         }
       }
     }
@@ -620,14 +620,14 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
       {
         Node ret = nm->mkNode(
             EQUAL, empty, nm->mkNode(STRING_STRREPL, x, repl[2], repl[1]));
-        return returnRewrite(node, ret, "str-eq-repl-emp");
+        return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_EMP);
       }
 
       // (= x (str.replace y x y)) ---> (= x y)
       if (repl[0] == repl[2] && x == repl[1])
       {
         Node ret = nm->mkNode(EQUAL, x, repl[0]);
-        return returnRewrite(node, ret, "str-eq-repl-to-eq");
+        return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_TO_EQ);
       }
 
       // (= x (str.replace x "A" "B")) ---> (not (str.contains x "A"))
@@ -637,7 +637,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
         if (eq.isConst() && !eq.getConst<bool>())
         {
           Node ret = nm->mkNode(NOT, nm->mkNode(STRING_STRCTN, x, repl[1]));
-          return returnRewrite(node, ret, "str-eq-repl-not-ctn");
+          return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_NOT_CTN);
         }
       }
 
@@ -652,7 +652,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
           Node ret = nm->mkNode(OR,
                                 nm->mkNode(EQUAL, repl[0], repl[1]),
                                 nm->mkNode(EQUAL, repl[0], repl[2]));
-          return returnRewrite(node, ret, "str-eq-repl-to-dis");
+          return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_TO_DIS);
         }
       }
     }
@@ -673,7 +673,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
       new_ret = inferEqsFromContains(node[i], node[1 - i]);
       if (!new_ret.isNull())
       {
-        return returnRewrite(node, new_ret, "str-eq-conj-len-entail");
+        return returnRewrite(node, new_ret, Rewrite::STR_EQ_CONJ_LEN_ENTAIL);
       }
     }
   }
@@ -715,7 +715,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
                                   pfx0.eqNode(pfx1),
                                   utils::mkConcat(sfxv0, stype)
                                       .eqNode(utils::mkConcat(sfxv1, stype)));
-            return returnRewrite(node, ret, "split-eq");
+            return returnRewrite(node, ret, Rewrite::SPLIT_EQ);
           }
           else if (checkEntailArith(lenPfx1, lenPfx0, true))
           {
@@ -735,7 +735,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
                                     pfx0.eqNode(utils::mkConcat(rpfxv1, stype)),
                                     utils::mkConcat(sfxv0, stype)
                                         .eqNode(utils::mkConcat(pfxv1, stype)));
-              return returnRewrite(node, ret, "split-eq-strip-r");
+              return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_R);
             }
 
             // If the prefix of the right-hand side is (strictly) longer than
@@ -762,7 +762,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
                                     utils::mkConcat(rpfxv0, stype).eqNode(pfx1),
                                     utils::mkConcat(pfxv0, stype)
                                         .eqNode(utils::mkConcat(sfxv1, stype)));
-              return returnRewrite(node, ret, "split-eq-strip-l");
+              return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_L);
             }
 
             // If the prefix of the left-hand side is (strictly) longer than
@@ -961,7 +961,7 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node)
     {
       retNode = vec.size() == 1 ? vec[0] : nm->mkNode(REGEXP_CONCAT, vec);
     }
-    return returnRewrite(node, retNode, "re.concat-flatten");
+    return returnRewrite(node, retNode, Rewrite::RE_CONCAT_FLATTEN);
   }
   Trace("strings-rewrite-debug")
       << "Strings::rewriteConcatRegExp start " << node << std::endl;
@@ -1039,7 +1039,7 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node)
   {
     // handles all cases where consecutive re constants are combined or
     // dropped as described in the loop above.
-    return returnRewrite(node, retNode, "re.concat");
+    return returnRewrite(node, retNode, Rewrite::RE_CONCAT);
   }
 
   // flipping adjacent star arguments
@@ -1056,7 +1056,7 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node)
   if (changed)
   {
     retNode = utils::mkConcat(cvec, rtype);
-    return returnRewrite(node, retNode, "re.concat.opt");
+    return returnRewrite(node, retNode, Rewrite::RE_CONCAT_OPT);
   }
   return node;
 }
@@ -1069,19 +1069,19 @@ Node SequencesRewriter::rewriteStarRegExp(TNode node)
   if (node[0].getKind() == REGEXP_STAR)
   {
     // ((R)*)* ---> R*
-    return returnRewrite(node, node[0], "re-star-nested-star");
+    return returnRewrite(node, node[0], Rewrite::RE_STAR_NESTED_STAR);
   }
   else if (node[0].getKind() == STRING_TO_REGEXP && node[0][0].isConst()
            && Word::isEmpty(node[0][0]))
   {
     // ("")* ---> ""
-    return returnRewrite(node, node[0], "re-star-empty-string");
+    return returnRewrite(node, node[0], Rewrite::RE_STAR_EMPTY_STRING);
   }
   else if (node[0].getKind() == REGEXP_EMPTY)
   {
     // (empty)* ---> ""
     retNode = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")));
-    return returnRewrite(node, retNode, "re-star-empty");
+    return returnRewrite(node, retNode, Rewrite::RE_STAR_EMPTY);
   }
   else if (node[0].getKind() == REGEXP_UNION)
   {
@@ -1110,7 +1110,7 @@ Node SequencesRewriter::rewriteStarRegExp(TNode node)
         retNode = nm->mkNode(REGEXP_STAR, retNode);
         // simplification of union beneath star based on loop above
         // for example, ( "" | "a" )* ---> ("a")*
-        return returnRewrite(node, retNode, "re-star-union");
+        return returnRewrite(node, retNode, Rewrite::RE_STAR_UNION);
       }
     }
   }
@@ -1140,7 +1140,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
     {
       if (nk == REGEXP_INTER)
       {
-        return returnRewrite(node, ni, "re.and-empty");
+        return returnRewrite(node, ni, Rewrite::RE_AND_EMPTY);
       }
       // otherwise, can ignore
     }
@@ -1148,7 +1148,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
     {
       if (nk == REGEXP_UNION)
       {
-        return returnRewrite(node, ni, "re.or-all");
+        return returnRewrite(node, ni, Rewrite::RE_OR_ALL);
       }
       // otherwise, can ignore
     }
@@ -1178,7 +1178,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
   if (retNode != node)
   {
     // flattening and removing children, based on loop above
-    return returnRewrite(node, retNode, "re.andor-flatten");
+    return returnRewrite(node, retNode, Rewrite::RE_ANDOR_FLATTEN);
   }
   return node;
 }
@@ -1190,7 +1190,7 @@ Node SequencesRewriter::rewriteLoopRegExp(TNode node)
   Node r = node[0];
   if (r.getKind() == REGEXP_STAR)
   {
-    return returnRewrite(node, r, "re.loop-star");
+    return returnRewrite(node, r, Rewrite::RE_LOOP_STAR);
   }
   TNode n1 = node[1];
   NodeManager* nm = NodeManager::currentNM();
@@ -1252,7 +1252,7 @@ Node SequencesRewriter::rewriteLoopRegExp(TNode node)
                       << std::endl;
   if (retNode != node)
   {
-    return returnRewrite(node, retNode, "re.loop");
+    return returnRewrite(node, retNode, Rewrite::RE_LOOP);
   }
   return node;
 }
@@ -1556,7 +1556,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
       {
         retNode = nm->mkConst(true);
         // e.g. (str.in.re "" (re.* (str.to.re x))) ----> true
-        return returnRewrite(node, retNode, "re-empty-in-str-star");
+        return returnRewrite(node, retNode, Rewrite::RE_EMPTY_IN_STR_STAR);
       }
       else if (s.size() == 1)
       {
@@ -1564,7 +1564,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
         {
           retNode = r[0][0].eqNode(x);
           // e.g. (str.in.re "A" (re.* (str.to.re x))) ----> "A" = x
-          return returnRewrite(node, retNode, "re-char-in-str-star");
+          return returnRewrite(node, retNode, Rewrite::RE_CHAR_IN_STR_STAR);
         }
       }
     }
@@ -1585,14 +1585,14 @@ Node SequencesRewriter::rewriteMembership(TNode node)
             nb << nm->mkNode(STRING_IN_REGEXP, xc, r);
           }
           return returnRewrite(
-              node, nb.constructNode(), "re-in-dist-char-star");
+              node, nb.constructNode(), Rewrite::RE_IN_DIST_CHAR_STAR);
         }
       }
     }
     if (r[0].getKind() == kind::REGEXP_SIGMA)
     {
       retNode = NodeManager::currentNM()->mkConst(true);
-      return returnRewrite(node, retNode, "re-in-sigma-star");
+      return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA_STAR);
     }
   }
   else if (r.getKind() == kind::REGEXP_CONCAT)
@@ -1642,14 +1642,14 @@ Node SequencesRewriter::rewriteMembership(TNode node)
         Node num = nm->mkConst(Rational(allSigmaMinSize));
         Node lenx = nm->mkNode(STRING_LENGTH, x);
         retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
-        return returnRewrite(node, retNode, "re-concat-pure-allchar");
+        return returnRewrite(node, retNode, Rewrite::RE_CONCAT_PURE_ALLCHAR);
       }
       else if (allSigmaMinSize == 0 && nchildren >= 3 && constIdx != 0
                && constIdx != nchildren - 1)
       {
         // x in re.++(_*, "abc", _*) ---> str.contains(x, "abc")
         retNode = nm->mkNode(STRING_STRCTN, x, constStr);
-        return returnRewrite(node, retNode, "re-concat-to-contains");
+        return returnRewrite(node, retNode, Rewrite::RE_CONCAT_TO_CONTAINS);
       }
     }
   }
@@ -1773,7 +1773,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
           }
           Trace("regexp-ext-rewrite") << "Regexp : rewrite : " << node << " -> "
                                       << retNode << std::endl;
-          return returnRewrite(node, retNode, "re-simple-consume");
+          return returnRewrite(node, retNode, Rewrite::RE_SIMPLE_CONSUME);
         }
       }
     }
@@ -2003,7 +2003,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
     if (Word::isEmpty(node[0]))
     {
       Node ret = node[0];
-      return returnRewrite(node, ret, "ss-emptystr");
+      return returnRewrite(node, ret, Rewrite::SS_EMPTYSTR);
     }
     // rewriting for constant arguments
     if (node[1].isConst() && node[2].isConst())
@@ -2016,13 +2016,13 @@ Node SequencesRewriter::rewriteSubstr(Node node)
         // start beyond the maximum size of strings
         // thus, it must be beyond the end point of this string
         Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, "ss-const-start-max-oob");
+        return returnRewrite(node, ret, Rewrite::SS_CONST_START_MAX_OOB);
       }
       else if (node[1].getConst<Rational>().sgn() < 0)
       {
         // start before the beginning of the string
         Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, "ss-const-start-neg");
+        return returnRewrite(node, ret, Rewrite::SS_CONST_START_NEG);
       }
       else
       {
@@ -2031,7 +2031,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
         {
           // start beyond the end of the string
           Node ret = Word::mkEmptyWord(node.getType());
-          return returnRewrite(node, ret, "ss-const-start-oob");
+          return returnRewrite(node, ret, Rewrite::SS_CONST_START_OOB);
         }
       }
       if (node[2].getConst<Rational>() > rMaxInt)
@@ -2039,12 +2039,12 @@ Node SequencesRewriter::rewriteSubstr(Node node)
         // take up to the end of the string
         size_t lenS = Word::getLength(s);
         Node ret = Word::suffix(s, lenS - start);
-        return returnRewrite(node, ret, "ss-const-len-max-oob");
+        return returnRewrite(node, ret, Rewrite::SS_CONST_LEN_MAX_OOB);
       }
       else if (node[2].getConst<Rational>().sgn() <= 0)
       {
         Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, "ss-const-len-non-pos");
+        return returnRewrite(node, ret, Rewrite::SS_CONST_LEN_NON_POS);
       }
       else
       {
@@ -2055,13 +2055,13 @@ Node SequencesRewriter::rewriteSubstr(Node node)
           // take up to the end of the string
           size_t lenS = Word::getLength(s);
           Node ret = Word::suffix(s, lenS - start);
-          return returnRewrite(node, ret, "ss-const-end-oob");
+          return returnRewrite(node, ret, Rewrite::SS_CONST_END_OOB);
         }
         else
         {
           // compute the substr using the constant string
           Node ret = Word::substr(s, start, len);
-          return returnRewrite(node, ret, "ss-const-ss");
+          return returnRewrite(node, ret, Rewrite::SS_CONST_SS);
         }
       }
     }
@@ -2072,12 +2072,12 @@ Node SequencesRewriter::rewriteSubstr(Node node)
   if (checkEntailArith(zero, node[1], true))
   {
     Node ret = Word::mkEmptyWord(node.getType());
-    return returnRewrite(node, ret, "ss-start-neg");
+    return returnRewrite(node, ret, Rewrite::SS_START_NEG);
   }
   else if (checkEntailArith(zero, node[2]))
   {
     Node ret = Word::mkEmptyWord(node.getType());
-    return returnRewrite(node, ret, "ss-len-non-pos");
+    return returnRewrite(node, ret, Rewrite::SS_LEN_NON_POS);
   }
 
   if (node[0].getKind() == STRING_SUBSTR)
@@ -2103,7 +2103,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
     if (checkEntailArith(node[1], node[0][2]))
     {
       Node ret = Word::mkEmptyWord(node.getType());
-      return returnRewrite(node, ret, "ss-start-geq-len");
+      return returnRewrite(node, ret, Rewrite::SS_START_GEQ_LEN);
     }
   }
   else if (node[0].getKind() == STRING_STRREPL)
@@ -2121,7 +2121,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
             nm->mkNode(kind::STRING_SUBSTR, node[0][0], node[1], node[2]),
             node[0][1],
             node[0][2]);
-        return returnRewrite(node, ret, "substr-repl-swap");
+        return returnRewrite(node, ret, Rewrite::SUBSTR_REPL_SWAP);
       }
     }
   }
@@ -2143,7 +2143,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
             kind::STRING_SUBSTR, utils::mkConcat(n1, stype), node[1], curr));
       }
       Node ret = utils::mkConcat(childrenr, stype);
-      return returnRewrite(node, ret, "ss-len-include");
+      return returnRewrite(node, ret, Rewrite::SS_LEN_INCLUDE);
     }
   }
 
@@ -2171,7 +2171,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
         {
           // end point beyond end point of string, map to tot_len
           Node ret = nm->mkNode(kind::STRING_SUBSTR, node[0], node[1], tot_len);
-          return returnRewrite(node, ret, "ss-end-pt-norm");
+          return returnRewrite(node, ret, Rewrite::SS_END_PT_NORM);
         }
         else
         {
@@ -2186,7 +2186,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
       if (checkEntailArithWithAssumption(n1_lt_tot_len, zero, node[2], false))
       {
         Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, "ss-start-entails-zero-len");
+        return returnRewrite(node, ret, Rewrite::SS_START_ENTAILS_ZERO_LEN);
       }
 
       // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
@@ -2195,7 +2195,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
       if (checkEntailArithWithAssumption(non_zero_len, node[1], tot_len, false))
       {
         Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, "ss-non-zero-len-entails-oob");
+        return returnRewrite(node, ret, Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB);
       }
 
       // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
@@ -2204,14 +2204,15 @@ Node SequencesRewriter::rewriteSubstr(Node node)
       if (checkEntailArithWithAssumption(geq_zero_start, zero, tot_len, false))
       {
         Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, "ss-geq-zero-start-entails-emp-s");
+        return returnRewrite(
+            node, ret, Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S);
       }
 
       // (str.substr s x x) ---> "" if (str.len s) <= 1
       if (node[1] == node[2] && checkEntailLengthOne(node[0]))
       {
         Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, "ss-len-one-z-z");
+        return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
       }
     }
     if (!curr.isNull())
@@ -2225,7 +2226,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
         {
           Node ret = nm->mkNode(
               kind::STRING_SUBSTR, utils::mkConcat(n1, stype), curr, node[2]);
-          return returnRewrite(node, ret, "ss-strip-start-pt");
+          return returnRewrite(node, ret, Rewrite::SS_STRIP_START_PT);
         }
         else
         {
@@ -2233,7 +2234,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
                                 utils::mkConcat(n1, stype),
                                 node[1],
                                 node[2]);
-          return returnRewrite(node, ret, "ss-strip-end-pt");
+          return returnRewrite(node, ret, Rewrite::SS_STRIP_END_PT);
         }
       }
     }
@@ -2273,7 +2274,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
         Node new_start = nm->mkNode(kind::PLUS, start_inner, start_outer);
         Node ret =
             nm->mkNode(kind::STRING_SUBSTR, node[0][0], new_start, new_len);
-        return returnRewrite(node, ret, "ss-combine");
+        return returnRewrite(node, ret, Rewrite::SS_COMBINE);
       }
     }
   }
@@ -2289,7 +2290,7 @@ Node SequencesRewriter::rewriteContains(Node node)
   if (node[0] == node[1])
   {
     Node ret = NodeManager::currentNM()->mkConst(true);
-    return returnRewrite(node, ret, "ctn-eq");
+    return returnRewrite(node, ret, Rewrite::CTN_EQ);
   }
   if (node[0].isConst())
   {
@@ -2297,7 +2298,7 @@ Node SequencesRewriter::rewriteContains(Node node)
     if (node[1].isConst())
     {
       Node ret = nm->mkConst(Word::find(node[0], node[1]) != std::string::npos);
-      return returnRewrite(node, ret, "ctn-const");
+      return returnRewrite(node, ret, Rewrite::CTN_CONST);
     }
     else
     {
@@ -2312,7 +2313,7 @@ Node SequencesRewriter::rewriteContains(Node node)
           // uses this function, hence we want to conclude false if possible.
           // len(x)>0 => contains( "", x ) ---> false
           Node ret = NodeManager::currentNM()->mkConst(false);
-          return returnRewrite(node, ret, "ctn-lhs-emptystr");
+          return returnRewrite(node, ret, Rewrite::CTN_LHS_EMPTYSTR);
         }
       }
       else if (checkEntailLengthOne(t))
@@ -2331,7 +2332,7 @@ Node SequencesRewriter::rewriteContains(Node node)
         // t = "" v t = "A" v t = "B" v t = "C" v t = "a" v t = "b" v t = "c"
         // if len(t) <= 1
         Node ret = nb;
-        return returnRewrite(node, ret, "ctn-split");
+        return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
       }
       else if (node[1].getKind() == kind::STRING_CONCAT)
       {
@@ -2339,7 +2340,7 @@ Node SequencesRewriter::rewriteContains(Node node)
         if (!canConstantContainConcat(node[0], node[1], firstc, lastc))
         {
           Node ret = NodeManager::currentNM()->mkConst(false);
-          return returnRewrite(node, ret, "ctn-nconst-ctn-concat");
+          return returnRewrite(node, ret, Rewrite::CTN_NCONST_CTN_CONCAT);
         }
       }
     }
@@ -2351,7 +2352,7 @@ Node SequencesRewriter::rewriteContains(Node node)
     {
       // contains( x, "" ) ---> true
       Node ret = NodeManager::currentNM()->mkConst(true);
-      return returnRewrite(node, ret, "ctn-rhs-emptystr");
+      return returnRewrite(node, ret, Rewrite::CTN_RHS_EMPTYSTR);
     }
     else if (len == 1)
     {
@@ -2370,7 +2371,7 @@ Node SequencesRewriter::rewriteContains(Node node)
         Node ret = nb.constructNode();
         // str.contains( x ++ y, "A" ) --->
         //   str.contains( x, "A" ) OR str.contains( y, "A" )
-        return returnRewrite(node, ret, "ctn-concat-char");
+        return returnRewrite(node, ret, Rewrite::CTN_CONCAT_CHAR);
       }
       else if (node[0].getKind() == STRING_STRREPL)
       {
@@ -2387,7 +2388,7 @@ Node SequencesRewriter::rewriteContains(Node node)
           // str.contains( str.replace( x, y, z ), "A" ) --->
           //   str.contains( x, "A" ) OR
           //   ( str.contains( x, y ) AND str.contains( z, "A" ) )
-          return returnRewrite(node, ret, "ctn-repl-char");
+          return returnRewrite(node, ret, Rewrite::CTN_REPL_CHAR);
         }
       }
     }
@@ -2403,7 +2404,7 @@ Node SequencesRewriter::rewriteContains(Node node)
   if (componentContains(nc1, nc2, nc1rb, nc1re) != -1)
   {
     Node ret = NodeManager::currentNM()->mkConst(true);
-    return returnRewrite(node, ret, "ctn-component");
+    return returnRewrite(node, ret, Rewrite::CTN_COMPONENT);
   }
   TypeNode stype = node[0].getType();
 
@@ -2414,7 +2415,7 @@ Node SequencesRewriter::rewriteContains(Node node)
   {
     Node ret = NodeManager::currentNM()->mkNode(
         kind::STRING_STRCTN, utils::mkConcat(nc1, stype), node[1]);
-    return returnRewrite(node, ret, "ctn-strip-endpt");
+    return returnRewrite(node, ret, Rewrite::CTN_STRIP_ENDPT);
   }
 
   for (const Node& n : nc2)
@@ -2435,7 +2436,7 @@ Node SequencesRewriter::rewriteContains(Node node)
         if (!ctnConst2.isNull() && !ctnConst2.getConst<bool>())
         {
           Node res = nm->mkConst(false);
-          return returnRewrite(node, res, "ctn-rpl-non-ctn");
+          return returnRewrite(node, res, Rewrite::CTN_RPL_NON_CTN);
         }
       }
 
@@ -2467,7 +2468,7 @@ Node SequencesRewriter::rewriteContains(Node node)
         {
           ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
         }
-        return returnRewrite(node, ret, "ctn-repl-self");
+        return returnRewrite(node, ret, Rewrite::CTN_REPL_SELF);
       }
     }
   }
@@ -2479,7 +2480,7 @@ Node SequencesRewriter::rewriteContains(Node node)
   {
     // len( n2 ) > len( n1 ) => contains( n1, n2 ) ---> false
     Node ret = NodeManager::currentNM()->mkConst(false);
-    return returnRewrite(node, ret, "ctn-len-ineq");
+    return returnRewrite(node, ret, Rewrite::CTN_LEN_INEQ);
   }
 
   // multi-set reasoning
@@ -2489,14 +2490,14 @@ Node SequencesRewriter::rewriteContains(Node node)
   if (checkEntailMultisetSubset(node[0], node[1]))
   {
     Node ret = nm->mkConst(false);
-    return returnRewrite(node, ret, "ctn-mset-nss");
+    return returnRewrite(node, ret, Rewrite::CTN_MSET_NSS);
   }
 
   if (checkEntailArith(len_n2, len_n1, false))
   {
     // len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
     Node ret = node[0].eqNode(node[1]);
-    return returnRewrite(node, ret, "ctn-len-ineq-nstrict");
+    return returnRewrite(node, ret, Rewrite::CTN_LEN_INEQ_NSTRICT);
   }
 
   // splitting
@@ -2534,7 +2535,7 @@ Node SequencesRewriter::rewriteContains(Node node)
                 NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
                                                  utils::mkConcat(spl[1], stype),
                                                  node[1]));
-            return returnRewrite(node, ret, "ctn-split");
+            return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
           }
         }
       }
@@ -2549,7 +2550,7 @@ Node SequencesRewriter::rewriteContains(Node node)
     if (node[0][2] == nm->mkNode(kind::STRING_LENGTH, node[1]))
     {
       Node ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
-      return returnRewrite(node, ret, "ctn-substr");
+      return returnRewrite(node, ret, Rewrite::CTN_SUBSTR);
     }
   }
   else if (node[0].getKind() == kind::STRING_STRREPL)
@@ -2562,7 +2563,7 @@ Node SequencesRewriter::rewriteContains(Node node)
         // (str.contains (str.replace x c1 c2) c3) ---> (str.contains x c3)
         // if there is no overlap between c1 and c3 and none between c2 and c3
         Node ret = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
-        return returnRewrite(node, ret, "ctn-repl-cnsts-to-ctn");
+        return returnRewrite(node, ret, Rewrite::CTN_REPL_CNSTS_TO_CTN);
       }
     }
 
@@ -2572,7 +2573,7 @@ Node SequencesRewriter::rewriteContains(Node node)
       if (node[0][1] == node[1])
       {
         Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
-        return returnRewrite(node, ret, "ctn-repl-to-ctn");
+        return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN);
       }
 
       // (str.contains (str.replace x y x) z) ---> (str.contains x z)
@@ -2580,7 +2581,7 @@ Node SequencesRewriter::rewriteContains(Node node)
       if (checkEntailLengthOne(node[1]))
       {
         Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
-        return returnRewrite(node, ret, "ctn-repl-len-one-to-ctn");
+        return returnRewrite(node, ret, Rewrite::CTN_REPL_LEN_ONE_TO_CTN);
       }
     }
 
@@ -2591,7 +2592,7 @@ Node SequencesRewriter::rewriteContains(Node node)
       Node ret = nm->mkNode(OR,
                             nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]),
                             nm->mkNode(STRING_STRCTN, node[0][0], node[0][2]));
-      return returnRewrite(node, ret, "ctn-repl-to-ctn-disj");
+      return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN_DISJ);
     }
 
     // (str.contains (str.replace x y z) w) --->
@@ -2607,7 +2608,7 @@ Node SequencesRewriter::rewriteContains(Node node)
             kind::STRING_STRCTN,
             nm->mkNode(kind::STRING_STRREPL, node[0][0], node[0][1], empty),
             node[1]);
-        return returnRewrite(node, ret, "ctn-repl-simp-repl");
+        return returnRewrite(node, ret, Rewrite::CTN_REPL_SIMP_REPL);
       }
     }
   }
@@ -2619,7 +2620,7 @@ Node SequencesRewriter::rewriteContains(Node node)
     if (node[0] == node[1][1] && node[1][0] == node[1][2])
     {
       Node ret = nm->mkNode(kind::STRING_STRCTN, node[0], node[1][0]);
-      return returnRewrite(node, ret, "ctn-repl");
+      return returnRewrite(node, ret, Rewrite::CTN_REPL);
     }
 
     // (str.contains x (str.replace "" x y)) --->
@@ -2632,7 +2633,7 @@ Node SequencesRewriter::rewriteContains(Node node)
     if (node[0] == node[1][1] && node[1][0] == emp)
     {
       Node ret = nm->mkNode(kind::EQUAL, emp, node[1]);
-      return returnRewrite(node, ret, "ctn-repl-empty");
+      return returnRewrite(node, ret, Rewrite::CTN_REPL_EMPTY);
     }
   }
 
@@ -2649,7 +2650,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
   {
     // z<0  implies  str.indexof( x, y, z ) --> -1
     Node negone = nm->mkConst(Rational(-1));
-    return returnRewrite(node, negone, "idof-neg");
+    return returnRewrite(node, negone, Rewrite::IDOF_NEG);
   }
 
   // the string type
@@ -2667,7 +2668,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
       // in our implementation, that accessing a position greater than
       // rMaxInt is guaranteed to be out of bounds.
       Node negone = nm->mkConst(Rational(-1));
-      return returnRewrite(node, negone, "idof-max");
+      return returnRewrite(node, negone, Rewrite::IDOF_MAX);
     }
     Assert(node[2].getConst<Rational>().sgn() >= 0);
     Node s = children0[0];
@@ -2678,12 +2679,12 @@ Node SequencesRewriter::rewriteIndexof(Node node)
     if (ret != std::string::npos)
     {
       Node retv = nm->mkConst(Rational(static_cast<unsigned>(ret)));
-      return returnRewrite(node, retv, "idof-find");
+      return returnRewrite(node, retv, Rewrite::IDOF_FIND);
     }
     else if (children0.size() == 1)
     {
       Node negone = nm->mkConst(Rational(-1));
-      return returnRewrite(node, negone, "idof-nfind");
+      return returnRewrite(node, negone, Rewrite::IDOF_NFIND);
     }
   }
 
@@ -2695,21 +2696,21 @@ Node SequencesRewriter::rewriteIndexof(Node node)
       {
         // indexof( x, x, 0 ) --> 0
         Node zero = nm->mkConst(Rational(0));
-        return returnRewrite(node, zero, "idof-eq-cst-start");
+        return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START);
       }
     }
     if (checkEntailArith(node[2], true))
     {
       // y>0  implies  indexof( x, x, y ) --> -1
       Node negone = nm->mkConst(Rational(-1));
-      return returnRewrite(node, negone, "idof-eq-nstart");
+      return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART);
     }
     Node emp = nm->mkConst(CVC4::String(""));
     if (node[0] != emp)
     {
       // indexof( x, x, z ) ---> indexof( "", "", z )
       Node ret = nm->mkNode(STRING_STRIDOF, emp, emp, node[2]);
-      return returnRewrite(node, ret, "idof-eq-norm");
+      return returnRewrite(node, ret, Rewrite::IDOF_EQ_NORM);
     }
   }
 
@@ -2724,7 +2725,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
       if (checkEntailArith(len0, node[2]) && checkEntailArith(node[2]))
       {
         // len(x)>=z ^ z >=0 implies indexof( x, "", z ) ---> z
-        return returnRewrite(node, node[2], "idof-emp-idof");
+        return returnRewrite(node, node[2], Rewrite::IDOF_EMP_IDOF);
       }
     }
   }
@@ -2733,7 +2734,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
   {
     // len(x)-z < len(y)  implies  indexof( x, y, z ) ----> -1
     Node negone = nm->mkConst(Rational(-1));
-    return returnRewrite(node, negone, "idof-len");
+    return returnRewrite(node, negone, Rewrite::IDOF_LEN);
   }
 
   Node fstr = node[0];
@@ -2765,7 +2766,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
           // str.indexof(str.++(x,y,z),y,0) ---> str.indexof(str.++(x,y),y,0)
           Node nn = utils::mkConcat(children0, stype);
           Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
-          return returnRewrite(node, ret, "idof-def-ctn");
+          return returnRewrite(node, ret, Rewrite::IDOF_DEF_CTN);
         }
 
         // Strip components from the beginning that are guaranteed not to match
@@ -2780,7 +2781,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
                          utils::mkConcat(children0, stype),
                          node[1],
                          node[2]));
-          return returnRewrite(node, ret, "idof-strip-cnst-endpts");
+          return returnRewrite(node, ret, Rewrite::IDOF_STRIP_CNST_ENDPTS);
         }
       }
 
@@ -2799,14 +2800,14 @@ Node SequencesRewriter::rewriteIndexof(Node node)
             nm->mkNode(kind::PLUS,
                        nm->mkNode(kind::MINUS, node[2], new_len),
                        nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len));
-        return returnRewrite(node, ret, "idof-strip-sym-len");
+        return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
       }
     }
     else
     {
       // str.contains( x, y ) --> false  implies  str.indexof(x,y,z) --> -1
       Node negone = nm->mkConst(Rational(-1));
-      return returnRewrite(node, negone, "idof-nctn");
+      return returnRewrite(node, negone, Rewrite::IDOF_NCTN);
     }
   }
   else
@@ -2830,7 +2831,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
         children.insert(children.end(), children0.begin(), children0.end());
         Node nn = utils::mkConcat(children, stype);
         Node res = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
-        return returnRewrite(node, res, "idof-norm-prefix");
+        return returnRewrite(node, res, Rewrite::IDOF_NORM_PREFIX);
       }
     }
   }
@@ -2845,7 +2846,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
       ret = nm->mkNode(STRING_STRIDOF, ret, node[1], node[2]);
       // For example:
       // str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 )
-      return returnRewrite(node, ret, "rpl-pull-endpt");
+      return returnRewrite(node, ret, Rewrite::RPL_PULL_ENDPT);
     }
   }
 
@@ -2861,7 +2862,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
   if (node[1].isConst() && Word::isEmpty(node[1]))
   {
     Node ret = nm->mkNode(STRING_CONCAT, node[2], node[0]);
-    return returnRewrite(node, ret, "rpl-rpl-empty");
+    return returnRewrite(node, ret, Rewrite::RPL_RPL_EMPTY);
   }
   // the string type
   TypeNode stype = node.getType();
@@ -2878,7 +2879,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
     {
       if (children0.size() == 1)
       {
-        return returnRewrite(node, node[0], "rpl-const-nfind");
+        return returnRewrite(node, node[0], Rewrite::RPL_CONST_NFIND);
       }
     }
     else
@@ -2897,7 +2898,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
       }
       children.insert(children.end(), children0.begin() + 1, children0.end());
       Node ret = utils::mkConcat(children, stype);
-      return returnRewrite(node, ret, "rpl-const-find");
+      return returnRewrite(node, ret, Rewrite::RPL_CONST_FIND);
     }
   }
 
@@ -2916,7 +2917,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
     Node l1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
     if (checkEntailArith(l1, l0))
     {
-      return returnRewrite(node, node[0], "rpl-rpl-len-id");
+      return returnRewrite(node, node[0], Rewrite::RPL_RPL_LEN_ID);
     }
 
     // (str.replace x y x) ---> (str.replace x (str.++ y1 ... yn) x)
@@ -2938,7 +2939,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
           if (node[1] != nn1)
           {
             Node ret = nm->mkNode(STRING_STRREPL, node[0], nn1, node[2]);
-            return returnRewrite(node, ret, "rpl-x-y-x-simp");
+            return returnRewrite(node, ret, Rewrite::RPL_X_Y_X_SIMP);
           }
         }
       }
@@ -2971,7 +2972,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
           cres.push_back(node[2]);
           cres.insert(cres.end(), ce.begin(), ce.end());
           Node ret = utils::mkConcat(cres, stype);
-          return returnRewrite(node, ret, "rpl-cctn-rpl");
+          return returnRewrite(node, ret, Rewrite::RPL_CCTN_RPL);
         }
         else if (!ce.empty())
         {
@@ -2988,14 +2989,14 @@ Node SequencesRewriter::rewriteReplace(Node node)
               node[2]));
           scc.insert(scc.end(), ce.begin(), ce.end());
           Node ret = utils::mkConcat(scc, stype);
-          return returnRewrite(node, ret, "rpl-cctn");
+          return returnRewrite(node, ret, Rewrite::RPL_CCTN);
         }
       }
     }
     else
     {
       // ~contains( t, s ) => ( replace( t, s, r ) ----> t )
-      return returnRewrite(node, node[0], "rpl-nctn");
+      return returnRewrite(node, node[0], Rewrite::RPL_NCTN);
     }
   }
   else if (cmp_conr.getKind() == kind::EQUAL || cmp_conr.getKind() == kind::AND)
@@ -3039,14 +3040,14 @@ Node SequencesRewriter::rewriteReplace(Node node)
         if (nn1 != node[1] || nn2 != node[2])
         {
           Node res = nm->mkNode(kind::STRING_STRREPL, node[0], nn1, nn2);
-          return returnRewrite(node, res, "rpl-emp-cnts-substs");
+          return returnRewrite(node, res, Rewrite::RPL_EMP_CNTS_SUBSTS);
         }
       }
 
       if (nn2 != node[2])
       {
         Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1], nn2);
-        return returnRewrite(node, res, "rpl-cnts-substs");
+        return returnRewrite(node, res, Rewrite::RPL_CNTS_SUBSTS);
       }
     }
   }
@@ -3072,7 +3073,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
                                              node[2]));
         cc.insert(cc.end(), ce.begin(), ce.end());
         Node ret = utils::mkConcat(cc, stype);
-        return returnRewrite(node, ret, "rpl-pull-endpt");
+        return returnRewrite(node, ret, Rewrite::RPL_PULL_ENDPT);
       }
     }
   }
@@ -3114,7 +3115,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
                             node[0],
                             utils::mkConcat(children1, stype),
                             node[2]);
-      return returnRewrite(node, res, "repl-subst-idx");
+      return returnRewrite(node, res, Rewrite::REPL_SUBST_IDX);
     }
   }
 
@@ -3162,7 +3163,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
                                 nm->mkNode(kind::STRING_STRREPL, y, w, z),
                                 y,
                                 z);
-          return returnRewrite(node, ret, "repl-repl-short-circuit");
+          return returnRewrite(node, ret, Rewrite::REPL_REPL_SHORT_CIRCUIT);
         }
       }
     }
@@ -3175,7 +3176,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
       if (node[1][0] == node[1][2] && node[1][0] == node[2])
       {
         // str.replace( x, str.replace( x, y, x ), x ) ---> x
-        return returnRewrite(node, node[0], "repl-repl2-inv-id");
+        return returnRewrite(node, node[0], Rewrite::REPL_REPL2_INV_ID);
       }
       bool dualReplIteSuccess = false;
       Node cmp_con2 = checkEntailContains(node[1][0], node[1][2]);
@@ -3209,7 +3210,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
                               nm->mkNode(STRING_STRCTN, node[0], node[1][1]),
                               node[0],
                               node[2]);
-        return returnRewrite(node, res, "repl-dual-repl-ite");
+        return returnRewrite(node, res, Rewrite::REPL_DUAL_REPL_ITE);
       }
     }
 
@@ -3245,7 +3246,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
     if (invSuccess)
     {
       Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1][0], node[2]);
-      return returnRewrite(node, res, "repl-repl2-inv");
+      return returnRewrite(node, res, Rewrite::REPL_REPL2_INV);
     }
   }
   if (node[2].getKind() == STRING_STRREPL)
@@ -3259,7 +3260,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
       {
         Node res =
             nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]);
-        return returnRewrite(node, res, "repl-repl3-inv");
+        return returnRewrite(node, res, Rewrite::REPL_REPL3_INV);
       }
     }
     if (node[2][0] == node[1])
@@ -3279,7 +3280,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
       }
       if (success)
       {
-        return returnRewrite(node, node[0], "repl-repl3-inv-id");
+        return returnRewrite(node, node[0], Rewrite::REPL_REPL3_INV_ID);
       }
     }
   }
@@ -3326,7 +3327,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
       // second occurrence of x. Notice this is specific to single characters
       // due to complications with finds that span multiple components for
       // non-characters.
-      return returnRewrite(node, ret, "repl-char-ncontrib-find");
+      return returnRewrite(node, ret, Rewrite::REPL_CHAR_NCONTRIB_FIND);
     }
   }
 
@@ -3353,7 +3354,7 @@ Node SequencesRewriter::rewriteReplaceAll(Node node)
     Node t = node[1];
     if (Word::isEmpty(s) || Word::isEmpty(t))
     {
-      return returnRewrite(node, node[0], "replall-empty-find");
+      return returnRewrite(node, node[0], Rewrite::REPLALL_EMPTY_FIND);
     }
     std::size_t sizeS = Word::getLength(s);
     std::size_t sizeT = Word::getLength(t);
@@ -3378,7 +3379,7 @@ Node SequencesRewriter::rewriteReplaceAll(Node node)
     } while (curr != std::string::npos && curr < sizeS);
     // constant evaluation
     Node res = utils::mkConcat(children, stype);
-    return returnRewrite(node, res, "replall-const");
+    return returnRewrite(node, res, Rewrite::REPLALL_CONST);
   }
 
   // rewrites that apply to both replace and replaceall
@@ -3400,7 +3401,7 @@ Node SequencesRewriter::rewriteReplaceInternal(Node node)
 
   if (node[1] == node[2])
   {
-    return returnRewrite(node, node[0], "rpl-id");
+    return returnRewrite(node, node[0], Rewrite::RPL_ID);
   }
 
   if (node[0] == node[1])
@@ -3408,7 +3409,7 @@ Node SequencesRewriter::rewriteReplaceInternal(Node node)
     // only holds for replaceall if non-empty
     if (nk == STRING_STRREPL || checkEntailNonEmpty(node[1]))
     {
-      return returnRewrite(node, node[2], "rpl-replace");
+      return returnRewrite(node, node[2], Rewrite::RPL_REPLACE);
     }
   }
 
@@ -3425,7 +3426,7 @@ Node SequencesRewriter::rewriteStrReverse(Node node)
     std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
     std::reverse(nvec.begin(), nvec.end());
     Node retNode = nm->mkConst(String(nvec));
-    return returnRewrite(node, retNode, "str-conv-const");
+    return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
   }
   else if (x.getKind() == STRING_CONCAT)
   {
@@ -3437,13 +3438,13 @@ Node SequencesRewriter::rewriteStrReverse(Node node)
     std::reverse(children.begin(), children.end());
     // rev( x1 ++ x2 ) --> rev( x2 ) ++ rev( x1 )
     Node retNode = nm->mkNode(STRING_CONCAT, children);
-    return returnRewrite(node, retNode, "str-rev-minscope-concat");
+    return returnRewrite(node, retNode, Rewrite::STR_REV_MINSCOPE_CONCAT);
   }
   else if (x.getKind() == STRING_REV)
   {
     // rev( rev( x ) ) --> x
     Node retNode = x[0];
-    return returnRewrite(node, retNode, "str-rev-idem");
+    return returnRewrite(node, retNode, Rewrite::STR_REV_IDEM);
   }
   return node;
 }
@@ -3456,7 +3457,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
   if (n[0] == n[1])
   {
     Node ret = NodeManager::currentNM()->mkConst(true);
-    return returnRewrite(n, ret, "suf/prefix-eq");
+    return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EQ);
   }
   if (n[0].isConst())
   {
@@ -3464,7 +3465,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
     if (t.isEmptyString())
     {
       Node ret = NodeManager::currentNM()->mkConst(true);
-      return returnRewrite(n, ret, "suf/prefix-empty-const");
+      return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY_CONST);
     }
   }
   if (n[1].isConst())
@@ -3484,12 +3485,12 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
           ret = NodeManager::currentNM()->mkConst(true);
         }
       }
-      return returnRewrite(n, ret, "suf/prefix-const");
+      return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CONST);
     }
     else if (lenS == 0)
     {
       Node ret = n[0].eqNode(n[1]);
-      return returnRewrite(n, ret, "suf/prefix-empty");
+      return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY);
     }
     else if (lenS == 1)
     {
@@ -3497,7 +3498,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
       // (str.contains "A" x )
       Node ret =
           NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, n[1], n[0]);
-      return returnRewrite(n, ret, "suf/prefix-ctn");
+      return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CTN);
     }
   }
   Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]);
@@ -3517,7 +3518,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
   Node eqs = inferEqsFromContains(n[1], n[0]);
   if (!eqs.isNull())
   {
-    return returnRewrite(n, eqs, "suf/prefix-to-eqs");
+    return returnRewrite(n, eqs, Rewrite::SUF_PREFIX_TO_EQS);
   }
 
   // general reduction to equality + substr
@@ -5565,9 +5566,9 @@ std::pair<bool, std::vector<Node> > SequencesRewriter::collectEmptyEqs(Node x)
       allEmptyEqs, std::vector<Node>(emptyNodes.begin(), emptyNodes.end()));
 }
 
-Node SequencesRewriter::returnRewrite(Node node, Node ret, const char* c)
+Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
 {
-  Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c
+  Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << r
                            << "." << std::endl;
 
   NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 5aba4ab6f..a98ad97ac 100644
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/attribute.h"
+#include "theory/strings/rewrites.h"
 #include "theory/theory_rewriter.h"
 #include "theory/type_enumerator.h"
 
@@ -149,7 +150,7 @@ class SequencesRewriter : public TheoryRewriter
   /**
    * Called when node rewrites to ret.
    *
-   * The string c indicates the justification for the rewrite, which is printed
+   * The rewrite r indicates the justification for the rewrite, which is printed
    * by this function for debugging.
    *
    * If node is not an equality and ret is an equality, this method applies
@@ -157,7 +158,7 @@ class SequencesRewriter : public TheoryRewriter
    * additional rewrites on ret, after which we return the result of this call.
    * Otherwise, this method simply returns ret.
    */
-  static Node returnRewrite(Node node, Node ret, const char* c);
+  static Node returnRewrite(Node node, Node ret, Rewrite r);
 
  public:
   RewriteResponse postRewrite(TNode node) override;
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index c7676d049..275c2e25e 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -41,7 +41,7 @@ Node StringsRewriter::rewriteStrToInt(Node node)
     {
       ret = nm->mkConst(Rational(-1));
     }
-    return returnRewrite(node, ret, "stoi-eval");
+    return returnRewrite(node, ret, Rewrite::STOI_EVAL);
   }
   else if (node[0].getKind() == STRING_CONCAT)
   {
@@ -53,7 +53,7 @@ Node StringsRewriter::rewriteStrToInt(Node node)
         if (!t.isNumber())
         {
           Node ret = nm->mkConst(Rational(-1));
-          return returnRewrite(node, ret, "stoi-concat-nonnum");
+          return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM);
         }
       }
     }
@@ -78,7 +78,7 @@ Node StringsRewriter::rewriteIntToStr(Node node)
       Assert(stmp[0] != '-');
       ret = nm->mkConst(String(stmp));
     }
-    return returnRewrite(node, ret, "itos-eval");
+    return returnRewrite(node, ret, Rewrite::ITOS_EVAL);
   }
   return node;
 }
@@ -114,7 +114,7 @@ Node StringsRewriter::rewriteStrConvert(Node node)
       nvec[i] = newChar;
     }
     Node retNode = nm->mkConst(String(nvec));
-    return returnRewrite(node, retNode, "str-conv-const");
+    return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
   }
   else if (node[0].getKind() == STRING_CONCAT)
   {
@@ -125,7 +125,7 @@ Node StringsRewriter::rewriteStrConvert(Node node)
     }
     // tolower( x1 ++ x2 ) --> tolower( x1 ) ++ tolower( x2 )
     Node retNode = concatBuilder.constructNode();
-    return returnRewrite(node, retNode, "str-conv-minscope-concat");
+    return returnRewrite(node, retNode, Rewrite::STR_CONV_MINSCOPE_CONCAT);
   }
   else if (node[0].getKind() == STRING_TOLOWER
            || node[0].getKind() == STRING_TOUPPER)
@@ -133,12 +133,12 @@ Node StringsRewriter::rewriteStrConvert(Node node)
     // tolower( tolower( x ) ) --> tolower( x )
     // tolower( toupper( x ) ) --> tolower( x )
     Node retNode = nm->mkNode(nk, node[0][0]);
-    return returnRewrite(node, retNode, "str-conv-idem");
+    return returnRewrite(node, retNode, Rewrite::STR_CONV_IDEM);
   }
   else if (node[0].getKind() == STRING_ITOS)
   {
     // tolower( str.from.int( x ) ) --> str.from.int( x )
-    return returnRewrite(node, node[0], "str-conv-itos");
+    return returnRewrite(node, node[0], Rewrite::STR_CONV_ITOS);
   }
   return node;
 }
@@ -150,14 +150,14 @@ Node StringsRewriter::rewriteStringLeq(Node n)
   if (n[0] == n[1])
   {
     Node ret = nm->mkConst(true);
-    return returnRewrite(n, ret, "str-leq-id");
+    return returnRewrite(n, ret, Rewrite::STR_LEQ_ID);
   }
   if (n[0].isConst() && n[1].isConst())
   {
     String s = n[0].getConst<String>();
     String t = n[1].getConst<String>();
     Node ret = nm->mkConst(s.isLeq(t));
-    return returnRewrite(n, ret, "str-leq-eval");
+    return returnRewrite(n, ret, Rewrite::STR_LEQ_EVAL);
   }
   // empty strings
   for (unsigned i = 0; i < 2; i++)
@@ -165,7 +165,7 @@ Node StringsRewriter::rewriteStringLeq(Node n)
     if (n[i].isConst() && n[i].getConst<String>().isEmptyString())
     {
       Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]);
-      return returnRewrite(n, ret, "str-leq-empty");
+      return returnRewrite(n, ret, Rewrite::STR_LEQ_EMPTY);
     }
   }
 
@@ -189,7 +189,7 @@ Node StringsRewriter::rewriteStringLeq(Node n)
     if (!s.isLeq(t))
     {
       Node ret = nm->mkConst(false);
-      return returnRewrite(n, ret, "str-leq-cprefix");
+      return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX);
     }
   }
   return n;
@@ -213,7 +213,7 @@ Node StringsRewriter::rewriteStringFromCode(Node n)
     {
       ret = nm->mkConst(String(""));
     }
-    return returnRewrite(n, ret, "from-code-eval");
+    return returnRewrite(n, ret, Rewrite::FROM_CODE_EVAL);
   }
   return n;
 }
@@ -236,7 +236,7 @@ Node StringsRewriter::rewriteStringToCode(Node n)
     {
       ret = nm->mkConst(Rational(-1));
     }
-    return returnRewrite(n, ret, "to-code-eval");
+    return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL);
   }
   return n;
 }