Commit 96acef58 authored by Julien's avatar Julien
Browse files

Fixed Makefile and clarified the README

parent cfe42b5c
SRCS=*.ml
INTR=*.mli
BUILD_DIR=_build/default/bin/
BIN_DIR=bin/
LIB_DIR=lib/onnx2SMT/
bins:$(BIN_DIR)$(SRCS)
dune build $(BIN_DIR)
onnx2SMT:$(LIB_DIR)$(SRCS)
dune build $(LIB_DIR)
doc:
dune build @doc
all:
dune build @install
static:
dune build @all
doc:
dune build @doc
install-deps:
opam install .
install-ext-deps:
opam update && opam depext
clean:
dune clean
......@@ -42,37 +42,40 @@ ISAIEH is not yet released as a binary, so you will need
to compile it from source.
### Dependencies:
Compiling and running will require the
following software and versions
* Ocaml 4.07.0
* piqilib 0.6.14
* piqi 0.7.6
* ocplib-endian 1.0
* dune 2.1
* zarith 1.7
* ppx_inline_test 0.12
* ppx_deriving 4.4.1
* janestreet OCaml Base 0.12.2
* janestreet stdio 0.12
The simplest way to obtain all of them is to use the
The list of OCaml dependencies is available under the
`dune-project` file at the root of the project.
The simplest way to get all dependencies is by using the
OCaml package manager, `opam`,
version 2.0 or higher.
Get it [here](https://opam.ocaml.org/).
Then, run `opam install .` at the root of project directory.
Then, run `opam install .` at the root
of project directory, or `make install-deps`.
`opam` will only take care of the OCaml dependencies. For
system dependencies, you may install `depext` using
`opam update && opam install depext`
(or `make install-ext-deps`), then typing
`opam depext` at the root of the project. A list of
necessary dependencies will be displayed and, if
your system is supported, the proper command to install
them will be given.
### Build:
* To build the project, type `dune build @install` at the root of
project directory. A static binary is available for compilation
(but it requires a statically linked libc, such as `musl`). To build
it, simply type `dune build`.
* To build the project after completing the dependencies
installation, type `make` (requires the `make`) utilitary.
* A static binary is available for compilation
(but it requires a statically linked libc,
such as `musl`). To build it, simply type `make static`.
* To build the API documentation, type `make doc`.
It will be available under `_build/default/_doc/_html`.
* To remove the build artifacts, type `make clean`.
### Run:
For now, a basic conversion from onnx to smt2 is the only
available binary.
* To run it, type
`dune exec -- bin/converter.exe /path/to/file.onnx`
at root of project.
`dune exec -- bin/converter/converter.exe /path/to/file.onnx`
at the root of the project.
Output will be saved under `/path/to/file.smt2`.
Change the target theory with option `-theory`.
For instance, to target
......@@ -127,6 +130,10 @@ ISAIEH is featured in the following publications:
for Deep Perception Systems Using Simulators_,
Julien Girard-Satabin, Guillaume Charpiat,
Zakaria Chihani, Marc Schoenauer, published at ECAI 2020
* _Partitionnement en régions linéaires pour la
vérification formelle de réseaux de neurones_,
Aymeric Varasse, Julien Girard-Satabin, Guillaume Charpiat,
Zakaria Chihani, Marc Schoenauer, published at J FLA 2021
## Citations
If you found this software useful for your work, please
......
......@@ -47,7 +47,7 @@ let pp_header t =
| Real_Theory -> "QF_NRA"
| Float_Theory -> "QF_FP"
in
[";;This file has been generated with onnx2SMTtool";
[";;This file has been generated with the ISAIEH tool";
"(set-logic "^logic_str^")";"(set-option :produce-models true)"]
(* SMT printing utils *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment