package encoding

  1. Overview
  2. Docs
Smt encoding library

Install

Dune Dependency

Authors

Maintainers

Sources

v0.0.2.tar.gz
md5=b7d315f0c74985afe527ca48df777371
sha512=dbb083d238cbf9a7ab0f446d0753ad37d98e7b5c324f5c34b918ce38786f35a2d84260b96f0deb72e0d74b2481b929de469e0f826525e5f10f163896db36ad49

Description

An OCaml abstraction layer for constraint solvers.

Published: 10 Jan 2024

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.

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

Dependencies (6)

  1. zarith >= "1.5"
  2. cmdliner >= "1.2.0"
  3. menhir build & >= "20220210"
  4. z3 >= "4.12.2" & < "4.13"
  5. ocaml >= "4.14.0"
  6. 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.