# 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 () =
Z3.add solver [ expr ];
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:

`Encoding.Solver_intf.S.get_value`

allows the retrieval of a single value from the solver.`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 () =
Z3.add solver [ expr ];
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.