From 75476b8dd73cfc8bbcfa25d692846e2e9463dec8 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 2 Feb 2019 18:55:05 -0600
Subject: [PATCH] test: use `mdx` to ensure the readme code snippets compile

---
 README.md | 99 +++++++++++++++++++++++++++++++++++++------------------
 dune      |  8 +++++
 msat.opam |  1 +
 3 files changed, 76 insertions(+), 32 deletions(-)
 create mode 100644 dune

diff --git a/README.md b/README.md
index 403ab049..3f7f0168 100644
--- a/README.md
+++ b/README.md
@@ -23,13 +23,17 @@ See https://gbury.github.io/mSAT/
 Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
 For the development version, use:
 
-    opam pin add msat https://github.com/Gbury/mSAT.git
+```
+opam pin add msat https://github.com/Gbury/mSAT.git
+```
 
 ### Manual installation
 
-You will need ocamlfind and ocamlbuild. The command is:
+You will need `dune` and `sequence`. The command is:
 
-    make install
+```
+$ make install
+```
 
 ## USAGE
 
@@ -47,43 +51,66 @@ as a functor which takes two modules :
 
 ### Sat Solver
 
-A ready-to-use SAT solver is available in the Sat module. It can be used
+A ready-to-use SAT solver is available in the `Msat_sat` module
+using the `msat.sat` library. It can be loaded
 as shown in the following code :
 
 ```ocaml
-(* Module initialization *)
-module Sat = Msat.Sat.Make()
-module E = Msat.Sat.Expr (* expressions *)
+# #require "msat.sat";;
+# #print_depth 0;; (* do not print details *)
+```
+
+Then we can create a solver and create some boolean variables:
+
+```ocaml
+module Sat = Msat_sat
+module E = Sat.Int_lit (* expressions *)
+
+let solver = Sat.create()
 
 (* We create here two distinct atoms *)
 let a = E.fresh ()    (* A 'new_atom' is always distinct from any other atom *)
 let b = E.make 1      (* Atoms can be created from integers *)
-
-(* We can try and check the satisfiability of some clauses --
-   here, the clause [a or b].
-   Sat.assume adds a list of clauses to the solver. *)
-let() = Sat.assume [[a; b]]
-let res = Sat.solve ()        (* Should return (Sat.Sat _) *)
-
-(* The Sat solver has an incremental mutable state, so we still have
-   the clause [a or b] in our assumptions.
-   We add [not a] and [not b] to the state. *)
-let () = Sat.assume [[E.neg a]; [E.neg b]]
-let res = Sat.solve ()        (* Should return (Sat.Unsat _) *)
 ```
 
+We can try and check the satisfiability of some clauses — here, the clause `a or b`.
+`Sat.assume` adds a list of clauses to the solver. Calling `Sat.solve`
+will check the satisfiability of the current set of clauses, here "Sat".
+
+```ocaml
+# Sat.assume solver [[a; b]] ();;
+- : unit = ()
+# let res = Sat.solve solver;;
+val res : Sat.res = Sat.Sat ...
+```
+
+The Sat solver has an incremental mutable state, so we still have
+the clause `a or b` in our assumptions.
+We add `not a` and `not b` to the state, and get "Unsat".
+
+```ocaml
+# Sat.assume solver [[E.neg a]; [E.neg b]] () ;;
+- : unit = ()
+# let res = Sat.solve solver ;;
+val res : Sat.res = Sat.Unsat ...
+```
 
 #### Formulas API
 
 Writing clauses by hand can be tedious and error-prone.
-The functor `Msat.Tseitin.Make` proposes a formula AST (parametrized by
+The functor `Msat_tseitin.Make` in the library `msat.tseitin`
+proposes a formula AST (parametrized by
 atoms) and a function to convert these formulas into clauses:
 
+```ocaml
+# #require "msat.tseitin";;
+```
+
 ```ocaml
 (* Module initialization *)
-module Sat = Msat.Sat.Make()
-module E = Msat.Sat.Expr (* expressions *)
-module F = Msat.Tseitin.Make(E)
+module F = Msat_tseitin.Make(E)
+
+let solver = Sat.create ()
 
 (* We create here two distinct atoms *)
 let a = E.fresh ()    (* A fresh atom is always distinct from any other atom *)
@@ -94,14 +121,22 @@ let p = F.make_atom a
 let q = F.make_atom b
 let r = F.make_and [p; q]
 let s = F.make_or [F.make_not p; F.make_not q]
-
-(* We can try and check the satisfiability of the given formulas *)
-let () = Sat.assume (F.make_cnf r)
-let _ = Sat.solve ()        (* Should return (Sat.Sat _) *)
-
-(* The Sat solver has an incremental mutable state, so we still have
- * the formula 'r' in our assumptions *)
-let () = Sat.assume (F.make_cnf s)
-let _ = Sat.solve ()        (* Should return (Sat.Unsat _) *)
+```
+
+We can try and check the satisfiability of the given formulas, by turning
+it into clauses using `make_cnf`:
+
+```ocaml
+# Sat.assume solver (F.make_cnf r) ();;
+- : unit = ()
+# Sat.solve solver;;
+- : Sat.res = Sat.Sat ...
+```
+
+```ocaml
+# Sat.assume solver (F.make_cnf s) ();;
+- : unit = ()
+# Sat.solve solver ;;
+- : Sat.res = Sat.Unsat ...
 ```
 
diff --git a/dune b/dune
new file mode 100644
index 00000000..d5e5e21b
--- /dev/null
+++ b/dune
@@ -0,0 +1,8 @@
+
+(alias
+ (name runtest)
+ (deps README.md)
+ (action (progn
+          (run mdx test %{deps})
+          (diff? %{deps} %{deps}.corrected))))
+
diff --git a/msat.opam b/msat.opam
index c0d0a3a5..c2fca559 100644
--- a/msat.opam
+++ b/msat.opam
@@ -15,6 +15,7 @@ depends: [
   "dune" {build}
   "sequence"
   "containers" {with-test}
+  "mdx" {with-test}
 ]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/Gbury/mSAT"