diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-15 08:09:14 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-15 08:09:14 -0500 |
| commit | 0f46eb0eec073b27e5517c5d8ccba93a5c9ba526 (patch) | |
| tree | b4ff898c5dc1d284c4f85af877ff785eb24cb645 | |
| parent | 9248f9d2b22c28c84774f31f58598c46d24f96f6 (diff) | |
Doc
| -rw-r--r-- | src/theory/strings/infer_info.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 6503fd12f..5aecf52cb 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -93,6 +93,8 @@ enum class Inference : uint32_t // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false 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: |