diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-02 14:54:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-02 14:54:37 -0500 |
| commit | 493bf7a8619e5779604fb73aa6a0b7000a529d6a (patch) | |
| tree | 22b48c59eb59b587da5b6f353568f056f9508ffd | |
| parent | bf040e895716b3f38a5ef92e3412e7615d96bc5f (diff) | |
Fix candidate rewrite utilities for non-first-class types (#2256)
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_filter.cpp | 21 | ||||
| -rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.cpp | 4 |
2 files changed, 19 insertions, 6 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index bf2248e25..c49557fa9 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -161,6 +161,7 @@ bool MatchTrie::getMatches(Node n, NotifyMatch* ntm) void MatchTrie::addTerm(Node n) { + Assert(!n.isNull()); std::vector<Node> visit; visit.push_back(n); MatchTrie* curr = this; @@ -301,13 +302,18 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n << "]..." << std::endl; Node bni = d_drewrite->toInternal(bn); - if (!d_match_trie.getMatches(bni, &d_ssenm)) + if (!bni.isNull()) { - keep = false; - Trace("cr-filter") << "...redundant (matchable)" << std::endl; - // regardless, would help to remember it - registerRelevantPair(n, eq_n); + if (!d_match_trie.getMatches(bni, &d_ssenm)) + { + keep = false; + Trace("cr-filter") << "...redundant (matchable)" << std::endl; + // regardless, would help to remember it + registerRelevantPair(n, eq_n); + } } + // if bni is null, it may involve non-first-class types that we cannot + // reason about } if (keep) @@ -356,7 +362,10 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) { Trace("crf-match") << "CRF add term : " << t << std::endl; Node ti = d_drewrite->toInternal(t); - d_match_trie.addTerm(ti); + if (!ti.isNull()) + { + d_match_trie.addTerm(ti); + } } d_pairs[t].insert(to); } diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index d8c5ac7b5..f48f73aee 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -109,6 +109,10 @@ Node DynamicRewriter::toInternal(Node a) for (const Node& ca : a) { Node cai = toInternal(ca); + if (cai.isNull()) + { + return Node::null(); + } children.push_back(cai); } if (!children.empty()) |