CBMC
mathematical_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Mathematical types
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Maria Svorenova, maria.svorenova@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_UTIL_MATHEMATICAL_TYPES_H
14 #define CPROVER_UTIL_MATHEMATICAL_TYPES_H
15 
16 #include "expr_cast.h" // IWYU pragma: keep
17 #include "invariant.h"
18 #include "type.h"
19 
21 class integer_typet : public typet
22 {
23 public:
24  integer_typet() : typet(ID_integer)
25  {
26  }
27 };
28 
30 class natural_typet : public typet
31 {
32 public:
33  natural_typet() : typet(ID_natural)
34  {
35  }
36 };
37 
39 class rational_typet : public typet
40 {
41 public:
42  rational_typet() : typet(ID_rational)
43  {
44  }
45 };
46 
48 class real_typet : public typet
49 {
50 public:
51  real_typet() : typet(ID_real)
52  {
53  }
54 };
55 
59 {
60 public:
61  // the domain of the function is composed of zero, one, or
62  // many variables, given by their type
63  using domaint = std::vector<typet>;
64 
65  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
67  ID_mathematical_function,
68  {type_with_subtypest(irep_idt(), _domain), _codomain})
69  {
70  }
71 
73  {
75  }
76 
77  const domaint &domain() const
78  {
79  return (const domaint &)to_type_with_subtypes(subtypes()[0]).subtypes();
80  }
81 
82  void add_variable(const typet &_type)
83  {
84  domain().push_back(_type);
85  }
86 
90  {
91  return subtypes()[1];
92  }
93 
95  const typet &codomain() const
96  {
97  return subtypes()[1];
98  }
99 };
100 
104 template <>
106 {
107  return type.id() == ID_mathematical_function;
108 }
109 
118 inline const mathematical_function_typet &
120 {
122  return static_cast<const mathematical_function_typet &>(type);
123 }
124 
127 {
129  return static_cast<mathematical_function_typet &>(type);
130 }
131 
132 bool is_number(const typet &type);
133 
134 #endif // CPROVER_UTIL_MATHEMATICAL_TYPES_H
Unbounded, signed integers (mathematical integers, not bitvectors)
const irep_idt & id() const
Definition: irep.h:388
A type for mathematical functions (do not confuse with functions/methods in code)
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
void add_variable(const typet &_type)
mathematical_function_typet(const domaint &_domain, const typet &_codomain)
std::vector< typet > domaint
const typet & codomain() const
Return the codomain, i.e., the set of values that the function maps to (the "target").
const domaint & domain() const
Natural numbers including zero (mathematical integers, not bitvectors)
Unbounded, signed rational numbers.
Unbounded, signed real numbers.
Type with multiple subtypes.
Definition: type.h:222
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
Definition: type.h:226
subtypest & subtypes()
Definition: type.h:237
The type of an expression, extends irept.
Definition: type.h:29
Templated functions to cast to specific exprt-derived classes.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
bool can_cast_type< mathematical_function_typet >(const typet &type)
Check whether a reference to a typet is a mathematical_function_typet.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Defines typet, type_with_subtypet and type_with_subtypest.
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:252
dstringt irep_idt