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.

8 files changed, 54 insertions, 159 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 {
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 280dc7047..ab532bc43 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -275,17 +275,6 @@ void CvcPrinter::toStreamNode(std::ostream& out,
       out << " ENDIF";
       return;
       break;
-    case kind::SEXPR_TYPE:
-      out << '[';
-      for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
-        if (i > 0) {
-          out << ", ";
-        }
-        toStreamNode(out, n[i], depth, false, lbind);
-      }
-      out << ']';
-      return;
-      break;
     case kind::SEXPR:
       // no-op
       break;
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 */