Refactoring quantifier annotation kinds, add kinds in preparation for pool-based instantiation (#6234)

This is in preparation for a new pool-based instantiation technique.

2 files changed, 56 insertions, 47 deletions

diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 3f15ef916..fa24275b1 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -35,6 +35,9 @@ sort INST_PATTERN_TYPE \
 operator INST_PATTERN 1: "instantiation pattern"
 operator INST_NO_PATTERN 1 "instantiation no-pattern"
 operator INST_ATTRIBUTE 1 "instantiation attribute"
+operator INST_POOL 1: "instantiation pool"
+operator INST_ADD_TO_POOL 2 "instantiation add to pool"
+operator SKOLEM_ADD_TO_POOL 2 "skolemization add to pool"
 
 sort INST_PATTERN_LIST_TYPE \
     Cardinality::INTEGERS \
@@ -44,12 +47,16 @@ sort INST_PATTERN_LIST_TYPE \
 # a list of instantiation patterns
 operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
 
-typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule 
-typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule 
-typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule 
-typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule 
-typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule 
-typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule 
+typerule FORALL ::CVC4::theory::quantifiers::QuantifierTypeRule
+typerule EXISTS ::CVC4::theory::quantifiers::QuantifierTypeRule
+typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule
 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule
 
+typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
+typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule INST_POOL ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule INST_ADD_TO_POOL ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule SKOLEM_ADD_TO_POOL ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule
+
 endtheory
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 5d1d4c5bf..6758cde28 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -26,45 +26,47 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-struct QuantifierForallTypeRule {
+struct QuantifierTypeRule
+{
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
     Debug("typecheck-q") << "type check for fa " << n << std::endl;
-    Assert(n.getKind() == kind::FORALL && n.getNumChildren() > 0);
+    Assert((n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS)
+           && n.getNumChildren() > 0);
     if( check ){
       if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
-        throw TypeCheckingExceptionPrivate(n, "first argument of universal quantifier is not bound var list");
+        throw TypeCheckingExceptionPrivate(
+            n, "first argument of quantifier is not bound var list");
       }
       if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n, "body of universal quantifier is not boolean");
+        throw TypeCheckingExceptionPrivate(n,
+                                           "body of quantifier is not boolean");
       }
-      if( n.getNumChildren()==3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
-        throw TypeCheckingExceptionPrivate(n, "third argument of universal quantifier is not instantiation pattern list");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* struct QuantifierForallTypeRule */
-
-struct QuantifierExistsTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Debug("typecheck-q") << "type check for ex " << n << std::endl;
-    Assert(n.getKind() == kind::EXISTS && n.getNumChildren() > 0);
-    if( check ){
-      if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
-        throw TypeCheckingExceptionPrivate(n, "first argument of existential quantifier is not bound var list");
-      }
-      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n, "body of existential quantifier is not boolean");
-      }
-      if( n.getNumChildren()==3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
-        throw TypeCheckingExceptionPrivate(n, "third argument of existential quantifier is not instantiation pattern list");
+      if (n.getNumChildren() == 3)
+      {
+        if (n[2].getType(check) != nodeManager->instPatternListType())
+        {
+          throw TypeCheckingExceptionPrivate(
+              n,
+              "third argument of quantifier is not instantiation "
+              "pattern list");
+        }
+        for (const Node& p : n[2])
+        {
+          if (p.getKind() == kind::INST_POOL
+              && p.getNumChildren() != n[0].getNumChildren())
+          {
+            throw TypeCheckingExceptionPrivate(
+                n,
+                "expected number of arguments to pool to be the same as the "
+                "number of bound variables of the quantified formula");
+          }
+        }
       }
     }
     return nodeManager->booleanType();
   }
-};/* struct QuantifierExistsTypeRule */
+}; /* struct QuantifierTypeRule */
 
 struct QuantifierBoundVarListTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -96,30 +98,30 @@ struct QuantifierInstPatternTypeRule {
   }
 };/* struct QuantifierInstPatternTypeRule */
 
-struct QuantifierInstNoPatternTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::INST_NO_PATTERN);
-    return nodeManager->instPatternType();
-  }
-};/* struct QuantifierInstNoPatternTypeRule */
-
-struct QuantifierInstAttributeTypeRule {
+struct QuantifierAnnotationTypeRule
+{
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::INST_ATTRIBUTE);
     return nodeManager->instPatternType();
   }
-};/* struct QuantifierInstAttributeTypeRule */
+}; /* struct QuantifierAnnotationTypeRule */
 
 struct QuantifierInstPatternListTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
     Assert(n.getKind() == kind::INST_PATTERN_LIST);
     if( check ){
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        if( n[i].getKind()!=kind::INST_PATTERN && n[i].getKind()!=kind::INST_NO_PATTERN && n[i].getKind()!=kind::INST_ATTRIBUTE ){
-          throw TypeCheckingExceptionPrivate(n, "argument of inst pattern list is not inst pattern");
+      for (const Node& nc : n)
+      {
+        Kind k = nc.getKind();
+        if (k != kind::INST_PATTERN && k != kind::INST_NO_PATTERN
+            && k != kind::INST_ATTRIBUTE && k != kind::INST_POOL
+            && k != kind::INST_ADD_TO_POOL && k != kind::SKOLEM_ADD_TO_POOL)
+        {
+          throw TypeCheckingExceptionPrivate(
+              n,
+              "argument of inst pattern list is not a legal quantifiers "
+              "annotation");
         }
       }
     }