Prerequisites

  1. GNU C,C++ complier and the make utility
  2. JAVA developer kit >= 1.6 (needed for the JAVA oracle example)
  3. OCAML 3.12.1 (needed for the OCaml oracle example, we assume OCaml libraries are in /opt/local or /usr/local)
  4. Minisat 2.2.0 for the C and OCaml oracle examples and SAT4J for the JAVA oracle example. (For the convenience of the users, we pack the source code of minisat and the jar file of SAT4J into our tool.)

Installation

We use BULL-dir to denote the root folder of BULL. The easiest way is to run the ./build.sh script in the root folder of BULL. It will automatically compile solvers, the core library, and oracles in different programming languages. For users who only need a part of the package, we describe how to compile each component in detail below.

The Core Library
  1. cd BULL-dir/Src/core
  2. make
Solvers

Before the compilation of the C or OCaml oracles, users have to first compile the minisat tool. For convenience, source code of minisat 2.2.0 is included in our package.

  1. cd BULL-dir/Src/solvers/minisat/core
  2. g++ -c -O2 -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -I../ Solver.cc
Oracles
  1. cd BULL-dir/Src/[c, cpp, java, ocaml]
  2. make
install.txt · Last modified: 2012/10/12 07:41 by gulu