From a15fb7585685582d34f676311743c8c0710fe78c Mon Sep 17 00:00:00 2001
From: "Adam C. Foltzer" <acfoltzer@galois.com>
Date: Sun, 18 Jan 2015 17:03:43 -0800
Subject: [PATCH] update book with allSat

---
 .../highAssurance/HighAssurance.tex           | 31 +++++++++++++------
 1 file changed, 22 insertions(+), 9 deletions(-)

diff --git a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
index 3d5564494..d9ff514db 100644
--- a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
+++ b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
@@ -831,7 +831,7 @@ \section{Checking satisfiability}
 search for other solutions by explicitly disallowing 3:
 \begin{Verbatim}
   Cryptol> :sat \x -> isSqrtOf9 x && ~(elem (x, [3]))
-  \x -> isSqrtOf9 x && ~(elem (x, [3])) 125 = True
+  \x -> isSqrtOf9 x && ~(elem (x, [3])) 131 = True
 \end{Verbatim}
 Note the use of the \lamex to\indLamExp indicate the new
 constraint. (Of course, we could have defined another function {\tt
@@ -842,18 +842,31 @@ \section{Checking satisfiability}
 told us that {\tt 125} is another solution. Indeed $125 * 125 =
 9\imod{2^7}$, as you can verify separately.  We can search for more:
 \begin{Verbatim}
-  Cryptol> :sat \x -> isSqrtOf9 x && ~(elem (x, [3 125]))
-  \x -> isSqrtOf9 x && ~(elem (x, [3, 125]) ) 131 = True
+  Cryptol> :sat \x -> isSqrtOf9 x && ~(elem (x, [3, 125]))
+  \x -> isSqrtOf9 x && ~(elem (x, [3, 131])) 253 = True
 \end{Verbatim}
-And more: 
+Rather than manually adding solutions we have already seen, we can
+search for other solutions by asking the satisfiability checker for
+more solutions using the {\tt satNum} setting:
 \begin{Verbatim}
-  Cryptol> :sat \x -> isSqrtOf9 x && ~(elem (x, [3 131 125]))
-  \x -> isSqrtOf9 x && ~(elem (x, [3, 131, 125]) ) 253 = True
+  Cryptol> :set satNum = 4
+  Cryptol> :sat isSqrtOf9
+  isSqrtOf9 3 = True
+  isSqrtOf9 131 = True
+  isSqrtOf9 125 = True
+  isSqrtOf9 253 = True
 \end{Verbatim}
-If we try one more time, we get:
+By default, {\tt satNum} is set to {\tt 1}, so we only see one
+solution. When we change it to {\tt 4}, the satisfiability checker
+will try to find {\em up to} 4 solutions. We can also set it to {\tt
+  all}, which will try to find as many solutions as possible.
 \begin{Verbatim}
-  Cryptol> :sat \x -> isSqrtOf9 x && ~(elem (x, [3, 131, 125, 253]))
-  Unsatisfiable.
+  Cryptol> :set satNum = 4
+  Cryptol> :sat isSqrtOf9
+  isSqrtOf9 3 = True
+  isSqrtOf9 131 = True
+  isSqrtOf9 125 = True
+  isSqrtOf9 253 = True
 \end{Verbatim}
 So, we can rest assured that there are exactly four 8-bit square roots
 of 9; namely 3, 131, 125, and 253. (Note that Cryptol can return the