Make SEXPR simply typed (#6160)

Currently, SEXPR applications are given a parametric type SEXPR_TYPE applied to the types of its arguments. This means that SEXPR that are type checked consume roughly double the memory. This issue arises in practice when printing proofs in the internal calculus.

There is no need to have SEXPR_TYPE as a parametric type, this PR makes SEXPR simply typed.

Also moves some implementation of TypeNode methods to type_node.cpp.

2 files changed, 11 insertions, 66 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index a11354b1a..cf68e060c 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -316,14 +316,10 @@ well-founded FUNCTION_TYPE \
 enumerator FUNCTION_TYPE \
     ::CVC4::theory::builtin::FunctionEnumerator \
     "theory/builtin/type_enumerator.h"
-operator SEXPR_TYPE 0: "the type of a symbolic expression"
-cardinality SEXPR_TYPE \
-    "::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
-well-founded SEXPR_TYPE \
-    "::CVC4::theory::builtin::SExprProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
+sort SEXPR_TYPE \
+    Cardinality::INTEGERS \
+    not-well-founded \
+    "the type of a symbolic expression"
 
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 84e64baa4..e0c68aa0f 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -81,13 +81,14 @@ class DistinctTypeRule {
 class SExprTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    std::vector<TypeNode> types;
-    for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
-        child_it != child_it_end;
-        ++child_it) {
-      types.push_back((*child_it).getType(check));
+    if (check)
+    {
+      for (TNode c : n)
+      {
+        c.getType(check);
+      }
     }
-    return nodeManager->mkSExprType(types);
+    return nodeManager->sExprType();
   }
 };/* class SExprTypeRule */
 
@@ -245,58 +246,6 @@ class FunctionProperties {
   }
 };/* class FuctionProperties */
 
-class SExprProperties {
- public:
-  inline static Cardinality computeCardinality(TypeNode type) {
-    // Don't assert this; allow other theories to use this cardinality
-    // computation.
-    //
-    // Assert(type.getKind() == kind::SEXPR_TYPE);
-
-    Cardinality card(1);
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      card *= (*i).getCardinality();
-    }
-
-    return card;
-  }
-
-  inline static bool isWellFounded(TypeNode type) {
-    // Don't assert this; allow other theories to use this
-    // wellfoundedness computation.
-    //
-    // Assert(type.getKind() == kind::SEXPR_TYPE);
-
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      if(! (*i).isWellFounded()) {
-        return false;
-      }
-    }
-
-    return true;
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::SEXPR_TYPE);
-
-    std::vector<Node> children;
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      children.push_back((*i).mkGroundTerm());
-    }
-
-    return NodeManager::currentNM()->mkNode(kind::SEXPR, children);
-  }
-};/* class SExprProperties */
-
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */