diff options
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 8e3304b6a..49bbe5680 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -56,12 +56,12 @@ RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() { } } -void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) { +void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) { std::map< Node, Node > rterms; for( unsigned i=0; i<d_terms.size(); i++ ){ Node r = d_terms[i]; if( !TermDb::hasInstConstAttr( d_terms[i] ) ){ - r = fm->getRepresentative( d_terms[i] ); + r = qe->getEqualityQuery()->getRepresentative( d_terms[i] ); } if( rterms.find( r )==rterms.end() ){ rterms[r] = d_terms[i]; @@ -132,7 +132,7 @@ void RelevantDomain::compute(){ RDomain * r = it2->second; RDomain * rp = r->getParent(); if( r==rp ){ - r->removeRedundantTerms( d_model ); + r->removeRedundantTerms( d_qe ); for( unsigned i=0; i<r->d_terms.size(); i++ ){ Trace("rel-dom") << r->d_terms[i] << " "; } @@ -190,7 +190,7 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { }else if( varCount==1 ){ int oCh = varCh==0 ? 1 : 0; bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] ); - Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << std::endl; + Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << ", pol = " << pol << ", hasPol = " << hasPol << ", kind = " << n.getKind() << std::endl; //the negative occurrence adds the term to the domain if( !hasPol || !pol ){ rds[varCh]->addTerm( n[oCh], ng ); @@ -202,7 +202,6 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { rds[varCh]->addTerm( QuantArith::offset( n[oCh], i==0 ? 1 : -1 ), ng ); } }else if( n.getKind()==GEQ ){ - Node nt = QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ); rds[varCh]->addTerm( QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ), ng ); } } @@ -228,6 +227,7 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { } } +/* Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) { RDomain * rf = getRDomain( f, i ); Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl; @@ -248,3 +248,4 @@ Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) { return r; } } +*/ |