diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-14 16:27:29 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-14 16:27:29 -0500 |
| commit | c84db60dabd8104928c7261c9df7bd9ef2917e9f (patch) | |
| tree | 25dfaeb4549fc995fddbc2940d94dfe5084e8860 /src/theory/quantifiers/relevant_domain.cpp | |
| parent | c3f7c3c9203a355a9c45bf820e3fea0e29b439de (diff) | |
Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235)
Fixes #4228. That benchmark now times out.
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index fbd1f05a6..6248e9722 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -207,6 +207,7 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { Node q = d_qe->getTermUtil()->getInstConstAttr( n ); //merge the RDomains unsigned id = n.getAttribute(InstVarNumAttribute()); + Assert(q[0][id].getType() == n.getType()); Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q; Trace("rel-dom-debug") << " with body : " << d_qe->getTermUtil()->getInstConstantBody( q ) << std::endl; RDomain * rq = getRDomain( q, id ); @@ -225,9 +226,14 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No d_rel_dom_lit[hasPol][pol][n].d_merge = false; int varCount = 0; int varCh = -1; + TermUtil* tu = d_qe->getTermUtil(); for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( n[i].getKind()==INST_CONSTANT ){ - d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain( q, n[i].getAttribute(InstVarNumAttribute()), false ); + // must get the quantified formula this belongs to, which may be + // different from q + Node qi = tu->getInstConstAttr(n[i]); + unsigned id = n[i].getAttribute(InstVarNumAttribute()); + d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false); varCount++; varCh = i; }else{ |