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
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Queries.Int_Boolector
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Testing Boolector specific interactive features.
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Queries.Int_Boolector (tests) where
import Data.SBV.Control
import Control.Monad (unless)
import Utils.SBVTestFramework
-- Test suite
tests :: TestTree
tests =
testGroup "Basics.QueryIndividual"
[ goldenCapturedIO "query_boolector" $ \rf -> runSMTWith boolector{verbose=True, redirectVerbose=Just rf} q
, goldenCapturedIO "query_bitwuzla" $ \rf -> runSMTWith bitwuzla {verbose=True, redirectVerbose=Just rf} q
]
q :: Symbolic ()
q = do a <- sInt32 "a"
b <- sInt32 "b"
constrain $ a .> 0
constrain $ b .> 0
query $ do constrain $ a+2 .<= 15
constrain $ a .< 3
constrain $ b .< 2
constrain $ a+b .< 12
constrain $ a .< 2
cs <- checkSat
case cs of
Sat -> return ()
Unk -> getInfo ReasonUnknown >>= error . show
r -> error $ "Something went bad, why not-sat/unk?: " ++ show r
-- Now assert so that we get even a bigger value..
constrain $ a .>= 1
_ <- checkSat
res <- (,) <$> getValue a <*> getValue b
unless (res == (1, 1)) $ error $ "Didn't get (1,1): " ++ show res
|
