Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bags/theory_bags_type_rules.cpp	Lines:	111	153	72.5 %
Date:	2021-09-15	Branches:	220	796	27.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mudathir Mohamed, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Bags theory type rules.
 */

#include "theory/bags/theory_bags_type_rules.h"

#include <sstream>

#include "base/check.h"
#include "expr/emptybag.h"
#include "theory/bags/make_bag_op.h"
#include "theory/bags/normal_form.h"
#include "util/cardinality.h"
#include "util/rational.h"

namespace cvc5 {
namespace theory {
namespace bags {

TypeNode BinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
{
  Assert(n.getKind() == kind::UNION_MAX || n.getKind() == kind::UNION_DISJOINT
         || n.getKind() == kind::INTERSECTION_MIN
         || n.getKind() == kind::DIFFERENCE_SUBTRACT
         || n.getKind() == kind::DIFFERENCE_REMOVE);
  TypeNode bagType = n[0].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      throw TypeCheckingExceptionPrivate(
          n, "operator expects a bag, first argument is not");
    }
    TypeNode secondBagType = n[1].getType(check);
    if (secondBagType != bagType)
    {
      std::stringstream ss;
      ss << "Operator " << n.getKind()
         << " expects two bags of the same type. Found types '" << bagType
         << "' and '" << secondBagType << "'.";
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
  }
  return bagType;
}

bool BinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
{
  // only UNION_DISJOINT has a const rule in kinds.
  // Other binary operators do not have const rules in kinds
  Assert(n.getKind() == kind::UNION_DISJOINT);
  return NormalForm::isConstant(n);
}

TypeNode SubBagTypeRule::computeType(NodeManager* nodeManager,
                                     TNode n,
                                     bool check)
{
  Assert(n.getKind() == kind::SUBBAG);
  TypeNode bagType = n[0].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      throw TypeCheckingExceptionPrivate(n, "SUBBAG operating on non-bag");
    }
    TypeNode secondBagType = n[1].getType(check);
    if (secondBagType != bagType)
    {
      if (!bagType.isComparableTo(secondBagType))
      {
        throw TypeCheckingExceptionPrivate(
            n, "SUBBAG operating on bags of different types");
      }
    }
  }
  return nodeManager->booleanType();
}

TypeNode CountTypeRule::computeType(NodeManager* nodeManager,
                                    TNode n,
                                    bool check)
{
  Assert(n.getKind() == kind::BAG_COUNT);
  TypeNode bagType = n[1].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      throw TypeCheckingExceptionPrivate(
          n, "checking for membership in a non-bag");
    }
    TypeNode elementType = n[0].getType(check);
    // e.g. (count 1 (mkBag (mkBag_op Real) 1.0 3))) is 3 whereas
    // (count 1.0 (mkBag (mkBag_op Int) 1 3))) throws a typing error
    if (!elementType.isSubtypeOf(bagType.getBagElementType()))
    {
      std::stringstream ss;
      ss << "member operating on bags of different types:\n"
         << "child type:  " << elementType << "\n"
         << "not subtype: " << bagType.getBagElementType() << "\n"
         << "in term : " << n;
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
  }
  return nodeManager->integerType();
}

TypeNode DuplicateRemovalTypeRule::computeType(NodeManager* nodeManager,
                                               TNode n,
                                               bool check)
{
  Assert(n.getKind() == kind::DUPLICATE_REMOVAL);
  TypeNode bagType = n[0].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      std::stringstream ss;
      ss << "Applying DUPLICATE_REMOVAL on a non-bag argument in term " << n;
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
  }
  return bagType;
}

