From 698ac133984800d12f072f6cdcab3196c3656e6e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Nov 2021 13:41:14 -0600 Subject: Add lazy approach for handling lambdas in the HO extension (#7625) This adds a new option --uf-lazy-ll for not applying lambda lifting eagerly. This is motivated by HO operators in theory of bags, e.g. bag.map, which cannot answer "sat" for simple problems where lambdas are mapped to bags, due to the introduction of quantified formulas for eliminating lambdas. It moves lambda lifting from term formula removal to a utility module within TheoryUF. If lazy lambda lifting is enabled, this module does not introduce quantified formulas for lambdas eagerly. It adds 2 lemma schemas for reasoning about quantifier-free constraints with lambdas natively in TheoryUF. It extends the model construction in the HoExtension to assign lambdas in the case that an equivalence class contains a variable that is defined by a lambda. --- src/api/cpp/cvc5_kind.h | 4 ---- 1 file changed, 4 deletions(-) (limited to 'src/api/cpp/cvc5_kind.h') diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 90a57317d..c0c269be2 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -331,10 +331,6 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ CARDINALITY_CONSTRAINT, -#if 0 - /* Partial uninterpreted function application. */ - PARTIAL_APPLY_UF, -#endif /** * Higher-order applicative encoding of function application, left * associative. -- cgit v1.2.3