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-05-22	Branches:	280	1074	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"

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