From 0f46eb0eec073b27e5517c5d8ccba93a5c9ba526 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 15 May 2020 08:09:14 -0500 Subject: Doc --- src/theory/strings/infer_info.h | 2 ++ 1 file changed, 2 insertions(+) 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: -- cgit v1.2.3