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
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Queries.Int_ABC
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Testing ABC specific interactive features.
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Queries.Int_ABC (tests) where
import Data.SBV.Control
import Control.Monad (unless)
import Utils.SBVTestFramework
-- Test suite
tests :: TestTree
tests =
testGroup "Basics.QueryIndividual"
[ goldenCapturedIO "query_abc" $ \rf -> runSMTWith abc{verbose=True, redirectVerbose=Just rf} q
]
q :: Symbolic ()
q = do a <- sInt32 "a"
b <- sInt32 "b"
constrain $ a .> 0
constrain $ b .> 0
-- this is severely limited since ABC doesn't like multi check-sat calls, oh well.
query $ do constrain $ a+2 .<= 15
constrain $ a .< 2
constrain $ b .< 2
constrain $ a+b .< 12
constrain $ a .< 2
cs <- checkSat
case cs of
Unk -> getInfo ReasonUnknown >>= error . show
Unsat -> error "Got UNSAT!"
DSat{} -> error "Got Delta-satisfiable!"
Sat -> do -- Query a/b
res <- (,) <$> getValue a <*> getValue b
unless (res == (1, 1)) $ error $ "Didn't get (1,1): " ++ show res
|
