diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-17 16:50:15 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-17 16:50:15 +0100 |
| commit | bdc1b222fbc674ab1f8a48fad9f78759c3baea23 (patch) | |
| tree | 70bee6724c49f351fb31cd9cfe6b1fa196654ba1 /src/theory/inference_id.h | |
| parent | f52cd17ba0f9c455db1d45341ba39f04b319e621 (diff) | |
Use InferenceId in sep theory. (#5912)
This PR uses the new InferenceIds in the separation logic theory.
Diffstat (limited to 'src/theory/inference_id.h')
| -rw-r--r-- | src/theory/inference_id.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index a48a8c366..bb69f5d7f 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -135,6 +135,11 @@ enum class InferenceId // cycle conflict for datatypes DATATYPES_CYCLE, + // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w + SEP_PTO_NEG_PROP, + // enforces injectiveness of pto: (pto x y) ^ (pto y w) ^ x = y => y = w + SEP_PTO_PROP, + //-------------------------------------- base solver // initial normalize singular // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" => |