From d4046f5e2e32d07c34b65fbcdfffae6a24d8c399 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Mar 2019 15:47:48 -0500 Subject: [PATCH] Properly handle lambdas in relevant domain (#2853) --- src/expr/node.h | 7 +++---- src/theory/quantifiers/relevant_domain.cpp | 4 +++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/expr/node.h b/src/expr/node.h index 750a5547b..50add7b17 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -470,10 +470,9 @@ public: inline bool isClosure() const { assertTNodeNotExpired(); - return getKind() == kind::LAMBDA || - getKind() == kind::FORALL || - getKind() == kind::EXISTS || - getKind() == kind::REWRITE_RULE; + return getKind() == kind::LAMBDA || getKind() == kind::FORALL + || getKind() == kind::EXISTS || getKind() == kind::REWRITE_RULE + || getKind() == kind::CHOICE; } /** diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 849e73822..76fe892e8 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -169,7 +169,9 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po computeRelevantDomainOpCh( rf, n[i] ); } } - if( n[i].getKind()!=FORALL ){ + // do not recurse under nested closures + if (!n[i].isClosure()) + { bool newHasPol; bool newPol; QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); -- 2.30.2