Created page with 'As of version 1.5.1 ProB supports [https://en.wikipedia.org/wiki/Common_subexpression_elimination common subexpression elimination (CSE)]. To enable it you need to set the advan…' |
No edit summary |
||
| Line 2: | Line 2: | ||
To enable it you need to set the advanced preference <tt>CSE</tt> to true (this can be done using the switch <tt>-p CSE TRUE</tt> when using the [[Using_the_Command-Line_Version_of_ProB|command-line version probcli]] or using the Advanced Preferences command in ProB Tcl/Tk). | To enable it you need to set the advanced preference <tt>CSE</tt> to true (this can be done using the switch <tt>-p CSE TRUE</tt> when using the [[Using_the_Command-Line_Version_of_ProB|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. | |||
Similarly, 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)) | |||
To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> to true. | |||
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. Similarly, 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))
To enable CSE also inside substitutions (aka B statements) you need to set the preference CSE_SUBST to true.