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:

# #use "topfind"
...
# #require "smtml"
# #install_printer Smtml.Expr.pp
# module Z3 = Smtml.Solver.Batch (Smtml.Z3_mappings)
module Z3 :
  sig
    type t = Smtml.Solver.Batch(Smtml.Z3_mappings).t
    type solver = Smtml.Solver.Batch(Smtml.Z3_mappings).solver
    val solver_time : float ref
    val solver_count : int ref
    val pp_statistics : t Smtml_prelude.Fmt.t
    val create : ?params:Smtml.Params.t -> ?logic:Smtml.Ty.logic -> unit -> t
    val interrupt : t -> unit
    val clone : t -> t
    val push : t -> unit
    val pop : t -> int -> unit
    val reset : t -> unit
    val add : t -> Smtml.Expr.t list -> unit
    val add_set : t -> Smtml.Expr.Set.t -> unit
    val get_assertions : t -> Smtml.Expr.t list
    val get_statistics : t -> Smtml.Statistics.t
    val check : t -> Smtml.Expr.t list -> Smtml.Solver_intf.satisfiability
    val check_set : t -> Smtml.Expr.Set.t -> Smtml.Solver_intf.satisfiability
    val get_value : t -> Smtml.Expr.t -> Smtml.Expr.t
    val model : ?symbols:Smtml.Symbol.t list -> t -> Smtml.Model.t option
  end
# let solver = Z3.create ()
val solver : Z3.t = <abstr>

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
# let x = Expr.symbol (Symbol.make Ty_bool "x")
val x : Expr.t = x
# let not_x = Expr.unop Ty_bool Not x
val not_x : Expr.t = (bool.not x)
# let not_not_x = Expr.unop Ty_bool Not not_x
val not_not_x : Expr.t = x
# let expr : Expr.t = Expr.relop Ty_bool Eq not_not_x x
val expr : Expr.t = (bool.eq x x)

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

# Z3.add solver [ expr ]
- : unit = ()
# assert (match Z3.check solver [] with `Sat -> true | _ -> false)
- : unit = ()

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:

# assert (match Z3.check solver [] with `Sat -> true | _ -> false)
- : unit = ()
# Z3.get_value solver x
- : Expr.t = false

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.

More Examples

More examples can be found here.