CBMC
mathematical_expr.h
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 #ifndef CPROVER_UTIL_MATHEMATICAL_EXPR_H
10 #define CPROVER_UTIL_MATHEMATICAL_EXPR_H
11 
14 
15 #include "mathematical_types.h"
16 #include "std_expr.h"
17 
20 class transt : public ternary_exprt
21 {
22 public:
24  const irep_idt &_id,
25  const exprt &_op0,
26  const exprt &_op1,
27  const exprt &_op2,
28  const typet &_type)
29  : ternary_exprt(_id, _op0, _op1, _op2, _type)
30  {
31  }
32 
34  {
35  return op0();
36  }
38  {
39  return op1();
40  }
42  {
43  return op2();
44  }
45 
46  const exprt &invar() const
47  {
48  return op0();
49  }
50  const exprt &init() const
51  {
52  return op1();
53  }
54  const exprt &trans() const
55  {
56  return op2();
57  }
58 };
59 
60 template <>
61 inline bool can_cast_expr<transt>(const exprt &base)
62 {
63  return base.id() == ID_trans;
64 }
65 
66 inline void validate_expr(const transt &value)
67 {
68  validate_operands(value, 3, "Transition systems must have three operands");
69 }
70 
75 inline const transt &to_trans_expr(const exprt &expr)
76 {
77  PRECONDITION(expr.id() == ID_trans);
78  const transt &ret = static_cast<const transt &>(expr);
79  validate_expr(ret);
80  return ret;
81 }
82 
84 inline transt &to_trans_expr(exprt &expr)
85 {
86  PRECONDITION(expr.id() == ID_trans);
87  transt &ret = static_cast<transt &>(expr);
88  validate_expr(ret);
89  return ret;
90 }
91 
93 class power_exprt : public binary_exprt
94 {
95 public:
96  power_exprt(const exprt &_base, const exprt &_exp)
97  : binary_exprt(_base, ID_power, _exp)
98  {
99  }
100 };
101 
102 template <>
103 inline bool can_cast_expr<power_exprt>(const exprt &base)
104 {
105  return base.id() == ID_power;
106 }
107 
108 inline void validate_expr(const power_exprt &value)
109 {
110  validate_operands(value, 2, "Power must have two operands");
111 }
112 
119 inline const power_exprt &to_power_expr(const exprt &expr)
120 {
121  PRECONDITION(expr.id() == ID_power);
122  const power_exprt &ret = static_cast<const power_exprt &>(expr);
123  validate_expr(ret);
124  return ret;
125 }
126 
129 {
130  PRECONDITION(expr.id() == ID_power);
131  power_exprt &ret = static_cast<power_exprt &>(expr);
132  validate_expr(ret);
133  return ret;
134 }
135 
138 {
139 public:
140  factorial_power_exprt(const exprt &_base, const exprt &_exp)
141  : binary_exprt(_base, ID_factorial_power, _exp)
142  {
143  }
144 };
145 
146 template <>
148 {
149  return base.id() == ID_factorial_power;
150 }
151 
152 inline void validate_expr(const factorial_power_exprt &value)
153 {
154  validate_operands(value, 2, "Factorial power must have two operands");
155 }
156 
164 {
165  PRECONDITION(expr.id() == ID_factorial_power);
166  const factorial_power_exprt &ret =
167  static_cast<const factorial_power_exprt &>(expr);
168  validate_expr(ret);
169  return ret;
170 }
171 
174 {
175  PRECONDITION(expr.id() == ID_factorial_power);
176  factorial_power_exprt &ret = static_cast<factorial_power_exprt &>(expr);
177  validate_expr(ret);
178  return ret;
179 }
180 
182 {
183 public:
185  : multi_ary_exprt(ID_tuple, std::move(operands), typet())
186  {
187  }
188 
190  : multi_ary_exprt(ID_tuple, std::move(operands), std::move(type))
191  {
192  }
193 };
194 
197 {
198 public:
200 
203  function_application_exprt(const exprt &_function, argumentst _arguments);
204 
205  exprt &function()
206  {
207  return op0();
208  }
209 
210  const exprt &function() const
211  {
212  return op0();
213  }
214 
217 
219  {
220  return op1().operands();
221  }
222 
223  const argumentst &arguments() const
224  {
225  return op1().operands();
226  }
227 };
228 
229 template <>
231 {
232  return base.id() == ID_function_application;
233 }
234 
235 inline void validate_expr(const function_application_exprt &value)
236 {
237  validate_operands(value, 2, "Function application must have two operands");
238 }
239 
246 inline const function_application_exprt &
248 {
249  PRECONDITION(expr.id() == ID_function_application);
250  const function_application_exprt &ret =
251  static_cast<const function_application_exprt &>(expr);
252  validate_expr(ret);
253  return ret;
254 }
255 
258 {
259  PRECONDITION(expr.id() == ID_function_application);
261  static_cast<function_application_exprt &>(expr);
262  validate_expr(ret);
263  return ret;
264 }
265 
268 {
269 public:
272  : binding_exprt(_id, {std::move(_symbol)}, std::move(_where), bool_typet())
273  {
274  }
275 
277  quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
278  : binding_exprt(_id, _variables, std::move(_where), bool_typet())
279  {
280  }
281 
282  // for the special case of one variable
284  {
285  auto &variables = this->variables();
286  PRECONDITION(variables.size() == 1);
287  return variables.front();
288  }
289 
290  // for the special case of one variable
291  const symbol_exprt &symbol() const
292  {
293  auto &variables = this->variables();
294  PRECONDITION(variables.size() == 1);
295  return variables.front();
296  }
297 };
298 
299 template <>
300 inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
301 {
302  return base.id() == ID_forall || base.id() == ID_exists;
303 }
304 
305 inline void validate_expr(const quantifier_exprt &value)
306 {
307  validate_operands(value, 2, "quantifier expressions must have two operands");
308  for(auto &op : value.variables())
310  op.id() == ID_symbol, "quantified variable shall be a symbol");
311 }
312 
319 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
320 {
322  const quantifier_exprt &ret = static_cast<const quantifier_exprt &>(expr);
323  validate_expr(ret);
324  return ret;
325 }
326 
329 {
331  quantifier_exprt &ret = static_cast<quantifier_exprt &>(expr);
332  validate_expr(ret);
333  return ret;
334 }
335 
338 {
339 public:
340  forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
341  : quantifier_exprt(ID_forall, _symbol, _where)
342  {
343  }
344 
345  forall_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
346  : quantifier_exprt(ID_forall, _variables, _where)
347  {
348  }
349 };
350 
351 template <>
352 inline bool can_cast_expr<forall_exprt>(const exprt &base)
353 {
354  return base.id() == ID_forall;
355 }
356 
357 inline void validate_expr(const forall_exprt &value)
358 {
359  validate_expr(static_cast<const quantifier_exprt &>(value));
360 }
361 
362 inline const forall_exprt &to_forall_expr(const exprt &expr)
363 {
364  PRECONDITION(expr.id() == ID_forall);
365  const forall_exprt &ret = static_cast<const forall_exprt &>(expr);
366  validate_expr(static_cast<const quantifier_exprt &>(ret));
367  return ret;
368 }
369 
371 {
372  PRECONDITION(expr.id() == ID_forall);
373  forall_exprt &ret = static_cast<forall_exprt &>(expr);
374  validate_expr(static_cast<const quantifier_exprt &>(ret));
375  return ret;
376 }
377 
380 {
381 public:
382  exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
383  : quantifier_exprt(ID_exists, _symbol, _where)
384  {
385  }
386 
387  exists_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
388  : quantifier_exprt(ID_exists, _variables, _where)
389  {
390  }
391 };
392 
393 template <>
394 inline bool can_cast_expr<exists_exprt>(const exprt &base)
395 {
396  return base.id() == ID_exists;
397 }
398 
399 inline void validate_expr(const exists_exprt &value)
400 {
401  validate_expr(static_cast<const quantifier_exprt &>(value));
402 }
403 
404 inline const exists_exprt &to_exists_expr(const exprt &expr)
405 {
406  PRECONDITION(expr.id() == ID_exists);
407  const exists_exprt &ret = static_cast<const exists_exprt &>(expr);
408  validate_expr(static_cast<const quantifier_exprt &>(ret));
409  return ret;
410 }
411 
413 {
414  PRECONDITION(expr.id() == ID_exists);
415  exists_exprt &ret = static_cast<exists_exprt &>(expr);
416  validate_expr(static_cast<const quantifier_exprt &>(ret));
417  return ret;
418 }
419 
422 {
423 public:
424  lambda_exprt(const variablest &, const exprt &_where);
425 
427  {
428  return static_cast<mathematical_function_typet &>(binding_exprt::type());
429  }
430 
432  {
433  return static_cast<const mathematical_function_typet &>(
435  }
436 
437  // apply the function to the given arguments
438  exprt application(const operandst &arguments) const
439  {
440  return instantiate(arguments);
441  }
442 };
443 
444 template <>
445 inline bool can_cast_expr<lambda_exprt>(const exprt &base)
446 {
447  return base.id() == ID_lambda;
448 }
449 
450 inline void validate_expr(const lambda_exprt &value)
451 {
452  validate_operands(value, 2, "lambda must have two operands");
453 }
454 
461 inline const lambda_exprt &to_lambda_expr(const exprt &expr)
462 {
463  PRECONDITION(expr.id() == ID_lambda);
464  DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
466  expr.type().id() == ID_mathematical_function,
467  "lambda must have right type");
468  return static_cast<const lambda_exprt &>(expr);
469 }
470 
473 {
474  PRECONDITION(expr.id() == ID_lambda);
475  DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
477  expr.type().id() == ID_mathematical_function,
478  "lambda must have right type");
479  return static_cast<lambda_exprt &>(expr);
480 }
481 
482 #endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:3107
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition: std_expr.cpp:225
variablest & variables()
Definition: std_expr.h:3128
std::vector< symbol_exprt > variablest
Definition: std_expr.h:3109
The Boolean type.
Definition: std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
An exists expression.
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
exists_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
Falling factorial power.
factorial_power_exprt(const exprt &_base, const exprt &_exp)
A forall expression.
forall_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
Application of (mathematical) function.
function_application_exprt(const exprt &_function, argumentst _arguments)
const argumentst & arguments() const
const mathematical_function_typet & function_type() const
This helper method provides the type of the expression returned by function.
const irep_idt & id() const
Definition: irep.h:388
A (mathematical) lambda expression.
lambda_exprt(const variablest &, const exprt &_where)
const mathematical_function_typet & type() const
exprt application(const operandst &arguments) const
mathematical_function_typet & type()
A type for mathematical functions (do not confuse with functions/methods in code)
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:912
Exponentiation.
power_exprt(const exprt &_base, const exprt &_exp)
A base class for quantifier expressions.
quantifier_exprt(irep_idt _id, symbol_exprt _symbol, exprt _where)
constructor for single variable
const symbol_exprt & symbol() const
symbol_exprt & symbol()
quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
constructor for multiple variables
Expression to hold a symbol (variable)
Definition: std_expr.h:131
An expression with three operands.
Definition: std_expr.h:67
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
Transition system, consisting of state invariant, initial state predicate, and transition predicate.
exprt & init()
const exprt & invar() const
const exprt & init() const
transt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
exprt & trans()
exprt & invar()
const exprt & trans() const
tuple_exprt(exprt::operandst operands, typet type)
tuple_exprt(exprt::operandst operands)
The type of an expression, extends irept.
Definition: type.h:29
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
bool can_cast_expr< forall_exprt >(const exprt &base)
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const exists_exprt & to_exists_expr(const exprt &expr)
bool can_cast_expr< quantifier_exprt >(const exprt &base)
bool can_cast_expr< exists_exprt >(const exprt &base)
void validate_expr(const transt &value)
bool can_cast_expr< function_application_exprt >(const exprt &base)
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast an exprt to a factorial_power_exprt.
bool can_cast_expr< lambda_exprt >(const exprt &base)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const transt & to_trans_expr(const exprt &expr)
Cast an exprt to a transt expr must be known to be transt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const forall_exprt & to_forall_expr(const exprt &expr)
bool can_cast_expr< transt >(const exprt &base)
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
bool can_cast_expr< power_exprt >(const exprt &base)
Mathematical types.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.