From a9220836cc16c82c97116004dd719809378c3306 Mon Sep 17 00:00:00 2001
From: GuillaumeGen <guillaume.genestier@tweag.io>
Date: Tue, 20 Sep 2022 18:31:33 +0200
Subject: [PATCH] Add examples and document it

---
 examples/Example/Monad/SatFile.hs   | 15 +++++++++++++++
 examples/Example/Monad/UnsatFile.hs | 12 ++++++++++++
 examples/Examples.hs                | 14 ++++++++++++++
 examples/README                     | 28 ++++++++++++++++++++++++++++
 examples/SMTLibFiles/CREDITS        |  2 ++
 examples/SMTLibFiles/Sat.smtlib     | 17 +++++++++++++++++
 examples/SMTLibFiles/Unsat.smtlib   |  8 ++++++++
 z3.cabal                            |  6 +++++-
 8 files changed, 101 insertions(+), 1 deletion(-)
 create mode 100644 examples/Example/Monad/SatFile.hs
 create mode 100644 examples/Example/Monad/UnsatFile.hs
 create mode 100644 examples/README
 create mode 100644 examples/SMTLibFiles/CREDITS
 create mode 100644 examples/SMTLibFiles/Sat.smtlib
 create mode 100644 examples/SMTLibFiles/Unsat.smtlib

diff --git a/examples/Example/Monad/SatFile.hs b/examples/Example/Monad/SatFile.hs
new file mode 100644
index 0000000..350ba8e
--- /dev/null
+++ b/examples/Example/Monad/SatFile.hs
@@ -0,0 +1,15 @@
+module Example.Monad.SatFile where
+
+import Z3.Monad
+
+run :: IO ()
+run =
+  evalZ3 result >>= print
+
+result :: MonadZ3 z3 => z3 (Result, Maybe String)
+result = do
+  fil <- parseSMTLib2File "examples/SMTLibFiles/Sat.smtlib" [] [] [] []
+  mapM_ assert fil
+  (res, mModel) <- solverCheckAndGetModel
+  strModel <- traverse showModel mModel
+  return (res, strModel)
diff --git a/examples/Example/Monad/UnsatFile.hs b/examples/Example/Monad/UnsatFile.hs
new file mode 100644
index 0000000..90e9932
--- /dev/null
+++ b/examples/Example/Monad/UnsatFile.hs
@@ -0,0 +1,12 @@
+module Example.Monad.UnsatFile where
+
+import Z3.Monad
+
+run :: IO ()
+run =
+  evalZ3 result >>= print
+
+result :: MonadZ3 z3 => z3 Result
+result = do
+  fil <- parseSMTLib2File "examples/SMTLibFiles/Unsat.smtlib" [] [] [] []
+  solverCheckAssumptions fil
diff --git a/examples/Examples.hs b/examples/Examples.hs
index 3e9d979..f91baa3 100644
--- a/examples/Examples.hs
+++ b/examples/Examples.hs
@@ -12,6 +12,8 @@ import qualified Example.Monad.ToSMTLib
 import qualified Example.Monad.Tuple
 import qualified Example.Monad.ParserInterface
 import qualified Example.Monad.IntList
+import qualified Example.Monad.UnsatFile
+import qualified Example.Monad.SatFile
 
 import System.Environment
 
@@ -49,9 +51,21 @@ examples =
   , ("intList"
     , Example.Monad.IntList.run
     )
+  , ("unsatFile"
+    , Example.Monad.UnsatFile.run
+    )
+  , ("satFile"
+    , Example.Monad.SatFile.run
+    )
   ]
 
 runExample :: String -> IO ()
+runExample "all" = mapM_ go examples
+  where
+    go :: (String, IO ()) -> IO ()
+    go (name, run) = do
+      putStrLn $ "\nRunning " ++ name ++ ":"
+      run
 runExample x = case lookup x examples of
                     Just x  -> x
                     Nothing -> error "Example not found"
diff --git a/examples/README b/examples/README
new file mode 100644
index 0000000..83da2f1
--- /dev/null
+++ b/examples/README
@@ -0,0 +1,28 @@
+# Examples of Haskell-Z3
+
+## Available examples
+
+To list the name of the available examples, run
+
+```
+cabal run --flags examples examples
+```
+
+## Run all examples
+
+To run all examples, run
+
+```
+cabal run --flags examples examples -- all
+```
+
+## Run one examples
+
+To run the example named `my-example`, run
+
+```
+cabal run --flags examples examples -- my-example
+```
+
+Note that the name of the example is the name of the file containing it,
+but with a lower-case first letter.
diff --git a/examples/SMTLibFiles/CREDITS b/examples/SMTLibFiles/CREDITS
new file mode 100644
index 0000000..82d8fa4
--- /dev/null
+++ b/examples/SMTLibFiles/CREDITS
@@ -0,0 +1,2 @@
+The example files in this folder were copied from the smt-lib website:
+https://smtlib.cs.uiowa.edu/examples.shtml
diff --git a/examples/SMTLibFiles/Sat.smtlib b/examples/SMTLibFiles/Sat.smtlib
new file mode 100644
index 0000000..087f353
--- /dev/null
+++ b/examples/SMTLibFiles/Sat.smtlib
@@ -0,0 +1,17 @@
+; Getting values or models
+(set-option :print-success false)
+(set-option :produce-models true)
+(set-logic QF_LIA)
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (+ x (* 2 y)) 20))
+(assert (= (- x y) 2))
+(check-sat)
+; sat
+(get-value (x y))
+; ((x 8) (y 6))
+(get-model)
+; ((define-fun x () Int 8)
+;  (define-fun y () Int 6)
+; )
+(exit)
diff --git a/examples/SMTLibFiles/Unsat.smtlib b/examples/SMTLibFiles/Unsat.smtlib
new file mode 100644
index 0000000..f45ba7f
--- /dev/null
+++ b/examples/SMTLibFiles/Unsat.smtlib
@@ -0,0 +1,8 @@
+; Integer arithmetic
+(set-logic QF_LIA)
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (- x y) (+ x (- y) 1)))
+(check-sat)
+; unsat
+(exit)
diff --git a/z3.cabal b/z3.cabal
index 4f0cbb2..dd60525 100644
--- a/z3.cabal
+++ b/z3.cabal
@@ -101,7 +101,8 @@ Executable examples
     Build-depends:     base >=4.5,
                        z3,
                        containers,
-                       transformers >= 0.2
+                       transformers >= 0.2,
+                       directory
   else
     Buildable:         False
 
@@ -120,6 +121,9 @@ Executable examples
                        Example.Monad.QuantifierElimination
                        Example.Monad.ToSMTLib
                        Example.Monad.Tuple
+                       Example.Monad.IntList
+                       Example.Monad.UnsatFile
+                       Example.Monad.SatFile
 
 Test-suite spec