Common Subexpression Elimination

Revision as of 08:02, 12 July 2015 by Michael Leuschel (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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

Basics of 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.

Substitutions

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).

Sharing Predicates

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)

Other Preferences

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).

Tips

To inspect the effect of CSE, you do one of the following:

  • In ProB Tcl/Tk you can use the command "Show Internal Representation" in the Debug menu to inspect the effect of CSE on your machine
  • For probcli, you can use the command -pp FILE to write the pretty-printed internal representation of your machine after CSE to a file
  • For the REPL of probcli (command -repl), you can use the option -p REPL_UNICODE TRUE to force ProB to print your expressions/predicates after CSE processing (using Unicode characters)