Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/sets/theory_sets_type_rules.cpp	Lines:	161	205	78.5 %
Date:	2021-09-29	Branches:	280	1072	26.1 %


/******************************************************************************
 * 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 <climits>
#include <sstream>

#include "theory/sets/normal_form.h"
#include "theory/sets/singleton_op.h"
#include "util/cardinality.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<SingletonOp>();
  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<EmptySet>();
  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<TypeNode> newTupleTypes;
  std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes();
  std::vector<TypeNode> 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<TypeNode> 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<TypeNode> 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<TypeNode> 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<TypeNode> 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<TypeNode> 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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Sets theory type rules.
14		*/
15
16		#include "theory/sets/theory_sets_type_rules.h"
17
18		#include <climits>
19		#include <sstream>
20
21		#include "theory/sets/normal_form.h"
22		#include "theory/sets/singleton_op.h"
23		#include "util/cardinality.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace sets {
28
29	5005	TypeNode SetsBinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
30		TNode n,
31		bool check)
32		{
33	5005	Assert(n.getKind() == kind::UNION \|\| n.getKind() == kind::INTERSECTION
34		\|\| n.getKind() == kind::SETMINUS);
35	5005	TypeNode setType = n[0].getType(check);
36	5005	if (check)
37		{
38	5005	if (!setType.isSet())
39		{
40		throw TypeCheckingExceptionPrivate(
41		n, "operator expects a set, first argument is not");
42		}
43	10010	TypeNode secondSetType = n[1].getType(check);
44	5005	if (secondSetType != setType)
45		{
46	4	std::stringstream ss;
47	2	ss << "Operator " << n.getKind()
48	2	<< " expects two sets of the same type. Found types '" << setType
49	2	<< "' and '" << secondSetType << "'.";
50	2	throw TypeCheckingExceptionPrivate(n, ss.str());
51		}
52		}
53	5003	return setType;
54		}
55
56	3108	bool SetsBinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager,
57		TNode n)
58		{
59		// only UNION has a const rule in kinds.
60		// INTERSECTION and SETMINUS are not used in the canonical representation of
61		// sets and therefore they do not have const rules in kinds
62	3108	Assert(n.getKind() == kind::UNION);
63	3108	return NormalForm::checkNormalConstant(n);
64		}
65
66	206	TypeNode SubsetTypeRule::computeType(NodeManager* nodeManager,
67		TNode n,
68		bool check)
69		{
70	206	Assert(n.getKind() == kind::SUBSET);
71	412	TypeNode setType = n[0].getType(check);
72	206	if (check)
73		{
74	206	if (!setType.isSet())
75		{
76		throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set");
77		}
78	412	TypeNode secondSetType = n[1].getType(check);
79	206	if (secondSetType != setType)
80		{
81		if (!setType.isComparableTo(secondSetType))
82		{
83		throw TypeCheckingExceptionPrivate(
84		n, "set subset operating on sets of different types");
85		}
86		}
87		}
88	412	return nodeManager->booleanType();
89		}
90
91	11180	TypeNode MemberTypeRule::computeType(NodeManager* nodeManager,
92		TNode n,
93		bool check)
94		{
95	11180	Assert(n.getKind() == kind::MEMBER);
96	22360	TypeNode setType = n[1].getType(check);
97	11180	if (check)
98		{
99	11180	if (!setType.isSet())
100		{
101		throw TypeCheckingExceptionPrivate(
102		n, "checking for membership in a non-set");
103		}
104	22360	TypeNode elementType = n[0].getType(check);
105		// e.g. (member 1 (singleton 1.0)) is true whereas
106		// (member 1.0 (singleton 1)) throws a typing error
107	11180	if (!elementType.isSubtypeOf(setType.getSetElementType()))
108		{
109		std::stringstream ss;
110		ss << "member operating on sets of different types:\n"
111		<< "child type: " << elementType << "\n"
112		<< "not subtype: " << setType.getSetElementType() << "\n"
113		<< "in term : " << n;
114		throw TypeCheckingExceptionPrivate(n, ss.str());
115		}
116		}
117	22360	return nodeManager->booleanType();
118		}
119
120	1909	TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager,
121		TNode n,
122		bool check)
123		{
124	1909	Assert(n.getKind() == kind::SINGLETON && n.hasOperator()
125		&& n.getOperator().getKind() == kind::SINGLETON_OP);
126
127	3818	SingletonOp op = n.getOperator().getConst<SingletonOp>();
128	3818	TypeNode type1 = op.getType();
129	1909	if (check)
130		{
131	3818	TypeNode type2 = n[0].getType(check);
132	3818	TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2);
133		// the type of the element should be a subtype of the type of the operator
134		// e.g. (singleton (singleton_op Real) 1) where 1 is an Int
135	1909	if (leastCommonType.isNull() \|\| leastCommonType != type1)
136		{
137		std::stringstream ss;
138		ss << "The type '" << type2 << "' of the element is not a subtype of '"
139		<< type1 << "' in term : " << n;
140		throw TypeCheckingExceptionPrivate(n, ss.str());
141		}
142		}
143	3818	return nodeManager->mkSetType(type1);
144		}
145
146	1757	bool SingletonTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
147		{
148	1757	Assert(n.getKind() == kind::SINGLETON);
149	1757	return n[0].isConst();
150		}
151
152	1721	TypeNode EmptySetTypeRule::computeType(NodeManager* nodeManager,
153		TNode n,
154		bool check)
155		{
156	1721	Assert(n.getKind() == kind::EMPTYSET);
157	3442	EmptySet emptySet = n.getConst<EmptySet>();
158	3442	return emptySet.getType();
159		}
160
161	1630	TypeNode CardTypeRule::computeType(NodeManager* nodeManager,
162		TNode n,
163		bool check)
164		{
165	1630	Assert(n.getKind() == kind::CARD);
166	3260	TypeNode setType = n[0].getType(check);
167	1630	if (check)
168		{
169	1630	if (!setType.isSet())
170		{
171		throw TypeCheckingExceptionPrivate(
172		n, "cardinality operates on a set, non-set object found");
173		}
174		}
175	3260	return nodeManager->integerType();
176		}
177
178	16	TypeNode ComplementTypeRule::computeType(NodeManager* nodeManager,
179		TNode n,
180		bool check)
181		{
182	16	Assert(n.getKind() == kind::COMPLEMENT);
183	16	TypeNode setType = n[0].getType(check);
184	16	if (check)
185		{
186	16	if (!setType.isSet())
187		{
188		throw TypeCheckingExceptionPrivate(
189		n, "COMPLEMENT operates on a set, non-set object found");
190		}
191		}
192	16	return setType;
193		}
194
195	89	TypeNode UniverseSetTypeRule::computeType(NodeManager* nodeManager,
196		TNode n,
197		bool check)
198		{
199	89	Assert(n.getKind() == kind::UNIVERSE_SET);
200		// for nullary operators, we only computeType for check=true, since they are
201		// given TypeAttr() on creation
202	89	Assert(check);
203	89	TypeNode setType = n.getType();
204	89	if (!setType.isSet())
205		{
206		throw TypeCheckingExceptionPrivate(n,
207		"Non-set type found for universe set");
208		}
209	89	return setType;
210		}
211
212	22	TypeNode ComprehensionTypeRule::computeType(NodeManager* nodeManager,
213		TNode n,
214		bool check)
215		{
216	22	Assert(n.getKind() == kind::COMPREHENSION);
217	22	if (check)
218		{
219	22	if (n[0].getType(check) != nodeManager->boundVarListType())
220		{
221		throw TypeCheckingExceptionPrivate(
222		n, "first argument of set comprehension is not bound var list");
223		}
224	22	if (n[1].getType(check) != nodeManager->booleanType())
225		{
226		throw TypeCheckingExceptionPrivate(
227		n, "body of set comprehension is not boolean");
228		}
229		}
230	22	return nodeManager->mkSetType(n[2].getType(check));
231		}
232
233	16	TypeNode ChooseTypeRule::computeType(NodeManager* nodeManager,
234		TNode n,
235		bool check)
236		{
237	16	Assert(n.getKind() == kind::CHOOSE);
238	32	TypeNode setType = n[0].getType(check);
239	16	if (check)
240		{
241	16	if (!setType.isSet())
242		{
243		throw TypeCheckingExceptionPrivate(
244		n, "CHOOSE operator expects a set, a non-set is found");
245		}
246		}
247	32	return setType.getSetElementType();
248		}
249
250	17	TypeNode IsSingletonTypeRule::computeType(NodeManager* nodeManager,
251		TNode n,
252		bool check)
253		{
254	17	Assert(n.getKind() == kind::IS_SINGLETON);
255	34	TypeNode setType = n[0].getType(check);
256	17	if (check)
257		{
258	17	if (!setType.isSet())
259		{
260		throw TypeCheckingExceptionPrivate(
261		n, "IS_SINGLETON operator expects a set, a non-set is found");
262		}
263		}
264	34	return nodeManager->booleanType();
265		}
266
267	25	TypeNode InsertTypeRule::computeType(NodeManager* nodeManager,
268		TNode n,
269		bool check)
270		{
271	25	Assert(n.getKind() == kind::INSERT);
272	25	size_t numChildren = n.getNumChildren();
273	25	Assert(numChildren >= 2);
274	25	TypeNode setType = n[numChildren - 1].getType(check);
275	25	if (check)
276		{
277	25	if (!setType.isSet())
278		{
279		throw TypeCheckingExceptionPrivate(n, "inserting into a non-set");
280		}
281	82	for (size_t i = 0; i < numChildren - 1; ++i)
282		{
283	114	TypeNode elementType = n[i].getType(check);
284	57	if (elementType != setType.getSetElementType())
285		{
286		throw TypeCheckingExceptionPrivate(
287		n,
288		"type of element should be same as element type of set being "
289		"inserted into");
290		}
291		}
292		}
293	25	return setType;
294		}
295
296	207	TypeNode RelBinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
297		TNode n,
298		bool check)
299		{
300	207	Assert(n.getKind() == kind::PRODUCT \|\| n.getKind() == kind::JOIN);
301
302	414	TypeNode firstRelType = n[0].getType(check);
303	414	TypeNode secondRelType = n[1].getType(check);
304	207	TypeNode resultType = firstRelType;
305
306	207	if (!firstRelType.isSet() \|\| !secondRelType.isSet())
307		{
308		throw TypeCheckingExceptionPrivate(
309		n, " Relational operator operates on non-sets");
310		}
311	207	if (!firstRelType[0].isTuple() \|\| !secondRelType[0].isTuple())
312		{
313		throw TypeCheckingExceptionPrivate(
314		n, " Relational operator operates on non-relations (sets of tuples)");
315		}
316
317	414	std::vector<TypeNode> newTupleTypes;
318	414	std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes();
319	414	std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes();
320
321		// JOIN is not allowed to apply on two unary sets
322	207	if (n.getKind() == kind::JOIN)
323		{
324	176	if ((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1))
325		{
326		throw TypeCheckingExceptionPrivate(
327		n, " Join operates on two unary relations");
328		}
329	176	else if (firstTupleTypes.back() != secondTupleTypes.front())
330		{
331		throw TypeCheckingExceptionPrivate(
332		n, " Join operates on two non-joinable relations");
333		}
334	528	newTupleTypes.insert(newTupleTypes.end(),
335		firstTupleTypes.begin(),
336	704	firstTupleTypes.end() - 1);
337	528	newTupleTypes.insert(newTupleTypes.end(),
338	352	secondTupleTypes.begin() + 1,
339	704	secondTupleTypes.end());
340		}
341	31	else if (n.getKind() == kind::PRODUCT)
342		{
343	31	newTupleTypes.insert(
344	62	newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end());
345	31	newTupleTypes.insert(
346	62	newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end());
347		}
348	207	resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
349
350	414	return resultType;
351		}
352
353	59	TypeNode RelTransposeTypeRule::computeType(NodeManager* nodeManager,
354		TNode n,
355		bool check)
356		{
357	59	Assert(n.getKind() == kind::TRANSPOSE);
358	118	TypeNode setType = n[0].getType(check);
359	59	if (check && (!setType.isSet() \|\| !setType.getSetElementType().isTuple()))
360		{
361		throw TypeCheckingExceptionPrivate(
362		n, "relation transpose operates on non-relation");
363		}
364	118	std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
365	59	std::reverse(tupleTypes.begin(), tupleTypes.end());
366	118	return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
367		}
368
369	31	TypeNode RelTransClosureTypeRule::computeType(NodeManager* nodeManager,
370		TNode n,
371		bool check)
372		{
373	31	Assert(n.getKind() == kind::TCLOSURE);
374	31	TypeNode setType = n[0].getType(check);
375	31	if (check)
376		{
377	31	if (!setType.isSet() \|\| !setType.getSetElementType().isTuple())
378		{
379		throw TypeCheckingExceptionPrivate(
380		n, " transitive closure operates on non-relation");
381		}
382	62	std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
383	31	if (tupleTypes.size() != 2)
384		{
385		throw TypeCheckingExceptionPrivate(
386		n, " transitive closure operates on non-binary relations");
387		}
388	31	if (tupleTypes[0] != tupleTypes[1])
389		{
390		throw TypeCheckingExceptionPrivate(
391		n,
392		" transitive closure operates on non-homogeneous binary relations");
393		}
394		}
395	31	return setType;
396		}
397
398	28	TypeNode JoinImageTypeRule::computeType(NodeManager* nodeManager,
399		TNode n,
400		bool check)
401		{
402	28	Assert(n.getKind() == kind::JOIN_IMAGE);
403
404	56	TypeNode firstRelType = n[0].getType(check);
405
406	28	if (!firstRelType.isSet())
407		{
408		throw TypeCheckingExceptionPrivate(
409		n, " JoinImage operator operates on non-relations");
410		}
411	28	if (!firstRelType[0].isTuple())
412		{
413		throw TypeCheckingExceptionPrivate(
414		n, " JoinImage operator operates on non-relations (sets of tuples)");
415		}
416
417	56	std::vector<TypeNode> tupleTypes = firstRelType[0].getTupleTypes();
418	28	if (tupleTypes.size() != 2)
419		{
420		throw TypeCheckingExceptionPrivate(
421		n, " JoinImage operates on a non-binary relation");
422		}
423	56	TypeNode valType = n[1].getType(check);
424	28	if (valType != nodeManager->integerType())
425		{
426		throw TypeCheckingExceptionPrivate(
427		n, " JoinImage cardinality constraint must be integer");
428		}
429	56	std::vector<TypeNode> newTupleTypes;
430	28	newTupleTypes.push_back(tupleTypes[0]);
431	56	return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
432		}
433
434	5	TypeNode RelIdenTypeRule::computeType(NodeManager* nodeManager,
435		TNode n,
436		bool check)
437		{
438	5	Assert(n.getKind() == kind::IDEN);
439	10	TypeNode setType = n[0].getType(check);
440	5	if (check)
441		{
442	5	if (!setType.isSet() && !setType.getSetElementType().isTuple())
443		{
444		throw TypeCheckingExceptionPrivate(n,
445		" Identity operates on non-relation");
446		}
447	5	if (setType[0].getTupleTypes().size() != 1)
448		{
449		throw TypeCheckingExceptionPrivate(
450		n, " Identity operates on non-unary relations");
451		}
452		}
453	10	std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
454	5	tupleTypes.push_back(tupleTypes[0]);
455	10	return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
456		}
457
458		Cardinality SetsProperties::computeCardinality(TypeNode type)
459		{
460		Assert(type.getKind() == kind::SET_TYPE);
461		Cardinality elementCard = 2;
462		elementCard ^= type[0].getCardinality();
463		return elementCard;
464		}
465
466		bool SetsProperties::isWellFounded(TypeNode type)
467		{
468		return type[0].isWellFounded();
469		}
470
471	6	Node SetsProperties::mkGroundTerm(TypeNode type)
472		{
473	6	Assert(type.isSet());
474	6	return NodeManager::currentNM()->mkConst(EmptySet(type));
475		}
476
477		} // namespace sets
478		} // namespace theory
479	22746	} // namespace cvc5