cprover
Loading...
Searching...
No Matches
mathematical_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for 'mathematical' expressions
4
5Author: 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
20class transt : public ternary_exprt
21{
22public:
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
60template <>
61inline bool can_cast_expr<transt>(const exprt &base)
62{
63 return base.id() == ID_trans;
64}
65
66inline void validate_expr(const transt &value)
67{
68 validate_operands(value, 3, "Transition systems must have three operands");
69}
70
75inline 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
85{
86 PRECONDITION(expr.id() == ID_trans);
87 transt &ret = static_cast<transt &>(expr);
88 validate_expr(ret);
89 return ret;
90}
91
94{
95public:
96 power_exprt(const exprt &_base, const exprt &_exp)
97 : binary_exprt(_base, ID_power, _exp)
98 {
99 }
100};
101
102template <>
103inline bool can_cast_expr<power_exprt>(const exprt &base)
104{
105 return base.id() == ID_power;
106}
107
108inline void validate_expr(const power_exprt &value)
109{
110 validate_operands(value, 2, "Power must have two operands");
111}
112
119inline 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{
139public:
140 factorial_power_exprt(const exprt &_base, const exprt &_exp)
141 : binary_exprt(_base, ID_factorial_power, _exp)
142 {
143 }
144};
145
146template <>
148{
149 return base.id() == ID_factorial_power;
150}
151
152inline 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{
183public:
185 : multi_ary_exprt(ID_tuple, std::move(operands), typet())
186 {
187 }
188};
189
192{
193public:
195
198 function_application_exprt(const exprt &_function, argumentst _arguments);
199
201 {
202 return op0();
203 }
204
205 const exprt &function() const
206 {
207 return op0();
208 }
209
212
214 {
215 return op1().operands();
216 }
217
218 const argumentst &arguments() const
219 {
220 return op1().operands();
221 }
222};
223
224template <>
226{
227 return base.id() == ID_function_application;
228}
229
231{
232 validate_operands(value, 2, "Function application must have two operands");
233}
234
241inline const function_application_exprt &
243{
244 PRECONDITION(expr.id() == ID_function_application);
245 const function_application_exprt &ret =
246 static_cast<const function_application_exprt &>(expr);
247 validate_expr(ret);
248 return ret;
249}
250
253{
254 PRECONDITION(expr.id() == ID_function_application);
256 static_cast<function_application_exprt &>(expr);
257 validate_expr(ret);
258 return ret;
259}
260
263{
264public:
267 : binding_exprt(_id, {std::move(_symbol)}, std::move(_where), bool_typet())
268 {
269 }
270
272 quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
273 : binding_exprt(_id, _variables, std::move(_where), bool_typet())
274 {
275 }
276
277 // for the special case of one variable
279 {
280 auto &variables = this->variables();
281 PRECONDITION(variables.size() == 1);
282 return variables.front();
283 }
284
285 // for the special case of one variable
286 const symbol_exprt &symbol() const
287 {
288 auto &variables = this->variables();
289 PRECONDITION(variables.size() == 1);
290 return variables.front();
291 }
292};
293
294template <>
296{
297 return base.id() == ID_forall || base.id() == ID_exists;
298}
299
300inline void validate_expr(const quantifier_exprt &value)
301{
302 validate_operands(value, 2, "quantifier expressions must have two operands");
303 for(auto &op : value.variables())
305 op.id() == ID_symbol, "quantified variable shall be a symbol");
306}
307
314inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
315{
317 const quantifier_exprt &ret = static_cast<const quantifier_exprt &>(expr);
318 validate_expr(ret);
319 return ret;
320}
321
324{
326 quantifier_exprt &ret = static_cast<quantifier_exprt &>(expr);
327 validate_expr(ret);
328 return ret;
329}
330
333{
334public:
335 forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
336 : quantifier_exprt(ID_forall, _symbol, _where)
337 {
338 }
339
340 forall_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
341 : quantifier_exprt(ID_forall, _variables, _where)
342 {
343 }
344};
345
346template <>
347inline bool can_cast_expr<forall_exprt>(const exprt &base)
348{
349 return base.id() == ID_forall;
350}
351
352inline void validate_expr(const forall_exprt &value)
353{
354 validate_expr(static_cast<const quantifier_exprt &>(value));
355}
356
357inline const forall_exprt &to_forall_expr(const exprt &expr)
358{
359 PRECONDITION(expr.id() == ID_forall);
360 const forall_exprt &ret = static_cast<const forall_exprt &>(expr);
361 validate_expr(static_cast<const quantifier_exprt &>(ret));
362 return ret;
363}
364
366{
367 PRECONDITION(expr.id() == ID_forall);
368 forall_exprt &ret = static_cast<forall_exprt &>(expr);
369 validate_expr(static_cast<const quantifier_exprt &>(ret));
370 return ret;
371}
372
375{
376public:
377 exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
378 : quantifier_exprt(ID_exists, _symbol, _where)
379 {
380 }
381
382 exists_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
383 : quantifier_exprt(ID_exists, _variables, _where)
384 {
385 }
386};
387
388template <>
389inline bool can_cast_expr<exists_exprt>(const exprt &base)
390{
391 return base.id() == ID_exists;
392}
393
394inline void validate_expr(const exists_exprt &value)
395{
396 validate_expr(static_cast<const quantifier_exprt &>(value));
397}
398
399inline const exists_exprt &to_exists_expr(const exprt &expr)
400{
401 PRECONDITION(expr.id() == ID_exists);
402 const exists_exprt &ret = static_cast<const exists_exprt &>(expr);
403 validate_expr(static_cast<const quantifier_exprt &>(ret));
404 return ret;
405}
406
408{
409 PRECONDITION(expr.id() == ID_exists);
410 exists_exprt &ret = static_cast<exists_exprt &>(expr);
411 validate_expr(static_cast<const quantifier_exprt &>(ret));
412 return ret;
413}
414
417{
418public:
419 lambda_exprt(const variablest &, const exprt &_where);
420
422 {
423 return static_cast<mathematical_function_typet &>(binding_exprt::type());
424 }
425
427 {
428 return static_cast<const mathematical_function_typet &>(
430 }
431
432 // apply the function to the given arguments
433 exprt application(const operandst &arguments) const
434 {
435 return instantiate(arguments);
436 }
437};
438
439template <>
440inline bool can_cast_expr<lambda_exprt>(const exprt &base)
441{
442 return base.id() == ID_lambda;
443}
444
445inline void validate_expr(const lambda_exprt &value)
446{
447 validate_operands(value, 2, "lambda must have two operands");
448}
449
456inline const lambda_exprt &to_lambda_expr(const exprt &expr)
457{
458 PRECONDITION(expr.id() == ID_lambda);
459 DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
461 expr.type().id() == ID_mathematical_function,
462 "lambda must have right type");
463 return static_cast<const lambda_exprt &>(expr);
464}
465
468{
469 PRECONDITION(expr.id() == ID_lambda);
470 DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
472 expr.type().id() == ID_mathematical_function,
473 "lambda must have right type");
474 return static_cast<lambda_exprt &>(expr);
475}
476
477#endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H
A base class for binary expressions.
Definition std_expr.h:550
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:2900
variablest & variables()
Definition std_expr.h:2921
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:234
std::vector< symbol_exprt > variablest
Definition std_expr.h:2902
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:37
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:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
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.
const exprt & function() const
const mathematical_function_typet & function_type() const
This helper method provides the type of the expression returned by function.
const argumentst & arguments() const
const irep_idt & id() const
Definition irep.h:396
A (mathematical) lambda expression.
mathematical_function_typet & type()
exprt application(const operandst &arguments) const
const mathematical_function_typet & type() const
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:824
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
quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
constructor for multiple variables
const symbol_exprt & symbol() const
symbol_exprt & symbol()
Expression to hold a symbol (variable)
Definition std_expr.h:80
An expression with three operands.
Definition std_expr.h:53
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
exprt & op2()
Definition expr.h:105
Transition system, consisting of state invariant, initial state predicate, and transition predicate.
const exprt & init() const
exprt & init()
exprt & invar()
transt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
const exprt & trans() const
exprt & trans()
const exprt & invar() const
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
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
bool can_cast_expr< forall_exprt >(const exprt &base)
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast an exprt to a factorial_power_exprt.
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)
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
const exists_exprt & to_exists_expr(const exprt &expr)
bool can_cast_expr< lambda_exprt >(const exprt &base)
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
const forall_exprt & to_forall_expr(const exprt &expr)
const transt & to_trans_expr(const exprt &expr)
Cast an exprt to a transt expr must be known to be transt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
bool can_cast_expr< transt >(const exprt &base)
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
bool can_cast_expr< power_exprt >(const exprt &base)
Mathematical types.
STL namespace.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.