Hans-Peter Deifel authored 8 years ago and Hans-Peter Deifel committed 8 years ago

R and B are now keywords and were used as identifiers. Now, r and
b (lowercase) is used instead in the testcases. For consistency, all
other identifiers were lowercased, too.

Hans-Peter Deifel authored 8 years ago and Hans-Peter Deifel committed 8 years ago

The CAMLparam0() macro must be invoked at the beginning of a function
that has local variables.

Makes them not only intended alt-free but also parsed to something alt-free

We want to still have the solver for naive unsat propagation

The satsolver is reatined and only updated with new clauses for every
state that is generated out of a core. Once the core becomes Open (as
opposed to expandable), the solver is no longer needed.

This patch makes the solver a `Solver option` and gets it deallocated
once no longer needed and resets the hashtable (makes it empty and zero
size) to save memory. This saves about 60% memory usage on some extreme
cases (e.g. exp_unsat from the CTL Benchmark set)

Instead of some calculation based of finishing on normal Cores really
count proper Open States