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 /test/regress/CMakeLists.txt | |
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 'test/regress/CMakeLists.txt')
-rw-r--r-- | test/regress/CMakeLists.txt | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d9076c81b..4937c8481 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -660,11 +660,14 @@ set(regress_0_tests regress0/ho/issue6536.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 + regress0/ho/lazy-lambda-model.smt2 regress0/ho/match-middle.smt2 regress0/ho/modulo-func-equality.smt2 regress0/ho/qgu-fuzz-ho-1-dd.smt2 regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 regress0/ho/shadowing-defs.smt2 + regress0/ho/simple-conf-lazy-lambda-lift.smt2 + regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 regress0/ho/simple-matching-partial.smt2 regress0/ho/simple-matching.smt2 regress0/ho/trans.smt2 @@ -1604,6 +1607,7 @@ set(regress_1_tests regress1/bags/intersection_min1.smt2 regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 + regress1/bags/map-lazy-lam.smt2 regress1/bags/map1.smt2 regress1/bags/map2.smt2 regress1/bags/map3.smt2 @@ -1728,8 +1732,10 @@ set(regress_1_tests regress1/fmf/with-ind-104-core.smt2 regress1/gensys_brn001.smt2 regress1/ho/bug_freeVar_BDD_General_data_270.p + regress1/ho/bug_freevar_PHI004^4-delta.smt2 regress1/ho/bound_var_bug.p regress1/ho/fta0328.lfho.p + regress1/ho/ho-fun-sharing-dd.smt2 regress1/ho/issue3136-fconst-bool-bool.smt2 regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 @@ -2805,8 +2811,6 @@ set(regression_disabled_tests ### regress1/bug472.smt2 regress1/datatypes/non-simple-rec-set.smt2 - # disabled temporarily until lazy lambda handling is merged - regress1/ho/bug_freevar_PHI004^4-delta.smt2 # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 # after disallowing solving for terms with quantifiers |