src/theory/strings/rewrites.h

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