diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-28 09:51:33 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-28 09:51:44 -0600 |
commit | d3822db24e15e255766866a47e6ffa0d8d91911b (patch) | |
tree | 221298973f410f4305f74cd6041b6a017aaa3075 /src/theory/quantifiers/relevant_domain.cpp | |
parent | 587bc5c82e2921a72cec58dc2ec69e3e0ed71866 (diff) |
More optimizations of quantifier instantiation data structures.
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 33d658e0a..5e489c5be 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -140,8 +140,9 @@ void RelevantDomain::compute(){ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( n.getKind()==APPLY_UF ){ - RDomain * rf = getRDomain( n.getOperator(), i ); + Node op = d_qe->getTermDatabase()->getOperator( n ); + if( !op.isNull() ){ + RDomain * rf = getRDomain( op, i ); if( n[i].getKind()==INST_CONSTANT ){ Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] ); //merge the RDomains |