diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-14 15:47:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-14 15:47:48 -0500 |
| commit | d4046f5e2e32d07c34b65fbcdfffae6a24d8c399 (patch) | |
| tree | 540ed4261b428b7e34ec32ed8652c07a062c7457 /src | |
| parent | 7247f321dc8d319c5079b31d450c09029506274a (diff) | |
Properly handle lambdas in relevant domain (#2853)
Diffstat (limited to 'src')
| -rw-r--r-- | src/expr/node.h | 7 | ||||
| -rw-r--r-- | 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 ); |