TypeNode MkBagTypeRule::computeType(NodeManager* nm, TNode n, bool check)
{
  Assert(n.getKind() == kind::MK_BAG && n.hasOperator()
         && n.getOperator().getKind() == kind::MK_BAG_OP);
  MakeBagOp op = n.getOperator().getConst<MakeBagOp>();
  TypeNode expectedElementType = op.getType();
  if (check)
  {
    if (n.getNumChildren() != 2)
    {
      std::stringstream ss;
      ss << "operands in term " << n << " are " << n.getNumChildren()
         << ", but MK_BAG expects 2 operands.";
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
    TypeNode type1 = n[1].getType(check);
    if (!type1.isInteger())
    {
      std::stringstream ss;
      ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1;
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }

    TypeNode actualElementType = n[0].getType(check);
    // the type of the element should be a subtype of the type of the operator
    // e.g. (mkBag (mkBag_op Real) 1 1) where 1 is an Int
    if (!actualElementType.isSubtypeOf(expectedElementType))
    {
      std::stringstream ss;
      ss << "The type '" << actualElementType
         << "' of the element is not a subtype of '" << expectedElementType
         << "' in term : " << n;
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
  }

  return nm->mkBagType(expectedElementType);
}

bool MkBagTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
{
  Assert(n.getKind() == kind::MK_BAG);
  // for a bag to be a constant, both the element and its multiplicity should
  // be constants, and the multiplicity should be > 0.
  return n[0].isConst() && n[1].isConst()
         && n[1].getConst<Rational>().sgn() == 1;
}

TypeNode IsSingletonTypeRule::computeType(NodeManager* nodeManager,
                                          TNode n,
                                          bool check)
{
  Assert(n.getKind() == kind::BAG_IS_SINGLETON);
  TypeNode bagType = n[0].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      throw TypeCheckingExceptionPrivate(
          n, "BAG_IS_SINGLETON operator expects a bag, a non-bag is found");
    }
  }
  return nodeManager->booleanType();
}

TypeNode EmptyBagTypeRule::computeType(NodeManager* nodeManager,
                                       TNode n,
                                       bool check)
{
  Assert(n.getKind() == kind::EMPTYBAG);
  EmptyBag emptyBag = n.getConst<EmptyBag>();
  return emptyBag.getType();
}

TypeNode CardTypeRule::computeType(NodeManager* nodeManager,
                                   TNode n,
                                   bool check)
{
  Assert(n.getKind() == kind::BAG_CARD);
  TypeNode bagType = n[0].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      throw TypeCheckingExceptionPrivate(
          n, "cardinality operates on a bag, non-bag object found");
    }
  }
  return nodeManager->integerType();
}

TypeNode ChooseTypeRule::computeType(NodeManager* nodeManager,
                                     TNode n,
                                     bool check)
{
  Assert(n.getKind() == kind::BAG_CHOOSE);
  TypeNode bagType = n[0].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      throw TypeCheckingExceptionPrivate(
          n, "CHOOSE operator expects a bag, a non-bag is found");
    }
  }
  return bagType.getBagElementType();
}

TypeNode FromSetTypeRule::computeType(NodeManager* nodeManager,
                                      TNode n,
                                      bool check)
{
  Assert(n.getKind() == kind::BAG_FROM_SET);
  TypeNode setType = n[0].getType(check);
  if (check)
  {
    if (!setType.isSet())
    {
      throw TypeCheckingExceptionPrivate(
          n, "bag.from_set operator expects a set, a non-set is found");
    }
  }
  TypeNode elementType = setType.getSetElementType();
  TypeNode bagType = nodeManager->mkBagType(elementType);
  return bagType;
}

TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager,
                                    TNode n,
                                    bool check)
{
  Assert(n.getKind() == kind::BAG_TO_SET);
  TypeNode bagType = n[0].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      throw TypeCheckingExceptionPrivate(
          n, "bag.to_set operator expects a bag, a non-bag is found");
    }
  }
  TypeNode elementType = bagType.getBagElementType();
  TypeNode setType = nodeManager->mkSetType(elementType);
  return setType;
}

