diff options
Diffstat (limited to 'src/theory/inference_id.h')
-rw-r--r-- | src/theory/inference_id.h | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index cebf02c9d..ad879d7ab 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -169,9 +169,7 @@ enum class InferenceId // ---------------------------------- bags theory BAGS_NON_NEGATIVE_COUNT, - BAGS_MK_BAG_DIFFERENT_ELEMENT, - BAGS_MK_BAG_SAME_ELEMENT, - BAGS_MK_BAG, + BAGS_BAG_MAKE, BAGS_EQUALITY, BAGS_DISEQUALITY, BAGS_EMPTY, @@ -840,6 +838,15 @@ enum class InferenceId // different applications // (not (= (f sk1 .. skn) (g sk1 .. skn)) UF_HO_MODEL_EXTENSIONALITY, + // equivalence of lambda functions + // f = g => forall x. reduce(lambda(f)(x)) = reduce(lambda(g)(x)) + // This is applied when lamda functions f and g are in the same eq class. + UF_HO_LAMBDA_UNIV_EQ, + // equivalence of a lambda function and an ordinary function + // f = h => h(t) = reduce(lambda(f)(t)) + // This is applied when lamda function f and ordinary function h are in the + // same eq class. + UF_HO_LAMBDA_APP_REDUCE, //-------------------- end model-construction specific part //-------------------- end HO extension to UF //-------------------------------------- end uf theory |