Common Subexpression Elimination - Revision history

Michael Leuschel at 07:02, 12 July 2015

2015-07-12T07:02:19Z

← Older revision		Revision as of 07:02, 12 July 2015
Line 1:		Line 1:
	As of version 1.5.1 ProB supports [https://en.wikipedia.org/wiki/Common_subexpression_elimination common subexpression elimination (CSE)].		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 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).		== Basics of CSE ==
			To enable CSE 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		With CSE enabled, ProB will translate the predicate
	x:dom(f(a)) & r=f(a)(x)		x:dom(f(a)) & r=f(a)(x)

Michael Leuschel: /* Tips */

2015-07-12T07:01:25Z

Tips

← Older revision		Revision as of 07:01, 12 July 2015
Line 44:		Line 44:
	== Tips ==		== Tips ==
	To inspect the effect of CSE, you do one of the following:		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		* 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 <tt>-pp FILE</tt> to write the pretty-printed internal representation of your machine after CSE to a file		* For probcli, you can use the command <tt>-pp FILE</tt> 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 <tt>-p REPL_UNICODE TRUE</tt> to force ProB to print your expressions/predicates after CSE processing (using Unicode characters)		* For the REPL of probcli (command -repl), you can use the option <tt>-p REPL_UNICODE TRUE</tt> to force ProB to print your expressions/predicates after CSE processing (using Unicode characters)

Michael Leuschel at 07:01, 12 July 2015

2015-07-12T07:01:07Z

← Older revision		Revision as of 07:01, 12 July 2015
Line 41:		Line 41:
	and ProB will find the solution <tt>x=4</tt>.		and ProB will find the solution <tt>x=4</tt>.
	With <tt>CSE_WD_ONLY</tt> to <tt>TRUE</tt>, the predicate will be left unchanged (and ProB will find the same solution).		With <tt>CSE_WD_ONLY</tt> to <tt>TRUE</tt>, 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 <tt>-pp FILE</tt> 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 <tt>-p REPL_UNICODE TRUE</tt> to force ProB to print your expressions/predicates after CSE processing (using Unicode characters)

Michael Leuschel: /* Sharing Predicates */

2015-06-30T06:25:18Z

Sharing Predicates

← Older revision		Revision as of 06:25, 30 June 2015
Line 31:		Line 31:
	After setting <tt>CSE_PRED</tt> to <tt>FALSE</tt>, this will be translated into:		After setting <tt>CSE_PRED</tt> to <tt>FALSE</tt>, this will be translated into:
	LET @0==(x + 1) IN @0 > 10 & (@0 > 10 => y = 22)		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 <tt>CSE_WD_ONLY</tt> to <tt>TRUE</tt>.
			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 <tt>x=4</tt>.
			With <tt>CSE_WD_ONLY</tt> to <tt>TRUE</tt>, the predicate will be left unchanged (and ProB will find the same solution).

Michael Leuschel: /* Substitutions */

2015-06-30T05:46:35Z

Substitutions

← Older revision		Revision as of 05:46, 30 June 2015
Line 20:		Line 20:
	== Substitutions ==		== Substitutions ==
	To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> to true.		To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> 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 <tt>CSE_PRED</tt> to <tt>FALSE</tt>.
			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 <tt>CSE_PRED</tt> to <tt>FALSE</tt>, this will be translated into:
			LET @0==(x + 1) IN @0 > 10 & (@0 > 10 => y = 22)

Michael Leuschel at 05:34, 30 June 2015

2015-06-30T05:34:02Z

← Older revision		Revision as of 05:34, 30 June 2015
Line 16:		Line 16:
	For example, in		For example, in
	LET @1==f(a) IN 2>3 & @1+@1>10		LET @1==f(a) IN 2>3 & @1+@1>10
	the expression <tt>f(a)</tt> will never be evaluated. This is important for well-definedness and for performance.		the expression <tt>f(a)</tt> 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 ==		== Substitutions ==
	To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> to true.		To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> to true.

Michael Leuschel at 05:33, 30 June 2015

2015-06-30T05:33:26Z

← Older revision		Revision as of 05:33, 30 June 2015
Line 13:		Line 13:

	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.		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.		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 ~~<tt>~~LET @1==f(a) IN 2>3 & @1+@1>10~~</tt>,~~ the expression <tt>f(a)</tt> will never be evaluated. This is important for well-definedness and for performance.		For example, in
			LET @1==f(a) IN 2>3 & @1+@1>10
			the expression <tt>f(a)</tt> will never be evaluated. This is important for well-definedness and for performance.

	== Substitutions ==		== Substitutions ==
	To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> to true.		To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> to true.

Michael Leuschel at 05:32, 30 June 2015

2015-06-30T05:32:21Z

← Older revision		Revision as of 05:32, 30 June 2015
Line 6:		Line 6:
	into		into
	(LET @0==(f(a)) IN x ∈ dom(@0) ∧ r = @0(x))		(LET @0==(f(a)) IN x ∈ dom(@0) ∧ r = @0(x))
	before evaluating it.		before evaluating it. As you can see, the common sub-expression <tt>f(a)</tt> has been lifted into a LET statement. This has the advantage that the expression <tt>f(a)</tt> will only get evaluated once (rather than twice, in case <tt>x:dom(f(a))</tt>). Identifiers introduced by the CSE always start with the @-sign.
	~~Similarly~~, the predicate		As another example, the predicate
	xx+2x > yyy & yyy > xx+2x		xx+2x > yyy & yyy > xx+2x
	gets translated into		gets translated into
	LET @2==(xx+2x) IN (LET @4==((yy)y) IN @2 > @4 & @4 > @2))		LET @2==(xx+2x) IN (LET @4==((yy)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 <tt>LET @1==f(a) IN 2>3 & @1+@1>10</tt>, the expression <tt>f(a)</tt> will never be evaluated. This is important for well-definedness and for performance.

			== Substitutions ==
	To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> to true.		To enable CSE also inside substitutions (aka B statements) you need to set the preference <tt>CSE_SUBST</tt> to true.

Michael Leuschel at 17:40, 29 June 2015

2015-06-29T17:40:23Z

← Older revision		Revision as of 17:40, 29 June 2015
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
			xx+2x > yyy & yyy > xx+2x
			gets translated into
			LET @2==(xx+2x) IN (LET @4==((yy)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.

Michael Leuschel: 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…'

2015-06-29T17:35:31Z

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…'

New page

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