package encoding

  1. Overview
  2. Docs
Smt encoding library

Install

Dune Dependency

Authors

Maintainers

Sources

v0.0.1.tar.gz
md5=dc32bbd40f0bfad2c8052d45a26d13f3
sha512=7946f81a6226378b493af9db129445bbe4f51e2924ed490692e485af1f16f09444cfc635e3c04064d5f9b64e64605f121e73e3c8feafa6bb03f8bd39ed99e671

Description

An OCaml abstraction layer for constraint solvers.

Published: 21 Nov 2023

README

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

  • Install opam.

  • Bootstrap the OCaml compiler:

opam init
opam switch create 5.1.0 5.1.0
  • Then, 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

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

Dependencies (5)

  1. zarith >= "1.5"
  2. menhir
  3. z3 >= "4.11.2" & < "4.13"
  4. ocaml >= "5.1.0"
  5. dune >= "3.0"

Dev Dependencies (2)

  1. odoc with-doc
  2. ppx_inline_test with-test

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.