Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235)

Fixes #4228. That benchmark now times out.

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<Node>& 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; i<n.getNumChildren(); i++ ){
       if( n[i].getKind()==INST_CONSTANT ){
-        d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain( q, n[i].getAttribute(InstVarNumAttribute()), false );
+        // must get the quantified formula this belongs to, which may be
+        // different from q
+        Node qi = tu->getInstConstAttr(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<Node>& vars);
 
 public:
-  /** ensure type */
-  static Node ensureType( Node n, TypeNode tn );
   
 //general utilities
   // TODO #1216 : promote these?