As of version 1.5.1 ProB supports common subexpression elimination (CSE).
To enable CSE 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.
To enable CSE also inside substitutions (aka B statements) you need to set the preference CSE_SUBST to true. By default, the CSE will only be applied to top-level predicates, such as the invariant, the assertions, the properties or individual predicates inside operations (but not the operation as a whole).
By default ProB's CSE will also share predicates. You can turn off CSE for predicates, i.e., only expressions get shared, by setting the preference CSE_PRED to FALSE. For example, by default ProB's CSE will translate
x+1 > 10 & (x+1 > 10 => y=22)
into
LET @1==(x + 1 > 10) IN @1 & (@1 => y = 22)
After setting CSE_PRED to FALSE, this will be translated into:
LET @0==(x + 1) IN @0 > 10 & (@0 > 10 => y = 22)
ProB will also share expressions which are potentially not well-defined, and takes extra care with those expressions (in particular in the context of set comprehensions and quantifications). However, you can completely turn off sharing of potentially not-well defined expressions by setting the preference CSE_WD_ONLY to TRUE. For example, by default the following predicate
x>1 & 100/x > 20 & 100/x <26
will get translate into
LET @0==(100 / x) IN (x > 1 & @0 > 20) & @0 < 26)
and ProB will find the solution x=4. With CSE_WD_ONLY to TRUE, the predicate will be left unchanged (and ProB will find the same solution).
To inspect the effect of CSE, you do one of the following: