/encoding

An OCaml SMT abstraction layer for constraint solvers.

Primary LanguageOCamlGNU General Public License v3.0GPL-3.0

OCaml Constraint Abstraction Layer

Build badge GPL-3.0 Platform

The OCaml Constraint Abstraction Layer (OCAL) serves as an abstracted constraint-solving wrapper, currently utilising Z3 as its backend solver. However, future plans for OCAL include support for other solvers in its backend, such as Yices and CVC5.

Installation

OPAM

  • Install opam.
  • Bootstrap the OCaml compiler:
opam init
opam switch create 5.1.0 5.1.0
  • And, then install encoding:
opam install encoding

Build from source

  • Install the library dependencies:
git clone https://github.com/wasp-platform/encoding.git
cd encoding
opam install . --deps-only
  • Build and test:
dune build
dune runtest
  • Install encoding on your path by running:
dune install