From 59cb18f291e5c3a583f8e8b8b5820ea393bd40ed Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 16 Sep 2021 12:14:07 -0500 Subject: [PATCH] Fix relevant domain for parametric operators (#7198) Fixes #6531. This issue also occurs when using `--full-saturate-quant` on facebook benchmarks that combine multiple sequence types. It does some cleanup on relevant domain in the process. --- src/theory/quantifiers/relevant_domain.cpp | 144 +++++++++++------- src/theory/quantifiers/relevant_domain.h | 12 +- src/theory/quantifiers/term_database.cpp | 2 +- .../quantifiers/term_tuple_enumerator.cpp | 7 +- 4 files changed, 99 insertions(+), 66 deletions(-) diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index f4eb95469..a531d88b7 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -85,20 +85,23 @@ RelevantDomain::RelevantDomain(Env& env, } RelevantDomain::~RelevantDomain() { - for( std::map< Node, std::map< int, RDomain * > >::iterator itr = d_rel_doms.begin(); itr != d_rel_doms.end(); ++itr ){ - for( std::map< int, RDomain * >::iterator itr2 = itr->second.begin(); itr2 != itr->second.end(); ++itr2 ){ - RDomain * current = (*itr2).second; + for (auto& r : d_rel_doms) + { + for (auto& rr : r.second) + { + RDomain* current = rr.second; Assert(current != NULL); delete current; } } } -RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getParent ) { +RelevantDomain::RDomain* RelevantDomain::getRDomain(Node n, + size_t i, + bool getParent) +{ if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){ d_rel_doms[n][i] = new RDomain; - d_rn_map[d_rel_doms[n][i]] = n; - d_ri_map[d_rel_doms[n][i]] = i; } return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i]; } @@ -112,9 +115,11 @@ void RelevantDomain::registerQuantifier(Node q) {} void RelevantDomain::compute(){ if( !d_is_computed ){ d_is_computed = true; - for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){ - for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - it2->second->reset(); + for (auto& r : d_rel_doms) + { + for (auto& rr : r.second) + { + rr.second->reset(); } } FirstOrderModel* fm = d_treg.getModel(); @@ -144,21 +149,37 @@ void RelevantDomain::compute(){ } } //print debug - for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){ - Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl; - for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - Trace("rel-dom") << " " << it2->first << " : "; - RDomain * r = it2->second; + for (std::pair >& d : d_rel_doms) + { + Trace("rel-dom") << "Relevant domain for " << d.first << " : " + << std::endl; + for (std::pair& dd : d.second) + { + Trace("rel-dom") << " " << dd.first << " : "; + RDomain* r = dd.second; RDomain * rp = r->getParent(); if( r==rp ){ r->removeRedundantTerms(d_qs); - for( unsigned i=0; id_terms.size(); i++ ){ - Trace("rel-dom") << r->d_terms[i] << " "; - } + Trace("rel-dom") << r->d_terms; }else{ - Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) "; + Trace("rel-dom") << "Dom( " << d.first << ", " << dd.first << " ) "; } Trace("rel-dom") << std::endl; + if (Configuration::isAssertionBuild()) + { + if (d.first.getKind() == FORALL) + { + TypeNode expectedType = d.first[0][dd.first].getType(); + for (const Node& t : r->d_terms) + { + if (!t.getType().isComparableTo(expectedType)) + { + Unhandled() << "Relevant domain: bad type " << t.getType() + << ", expected " << expectedType; + } + } + } + } } } } @@ -212,7 +233,10 @@ void RelevantDomain::computeRelevantDomainNode(Node q, { Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl; Node op = d_treg.getTermDatabase()->getMatchOperator(n); - if (!op.isNull()) + // Relevant domain only makes sense for non-parametric operators, thus we + // check op==n.getOperator() here. This otherwise would lead to bad types + // for terms in the relevant domain. + if (!op.isNull() && op == n.getOperator()) { for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) { @@ -230,19 +254,24 @@ void RelevantDomain::computeRelevantDomainNode(Node q, if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){ //compute the information for what this literal does computeRelevantDomainLit( q, hasPol, pol, n ); - if( d_rel_dom_lit[hasPol][pol][n].d_merge ){ - Assert(d_rel_dom_lit[hasPol][pol][n].d_rd[0] != NULL - && d_rel_dom_lit[hasPol][pol][n].d_rd[1] != NULL); - RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent(); - RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent(); + RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n]; + if (rdl.d_merge) + { + Assert(rdl.d_rd[0] != nullptr && rdl.d_rd[1] != nullptr); + RDomain* rd1 = rdl.d_rd[0]->getParent(); + RDomain* rd2 = rdl.d_rd[1]->getParent(); if( rd1!=rd2 ){ rd1->merge( rd2 ); } - }else{ - if( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL ){ - RDomain * rd = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent(); - for( unsigned i=0; iaddTerm( d_rel_dom_lit[hasPol][pol][n].d_val[i] ); + } + else + { + if (rdl.d_rd[0] != nullptr) + { + RDomain* rd = rdl.d_rd[0]->getParent(); + for (unsigned i = 0; i < rdl.d_val.size(); i++) + { + rd->addTerm(rdl.d_val[i]); } } } @@ -254,7 +283,7 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { if( n.getKind()==INST_CONSTANT ){ Node q = TermUtil::getInstConstAttr(n); //merge the RDomains - unsigned id = n.getAttribute(InstVarNumAttribute()); + size_t 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_qreg.getInstConstantBody(q) @@ -272,7 +301,8 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) { if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){ - d_rel_dom_lit[hasPol][pol][n].d_merge = false; + RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n]; + rdl.d_merge = false; int varCount = 0; int varCh = -1; for( unsigned i=0; i