Link ncurses bindings against libtinfo and libgpm
This is needed to produce static binaries.
Remove pgsolver dependency
Use pgsolver from opam instead of bundling it
Simplifies the installation process and allows to compare performancewith other tools that use the same pgsolver version.
Move aconjunctive formula generator to benchmarks/
oasis: Correctly declare TCSLib dependency for pgsolver
Add script to generate test formulas
- gen.ml: Generates a specific set of formulas, usable for benchmarking cool against pgsolver
Modularize reasoner by focus tracking strategy
Only iterate through open states in PG solution
Solve game twice to accommodate for partial games
Import pgsolver as git submodule
A parity game solver that will be used to solve games arising from thefull mu-calculus.
- Adds a new submodule under `vendor/` for pgsolver. Linking without including it in the source proved difficult at the moment.- Adds a new library `libpgsolver` to _oasis that contains the files...
tests: Add unit tests
Adds a whole new set of tests that don't just test the whole reasoningprocess on a formula, but smaller individual functions.
Right now there are only two tests but more should follow.
build: Add testsuite to oasis
Enables 'make test' and 'ocaml setup.ml -test' to run the testsuite.
build: Use new Makefile as generated by oasis
Adds many new targets including 'test' and 'distclean'
Add comment on purpose of glpk_stub to various files
Remove libbdd and libglpk from C linker command
Now that GMLMIP is removed, those are not needed any more. Now coolcan really be built without GMLMIPs dependencies (as is now advertisedby the INSTALL file).
Enable documentation generation in oasis
Documentation can be built with: ocaml setup.ml -doc
This also fixes two documentation comments that had the wrong syntax.
Merge branch 'remove-gmlmip'
This drops the rule implementation for GML and PML, because they wererelying on GMLMIP which complicated the build process and didn't workcompletely. See Issue 19.
GML and PML are still implemented as functors but currently disabled.To re-instantiate them, an OCaml implementation is needed.
Add emacs mode lines to various files
Fix static linking
Add basic debugging repl
Implement raw syntax for constant functors
Add curses painting basics
Add basic curses and readline bindings
Disable glpk_stub.c until we do not need GMLMIP anymore
Port glpk_stub.c to GLPK 4.54 and add it to _oasis
Some options and functions are still missing, e.g. MILP support
Implement parsing of complex functors
Add basic testsuite skeleton
Make if conditions in _oasis more conform
Explicitly name all internal moduls
Compile entiere GMLMIP-0.1 into cool
Move more cpp to c
Use -cc g++ everywhere in oasis file
Add build flat for static linking
Add coalgcompare frontend
Add OWL frontend
Improve _oasis file
Separate cool into library and coalg frontend
Minor _oasis file cleanups
Make coalg build with oasis
Make c++ sources compile with oasis
Add first not-yet-working _oasis