diff options
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 144 | ||||
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.h | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
| -rw-r--r-- | src/theory/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<const Node, std::map<size_t, RDomain*> >& d : d_rel_doms) + { + Trace("rel-dom") << "Relevant domain for " << d.first << " : " + << std::endl; + for (std::pair<const size_t, RDomain*>& 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; i<r->d_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; i<d_rel_dom_lit[hasPol][pol][n].d_val.size(); i++ ){ - rd->addTerm( 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<n.getNumChildren(); i++ ){ @@ -281,24 +311,24 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No // different from q Node qi = TermUtil::getInstConstAttr(n[i]); unsigned id = n[i].getAttribute(InstVarNumAttribute()); - d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false); + rdl.d_rd[i] = getRDomain(qi, id, false); varCount++; varCh = i; }else{ - d_rel_dom_lit[hasPol][pol][n].d_rd[i] = NULL; + rdl.d_rd[i] = nullptr; } } Node r_add; bool varLhs = true; if( varCount==2 ){ - d_rel_dom_lit[hasPol][pol][n].d_merge = true; + rdl.d_merge = true; }else{ if( varCount==1 ){ r_add = n[1-varCh]; varLhs = (varCh==0); - d_rel_dom_lit[hasPol][pol][n].d_rd[0] = d_rel_dom_lit[hasPol][pol][n].d_rd[varCh]; - d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL; + rdl.d_rd[0] = rdl.d_rd[varCh]; + rdl.d_rd[1] = nullptr; }else{ //solve the inequality for one/two variables, if possible if( n[0].getType().isReal() ){ @@ -323,7 +353,10 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No hasNonVar = true; } } + Trace("rel-dom") << "Process lit " << n << ", var/var2=" << var + << "/" << var2 << std::endl; if( !var.isNull() ){ + Assert(var.hasAttribute(InstVarNumAttribute())); if( var2.isNull() ){ //single variable solve Node veq_c; @@ -334,47 +367,54 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No if( veq_c.isNull() ){ r_add = val; varLhs = (ires==1); - d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false ); - d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL; + rdl.d_rd[0] = getRDomain( + q, var.getAttribute(InstVarNumAttribute()), false); + rdl.d_rd[1] = nullptr; } } }else if( !hasNonVar ){ + Assert(var2.hasAttribute(InstVarNumAttribute())); //merge the domains - d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false ); - d_rel_dom_lit[hasPol][pol][n].d_rd[1] = getRDomain( q, var2.getAttribute(InstVarNumAttribute()), false ); - d_rel_dom_lit[hasPol][pol][n].d_merge = true; + rdl.d_rd[0] = getRDomain( + q, var.getAttribute(InstVarNumAttribute()), false); + rdl.d_rd[1] = getRDomain( + q, var2.getAttribute(InstVarNumAttribute()), false); + rdl.d_merge = true; } } } } } } - if( d_rel_dom_lit[hasPol][pol][n].d_merge ){ + if (rdl.d_merge) + { //do not merge if constant negative polarity if( hasPol && !pol ){ - d_rel_dom_lit[hasPol][pol][n].d_merge = false; + rdl.d_merge = false; } - }else if( !r_add.isNull() && !TermUtil::hasInstConstAttr( r_add ) ){ + } + else if (!r_add.isNull() && !TermUtil::hasInstConstAttr(r_add)) + { Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl; //the negative occurrence adds the term to the domain if( !hasPol || !pol ){ - d_rel_dom_lit[hasPol][pol][n].d_val.push_back( r_add ); + rdl.d_val.push_back(r_add); } //the positive occurence adds other terms if( ( !hasPol || pol ) && n[0].getType().isInteger() ){ if( n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ - d_rel_dom_lit[hasPol][pol][n].d_val.push_back( - ArithMSum::offset(r_add, i == 0 ? 1 : -1)); + rdl.d_val.push_back(ArithMSum::offset(r_add, i == 0 ? 1 : -1)); } }else if( n.getKind()==GEQ ){ - d_rel_dom_lit[hasPol][pol][n].d_val.push_back( - ArithMSum::offset(r_add, varLhs ? 1 : -1)); + rdl.d_val.push_back(ArithMSum::offset(r_add, varLhs ? 1 : -1)); } } - }else{ - d_rel_dom_lit[hasPol][pol][n].d_rd[0] = NULL; - d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL; + } + else + { + rdl.d_rd[0] = nullptr; + rdl.d_rd[1] = nullptr; } } } diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 3b44b2263..ab1a0e064 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -108,21 +108,13 @@ class RelevantDomain : public QuantifiersUtil * of the equivalence class of relevant domain objects, * which is computed as a union find (see RDomain::d_parent). */ - RDomain* getRDomain(Node n, int i, bool getParent = true); + RDomain* getRDomain(Node n, size_t i, bool getParent = true); private: /** the relevant domains for each quantified formula and function, * for each variable # and argument #. */ - std::map< Node, std::map< int, RDomain * > > d_rel_doms; - /** stores the function or quantified formula associated with - * each relevant domain object. - */ - std::map< RDomain *, Node > d_rn_map; - /** stores the argument or variable number associated with - * each relevant domain object. - */ - std::map< RDomain *, int > d_ri_map; + std::map<Node, std::map<size_t, RDomain*> > d_rel_doms; /** Reference to the quantifiers state object */ QuantifiersState& d_qs; /** Reference to the quantifiers registry */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 7126d3567..6644f2b27 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -178,7 +178,7 @@ Node TermDb::getMatchOperator( Node n ) { if (k == SELECT || k == STORE || k == UNION || k == INTERSECTION || k == SUBSET || k == SETMINUS || k == MEMBER || k == SINGLETON || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR || k == APPLY_TESTER - || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH) + || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH || k == STRING_LENGTH) { //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index f505d2774..6982fc806 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -292,9 +292,10 @@ void TermTupleEnumeratorBase::next(/*out*/ std::vector<Node>& terms) : getTerm(variableIx, d_termIndex[variableIx]); terms[variableIx] = t; Trace("inst-alg-rd") << t << " "; - Assert(terms[variableIx].isNull() - || terms[variableIx].getType().isComparableTo( - d_quantifier[0][variableIx].getType())); + Assert(t.isNull() + || t.getType().isComparableTo(d_quantifier[0][variableIx].getType())) + << "Bad type: " << t << " " << t.getType() << " " + << d_quantifier[0][variableIx].getType(); } Trace("inst-alg-rd") << std::endl; } |