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  // convenience helper
102  power_exprt(const mp_integer &_base, const exprt &_exp);
103 
104  const exprt &base() const
105  {
106  return op0();
107  }
108 
110  {
111  return op0();
112  }
113 
114  const exprt &exponent() const
115  {
116  return op1();
117  }
118 
120  {
121  return op1();
122  }
123 };
124 
125 template <>
126 inline bool can_cast_expr<power_exprt>(const exprt &base)
127 {
128  return base.id() == ID_power;
129 }
130 
137 inline const power_exprt &to_power_expr(const exprt &expr)
138 {
139  PRECONDITION(expr.id() == ID_power);
140  power_exprt::check(expr);
141  return static_cast<const power_exprt &>(expr);
142 }
143 
146 {
147  PRECONDITION(expr.id() == ID_power);
148  power_exprt::check(expr);
149  return static_cast<power_exprt &>(expr);
150 }
151 
154 {
155 public:
156  factorial_power_exprt(const exprt &_base, const exprt &_exp)
157  : binary_exprt(_base, ID_factorial_power, _exp)
158  {
159  }
160 };
161 
162 template <>
164 {
165  return base.id() == ID_factorial_power;
166 }
167 
168 inline void validate_expr(const factorial_power_exprt &value)
169 {
170  validate_operands(value, 2, "Factorial power must have two operands");
171 }
172 
180 {
181  PRECONDITION(expr.id() == ID_factorial_power);
182  const factorial_power_exprt &ret =
183  static_cast<const factorial_power_exprt &>(expr);
184  validate_expr(ret);
185  return ret;
186 }
187 
190 {
191  PRECONDITION(expr.id() == ID_factorial_power);
192  factorial_power_exprt &ret = static_cast<factorial_power_exprt &>(expr);
193  validate_expr(ret);
194  return ret;
195 }
196 
198 {
199 public:
201  : multi_ary_exprt(ID_tuple, std::move(operands), typet())
202  {
203  }
204 
206  : multi_ary_exprt(ID_tuple, std::move(operands), std::move(type))
207  {
208  }
209 };
210 
213 {
214 public:
216 
219  function_application_exprt(const exprt &_function, argumentst _arguments);
220 
221  exprt &function()
222  {
223  return op0();
224  }
225 
226  const exprt &function() const
227  {
228  return op0();
229  }
230 
233 
235  {
236  return op1().operands();
237  }
238 
239  const argumentst &arguments() const
240  {
241  return op1().operands();
242  }
243 };
244 
245 template <>
247 {
248  return base.id() == ID_function_application;
249 }
250 
251 inline void validate_expr(const function_application_exprt &value)
252 {
253  validate_operands(value, 2, "Function application must have two operands");
254 }
255 
262 inline const function_application_exprt &
264 {
265  PRECONDITION(expr.id() == ID_function_application);
266  const function_application_exprt &ret =
267  static_cast<const function_application_exprt &>(expr);
268  validate_expr(ret);
269  return ret;
270 }
271 
274 {
275  PRECONDITION(expr.id() == ID_function_application);
277  static_cast<function_application_exprt &>(expr);
278  validate_expr(ret);
279  return ret;
280 }
281 
284 {
285 public:
288  : binding_exprt(_id, {std::move(_symbol)}, std::move(_where), bool_typet())
289  {
290  }
291 
293  quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
294  : binding_exprt(_id, _variables, std::move(_where), bool_typet())
295  {
296  }
297 
298  // for the special case of one variable
300  {
301  auto &variables = this->variables();
302  PRECONDITION(variables.size() == 1);
303  return variables.front();
304  }
305 
306  // for the special case of one variable
307  const symbol_exprt &symbol() const
308  {
309  auto &variables = this->variables();
310  PRECONDITION(variables.size() == 1);
311  return variables.front();
312  }
313 };
314 
315 template <>
316 inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
317 {
318  return base.id() == ID_forall || base.id() == ID_exists;
319 }
320 
321 inline void validate_expr(const quantifier_exprt &value)
322 {
323  validate_operands(value, 2, "quantifier expressions must have two operands");
324  for(auto &op : value.variables())
326  op.id() == ID_symbol, "quantified variable shall be a symbol");
327 }
328 
335 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
336 {
338  const quantifier_exprt &ret = static_cast<const quantifier_exprt &>(expr);
339  validate_expr(ret);
340  return ret;
341 }
342 
345 {
347  quantifier_exprt &ret = static_cast<quantifier_exprt &>(expr);
348  validate_expr(ret);
349  return ret;
350 }
351 
354 {
355 public:
356  forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
357  : quantifier_exprt(ID_forall, _symbol, _where)
358  {
359  }
360 
361  forall_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
362  : quantifier_exprt(ID_forall, _variables, _where)
363  {
364  }
365 };
366 
367 template <>
368 inline bool can_cast_expr<forall_exprt>(const exprt &base)
369 {
370  return base.id() == ID_forall;
371 }
372 
373 inline void validate_expr(const forall_exprt &value)
374 {
375  validate_expr(static_cast<const quantifier_exprt &>(value));
376 }
377 
378 inline const forall_exprt &to_forall_expr(const exprt &expr)
379 {
380  PRECONDITION(expr.id() == ID_forall);
381  const forall_exprt &ret = static_cast<const forall_exprt &>(expr);
382  validate_expr(static_cast<const quantifier_exprt &>(ret));
383  return ret;
384 }
385 
387 {
388  PRECONDITION(expr.id() == ID_forall);
389  forall_exprt &ret = static_cast<forall_exprt &>(expr);
390  validate_expr(static_cast<const quantifier_exprt &>(ret));
391  return ret;
392 }
393 
396 {
397 public:
398  exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
399  : quantifier_exprt(ID_exists, _symbol, _where)
400  {
401  }
402 
403  exists_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
404  : quantifier_exprt(ID_exists, _variables, _where)
405  {
406  }
407 };
408 
409 template <>
410 inline bool can_cast_expr<exists_exprt>(const exprt &base)
411 {
412  return base.id() == ID_exists;
413 }
414 
415 inline void validate_expr(const exists_exprt &value)
416 {
417  validate_expr(static_cast<const quantifier_exprt &>(value));
418 }
419 
420 inline const exists_exprt &to_exists_expr(const exprt &expr)
421 {
422  PRECONDITION(expr.id() == ID_exists);
423  const exists_exprt &ret = static_cast<const exists_exprt &>(expr);
424  validate_expr(static_cast<const quantifier_exprt &>(ret));
425  return ret;
426 }
427 
429 {
430  PRECONDITION(expr.id() == ID_exists);
431  exists_exprt &ret = static_cast<exists_exprt &>(expr);
432  validate_expr(static_cast<const quantifier_exprt &>(ret));
433  return ret;
434 }
435 
438 {
439 public:
440  lambda_exprt(const variablest &, const exprt &_where);
441 
443  {
444  return static_cast<mathematical_function_typet &>(binding_exprt::type());
445  }
446 
448  {
449  return static_cast<const mathematical_function_typet &>(
451  }
452 
453  // apply the function to the given arguments
454  exprt application(const operandst &arguments) const
455  {
456  return instantiate(arguments);
457  }
458 };
459 
460 template <>
461 inline bool can_cast_expr<lambda_exprt>(const exprt &base)
462 {
463  return base.id() == ID_lambda;
464 }
465 
466 inline void validate_expr(const lambda_exprt &value)
467 {
468  validate_operands(value, 2, "lambda must have two operands");
469 }
470 
477 inline const lambda_exprt &to_lambda_expr(const exprt &expr)
478 {
479  PRECONDITION(expr.id() == ID_lambda);
480  DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
482  expr.type().id() == ID_mathematical_function,
483  "lambda must have right type");
484  return static_cast<const lambda_exprt &>(expr);
485 }
486 
489 {
490  PRECONDITION(expr.id() == ID_lambda);
491  DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
493  expr.type().id() == ID_mathematical_function,
494  "lambda must have right type");
495  return static_cast<lambda_exprt &>(expr);
496 }
497 
498 #endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:650
exprt & op0()
Definition: expr.h:133
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:3117
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:3138
std::vector< symbol_exprt > variablest
Definition: std_expr.h:3119
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)
const exprt & base() const
const exprt & exponent() const
exprt & exponent()
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.
BigInt mp_integer
Definition: smt_terms.h:17
#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.