Memoization for Functions - Revision history

Michael Leuschel at 06:43, 24 May 2019

2019-05-24T06:43:18Z

@@ Line 79: / Line 79: @@
 MemoID 6 (M91) : Values Stored: 111 (15 ms to compute), Reused 295
 Hashes computed: 1002, expansions reused: 0
 Memoization functions registered: 6, results reused: 1345
 </pre>

Michael Leuschel at 06:40, 24 May 2019

2019-05-24T06:40:42Z

← Older revision		Revision as of 06:40, 24 May 2019
Line 66:		Line 66:
	</pre>		</pre>

	If the compile time flag <tt>-Dprob_profile=true</tt> is set, the output is more ~~detaild~~:		If the compile time flag <tt>-Dprob_profile=true</tt> is set, the output is more detailed:

	<pre>		<pre>

Michael Leuschel at 06:40, 24 May 2019

2019-05-24T06:40:30Z

← Older revision		Revision as of 06:40, 24 May 2019
Line 49:		Line 49:
	<pre>		<pre>
	--------------------------		--------------------------
	ProB profile info after ~~29290~~ ms walltime (~~7849~~ ms runtime)		ProB profile info after 9670 ms walltime (7217 ms runtime)
	No source profiling information available		No source profiling information available
	Recompile ProB with -Dprob_src_profile=true		Recompile ProB with -Dprob_src_profile=true
Line 56:		Line 56:
	MEMO Table:		MEMO Table:
	Summary of reuse per memoization ID:		Summary of reuse per memoization ID:
	MemoID 1 (prime) : Values Stored: 999 (0 ms to compute), Reused ?		MemoID 1 (prime) : Values Stored: 999 (? ms to compute), Reused ?
	MemoID 2 (fib) : Values Stored: 31 (0 ms to compute), Reused ?		MemoID 2 (fib) : Values Stored: 31 (? ms to compute), Reused ?
	MemoID 3 (fact) : Values Stored: 11 (0 ms to compute), Reused ?		MemoID 3 (fact) : Values Stored: 11 (? ms to compute), Reused ?
	MemoID 4 (evenupto) : Values Stored: 0 (0 ms to compute), Reused ?		MemoID 4 (evenupto) : Values Stored: 0 (? ms to compute), Reused ?
	MemoID 5 (sum) : Values Stored: 1001 (0 ms to compute), Reused ?		MemoID 5 (sum) : Values Stored: 1001 (? ms to compute), Reused ?
	MemoID 6 (M91) : Values Stored: 111 (0 ms to compute), Reused ?		MemoID 6 (M91) : Values Stored: 111 (? ms to compute), Reused ?
	Hashes computed: 1002, expansions reused: 0		Hashes computed: 1002, expansions reused: 0
	Memoization functions registered: 6, results reused: 1345		Memoization functions registered: 6, results reused: 1345
Line 69:		Line 69:

	<pre>		<pre>
			...
	MEMO Table:		MEMO Table:
	Summary of reuse per memoization ID:		Summary of reuse per memoization ID:

Michael Leuschel at 06:34, 24 May 2019

2019-05-24T06:34:32Z

← Older revision		Revision as of 06:34, 24 May 2019
Line 45:		Line 45:


	With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization.		With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization. An example output is the following one:

			<pre>
			--------------------------
			ProB profile info after 29290 ms walltime (7849 ms runtime)
			No source profiling information available
			Recompile ProB with -Dprob_src_profile=true
			No profiling information available
			Recompile ProB with -Dprob_profile=true
			MEMO Table:
			Summary of reuse per memoization ID:
			MemoID 1 (prime) : Values Stored: 999 (0 ms to compute), Reused ?
			MemoID 2 (fib) : Values Stored: 31 (0 ms to compute), Reused ?
			MemoID 3 (fact) : Values Stored: 11 (0 ms to compute), Reused ?
			MemoID 4 (evenupto) : Values Stored: 0 (0 ms to compute), Reused ?
			MemoID 5 (sum) : Values Stored: 1001 (0 ms to compute), Reused ?
			MemoID 6 (M91) : Values Stored: 111 (0 ms to compute), Reused ?
			Hashes computed: 1002, expansions reused: 0
			Memoization functions registered: 6, results reused: 1345
			</pre>

			If the compile time flag <tt>-Dprob_profile=true</tt> is set, the output is more detaild:

			<pre>
			MEMO Table:
			Summary of reuse per memoization ID:
			MemoID 1 (prime) : Values Stored: 999 (336 ms to compute), Reused 1003
			MemoID 2 (fib) : Values Stored: 31 (20 ms to compute), Reused 45
			MemoID 3 (fact) : Values Stored: 11 (10 ms to compute), Reused 1
			MemoID 4 (evenupto) : Values Stored: 0 (0 ms to compute), Reused 0
			MemoID 5 (sum) : Values Stored: 1001 (16659 ms to compute), Reused 1
			MemoID 6 (M91) : Values Stored: 111 (15 ms to compute), Reused 295
			Hashes computed: 1002, expansions reused: 0
			Memoization functions registered: 6, results reused: 1345
			</pre>

Michael Leuschel at 16:22, 9 May 2019

2019-05-09T16:22:56Z

← Older revision		Revision as of 16:22, 9 May 2019
Line 23:		Line 23:
	fib(30)=1346269;		fib(30)=1346269;
	fib[28..30] = {514229,832040,1346269};		fib[28..30] = {514229,832040,1346269};
	30\|->1346269 : fib;		30\|->1346269 : fib;
	30\|->1346268 /: fib;		30\|->1346268 /: fib;
	{x\| 30\|->x:fib} = {1346269};		{x\| 30\|->x:fib} = {1346269};
	END		END

Michael Leuschel at 16:22, 9 May 2019

