From bd96a673410c8c8389ede1a3ebe8bd1e0cea0f43 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Mar 2021 10:52:11 -0500 Subject: [PATCH] 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. --- src/expr/node_manager.cpp | 5 ++ src/expr/node_manager.h | 17 +---- src/expr/proof_node_to_sexpr.cpp | 11 ++-- src/expr/type_node.cpp | 46 +++++++++---- src/expr/type_node.h | 46 ------------- src/printer/cvc/cvc_printer.cpp | 11 ---- src/theory/builtin/kinds | 12 ++-- .../builtin/theory_builtin_type_rules.h | 65 ++----------------- 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(size)); } +TypeNode NodeManager::sExprType() +{ + return mkTypeConst(SEXPR_TYPE); +} + TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) { return mkTypeConst(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 - * types. types 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& types); + TypeNode sExprType(); /** Make the type of floating-point with exp bit exponent and sig bit significand */ @@ -1140,14 +1135,6 @@ public: } };/* class NodeManagerScope */ -inline TypeNode NodeManager::mkSExprType(const std::vector& types) { - std::vector 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 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 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 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() != REGEXP_TYPE); + || (getConst() != REGEXP_TYPE + && getConst() != SEXPR_TYPE)); } bool TypeNode::isWellFounded() const { @@ -424,15 +426,6 @@ vector TypeNode::getTupleTypes() const { return types; } -vector TypeNode::getSExprTypes() const { - Assert(isSExpr()); - vector 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 getTupleTypes() const; - /** Is this a symbolic expression type? */ - bool isSExpr() const; - - /** Get the constituent types of a symbolic expression type */ - std::vector 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 exp exponent bits and sig 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 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 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 */ -- 2.30.2