diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 17:27:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-23 17:27:05 -0500 |
commit | 0faead1572109c1d7cb3d67647da02d0b4600a20 (patch) | |
tree | e0bd28feb049be6a36a63fd73df37f9d3cc7aa54 /src/theory/strings/infer_info.h | |
parent | eaf29fee0871f1b7a8c9cc7c208c6b6d5570bae5 (diff) |
Infer emptiness instead of splitting when a string equality rewrites to a constant (#3218)
Diffstat (limited to 'src/theory/strings/infer_info.h')
-rw-r--r-- | src/theory/strings/infer_info.h | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 9b19eba4b..745a499d3 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -33,10 +33,17 @@ namespace strings { enum Inference { INFER_NONE = 0, + // infer empty, for example: + // (~) x = "" + // This is inferred when we encounter an x such that x = "" rewrites to a + // constant. This inference is used for instance when we otherwise would have + // split on the emptiness of x but the rewriter tells us the emptiness of x + // can be inferred. + INFER_INFER_EMP = 1, // string split constant propagation, for example: // x = y, x = "abc", y = y1 ++ "b" ++ y2 // implies y1 = "a" ++ y1' - INFER_SSPLIT_CST_PROP = 1, + INFER_SSPLIT_CST_PROP, // string split variable propagation, for example: // x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 ) // implies x1 = y1 ++ x1' |