Skip to content

Commit 545835c

Browse files
tautschnigtautschnig
committed
Re-use validate_expr in mathematical_expr.h
This provides two advantages: 1) Member access such as testing the number of operands does not break sharing, because it is done in a const context. 2) Code re-use: we no longer implement the same check in two different ways. With the exception of {exist,forall,quantifier}_exprt, all changes in this commit were applied automatically via text replacement. For quantifiers, additional checks were inserted (use of can_cast_expr, validate_expr uses quantifier_exprt's validate_expr).
1 parent 7cbb983 commit 545835c

File tree

1 file changed

+49
-50
lines changed

1 file changed

+49
-50
lines changed

‎src/util/mathematical_expr.h

Lines changed: 49 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -79,18 +79,18 @@ inline void validate_expr(const transt &value)
7979
inline const transt &to_trans_expr(const exprt &expr)
8080
{
8181
PRECONDITION(expr.id() == ID_trans);
82-
DATA_INVARIANT(
83-
expr.operands().size() == 3, "Transition systems must have three operands");
84-
return static_cast<const transt &>(expr);
82+
const transt &ret = static_cast<const transt &>(expr);
83+
validate_expr(ret);
84+
return ret;
8585
}
8686

8787
/// \copydoc to_trans_expr(const exprt &)
8888
inline transt &to_trans_expr(exprt &expr)
8989
{
9090
PRECONDITION(expr.id() == ID_trans);
91-
DATA_INVARIANT(
92-
expr.operands().size() == 3, "Transition systems must have three operands");
93-
return static_cast<transt &>(expr);
91+
transt &ret = static_cast<transt &>(expr);
92+
validate_expr(ret);
93+
return ret;
9494
}
9595

9696
/// \brief Exponentiation
@@ -128,16 +128,18 @@ inline void validate_expr(const power_exprt &value)
128128
inline const power_exprt &to_power_expr(const exprt &expr)
129129
{
130130
PRECONDITION(expr.id() == ID_power);
131-
DATA_INVARIANT(expr.operands().size() == 2, "Power must have two operands");
132-
return static_cast<const power_exprt &>(expr);
131+
const power_exprt &ret = static_cast<const power_exprt &>(expr);
132+
validate_expr(ret);
133+
return ret;
133134
}
134135

135136
/// \copydoc to_power_expr(const exprt &)
136137
inline power_exprt &to_power_expr(exprt &expr)
137138
{
138139
PRECONDITION(expr.id() == ID_power);
139-
DATA_INVARIANT(expr.operands().size() == 2, "Power must have two operands");
140-
return static_cast<power_exprt &>(expr);
140+
power_exprt &ret = static_cast<power_exprt &>(expr);
141+
validate_expr(ret);
142+
return ret;
141143
}
142144

143145
/// \brief Falling factorial power
@@ -175,18 +177,19 @@ inline void validate_expr(const factorial_power_exprt &value)
175177
inline const factorial_power_exprt &to_factorial_power_expr(const exprt &expr)
176178
{
177179
PRECONDITION(expr.id() == ID_factorial_power);
178-
DATA_INVARIANT(
179-
expr.operands().size() == 2, "Factorial power must have two operands");
180-
return static_cast<const factorial_power_exprt &>(expr);
180+
const factorial_power_exprt &ret =
181+
static_cast<const factorial_power_exprt &>(expr);
182+
validate_expr(ret);
183+
return ret;
181184
}
182185

183186
/// \copydoc to_factorial_power_expr(const exprt &)
184187
inline factorial_power_exprt &to_factorial_expr(exprt &expr)
185188
{
186189
PRECONDITION(expr.id() == ID_factorial_power);
187-
DATA_INVARIANT(
188-
expr.operands().size() == 2, "Factorial power must have two operands");
189-
return static_cast<factorial_power_exprt &>(expr);
190+
factorial_power_exprt &ret = static_cast<factorial_power_exprt &>(expr);
191+
validate_expr(ret);
192+
return ret;
190193
}
191194

192195
/// \brief Application of (mathematical) function
@@ -246,18 +249,20 @@ inline const function_application_exprt &
246249
to_function_application_expr(const exprt &expr)
247250
{
248251
PRECONDITION(expr.id() == ID_function_application);
249-
DATA_INVARIANT(
250-
expr.operands().size() == 2, "Function application must have two operands");
251-
return static_cast<const function_application_exprt &>(expr);
252+
const function_application_exprt &ret =
253+
static_cast<const function_application_exprt &>(expr);
254+
validate_expr(ret);
255+
return ret;
252256
}
253257

254258
/// \copydoc to_function_application_expr(const exprt &)
255259
inline function_application_exprt &to_function_application_expr(exprt &expr)
256260
{
257261
PRECONDITION(expr.id() == ID_function_application);
258-
DATA_INVARIANT(
259-
expr.operands().size() == 2, "Function application must have two operands");
260-
return static_cast<function_application_exprt &>(expr);
262+
function_application_exprt &ret =
263+
static_cast<function_application_exprt &>(expr);
264+
validate_expr(ret);
265+
return ret;
261266
}
262267

263268
/// \brief A base class for quantifier expressions
@@ -302,6 +307,8 @@ inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
302307
inline void validate_expr(const quantifier_exprt &value)
303308
{
304309
validate_operands(value, 2, "quantifier expressions must have two operands");
310+
DATA_INVARIANT(
311+
value.op0().id() == ID_symbol, "quantified variable shall be a symbol");
305312
}
306313

307314
/// \brief Cast an exprt to a \ref quantifier_exprt
@@ -312,23 +319,19 @@ inline void validate_expr(const quantifier_exprt &value)
312319
/// \return Object of type \ref quantifier_exprt
313320
inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
314321
{
315-
DATA_INVARIANT(
316-
expr.operands().size() == 2,
317-
"quantifier expressions must have two operands");
318-
DATA_INVARIANT(
319-
expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
320-
return static_cast<const quantifier_exprt &>(expr);
322+
PRECONDITION(can_cast_expr<quantifier_exprt>(expr));
323+
const quantifier_exprt &ret = static_cast<const quantifier_exprt &>(expr);
324+
validate_expr(ret);
325+
return ret;
321326
}
322327

323328
/// \copydoc to_quantifier_expr(const exprt &)
324329
inline quantifier_exprt &to_quantifier_expr(exprt &expr)
325330
{
326-
DATA_INVARIANT(
327-
expr.operands().size() == 2,
328-
"quantifier expressions must have two operands");
329-
DATA_INVARIANT(
330-
expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
331-
return static_cast<quantifier_exprt &>(expr);
331+
PRECONDITION(can_cast_expr<quantifier_exprt>(expr));
332+
quantifier_exprt &ret = static_cast<quantifier_exprt &>(expr);
333+
validate_expr(ret);
334+
return ret;
332335
}
333336

334337
/// \brief A forall expression
@@ -344,19 +347,17 @@ class forall_exprt : public quantifier_exprt
344347
inline const forall_exprt &to_forall_expr(const exprt &expr)
345348
{
346349
PRECONDITION(expr.id() == ID_forall);
347-
DATA_INVARIANT(
348-
expr.operands().size() == 2,
349-
"forall expressions have exactly two operands");
350-
return static_cast<const forall_exprt &>(expr);
350+
const forall_exprt &ret = static_cast<const forall_exprt &>(expr);
351+
validate_expr(static_cast<const quantifier_exprt &>(ret));
352+
return ret;
351353
}
352354

353355
inline forall_exprt &to_forall_expr(exprt &expr)
354356
{
355357
PRECONDITION(expr.id() == ID_forall);
356-
DATA_INVARIANT(
357-
expr.operands().size() == 2,
358-
"forall expressions have exactly two operands");
359-
return static_cast<forall_exprt &>(expr);
358+
forall_exprt &ret = static_cast<forall_exprt &>(expr);
359+
validate_expr(static_cast<const quantifier_exprt &>(ret));
360+
return ret;
360361
}
361362

362363
/// \brief An exists expression
@@ -372,19 +373,17 @@ class exists_exprt : public quantifier_exprt
372373
inline const exists_exprt &to_exists_expr(const exprt &expr)
373374
{
374375
PRECONDITION(expr.id() == ID_exists);
375-
DATA_INVARIANT(
376-
expr.operands().size() == 2,
377-
"exists expressions have exactly two operands");
378-
return static_cast<const exists_exprt &>(expr);
376+
const exists_exprt &ret = static_cast<const exists_exprt &>(expr);
377+
validate_expr(static_cast<const quantifier_exprt &>(ret));
378+
return ret;
379379
}
380380

381381
inline exists_exprt &to_exists_expr(exprt &expr)
382382
{
383383
PRECONDITION(expr.id() == ID_exists);
384-
DATA_INVARIANT(
385-
expr.operands().size() == 2,
386-
"exists expressions have exactly two operands");
387-
return static_cast<exists_exprt &>(expr);
384+
exists_exprt &ret = static_cast<exists_exprt &>(expr);
385+
validate_expr(static_cast<const quantifier_exprt &>(ret));
386+
return ret;
388387
}
389388

390389
#endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H

0 commit comments

Comments
 (0)