Smtml

The full API can be found here. Coverage here

Smt.ml 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 Smt.ml include support for other solvers in its backend, such as Yices and cvc5.

Creating Solvers

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

module Z3 = Smtml.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 Smtml.Expr.t. These expressions consist of two key components: an arbitrary grammar expression of type Smtml.Expr.expr for building logical expressions, and a theory annotation of type Smtml.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 constructors unop, binop, relop, etc.

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

open Smtml
open Ty
open Expr

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

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

(* Creating the equality *)
let expr : Expr.t = relop Ty_bool Eq not_not_x x

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. Smtml.Solver_intf.S.get_value allows the retrieval of a single value from the solver.
2. Smtml.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.