Project

General

Profile

Statistics
| Branch: | Revision:

cool / INSTALL @ master

History | View | Annotate | Download (2.15 KB)

1 2bda8737 Hans-Peter Deifel
// -*- mode: adoc; fill-column: 80; -*-
2 7625cc6d Thorsten Wißmann
cool solver installation notes
3
==============================
4
5
Dependencies
6
------------
7
Install ocaml include files, minisat include files. Place them in the include
8 2340c194 Thorsten Wißmann
directory (e.g. /usr/include, /usr/lib/ocaml, or .).
9 7625cc6d Thorsten Wißmann
10 6fad6e7e Thorsten Wißmann
Dependencies:
11
12 2340c194 Thorsten Wißmann
  - oasis (only needed if there is no setup.ml, e.g. when building from git)
13 6fad6e7e Thorsten Wißmann
  - ocamlfind (package called ocaml-findlib)
14
  - ocamlgraph (package ocaml-ocamlgraph)
15 69a71d22 Thorsten Wißmann
  - readline
16
  - minisat (at least minisat 2)
17 e034e268 Thorsten Wißmann
18 f05f5d4c Christoph Egger
On Debian or Ubuntu, install the following packages:
19 69a71d22 Thorsten Wißmann
20
  - git
21
  - build-essential
22
  - oasis
23
  - libocamlgraph-ocaml-dev
24
  - libreadline-dev
25 f60698a6 Christoph Egger
  - minisat
26 69a71d22 Thorsten Wißmann
27 6fad6e7e Thorsten Wißmann
28 7625cc6d Thorsten Wißmann
Build
29
-----
30 2340c194 Thorsten Wißmann
In case there is no setup.ml yet, create it with oasis:
31 7625cc6d Thorsten Wißmann
32 2340c194 Thorsten Wißmann
    oasis setup
33 07c21167 Thorsten Wißmann
34 c49eea11 Thorsten Wißmann
35
In particular, if you have cloned cool via git, then you will need
36
to create setup.ml using the command above.
37
38 2340c194 Thorsten Wißmann
Then compile it:
39
40
    ocaml setup.ml -configure
41
    ocaml setup.ml -build
42
43 c49eea11 Thorsten Wißmann
(There will be some warnings.)
44
45 2340c194 Thorsten Wißmann
Now you have a freshly built coalg.native in the toplevel directory.
46 7625cc6d Thorsten Wißmann
47 cac42fce Thorsten Wißmann
If you want the executables statically linked, then run the configure step with
48
the flag --enable-static.
49
50 69a71d22 Thorsten Wißmann
Verbose manual installation tutorial of the git version
51
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
52
Install the packaged dependencies (see above). Install minisat, e.g. manually
53
via git:
54
55
  git clone TODO
56
  make config prefix=/usr/local
57
  sudo make install
58
59
Clone the cool git repository via
60
61
    TODO
62
    cd cool
63
64
And build
65
66
    oasis setup.ml
67
    ocaml setup.ml -configure
68
    ocaml setup.ml -build
69
70 7625cc6d Thorsten Wißmann
Installation
71
------------
72
Not possible yet.
73
74 f1fa9ad5 Thorsten Wißmann
Benchmarking
75
------------
76
You should remove the debug flag (-g) from the Makefile and recompile before
77
doing time measurements.
78
79 0dfb55b5 Thorsten Wißmann
Examples
80
--------
81
82 233d5f2b Thorsten Wißmann
To see a longer list of example formulas, just run the testsuite:
83
84
  ./cool-testsuite.native
85
86 0dfb55b5 Thorsten Wißmann
Coalition Logic
87
~~~~~~~~~~~~~~~
88
Some formulas are
89
90
  [{1}] C & [{ 2 }] ~C
91
  [{1}] C & <{ 2 }> ~C
92
  [{1}] C & <{ 1 2 }> ~C
93
  <{ 1 2 }> C & <{ 1 2 3 4 5 6 7 8 9 10 }> ~C
94
  <{ 1 2 }> C & <{ 1 2 3 4 5 6 7 8 9 }> ~C
95
  <{ 1 2 }> C & <{ 1 2 }> ~C
96
  <{ 1 2 }> C & [{ 1 2 }] ~C
97
98
So call for example:
99
100 6fb39da4 Thorsten Wißmann
  ./coalg sat CL  <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
101 0dfb55b5 Thorsten Wißmann
102
103
104 7625cc6d Thorsten Wißmann
// vim: ft=asciidoc tw=80