From: Aina Niemetz Date: Wed, 21 Apr 2021 12:27:16 +0000 (-0700) Subject: Sets: Move implementation of type rules to cpp. (#6401) X-Git-Tag: cvc5-1.0.0~1868 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8062e5527ccf7a02266336bb37a5c0e7c82d971b;p=cvc5.git Sets: Move implementation of type rules to cpp. (#6401) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index cfb12ec0b..554739b98 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -928,6 +928,7 @@ libcvc4_add_sources( theory/sets/theory_sets_rewriter.h theory/sets/theory_sets_type_enumerator.cpp theory/sets/theory_sets_type_enumerator.h + theory/sets/theory_sets_type_rules.cpp theory/sets/theory_sets_type_rules.h theory/shared_solver.cpp theory/shared_solver.h diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp new file mode 100644 index 000000000..232865994 --- /dev/null +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -0,0 +1,477 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Sets theory type rules. + */ + +#include "theory/sets/theory_sets_type_rules.h" + +#include +#include + +#include "theory/sets/normal_form.h" + +namespace cvc5 { +namespace theory { +namespace sets { + +TypeNode SetsBinaryOperatorTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION + || n.getKind() == kind::SETMINUS); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "operator expects a set, first argument is not"); + } + TypeNode secondSetType = n[1].getType(check); + if (secondSetType != setType) + { + std::stringstream ss; + ss << "Operator " << n.getKind() + << " expects two sets of the same type. Found types '" << setType + << "' and '" << secondSetType << "'."; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + return setType; +} + +bool SetsBinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager, + TNode n) +{ + // only UNION has a const rule in kinds. + // INTERSECTION and SETMINUS are not used in the canonical representation of + // sets and therefore they do not have const rules in kinds + Assert(n.getKind() == kind::UNION); + return NormalForm::checkNormalConstant(n); +} + +TypeNode SubsetTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::SUBSET); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set"); + } + TypeNode secondSetType = n[1].getType(check); + if (secondSetType != setType) + { + if (!setType.isComparableTo(secondSetType)) + { + throw TypeCheckingExceptionPrivate( + n, "set subset operating on sets of different types"); + } + } + } + return nodeManager->booleanType(); +} + +TypeNode MemberTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::MEMBER); + TypeNode setType = n[1].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "checking for membership in a non-set"); + } + TypeNode elementType = n[0].getType(check); + // e.g. (member 1 (singleton 1.0)) is true whereas + // (member 1.0 (singleton 1)) throws a typing error + if (!elementType.isSubtypeOf(setType.getSetElementType())) + { + std::stringstream ss; + ss << "member operating on sets of different types:\n" + << "child type: " << elementType << "\n" + << "not subtype: " << setType.getSetElementType() << "\n" + << "in term : " << n; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + return nodeManager->booleanType(); +} + +TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::SINGLETON && n.hasOperator() + && n.getOperator().getKind() == kind::SINGLETON_OP); + + SingletonOp op = n.getOperator().getConst(); + TypeNode type1 = op.getType(); + if (check) + { + TypeNode type2 = n[0].getType(check); + TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2); + // the type of the element should be a subtype of the type of the operator + // e.g. (singleton (singleton_op Real) 1) where 1 is an Int + if (leastCommonType.isNull() || leastCommonType != type1) + { + std::stringstream ss; + ss << "The type '" << type2 << "' of the element is not a subtype of '" + << type1 << "' in term : " << n; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + return nodeManager->mkSetType(type1); +} + +bool SingletonTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) +{ + Assert(n.getKind() == kind::SINGLETON); + return n[0].isConst(); +} + +TypeNode EmptySetTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::EMPTYSET); + EmptySet emptySet = n.getConst(); + return emptySet.getType(); +} + +TypeNode CardTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::CARD); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "cardinality operates on a set, non-set object found"); + } + } + return nodeManager->integerType(); +} + +TypeNode ComplementTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::COMPLEMENT); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "COMPLEMENT operates on a set, non-set object found"); + } + } + return setType; +} + +TypeNode UniverseSetTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::UNIVERSE_SET); + // for nullary operators, we only computeType for check=true, since they are + // given TypeAttr() on creation + Assert(check); + TypeNode setType = n.getType(); + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate(n, + "Non-set type found for universe set"); + } + return setType; +} + +TypeNode ComprehensionTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::COMPREHENSION); + if (check) + { + if (n[0].getType(check) != nodeManager->boundVarListType()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument of set comprehension is not bound var list"); + } + if (n[1].getType(check) != nodeManager->booleanType()) + { + throw TypeCheckingExceptionPrivate( + n, "body of set comprehension is not boolean"); + } + } + return nodeManager->mkSetType(n[2].getType(check)); +} + +TypeNode ChooseTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::CHOOSE); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "CHOOSE operator expects a set, a non-set is found"); + } + } + return setType.getSetElementType(); +} + +TypeNode IsSingletonTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::IS_SINGLETON); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "IS_SINGLETON operator expects a set, a non-set is found"); + } + } + return nodeManager->booleanType(); +} + +TypeNode InsertTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::INSERT); + size_t numChildren = n.getNumChildren(); + Assert(numChildren >= 2); + TypeNode setType = n[numChildren - 1].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate(n, "inserting into a non-set"); + } + for (size_t i = 0; i < numChildren - 1; ++i) + { + TypeNode elementType = n[i].getType(check); + if (elementType != setType.getSetElementType()) + { + throw TypeCheckingExceptionPrivate( + n, + "type of element should be same as element type of set being " + "inserted into"); + } + } + } + return setType; +} + +TypeNode RelBinaryOperatorTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::PRODUCT || n.getKind() == kind::JOIN); + + TypeNode firstRelType = n[0].getType(check); + TypeNode secondRelType = n[1].getType(check); + TypeNode resultType = firstRelType; + + if (!firstRelType.isSet() || !secondRelType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, " Relational operator operates on non-sets"); + } + if (!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) + { + throw TypeCheckingExceptionPrivate( + n, " Relational operator operates on non-relations (sets of tuples)"); + } + + std::vector newTupleTypes; + std::vector firstTupleTypes = firstRelType[0].getTupleTypes(); + std::vector secondTupleTypes = secondRelType[0].getTupleTypes(); + + // JOIN is not allowed to apply on two unary sets + if (n.getKind() == kind::JOIN) + { + if ((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) + { + throw TypeCheckingExceptionPrivate( + n, " Join operates on two unary relations"); + } + else if (firstTupleTypes.back() != secondTupleTypes.front()) + { + throw TypeCheckingExceptionPrivate( + n, " Join operates on two non-joinable relations"); + } + newTupleTypes.insert(newTupleTypes.end(), + firstTupleTypes.begin(), + firstTupleTypes.end() - 1); + newTupleTypes.insert(newTupleTypes.end(), + secondTupleTypes.begin() + 1, + secondTupleTypes.end()); + } + else if (n.getKind() == kind::PRODUCT) + { + newTupleTypes.insert( + newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()); + newTupleTypes.insert( + newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end()); + } + resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); + + return resultType; +} + +TypeNode RelTransposeTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::TRANSPOSE); + TypeNode setType = n[0].getType(check); + if (check && (!setType.isSet() || !setType.getSetElementType().isTuple())) + { + throw TypeCheckingExceptionPrivate( + n, "relation transpose operates on non-relation"); + } + std::vector tupleTypes = setType[0].getTupleTypes(); + std::reverse(tupleTypes.begin(), tupleTypes.end()); + return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); +} + +TypeNode RelTransClosureTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::TCLOSURE); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet() || !setType.getSetElementType().isTuple()) + { + throw TypeCheckingExceptionPrivate( + n, " transitive closure operates on non-relation"); + } + std::vector tupleTypes = setType[0].getTupleTypes(); + if (tupleTypes.size() != 2) + { + throw TypeCheckingExceptionPrivate( + n, " transitive closure operates on non-binary relations"); + } + if (tupleTypes[0] != tupleTypes[1]) + { + throw TypeCheckingExceptionPrivate( + n, + " transitive closure operates on non-homogeneous binary relations"); + } + } + return setType; +} + +TypeNode JoinImageTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::JOIN_IMAGE); + + TypeNode firstRelType = n[0].getType(check); + + if (!firstRelType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, " JoinImage operator operates on non-relations"); + } + if (!firstRelType[0].isTuple()) + { + throw TypeCheckingExceptionPrivate( + n, " JoinImage operator operates on non-relations (sets of tuples)"); + } + + std::vector tupleTypes = firstRelType[0].getTupleTypes(); + if (tupleTypes.size() != 2) + { + throw TypeCheckingExceptionPrivate( + n, " JoinImage operates on a non-binary relation"); + } + TypeNode valType = n[1].getType(check); + if (valType != nodeManager->integerType()) + { + throw TypeCheckingExceptionPrivate( + n, " JoinImage cardinality constraint must be integer"); + } + std::vector newTupleTypes; + newTupleTypes.push_back(tupleTypes[0]); + return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); +} + +TypeNode RelIdenTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::IDEN); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet() && !setType.getSetElementType().isTuple()) + { + throw TypeCheckingExceptionPrivate(n, + " Identity operates on non-relation"); + } + if (setType[0].getTupleTypes().size() != 1) + { + throw TypeCheckingExceptionPrivate( + n, " Identity operates on non-unary relations"); + } + } + std::vector tupleTypes = setType[0].getTupleTypes(); + tupleTypes.push_back(tupleTypes[0]); + return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); +} + +Cardinality SetsProperties::computeCardinality(TypeNode type) +{ + Assert(type.getKind() == kind::SET_TYPE); + Cardinality elementCard = 2; + elementCard ^= type[0].getCardinality(); + return elementCard; +} + +bool SetsProperties::isWellFounded(TypeNode type) +{ + return type[0].isWellFounded(); +} + +Node SetsProperties::mkGroundTerm(TypeNode type) +{ + Assert(type.isSet()); + return NodeManager::currentNM()->mkConst(EmptySet(type)); +} + +} // namespace sets +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 94e18dc64..f0d8991ce 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -18,9 +18,8 @@ #ifndef CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H #define CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H -#include - -#include "theory/sets/normal_form.h" +#include "expr/node.h" +#include "expr/type_node.h" namespace cvc5 { namespace theory { @@ -28,405 +27,101 @@ namespace sets { struct SetsBinaryOperatorTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION - || n.getKind() == kind::SETMINUS); - TypeNode setType = n[0].getType(check); - if (check) - { - if (!setType.isSet()) - { - throw TypeCheckingExceptionPrivate( - n, "operator expects a set, first argument is not"); - } - TypeNode secondSetType = n[1].getType(check); - if (secondSetType != setType) - { - std::stringstream ss; - ss << "Operator " << n.getKind() - << " expects two sets of the same type. Found types '" << setType - << "' and '" << secondSetType << "'."; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - return setType; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) - { - // only UNION has a const rule in kinds. - // INTERSECTION and SETMINUS are not used in the canonical representation of - // sets and therefore they do not have const rules in kinds - Assert(n.getKind() == kind::UNION); - return NormalForm::checkNormalConstant(n); - } -}; /* struct SetsBinaryOperatorTypeRule */ + static bool computeIsConst(NodeManager* nodeManager, TNode n); +}; -struct SubsetTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::SUBSET); - TypeNode setType = n[0].getType(check); - if( check ) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set"); - } - TypeNode secondSetType = n[1].getType(check); - if(secondSetType != setType) { - if( !setType.isComparableTo( secondSetType ) ){ - throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types"); - } - } - } - return nodeManager->booleanType(); - } -};/* struct SetSubsetTypeRule */ +struct SubsetTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; struct MemberTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - Assert(n.getKind() == kind::MEMBER); - TypeNode setType = n[1].getType(check); - if (check) - { - if (!setType.isSet()) - { - throw TypeCheckingExceptionPrivate( - n, "checking for membership in a non-set"); - } - TypeNode elementType = n[0].getType(check); - // e.g. (member 1 (singleton 1.0)) is true whereas - // (member 1.0 (singleton 1)) throws a typing error - if (!elementType.isSubtypeOf(setType.getSetElementType())) - { - std::stringstream ss; - ss << "member operating on sets of different types:\n" - << "child type: " << elementType << "\n" - << "not subtype: " << setType.getSetElementType() << "\n" - << "in term : " << n; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - return nodeManager->booleanType(); - } -}; /* struct MemberTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; struct SingletonTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - Assert(n.getKind() == kind::SINGLETON && n.hasOperator() - && n.getOperator().getKind() == kind::SINGLETON_OP); - - SingletonOp op = n.getOperator().getConst(); - TypeNode type1 = op.getType(); - if (check) - { - TypeNode type2 = n[0].getType(check); - TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2); - // the type of the element should be a subtype of the type of the operator - // e.g. (singleton (singleton_op Real) 1) where 1 is an Int - if (leastCommonType.isNull() || leastCommonType != type1) - { - std::stringstream ss; - ss << "The type '" << type2 << "' of the element is not a subtype of '" - << type1 << "' in term : " << n; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - return nodeManager->mkSetType(type1); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) - { - Assert(n.getKind() == kind::SINGLETON); - return n[0].isConst(); - } -}; /* struct SingletonTypeRule */ + static bool computeIsConst(NodeManager* nodeManager, TNode n); +}; -struct EmptySetTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::EMPTYSET); - EmptySet emptySet = n.getConst(); - return emptySet.getType(); - } -};/* struct EmptySetTypeRule */ +struct EmptySetTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct CardTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::CARD); - TypeNode setType = n[0].getType(check); - if( check ) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "cardinality operates on a set, non-set object found"); - } - } - return nodeManager->integerType(); - } -};/* struct CardTypeRule */ +struct CardTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct ComplementTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::COMPLEMENT); - TypeNode setType = n[0].getType(check); - if( check ) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found"); - } - } - return setType; - } -};/* struct ComplementTypeRule */ +struct ComplementTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct UniverseSetTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::UNIVERSE_SET); - // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation - Assert(check); - TypeNode setType = n.getType(); - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "Non-set type found for universe set"); - } - return setType; - } -};/* struct ComplementTypeRule */ +struct UniverseSetTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; struct ComprehensionTypeRule { - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::COMPREHENSION); - if (check) - { - if (n[0].getType(check) != nodeManager->boundVarListType()) - { - throw TypeCheckingExceptionPrivate( - n, "first argument of set comprehension is not bound var list"); - } - if (n[1].getType(check) != nodeManager->booleanType()) - { - throw TypeCheckingExceptionPrivate( - n, "body of set comprehension is not boolean"); - } - } - return nodeManager->mkSetType(n[2].getType(check)); - } -}; /* struct ComprehensionTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; struct ChooseTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - Assert(n.getKind() == kind::CHOOSE); - TypeNode setType = n[0].getType(check); - if (check) - { - if (!setType.isSet()) - { - throw TypeCheckingExceptionPrivate( - n, "CHOOSE operator expects a set, a non-set is found"); - } - } - return setType.getSetElementType(); - } -}; /* struct ChooseTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; struct IsSingletonTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - Assert(n.getKind() == kind::IS_SINGLETON); - TypeNode setType = n[0].getType(check); - if (check) - { - if (!setType.isSet()) - { - throw TypeCheckingExceptionPrivate( - n, "IS_SINGLETON operator expects a set, a non-set is found"); - } - } - return nodeManager->booleanType(); - } -}; /* struct IsSingletonTypeRule */ - -struct InsertTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::INSERT); - size_t numChildren = n.getNumChildren(); - Assert(numChildren >= 2); - TypeNode setType = n[numChildren-1].getType(check); - if( check ) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "inserting into a non-set"); - } - for(size_t i = 0; i < numChildren-1; ++i) { - TypeNode elementType = n[i].getType(check); - if(elementType != setType.getSetElementType()) { - throw TypeCheckingExceptionPrivate - (n, "type of element should be same as element type of set being inserted into"); - } - } - } - return setType; - } -};/* struct InsertTypeRule */ - -struct RelBinaryOperatorTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::PRODUCT || n.getKind() == kind::JOIN); - - TypeNode firstRelType = n[0].getType(check); - TypeNode secondRelType = n[1].getType(check); - TypeNode resultType = firstRelType; - - if(!firstRelType.isSet() || !secondRelType.isSet()) { - throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-sets"); - } - if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) { - throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-relations (sets of tuples)"); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; - std::vector newTupleTypes; - std::vector firstTupleTypes = firstRelType[0].getTupleTypes(); - std::vector secondTupleTypes = secondRelType[0].getTupleTypes(); - - // JOIN is not allowed to apply on two unary sets - if( n.getKind() == kind::JOIN ) { - if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) { - throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations"); - } else if(firstTupleTypes.back() != secondTupleTypes.front()) { - throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations"); - } - newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1); - newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end()); - }else if( n.getKind() == kind::PRODUCT ) { - newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()); - newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end()); - } - resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); - - return resultType; - } -};/* struct RelBinaryOperatorTypeRule */ - -struct RelTransposeTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::TRANSPOSE); - TypeNode setType = n[0].getType(check); - if(check && (!setType.isSet() || !setType.getSetElementType().isTuple())) { - throw TypeCheckingExceptionPrivate(n, "relation transpose operates on non-relation"); - } - std::vector tupleTypes = setType[0].getTupleTypes(); - std::reverse(tupleTypes.begin(), tupleTypes.end()); - return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); - } -};/* struct RelTransposeTypeRule */ - -struct RelTransClosureTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::TCLOSURE); - TypeNode setType = n[0].getType(check); - if(check) { - if(!setType.isSet() || !setType.getSetElementType().isTuple()) { - throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-relation"); - } - std::vector tupleTypes = setType[0].getTupleTypes(); - if(tupleTypes.size() != 2) { - throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-binary relations"); - } - if(tupleTypes[0] != tupleTypes[1]) { - throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-homogeneous binary relations"); - } - } - return setType; - } -};/* struct RelTransClosureTypeRule */ +struct InsertTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct JoinImageTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::JOIN_IMAGE); +struct RelBinaryOperatorTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; - TypeNode firstRelType = n[0].getType(check); +struct RelTransposeTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; - if(!firstRelType.isSet()) { - throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations"); - } - if(!firstRelType[0].isTuple()) { - throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations (sets of tuples)"); - } +struct RelTransClosureTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; - std::vector tupleTypes = firstRelType[0].getTupleTypes(); - if(tupleTypes.size() != 2) { - throw TypeCheckingExceptionPrivate(n, " JoinImage operates on a non-binary relation"); - } - TypeNode valType = n[1].getType(check); - if (valType != nodeManager->integerType()) { - throw TypeCheckingExceptionPrivate( - n, " JoinImage cardinality constraint must be integer"); - } - std::vector newTupleTypes; - newTupleTypes.push_back(tupleTypes[0]); - return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); - } -};/* struct JoinImageTypeRule */ +struct JoinImageTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct RelIdenTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::IDEN); - TypeNode setType = n[0].getType(check); - if(check) { - if(!setType.isSet() && !setType.getSetElementType().isTuple()) { - throw TypeCheckingExceptionPrivate(n, " Identity operates on non-relation"); - } - if(setType[0].getTupleTypes().size() != 1) { - throw TypeCheckingExceptionPrivate(n, " Identity operates on non-unary relations"); - } - } - std::vector tupleTypes = setType[0].getTupleTypes(); - tupleTypes.push_back(tupleTypes[0]); - return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); - } -};/* struct RelIdenTypeRule */ +struct RelIdenTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct SetsProperties { - inline static Cardinality computeCardinality(TypeNode type) { - Assert(type.getKind() == kind::SET_TYPE); - Cardinality elementCard = 2; - elementCard ^= type[0].getCardinality(); - return elementCard; - } +struct SetsProperties +{ + static Cardinality computeCardinality(TypeNode type); - inline static bool isWellFounded(TypeNode type) { - return type[0].isWellFounded(); - } + static bool isWellFounded(TypeNode type); - inline static Node mkGroundTerm(TypeNode type) { - Assert(type.isSet()); - return NodeManager::currentNM()->mkConst(EmptySet(type)); - } -};/* struct SetsProperties */ + static Node mkGroundTerm(TypeNode type); +}; } // namespace sets } // namespace theory