diff options
| -rw-r--r-- | src/theory/bags/theory_bags_type_rules.h | 14 | ||||
| -rw-r--r-- | src/theory/sets/singleton_op.cpp | 2 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_rules.cpp | 9 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 73 |
4 files changed, 88 insertions, 10 deletions
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index 3bc3b3462..d7b8b2737 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -31,7 +31,7 @@ namespace bags { /** * Type rule for binary operators (bag.union_max, bag.union_disjoint, * bag.inter_min bag.difference_subtract, bag.difference_remove) to check - * if the two arguments are of the same sort. + * if the two arguments are bags of the same sort. */ struct BinaryOperatorTypeRule { @@ -40,8 +40,8 @@ struct BinaryOperatorTypeRule }; /* struct BinaryOperatorTypeRule */ /** - * Type rule for binary operator bag.subbag to check if the two arguments have - * the same sort. + * Type rule for binary operator bag.subbag to check if the two arguments are + * bags of the same sort. */ struct SubBagTypeRule { @@ -76,7 +76,7 @@ struct BagMakeTypeRule }; /* struct BagMakeTypeRule */ /** - * Type rule for bag.is_singleton to check the argument is of a bag. + * Type rule for (bag.is_singleton B) to check the argument B is a bag. */ struct IsSingletonTypeRule { @@ -84,7 +84,7 @@ struct IsSingletonTypeRule }; /* struct IsSingletonTypeRule */ /** - * Type rule for (as bag.empty (Bag ...)) + * Type rule for (as bag.empty (Bag T)) where T is a type */ struct EmptyBagTypeRule { @@ -92,7 +92,7 @@ struct EmptyBagTypeRule }; /* struct EmptyBagTypeRule */ /** - * Type rule for (bag.card ..) to check the argument is of a bag. + * Type rule for (bag.card B) to check the argument B is a bag. */ struct CardTypeRule { @@ -100,7 +100,7 @@ struct CardTypeRule }; /* struct CardTypeRule */ /** - * Type rule for (bag.choose ..) to check the argument is of a bag. + * Type rule for (bag.choose B) to check the argument B is a bag. */ struct ChooseTypeRule { diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp index fb64b01cd..327df6984 100644 --- a/src/theory/sets/singleton_op.cpp +++ b/src/theory/sets/singleton_op.cpp @@ -23,7 +23,7 @@ namespace cvc5 { std::ostream& operator<<(std::ostream& out, const SetSingletonOp& op) { - return out << "(singleton_op " << op.getType() << ')'; + return out << "(SetSingletonOp " << op.getType() << ')'; } size_t SetSingletonOpHashFunction::operator()(const SetSingletonOp& op) const diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index 8101661bd..a8a79d5f9 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -131,7 +131,7 @@ TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager, 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 + // e.g. (set.singleton (SetSingletonOp Real) 1) where 1 is an Int if (leastCommonType.isNull() || leastCommonType != type1) { std::stringstream ss; @@ -463,6 +463,13 @@ TypeNode JoinImageTypeRule::computeType(NodeManager* nodeManager, throw TypeCheckingExceptionPrivate( n, " JoinImage operates on a non-binary relation"); } + if (tupleTypes[0] != tupleTypes[1]) + { + // TODO: Investigate supporting JoinImage for general binary + // relationshttps://github.com/cvc5/cvc5-projects/issues/346 + throw TypeCheckingExceptionPrivate( + n, " JoinImage operates on a pair of different types"); + } TypeNode valType = n[1].getType(check); if (valType != nodeManager->integerType()) { diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index b793205c0..dc473d145 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -25,23 +25,38 @@ namespace cvc5 { namespace theory { namespace sets { +/** + * Type rule for binary operators (set.union, set.inter_min, set.minus) to check + * if the two arguments are sets of the same sort. + */ struct SetsBinaryOperatorTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); - static bool computeIsConst(NodeManager* nodeManager, TNode n); }; +/** + * Type rule for binary operator set.subset to check if the two arguments are + * sets of the same sort. + */ struct SubsetTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for binary operator set.member to check the sort of the first + * argument matches the element sort of the given set. + */ struct MemberTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for (set.singleton (SetSingletonOp t) x) to check the sort of x + * matches the sort t. + */ struct SingletonTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); @@ -49,41 +64,68 @@ struct SingletonTypeRule static bool computeIsConst(NodeManager* nodeManager, TNode n); }; +/** + * Type rule for (as set.empty (Set T)) where T is a type + */ struct EmptySetTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for (bag.card A) to check the argument A is a set. + */ struct CardTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for (set.complement A) to check the argument A is a set. + */ struct ComplementTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for (as set.universe (Set T)) where T is a type + */ struct UniverseSetTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for (set.comprehension ((x1 T1) ... (xn Tn)) predicate body) + * that checks x1 ... xn are bound variables, predicate is a boolean term, + * and computes the type (Set T) where T is the type of body + */ struct ComprehensionTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for (set.choose A) to check the argument A is a set. + */ struct ChooseTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for (set.is_singleton A) to check the argument A is a set. + */ struct IsSingletonTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for (set.insert e1 ... en A) that checks the sorts of e1, ..., en + * match the element sort of the set A + */ struct InsertTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); @@ -98,26 +140,55 @@ struct SetMapTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; /* struct SetMapTypeRule */ +/** + * Type rule for binary operators (rel.join, rel.product) to check + * if the two arguments are relations (set of tuples). + * For arguments A of type (Set (Tuple A1 ... Am)) and B of type + * (Set (Tuple B1 ... Bn)): + * - (rel.product A B): it computes the type (Set (Tuple (A1 ... Am B1 ... Bn)). + * - (rel.join A B) it checks that m, n > 1 and Am = B1 and computes the type + * (Set (Tuple (A1 ... Am-1 B2 ... Bn)). + */ struct RelBinaryOperatorTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for unary operator (rel.transpose A) to check that A is a relation + * (set of Tuples). For an argument A of type (Set (Tuple A1 ... An)) + * it reveres A1 ... An and computes the type (Set (Tuple An ... A1)). + */ struct RelTransposeTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for unary operator (rel.tclosure A) to check that A is a binary + * relation of type (Set (Tuple T T)), where T is a type + */ struct RelTransClosureTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for operator (rel.join_image A c) that checks A is a binary + * relation of type (Set (Tuple T T)), where T is a type, and c is an integer + * term (in fact c should be a non-negative constant, otherwise a logic + * exception is thrown TheorySetsPrivate::preRegisterTerm). + */ struct JoinImageTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for unary operator (rel.iden A) to check that A is a unary relation + * of type (Set (Tuple T)) and computes the type (Set (Tuple T T)) for the + * identity + */ struct RelIdenTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); |