2019-05-09T16:22:38Z

← Older revision		Revision as of 16:22, 9 May 2019
Line 23:		Line 23:
	fib(30)=1346269;		fib(30)=1346269;
	fib[28..30] = {514229,832040,1346269};		fib[28..30] = {514229,832040,1346269};
			30\|->1346269 : fib;
			30\|->1346268 /: fib;
			{x\| 30\|->x:fib} = {1346269};
	END		END

Line 32:		Line 35:
	* computation of relational image such as fib[28..30], which internally results in three function calls to fib		* computation of relational image such as fib[28..30], which internally results in three function calls to fib
	* membership predicates of the form x\|->y:fib, where x is a known value		* membership predicates of the form x\|->y:fib, where x is a known value
			* non-membership predicates of the form x\|->y/:fib, where x is a known value

	The following points are relevant:		The following points are relevant:

Michael Leuschel at 15:14, 9 May 2019

2019-05-09T15:14:33Z

← Older revision		Revision as of 15:14, 9 May 2019
Line 31:		Line 31:
	* function calls such as fib(30) (which in turn calls fib(29) and fib(28) which are also memoized)		* function calls such as fib(30) (which in turn calls fib(29) and fib(28) which are also memoized)
	* computation of relational image such as fib[28..30], which internally results in three function calls to fib		* computation of relational image such as fib[28..30], which internally results in three function calls to fib
			* membership predicates of the form x\|->y:fib, where x is a known value

	The following points are relevant:		The following points are relevant:
	* Memoization is currently only possible for functions declared in the ABSTRACT_CONSTANTS section		* Memoization is currently only possible for functions declared in the ABSTRACT_CONSTANTS section
	* Memoization means that all results of function calls are stored. The memoization table is reset when another B machine is loaded or the same B machine is re-loaded.		* Memoization means that all results of function calls are stored. The memoization table is reset when another B machine is loaded or the same B machine is re-loaded.
	* Memoized functions are ~~automatically marked as~~ symbolic. If your function is finite and relatively small, it may be better to put the function into the CONCRETE_CONSTANTS section so that it gets computed in its entirety once.		* Memoized functions are often treated in a similar way to symbolic functions. If your function is finite and relatively small, it may be better to put the function into the CONCRETE_CONSTANTS section so that it gets computed in its entirety once.
	* Memoization of a function f is currently <b>not</b> active for computations such as dom(f), ran(f) or ~~x\|->y:f~~.		* Memoization of a function f is currently <b>not</b> active for computations such as dom(f).
			* If a predicate requires the computation of the full function, e.g., ran(f), then the results will be stored and will be available for future function calls or in case the full value is needed again.


	With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization.		With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization.

Michael Leuschel at 10:45, 7 May 2019

2019-05-07T10:45:05Z

← Older revision		Revision as of 10:45, 7 May 2019
Line 36:		Line 36:
	* Memoization means that all results of function calls are stored. The memoization table is reset when another B machine is loaded or the same B machine is re-loaded.		* Memoization means that all results of function calls are stored. The memoization table is reset when another B machine is loaded or the same B machine is re-loaded.
	* Memoized functions are automatically marked as symbolic. If your function is finite and relatively small, it may be better to put the function into the CONCRETE_CONSTANTS section so that it gets computed in its entirety once.		* Memoized functions are automatically marked as symbolic. If your function is finite and relatively small, it may be better to put the function into the CONCRETE_CONSTANTS section so that it gets computed in its entirety once.
	* Memoization of a function f is currently not active for computations such as dom(f), ran(f).		* Memoization of a function f is currently <b>not</b> active for computations such as dom(f), ran(f) or x\|->y:f.


	With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization.		With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization.

Michael Leuschel at 10:40, 7 May 2019

2019-05-07T10:40:29Z

← Older revision		Revision as of 10:40, 7 May 2019
Line 22:		Line 22:
	ASSERTIONS		ASSERTIONS
	fib(30)=1346269;		fib(30)=1346269;
			fib[28..30] = {514229,832040,1346269};
	END		END

	Memoization means that the recursive Fibonacci function now runs in linear time rather than in exponential time.		Memoization means that the recursive Fibonacci function now runs in linear time rather than in exponential time.
	Generally, memoization is useful for functions which are complex to compute but which are called repeatedly with the same arguments.		Generally, memoization is useful for functions which are complex to compute but which are called repeatedly with the same arguments.

			As can be seen above, memoization is active for
			* function calls such as fib(30) (which in turn calls fib(29) and fib(28) which are also memoized)
			* computation of relational image such as fib[28..30], which internally results in three function calls to fib

			The following points are relevant:
			* Memoization is currently only possible for functions declared in the ABSTRACT_CONSTANTS section
			* Memoization means that all results of function calls are stored. The memoization table is reset when another B machine is loaded or the same B machine is re-loaded.
			* Memoized functions are automatically marked as symbolic. If your function is finite and relatively small, it may be better to put the function into the CONCRETE_CONSTANTS section so that it gets computed in its entirety once.
			* Memoization of a function f is currently not active for computations such as dom(f), ran(f).


	With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization.		With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization.

Michael Leuschel at 10:06, 16 April 2019

2019-04-16T10:06:27Z

← Older revision		Revision as of 10:06, 16 April 2019
Line 26:		Line 26:
	Memoization means that the recursive Fibonacci function now runs in linear time rather than in exponential time.		Memoization means that the recursive Fibonacci function now runs in linear time rather than in exponential time.
	Generally, memoization is useful for functions which are complex to compute but which are called repeatedly with the same arguments.		Generally, memoization is useful for functions which are complex to compute but which are called repeatedly with the same arguments.


			With the command-line version probcli you can use the <tt>-profile</tt> command to obtain some statistics about memoization.