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 #include <map>
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 
56  const std::map<irep_idt, exprt> &substitutions,
57  exprt src)
58 {
59  if(src.id() == ID_symbol)
60  {
61  auto s_it = substitutions.find(to_symbol_expr(src).get_identifier());
62  if(s_it == substitutions.end())
63  return {};
64  else
65  return s_it->second;
66  }
67 
68  if(!src.has_operands())
69  return {};
70 
71  bool op_changed = false;
72 
73  for(auto &op : src.operands())
74  {
75  auto op_result = substitute_symbols_rec(substitutions, op);
76 
77  if(op_result.has_value())
78  {
79  op = op_result.value();
80  op_changed = true;
81  }
82  }
83 
84  if(op_changed)
85  return src;
86  else
87  return {};
88 }
89 
90 exprt lambda_exprt::application(const operandst &arguments) const
91 {
92  // number of arguments must match function signature
93  auto &variables = this->variables();
94  PRECONDITION(variables.size() == arguments.size());
95 
96  std::map<symbol_exprt, exprt> value_map;
97 
98  for(std::size_t i = 0; i < variables.size(); i++)
99  {
100  // types must match
101  PRECONDITION(variables[i].type() == arguments[i].type());
102  value_map[variables[i]] = arguments[i];
103  }
104 
105  // build a subsitution map
106  std::map<irep_idt, exprt> substitutions;
107 
108  for(std::size_t i = 0; i < variables.size(); i++)
109  substitutions[variables[i].get_identifier()] = arguments[i];
110 
111  // now recurse downwards and substitute in 'where'
112  auto substitute_result = substitute_symbols_rec(substitutions, where());
113 
114  if(substitute_result.has_value())
115  return substitute_result.value();
116  else
117  return where(); // trivial case, variables not used
118 }
lambda_type
static mathematical_function_typet lambda_type(const lambda_exprt::variablest &variables, const exprt &where)
Definition: mathematical_expr.cpp:34
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:215
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
substitute_symbols_rec
static optionalt< exprt > substitute_symbols_rec(const std::map< irep_idt, exprt > &substitutions, exprt src)
Definition: mathematical_expr.cpp:55
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:54
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: mathematical_expr.h:196
binding_exprt::variables
variablest & variables()
Definition: std_expr.h:2793
mathematical_types.h
Mathematical types.
function_application_exprt::function_type
const mathematical_function_typet & function_type() const
This helper method provides the type of the expression returned by function.
Definition: mathematical_expr.cpp:28
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
mathematical_function_typet::domain
domaint & domain()
Definition: mathematical_types.h:72
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2774
mathematical_function_typet::domaint
std::vector< typet > domaint
Definition: mathematical_types.h:63
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
irept::id
const irep_idt & id() const
Definition: irep.h:407
binding_exprt
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:2772
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
lispexprt::type
enum lispexprt::@8 type
function_application_exprt::function_application_exprt
function_application_exprt(const exprt &_function, argumentst _arguments)
Definition: mathematical_expr.cpp:14
binding_exprt::where
exprt & where()
Definition: std_expr.h:2803
lambda_exprt::type
mathematical_function_typet & type()
Definition: mathematical_expr.h:391
lambda_exprt::application
exprt application(const operandst &) const
Definition: mathematical_expr.cpp:90
tuple_exprt
Definition: mathematical_expr.h:182
exprt::operands
operandst & operands()
Definition: expr.h:96
lambda_exprt::lambda_exprt
lambda_exprt(const variablest &, const exprt &_where)
Definition: mathematical_expr.cpp:46
mathematical_function_typet
A type for mathematical functions (do not confuse with functions/methods in code)
Definition: mathematical_types.h:59
mathematical_expr.h
API to expression classes for 'mathematical' expressions.