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