1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
{-# LANGUAGE GADTs #-}
module Main where
import Data.Foldable (forM_)
import System.IO (FilePath)
import Data.Parameterized.Nonce (newIONonceGenerator)
import Data.Parameterized.Some (Some(..))
import What4.Config (extendConfig)
import What4.Expr
( ExprBuilder, FloatModeRepr(..), newExprBuilder
, BoolExpr, GroundValue, groundEval
, EmptyExprBuilderState(..) )
import What4.Interface
( BaseTypeRepr(..), getConfiguration
, freshConstant, safeSymbol
, notPred, orPred, andPred )
import What4.Solver
(defaultLogData, z3Options, withZ3, SatResult(..))
import What4.Protocol.SMTLib2
(assume, sessionWriter, runCheckSat)
z3executable :: FilePath
z3executable = "z3"
main :: IO ()
main = do
Some ng <- newIONonceGenerator
sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
-- This line is necessary for working with z3.
extendConfig z3Options (getConfiguration sym)
-- Let's determine if the following formula is satisfiable:
-- f(p, q, r) = (p | !q) & (q | r) & (!p | !r) & (!p | !q | r)
-- First, declare fresh constants for each of the three variables p, q, r.
p <- freshConstant sym (safeSymbol "p") BaseBoolRepr
q <- freshConstant sym (safeSymbol "q") BaseBoolRepr
r <- freshConstant sym (safeSymbol "r") BaseBoolRepr
-- Next, create terms for the negation of p, q, and r.
not_p <- notPred sym p
not_q <- notPred sym q
not_r <- notPred sym r
-- Next, build up each clause of f individually.
clause1 <- orPred sym p not_q
clause2 <- orPred sym q r
clause3 <- orPred sym not_p not_r
clause4 <- orPred sym not_p =<< orPred sym not_q r
-- Finally, create f out of the conjunction of all four clauses.
f <- andPred sym clause1 =<<
andPred sym clause2 =<<
andPred sym clause3 clause4
-- Determine if f is satisfiable, and print the instance if one is found.
checkModel sym f [ ("p", p)
, ("q", q)
, ("r", r)
]
-- Now, let's add one more clause to f.
clause5 <- orPred sym p =<< orPred sym q not_r
g <- andPred sym f clause5
-- Determine if g is satisfiable.
checkModel sym g [ ("p", p)
, ("q", q)
, ("r", r)
]
-- | Determine whether a predicate is satisfiable, and print out the values of a
-- set of expressions if a satisfying instance is found.
checkModel ::
ExprBuilder t st fs ->
BoolExpr t ->
[(String, BoolExpr t)] ->
IO ()
checkModel sym f es = do
-- We will use z3 to determine if f is satisfiable.
withZ3 sym z3executable defaultLogData $ \session -> do
-- Assume f is true.
assume (sessionWriter session) f
runCheckSat session $ \result ->
case result of
Sat (ge, _) -> do
putStrLn "Satisfiable, with model:"
forM_ es $ \(nm, e) -> do
v <- groundEval ge e
putStrLn $ " " ++ nm ++ " := " ++ show v
Unsat _ -> putStrLn "Unsatisfiable."
Unknown -> putStrLn "Solver failed to find a solution."
|
