From e60e8936e1fa8d7ec5a37bb35888d210f60eed53 Mon Sep 17 00:00:00 2001 From: Emina Torlak Date: Sun, 20 Sep 2015 15:07:51 -0700 Subject: [PATCH] More detailed build/install/run instructions. --- README.md | 47 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 36 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 8f370c3c..77d43a7b 100644 --- a/README.md +++ b/README.md @@ -8,12 +8,12 @@ manipulating, and solving relational constraints. The source code is extensively documented, and the repository includes many [examples](https://github.com/emina/kodkod/tree/master/examples/kodkod/examples) demonstrating the use of the Kodkod API. -Kodkod is open-source and available under the [MIT license](LICENSE). However, the implementation relies on third-party SAT solvers ([SAT4J](http://www.sat4j.org), [MiniSAT](http://minisat.se), [Glucose](http://www.labri.fr/perso/lsimon/glucose/), and [(P)Lingeling](http://fmv.jku.at/lingeling/)), some of which are released under stricter licenses. Please see the solver licenses for details. +Kodkod is open-source and available under the [MIT license](LICENSE). However, the implementation relies on third-party SAT solvers ([SAT4J](http://www.sat4j.org), [MiniSat](http://minisat.se), [Glucose](http://www.labri.fr/perso/lsimon/glucose/), and [(P)Lingeling](http://fmv.jku.at/lingeling/)), some of which are released under stricter licenses. Please see the solver licenses for details. ### Building and installing Kodkod The following compilation and installation instructions have been -tested on Linux (Fedora 22) and on Mac OS X (10.10.5). You may +tested on Linux (Fedora 22 with gcc 5.1.1) and on Mac OS X (10.10.5 with clang 6.0 and gcc 4.9). You may need to modify the build scripts for other operating systems. Kodkod uses the [Waf](https://github.com/waf-project/waf) build @@ -21,27 +21,52 @@ system, which requires Python 2.5 or later. You will also need Java 8 and a C/C++ compiler, and your JAVA_HOME environment variable needs to point to the JDK 8 home directory. +* Set the JAVA_HOME variable. For example, on OS X: + + ``$ export JAVA_HOME=`/usr/libexec/java_home` `` + * Clone the kodkod repository: `$ git clone https://github.com/emina/kodkod.git` `$ cd kodkod` -* Download Waf 1.8.12: +* Download Waf 1.8.12 and make it executable: `$ wget --no-check-certificate https://waf.io/waf-1.8.12` - `$ mv waf-1.8.12 waf` - `$ chmod 755 waf` - `$ alias waf=$PWD/waf` + `$ chmod u+x waf-1.8.12` + `$ alias waf=$PWD/waf-1.8.12` -* Build the native libraries, `kodkod.jar`, and `examples.jar` and install them into - the `kodkod/lib` directory: +* Build the native libraries, ``kodkod.jar``, and ``examples.jar`` and install them into the ``kodkod/lib`` directory: `$ waf configure --prefix=. --libdir=lib build install` +### Running Kodkod -* Solve an example problem: - - `$ java -cp lib/kodkod.jar:lib/examples.jar -Djava.library.path=lib kodkod.examples.sudoku.Sudoku` +[Download](http://alloy.mit.edu/kodkod/download.html) (or [build](https://github.com/emina/kodkod#building-and-installing-kodkod)) the ``kodkod.jar`` binary, solver binaries, and the ``examples.jar`` binary. Assuming that the current working directory contains these binaries, run the [Sudoku example](https://github.com/emina/kodkod/blob/master/examples/kodkod/examples/sudoku/Sudoku.java) as follows: + + `$ java -cp kodkod.jar:examples.jar -Djava.library.path=. kodkod.examples.sudoku.Sudoku` + +The program will produce a solution to a sample Sudoku puzzle: + +``` +p cnf 3452 7954 +primary variables: 486 +translation time: 176 ms +solving time: 2 ms ++-------+-------+-------+ +| 6 4 7 | 2 1 3 | 9 5 8 | +| 9 1 8 | 5 6 4 | 7 2 3 | +| 2 5 3 | 8 7 9 | 4 6 1 | ++-------+-------+-------+ +| 1 9 5 | 6 4 7 | 8 3 2 | +| 4 8 2 | 3 5 1 | 6 7 9 | +| 7 3 6 | 9 2 8 | 1 4 5 | ++-------+-------+-------+ +| 5 7 4 | 1 9 2 | 3 8 6 | +| 8 2 9 | 7 3 6 | 5 1 4 | +| 3 6 1 | 4 8 5 | 2 9 7 | ++-------+-------+-------+ +```