Previously, cool would simply raise an exception if the formula was
not aconjunctive. This was done to ease testing of the new reasoner
algorithm.

Now, the reasoner decides whether the formula is aconjunctive or not
and uses a specific algorithm based on the result.

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

This fails currently, because the check for aconjunctivity is
currently hard coded, ruling out all formulas that aren't
aconjunctive.

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

For the aconjunctive fragment, we replace the generation of a single
core with all tracked deferrals by the generation of multiple cores,
each annotated with a single deferral from the above set.

0 and 1 are used for Sat and Unsat respectively. But if the child
throws an exception, another exit status is returned which the parent
now recognizes.

As it stands, cool leaks tons of memory with each `isSat` call. Until
this is fixed, the new `--slow` testsuite would need at least 16GB of
memory if all formulas are decided in one process. Thus, we now call
isSat in a new child-process and allow the OS to reclaim memory after
the child exits.

NB: This uses the Unix.fork API, which is not available on Windows.

This imports some of the quickly decidable ctl comparision benchmark
formulas into the test suite.

The testsuite also gained a --slow parameter, that enables slower (but
still fairly fast) formulas.

Now that GMLMIP is removed, those are not needed any more. Now cool
can really be built without GMLMIPs dependencies (as is now advertised
by the INSTALL file).

Documentation can be built with: ocaml setup.ml -doc

This also fixes two documentation comments that had the wrong syntax.

The 'step' command takes an optional repeat count. Now it stops
stepping and prints the result if the reasoner finishes before
reaching the specified number of steps.

- Use more readable colors and proper spacing
- Differentiate between cores and states by shape
- Add a legend
- Teach debugger to optionally write graph to file instead of stdout

This is easier to type with a standard compose key as opposed as the
arguably more correct "Greek Small Letter Mu".

Otherwise, the debugger would report the reasoner result to be "Sat"
when it should really be "Unsat".

Also shows the correct binary name in the usage output.

- Show a prompt before each input.
- Don't die if the verification of a formula fails. Show an error
  instead and accept the next input.

It's not needed any more

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.

This fixes the warning "the label idx is defined in both types state
and core." by renaming the label to idxS and idxC respectively.

This is generated by the editor completion framework called merlin:
https://github.com/ocaml/merlin

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.