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