Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of inference information utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/strings/rewrites.h"
      14                 :            : 
      15                 :            : #include <iostream>
      16                 :            : 
      17                 :            : #include "base/check.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : namespace theory {
      21                 :            : namespace strings {
      22                 :            : 
      23                 :        202 : const char* toString(Rewrite r)
      24                 :            : {
      25 [ +  + ][ +  + ]:        202 :   switch (r)
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ -  - ]
      26                 :            :   {
      27                 :          1 :     case Rewrite::NONE: return "NONE";
      28                 :          1 :     case Rewrite::CTN_COMPONENT: return "CTN_COMPONENT";
      29                 :          1 :     case Rewrite::CTN_CONCAT_CHAR: return "CTN_CONCAT_CHAR";
      30                 :          1 :     case Rewrite::CTN_CONST: return "CTN_CONST";
      31                 :          1 :     case Rewrite::CTN_EQ: return "CTN_EQ";
      32                 :          1 :     case Rewrite::CTN_LEN_INEQ: return "CTN_LEN_INEQ";
      33                 :          1 :     case Rewrite::CTN_LEN_INEQ_NSTRICT: return "CTN_LEN_INEQ_NSTRICT";
      34                 :          1 :     case Rewrite::CTN_LHS_EMPTYSTR: return "CTN_LHS_EMPTYSTR";
      35                 :          1 :     case Rewrite::CTN_MSET_NSS: return "CTN_MSET_NSS";
      36                 :          1 :     case Rewrite::CTN_NCONST_CTN_CONCAT: return "CTN_NCONST_CTN_CONCAT";
      37                 :          1 :     case Rewrite::CTN_REPL: return "CTN_REPL";
      38                 :          1 :     case Rewrite::CTN_REPL_CHAR: return "CTN_REPL_CHAR";
      39                 :          1 :     case Rewrite::CTN_REPL_EMPTY: return "CTN_REPL_EMPTY";
      40                 :          1 :     case Rewrite::CTN_REPL_LEN_ONE_TO_CTN: return "CTN_REPL_LEN_ONE_TO_CTN";
      41                 :          1 :     case Rewrite::CTN_REPL_TO_CTN: return "CTN_REPL_TO_CTN";
      42                 :          1 :     case Rewrite::CTN_REPL_TO_CTN_DISJ: return "CTN_REPL_TO_CTN_DISJ";
      43                 :          1 :     case Rewrite::CTN_RHS_EMPTYSTR: return "CTN_RHS_EMPTYSTR";
      44                 :          1 :     case Rewrite::CTN_RPL_NON_CTN: return "CTN_RPL_NON_CTN";
      45                 :          1 :     case Rewrite::CTN_CONCAT_CTN_SUBSTR: return "CTN_CONCAT_CTN_SUBSTR";
      46                 :          1 :     case Rewrite::CTN_SPLIT: return "CTN_SPLIT";
      47                 :          1 :     case Rewrite::CTN_SPLIT_ONES: return "CTN_SPLIT_ONES";
      48                 :          1 :     case Rewrite::CTN_STRIP_ENDPT: return "CTN_STRIP_ENDPT";
      49                 :          1 :     case Rewrite::CTN_SUBSTR: return "CTN_SUBSTR";
      50                 :          1 :     case Rewrite::CTN_CONCAT_COM_NON_CTN: return "CTN_CONCAT_COM_NON_CTN";
      51                 :          1 :     case Rewrite::CTN_ITOS_NON_DIGIT: return "CTN_ITOS_NON_DIGIT";
      52                 :          1 :     case Rewrite::EQ_NCTN: return "EQ_NCTN";
      53                 :          1 :     case Rewrite::EQ_NFIX: return "EQ_NFIX";
      54                 :          1 :     case Rewrite::FROM_CODE_EVAL: return "FROM_CODE_EVAL";
      55                 :          1 :     case Rewrite::IDOF_DEF_CTN: return "IDOF_DEF_CTN";
      56                 :          1 :     case Rewrite::IDOF_EMP_IDOF: return "IDOF_EMP_IDOF";
      57                 :          1 :     case Rewrite::IDOF_EQ_CST_START: return "IDOF_EQ_CST_START";
      58                 :          1 :     case Rewrite::IDOF_EQ_NORM: return "IDOF_EQ_NORM";
      59                 :          1 :     case Rewrite::IDOF_EQ_NSTART: return "IDOF_EQ_NSTART";
      60                 :          1 :     case Rewrite::IDOF_FIND: return "IDOF_FIND";
      61                 :          1 :     case Rewrite::IDOF_LEN: return "IDOF_LEN";
      62                 :          1 :     case Rewrite::IDOF_MAX: return "IDOF_MAX";
      63                 :          1 :     case Rewrite::IDOF_NCTN: return "IDOF_NCTN";
      64                 :          1 :     case Rewrite::IDOF_NEG: return "IDOF_NEG";
      65                 :          1 :     case Rewrite::IDOF_NFIND: return "IDOF_NFIND";
      66                 :          1 :     case Rewrite::IDOF_NORM_PREFIX: return "IDOF_NORM_PREFIX";
      67                 :          1 :     case Rewrite::IDOF_PULL_ENDPT: return "IDOF_PULL_ENDPT";
      68                 :          1 :     case Rewrite::IDOF_STRIP_CNST_ENDPTS: return "IDOF_STRIP_CNST_ENDPTS";
      69                 :          1 :     case Rewrite::IDOF_STRIP_SYM_LEN: return "IDOF_STRIP_SYM_LEN";
      70                 :          1 :     case Rewrite::INDEXOF_RE_EMP_RE: return "INDEXOF_RE_EMP_RE";
      71                 :          1 :     case Rewrite::INDEXOF_RE_EVAL: return "INDEXOF_RE_EVAL";
      72                 :          1 :     case Rewrite::INDEXOF_RE_INVALID_INDEX: return "INDEXOF_RE_INVALID_INDEX";
      73                 :          1 :     case Rewrite::INDEXOF_RE_MAX_INDEX: return "INDEXOF_RE_MAX_INDEX";
      74                 :          1 :     case Rewrite::INDEXOF_RE_NONE: return "INDEXOF_RE_NONE";
      75                 :          1 :     case Rewrite::ITOS_EVAL: return "ITOS_EVAL";
      76                 :          1 :     case Rewrite::RE_ALL_ELIM: return "RE_ALL_ELIM";
      77                 :          1 :     case Rewrite::RE_AND_EMPTY: return "RE_AND_EMPTY";
      78                 :          1 :     case Rewrite::RE_ANDOR_FLATTEN: return "RE_ANDOR_FLATTEN";
      79                 :          1 :     case Rewrite::RE_ANDOR_CONST_REMOVE: return "RE_ANDOR_CONST_REMOVE";
      80                 :          1 :     case Rewrite::RE_ANDOR_INC_CONFLICT: return "RE_ANDOR_INC_CONFLICT";
      81                 :          1 :     case Rewrite::RE_INTER_CONST_CONST_CONFLICT:
      82                 :          1 :       return "RE_INTER_CONST_CONST_CONFLICT";
      83                 :          1 :     case Rewrite::RE_INTER_CONST_RE_CONFLICT:
      84                 :          1 :       return "RE_INTER_CONST_RE_CONFLICT";
      85                 :          1 :     case Rewrite::RE_CHAR_IN_STR_STAR: return "RE_CHAR_IN_STR_STAR";
      86                 :          1 :     case Rewrite::RE_CONCAT: return "RE_CONCAT";
      87                 :          1 :     case Rewrite::RE_CONCAT_FLATTEN: return "RE_CONCAT_FLATTEN";
      88                 :          1 :     case Rewrite::RE_CONCAT_OPT: return "RE_CONCAT_OPT";
      89                 :          1 :     case Rewrite::RE_CONCAT_PURE_ALLCHAR: return "RE_CONCAT_PURE_ALLCHAR";
      90                 :          1 :     case Rewrite::RE_CONCAT_TO_CONTAINS: return "RE_CONCAT_TO_CONTAINS";
      91                 :          1 :     case Rewrite::RE_EMPTY_IN_STR_STAR: return "RE_EMPTY_IN_STR_STAR";
      92                 :          1 :     case Rewrite::RE_IN_DIST_CHAR_STAR: return "RE_IN_DIST_CHAR_STAR";
      93                 :          1 :     case Rewrite::RE_IN_SIGMA_STAR: return "RE_IN_SIGMA_STAR";
      94                 :          1 :     case Rewrite::RE_IN_CHAR_MODULUS_STAR: return "RE_IN_CHAR_MODULUS_STAR";
      95                 :          1 :     case Rewrite::RE_IN_INCLUSION: return "RE_IN_INCLUSION";
      96                 :          1 :     case Rewrite::RE_LOOP: return "RE_LOOP";
      97                 :          1 :     case Rewrite::RE_LOOP_NONE: return "RE_LOOP_NONE";
      98                 :          1 :     case Rewrite::RE_LOOP_ZERO: return "RE_LOOP_ZERO";
      99                 :          1 :     case Rewrite::RE_LOOP_STAR: return "RE_LOOP_STAR";
     100                 :          1 :     case Rewrite::RE_OR_ALL: return "RE_OR_ALL";
     101                 :          1 :     case Rewrite::RE_SIMPLE_CONSUME: return "RE_SIMPLE_CONSUME";
     102                 :          1 :     case Rewrite::RE_STAR_EMPTY: return "RE_STAR_EMPTY";
     103                 :          1 :     case Rewrite::RE_STAR_EMPTY_STRING: return "RE_STAR_EMPTY_STRING";
     104                 :          1 :     case Rewrite::RE_STAR_NESTED_STAR: return "RE_STAR_NESTED_STAR";
     105                 :          1 :     case Rewrite::RE_STAR_UNION: return "RE_STAR_UNION";
     106                 :          1 :     case Rewrite::RE_STAR_UNION_CHAR: return "RE_STAR_UNION_CHAR";
     107                 :          1 :     case Rewrite::REPL_CHAR_NCONTRIB_FIND: return "REPL_CHAR_NCONTRIB_FIND";
     108                 :          1 :     case Rewrite::REPL_DUAL_REPL_ITE: return "REPL_DUAL_REPL_ITE";
     109                 :          1 :     case Rewrite::REPL_REPL_SHORT_CIRCUIT: return "REPL_REPL_SHORT_CIRCUIT";
     110                 :          1 :     case Rewrite::REPL_REPL2_INV: return "REPL_REPL2_INV";
     111                 :          1 :     case Rewrite::REPL_REPL2_INV_ID: return "REPL_REPL2_INV_ID";
     112                 :          1 :     case Rewrite::REPL_REPL3_INV: return "REPL_REPL3_INV";
     113                 :          1 :     case Rewrite::REPL_REPL3_INV_ID: return "REPL_REPL3_INV_ID";
     114                 :          1 :     case Rewrite::REPL_SUBST_IDX: return "REPL_SUBST_IDX";
     115                 :          1 :     case Rewrite::REPLALL_CONST: return "REPLALL_CONST";
     116                 :          1 :     case Rewrite::REPLALL_EMPTY_FIND: return "REPLALL_EMPTY_FIND";
     117                 :          1 :     case Rewrite::RPL_CCTN: return "RPL_CCTN";
     118                 :          1 :     case Rewrite::RPL_CCTN_RPL: return "RPL_CCTN_RPL";
     119                 :          1 :     case Rewrite::RPL_CONST_FIND: return "RPL_CONST_FIND";
     120                 :          1 :     case Rewrite::RPL_CONST_NFIND: return "RPL_CONST_NFIND";
     121                 :          1 :     case Rewrite::RPL_ID: return "RPL_ID";
     122                 :          1 :     case Rewrite::RPL_NCTN: return "RPL_NCTN";
     123                 :          1 :     case Rewrite::RPL_PULL_ENDPT: return "RPL_PULL_ENDPT";
     124                 :          1 :     case Rewrite::RPL_REPLACE: return "RPL_REPLACE";
     125                 :          1 :     case Rewrite::RPL_RPL_EMPTY: return "RPL_RPL_EMPTY";
     126                 :          1 :     case Rewrite::RPL_RPL_LEN_ID: return "RPL_RPL_LEN_ID";
     127                 :          1 :     case Rewrite::REPLACE_RE_EVAL: return "REPLACE_RE_EVAL";
     128                 :          1 :     case Rewrite::REPLACE_RE_NONE: return "REPLACE_RE_NONE";
     129                 :          1 :     case Rewrite::REPLACE_RE_ALL_EVAL: return "REPLACE_RE_ALL_EVAL";
     130                 :          1 :     case Rewrite::REPLACE_RE_ALL_NONE: return "REPLACE_RE_ALL_NONE";
     131                 :          1 :     case Rewrite::REPLACE_RE_EMP_RE: return "REPLACE_RE_EMP_RE";
     132                 :          1 :     case Rewrite::SPLIT_EQ: return "SPLIT_EQ";
     133                 :          1 :     case Rewrite::SPLIT_EQ_STRIP_L: return "SPLIT_EQ_STRIP_L";
     134                 :          1 :     case Rewrite::SPLIT_EQ_STRIP_R: return "SPLIT_EQ_STRIP_R";
     135                 :          1 :     case Rewrite::SS_COMBINE_EQ: return "SS_COMBINE_EQ";
     136                 :          1 :     case Rewrite::SS_COMBINE_GEQ_INNER: return "SS_COMBINE_GEQ_INNER";
     137                 :          1 :     case Rewrite::SS_COMBINE_GEQ_OUTER: return "SS_COMBINE_GEQ_OUTER";
     138                 :          1 :     case Rewrite::SS_CONST_END_OOB: return "SS_CONST_END_OOB";
     139                 :          1 :     case Rewrite::SS_CONST_LEN_MAX_OOB: return "SS_CONST_LEN_MAX_OOB";
     140                 :          1 :     case Rewrite::SS_CONST_LEN_NON_POS: return "SS_CONST_LEN_NON_POS";
     141                 :          1 :     case Rewrite::SS_CONST_SS: return "SS_CONST_SS";
     142                 :          1 :     case Rewrite::SS_CONST_START_MAX_OOB: return "SS_CONST_START_MAX_OOB";
     143                 :          1 :     case Rewrite::SS_CONST_START_NEG: return "SS_CONST_START_NEG";
     144                 :          1 :     case Rewrite::SS_CONST_START_OOB: return "SS_CONST_START_OOB";
     145                 :          1 :     case Rewrite::SS_EMPTYSTR: return "SS_EMPTYSTR";
     146                 :          1 :     case Rewrite::SS_END_PT_NORM: return "SS_END_PT_NORM";
     147                 :          1 :     case Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S:
     148                 :          1 :       return "SS_GEQ_ZERO_START_ENTAILS_EMP_S";
     149                 :          1 :     case Rewrite::SS_LEN_INCLUDE: return "SS_LEN_INCLUDE";
     150                 :          1 :     case Rewrite::SS_LEN_NON_POS: return "SS_LEN_NON_POS";
     151                 :          1 :     case Rewrite::SS_LEN_ONE_Z_Z: return "SS_LEN_ONE_Z_Z";
     152                 :          1 :     case Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB:
     153                 :          1 :       return "SS_NON_ZERO_LEN_ENTAILS_OOB";
     154                 :          1 :     case Rewrite::SS_START_ENTAILS_ZERO_LEN: return "SS_START_ENTAILS_ZERO_LEN";
     155                 :          1 :     case Rewrite::SS_START_GEQ_LEN: return "SS_START_GEQ_LEN";
     156                 :          1 :     case Rewrite::SS_START_NEG: return "SS_START_NEG";
     157                 :          1 :     case Rewrite::SS_STRIP_END_PT: return "SS_STRIP_END_PT";
     158                 :          1 :     case Rewrite::SS_STRIP_START_PT: return "SS_STRIP_START_PT";
     159                 :          1 :     case Rewrite::UPD_EVAL: return "UPD_EVAL";
     160                 :          1 :     case Rewrite::UPD_EVAL_SYM: return "UPD_EVAL_SYM";
     161                 :          1 :     case Rewrite::UPD_EMPTYSTR: return "UPD_EMPTYSTR";
     162                 :          1 :     case Rewrite::UPD_CONST_INDEX_MAX_OOB: return "UPD_CONST_INDEX_MAX_OOB";
     163                 :          1 :     case Rewrite::UPD_CONST_INDEX_NEG: return "UPD_CONST_INDEX_NEG";
     164                 :          1 :     case Rewrite::UPD_CONST_INDEX_OOB: return "UPD_CONST_INDEX_OOB";
     165                 :          1 :     case Rewrite::UPD_REV: return "UPD_REV";
     166                 :          1 :     case Rewrite::UPD_OOB: return "UPD_OOB";
     167                 :          1 :     case Rewrite::STOI_CONCAT_NONNUM: return "STOI_CONCAT_NONNUM";
     168                 :          1 :     case Rewrite::STOI_EVAL: return "STOI_EVAL";
     169                 :          1 :     case Rewrite::STR_CONV_CONST: return "STR_CONV_CONST";
     170                 :          1 :     case Rewrite::STR_CONV_IDEM: return "STR_CONV_IDEM";
     171                 :          1 :     case Rewrite::STR_CONV_ITOS: return "STR_CONV_ITOS";
     172                 :          1 :     case Rewrite::STR_CONV_MINSCOPE_CONCAT: return "STR_CONV_MINSCOPE_CONCAT";
     173                 :          1 :     case Rewrite::STR_EMP_REPL_EMP: return "STR_EMP_REPL_EMP";
     174                 :          1 :     case Rewrite::STR_EMP_REPL_EMP_R: return "STR_EMP_REPL_EMP_R";
     175                 :          1 :     case Rewrite::STR_EMP_REPL_X_Y_X: return "STR_EMP_REPL_X_Y_X";
     176                 :          1 :     case Rewrite::STR_EMP_SUBSTR_ELIM: return "STR_EMP_SUBSTR_ELIM";
     177                 :          1 :     case Rewrite::STR_EMP_SUBSTR_LEQ_LEN: return "STR_EMP_SUBSTR_LEQ_LEN";
     178                 :          1 :     case Rewrite::STR_EMP_SUBSTR_LEQ_Z: return "STR_EMP_SUBSTR_LEQ_Z";
     179                 :          1 :     case Rewrite::STR_EQ_CONJ_LEN_ENTAIL: return "STR_EQ_CONJ_LEN_ENTAIL";
     180                 :          1 :     case Rewrite::STR_EQ_REPL_EMP: return "STR_EQ_REPL_EMP";
     181                 :          1 :     case Rewrite::STR_EQ_REPL_NOT_CTN: return "STR_EQ_REPL_NOT_CTN";
     182                 :          1 :     case Rewrite::STR_EQ_REPL_TO_DIS: return "STR_EQ_REPL_TO_DIS";
     183                 :          1 :     case Rewrite::STR_EQ_REPL_TO_EQ: return "STR_EQ_REPL_TO_EQ";
     184                 :          1 :     case Rewrite::STR_EQ_UNIFY: return "STR_EQ_UNIFY";
     185                 :          1 :     case Rewrite::STR_LEQ_CPREFIX: return "STR_LEQ_CPREFIX";
     186                 :          1 :     case Rewrite::STR_LEQ_EMPTY: return "STR_LEQ_EMPTY";
     187                 :          1 :     case Rewrite::STR_LEQ_EVAL: return "STR_LEQ_EVAL";
     188                 :          1 :     case Rewrite::STR_LEQ_ID: return "STR_LEQ_ID";
     189                 :          1 :     case Rewrite::STR_REV_CONST: return "STR_REV_CONST";
     190                 :          1 :     case Rewrite::STR_REV_IDEM: return "STR_REV_IDEM";
     191                 :          1 :     case Rewrite::STR_REV_UNIT: return "STR_REV_UNIT";
     192                 :          1 :     case Rewrite::STR_REV_MINSCOPE_CONCAT: return "STR_REV_MINSCOPE_CONCAT";
     193                 :          1 :     case Rewrite::SUBSTR_REPL_SWAP: return "SUBSTR_REPL_SWAP";
     194                 :          1 :     case Rewrite::SUF_PREFIX_CONST: return "SUF_PREFIX_CONST";
     195                 :          1 :     case Rewrite::SUF_PREFIX_CTN: return "SUF_PREFIX_CTN";
     196                 :          1 :     case Rewrite::SUF_PREFIX_EMPTY: return "SUF_PREFIX_EMPTY";
     197                 :          1 :     case Rewrite::SUF_PREFIX_EMPTY_CONST: return "SUF_PREFIX_EMPTY_CONST";
     198                 :          1 :     case Rewrite::SUF_PREFIX_EQ: return "SUF_PREFIX_EQ";
     199                 :          1 :     case Rewrite::SUF_PREFIX_TO_EQS: return "SUF_PREFIX_TO_EQS";
     200                 :          1 :     case Rewrite::TO_CODE_EVAL: return "TO_CODE_EVAL";
     201                 :          1 :     case Rewrite::EQ_REFL: return "EQ_REFL";
     202                 :          1 :     case Rewrite::EQ_CONST_FALSE: return "EQ_CONST_FALSE";
     203                 :          1 :     case Rewrite::EQ_SYM: return "EQ_SYM";
     204                 :          1 :     case Rewrite::CONCAT_NORM: return "CONCAT_NORM";
     205                 :          1 :     case Rewrite::IS_DIGIT_ELIM: return "IS_DIGIT_ELIM";
     206                 :          1 :     case Rewrite::RE_CONCAT_EMPTY: return "RE_CONCAT_EMPTY";
     207                 :          1 :     case Rewrite::RE_IN_EMPTY: return "RE_IN_EMPTY";
     208                 :          1 :     case Rewrite::RE_IN_SIGMA: return "RE_IN_SIGMA";
     209                 :          1 :     case Rewrite::RE_IN_EVAL: return "RE_IN_EVAL";
     210                 :          1 :     case Rewrite::RE_IN_COMPLEMENT: return "RE_IN_COMPLEMENT";
     211                 :          1 :     case Rewrite::RE_IN_RANGE: return "RE_IN_RANGE";
     212                 :          1 :     case Rewrite::RE_IN_CSTRING: return "RE_IN_CSTRING";
     213                 :          1 :     case Rewrite::RE_IN_ANDOR: return "RE_IN_ANDOR";
     214                 :          1 :     case Rewrite::RE_REPEAT_ELIM: return "RE_REPEAT_ELIM";
     215                 :          1 :     case Rewrite::SUF_PREFIX_ELIM: return "SUF_PREFIX_ELIM";
     216                 :          1 :     case Rewrite::STR_LT_ELIM: return "STR_LT_ELIM";
     217                 :          1 :     case Rewrite::RE_RANGE_SINGLE: return "RE_RANGE_SINGLE";
     218                 :          1 :     case Rewrite::RE_RANGE_EMPTY: return "RE_RANGE_EMPTY";
     219                 :          1 :     case Rewrite::RE_RANGE_NON_SINGLETON: return "RE_RANGE_NON_SINGLETON";
     220                 :          1 :     case Rewrite::RE_OPT_ELIM: return "RE_OPT_ELIM";
     221                 :          1 :     case Rewrite::RE_PLUS_ELIM: return "RE_PLUS_ELIM";
     222                 :          1 :     case Rewrite::RE_DIFF_ELIM: return "RE_DIFF_ELIM";
     223                 :          1 :     case Rewrite::LEN_EVAL: return "LEN_EVAL";
     224                 :          1 :     case Rewrite::LEN_CONCAT: return "LEN_CONCAT";
     225                 :          1 :     case Rewrite::LEN_REPL_INV: return "LEN_REPL_INV";
     226                 :          1 :     case Rewrite::LEN_CONV_INV: return "LEN_CONV_INV";
     227                 :          1 :     case Rewrite::LEN_SEQ_UNIT: return "LEN_SEQ_UNIT";
     228                 :          1 :     case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM";
     229                 :          1 :     case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL";
     230                 :          1 :     case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL";
     231                 :          1 :     case Rewrite::SEQ_NTH_EVAL_OOB: return "SEQ_NTH_EVAL_OOB";
     232                 :          1 :     case Rewrite::SEQ_NTH_EVAL_SYM: return "SEQ_NTH_EVAL_SYM";
     233                 :          0 :     case Rewrite::UNKNOWN: return "?";
     234                 :          0 :     default:
     235                 :          0 :       DebugUnhandled() << "No print for rewrite " << static_cast<size_t>(r);
     236                 :            :       return "?Unhandled";
     237                 :            :   }
     238                 :            : }
     239                 :            : 
     240                 :        202 : std::ostream& operator<<(std::ostream& out, Rewrite r)
     241                 :            : {
     242                 :        202 :   out << toString(r);
     243                 :        202 :   return out;
     244                 :            : }
     245                 :            : 
     246                 :            : }  // namespace strings
     247                 :            : }  // namespace theory
     248                 :            : }  // namespace cvc5::internal