diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-11 13:41:14 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-11 19:41:14 +0000 |
| commit | 698ac133984800d12f072f6cdcab3196c3656e6e (patch) | |
| tree | adfb3bc203f3c139c6eca6950fd116a57732341d /src/api/cpp/cvc5_kind.h | |
| parent | d6fd1eff6025be9f0d8d5e7dcb02bffdda931828 (diff) | |
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.
Diffstat (limited to 'src/api/cpp/cvc5_kind.h')
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 4 |
1 files changed, 0 insertions, 4 deletions
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<Term>& children) const` */ CARDINALITY_CONSTRAINT, -#if 0 - /* Partial uninterpreted function application. */ - PARTIAL_APPLY_UF, -#endif /** * Higher-order applicative encoding of function application, left * associative. |