Inez - A Constraint Solver
Inez is a constraint solver.
Inez implements the ILP Modulo Theories scheme, as described in a CAV paper. Simply put, we combine a Mathematical Programming solver with background solvers.
Inez is OCaml-centric. The preferred mode of interacting with the solver is via scripts written in a Camlp4-powered superset of OCaml.
Inez is a research prototype, and may contain serious bugs. You should not use it in production.
Inez is known to work on x86_64 GNU/Linux and Mac OS X. Other modern Unixen should work, as long as all dependencies are satisfied.
Inez does not work on Windows. We depend quite heavily on Jane Street Core, which is Unix-only.
Inez depends on the SCIP optimization suite, version 3.1.x. The SCIP optimization suite is available without charge for academic and non-commercial purposes. For other purposes, a license agreement is required.
Once you obtain the "optimization suite" distribution, the following recipe suffices (applied to the toplevel directory):
make scipoptlib \ SHARED=true \ READLINE=false \ ZLIB=false \ GMP=false \ ZIMPL=false
.so is under
lib/. Create a symbolic link to it as follows:
ln -s libscipopt-3.1.0.linux.x86_64.gnu.opt.so libscipopt.so
C and C++ Libraries and Tools
Building Inez requires GCC (C++ frontend included). We also depend on Boost. Fetch and untar a fresh tarball.
OCaml Libraries and Tools
Inez requires OCaml 4.02 or newer. Additionally, you will need recent versions of the following packages:
The best way to obtain the above is via OPAM.
Once all dependencies are satisfied, you have to:
OMakefile.configfor your setup.
omake frontend/inez.optto build Inez.
inez.opt is dynamically linked against
LD_LIBRARY_PATH so that the dynamic linker can find this shared
library. On OS X, you should set
DYLD_FALLBACK_LIBRARY_PATH in place
inez.opt accepts a single argument for the input program. Some
examples can be found under