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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
module Main where
import Test.Tasty
import Test.Tasty.HUnit
import Data.Foldable (forM_)
import qualified Data.Text as Text
import Data.Parameterized.Nonce (newIONonceGenerator)
import Data.Parameterized.Some (Some(..))
import System.IO (FilePath, IOMode(..), openFile, hClose)
import System.IO.Temp (withSystemTempFile)
import What4.Config (extendConfig)
import What4.Expr
( ExprBuilder, FloatModeRepr(..), newExprBuilder
, BoolExpr, IntegerExpr, GroundValue, groundEval
, EmptyExprBuilderState(..))
import What4.Interface
( BaseTypeRepr(..), getConfiguration
, freshConstant, safeSymbol, notPred
, impliesPred, intLit, intAdd, intLe )
import What4.Solver
import What4.Symbol (SolverSymbol(..))
import What4.Protocol.SMTLib2 as SMT2
(assume, sessionWriter, runCheckSat, runGetAbducts, Writer)
import What4.Protocol.SMTWriter
(mkSMTTerm)
import What4.Protocol.Online
cvc5executable :: FilePath
cvc5executable = "cvc5"
-- Call the online getAbduct tactic
testGetAbductOnline ::
ExprBuilder t st fs ->
[BoolExpr t] ->
BoolExpr t ->
Int ->
IO [String]
testGetAbductOnline sym hs g n = do
-- Print SMT file in /tmp/
withSystemTempFile "what4abdonline" $ \fname mirroredOutput -> do
proc <- startSolverProcess @(SMT2.Writer CVC5) cvc5Features (Just mirroredOutput) sym
let conn = solverConn proc
inNewFrame proc $ do
mapM_ (\x -> assume conn x) hs
getAbducts proc n (Text.pack "abd") g
-- Call the offline getAbduct tactic
testGetAbductOffline ::
ExprBuilder t st fs ->
BoolExpr t ->
Int ->
IO [String]
testGetAbductOffline sym f n = do
-- Print SMT file in /tmp/
withSystemTempFile "what4abdoffline" $ \fname mirroredOutput -> do
let logData = LogData { logCallbackVerbose = \_ _ -> return ()
, logVerbosity = 2
, logReason = "defaultReason"
, logHandle = Just mirroredOutput }
withCVC5 sym cvc5executable logData $ \session -> do
f_term <- mkSMTTerm (sessionWriter session) f
runGetAbducts session n (Text.pack "abd") f_term
-- Prove f using an SMT solver, by checking if ~f is unsatisfiable
prove ::
ExprBuilder t st fs ->
BoolExpr t ->
[(String, IntegerExpr t)] ->
IO (SatResult () ())
prove sym f es = do
-- Print SMT file in /tmp/
withSystemTempFile "what4prove" $ \fname mirroredOutput -> do
proc <- startSolverProcess @(SMT2.Writer CVC5) cvc5Features (Just mirroredOutput) sym
let logData = LogData { logCallbackVerbose = \_ _ -> return ()
, logVerbosity = 2
, logReason = "defaultReason"
, logHandle = Just mirroredOutput }
-- To prove f, we check whether not f is unsat
notf <- notPred sym f
withCVC5 sym cvc5executable logData $ \session -> do
checkSatisfiable proc "test" notf
-- Tests
testAbdOnline :: ExprBuilder t st fs ->
[BoolExpr t] ->
BoolExpr t ->
TestTree
testAbdOnline sym hs g = testCase "getting 3 abducts using cvc5 online" $ do
-- Ask for 3 abducts for f
res <- testGetAbductOnline sym hs g 3
(length res == 3) @? "3 online abducts"
testAbdOffline :: ExprBuilder t st fs ->
BoolExpr t ->
[(String, IntegerExpr t)] ->
TestTree
testAbdOffline sym f es = testCase "getting 3 abducts using cvc5 offline" $ do
-- Ask for 3 abducts for f
res <- testGetAbductOffline sym f 3
(length res == 3) @? "3 offline abducts"
testSatAbd :: ExprBuilder t st fs ->
BoolExpr t ->
[(String, IntegerExpr t)] ->
TestTree
testSatAbd sym f es = testCase "testing SAT query for abduction" $ do
-- Prove f (is ~f unsatisfiable?). We expect ~f to be satisfiable
res <- prove sym f es
isSat res @? "sat"
main :: IO ()
main = do
Some ng <- newIONonceGenerator
sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
-- This line is necessary for working with cvc5.
extendConfig cvc5Options (getConfiguration sym)
-- Build this formula: ~(y >= 0 => (x + y + z) >= 0)
-- First, declare fresh constants for each of the three variables x, y, z.
x <- freshConstant sym (safeSymbol "x") BaseIntegerRepr
y <- freshConstant sym (safeSymbol "y") BaseIntegerRepr
z <- freshConstant sym (safeSymbol "z") BaseIntegerRepr
-- Next, build up the clause
zero <- intLit sym 0 -- 0
pxyz <- intAdd sym x =<< intAdd sym y z -- x + y + z
ygte0 <- intLe sym zero y -- 0 <= y
xyzgte0 <- intLe sym zero pxyz -- 0 <= (x + y + z)
f <- impliesPred sym ygte0 xyzgte0 -- (0 <= y) -> (0 <= (x + y + z))
defaultMain $ testGroup "Tests" $
[ -- test passes if f is disproved (~f is sat)
testSatAbd sym f [ ("x", x)
, ("y", y)
, ("z", z)
],
-- test passes if cvc5 returns 3 abducts (offline)
testAbdOffline sym f [ ("x", x)
, ("y", y)
, ("z", z)
],
-- test passes if cvc5 returns 3 abducts (online)
testAbdOnline sym [ygte0] xyzgte0
]
|
