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
The type of an expression, extends irept.
Definition: type.h:27
mathematical_function_typet(const domaint &_domain, const typet &_codomain)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:206
Natural numbers including zero (mathematical integers, not bitvectors)
std::vector< typet > domaint
Unbounded, signed rational numbers.
Type with multiple subtypes.
Definition: type.h:169
subtypest & subtypes()
Definition: type.h:191
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
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, signedbv, floatbv or fixedbv.
A type for mathematical functions (do not confuse with functions/methods in code) ...
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const domaint & domain() const
Unbounded, signed integers (mathematical integers, not bitvectors)
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
Unbounded, signed real numbers.
void add_variable(const typet &_type)
const typet & codomain() const
Return the codomain, i.e., the set of values that the function maps to (the "target").
Defines typet, type_with_subtypet and type_with_subtypest.
bool can_cast_type< mathematical_function_typet >(const typet &type)
Check whether a reference to a typet is a mathematical_function_typet.