Add examples and document it

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)

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

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"

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.

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

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)

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)

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