cprover
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"
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)
66  : type_with_subtypest(ID_mathematical_function)
67  {
68  subtypes().resize(2);
69  domain() = _domain;
70  codomain() = _codomain;
71  }
72 
74  {
76  }
77 
78  const domaint &domain() const
79  {
80  return (const domaint &)to_type_with_subtypes(subtypes()[0]).subtypes();
81  }
82 
83  void add_variable(const typet &_type)
84  {
85  domain().push_back(_type);
86  }
87 
91  {
92  return subtypes()[1];
93  }
94 
96  const typet &codomain() const
97  {
98  return subtypes()[1];
99  }
100 };
101 
105 template <>
107 {
108  return type.id() == ID_mathematical_function;
109 }
110 
119 inline const mathematical_function_typet &
121 {
123  return static_cast<const mathematical_function_typet &>(type);
124 }
125 
128 {
130  return static_cast<mathematical_function_typet &>(type);
131 }
132 
133 bool is_number(const typet &type);
134 
135 #endif // CPROVER_UTIL_MATHEMATICAL_TYPES_H
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
type_with_subtypest
Type with multiple subtypes.
Definition: type.h:169
mathematical_function_typet::domain
const domaint & domain() const
Definition: mathematical_types.h:78
rational_typet
Unbounded, signed rational numbers.
Definition: mathematical_types.h:39
typet
The type of an expression, extends irept.
Definition: type.h:27
can_cast_type< 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.
Definition: mathematical_types.h:106
natural_typet::natural_typet
natural_typet()
Definition: mathematical_types.h:33
integer_typet
Unbounded, signed integers (mathematical integers, not bitvectors)
Definition: mathematical_types.h:21
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:206
to_mathematical_function_type
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Definition: mathematical_types.h:120
is_number
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Definition: mathematical_types.cpp:17
invariant.h
type_with_subtypest::subtypes
subtypest & subtypes()
Definition: type.h:191
type.h
real_typet
Unbounded, signed real numbers.
Definition: mathematical_types.h:48
mathematical_function_typet::domain
domaint & domain()
Definition: mathematical_types.h:73
mathematical_function_typet::codomain
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
Definition: mathematical_types.h:90
mathematical_function_typet::domaint
std::vector< typet > domaint
Definition: mathematical_types.h:63
irept::id
const irep_idt & id() const
Definition: irep.h:259
mathematical_function_typet::add_variable
void add_variable(const typet &_type)
Definition: mathematical_types.h:83
rational_typet::rational_typet
rational_typet()
Definition: mathematical_types.h:42
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
integer_typet::integer_typet
integer_typet()
Definition: mathematical_types.h:24
mathematical_function_typet::mathematical_function_typet
mathematical_function_typet(const domaint &_domain, const typet &_codomain)
Definition: mathematical_types.h:65
mathematical_function_typet::codomain
const typet & codomain() const
Return the codomain, i.e., the set of values that the function maps to (the "target").
Definition: mathematical_types.h:96
real_typet::real_typet
real_typet()
Definition: mathematical_types.h:51
mathematical_function_typet
A type for mathematical functions (do not confuse with functions/methods in code)
Definition: mathematical_types.h:58
natural_typet
Natural numbers including zero (mathematical integers, not bitvectors)
Definition: mathematical_types.h:30