Project

General

Profile

Statistics
| Branch: | Revision:

cool / INSTALL @ master

History | View | Annotate | Download (2.15 KB)

1
// -*- mode: adoc; fill-column: 80; -*-
2
cool solver installation notes
3
==============================
4

    
5
Dependencies
6
------------
7
Install ocaml include files, minisat include files. Place them in the include
8
directory (e.g. /usr/include, /usr/lib/ocaml, or .).
9

    
10
Dependencies:
11

    
12
  - oasis (only needed if there is no setup.ml, e.g. when building from git)
13
  - ocamlfind (package called ocaml-findlib)
14
  - ocamlgraph (package ocaml-ocamlgraph)
15
  - readline
16
  - minisat (at least minisat 2)
17

    
18
On Debian or Ubuntu, install the following packages:
19

    
20
  - git
21
  - build-essential
22
  - oasis
23
  - libocamlgraph-ocaml-dev
24
  - libreadline-dev
25
  - minisat
26

    
27

    
28
Build
29
-----
30
In case there is no setup.ml yet, create it with oasis:
31

    
32
    oasis setup
33

    
34

    
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
Then compile it:
39

    
40
    ocaml setup.ml -configure
41
    ocaml setup.ml -build
42

    
43
(There will be some warnings.)
44

    
45
Now you have a freshly built coalg.native in the toplevel directory.
46

    
47
If you want the executables statically linked, then run the configure step with
48
the flag --enable-static.
49

    
50
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
Installation
71
------------
72
Not possible yet.
73

    
74
Benchmarking
75
------------
76
You should remove the debug flag (-g) from the Makefile and recompile before
77
doing time measurements.
78

    
79
Examples
80
--------
81

    
82
To see a longer list of example formulas, just run the testsuite:
83

    
84
  ./cool-testsuite.native
85

    
86
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
  ./coalg sat CL  <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
101

    
102

    
103

    
104
// vim: ft=asciidoc tw=80