Array.exists is only available since OCaml 4.03.0 and we need to
support version at least version 4.02.3.

This drops the rule implementation for GML and PML, because they were
relying on GMLMIP which complicated the build process and didn't work
completely. See Issue 19.

GML and PML are still implemented as functors but currently disabled.
To re-instantiate them, an OCaml implementation is needed.

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

Fixes the syntax of all tests that use R and B as identifiers, which
are keywords now.

Also disables all tests involving nominals as they are currently all
throwing exceptions.

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