cprover
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 };
189 
191 
194 {
195 public:
197 
200  function_application_exprt(const exprt &_function, argumentst _arguments);
201 
202  exprt &function()
203  {
204  return op0();
205  }
206 
207  const exprt &function() const
208  {
209  return op0();
210  }
211 
214 
216  {
217  return op1().operands();
218  }
219 
220  const argumentst &arguments() const
221  {
222  return op1().operands();
223  }
224 };
225 
226 template <>
228 {
229  return base.id() == ID_function_application;
230 }
231 
232 inline void validate_expr(const function_application_exprt &value)
233 {
234  validate_operands(value, 2, "Function application must have two operands");
235 }
236 
243 inline const function_application_exprt &
245 {
246  PRECONDITION(expr.id() == ID_function_application);
247  const function_application_exprt &ret =
248  static_cast<const function_application_exprt &>(expr);
249  validate_expr(ret);
250  return ret;
251 }
252 
255 {
256  PRECONDITION(expr.id() == ID_function_application);
258  static_cast<function_application_exprt &>(expr);
259  validate_expr(ret);
260  return ret;
261 }
262 
265 {
266 public:
269  : binding_exprt(_id, {std::move(_symbol)}, std::move(_where), bool_typet())
270  {
271  }
272 
274  quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
275  : binding_exprt(_id, _variables, std::move(_where), bool_typet())
276  {
277  }
278 
279  // for the special case of one variable
281  {
282  auto &variables = this->variables();
283  PRECONDITION(variables.size() == 1);
284  return variables.front();
285  }
286 
287  // for the special case of one variable
288  const symbol_exprt &symbol() const
289  {
290  auto &variables = this->variables();
291  PRECONDITION(variables.size() == 1);
292  return variables.front();
293  }
294 };
295 
296 template <>
297 inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
298 {
299  return base.id() == ID_forall || base.id() == ID_exists;
300 }
301 
302 inline void validate_expr(const quantifier_exprt &value)
303 {
304  validate_operands(value, 2, "quantifier expressions must have two operands");
305  for(auto &op : value.variables())
307  op.id() == ID_symbol, "quantified variable shall be a symbol");
308 }
309 
316 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
317 {
319  const quantifier_exprt &ret = static_cast<const quantifier_exprt &>(expr);
320  validate_expr(ret);
321  return ret;
322 }
323 
326 {
328  quantifier_exprt &ret = static_cast<quantifier_exprt &>(expr);
329  validate_expr(ret);
330  return ret;
331 }
332 
335 {
336 public:
337  forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
338  : quantifier_exprt(ID_forall, _symbol, _where)
339  {
340  }
341 };
342 
343 inline const forall_exprt &to_forall_expr(const exprt &expr)
344 {
345  PRECONDITION(expr.id() == ID_forall);
346  const forall_exprt &ret = static_cast<const forall_exprt &>(expr);
347  validate_expr(static_cast<const quantifier_exprt &>(ret));
348  return ret;
349 }
350 
352 {
353  PRECONDITION(expr.id() == ID_forall);
354  forall_exprt &ret = static_cast<forall_exprt &>(expr);
355  validate_expr(static_cast<const quantifier_exprt &>(ret));
356  return ret;
357 }
358 
361 {
362 public:
363  exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
364  : quantifier_exprt(ID_exists, _symbol, _where)
365  {
366  }
367 };
368 
369 inline const exists_exprt &to_exists_expr(const exprt &expr)
370 {
371  PRECONDITION(expr.id() == ID_exists);
372  const exists_exprt &ret = static_cast<const exists_exprt &>(expr);
373  validate_expr(static_cast<const quantifier_exprt &>(ret));
374  return ret;
375 }
376 
378 {
379  PRECONDITION(expr.id() == ID_exists);
380  exists_exprt &ret = static_cast<exists_exprt &>(expr);
381  validate_expr(static_cast<const quantifier_exprt &>(ret));
382  return ret;
383 }
384 
387 {
388 public:
389  lambda_exprt(const variablest &, const exprt &_where);
390 
392  {
393  return static_cast<mathematical_function_typet &>(binding_exprt::type());
394  }
395 
397  {
398  return static_cast<const mathematical_function_typet &>(
400  }
401 
402  // apply the function to the given arguments
403  exprt application(const operandst &) const;
404 };
405 
406 template <>
407 inline bool can_cast_expr<lambda_exprt>(const exprt &base)
408 {
409  return base.id() == ID_lambda;
410 }
411 
412 inline void validate_expr(const lambda_exprt &value)
413 {
414  validate_operands(value, 2, "lambda must have two operands");
415 }
416 
423 inline const lambda_exprt &to_lambda_expr(const exprt &expr)
424 {
425  PRECONDITION(expr.id() == ID_lambda);
426  DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
428  expr.type().id() == ID_mathematical_function,
429  "lambda must have right type");
430  return static_cast<const lambda_exprt &>(expr);
431 }
432 
435 {
436  PRECONDITION(expr.id() == ID_lambda);
437  DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
439  expr.type().id() == ID_mathematical_function,
440  "lambda must have right type");
441  return static_cast<lambda_exprt &>(expr);
442 }
443 
444 #endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H
function_application_exprt::arguments
const argumentst & arguments() const
Definition: mathematical_expr.h:220
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:215
can_cast_expr< factorial_power_exprt >
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
Definition: mathematical_expr.h:147
can_cast_expr< quantifier_exprt >
bool can_cast_expr< quantifier_exprt >(const exprt &base)
Definition: mathematical_expr.h:297
factorial_power_exprt
Falling factorial power.
Definition: mathematical_expr.h:138
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:741
to_lambda_expr
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Definition: mathematical_expr.h:423
forall_exprt
A forall expression.
Definition: mathematical_expr.h:335
ternary_exprt::op2
exprt & op2()
Definition: expr.h:109
typet
The type of an expression, extends irept.
Definition: type.h:28
validate_expr
void validate_expr(const transt &value)
Definition: mathematical_expr.h:66
ternary_exprt
An expression with three operands.
Definition: std_expr.h:54
power_exprt
Exponentiation.
Definition: mathematical_expr.h:94
lambda_exprt::type
const mathematical_function_typet & type() const
Definition: mathematical_expr.h:396
transt::invar
exprt & invar()
Definition: mathematical_expr.h:33
validate_operands
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
to_factorial_power_expr
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast an exprt to a factorial_power_exprt.
Definition: mathematical_expr.h:163
exists_exprt
An exists expression.
Definition: mathematical_expr.h:361
ternary_exprt::op1
exprt & op1()
Definition: expr.h:106
exprt
Base class for all expressions.
Definition: expr.h:54
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
bool_typet
The Boolean type.
Definition: std_types.h:37
quantifier_exprt
A base class for quantifier expressions.
Definition: mathematical_expr.h:265
quantifier_exprt::symbol
const symbol_exprt & symbol() const
Definition: mathematical_expr.h:288
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
power_exprt::power_exprt
power_exprt(const exprt &_base, const exprt &_exp)
Definition: mathematical_expr.h:96
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: mathematical_expr.h:196
transt
Transition system, consisting of state invariant, initial state predicate, and transition predicate.
Definition: mathematical_expr.h:21
forall_exprt::forall_exprt
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: mathematical_expr.h:337
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
transt::transt
transt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
Definition: mathematical_expr.h:23
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
quantifier_exprt::quantifier_exprt
quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
constructor for multiple variables
Definition: mathematical_expr.h:274
transt::init
const exprt & init() const
Definition: mathematical_expr.h:50
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
quantifier_exprt::symbol
symbol_exprt & symbol()
Definition: mathematical_expr.h:280
ternary_exprt::op0
exprt & op0()
Definition: expr.h:103
to_trans_expr
const transt & to_trans_expr(const exprt &expr)
Cast an exprt to a transt expr must be known to be transt.
Definition: mathematical_expr.h:75
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:194
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2774
transt::init
exprt & init()
Definition: mathematical_expr.h:37
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
tuple_exprt::tuple_exprt
tuple_exprt(exprt::operandst operands)
Definition: mathematical_expr.h:184
can_cast_expr< power_exprt >
bool can_cast_expr< power_exprt >(const exprt &base)
Definition: mathematical_expr.h:103
transt::invar
const exprt & invar() const
Definition: mathematical_expr.h:46
factorial_power_exprt::factorial_power_exprt
factorial_power_exprt(const exprt &_base, const exprt &_exp)
Definition: mathematical_expr.h:140
to_exists_expr
const exists_exprt & to_exists_expr(const exprt &expr)
Definition: mathematical_expr.h:369
function_application_exprt::function_application_exprt
function_application_exprt(const exprt &_function, argumentst _arguments)
Definition: mathematical_expr.cpp:14
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:316
can_cast_expr< lambda_exprt >
bool can_cast_expr< lambda_exprt >(const exprt &base)
Definition: mathematical_expr.h:407
can_cast_expr< function_application_exprt >
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: mathematical_expr.h:227
lambda_exprt::type
mathematical_function_typet & type()
Definition: mathematical_expr.h:391
lambda_exprt
A (mathematical) lambda expression.
Definition: mathematical_expr.h:387
can_cast_expr< transt >
bool can_cast_expr< transt >(const exprt &base)
Definition: mathematical_expr.h:61
to_factorial_expr
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
Definition: mathematical_expr.h:173
transt::trans
exprt & trans()
Definition: mathematical_expr.h:41
transt::trans
const exprt & trans() const
Definition: mathematical_expr.h:54
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
to_power_expr
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
Definition: mathematical_expr.h:119
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
std_expr.h
API to expression classes.
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
to_function_application_expr
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: mathematical_expr.h:244
exists_exprt::exists_exprt
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: mathematical_expr.h:363
to_forall_expr
const forall_exprt & to_forall_expr(const exprt &expr)
Definition: mathematical_expr.h:343
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
quantifier_exprt::quantifier_exprt
quantifier_exprt(irep_idt _id, symbol_exprt _symbol, exprt _where)
constructor for single variable
Definition: mathematical_expr.h:268