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 
20 class constant_exprt;
21 
23 class integer_typet : public typet
24 {
25 public:
26  integer_typet() : typet(ID_integer)
27  {
28  }
29 
30  constant_exprt zero_expr() const;
31  constant_exprt one_expr() const;
32 };
33 
35 class natural_typet : public typet
36 {
37 public:
38  natural_typet() : typet(ID_natural)
39  {
40  }
41 
42  constant_exprt zero_expr() const;
43  constant_exprt one_expr() const;
44 };
45 
47 class rational_typet : public typet
48 {
49 public:
50  rational_typet() : typet(ID_rational)
51  {
52  }
53 
54  constant_exprt zero_expr() const;
55  constant_exprt one_expr() const;
56 };
57 
59 class real_typet : public typet
60 {
61 public:
62  real_typet() : typet(ID_real)
63  {
64  }
65 
66  constant_exprt zero_expr() const;
67  constant_exprt one_expr() const;
68 };
69 
73 {
74 public:
75  // the domain of the function is composed of zero, one, or
76  // many variables, given by their type
77  using domaint = std::vector<typet>;
78 
79  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
81  ID_mathematical_function,
82  {type_with_subtypest(irep_idt(), _domain), _codomain})
83  {
84  }
85 
87  {
89  }
90 
91  const domaint &domain() const
92  {
93  return (const domaint &)to_type_with_subtypes(subtypes()[0]).subtypes();
94  }
95 
96  void add_variable(const typet &_type)
97  {
98  domain().push_back(_type);
99  }
100 
104  {
105  return subtypes()[1];
106  }
107 
109  const typet &codomain() const
110  {
111  return subtypes()[1];
112  }
113 };
114 
118 template <>
120 {
121  return type.id() == ID_mathematical_function;
122 }
123 
132 inline const mathematical_function_typet &
134 {
136  return static_cast<const mathematical_function_typet &>(type);
137 }
138 
141 {
143  return static_cast<mathematical_function_typet &>(type);
144 }
145 
146 bool is_number(const typet &type);
147 
148 #endif // CPROVER_UTIL_MATHEMATICAL_TYPES_H
A constant literal expression.
Definition: std_expr.h:2990
Unbounded, signed integers (mathematical integers, not bitvectors)
constant_exprt one_expr() const
constant_exprt zero_expr() const
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)
constant_exprt zero_expr() const
constant_exprt one_expr() const
Unbounded, signed rational numbers.
constant_exprt zero_expr() const
constant_exprt one_expr() const
Unbounded, signed real numbers.
constant_exprt zero_expr() const
constant_exprt one_expr() const
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