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.

5 files changed, 43 insertions, 82 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 599d3e8f7..a5329147b 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -165,6 +165,11 @@ TypeNode NodeManager::mkBitVectorType(unsigned size)
   return mkTypeConst<BitVectorSize>(BitVectorSize(size));
 }
 
+TypeNode NodeManager::sExprType()
+{
+  return mkTypeConst<TypeConstant>(SEXPR_TYPE);
+}
+
 TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig)
 {
   return mkTypeConst<FloatingPointSize>(FloatingPointSize(exp, sig));
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ce89f5dc6..52ce096d5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -935,14 +935,9 @@ class NodeManager
   TypeNode mkRecordType(const Record& rec);
 
   /**
-   * Make a symbolic expression type with types from
-   * <code>types</code>. <code>types</code> may have any number of
-   * elements.
-   *
-   * @param types a vector of types
-   * @returns the symbolic expression type (types[0], ..., types[n])
+   * @returns the symbolic expression type
    */
-  inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
+  TypeNode sExprType();
 
   /** Make the type of floating-point with <code>exp</code> bit exponent and
       <code>sig</code> bit significand */
@@ -1140,14 +1135,6 @@ public:
   }
 };/* class NodeManagerScope */
 
-inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
-  std::vector<TypeNode> typeNodes;
-  for (unsigned i = 0; i < types.size(); ++ i) {
-    typeNodes.push_back(types[i]);
-  }
-  return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
-}
-
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
   CheckArgument(!indexType.isNull(), indexType,
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index 34868b67f..c298dafe6 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -27,9 +27,8 @@ namespace CVC4 {
 ProofNodeToSExpr::ProofNodeToSExpr()
 {
   NodeManager* nm = NodeManager::currentNM();
-  std::vector<TypeNode> types;
-  d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->mkSExprType(types));
-  d_argsMarker = nm->mkBoundVar(":args", nm->mkSExprType(types));
+  d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->sExprType());
+  d_argsMarker = nm->mkBoundVar(":args", nm->sExprType());
 }
 
 Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
@@ -125,8 +124,7 @@ Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r)
   std::stringstream ss;
   ss << r;
   NodeManager* nm = NodeManager::currentNM();
-  std::vector<TypeNode> types;
-  Node var = nm->mkBoundVar(ss.str(), nm->mkSExprType(types));
+  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
   d_pfrMap[r] = var;
   return var;
 }
@@ -141,8 +139,7 @@ Node ProofNodeToSExpr::getOrMkNodeVariable(Node n)
   std::stringstream ss;
   ss << n;
   NodeManager* nm = NodeManager::currentNM();
-  std::vector<TypeNode> types;
-  Node var = nm->mkBoundVar(ss.str(), nm->mkSExprType(types));
+  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
   d_nodeMap[n] = var;
   return var;
 }
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8cf4fbccd..8d474ca5f 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -283,11 +283,13 @@ bool TypeNode::isClosedEnumerable()
   return getAttribute(IsClosedEnumerableAttr());
 }
 
-bool TypeNode::isFirstClass() const {
+bool TypeNode::isFirstClass() const
+{
   return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE
-         && getKind() != kind::TESTER_TYPE && getKind() != kind::SEXPR_TYPE
+         && getKind() != kind::TESTER_TYPE
          && (getKind() != kind::TYPE_CONSTANT
-             || getConst<TypeConstant>() != REGEXP_TYPE);
+             || (getConst<TypeConstant>() != REGEXP_TYPE
+                 && getConst<TypeConstant>() != SEXPR_TYPE));
 }
 
 bool TypeNode::isWellFounded() const {
@@ -424,15 +426,6 @@ vector<TypeNode> TypeNode::getTupleTypes() const {
   return types;
 }
 
-vector<TypeNode> TypeNode::getSExprTypes() const {
-  Assert(isSExpr());
-  vector<TypeNode> types;
-  for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
-    types.push_back((*this)[i]);
-  }
-  return types;
-}
-
 /** Is this an instantiated datatype type */
 bool TypeNode::isInstantiatedDatatype() const {
   if(getKind() == kind::DATATYPE_TYPE) {
@@ -589,7 +582,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
     case kind::SEQUENCE_TYPE:
     case kind::SET_TYPE:
     case kind::BAG_TYPE:
-    case kind::SEXPR_TYPE:
     {
       // we don't support subtyping except for built in types Int and Real.
       return TypeNode();  // return null type
@@ -651,7 +643,33 @@ bool TypeNode::isSortConstructor() const {
   return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
 }
 
-/** Is this a codatatype type */
+bool TypeNode::isFloatingPoint() const
+{
+  return getKind() == kind::FLOATINGPOINT_TYPE;
+}
+
+bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE; }
+
+bool TypeNode::isDatatype() const
+{
+  return getKind() == kind::DATATYPE_TYPE
+         || getKind() == kind::PARAMETRIC_DATATYPE;
+}
+
+bool TypeNode::isParametricDatatype() const
+{
+  return getKind() == kind::PARAMETRIC_DATATYPE;
+}
+
+bool TypeNode::isConstructor() const
+{
+  return getKind() == kind::CONSTRUCTOR_TYPE;
+}
+
+bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; }
+
+bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; }
+
 bool TypeNode::isCodatatype() const
 {
   if (isDatatype())
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 15cfeede6..baff528ff 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -604,12 +604,6 @@ public:
   /** Get the constituent types of a tuple type */
   std::vector<TypeNode> getTupleTypes() const;
 
-  /** Is this a symbolic expression type? */
-  bool isSExpr() const;
-
-  /** Get the constituent types of a symbolic expression type */
-  std::vector<TypeNode> getSExprTypes() const;
-
   /** Is this a regexp type */
   bool isRegExp() const;
 
@@ -1007,46 +1001,6 @@ inline TypeNode TypeNode::getRangeType() const {
   return (*this)[getNumChildren() - 1];
 }
 
-/** Is this a symbolic expression type? */
-inline bool TypeNode::isSExpr() const {
-  return getKind() == kind::SEXPR_TYPE;
-}
-
-/** Is this a floating-point type */
-inline bool TypeNode::isFloatingPoint() const {
-  return getKind() == kind::FLOATINGPOINT_TYPE;
-}
-
-/** Is this a bit-vector type */
-inline bool TypeNode::isBitVector() const {
-  return getKind() == kind::BITVECTOR_TYPE;
-}
-
-/** Is this a datatype type */
-inline bool TypeNode::isDatatype() const {
-  return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE;
-}
-
-/** Is this a parametric datatype type */
-inline bool TypeNode::isParametricDatatype() const {
-  return getKind() == kind::PARAMETRIC_DATATYPE;
-}
-
-/** Is this a constructor type */
-inline bool TypeNode::isConstructor() const {
-  return getKind() == kind::CONSTRUCTOR_TYPE;
-}
-
-/** Is this a selector type */
-inline bool TypeNode::isSelector() const {
-  return getKind() == kind::SELECTOR_TYPE;
-}
-
-/** Is this a tester type */
-inline bool TypeNode::isTester() const {
-  return getKind() == kind::TESTER_TYPE;
-}
-
 /** Is this a floating-point type of with <code>exp</code> exponent bits
     and <code>sig</code> significand bits */
 inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {