Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv_type_rules.h	Lines:	0	6	0.0 %
Date:	2021-05-22	Branches:	0	20	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andrew Reynolds, Dejan Jovanovic
 *
 * 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 "cvc5_private.h"

#ifndef CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
#define CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H

#include "expr/node.h"

namespace cvc5 {

class TypeNode;

namespace theory {
namespace bv {

/* -------------------------------------------------------------------------- */

class CardinalityComputer
{
 public:
  static Cardinality computeCardinality(TypeNode type);
};

/* -------------------------------------------------------------------------- */

class BitVectorConstantTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

/* -------------------------------------------------------------------------- */

class BitVectorFixedWidthTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

/* -------------------------------------------------------------------------- */

class BitVectorPredicateTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorUnaryPredicateTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorBVPredTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

/* -------------------------------------------------------------------------- */
/* non-parameterized operator kinds                                           */
/* -------------------------------------------------------------------------- */

class BitVectorConcatTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorToBVTypeRule
{
 public:
  inline static TypeNode computeType(NodeManager* nodeManager,
                                     TNode n,
                                     bool check)
  {
    for (const auto& child : n)
    {
      TypeNode t = child.getType(check);
      if (!t.isBoolean())
      {
        throw TypeCheckingExceptionPrivate(n, "expecting Boolean terms");
      }
    }
    return nodeManager->mkBitVectorType(n.getNumChildren());
  }
};

class BitVectorITETypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

/* -------------------------------------------------------------------------- */
/* parameterized operator kinds                                               */
/* -------------------------------------------------------------------------- */

class BitVectorBitOfTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorExtractTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorRepeatTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorExtendTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class IntToBitVectorOpTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorConversionTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

/* -------------------------------------------------------------------------- */
/* internal                                                                   */
/* -------------------------------------------------------------------------- */

class BitVectorEagerAtomTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorAckermanizationUdivTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

class BitVectorAckermanizationUremTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};

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

#endif /* CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Andrew Reynolds, Dejan Jovanovic
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 "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
19		#define CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
20
21		#include "expr/node.h"
22
23		namespace cvc5 {
24
25		class TypeNode;
26
27		namespace theory {
28		namespace bv {
29
30		/* -------------------------------------------------------------------------- */
31
32		class CardinalityComputer
33		{
34		public:
35		static Cardinality computeCardinality(TypeNode type);
36		};
37
38		/* -------------------------------------------------------------------------- */
39
40		class BitVectorConstantTypeRule
41		{
42		public:
43		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
44		};
45
46		/* -------------------------------------------------------------------------- */
47
48		class BitVectorFixedWidthTypeRule
49		{
50		public:
51		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
52		};
53
54		/* -------------------------------------------------------------------------- */
55
56		class BitVectorPredicateTypeRule
57		{
58		public:
59		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
60		};
61
62		class BitVectorUnaryPredicateTypeRule
63		{
64		public:
65		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
66		};
67
68		class BitVectorBVPredTypeRule
69		{
70		public:
71		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
72		};
73
74		/* -------------------------------------------------------------------------- */
75		/* non-parameterized operator kinds */
76		/* -------------------------------------------------------------------------- */
77
78		class BitVectorConcatTypeRule
79		{
80		public:
81		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
82		};
83
84		class BitVectorToBVTypeRule
85		{
86		public:
87		inline static TypeNode computeType(NodeManager* nodeManager,
88		TNode n,
89		bool check)
90		{
91		for (const auto& child : n)
92		{
93		TypeNode t = child.getType(check);
94		if (!t.isBoolean())
95		{
96		throw TypeCheckingExceptionPrivate(n, "expecting Boolean terms");
97		}
98		}
99		return nodeManager->mkBitVectorType(n.getNumChildren());
100		}
101		};
102
103		class BitVectorITETypeRule
104		{
105		public:
106		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
107		};
108
109		/* -------------------------------------------------------------------------- */
110		/* parameterized operator kinds */
111		/* -------------------------------------------------------------------------- */
112
113		class BitVectorBitOfTypeRule
114		{
115		public:
116		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
117		};
118
119		class BitVectorExtractTypeRule
120		{
121		public:
122		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
123		};
124
125		class BitVectorRepeatTypeRule
126		{
127		public:
128		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
129		};
130
131		class BitVectorExtendTypeRule
132		{
133		public:
134		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
135		};
136
137		class IntToBitVectorOpTypeRule
138		{
139		public:
140		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
141		};
142
143		class BitVectorConversionTypeRule
144		{
145		public:
146		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
147		};
148
149		/* -------------------------------------------------------------------------- */
150		/* internal */
151		/* -------------------------------------------------------------------------- */
152
153		class BitVectorEagerAtomTypeRule
154		{
155		public:
156		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
157		};
158
159		class BitVectorAckermanizationUdivTypeRule
160		{
161		public:
162		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
163		};
164
165		class BitVectorAckermanizationUremTypeRule
166		{
167		public:
168		static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
169		};
170
171		} // namespace bv
172		} // namespace theory
173		} // namespace cvc5
174
175		#endif /* CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H */