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 "std_expr.h"
16 
19 class transt : public ternary_exprt
20 {
21 public:
23  const irep_idt &_id,
24  const exprt &_op0,
25  const exprt &_op1,
26  const exprt &_op2,
27  const typet &_type)
28  : ternary_exprt(_id, _op0, _op1, _op2, _type)
29  {
30  }
31 
33  {
34  return op0();
35  }
37  {
38  return op1();
39  }
41  {
42  return op2();
43  }
44 
45  const exprt &invar() const
46  {
47  return op0();
48  }
49  const exprt &init() const
50  {
51  return op1();
52  }
53  const exprt &trans() const
54  {
55  return op2();
56  }
57 };
58 
59 template <>
60 inline bool can_cast_expr<transt>(const exprt &base)
61 {
62  return base.id() == ID_trans;
63 }
64 
65 inline void validate_expr(const transt &value)
66 {
67  validate_operands(value, 3, "Transition systems must have three operands");
68 }
69 
74 inline const transt &to_trans_expr(const exprt &expr)
75 {
76  PRECONDITION(expr.id() == ID_trans);
77  const transt &ret = static_cast<const transt &>(expr);
78  validate_expr(ret);
79  return ret;
80 }
81 
83 inline transt &to_trans_expr(exprt &expr)
84 {
85  PRECONDITION(expr.id() == ID_trans);
86  transt &ret = static_cast<transt &>(expr);
87  validate_expr(ret);
88  return ret;
89 }
90 
92 class power_exprt : public binary_exprt
93 {
94 public:
95  power_exprt(const exprt &_base, const exprt &_exp)
96  : binary_exprt(_base, ID_power, _exp)
97  {
98  }
99 };
100 
101 template <>
102 inline bool can_cast_expr<power_exprt>(const exprt &base)
103 {
104  return base.id() == ID_power;
105 }
106 
107 inline void validate_expr(const power_exprt &value)
108 {
109  validate_operands(value, 2, "Power must have two operands");
110 }
111 
118 inline const power_exprt &to_power_expr(const exprt &expr)
119 {
120  PRECONDITION(expr.id() == ID_power);
121  const power_exprt &ret = static_cast<const power_exprt &>(expr);
122  validate_expr(ret);
123  return ret;
124 }
125 
128 {
129  PRECONDITION(expr.id() == ID_power);
130  power_exprt &ret = static_cast<power_exprt &>(expr);
131  validate_expr(ret);
132  return ret;
133 }
134 
137 {
138 public:
139  factorial_power_exprt(const exprt &_base, const exprt &_exp)
140  : binary_exprt(_base, ID_factorial_power, _exp)
141  {
142  }
143 };
144 
145 template <>
147 {
148  return base.id() == ID_factorial_power;
149 }
150 
151 inline void validate_expr(const factorial_power_exprt &value)
152 {
153  validate_operands(value, 2, "Factorial power must have two operands");
154 }
155 
163 {
164  PRECONDITION(expr.id() == ID_factorial_power);
165  const factorial_power_exprt &ret =
166  static_cast<const factorial_power_exprt &>(expr);
167  validate_expr(ret);
168  return ret;
169 }
170 
173 {
174  PRECONDITION(expr.id() == ID_factorial_power);
175  factorial_power_exprt &ret = static_cast<factorial_power_exprt &>(expr);
176  validate_expr(ret);
177  return ret;
178 }
179 
181 {
182 public:
184  : multi_ary_exprt(ID_tuple, std::move(operands), typet())
185  {
186  }
187 };
188 
191 {
192 public:
194 
195  DEPRECATED(
196  SINCE(2019, 3, 3, "use function_application_exprt(fkt, arg) instead"))
198  const symbol_exprt &_function,
199  const argumentst &_arguments,
200  const typet &_type)
201  : binary_exprt(
202  _function,
203  ID_function_application,
204  tuple_exprt(_arguments),
205  _type)
206  {
207  }
208 
209  function_application_exprt(const exprt &_function, argumentst _arguments);
210 
211  exprt &function()
212  {
213  return op0();
214  }
215 
216  const exprt &function() const
217  {
218  return op0();
219  }
220 
222  {
223  return op1().operands();
224  }
225 
226  const argumentst &arguments() const
227  {
228  return op1().operands();
229  }
230 };
231 
232 template <>
234 {
235  return base.id() == ID_function_application;
236 }
237 
238 inline void validate_expr(const function_application_exprt &value)
239 {
240  validate_operands(value, 2, "Function application must have two operands");
241 }
242 
249 inline const function_application_exprt &
251 {
252  PRECONDITION(expr.id() == ID_function_application);
253  const function_application_exprt &ret =
254  static_cast<const function_application_exprt &>(expr);
255  validate_expr(ret);
256  return ret;
257 }
258 
261 {
262  PRECONDITION(expr.id() == ID_function_application);
264  static_cast<function_application_exprt &>(expr);
265  validate_expr(ret);
266  return ret;
267 }
268 
271 {
272 public:
275  : binding_exprt(_id, {std::move(_symbol)}, std::move(_where), bool_typet())
276  {
277  }
278 
280  quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
281  : binding_exprt(_id, _variables, std::move(_where), bool_typet())
282  {
283  }
284 
285  // for the special case of one variable
287  {
288  auto &variables = this->variables();
289  PRECONDITION(variables.size() == 1);
290  return variables.front();
291  }
292 
293  // for the special case of one variable
294  const symbol_exprt &symbol() const
295  {
296  auto &variables = this->variables();
297  PRECONDITION(variables.size() == 1);
298  return variables.front();
299  }
300 };
301 
302 template <>
303 inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
304 {
305  return base.id() == ID_forall || base.id() == ID_exists;
306 }
307 
308 inline void validate_expr(const quantifier_exprt &value)
309 {
310  validate_operands(value, 2, "quantifier expressions must have two operands");
311  for(auto &op : value.variables())
313  op.id() == ID_symbol, "quantified variable shall be a symbol");
314 }
315 
322 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
323 {
325  const quantifier_exprt &ret = static_cast<const quantifier_exprt &>(expr);
326  validate_expr(ret);
327  return ret;
328 }
329 
332 {
334  quantifier_exprt &ret = static_cast<quantifier_exprt &>(expr);
335  validate_expr(ret);
336  return ret;
337 }
338 
341 {
342 public:
343  forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
344  : quantifier_exprt(ID_forall, _symbol, _where)
345  {
346  }
347 };
348 
349 inline const forall_exprt &to_forall_expr(const exprt &expr)
350 {
351  PRECONDITION(expr.id() == ID_forall);
352  const forall_exprt &ret = static_cast<const forall_exprt &>(expr);
353  validate_expr(static_cast<const quantifier_exprt &>(ret));
354  return ret;
355 }
356 
358 {
359  PRECONDITION(expr.id() == ID_forall);
360  forall_exprt &ret = static_cast<forall_exprt &>(expr);
361  validate_expr(static_cast<const quantifier_exprt &>(ret));
362  return ret;
363 }
364 
367 {
368 public:
369  exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
370  : quantifier_exprt(ID_exists, _symbol, _where)
371  {
372  }
373 };
374 
375 inline const exists_exprt &to_exists_expr(const exprt &expr)
376 {
377  PRECONDITION(expr.id() == ID_exists);
378  const exists_exprt &ret = static_cast<const exists_exprt &>(expr);
379  validate_expr(static_cast<const quantifier_exprt &>(ret));
380  return ret;
381 }
382 
384 {
385  PRECONDITION(expr.id() == ID_exists);
386  exists_exprt &ret = static_cast<exists_exprt &>(expr);
387  validate_expr(static_cast<const quantifier_exprt &>(ret));
388  return ret;
389 }
390 
391 #endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H
function_application_exprt::arguments
const argumentst & arguments() const
Definition: mathematical_expr.h:226
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:221
can_cast_expr< factorial_power_exprt >
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
Definition: mathematical_expr.h:146
can_cast_expr< quantifier_exprt >
bool can_cast_expr< quantifier_exprt >(const exprt &base)
Definition: mathematical_expr.h:303
factorial_power_exprt
Falling factorial power.
Definition: mathematical_expr.h:137
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:791
forall_exprt
A forall expression.
Definition: mathematical_expr.h:341
function_application_exprt::function_application_exprt
function_application_exprt(const symbol_exprt &_function, const argumentst &_arguments, const typet &_type)
Definition: mathematical_expr.h:197
ternary_exprt::op2
exprt & op2()
Definition: expr.h:108
typet
The type of an expression, extends irept.
Definition: type.h:29
validate_expr
void validate_expr(const transt &value)
Definition: mathematical_expr.h:65
ternary_exprt
An expression with three operands.
Definition: std_expr.h:55
power_exprt
Exponentiation.
Definition: mathematical_expr.h:93
transt::invar
exprt & invar()
Definition: mathematical_expr.h:32
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:162
exists_exprt
An exists expression.
Definition: mathematical_expr.h:367
ternary_exprt::op1
exprt & op1()
Definition: expr.h:105
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
bool_typet
The Boolean type.
Definition: std_types.h:37
quantifier_exprt
A base class for quantifier expressions.
Definition: mathematical_expr.h:271
quantifier_exprt::symbol
const symbol_exprt & symbol() const
Definition: mathematical_expr.h:294
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
power_exprt::power_exprt
power_exprt(const exprt &_base, const exprt &_exp)
Definition: mathematical_expr.h:95
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: mathematical_expr.h:193
transt
Transition system, consisting of state invariant, initial state predicate, and transition predicate.
Definition: mathematical_expr.h:20
forall_exprt::forall_exprt
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: mathematical_expr.h:343
binding_exprt::variables
variablest & variables()
Definition: std_expr.h:4142
transt::transt
transt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
Definition: mathematical_expr.h:22
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:280
transt::init
const exprt & init() const
Definition: mathematical_expr.h:49
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
quantifier_exprt::symbol
symbol_exprt & symbol()
Definition: mathematical_expr.h:286
ternary_exprt::op0
exprt & op0()
Definition: expr.h:102
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:74
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:4123
transt::init
exprt & init()
Definition: mathematical_expr.h:36
irept::id
const irep_idt & id() const
Definition: irep.h:418
binding_exprt
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:4121
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
tuple_exprt::tuple_exprt
tuple_exprt(exprt::operandst operands)
Definition: mathematical_expr.h:183
can_cast_expr< power_exprt >
bool can_cast_expr< power_exprt >(const exprt &base)
Definition: mathematical_expr.h:102
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
transt::invar
const exprt & invar() const
Definition: mathematical_expr.h:45
factorial_power_exprt::factorial_power_exprt
factorial_power_exprt(const exprt &_base, const exprt &_exp)
Definition: mathematical_expr.h:139
to_exists_expr
const exists_exprt & to_exists_expr(const exprt &expr)
Definition: mathematical_expr.h:375
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:322
can_cast_expr< function_application_exprt >
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: mathematical_expr.h:233
can_cast_expr< transt >
bool can_cast_expr< transt >(const exprt &base)
Definition: mathematical_expr.h:60
to_factorial_expr
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
Definition: mathematical_expr.h:172
transt::trans
exprt & trans()
Definition: mathematical_expr.h:40
transt::trans
const exprt & trans() const
Definition: mathematical_expr.h:53
tuple_exprt
Definition: mathematical_expr.h:181
exprt::operands
operandst & operands()
Definition: expr.h:95
to_power_expr
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
Definition: mathematical_expr.h:118
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
std_expr.h
API to expression classes.
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:250
exists_exprt::exists_exprt
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
Definition: mathematical_expr.h:369
to_forall_expr
const forall_exprt & to_forall_expr(const exprt &expr)
Definition: mathematical_expr.h:349
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
quantifier_exprt::quantifier_exprt
quantifier_exprt(irep_idt _id, symbol_exprt _symbol, exprt _where)
constructor for single variable
Definition: mathematical_expr.h:274