From feff94bdbb115ab588685c1252887d958fe70aba Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 7 Aug 2021 21:09:20 -0400
Subject: [PATCH] doc: update guide (models changed, more printers needed)

---
 doc/guide.md | 30 ++++++++++++++++++++++--------
 1 file changed, 22 insertions(+), 8 deletions(-)

diff --git a/doc/guide.md b/doc/guide.md
index 0583941a..f523fc31 100644
--- a/doc/guide.md
+++ b/doc/guide.md
@@ -100,7 +100,6 @@ for legibility:
 # #install_printer Ty.pp;;
 # #install_printer Fun.pp;;
 # #install_printer Model.pp;;
-# #install_printer Solver.Atom.pp;;
 # #install_printer Solver.Model.pp;;
 # #install_printer Proof.pp_debug;;
 Proof.pp_debug has a wrong type for a printing function.
@@ -203,6 +202,11 @@ val solver : Solver.t = <abstr>
 
 # Solver.add_theory;;
 - : Solver.t -> Solver.theory -> unit = <fun>
+
+# (* print solver's atoms *)
+  let pp_atom out a = Solver.Atom.pp solver out a;;
+val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
+# #install_printer pp_atom;;
 ```
 
 Alright, let's do some solving now ⚙️. We're going to assert
@@ -221,8 +225,8 @@ Sidekick_base_solver.Solver.Sat
  (model
   (true := true)
   (false := false)
-  (p := false)
-  (q := false)
+  (p := true)
+  (q := true)
   (_tseitin_equiv_0 := true))
 ```
 
@@ -258,8 +262,8 @@ Sidekick_base_solver.Solver.Sat
  (model
   (true := true)
   (false := false)
-  (p := false)
-  (q := false)
+  (p := true)
+  (q := true)
   (_tseitin_equiv_0 := true))
 ```
 
@@ -276,9 +280,9 @@ Sidekick_base_solver.Solver.Sat
  (model
   (true := true)
   (false := false)
-  (p := false)
-  (q := false)
-  (r := false)
+  (p := true)
+  (q := true)
+  (r := true)
   (_tseitin_equiv_0 := true)
   (_tseitin_implies_1 := true))
 ```
@@ -313,6 +317,11 @@ Let's create a new solver and add the theory of reals to it.
 ```ocaml
 # let solver = Solver.create ~theories:[th_bool; th_lra] tstore () ();;
 val solver : Solver.t = <abstr>
+
+# (* print solver's atoms *)
+  let pp_atom out a = Solver.Atom.pp solver out a;;
+val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
+# #install_printer pp_atom;;
 ```
 
 Create a few arithmetic constants.
@@ -406,6 +415,11 @@ Anyway, Sidekick knows how to reason about functions.
 # let solver = Solver.create ~theories:[] tstore () ();;
 val solver : Solver.t = <abstr>
 
+# (* print solver's atoms *)
+  let pp_atom out a = Solver.Atom.pp solver out a;;
+val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
+# #install_printer pp_atom;;
+
 # (* helper *)
   let appf1 x = Term.app_fun_l tstore f1 x;;
 val appf1 : Term.t list -> Term.t = <fun>