1-----------------------------------------------------------------------------
2-- |
3-- Module      :  TestSuite.Queries.Sums
4-- Copyright   :  (c) Joel Burget
5--                    Levent Erkok
6-- License     :  BSD3
7-- Maintainer  :  erkokl@gmail.com
8-- Stability   :  experimental
9--
10-- Testing sum queries
11-----------------------------------------------------------------------------
12
13{-# LANGUAGE ScopedTypeVariables #-}
14{-# LANGUAGE TypeApplications    #-}
15
16{-# OPTIONS_GHC -Wall -Werror #-}
17
18module TestSuite.Queries.Sums (tests)  where
19
20import Data.SBV
21import Data.SBV.Control
22import Data.SBV.Either as E
23import Data.SBV.Maybe  as M
24
25import qualified Data.SBV.List as L
26
27import Utils.SBVTestFramework
28
29-- Test suite
30tests :: TestTree
31tests =
32  testGroup "Basics.QuerySums"
33    [ goldenCapturedIO "query_Sums"            $ testQuery querySums
34    , goldenCapturedIO "query_ListOfSum"       $ testQuery queryListOfSum
35    , goldenCapturedIO "query_Maybe"           $ testQuery queryMaybe
36    , goldenCapturedIO "query_ListOfMaybe"     $ testQuery queryListOfMaybe
37    , goldenCapturedIO "query_SumMaybeBoth"    $ testQuery querySumMaybeBoth
38    , goldenCapturedIO "query_sumMergeMaybe1"  $ testQuery querySumMergeMaybe1
39    , goldenCapturedIO "query_sumMergeMaybe2"  $ testQuery querySumMergeMaybe2
40    , goldenCapturedIO "query_sumMergeEither1" $ testQuery querySumMergeEither1
41    , goldenCapturedIO "query_sumMergeEither2" $ testQuery querySumMergeEither2
42    ]
43
44testQuery :: Show a => Symbolic a -> FilePath -> IO ()
45testQuery t rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t
46                    appendFile rf ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")
47
48querySums :: Symbolic (Either Integer Char)
49querySums = do
50  a <- sEither @Integer @Char "a"
51
52  constrain $ E.either (.== 1) (const sFalse) a
53
54  query $ do
55    _ <- checkSat
56
57    av <- getValue a
58
59    if av == Left 1
60       then return av
61       else error $ "Didn't expect this: " ++ show av
62
63queryListOfSum :: Symbolic [Either Integer Char]
64queryListOfSum = do
65  lst <- sList @(Either Integer Char) "lst"
66  constrain $ L.length lst .== 2
67  constrain $ isLeft $ L.head lst
68  constrain $ isRight $ L.head $ L.tail lst
69
70  query $ do
71    _  <- checkSat
72    av <- getValue lst
73
74    case av of
75      [Left _, Right _] -> return av
76      _                 -> error $ "Didn't expect this: " ++ show av
77
78queryMaybe :: Symbolic (Maybe Integer)
79queryMaybe = do
80  a <- sMaybe @Integer "a"
81
82  constrain $ M.maybe sFalse (.== 1) a
83
84  query $ do
85    _ <- checkSat
86
87    av <- getValue a
88
89    if av == Just 1
90       then return av
91       else error $ "Didn't expect this: " ++ show av
92
93queryListOfMaybe :: Symbolic [Maybe Char]
94queryListOfMaybe = do
95  lst <- sList @(Maybe Char) "lst"
96  constrain $ L.length lst .== 2
97  constrain $ isJust $ L.head lst
98  constrain $ isNothing $ L.head $ L.tail lst
99
100  query $ do
101    _  <- checkSat
102    av <- getValue lst
103
104    case av of
105      [Just _, Nothing] -> return av
106      _                 -> error $ "Didn't expect this: " ++ show av
107
108querySumMaybeBoth :: Symbolic (Either Integer Integer, Maybe Integer)
109querySumMaybeBoth = query $ do
110        (x :: SEither Integer Integer) <- freshVar_
111        (y :: SMaybe Integer)          <- freshVar_
112
113        constrain $ isLeft x
114        constrain $ isJust y
115
116        _ <- checkSat
117        xv <- getValue x
118        yv <- getValue y
119        return (xv, yv)
120
121querySumMergeMaybe1 :: Symbolic (Maybe Integer, Maybe Integer, Bool)
122querySumMergeMaybe1 = query $ do
123   (x :: SMaybe Integer) <- freshVar_
124   (y :: SMaybe Integer) <- freshVar_
125   b  <- freshVar_
126
127   constrain $ isNothing $ ite b x y
128
129   _ <- checkSat
130   xv <- getValue x
131   yv <- getValue y
132   bv <- getValue b
133   return (xv, yv, bv)
134
135querySumMergeMaybe2 :: Symbolic (Maybe Integer, Maybe Integer, Bool)
136querySumMergeMaybe2 = query $ do
137   (x :: SMaybe Integer) <- freshVar_
138   (y :: SMaybe Integer) <- freshVar_
139   b  <- freshVar_
140
141   constrain $ isJust $ ite b x y
142
143   _ <- checkSat
144   xv <- getValue x
145   yv <- getValue y
146   bv <- getValue b
147   return (xv, yv, bv)
148
149querySumMergeEither1 :: Symbolic (Either Integer Bool, Either Integer Bool, Bool)
150querySumMergeEither1 = query $ do
151   (x :: SEither Integer Bool) <- freshVar_
152   (y :: SEither Integer Bool) <- freshVar_
153   b  <- freshVar_
154
155   constrain $ isLeft $ ite b x y
156
157   _ <- checkSat
158   xv <- getValue x
159   yv <- getValue y
160   bv <- getValue b
161   return (xv, yv, bv)
162
163querySumMergeEither2 :: Symbolic (Either Integer Bool, Either Integer Bool, Bool)
164querySumMergeEither2 = query $ do
165   (x :: SEither Integer Bool) <- freshVar_
166   (y :: SEither Integer Bool) <- freshVar_
167   b  <- freshVar_
168
169   constrain $ isRight $ ite b x y
170
171   _ <- checkSat
172   xv <- getValue x
173   yv <- getValue y
174   bv <- getValue b
175   return (xv, yv, bv)
176
177{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
178