Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bags/theory_bags_type_rules.cpp	Lines:	92	127	72.4 %
Date:	2021-05-22	Branches:	179	684	26.2 %


/******************************************************************************
 * 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 "theory/bags/normal_form.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;
}

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