Legend:
Library
Module
Module type
Parameter
Class
Class type

# Encoding

The full API can be found here. Coverage here

Encoding is a free and open-source OCaml SMT constraint abstraction layer that serves as an abstracted constraint-solving wrapper, currently utilising Z3 as its backend solver. However, future plans for Encoding include support for other solvers in its backend, such as Yices and CVC5.

## Creating Solvers

To begin creating solvers, utilize the modules provided in `Encoding.Solver` for Z3 encoding. The simplest approach to creating a solver in the Encoding is outlined below:

``````module Z3 = Encoding.Solver.Z3_incremental

let solver : Z3.t = Z3.create ()``````

For a comprehensive understanding of the solver functions and modes, refer to the documentation found here.

## Creating Expressions

To provide constraints to the solver, it is necessary to first construct expressions of type `Encoding.Expr.t`. These expressions consist of two key components: an arbitrary grammar expression of type `Encoding.Expr.expr` for building logical expressions, and a theory annotation of type `Encoding.Ty.t` that informs the SMT solver about the theory in which to encode our expressions. The combination of these two components is achieved using the `@:` operator.

As an illustration, consider the creation of the logical formula equivalent to `not (not x) = x`:

``````open Encoding
open Ty
open Expr

(* Creating a symbol *)
let x = mk_symbol Symbol.("x" @: Ty_bool)

(* Creating unary operations *)
let not_x : Expr.t = Unop (Not, x) @: Ty_bool
let not_not_x : Expr.t = Unop (Not, not_x) @: Ty_bool

(* Creating the equality *)
let expr : Expr.t = Relop (Eq, not_not_x, x) @: Ty_bool``````

Once our proposition is encoded in the abstract grammar, it can be passed to the solver for verification:

``````let () =
assert (Z3.check solver [])``````

## Retreiving Values from the Solver

In many cases, the ability to swiftly retrieve concrete values or sets of values from a set of satisfiable constraints proves to be immensely beneficial. The Encoding facilitates this process through two essential functions:

1. `Encoding.Solver_intf.S.get_value` allows the retrieval of a single value from the solver.
2. `Encoding.Solver_intf.S.model` enables the retrieval of all possible assignments within our constraints.

To illustrate, let's consider retrieving the value of `x` from our previous example:

``````let () =
assert (Z3.check solver []);
let v = Z3.get_value solver x in
Format.printf "x = %a@." Expr.pp v``````

In this snippet, we add our constraint to the solver, ensure its satisfiability, and then retrieve the value of `x`. The retrieved value is subsequently formatted for display using the Format module.

Innovation. Community. Security.

##### Ecosystem
Packages Community Events OCaml Planet Jobs
##### Policies
Carbon Footprint Governance Privacy Code of Conduct