diff options
Diffstat (limited to 'src/theory/strings/infer_info.h')
| -rw-r--r-- | src/theory/strings/infer_info.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 1b190a2db..b7e292226 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -107,6 +107,10 @@ enum class Inference : uint32_t // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false // Proof: substitution+rewriting, CTN_NOT_EQUAL F_NCTN, + // Normal form equality conflict + // x = N[x] ^ y = N[y] ^ x=y => false + // where Rewriter::rewrite(N[x]=N[y]) = false. + N_EQ_CONF, // Given two normal forms, infers that the remainder one of them has to be // empty. For example: // If x1 ++ x2 = y1 and x1 = y1, then x2 = "" |