Encoding

The full API can be found 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:

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 () =
  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.