cprover
Loading...
Searching...
No Matches
mathematical_types.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Mathematical types
4
5Author: 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
21class integer_typet : public typet
22{
23public:
24 integer_typet() : typet(ID_integer)
25 {
26 }
27};
28
30class natural_typet : public typet
31{
32public:
33 natural_typet() : typet(ID_natural)
34 {
35 }
36};
37
39class rational_typet : public typet
40{
41public:
42 rational_typet() : typet(ID_rational)
43 {
44 }
45};
46
48class real_typet : public typet
49{
50public:
51 real_typet() : typet(ID_real)
52 {
53 }
54};
55
59{
60public:
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
104template <>
106{
107 return type.id() == ID_mathematical_function;
108}
109
118inline 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
132bool 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:396
A type for mathematical functions (do not confuse with functions/methods in code)
const domaint & domain() const
const typet & codomain() const
Return the codomain, i.e., the set of values that the function maps to (the "target").
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)
Natural numbers including zero (mathematical integers, not bitvectors)
Unbounded, signed rational numbers.
Unbounded, signed real numbers.
Type with multiple subtypes.
Definition type.h:191
subtypest & subtypes()
Definition type.h:206
The type of an expression, extends irept.
Definition type.h:29
Templated functions to cast to specific exprt-derived classes.
dstringt irep_idt
Definition irep.h:37
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:221