alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[lbtt]

Browse source 
Fix generation of random formulae on 64bits systems.

* src/main.cc (testLoop): Generate random short ints between 0 and
SHRT_MAX, not between 0 and LONG_MAX.  On systems where long ints
are 64bits, LRAND(0,LONG_MAX) was returning a value with the lower
32 bits set to 0, and the latter truncation to short int always
yielded the value 0.  Consequently all generated formulae were
identical...
This commit is contained in:
Alexandre Duret-Lutz 2009-11-26 15:51:01 +01:00
parent c95eb21ecf
commit 3cbd681c6d
2 changed files with 20 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

11
lbtt/ChangeLog
View file

@ -1,3 +1,14 @@
2009-11-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix generation of random formulae on 64bits systems.
* src/main.cc (testLoop): Generate random short ints between 0 and
SHRT_MAX, not between 0 and LONG_MAX. On systems where long ints
are 64bits, LRAND(0,LONG_MAX) was returning a value with the lower
32 bits set to 0, and the latter truncation to short int always
yielded the value 0. Consequently all generated formulae were
identical...
2009-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/Configuration.cc (registerAlgorithm): Do not complain about

18
lbtt/src/main.cc
View file

@ -325,11 +325,11 @@ bool testLoop()
SRAND(configuration.global_options.statespace_random_seed);
for (int i = 0; i < 3; i++)
statespace_random_state[i] = static_cast<short int>(LRAND(0, LONG_MAX));
statespace_random_state[i] = static_cast<short int>(LRAND(0, SHRT_MAX));
SRAND(configuration.global_options.formula_random_seed);
for (int i = 0; i < 3; i++)
formula_random_state[i] = static_cast<short int>(LRAND(0, LONG_MAX));
formula_random_state[i] = static_cast<short int>(LRAND(0, SHRT_MAX));
#endif /* HAVE_RAND48 */
/*
@ -367,7 +367,7 @@ bool testLoop()
round_info.error = false;
round_info.skip
= (round_info.current_round < round_info.next_round_to_run);
if (!round_info.skip)
printText(string("Round ") + toString(round_info.current_round)
+ " of " + toString(global_options.number_of_rounds) + "\n\n",
@ -390,13 +390,13 @@ bool testLoop()
seed48(statespace_random_state);
for (int i = 0; i < 3; i++)
statespace_random_state[i] = static_cast<short int>
(LRAND(0, LONG_MAX));
(LRAND(0, SHRT_MAX));
#else
SRAND(global_options.statespace_random_seed);
configuration.global_options.statespace_random_seed
= LRAND(0, RAND_MAX);
#endif /* HAVE_RAND48 */
if (global_options.statespace_change_interval == 0)
round_info.next_round_to_change_statespace
= global_options.number_of_rounds + 1;
@ -434,7 +434,7 @@ bool testLoop()
*/
round_info.fresh_formula
= (round_info.next_round_to_change_formula
= (round_info.next_round_to_change_formula
== round_info.current_round);
if (round_info.fresh_formula)
@ -442,7 +442,7 @@ bool testLoop()
#ifdef HAVE_RAND48
seed48(formula_random_state);
for (int i = 0; i < 3; i++)
formula_random_state[i] = static_cast<short int>(LRAND(0, LONG_MAX));
formula_random_state[i] = static_cast<short int>(LRAND(0, SHRT_MAX));
#else
SRAND(global_options.formula_random_seed);
configuration.global_options.formula_random_seed = LRAND(0, RAND_MAX);
@ -743,7 +743,7 @@ bool testLoop()
int main(int argc, char* argv[])
{
try
try
{
configuration.read(argc, argv);
}
@ -792,7 +792,7 @@ int main(int argc, char* argv[])
using_history();
#endif /* HAVE_READLINE */
try
try
{
allocateTempFilenames();
if (!testLoop())