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.

1 files changed, 4 insertions, 7 deletions

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;
 }