TypeNode BagMapTypeRule::computeType(NodeManager* nodeManager,
                                     TNode n,
                                     bool check)
{
  Assert(n.getKind() == kind::BAG_MAP);
  TypeNode functionType = n[0].getType(check);
  TypeNode bagType = n[1].getType(check);
  if (check)
  {
    if (!bagType.isBag())
    {
      throw TypeCheckingExceptionPrivate(
          n,
          "bag.map operator expects a bag in the second argument, "
          "a non-bag is found");
    }

    TypeNode elementType = bagType.getBagElementType();

    if (!(functionType.isFunction()))
    {
      std::stringstream ss;
      ss << "Operator " << n.getKind() << " expects a function of type  (-> "
         << elementType << " *) as a first argument. "
         << "Found a term of type '" << functionType << "'.";
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
    std::vector<TypeNode> argTypes = functionType.getArgTypes();
    if (!(argTypes.size() == 1 && argTypes[0] == elementType))
    {
      std::stringstream ss;
      ss << "Operator " << n.getKind() << " expects a function of type  (-> "
         << elementType << " *). "
         << "Found a function of type '" << functionType << "'.";
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
  }
  TypeNode rangeType = n[0].getType().getRangeType();
  TypeNode retType = nodeManager->mkBagType(rangeType);
  return retType;
}

Cardinality BagsProperties::computeCardinality(TypeNode type)
{
  return Cardinality::INTEGERS;
}

bool BagsProperties::isWellFounded(TypeNode type)
{
  return type[0].isWellFounded();
}

Node BagsProperties::mkGroundTerm(TypeNode type)
{
  Assert(type.isBag());
  return NodeManager::currentNM()->mkConst(EmptyBag(type));
}
}  // namespace bags
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mudathir Mohamed, Aina Niemetz
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		* Bags theory type rules.
14		*/
15
16		#include "theory/bags/theory_bags_type_rules.h"
17
18		#include <sstream>
19
20		#include "base/check.h"
21		#include "expr/emptybag.h"
22		#include "theory/bags/make_bag_op.h"
23		#include "theory/bags/normal_form.h"
24		#include "util/cardinality.h"
25		#include "util/rational.h"
26
27		namespace cvc5 {
28		namespace theory {
29		namespace bags {
30
31	318	TypeNode BinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
32		TNode n,
33		bool check)
34		{
35	318	Assert(n.getKind() == kind::UNION_MAX \|\| n.getKind() == kind::UNION_DISJOINT
36		\|\| n.getKind() == kind::INTERSECTION_MIN
37		\|\| n.getKind() == kind::DIFFERENCE_SUBTRACT
38		\|\| n.getKind() == kind::DIFFERENCE_REMOVE);
39	318	TypeNode bagType = n[0].getType(check);
40	318	if (check)
41		{
42	318	if (!bagType.isBag())
43		{
44		throw TypeCheckingExceptionPrivate(
45		n, "operator expects a bag, first argument is not");
46		}
47	636	TypeNode secondBagType = n[1].getType(check);
48	318	if (secondBagType != bagType)
49		{
50		std::stringstream ss;
51		ss << "Operator " << n.getKind()
52		<< " expects two bags of the same type. Found types '" << bagType
53		<< "' and '" << secondBagType << "'.";
54		throw TypeCheckingExceptionPrivate(n, ss.str());
55		}
56		}
57	318	return bagType;
58		}
59
60	121	bool BinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
61		{
62		// only UNION_DISJOINT has a const rule in kinds.
63		// Other binary operators do not have const rules in kinds
64	121	Assert(n.getKind() == kind::UNION_DISJOINT);
65	121	return NormalForm::isConstant(n);
66		}
67
68	10	TypeNode SubBagTypeRule::computeType(NodeManager* nodeManager,
69		TNode n,
70		bool check)
71		{
72	10	Assert(n.getKind() == kind::SUBBAG);
73	20	TypeNode bagType = n[0].getType(check);
74	10	if (check)
75		{
76	10	if (!bagType.isBag())
77		{
78		throw TypeCheckingExceptionPrivate(n, "SUBBAG operating on non-bag");
79		}
80	20	TypeNode secondBagType = n[1].getType(check);
81	10	if (secondBagType != bagType)
82		{
83		if (!bagType.isComparableTo(secondBagType))
84		{
85		throw TypeCheckingExceptionPrivate(
86		n, "SUBBAG operating on bags of different types");
87		}
88		}
89		}
90	20	return nodeManager->booleanType();
91		}
92
93	515	TypeNode CountTypeRule::computeType(NodeManager* nodeManager,
94		TNode n,
95		bool check)
96		{
97	515	Assert(n.getKind() == kind::BAG_COUNT);
98	1030	TypeNode bagType = n[1].getType(check);
99	515	if (check)
100		{
101	515	if (!bagType.isBag())
102		{
103		throw TypeCheckingExceptionPrivate(
104		n, "checking for membership in a non-bag");
105		}
106	1030	TypeNode elementType = n[0].getType(check);
107		// e.g. (count 1 (mkBag (mkBag_op Real) 1.0 3))) is 3 whereas
108		// (count 1.0 (mkBag (mkBag_op Int) 1 3))) throws a typing error
109	515	if (!elementType.isSubtypeOf(bagType.getBagElementType()))
110		{
111	4	std::stringstream ss;
112		ss << "member operating on bags of different types:\n"
113	2	<< "child type: " << elementType << "\n"
114	4	<< "not subtype: " << bagType.getBagElementType() << "\n"
115	2	<< "in term : " << n;
116	2	throw TypeCheckingExceptionPrivate(n, ss.str());
117		}
118		}
119	1026	return nodeManager->integerType();
120		}
121
122	16	TypeNode DuplicateRemovalTypeRule::computeType(NodeManager* nodeManager,
123		TNode n,
124		bool check)
125		{
126	16	Assert(n.getKind() == kind::DUPLICATE_REMOVAL);
127	16	TypeNode bagType = n[0].getType(check);
128	16	if (check)
129		{
130	16	if (!bagType.isBag())
131		{
132		std::stringstream ss;
133		ss << "Applying DUPLICATE_REMOVAL on a non-bag argument in term " << n;
134		throw TypeCheckingExceptionPrivate(n, ss.str());
135		}
136		}
137	16	return bagType;
138		}
139
140	273	TypeNode MkBagTypeRule::computeType(NodeManager* nm, TNode n, bool check)
141		{
142	273	Assert(n.getKind() == kind::MK_BAG && n.hasOperator()
143		&& n.getOperator().getKind() == kind::MK_BAG_OP);
144	546	MakeBagOp op = n.getOperator().getConst<MakeBagOp>();
145	546	TypeNode expectedElementType = op.getType();
146	273	if (check)
147		{
148	273	if (n.getNumChildren() != 2)
149		{
150		std::stringstream ss;
151		ss << "operands in term " << n << " are " << n.getNumChildren()
152		<< ", but MK_BAG expects 2 operands.";
153		throw TypeCheckingExceptionPrivate(n, ss.str());
154		}
155	546	TypeNode type1 = n[1].getType(check);
156	273	if (!type1.isInteger())
157		{
158		std::stringstream ss;
159		ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1;
160		throw TypeCheckingExceptionPrivate(n, ss.str());
161		}
162
163	546	TypeNode actualElementType = n[0].getType(check);
164		// the type of the element should be a subtype of the type of the operator
165		// e.g. (mkBag (mkBag_op Real) 1 1) where 1 is an Int
166	273	if (!actualElementType.isSubtypeOf(expectedElementType))
167		{
168		std::stringstream ss;
169		ss << "The type '" << actualElementType
170		<< "' of the element is not a subtype of '" << expectedElementType
171		<< "' in term : " << n;
172		throw TypeCheckingExceptionPrivate(n, ss.str());
173		}
174		}
175
176	546	return nm->mkBagType(expectedElementType);
177		}
178
179	220	bool MkBagTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
180		{
181	220	Assert(n.getKind() == kind::MK_BAG);
182		// for a bag to be a constant, both the element and its multiplicity should
183		// be constants, and the multiplicity should be > 0.
184	797	return n[0].isConst() && n[1].isConst()
185	1010	&& n[1].getConst<Rational>().sgn() == 1;
186		}
187
188	10	TypeNode IsSingletonTypeRule::computeType(NodeManager* nodeManager,
189		TNode n,
190		bool check)
191		{
192	10	Assert(n.getKind() == kind::BAG_IS_SINGLETON);
193	20	TypeNode bagType = n[0].getType(check);
194	10	if (check)
195		{
196	10	if (!bagType.isBag())
197		{
198		throw TypeCheckingExceptionPrivate(
199		n, "BAG_IS_SINGLETON operator expects a bag, a non-bag is found");
200		}
201		}
202	20	return nodeManager->booleanType();
203		}
204
205	1620	TypeNode EmptyBagTypeRule::computeType(NodeManager* nodeManager,
206		TNode n,
207		bool check)
208		{
209	1620	Assert(n.getKind() == kind::EMPTYBAG);
210	3240	EmptyBag emptyBag = n.getConst<EmptyBag>();
211	3240	return emptyBag.getType();
212		}
213
214	14	TypeNode CardTypeRule::computeType(NodeManager* nodeManager,
215		TNode n,
216		bool check)
217		{
218	14	Assert(n.getKind() == kind::BAG_CARD);
219	28	TypeNode bagType = n[0].getType(check);
220	14	if (check)
221		{
222	14	if (!bagType.isBag())
223		{
224		throw TypeCheckingExceptionPrivate(
225		n, "cardinality operates on a bag, non-bag object found");
226		}
227		}
228	28	return nodeManager->integerType();
229		}
230
231	8	TypeNode ChooseTypeRule::computeType(NodeManager* nodeManager,
232		TNode n,
233		bool check)
234		{
235	8	Assert(n.getKind() == kind::BAG_CHOOSE);
236	16	TypeNode bagType = n[0].getType(check);
237	8	if (check)
238		{
239	8	if (!bagType.isBag())
240		{
241		throw TypeCheckingExceptionPrivate(
242		n, "CHOOSE operator expects a bag, a non-bag is found");
243		}
244		}
245	16	return bagType.getBagElementType();
246		}
247
248	10	TypeNode FromSetTypeRule::computeType(NodeManager* nodeManager,
249		TNode n,
250		bool check)
251		{
252	10	Assert(n.getKind() == kind::BAG_FROM_SET);
253	20	TypeNode setType = n[0].getType(check);
254	10	if (check)
255		{
256	10	if (!setType.isSet())
257		{
258		throw TypeCheckingExceptionPrivate(
259		n, "bag.from_set operator expects a set, a non-set is found");
260		}
261		}
262	20	TypeNode elementType = setType.getSetElementType();
263	10	TypeNode bagType = nodeManager->mkBagType(elementType);
264	20	return bagType;
265		}
266
267	10	TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager,
268		TNode n,
269		bool check)
270		{
271	10	Assert(n.getKind() == kind::BAG_TO_SET);
272	20	TypeNode bagType = n[0].getType(check);
273	10	if (check)
274		{
275	10	if (!bagType.isBag())
276		{
277		throw TypeCheckingExceptionPrivate(
278		n, "bag.to_set operator expects a bag, a non-bag is found");
279		}
280		}
281	20	TypeNode elementType = bagType.getBagElementType();
282	10	TypeNode setType = nodeManager->mkSetType(elementType);
283	20	return setType;
284		}
285
286	12	TypeNode BagMapTypeRule::computeType(NodeManager* nodeManager,
287		TNode n,
288		bool check)
289		{
290	12	Assert(n.getKind() == kind::BAG_MAP);
291	24	TypeNode functionType = n[0].getType(check);
292	24	TypeNode bagType = n[1].getType(check);
293	12	if (check)
294		{
295	12	if (!bagType.isBag())
296		{
297		throw TypeCheckingExceptionPrivate(
298		n,
299		"bag.map operator expects a bag in the second argument, "
300	2	"a non-bag is found");
301		}
302
303	20	TypeNode elementType = bagType.getBagElementType();
304
305	10	if (!(functionType.isFunction()))
306		{
307		std::stringstream ss;
308		ss << "Operator " << n.getKind() << " expects a function of type (-> "
309		<< elementType << " *) as a first argument. "
310		<< "Found a term of type '" << functionType << "'.";
311		throw TypeCheckingExceptionPrivate(n, ss.str());
312		}
313	20	std::vector<TypeNode> argTypes = functionType.getArgTypes();
314	10	if (!(argTypes.size() == 1 && argTypes[0] == elementType))
315		{
316	4	std::stringstream ss;
317	2	ss << "Operator " << n.getKind() << " expects a function of type (-> "
318	2	<< elementType << " *). "
319	2	<< "Found a function of type '" << functionType << "'.";
320	2	throw TypeCheckingExceptionPrivate(n, ss.str());
321		}
322		}
323	16	TypeNode rangeType = n[0].getType().getRangeType();
324	8	TypeNode retType = nodeManager->mkBagType(rangeType);
325	16	return retType;
326		}
327
328		Cardinality BagsProperties::computeCardinality(TypeNode type)
329		{
330		return Cardinality::INTEGERS;
331		}
332
333		bool BagsProperties::isWellFounded(TypeNode type)
334		{
335		return type[0].isWellFounded();
336		}
337
338		Node BagsProperties::mkGroundTerm(TypeNode type)
339		{
340		Assert(type.isBag());
341		return NodeManager::currentNM()->mkConst(EmptyBag(type));
342		}
343		} // namespace bags
344		} // namespace theory
345	29577	} // namespace cvc5