diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-17 16:10:43 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 16:10:43 +0100 |
commit | f52cd17ba0f9c455db1d45341ba39f04b319e621 (patch) | |
tree | f74b8241764dc2d7ecfc026ba60516b5211dc701 /src/theory/inference_id.h | |
parent | fb5e3113312322c21a00062b22c358c30fa27101 (diff) |
TheoryIds for UF theory. (#5901)
This PR introduces new InferenceId for the uf theory and uses them instead of InferenceId::UNKNOWN.
Diffstat (limited to 'src/theory/inference_id.h')
-rw-r--r-- | src/theory/inference_id.h | 35 |
1 files changed, 34 insertions, 1 deletions
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index f28faa037..a48a8c366 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -404,7 +404,40 @@ enum class InferenceId STRINGS_PREFIX_CONFLICT, //-------------------------------------- end prefix conflict - UNKNOWN, + // Clause from the uf symmetry breaker + UF_BREAK_SYMMETRY, + UF_CARD_CLIQUE, + UF_CARD_COMBINED, + UF_CARD_ENFORCE_NEGATIVE, + UF_CARD_EQUIV, + UF_CARD_MONOTONE_COMBINED, + UF_CARD_SIMPLE_CONFLICT, + UF_CARD_SPLIT, + //-------------------------------------- begin HO extension to UF + // Encodes an n-ary application as a chain of binary HO_APPLY applications + // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn)) + UF_HO_APP_ENCODE, + UF_HO_APP_CONV_SKOLEM, + // Adds an extensionality lemma to witness that disequal functions have + // different applications + // (not (= (f sk1 .. skn) (g sk1 .. skn)) + UF_HO_EXTENSIONALITY, + //-------------------------------------- begin model-construction specific part + // These rules are necessary to ensure that we build models properly. For more + // details see Section 3.3 of Barbosa et al. CADE'19. + // + // Enforces that a regular APPLY_UF term in the model is equal to its HO_APPLY + // equivalent by adding the equality as a lemma + // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn)) + UF_HO_MODEL_APP_ENCODE, + // Adds an extensionality lemma to witness that disequal functions have + // different applications + // (not (= (f sk1 .. skn) (g sk1 .. skn)) + UF_HO_MODEL_EXTENSIONALITY, + //-------------------------------------- end model-construction specific part + //-------------------------------------- end HO extension to UF + + UNKNOWN }; /** |