From c84db60dabd8104928c7261c9df7bd9ef2917e9f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Apr 2020 16:27:29 -0500 Subject: [PATCH] Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235) Fixes #4228. That benchmark now times out. --- .../quantifiers/inst_strategy_enumerative.cpp | 3 ++- src/theory/quantifiers/instantiate.cpp | 18 +++++++++++++++++- src/theory/quantifiers/instantiate.h | 5 +++++ src/theory/quantifiers/relevant_domain.cpp | 8 +++++++- src/theory/quantifiers/term_util.cpp | 13 ------------- src/theory/quantifiers/term_util.h | 2 -- 6 files changed, 31 insertions(+), 18 deletions(-) diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 47e4a9228..ce024fe8b 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -301,7 +301,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { terms.push_back(d_rd->getRDomain(f, i)->d_terms[childIndex[i]]); Trace("inst-alg-rd") - << " " << d_rd->getRDomain(f, i)->d_terms[childIndex[i]] + << " (rd) " << d_rd->getRDomain(f, i)->d_terms[childIndex[i]] << std::endl; } else @@ -312,6 +312,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) << " " << term_db_list[ftypes[i]][childIndex[i]] << std::endl; } + Assert(terms[i].getType().isComparableTo(ftypes[i])); } if (ie->addInstantiation(f, terms)) { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 9969de458..218753308 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -116,7 +116,7 @@ bool Instantiate::addInstantiation( // Ensure the type is correct, this for instance ensures that real terms // are cast to integers for { x -> t } where x has type Int and t has // type Real. - terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn); + terms[i] = ensureType(terms[i], tn); if (mkRep) { // pick the best possible representative for instantiation, based on past @@ -747,6 +747,22 @@ void Instantiate::debugPrintModel() } } +Node Instantiate::ensureType(Node n, TypeNode tn) +{ + Trace("inst-add-debug2") << "Ensure " << n << " : " << tn << std::endl; + TypeNode ntn = n.getType(); + Assert(ntn.isComparableTo(tn)); + if (ntn.isSubtypeOf(tn)) + { + return n; + } + if (tn.isInteger()) + { + return NodeManager::currentNM()->mkNode(TO_INTEGER, n); + } + return Node::null(); +} + Instantiate::Statistics::Statistics() : d_instantiations("Instantiate::Instantiations_Total", 0), d_inst_duplicate("Instantiate::Duplicate_Inst", 0), diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index cd3993756..d10a44149 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -318,6 +318,11 @@ class Instantiate : public QuantifiersUtil bool addedLem = true); /** remove instantiation from the cache */ bool removeInstantiationInternal(Node q, std::vector& terms); + /** + * Ensure that n has type tn, return a term equivalent to it for that type + * if possible. + */ + static Node ensureType(Node n, TypeNode tn); /** pointer to the quantifiers engine */ QuantifiersEngine* d_qe; 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; igetInstConstAttr(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{ diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index cc920f1d7..c8c72344f 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -305,19 +305,6 @@ void TermUtil::computeInstConstContainsForQuant(Node q, } } -Node TermUtil::ensureType( Node n, TypeNode tn ) { - TypeNode ntn = n.getType(); - Assert(ntn.isComparableTo(tn)); - if( ntn.isSubtypeOf( tn ) ){ - return n; - }else{ - if( tn.isInteger() ){ - return NodeManager::currentNM()->mkNode( TO_INTEGER, n ); - } - return Node::null(); - } -} - int TermUtil::getTermDepth( Node n ) { if (!n.hasAttribute(TermDepthAttribute()) ){ int maxDepth = -1; diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 904f301b9..315b4b1d0 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -160,8 +160,6 @@ public: std::vector& vars); public: - /** ensure type */ - static Node ensureType( Node n, TypeNode tn ); //general utilities // TODO #1216 : promote these? -- 2.30.2