Common Subexpression Elimination

As of version 1.5.1 ProB supports common subexpression elimination (CSE).

To enable it you need to set the advanced preference CSE to true (this can be done using the switch -p CSE TRUE when using the command-line version probcli or using the Advanced Preferences command in ProB Tcl/Tk). With CSE enabled, ProB will translate the predicate

x:dom(f(a)) & r=f(a)(x)

into

(LET @0==(f(a)) IN x ∈ dom(@0) ∧ r = @0(x))

before evaluating it. As you can see, the common sub-expression f(a) has been lifted into a LET statement. This has the advantage that the expression f(a) will only get evaluated once (rather than twice, in case x:dom(f(a))). Identifiers introduced by the CSE always start with the @-sign. As another example, the predicate

x*x+2*x > y*y*y & y*y*y > x*x+2*x

gets translated into

LET @2==(x*x+2*x) IN (LET @4==((y*y)*y) IN @2 > @4 & @4 > @2))

You may observe that the B-language does not have a let-construct for expression nor predicates (only for substitutions). There are various ways one can overcome this (e.g., using an existential quantifier for a predicate), but ProB adds its own LET-construct to the language in the interpreter. Moreover, to avoid issues with well-definedness and ensuring that ProB only evaluates the LET expressions when really needed, this LET has a different behaviour than the "standard" constructs. Indeed, ProB's LET is lazy, i.e., it will only evaluate the expression when required by the computation of the body of the LET. For example, in

LET @1==f(a) IN 2>3 & @1+@1>10

the expression f(a) will never be evaluated. This is important for well-definedness (e.g., suppose a is not in the domain of f) and for performance.

Substitutions

To enable CSE also inside substitutions (aka B statements) you need to set the preference CSE_SUBST to true.