{0 Smtml}

The full API can be {{:Smtml/index.html} found here}.
Coverage {{:https://formalsec.github.io/smtml/coverage/index.html} here}

{e 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.

{1 Creating Solvers}

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

{@ocaml[
# #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 {{:Smtml/Solver/index.html} found here}.

{1 Creating Expressions}

To provide constraints to the solver, it is necessary to first construct
expressions of type {!type:Smtml.Expr.t}. These expressions consist of two
key components: an arbitrary grammar expression of type {!type:Smtml.Expr.expr}
for building logical expressions, and a theory annotation of type {!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]:

{@ocaml[
# 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:

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

{1 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:

+ {!val:Smtml.Solver_intf.S.get_value} allows the retrieval of a single value
  from the solver.
+ {!val: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:

{@ocaml[
# 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.

{1 More Examples}

More examples can be found {{!examples}here}.
