Update README.md with trivial library usage examples

README.md

@@ -12,15 +12,17 @@ error feedback enhance performance and usability.
 
 Install [opam](https://opam.ocaml.org/doc/Install.html) and bootstrap the OCaml compiler:
 
+<!-- $MDX skip -->
 ```sh
-opam init
-opam switch create 5.1.1 5.1.1
+$ opam init
+$ opam switch create 5.1.1 5.1.1
 ```
 
 Then install encoding:
 
+<!-- $MDX skip -->
 ```sh
-opam install smtml
+$ opam install smtml
 ```
 
 ### Installing a Solver
@@ -30,16 +32,18 @@ with different SMT solvers. By default, Smt.ml installs without a solver, but
 you can enable support for a specific solver by installing it with opam.
 For example, to install smtml with Z3:
 
+<!-- $MDX skip -->
 ```sh
-opam install smtml z3
+$ opam install smtml z3
 ```
 
 Alternatively, if you've already installed Smt.ml through opam, you can simply
 install the solver of your choice and opam will recompile smtml for you.
 For example, to install Z3 after installing smtml:
 
+<!-- $MDX skip -->
 ```sh
-opam install z3
+$ opam install z3
 ```
 
 See the [Supported Solvers](#supported-solvers) section below for a complete
@@ -49,31 +53,147 @@ list of available solvers.
 
 Clone the repo and install the dependencies:
 
+<!-- $MDX skip -->
 ```sh
-git clone https://github.com/formalsec/smtml.git
-cd smtml
-opam install . --deps-only --with-test
+$ git clone https://github.com/formalsec/smtml.git
+$ cd smtml
+$ opam install . --deps-only --with-test
 ```
 
 Build and test:
 
+<!-- $MDX skip -->
 ```sh
-dune build @install
-dune runtest
+$ dune build @install
+$ dune runtest
 ```
 
 Install `smtml` on your path by running:
 
+<!-- $MDX skip -->
 ```sh
-dune install
+$ dune install
 ```
 
 ### Code Coverage Reports
 
+<!-- $MDX skip -->
 ```sh
-BISECT_FILE=`pwd`/bisect dune runtest --force --instrument-with bisect_ppx
-bisect-ppx-report summary # Shell summary
-bisect-ppx-report html    # Detailed Report in _coverage/index.html
+$ BISECT_FILE=`pwd`/bisect dune runtest --force --instrument-with bisect_ppx
+$ bisect-ppx-report summary # Shell summary
+$ bisect-ppx-report html    # Detailed Report in _coverage/index.html
+```
+
+## Quick Start
+
+```ocaml
+# #require "smtml";;
+# open Smtml;;
+# #install_printer Expr.pp;;
+# #install_printer Value.pp
+# #install_printer Symbol.pp
+# #install_printer Statistics.pp;;
+# let pp_model = Model.pp ~no_values:false;;
+val pp_model : Model.t Fmt.t = <fun>
+# #install_printer pp_model;;
+
+# module Z3 = Solver.Batch (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 -> Expr.t list -> unit
+    val add_set : t -> Expr.Set.t -> unit
+    val get_assertions : t -> Expr.t list
+    val get_statistics : t -> Statistics.t
+    val check : t -> Expr.t list -> [ `Sat | `Unknown | `Unsat ]
+    val check_set : t -> Expr.Set.t -> [ `Sat | `Unknown | `Unsat ]
+    val get_value : t -> Expr.t -> Expr.t
+    val model : ?symbols:Symbol.t list -> t -> Model.t option
+  end
+# let solver = Z3.create ();;
+val solver : Z3.t = <abstr>
+
+# let cond =
+    let a = Expr.symbol (Symbol.make Ty.Ty_bool "a") in
+    let b = Expr.symbol (Symbol.make Ty.Ty_bool "b") in
+    Expr.(binop Ty_bool And a (unop Ty_bool Not b));;
+val cond : Expr.t = (bool.and a (bool.not b))
+
+# match Z3.check solver [ cond ] with
+    | `Sat -> "Satisfiable"
+    | `Unsat -> "Unsatisfiable"
+    | `Unknown -> "Unknown";;
+- : string = "Satisfiable"
+```
+
+## Features & Usage
+
+### Multi-Solver Support
+
+```ocaml
+# module Z3 = Solver.Batch (Z3_mappings);;
+...
+# module Bzla = Solver.Batch (Bitwuzla_mappings);;
+...
+```
+
+### Bitvector Arithmetic
+
+```ocaml
+# let cond =
+    let x = Expr.Bitv.I32.sym "x" in
+    let y = Expr.Bitv.I32.v 0xdeadbeefl in
+    let sum = Expr.(binop (Ty_bitv 32) Add x y) in
+    Expr.(relop Ty_bool Eq sum (Expr.Bitv.I32.v 0xffffffffl));;
+val cond : Expr.t = (bool.eq (i32.add x -559038737) -1)
+
+# let model =
+    let () = Z3.add solver [ cond ] in
+    let _ = Z3.check solver [] in
+    Z3.model solver
+val model : Model.t option = Some (model
+                                (x i32 559038736))
+```
+
+### Model Inspection
+
+```ocaml
+# match model with
+    | Some model -> Model.get_bindings model
+    | None -> []
+- : (Symbol.t * Value.t) list = [(x, 559038736)]
+```
+
+### Solver Statistics
+
+<!-- $MDX non-deterministic -->
+```ocaml
+# let stats = Z3.get_statistics solver;;
+val stats : Statistics.t =
+  ((added eqs 4)
+   (arith-make-feasible 2)
+   (arith-max-columns 4)
+   (bv bit2core 32)
+   (del clause 2)
+   (final checks 2)
+   (max memory 17.15)
+   (memory 17.15)
+   (mk bool var 38)
+   (mk clause 3)
+   (num allocs 11363)
+   (num checks 2)
+   (propagations 3)
+   (rlimit count 262))
 ```
 
 ## Supported Solvers
@@ -99,11 +219,12 @@ bisect-ppx-report html    # Detailed Report in _coverage/index.html
 
 The name `Smt.ml` is a portmanteau of the terms `SMT` and `OCaml`. The `.ml`
 extension is a common file extension for OCaml source files. The library itself
-is named `smtml` and can be imported into OCaml programs using the following
-syntax:
+is named `smtml` and can be imported into OCaml projects by:
 
-```ocaml
-open Smtml
+```dune
+(library
+  (name client_library)
+  (libraries smtml))
 ```
 
 ### Changelog

doc/index.mld

@@ -20,8 +20,6 @@ opam install smtml
 
 Basic usage in OCaml toplevel:
 {@ocaml[
-# #use "topfind";;
-...
 # #require "smtml";;
 # #install_printer Smtml.Expr.pp;;
 # let pp_model = Smtml.Model.pp ~no_values:false;;
@@ -90,13 +88,11 @@ Construct type-safe SMT expressions using:
 Example: Bitvector arithmetic
 {@ocaml[
 # open Smtml;;
-# let x = Expr.symbol (Symbol.make (Ty_bitv 8) "x");;
-val x : Expr.t = x
-# let y = Expr.symbol (Symbol.make (Ty_bitv 8) "y");;
-val y : Expr.t = y
-# let sum = Expr.binop (Ty_bitv 8) Add x y;;
-val sum : Expr.t = (i8.add x y)
-# let cond = Expr.relop Ty_bool Eq sum (Expr.value (Num (I8 42)));;
+# 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
+  Expr.relop Ty_bool Eq sum (Expr.value (Num (I8 42)));;
 val cond : Expr.t = (bool.eq (i8.add x y) 42)
 ]}
 

dune

@@ -0,0 +1,7 @@
+(mdx
+ (enabled_if
+  (and
+   %{lib-available:z3}
+   (not %{lib-available:bitwuzla-cxx})
+   (not %{lib-available:colibri2.core})
+   (not %{lib-available:cvc5}))))