From 2d071aa5cfd697cab7177cd3b520a87aaf0049dd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Nov 2021 15:40:36 -0600 Subject: [PATCH] Only eliminate lambdas in higher-order elimination if ho-elim is enabled (#7603) Required for lazy lambdas in HO. Also properly guards the case when the preprocessing pass is a no-op. --- src/preprocessing/passes/ho_elim.cpp | 103 +++++++++++++++------------ test/regress/CMakeLists.txt | 3 +- 2 files changed, 58 insertions(+), 48 deletions(-) diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index d3372a28e..e122b33d6 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -305,67 +305,76 @@ Node HoElim::eliminateHo(Node n) PreprocessingPassResult HoElim::applyInternal( AssertionPipeline* assertionsToPreprocess) { + // this preprocessing pass is only applicable if we are eliminating + // higher-order, or are adding the store axiom + if (!options().quantifiers.hoElim && !options().quantifiers.hoElimStoreAx) + { + return PreprocessingPassResult::NO_CONFLICT; + } // step [1]: apply lambda lifting to eliminate all lambdas NodeManager* nm = NodeManager::currentNM(); std::vector axioms; - std::map newLambda; - for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + if (options().quantifiers.hoElim) { - Node prev = (*assertionsToPreprocess)[i]; - Node res = eliminateLambdaComplete(prev, newLambda); - if (res != prev) + std::map newLambda; + for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { - res = rewrite(res); - Assert(!expr::hasFreeVar(res)); - assertionsToPreprocess->replace(i, res); + Node prev = (*assertionsToPreprocess)[i]; + Node res = eliminateLambdaComplete(prev, newLambda); + if (res != prev) + { + res = rewrite(res); + Assert(!expr::hasFreeVar(res)); + assertionsToPreprocess->replace(i, res); + } } - } - // do lambda lifting on new lambda definitions - // this will do fixed point to eliminate lambdas within lambda lifting axioms. - while (!newLambda.empty()) - { - std::map lproc = newLambda; - newLambda.clear(); - for (const std::pair& l : lproc) + // do lambda lifting on new lambda definitions + // this will do fixed point to eliminate lambdas within lambda lifting axioms. + while (!newLambda.empty()) { - Node lambda = l.second; - std::vector vars; - std::vector nvars; - for (const Node& v : lambda[0]) + std::map lproc = newLambda; + newLambda.clear(); + for (const std::pair& l : lproc) { - Node bv = nm->mkBoundVar(v.getType()); - vars.push_back(v); - nvars.push_back(bv); - } + Node lambda = l.second; + std::vector vars; + std::vector nvars; + for (const Node& v : lambda[0]) + { + Node bv = nm->mkBoundVar(v.getType()); + vars.push_back(v); + nvars.push_back(bv); + } - Node bd = lambda[1].substitute( - vars.begin(), vars.end(), nvars.begin(), nvars.end()); - Node bvl = nm->mkNode(BOUND_VAR_LIST, nvars); + Node bd = lambda[1].substitute( + vars.begin(), vars.end(), nvars.begin(), nvars.end()); + Node bvl = nm->mkNode(BOUND_VAR_LIST, nvars); - nvars.insert(nvars.begin(), l.first); - Node curr = nm->mkNode(APPLY_UF, nvars); + nvars.insert(nvars.begin(), l.first); + Node curr = nm->mkNode(APPLY_UF, nvars); - Node llfax = nm->mkNode(FORALL, bvl, curr.eqNode(bd)); - Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax - << " for " << lambda << std::endl; - Assert(!expr::hasFreeVar(llfax)); - Node llfaxe = eliminateLambdaComplete(llfax, newLambda); - Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for " - << lambda << std::endl; - axioms.push_back(llfaxe); + Node llfax = nm->mkNode(FORALL, bvl, curr.eqNode(bd)); + Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax + << " for " << lambda << std::endl; + Assert(!expr::hasFreeVar(llfax)); + Node llfaxe = eliminateLambdaComplete(llfax, newLambda); + Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for " + << lambda << std::endl; + axioms.push_back(llfaxe); + } } - } - d_visited.clear(); - // add lambda lifting axioms as a conjunction to the first assertion - if (!axioms.empty()) - { - Node conj = nm->mkAnd(axioms); - conj = rewrite(conj); - Assert(!expr::hasFreeVar(conj)); - assertionsToPreprocess->conjoin(0, conj); + d_visited.clear(); + // add lambda lifting axioms as a conjunction to the first assertion + if (!axioms.empty()) + { + Node conj = nm->mkAnd(axioms); + conj = rewrite(conj); + Assert(!expr::hasFreeVar(conj)); + assertionsToPreprocess->conjoin(0, conj); + } + axioms.clear(); } - axioms.clear(); // step [2]: eliminate all higher-order constraints for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 23ef3936c..b08b2f6f5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1725,7 +1725,6 @@ set(regress_1_tests regress1/fmf/sort-inf-int.smt2 regress1/fmf/with-ind-104-core.smt2 regress1/gensys_brn001.smt2 - regress1/ho/bug_freevar_PHI004^4-delta.smt2 regress1/ho/bug_freeVar_BDD_General_data_270.p regress1/ho/bound_var_bug.p regress1/ho/fta0328.lfho.p @@ -2804,6 +2803,8 @@ 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 -- 2.30.2