Add lazy approach for handling lambdas in the HO extension (#7625)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 11 Nov 2021 19:41:14 +0000 (13:41 -0600)
committerGitHub <noreply@github.com>
Thu, 11 Nov 2021 19:41:14 +0000 (19:41 +0000)
commit698ac133984800d12f072f6cdcab3196c3656e6e
treeadfb3bc203f3c139c6eca6950fd116a57732341d
parentd6fd1eff6025be9f0d8d5e7dcb02bffdda931828
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.
19 files changed:
src/CMakeLists.txt
src/api/cpp/cvc5_kind.h
src/smt/term_formula_removal.cpp
src/theory/inference_id.cpp
src/theory/inference_id.h
src/theory/uf/ho_extension.cpp
src/theory/uf/ho_extension.h
src/theory/uf/kinds
src/theory/uf/lambda_lift.cpp
src/theory/uf/lambda_lift.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
test/regress/CMakeLists.txt
test/regress/regress0/ho/lazy-lambda-model.smt2 [new file with mode: 0644]
test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 [new file with mode: 0644]
test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2 [new file with mode: 0644]
test/regress/regress1/bags/map-lazy-lam.smt2 [new file with mode: 0644]
test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
test/regress/regress1/ho/ho-fun-sharing-dd.smt2 [new file with mode: 0644]