cprover
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
#include "
mathematical_types.h
"
11
12
function_application_exprt::function_application_exprt
(
13
const
exprt
&_function,
14
argumentst
_arguments)
15
:
binary_exprt
(
16
_function,
17
ID_function_application,
18
tuple_exprt
(std::move(_arguments)),
19
to_mathematical_function_type
(_function.
type
()).codomain())
20
{
21
const
auto
&domain =
to_mathematical_function_type
(_function.
type
()).
domain
();
22
PRECONDITION
(domain.size() ==
arguments
().
size
());
23
}
function_application_exprt::arguments
argumentst & arguments()
Definition:
mathematical_expr.h:221
function_application_exprt::function_application_exprt
function_application_exprt(const symbol_exprt &_function, const argumentst &_arguments, const typet &_type)
Definition:
mathematical_expr.h:197
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition:
expr.cpp:26
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:119
exprt
Base class for all expressions.
Definition:
expr.h:53
binary_exprt
A base class for binary expressions.
Definition:
std_expr.h:601
function_application_exprt::argumentst
exprt::operandst argumentst
Definition:
mathematical_expr.h:193
mathematical_types.h
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:81
mathematical_function_typet::domain
domaint & domain()
Definition:
mathematical_types.h:72
PRECONDITION
#define PRECONDITION(CONDITION)
Definition:
invariant.h:464
lispexprt::type
enum lispexprt::@10 type
tuple_exprt
Definition:
mathematical_expr.h:181
mathematical_expr.h
util
mathematical_expr.cpp
Generated by
1.8.18