Ocaml swiched to immutable strings by default in this version. Cool should
probably be ported to use those, but in the meantime we just disable the feature
to make it build on newer ocaml versions.

bench_one_formula hadn't yet realized that cool has the pgsolver
variant now included.

Instead of a global variable in bench_one_formula.sh

Allows to use `time` on systems where `perf` is not installed.

Since we don't do full game solving at every step, we can gain a lot
of performance by doing simple unsat propagation when a core or state
is determined to be unsatisfiable.

This can now be done with the regular cool script as pgsolver is
available as command line flag.

Attempting to use such an algorithm with intermediate propagation
results in an error.

Allows to specify the exact algorithm after an optional colon in the
'pgsolver' argument for --gameSolver

example:

  coalg.native sat K --gameSolver pgsolver:stratimprloc2

To avoid name clashes with the ocaml minisat library that is used by
pgsolver.

The cool variant that uses pgsolver to solve its games doesn't have to
be a separate binary anymore.

This function is specific to the pgsolver version of the reasoner, so
we now name it as such.

This adds the new command line flag --gameSolver with values "cool"
and "pgsolver" to switch between different game solving
implementations.

Also disables the build of the corresponding executable by
default (can be reenabled with the flat 'benchmarks').

Looks like we misinterpreted the meaning of "local" in pgsolver. It
only calculates the correct solution for the root node, but we
need information about other nodes for intermediate
propagation (on-the-fly game solving).

Now we use a non-local solver, which works but is very slow at the
moment because the game has to be constructed anew every time we
propagate. => We should try to keep the game up-to-date as we expand
nodes, if possible.

This is needed to produce static binaries.

This is needed to produce static binaries.

This reverts commit 5de20a33.

Wrong branch...

Since pgsolver is now a dependency and is not available in common
Linux distributions, we advise people to install all ocaml
dependencies with opam instead.

In this case, no stddev is generated

Otherwise, 'perf stat' returns a zero exit code if mlsolver is killed
by a signal (e.g in case of an OOM situation)

Allows benchmarks of two formula series to be performed in parallel
without interfering with each other.

Some csv tools can only sort lexicographically

who knows if we might need it

This ensures that decimal separators are consistent.

Allows to collect other results than just the time. For example how
many states the game has and what the result was (sat/unsat).