CBMC
mathematical_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for 'mathematical' expressions
4 
5 Author: 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,
16  argumentst _arguments)
17  : binary_exprt(
18  _function,
19  ID_function_application,
20  tuple_exprt(std::move(_arguments)),
21  to_mathematical_function_type(_function.type()).codomain())
22 {
23  const auto &domain = function_type().domain();
24  PRECONDITION(domain.size() == arguments().size());
25 }
26 
29 {
30  return to_mathematical_function_type(function().type());
31 }
32 
34 lambda_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 
46 lambda_exprt::lambda_exprt(const variablest &_variables, const exprt &_where)
47  : binding_exprt(
48  ID_lambda,
49  _variables,
50  _where,
51  lambda_type(_variables, _where))
52 {
53 }
54 
55 power_exprt::power_exprt(const mp_integer &_base, const exprt &_exp)
56  : power_exprt{from_integer(_base, _exp.type()), _exp}
57 {
59 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
A base class for binary expressions.
Definition: std_expr.h:638
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:3112
std::vector< symbol_exprt > variablest
Definition: std_expr.h:3114
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)
std::vector< typet > domaint
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.
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463