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.
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));
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 */
}
};/* 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,
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)
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;
}
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;
}
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 {
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) {
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
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())
/** 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;
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 {
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;
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
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 */
}
};/* 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 */
projects / cvc5.git / commitdiff