CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
mathematical_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for 'mathematical' expressions
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "mathematical_expr.h"
10
11#include "arith_tools.h"
12#include "mathematical_types.h"
13
15 const exprt &_function,
22{
23 const auto &domain = function_type().domain();
24 PRECONDITION(domain.size() == arguments().size());
25}
26
32
34lambda_type(const lambda_exprt::variablest &variables, const exprt &where)
35{
37
38 domain.reserve(variables.size());
39
40 for(const auto &v : variables)
41 domain.push_back(v.type());
42
43 return mathematical_function_typet(std::move(domain), where.type());
44}
45
54
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A base class for binary expressions.
Definition std_expr.h:638
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:3234
std::vector< symbol_exprt > variablest
Definition std_expr.h:3236
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
function_application_exprt(const exprt &_function, argumentst _arguments)
const mathematical_function_typet & function_type() const
This helper method provides the type of the expression returned by function.
bool is_not_nil() const
Definition irep.h:372
lambda_exprt(const variablest &, const exprt &_where)
A type for mathematical functions (do not confuse with functions/methods in code)
Exponentiation.
power_exprt(const exprt &_base, const exprt &_exp)
const exprt & base() const
static mathematical_function_typet lambda_type(const lambda_exprt::variablest &variables, const exprt &where)
API to expression classes for 'mathematical' expressions.
Mathematical types.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
STL namespace.
#define PRECONDITION(CONDITION)
Definition invariant.h:463