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-08-01	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"
#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	7412	TypeNode SetsBinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
30		TNode n,
31		bool check)
32		{
33	7412	Assert(n.getKind() == kind::UNION \|\| n.getKind() == kind::INTERSECTION
34		\|\| n.getKind() == kind::SETMINUS);
35	7412	TypeNode setType = n[0].getType(check);
36	7412	if (check)
37		{
38	7412	if (!setType.isSet())
39		{
40		throw TypeCheckingExceptionPrivate(
41		n, "operator expects a set, first argument is not");
42		}
43	14824	TypeNode secondSetType = n[1].getType(check);
44	7412	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	7410	return setType;
54		}
55
56	4233	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	4233	Assert(n.getKind() == kind::UNION);
63	4233	return NormalForm::checkNormalConstant(n);
64		}
65
66	370	TypeNode SubsetTypeRule::computeType(NodeManager* nodeManager,
67		TNode n,
68		bool check)
69		{
70	370	Assert(n.getKind() == kind::SUBSET);
71	740	TypeNode setType = n[0].getType(check);
72	370	if (check)
73		{
74	370	if (!setType.isSet())
75		{
76		throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set");
77		}
78	740	TypeNode secondSetType = n[1].getType(check);
79	370	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	740	return nodeManager->booleanType();
89		}
90
91	23331	TypeNode MemberTypeRule::computeType(NodeManager* nodeManager,
92		TNode n,
93		bool check)
94		{
95	23331	Assert(n.getKind() == kind::MEMBER);
96	46662	TypeNode setType = n[1].getType(check);
97	23331	if (check)
98		{
99	23331	if (!setType.isSet())
100		{
101		throw TypeCheckingExceptionPrivate(
102		n, "checking for membership in a non-set");
103		}
104	46662	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	23331	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	46662	return nodeManager->booleanType();
118		}
119
120	3150	TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager,
121		TNode n,
122		bool check)
123		{
124	3150	Assert(n.getKind() == kind::SINGLETON && n.hasOperator()
125		&& n.getOperator().getKind() == kind::SINGLETON_OP);
126
127	6300	SingletonOp op = n.getOperator().getConst<SingletonOp>();
128	6300	TypeNode type1 = op.getType();
129	3150	if (check)
130		{
131	6300	TypeNode type2 = n[0].getType(check);
132	6300	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	3150	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	6300	return nodeManager->mkSetType(type1);
144		}
145
146	2941	bool SingletonTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
147		{
148	2941	Assert(n.getKind() == kind::SINGLETON);
149	2941	return n[0].isConst();
150		}
151
152	1956	TypeNode EmptySetTypeRule::computeType(NodeManager* nodeManager,
153		TNode n,
154		bool check)
155		{
156	1956	Assert(n.getKind() == kind::EMPTYSET);
157	3912	EmptySet emptySet = n.getConst<EmptySet>();
158	3912	return emptySet.getType();
159		}
160
161	2719	TypeNode CardTypeRule::computeType(NodeManager* nodeManager,
162		TNode n,
163		bool check)
164		{
165	2719	Assert(n.getKind() == kind::CARD);
166	5438	TypeNode setType = n[0].getType(check);
167	2719	if (check)
168		{
169	2719	if (!setType.isSet())
170		{
171		throw TypeCheckingExceptionPrivate(
172		n, "cardinality operates on a set, non-set object found");
173		}
174		}
175	5438	return nodeManager->integerType();
176		}
177
178	23	TypeNode ComplementTypeRule::computeType(NodeManager* nodeManager,
179		TNode n,
180		bool check)
181		{
182	23	Assert(n.getKind() == kind::COMPLEMENT);
183	23	TypeNode setType = n[0].getType(check);
184	23	if (check)
185		{
186	23	if (!setType.isSet())
187		{
188		throw TypeCheckingExceptionPrivate(
189		n, "COMPLEMENT operates on a set, non-set object found");
190		}
191		}
192	23	return setType;
193		}
194
195	134	TypeNode UniverseSetTypeRule::computeType(NodeManager* nodeManager,
196		TNode n,
197		bool check)
198		{
199	134	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	134	Assert(check);
203	134	TypeNode setType = n.getType();
204	134	if (!setType.isSet())
205		{
206		throw TypeCheckingExceptionPrivate(n,
207		"Non-set type found for universe set");
208		}
209	134	return setType;
210		}
211
212	53	TypeNode ComprehensionTypeRule::computeType(NodeManager* nodeManager,
213		TNode n,
214		bool check)
215		{
216	53	Assert(n.getKind() == kind::COMPREHENSION);
217	53	if (check)
218		{
219	53	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	53	if (n[1].getType(check) != nodeManager->booleanType())
225		{
226		throw TypeCheckingExceptionPrivate(
227		n, "body of set comprehension is not boolean");
228		}
229		}
230	53	return nodeManager->mkSetType(n[2].getType(check));
231		}
232
233	18	TypeNode ChooseTypeRule::computeType(NodeManager* nodeManager,
234		TNode n,
235		bool check)
236		{
237	18	Assert(n.getKind() == kind::CHOOSE);
238	36	TypeNode setType = n[0].getType(check);
239	18	if (check)
240		{
241	18	if (!setType.isSet())
242		{
243		throw TypeCheckingExceptionPrivate(
244		n, "CHOOSE operator expects a set, a non-set is found");
245		}
246		}
247	36	return setType.getSetElementType();
248		}
249
250	29	TypeNode IsSingletonTypeRule::computeType(NodeManager* nodeManager,
251		TNode n,
252		bool check)
253		{
254	29	Assert(n.getKind() == kind::IS_SINGLETON);
255	58	TypeNode setType = n[0].getType(check);
256	29	if (check)
257		{
258	29	if (!setType.isSet())
259		{
260		throw TypeCheckingExceptionPrivate(
261		n, "IS_SINGLETON operator expects a set, a non-set is found");
262		}
263		}
264	58	return nodeManager->booleanType();
265		}
266
267	31	TypeNode InsertTypeRule::computeType(NodeManager* nodeManager,
268		TNode n,
269		bool check)
270		{
271	31	Assert(n.getKind() == kind::INSERT);
272	31	size_t numChildren = n.getNumChildren();
273	31	Assert(numChildren >= 2);
274	31	TypeNode setType = n[numChildren - 1].getType(check);
275	31	if (check)
276		{
277	31	if (!setType.isSet())
278		{
279		throw TypeCheckingExceptionPrivate(n, "inserting into a non-set");
280		}
281	110	for (size_t i = 0; i < numChildren - 1; ++i)
282		{
283	158	TypeNode elementType = n[i].getType(check);
284	79	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	31	return setType;
294		}
295
296	365	TypeNode RelBinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
297		TNode n,
298		bool check)
299		{
300	365	Assert(n.getKind() == kind::PRODUCT \|\| n.getKind() == kind::JOIN);
301
302	730	TypeNode firstRelType = n[0].getType(check);
303	730	TypeNode secondRelType = n[1].getType(check);
304	365	TypeNode resultType = firstRelType;
305
306	365	if (!firstRelType.isSet() \|\| !secondRelType.isSet())
307		{
308		throw TypeCheckingExceptionPrivate(
309		n, " Relational operator operates on non-sets");
310		}
311	365	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	730	std::vector<TypeNode> newTupleTypes;
318	730	std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes();
319	730	std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes();
320
321		// JOIN is not allowed to apply on two unary sets
322	365	if (n.getKind() == kind::JOIN)
323		{
324	318	if ((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1))
325		{
326		throw TypeCheckingExceptionPrivate(
327		n, " Join operates on two unary relations");
328		}
329	318	else if (firstTupleTypes.back() != secondTupleTypes.front())
330		{
331		throw TypeCheckingExceptionPrivate(
332		n, " Join operates on two non-joinable relations");
333		}
334	954	newTupleTypes.insert(newTupleTypes.end(),
335		firstTupleTypes.begin(),
336	1272	firstTupleTypes.end() - 1);
337	954	newTupleTypes.insert(newTupleTypes.end(),
338	636	secondTupleTypes.begin() + 1,
339	1272	secondTupleTypes.end());
340		}
341	47	else if (n.getKind() == kind::PRODUCT)
342		{
343	47	newTupleTypes.insert(
344	94	newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end());
345	47	newTupleTypes.insert(
346	94	newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end());
347		}
348	365	resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
349
350	730	return resultType;
351		}
352
353	119	TypeNode RelTransposeTypeRule::computeType(NodeManager* nodeManager,
354		TNode n,
355		bool check)
356		{
357	119	Assert(n.getKind() == kind::TRANSPOSE);
358	238	TypeNode setType = n[0].getType(check);
359	119	if (check && (!setType.isSet() \|\| !setType.getSetElementType().isTuple()))
360		{
361		throw TypeCheckingExceptionPrivate(
362		n, "relation transpose operates on non-relation");
363		}
364	238	std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
365	119	std::reverse(tupleTypes.begin(), tupleTypes.end());
366	238	return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
367		}
368
369	44	TypeNode RelTransClosureTypeRule::computeType(NodeManager* nodeManager,
370		TNode n,
371		bool check)
372		{
373	44	Assert(n.getKind() == kind::TCLOSURE);
374	44	TypeNode setType = n[0].getType(check);
375	44	if (check)
376		{
377	44	if (!setType.isSet() \|\| !setType.getSetElementType().isTuple())
378		{
379		throw TypeCheckingExceptionPrivate(
380		n, " transitive closure operates on non-relation");
381		}
382	88	std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
383	44	if (tupleTypes.size() != 2)
384		{
385		throw TypeCheckingExceptionPrivate(
386		n, " transitive closure operates on non-binary relations");
387		}
388	44	if (tupleTypes[0] != tupleTypes[1])
389		{
390		throw TypeCheckingExceptionPrivate(
391		n,
392		" transitive closure operates on non-homogeneous binary relations");
393		}
394		}
395	44	return setType;
396		}
397
398	38	TypeNode JoinImageTypeRule::computeType(NodeManager* nodeManager,
399		TNode n,
400		bool check)
401		{
402	38	Assert(n.getKind() == kind::JOIN_IMAGE);
403
404	76	TypeNode firstRelType = n[0].getType(check);
405
406	38	if (!firstRelType.isSet())
407		{
408		throw TypeCheckingExceptionPrivate(
409		n, " JoinImage operator operates on non-relations");
410		}
411	38	if (!firstRelType[0].isTuple())
412		{
413		throw TypeCheckingExceptionPrivate(
414		n, " JoinImage operator operates on non-relations (sets of tuples)");
415		}
416
417	76	std::vector<TypeNode> tupleTypes = firstRelType[0].getTupleTypes();
418	38	if (tupleTypes.size() != 2)
419		{
420		throw TypeCheckingExceptionPrivate(
421		n, " JoinImage operates on a non-binary relation");
422		}
423	76	TypeNode valType = n[1].getType(check);
424	38	if (valType != nodeManager->integerType())
425		{
426		throw TypeCheckingExceptionPrivate(
427		n, " JoinImage cardinality constraint must be integer");
428		}
429	76	std::vector<TypeNode> newTupleTypes;
430	38	newTupleTypes.push_back(tupleTypes[0]);
431	76	return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
432		}
433
434	9	TypeNode RelIdenTypeRule::computeType(NodeManager* nodeManager,
435		TNode n,
436		bool check)
437		{
438	9	Assert(n.getKind() == kind::IDEN);
439	18	TypeNode setType = n[0].getType(check);
440	9	if (check)
441		{
442	9	if (!setType.isSet() && !setType.getSetElementType().isTuple())
443		{
444		throw TypeCheckingExceptionPrivate(n,
445		" Identity operates on non-relation");
446		}
447	9	if (setType[0].getTupleTypes().size() != 1)
448		{
449		throw TypeCheckingExceptionPrivate(
450		n, " Identity operates on non-unary relations");
451		}
452		}
453	18	std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
454	9	tupleTypes.push_back(tupleTypes[0]);
455	18	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	29280	} // namespace cvc5