diff options
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 }; /** |