diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-30 18:15:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-30 18:15:07 -0500 |
| commit | bc4055d4543f3b697ade38b810f7ac3cf02dc3c8 (patch) | |
| tree | f66e1d9788fb9e7a5fbc1dfb98699da8f0298c92 /src/theory/strings/rewrites.h | |
| parent | 6838885b1250e0abbb1b8d56e6b400a5d7f3ca95 (diff) | |
Rewrites for all remaining return statements in strings rewriter (#4178)
Towards proofs for string rewrites. All return statements all now associated with an enum value.
An indentation in a block of code changed in rewriteMembership.
Diffstat (limited to 'src/theory/strings/rewrites.h')
| -rw-r--r-- | src/theory/strings/rewrites.h | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index 91d52197c..cfa8c8448 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -172,7 +172,36 @@ enum class Rewrite : uint32_t SUF_PREFIX_EMPTY_CONST, SUF_PREFIX_EQ, SUF_PREFIX_TO_EQS, - TO_CODE_EVAL + TO_CODE_EVAL, + EQ_REFL, + EQ_CONST_FALSE, + EQ_SYM, + CONCAT_NORM, + IS_DIGIT_ELIM, + RE_CONCAT_EMPTY, + RE_CONSUME_CCONF, + RE_CONSUME_S, + RE_CONSUME_S_CCONF, + RE_CONSUME_S_FULL, + RE_IN_EMPTY, + RE_IN_SIGMA, + RE_IN_EVAL, + RE_IN_COMPLEMENT, + RE_IN_RANGE, + RE_IN_CSTRING, + RE_IN_ANDOR, + RE_REPEAT_ELIM, + SUF_PREFIX_ELIM, + STR_LT_ELIM, + RE_RANGE_SINGLE, + RE_OPT_ELIM, + RE_PLUS_ELIM, + RE_DIFF_ELIM, + LEN_EVAL, + LEN_CONCAT, + LEN_REPL_INV, + LEN_CONV_INV, + CHARAT_ELIM }; /** |