- May 02, 2019
-
-
Hans-Peter Deifel authored
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.
-
- Jan 12, 2018
-
-
Hans-Peter Deifel authored
bench_one_formula hadn't yet realized that cool has the pgsolver variant now included.
-
Hans-Peter Deifel authored
Instead of a global variable in bench_one_formula.sh
-
Hans-Peter Deifel authored
Allows to use `time` on systems where `perf` is not installed.
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
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.
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
This can now be done with the regular cool script as pgsolver is available as command line flag.
-
Hans-Peter Deifel authored
Attempting to use such an algorithm with intermediate propagation results in an error.
-
Hans-Peter Deifel authored
Allows to specify the exact algorithm after an optional colon in the 'pgsolver' argument for --gameSolver example: coalg.native sat K --gameSolver pgsolver:stratimprloc2
-
Hans-Peter Deifel authored
To avoid name clashes with the ocaml minisat library that is used by pgsolver.
-
- Jan 11, 2018
-
-
Hans-Peter Deifel authored
The cool variant that uses pgsolver to solve its games doesn't have to be a separate binary anymore.
-
- Nov 28, 2017
-
-
Hans-Peter Deifel authored
This function is specific to the pgsolver version of the reasoner, so we now name it as such.
-
- Nov 27, 2017
-
-
Hans-Peter Deifel authored
This adds the new command line flag --gameSolver with values "cool" and "pgsolver" to switch between different game solving implementations.
-
- Nov 24, 2017
-
-
Hans-Peter Deifel authored
-
- Nov 16, 2017
-
-
Hans-Peter Deifel authored
Also disables the build of the corresponding executable by default (can be reenabled with the flat 'benchmarks').
-
- Nov 11, 2017
-
-
Hans-Peter Deifel authored
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.
-
- Nov 09, 2017
-
-
Hans-Peter Deifel authored
This is needed to produce static binaries.
-
- Nov 07, 2017
-
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
This is needed to produce static binaries.
-
- Nov 02, 2017
-
-
Hans-Peter Deifel authored
This reverts commit 5de20a33. Wrong branch...
-
Hans-Peter Deifel authored
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.
-
Hans-Peter Deifel authored
In this case, no stddev is generated
-
- Oct 20, 2017
-
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
- Oct 19, 2017
-
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
Otherwise, 'perf stat' returns a zero exit code if mlsolver is killed by a signal (e.g in case of an OOM situation)
-
Hans-Peter Deifel authored
Allows benchmarks of two formula series to be performed in parallel without interfering with each other.
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
Some csv tools can only sort lexicographically
-
Hans-Peter Deifel authored
who knows if we might need it
-
Hans-Peter Deifel authored
This ensures that decimal separators are consistent.
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
Allows to collect other results than just the time. For example how many states the game has and what the result was (sat/unsat).
-