Smtml - SMT Solving in OCaml

Getting Started

Install via OPAM:

opam install smtml

Basic usage in OCaml toplevel:

# #require "smtml";;
# #install_printer Smtml.Expr.pp;;
# let pp_model = Smtml.Model.pp ~no_values:false;;
val pp_model : Smtml.Model.t Fmt.t = <fun>
# #install_printer pp_model;;
# #install_printer Smtml.Statistics.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 Fmt.t
    val create : ?params:Smtml.Params.t -> ?logic:Smtml.Logic.t -> 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 -> [ `Sat | `Unknown | `Unsat ]
    val check_set : t -> Smtml.Expr.Set.t -> [ `Sat | `Unknown | `Unsat ]
    val get_value : t -> Smtml.Expr.t -> Smtml.Expr.t
    val model : ?symbols:Smtml.Symbol.t list -> t -> Smtml.Model.t option
    val get_sat_model :
      ?symbols:Smtml.Symbol.t list ->
      t ->
      Smtml.Expr.Set.t -> [ `Model of Smtml.Model.t | `Unknown | `Unsat ]
  end
# let solver = Z3.create ();;
val solver : Z3.t = <abstr>

Creating Solvers

Smtml provides different solver modes through functors:

• Smtml.Solver.Batch for one-shot solving
• Smtml.Solver.Incremental for incremental solving

Create a Z3-based batch solver with custom parameters:

# let params = Smtml.Params.(default () $ (Timeout, 5000));;
val params : Smtml.Params.t = <abstr>
# let solver = Z3.create ~params ~logic:Smtml.Logic.QF_BV ();;
val solver : Z3.t = <abstr>

Solver Operations

Key operations (see Smtml.Solver_intf):

• Smtml.Solver_intf.S.push/ Smtml.Solver_intf.S.pop for context management
• Smtml.Solver_intf.S.add for adding constraints
• Smtml.Solver_intf.S.check for satisfiability checks
• Smtml.Solver_intf.S.get_value for model extraction

Building Expressions

Construct type-safe SMT expressions using:

• Smtml.Symbol for creating variables
• Smtml.Expr combinators
• Smtml.Ty for type annotations

Example: Bitvector arithmetic

# open Smtml;;
# let cond =
  let x = Expr.symbol (Symbol.make (Ty_bitv 8) "x") in
  let y = Expr.symbol (Symbol.make (Ty_bitv 8) "y") in
  let sum = Expr.binop (Ty_bitv 8) Add x y in
  let num = Expr.value (Bitv (Bitvector.of_int8 42)) in
  Expr.relop Ty_bool Eq sum num;;
val cond : Expr.t = (bool.eq (i8.add x y) 42)

Checking Satisfiability

Add constraints and check satisfiability:

# Z3.add solver [ cond ];;
- : unit = ()
# match Z3.check solver [] with
  | `Sat -> "Satisfiable"
  | `Unsat -> "Unsatisfiable"
  | `Unknown -> "Unknown";;
- : string = "Satisfiable"

Working with Models

Extract values from satisfiable constraints:

# let model = Z3.model solver |> Option.get;;
val model : Model.t = (model
    (x i8 9)
    (y i8 33))
# let x_val =
  let x = Symbol.make (Ty_bitv 8) "x" in
  Model.evaluate model x;;
val x_val : Value.t option = Some (Smtml.Value.Bitv <abstr>)

Advanced Features

Solver Parameters

Customize solver behavior using parameters:

let params = Smtml.Params.(
  default ()
  $ (Timeout, 1000)
  $ (Model, true)
  $ (Unsat_core, false)
);;

Solver Statistics

Track solver performance:

# Z3.get_statistics solver
- : Statistics.t =
((max memory 16.9)
 (memory 16.9)
 (num allocs 7625)
 (rlimit count 362)
 (sat backjumps 2)
 (sat conflicts 2)
 (sat decisions 15)
 (sat mk clause 2ary 57)
 (sat mk clause nary 98)
 (sat mk var 53)
 (sat propagations 2ary 28)
 (sat propagations nary 30))

More Examples

Explore comprehensive usage scenarios:

• Optimizer - Using optimizers

Contributing

Smtml is open source! Report issues and contribute at: GitHub Repository