From: Tim King Date: Mon, 3 Oct 2016 04:17:50 +0000 (-0700) Subject: Removing the throw specifiers from theory_datatypes_type_rules.h. X-Git-Tag: cvc5-1.0.0~6028^2~4 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f6912760620b6365f2aacb004ac724a18a9157d8;p=cvc5.git Removing the throw specifiers from theory_datatypes_type_rules.h. --- diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 9c8387958..8a440974d 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -25,56 +25,64 @@ namespace CVC4 { namespace expr { - namespace attr { - struct DatatypeConstructorTypeGroundTermTag {}; - }/* CVC4::expr::attr namespace */ -}/* CVC4::expr namespace */ +namespace attr { +struct DatatypeConstructorTypeGroundTermTag {}; +} /* CVC4::expr::attr namespace */ +} /* CVC4::expr namespace */ namespace theory { namespace datatypes { -typedef expr::Attribute GroundTermAttr; - +typedef expr::Attribute + GroundTermAttr; struct DatatypeConstructorTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate, AssertionException) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); TypeNode consType = n.getOperator().getType(check); Type t = consType.getConstructorRangeType().toType(); - Assert( t.isDatatype() ); + Assert(t.isDatatype()); DatatypeType dt = DatatypeType(t); TNode::iterator child_it = n.begin(); TNode::iterator child_it_end = n.end(); TypeNode::iterator tchild_it = consType.begin(); - if( ( dt.isParametric() || check ) && n.getNumChildren() != consType.getNumChildren() - 1 ){ - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the constructor type"); + if ((dt.isParametric() || check) && + n.getNumChildren() != consType.getNumChildren() - 1) { + throw TypeCheckingExceptionPrivate( + n, "number of arguments does not match the constructor type"); } - if( dt.isParametric() ){ - Debug("typecheck-idt") << "typecheck parameterized datatype " << n << std::endl; - Matcher m( dt ); - for(; child_it != child_it_end; ++child_it, ++tchild_it) { + if (dt.isParametric()) { + Debug("typecheck-idt") << "typecheck parameterized datatype " << n + << std::endl; + Matcher m(dt); + for (; child_it != child_it_end; ++child_it, ++tchild_it) { TypeNode childType = (*child_it).getType(check); - if( !m.doMatching( *tchild_it, childType ) ){ - throw TypeCheckingExceptionPrivate(n, "matching failed for parameterized constructor"); + if (!m.doMatching(*tchild_it, childType)) { + throw TypeCheckingExceptionPrivate( + n, "matching failed for parameterized constructor"); } } - std::vector< Type > instTypes; - m.getMatches( instTypes ); - TypeNode range = TypeNode::fromType( dt.instantiate( instTypes ) ); + std::vector instTypes; + m.getMatches(instTypes); + TypeNode range = TypeNode::fromType(dt.instantiate(instTypes)); Debug("typecheck-idt") << "Return " << range << std::endl; return range; - }else{ - if(check) { - Debug("typecheck-idt") << "typecheck cons: " << n << " " << n.getNumChildren() << std::endl; - Debug("typecheck-idt") << "cons type: " << consType << " " << consType.getNumChildren() << std::endl; - for(; child_it != child_it_end; ++child_it, ++tchild_it) { + } else { + if (check) { + Debug("typecheck-idt") << "typecheck cons: " << n << " " + << n.getNumChildren() << std::endl; + Debug("typecheck-idt") << "cons type: " << consType << " " + << consType.getNumChildren() << std::endl; + for (; child_it != child_it_end; ++child_it, ++tchild_it) { TypeNode childType = (*child_it).getType(check); - Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; + Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " + << (*tchild_it) << std::endl; TypeNode argumentType = *tchild_it; - if(!childType.isComparableTo(argumentType)) { + if (!childType.isComparableTo(argumentType)) { std::stringstream ss; - ss << "bad type for constructor argument:\nexpected: " << argumentType << "\ngot : " << childType; + ss << "bad type for constructor argument:\nexpected: " + << argumentType << "\ngot : " << childType; throw TypeCheckingExceptionPrivate(n, ss.str()); } } @@ -83,132 +91,131 @@ struct DatatypeConstructorTypeRule { } } - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) - throw(AssertionException) { + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); NodeManagerScope nms(nodeManager); - for(TNode::const_iterator i = n.begin(); i != n.end(); ++i) { - if( ! (*i).isConst() ) { + for (TNode::const_iterator i = n.begin(); i != n.end(); ++i) { + if (!(*i).isConst()) { return false; } } return true; } -};/* struct DatatypeConstructorTypeRule */ +}; /* struct DatatypeConstructorTypeRule */ struct DatatypeSelectorTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { - Assert(n.getKind() == kind::APPLY_SELECTOR || n.getKind() == kind::APPLY_SELECTOR_TOTAL ); + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + Assert(n.getKind() == kind::APPLY_SELECTOR || + n.getKind() == kind::APPLY_SELECTOR_TOTAL); TypeNode selType = n.getOperator().getType(check); Type t = selType[0].toType(); - Assert( t.isDatatype() ); + Assert(t.isDatatype()); DatatypeType dt = DatatypeType(t); - if( ( dt.isParametric() || check ) && n.getNumChildren() != 1 ){ - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the selector type"); + if ((dt.isParametric() || check) && n.getNumChildren() != 1) { + throw TypeCheckingExceptionPrivate( + n, "number of arguments does not match the selector type"); } - if( dt.isParametric() ){ - Debug("typecheck-idt") << "typecheck parameterized sel: " << n << std::endl; - Matcher m( dt ); + if (dt.isParametric()) { + Debug("typecheck-idt") << "typecheck parameterized sel: " << n + << std::endl; + Matcher m(dt); TypeNode childType = n[0].getType(check); - if(! childType.isInstantiatedDatatype()) { - throw TypeCheckingExceptionPrivate(n, "Datatype type not fully instantiated"); + if (!childType.isInstantiatedDatatype()) { + throw TypeCheckingExceptionPrivate( + n, "Datatype type not fully instantiated"); } - if( !m.doMatching( selType[0], childType ) ){ - throw TypeCheckingExceptionPrivate(n, "matching failed for selector argument of parameterized datatype"); + if (!m.doMatching(selType[0], childType)) { + throw TypeCheckingExceptionPrivate( + n, + "matching failed for selector argument of parameterized datatype"); } - std::vector< Type > types, matches; - m.getTypes( types ); - m.getMatches( matches ); + std::vector types, matches; + m.getTypes(types); + m.getMatches(matches); Type range = selType[1].toType(); - range = range.substitute( types, matches ); + range = range.substitute(types, matches); Debug("typecheck-idt") << "Return " << range << std::endl; - return TypeNode::fromType( range ); - }else{ - if(check) { + return TypeNode::fromType(range); + } else { + if (check) { Debug("typecheck-idt") << "typecheck sel: " << n << std::endl; Debug("typecheck-idt") << "sel type: " << selType << std::endl; TypeNode childType = n[0].getType(check); - if(!selType[0].isComparableTo(childType)) { - Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " << childType.getKind() << std::endl; - throw TypeCheckingExceptionPrivate(n, "bad type for selector argument"); + if (!selType[0].isComparableTo(childType)) { + Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " + << childType.getKind() << std::endl; + throw TypeCheckingExceptionPrivate(n, + "bad type for selector argument"); } } return selType[1]; } } -};/* struct DatatypeSelectorTypeRule */ +}; /* struct DatatypeSelectorTypeRule */ struct DatatypeTesterTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { Assert(n.getKind() == kind::APPLY_TESTER); - if(check) { - if(n.getNumChildren() != 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the tester type"); + if (check) { + if (n.getNumChildren() != 1) { + throw TypeCheckingExceptionPrivate( + n, "number of arguments does not match the tester type"); } TypeNode testType = n.getOperator().getType(check); TypeNode childType = n[0].getType(check); Type t = testType[0].toType(); - Assert( t.isDatatype() ); + Assert(t.isDatatype()); DatatypeType dt = DatatypeType(t); - if(dt.isParametric()) { - Debug("typecheck-idt") << "typecheck parameterized tester: " << n << std::endl; - Matcher m( dt ); - if( !m.doMatching( testType[0], childType ) ){ - throw TypeCheckingExceptionPrivate(n, "matching failed for tester argument of parameterized datatype"); + if (dt.isParametric()) { + Debug("typecheck-idt") << "typecheck parameterized tester: " << n + << std::endl; + Matcher m(dt); + if (!m.doMatching(testType[0], childType)) { + throw TypeCheckingExceptionPrivate( + n, + "matching failed for tester argument of parameterized datatype"); } } else { Debug("typecheck-idt") << "typecheck test: " << n << std::endl; Debug("typecheck-idt") << "test type: " << testType << std::endl; - if(!testType[0].isComparableTo(childType)) { + if (!testType[0].isComparableTo(childType)) { throw TypeCheckingExceptionPrivate(n, "bad type for tester argument"); } } } return nodeManager->booleanType(); } -};/* struct DatatypeTesterTypeRule */ +}; /* struct DatatypeTesterTypeRule */ struct DatatypeAscriptionTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { Debug("typecheck-idt") << "typechecking ascription: " << n << std::endl; Assert(n.getKind() == kind::APPLY_TYPE_ASCRIPTION); - TypeNode t = TypeNode::fromType(n.getOperator().getConst().getType()); - if(check) { + TypeNode t = TypeNode::fromType( + n.getOperator().getConst().getType()); + if (check) { TypeNode childType = n[0].getType(check); - //if(!t.getKind() == kind::DATATYPE_TYPE) { - // throw TypeCheckingExceptionPrivate(n, "bad type for datatype type ascription"); - //} - //DatatypeType dt = DatatypeType(childType.toType()); - //if( dt.isParametric() ){ - // Debug("typecheck-idt") << "typecheck parameterized ascription: " << n << std::endl; - // Matcher m( dt ); - // if( !m.doMatching( childType, t ) ){ - // throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype"); - // } - //}else{ - // Debug("typecheck-idt") << "typecheck test: " << n << std::endl; - // if(t != childType) { - // throw TypeCheckingExceptionPrivate(n, "bad type for type ascription argument"); - // } - //} Matcher m; - if( childType.getKind() == kind::CONSTRUCTOR_TYPE ){ - m.addTypesFromDatatype( ConstructorType(childType.toType()).getRangeType() ); - }else if( childType.getKind() == kind::DATATYPE_TYPE ){ - m.addTypesFromDatatype( DatatypeType(childType.toType()) ); + if (childType.getKind() == kind::CONSTRUCTOR_TYPE) { + m.addTypesFromDatatype( + ConstructorType(childType.toType()).getRangeType()); + } else if (childType.getKind() == kind::DATATYPE_TYPE) { + m.addTypesFromDatatype(DatatypeType(childType.toType())); } - if( !m.doMatching( childType, t ) ){ - throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype"); + if (!m.doMatching(childType, t)) { + throw TypeCheckingExceptionPrivate(n, + "matching failed for type " + "ascription argument of " + "parameterized datatype"); } - } return t; } -};/* struct DatatypeAscriptionTypeRule */ +}; /* struct DatatypeAscriptionTypeRule */ struct ConstructorProperties { inline static Cardinality computeCardinality(TypeNode type) { @@ -217,24 +224,26 @@ struct ConstructorProperties { // that of a tuple than that of a function. AssertArgument(type.isConstructor(), type); Cardinality c = 1; - for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) { + for (unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) { c *= type[i].getCardinality(); } return c; } -};/* struct ConstructorProperties */ +}; /* struct ConstructorProperties */ struct TupleUpdateTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { Assert(n.getKind() == kind::TUPLE_UPDATE); const TupleUpdate& tu = n.getOperator().getConst(); TypeNode tupleType = n[0].getType(check); TypeNode newValue = n[1].getType(check); - if(check) { - if(!tupleType.isTuple()) { - throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); + if (check) { + if (!tupleType.isTuple()) { + throw TypeCheckingExceptionPrivate( + n, "Tuple-update expression formed over non-tuple"); } - if(tu.getIndex() >= tupleType.getTupleLength()) { + if (tu.getIndex() >= tupleType.getTupleLength()) { std::stringstream ss; ss << "Tuple-update expression index `" << tu.getIndex() << "' is not a valid index; tuple type only has " @@ -244,21 +253,23 @@ struct TupleUpdateTypeRule { } return tupleType; } -};/* struct TupleUpdateTypeRule */ +}; /* struct TupleUpdateTypeRule */ struct RecordUpdateTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { Assert(n.getKind() == kind::RECORD_UPDATE); NodeManagerScope nms(nodeManager); const RecordUpdate& ru = n.getOperator().getConst(); TypeNode recordType = n[0].getType(check); TypeNode newValue = n[1].getType(check); - if(check) { - if(!recordType.isRecord()) { - throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record"); + if (check) { + if (!recordType.isRecord()) { + throw TypeCheckingExceptionPrivate( + n, "Record-update expression formed over non-record"); } const Record& rec = recordType.getRecord(); - if(!rec.contains(ru.getField())) { + if (!rec.contains(ru.getField())) { std::stringstream ss; ss << "Record-update field `" << ru.getField() << "' is not a valid field name for the record type"; @@ -267,44 +278,49 @@ struct RecordUpdateTypeRule { } return recordType; } -};/* struct RecordUpdateTypeRule */ +}; /* struct RecordUpdateTypeRule */ class DtSizeTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode t = n[0].getType(check); if (!t.isDatatype()) { - throw TypeCheckingExceptionPrivate(n, "expecting datatype size term to have datatype argument."); + throw TypeCheckingExceptionPrivate( + n, "expecting datatype size term to have datatype argument."); } } return nodeManager->integerType(); } -};/* class DtSizeTypeRule */ +}; /* class DtSizeTypeRule */ class DtHeightBoundTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode t = n[0].getType(check); if (!t.isDatatype()) { - throw TypeCheckingExceptionPrivate(n, "expecting datatype height bound term to have datatype argument."); + throw TypeCheckingExceptionPrivate( + n, + "expecting datatype height bound term to have datatype argument."); } - if( n[1].getKind()!=kind::CONST_RATIONAL ){ - throw TypeCheckingExceptionPrivate(n, "datatype height bound must be a constant"); + if (n[1].getKind() != kind::CONST_RATIONAL) { + throw TypeCheckingExceptionPrivate( + n, "datatype height bound must be a constant"); } - if( n[1].getConst().getNumerator().sgn()==-1 ){ - throw TypeCheckingExceptionPrivate(n, "datatype height bound must be non-negative"); + if (n[1].getConst().getNumerator().sgn() == -1) { + throw TypeCheckingExceptionPrivate( + n, "datatype height bound must be non-negative"); } } return nodeManager->booleanType(); } -};/* class DtHeightBoundTypeRule */ +}; /* class DtHeightBoundTypeRule */ -}/* CVC4::theory::datatypes namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} /* CVC4::theory::datatypes namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */