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 
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
lispexprt::type
enum lispexprt::@6 type
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
Mathematical types.
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
tuple_exprt
Definition: mathematical_expr.h:181
mathematical_expr.h
API to expression classes for 'mathematical' expressions.