An OCaml abstraction layer for constraint solvers.
Published: 21 Nov 2023
OCaml Constraint Abstraction Layer
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.
Build from source
Bootstrap the OCaml compiler:
opam switch create 5.1.0 5.1.0
Then, install the library dependencies:
git clone https://github.com/wasp-platform/encoding.git
opam install . --deps-only
Build and test:
encodingon your path by running:
Use encoding in your project
To incorporate encoding into your project, you can pin to your project:
opam pin encoding git+https://github.com/wasp-platform/encoding