Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv_type_rules.cpp	Lines:	99	136	72.8 %
Date:	2021-08-01	Branches:	145	490	29.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Dejan Jovanovic, Christopher L. Conway
 *
 * 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.
 * ****************************************************************************
 *
 * Bitvector theory typing rules.
 */

#include "theory/bv/theory_bv_type_rules.h"

#include <algorithm>

#include "expr/type_node.h"
#include "util/bitvector.h"
#include "util/cardinality.h"
#include "util/integer.h"

namespace cvc5 {
namespace theory {
namespace bv {

Cardinality CardinalityComputer::computeCardinality(TypeNode type)
{
  Assert(type.getKind() == kind::BITVECTOR_TYPE);

  uint32_t size = type.getConst<BitVectorSize>();
  if (size == 0)
  {
    return 0;
  }
  return Integer(2).pow(size);
}

TypeNode BitVectorConstantTypeRule::computeType(NodeManager* nodeManager,
                                                TNode n,
                                                bool check)
{
  if (check)
  {
    if (n.getConst<BitVector>().getSize() == 0)
    {
      throw TypeCheckingExceptionPrivate(n, "constant of size 0");
    }
  }
  return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
}

TypeNode BitVectorFixedWidthTypeRule::computeType(NodeManager* nodeManager,
                                                  TNode n,
                                                  bool check)
{
  TNode::iterator it = n.begin();
  TypeNode t = (*it).getType(check);
  if (check)
  {
    if (!t.isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
    }
    TNode::iterator it_end = n.end();
    for (++it; it != it_end; ++it)
    {
      if ((*it).getType(check) != t)
      {
        throw TypeCheckingExceptionPrivate(
            n, "expecting bit-vector terms of the same width");
      }
    }
  }
  return t;
}

TypeNode BitVectorPredicateTypeRule::computeType(NodeManager* nodeManager,
                                                 TNode n,
                                                 bool check)
{
  if (check)
  {
    TypeNode lhsType = n[0].getType(check);
    if (!lhsType.isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
    }
    TypeNode rhsType = n[1].getType(check);
    if (lhsType != rhsType)
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting bit-vector terms of the same width");
    }
  }
  return nodeManager->booleanType();
}

TypeNode BitVectorUnaryPredicateTypeRule::computeType(NodeManager* nodeManager,
                                                      TNode n,
                                                      bool check)
{
  if (check)
  {
    TypeNode type = n[0].getType(check);
    if (!type.isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
    }
  }
  return nodeManager->booleanType();
}

TypeNode BitVectorBVPredTypeRule::computeType(NodeManager* nodeManager,
                                              TNode n,
                                              bool check)
{
  if (check)
  {
    TypeNode lhs = n[0].getType(check);
    TypeNode rhs = n[1].getType(check);
    if (!lhs.isBitVector() || lhs != rhs)
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting bit-vector terms of the same width");
    }
  }
  return nodeManager->mkBitVectorType(1);
}

TypeNode BitVectorConcatTypeRule::computeType(NodeManager* nodeManager,
                                              TNode n,
                                              bool check)
{
  uint32_t size = 0;
  for (const auto& child : n)
  {
    TypeNode t = child.getType(check);
    // NOTE: We're throwing a type-checking exception here even
    // when check is false, bc if we don't check that the arguments
    // are bit-vectors the result type will be inaccurate
    if (!t.isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
    }
    size += t.getBitVectorSize();
  }
  return nodeManager->mkBitVectorType(size);
}

TypeNode BitVectorITETypeRule::computeType(NodeManager* nodeManager,
                                           TNode n,
                                           bool check)
{
  Assert(n.getNumChildren() == 3);
  TypeNode thenpart = n[1].getType(check);
  if (check)
  {
    TypeNode cond = n[0].getType(check);
    if (cond != nodeManager->mkBitVectorType(1))
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting condition to be bit-vector term size 1");
    }
    TypeNode elsepart = n[2].getType(check);
    if (thenpart != elsepart)
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting then and else parts to have same type");
    }
  }
  return thenpart;
}

TypeNode BitVectorBitOfTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
{
  if (check)
  {
    BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
    TypeNode t = n[0].getType(check);

    if (!t.isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
    }
    if (info.d_bitIndex >= t.getBitVectorSize())
    {
      throw TypeCheckingExceptionPrivate(
          n, "extract index is larger than the bitvector size");
    }
  }
  return nodeManager->booleanType();
}

TypeNode BitVectorExtractTypeRule::computeType(NodeManager* nodeManager,
                                               TNode n,
                                               bool check)
{
  BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();

  // NOTE: We're throwing a type-checking exception here even
  // if check is false, bc if we allow high < low the resulting
  // type will be illegal
  if (extractInfo.d_high < extractInfo.d_low)
  {
    throw TypeCheckingExceptionPrivate(
        n, "high extract index is smaller than the low extract index");
  }

  if (check)
  {
    TypeNode t = n[0].getType(check);
    if (!t.isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
    }
    if (extractInfo.d_high >= t.getBitVectorSize())
    {
      throw TypeCheckingExceptionPrivate(
          n, "high extract index is bigger than the size of the bit-vector");
    }
  }
  return nodeManager->mkBitVectorType(extractInfo.d_high - extractInfo.d_low
                                      + 1);
}

TypeNode BitVectorRepeatTypeRule::computeType(NodeManager* nodeManager,
                                              TNode n,
                                              bool check)
{
  TypeNode t = n[0].getType(check);
  // NOTE: We're throwing a type-checking exception here even
  // when check is false, bc if the argument isn't a bit-vector
  // the result type will be inaccurate
  if (!t.isBitVector())
  {
    throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
  }
  uint32_t repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
  if (repeatAmount == 0)
  {
    throw TypeCheckingExceptionPrivate(n, "expecting number of repeats > 0");
  }
  return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
}

TypeNode BitVectorExtendTypeRule::computeType(NodeManager* nodeManager,
                                              TNode n,
                                              bool check)
{
  TypeNode t = n[0].getType(check);
  // NOTE: We're throwing a type-checking exception here even
  // when check is false, bc if the argument isn't a bit-vector
  // the result type will be inaccurate
  if (!t.isBitVector())
  {
    throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
  }
  uint32_t extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND
                              ? n.getOperator().getConst<BitVectorSignExtend>()
                              : n.getOperator().getConst<BitVectorZeroExtend>();
  return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
}

TypeNode IntToBitVectorOpTypeRule::computeType(NodeManager* nodeManager,
                                               TNode n,
                                               bool check)
{
  Assert(n.getKind() == kind::INT_TO_BITVECTOR_OP);
  size_t bvSize = n.getConst<IntToBitVector>();
  if (bvSize == 0)
  {
    throw TypeCheckingExceptionPrivate(n, "expecting bit-width > 0");
  }
  return nodeManager->mkFunctionType(nodeManager->integerType(),
                                     nodeManager->mkBitVectorType(bvSize));
}

TypeNode BitVectorConversionTypeRule::computeType(NodeManager* nodeManager,
                                                  TNode n,
                                                  bool check)
{
  if (n.getKind() == kind::BITVECTOR_TO_NAT)
  {
    if (check && !n[0].getType(check).isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
    }
    return nodeManager->integerType();
  }

  Assert(n.getKind() == kind::INT_TO_BITVECTOR);
  size_t bvSize = n.getOperator().getConst<IntToBitVector>();
  if (check && !n[0].getType(check).isInteger())
  {
    throw TypeCheckingExceptionPrivate(n, "expecting integer term");
  }
  return nodeManager->mkBitVectorType(bvSize);
}

TypeNode BitVectorEagerAtomTypeRule::computeType(NodeManager* nodeManager,
                                                 TNode n,
                                                 bool check)
{
  if (check)
  {
    TypeNode lhsType = n[0].getType(check);
    if (!lhsType.isBoolean())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting boolean term");
    }
  }
  return nodeManager->booleanType();
}

TypeNode BitVectorAckermanizationUdivTypeRule::computeType(
    NodeManager* nodeManager, TNode n, bool check)
{
  TypeNode lhsType = n[0].getType(check);
  if (check)
  {
    if (!lhsType.isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
    }
  }
  return lhsType;
}

TypeNode BitVectorAckermanizationUremTypeRule::computeType(
    NodeManager* nodeManager, TNode n, bool check)
{
  TypeNode lhsType = n[0].getType(check);
  if (check)
  {
    if (!lhsType.isBitVector())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
    }
  }
  return lhsType;
}

}  // namespace bv
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Dejan Jovanovic, Christopher L. Conway
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		* Bitvector theory typing rules.
14		*/
15
16		#include "theory/bv/theory_bv_type_rules.h"
17
18		#include <algorithm>
19
20		#include "expr/type_node.h"
21		#include "util/bitvector.h"
22		#include "util/cardinality.h"
23		#include "util/integer.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace bv {
28
29	2550	Cardinality CardinalityComputer::computeCardinality(TypeNode type)
30		{
31	2550	Assert(type.getKind() == kind::BITVECTOR_TYPE);
32
33	2550	uint32_t size = type.getConst<BitVectorSize>();
34	2550	if (size == 0)
35		{
36	2	return 0;
37		}
38	2548	return Integer(2).pow(size);
39		}
40
41	69563	TypeNode BitVectorConstantTypeRule::computeType(NodeManager* nodeManager,
42		TNode n,
43		bool check)
44		{
45	69563	if (check)
46		{
47	55357	if (n.getConst<BitVector>().getSize() == 0)
48		{
49		throw TypeCheckingExceptionPrivate(n, "constant of size 0");
50		}
51		}
52	69563	return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
53		}
54
55	723486	TypeNode BitVectorFixedWidthTypeRule::computeType(NodeManager* nodeManager,
56		TNode n,
57		bool check)
58		{
59	723486	TNode::iterator it = n.begin();
60	723486	TypeNode t = (*it).getType(check);
61	723486	if (check)
62		{
63	723486	if (!t.isBitVector())
64		{
65		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
66		}
67	723486	TNode::iterator it_end = n.end();
68	1896414	for (++it; it != it_end; ++it)
69		{
70	1172928	if ((*it).getType(check) != t)
71		{
72		throw TypeCheckingExceptionPrivate(
73		n, "expecting bit-vector terms of the same width");
74		}
75		}
76		}
77	723486	return t;
78		}
79
80	86930	TypeNode BitVectorPredicateTypeRule::computeType(NodeManager* nodeManager,
81		TNode n,
82		bool check)
83		{
84	86930	if (check)
85		{
86	173860	TypeNode lhsType = n[0].getType(check);
87	86930	if (!lhsType.isBitVector())
88		{
89		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
90		}
91	173860	TypeNode rhsType = n[1].getType(check);
92	86930	if (lhsType != rhsType)
93		{
94		throw TypeCheckingExceptionPrivate(
95		n, "expecting bit-vector terms of the same width");
96		}
97		}
98	86930	return nodeManager->booleanType();
99		}
100
101		TypeNode BitVectorUnaryPredicateTypeRule::computeType(NodeManager* nodeManager,
102		TNode n,
103		bool check)
104		{
105		if (check)
106		{
107		TypeNode type = n[0].getType(check);
108		if (!type.isBitVector())
109		{
110		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
111		}
112		}
113		return nodeManager->booleanType();
114		}
115
116	166535	TypeNode BitVectorBVPredTypeRule::computeType(NodeManager* nodeManager,
117		TNode n,
118		bool check)
119		{
120	166535	if (check)
121		{
122	333070	TypeNode lhs = n[0].getType(check);
123	333070	TypeNode rhs = n[1].getType(check);
124	166535	if (!lhs.isBitVector() \|\| lhs != rhs)
125		{
126		throw TypeCheckingExceptionPrivate(
127		n, "expecting bit-vector terms of the same width");
128		}
129		}
130	166535	return nodeManager->mkBitVectorType(1);
131		}
132
133	99671	TypeNode BitVectorConcatTypeRule::computeType(NodeManager* nodeManager,
134		TNode n,
135		bool check)
136		{
137	99671	uint32_t size = 0;
138	399659	for (const auto& child : n)
139		{
140	599976	TypeNode t = child.getType(check);
141		// NOTE: We're throwing a type-checking exception here even
142		// when check is false, bc if we don't check that the arguments
143		// are bit-vectors the result type will be inaccurate
144	299988	if (!t.isBitVector())
145		{
146		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
147		}
148	299988	size += t.getBitVectorSize();
149		}
150	99671	return nodeManager->mkBitVectorType(size);
151		}
152
153	12712	TypeNode BitVectorITETypeRule::computeType(NodeManager* nodeManager,
154		TNode n,
155		bool check)
156		{
157	12712	Assert(n.getNumChildren() == 3);
158	12712	TypeNode thenpart = n[1].getType(check);
159	12712	if (check)
160		{
161	25424	TypeNode cond = n[0].getType(check);
162	12712	if (cond != nodeManager->mkBitVectorType(1))
163		{
164		throw TypeCheckingExceptionPrivate(
165		n, "expecting condition to be bit-vector term size 1");
166		}
167	25424	TypeNode elsepart = n[2].getType(check);
168	12712	if (thenpart != elsepart)
169		{
170		throw TypeCheckingExceptionPrivate(
171		n, "expecting then and else parts to have same type");
172		}
173		}
174	12712	return thenpart;
175		}
176
177	193474	TypeNode BitVectorBitOfTypeRule::computeType(NodeManager* nodeManager,
178		TNode n,
179		bool check)
180		{
181	193474	if (check)
182		{
183	193474	BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
184	386948	TypeNode t = n[0].getType(check);
185
186	193474	if (!t.isBitVector())
187		{
188		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
189		}
190	193474	if (info.d_bitIndex >= t.getBitVectorSize())
191		{
192		throw TypeCheckingExceptionPrivate(
193		n, "extract index is larger than the bitvector size");
194		}
195		}
196	193474	return nodeManager->booleanType();
197		}
198
199	107379	TypeNode BitVectorExtractTypeRule::computeType(NodeManager* nodeManager,
200		TNode n,
201		bool check)
202		{
203	107379	BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
204
205		// NOTE: We're throwing a type-checking exception here even
206		// if check is false, bc if we allow high < low the resulting
207		// type will be illegal
208	107379	if (extractInfo.d_high < extractInfo.d_low)
209		{
210		throw TypeCheckingExceptionPrivate(
211		n, "high extract index is smaller than the low extract index");
212		}
213
214	107379	if (check)
215		{
216	214758	TypeNode t = n[0].getType(check);
217	107379	if (!t.isBitVector())
218		{
219		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
220		}
221	107379	if (extractInfo.d_high >= t.getBitVectorSize())
222		{
223		throw TypeCheckingExceptionPrivate(
224		n, "high extract index is bigger than the size of the bit-vector");
225		}
226		}
227	107379	return nodeManager->mkBitVectorType(extractInfo.d_high - extractInfo.d_low
228	107379	+ 1);
229		}
230
231	357	TypeNode BitVectorRepeatTypeRule::computeType(NodeManager* nodeManager,
232		TNode n,
233		bool check)
234		{
235	714	TypeNode t = n[0].getType(check);
236		// NOTE: We're throwing a type-checking exception here even
237		// when check is false, bc if the argument isn't a bit-vector
238		// the result type will be inaccurate
239	357	if (!t.isBitVector())
240		{
241		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
242		}
243	357	uint32_t repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
244	357	if (repeatAmount == 0)
245		{
246	1	throw TypeCheckingExceptionPrivate(n, "expecting number of repeats > 0");
247		}
248	712	return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
249		}
250
251	27570	TypeNode BitVectorExtendTypeRule::computeType(NodeManager* nodeManager,
252		TNode n,
253		bool check)
254		{
255	55140	TypeNode t = n[0].getType(check);
256		// NOTE: We're throwing a type-checking exception here even
257		// when check is false, bc if the argument isn't a bit-vector
258		// the result type will be inaccurate
259	27570	if (!t.isBitVector())
260		{
261		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
262		}
263	27570	uint32_t extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND
264	72994	? n.getOperator().getConst<BitVectorSignExtend>()
265	45424	: n.getOperator().getConst<BitVectorZeroExtend>();
266	55140	return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
267		}
268
269	31	TypeNode IntToBitVectorOpTypeRule::computeType(NodeManager* nodeManager,
270		TNode n,
271		bool check)
272		{
273	31	Assert(n.getKind() == kind::INT_TO_BITVECTOR_OP);
274	31	size_t bvSize = n.getConst<IntToBitVector>();
275	31	if (bvSize == 0)
276		{
277	1	throw TypeCheckingExceptionPrivate(n, "expecting bit-width > 0");
278		}
279	60	return nodeManager->mkFunctionType(nodeManager->integerType(),
280	90	nodeManager->mkBitVectorType(bvSize));
281		}
282
283	1200	TypeNode BitVectorConversionTypeRule::computeType(NodeManager* nodeManager,
284		TNode n,
285		bool check)
286		{
287	1200	if (n.getKind() == kind::BITVECTOR_TO_NAT)
288		{
289	558	if (check && !n[0].getType(check).isBitVector())
290		{
291		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
292		}
293	558	return nodeManager->integerType();
294		}
295
296	642	Assert(n.getKind() == kind::INT_TO_BITVECTOR);
297	642	size_t bvSize = n.getOperator().getConst<IntToBitVector>();
298	642	if (check && !n[0].getType(check).isInteger())
299		{
300		throw TypeCheckingExceptionPrivate(n, "expecting integer term");
301		}
302	642	return nodeManager->mkBitVectorType(bvSize);
303		}
304
305	250	TypeNode BitVectorEagerAtomTypeRule::computeType(NodeManager* nodeManager,
306		TNode n,
307		bool check)
308		{
309	250	if (check)
310		{
311	500	TypeNode lhsType = n[0].getType(check);
312	250	if (!lhsType.isBoolean())
313		{
314		throw TypeCheckingExceptionPrivate(n, "expecting boolean term");
315		}
316		}
317	250	return nodeManager->booleanType();
318		}
319
320		TypeNode BitVectorAckermanizationUdivTypeRule::computeType(
321		NodeManager* nodeManager, TNode n, bool check)
322		{
323		TypeNode lhsType = n[0].getType(check);
324		if (check)
325		{
326		if (!lhsType.isBitVector())
327		{
328		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
329		}
330		}
331		return lhsType;
332		}
333
334		TypeNode BitVectorAckermanizationUremTypeRule::computeType(
335		NodeManager* nodeManager, TNode n, bool check)
336		{
337		TypeNode lhsType = n[0].getType(check);
338		if (check)
339		{
340		if (!lhsType.isBitVector())
341		{
342		throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
343		}
344		}
345		return lhsType;
346		}
347
348		} // namespace bv
349		} // namespace theory
350	29280	} // namespace cvc5