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
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Uninterpreted.Sort
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test suite for uninterpreted sorts
-----------------------------------------------------------------------------
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Uninterpreted.Sort(tests) where
import Utils.SBVTestFramework
data L
mkUninterpretedSort ''L
tests :: TestTree
tests =
testGroup "Uninterpreted.Sort"
[ testCase "unint-sort"
(assert . (==4) . length . (extractModels :: AllSatResult -> [L]) =<< allSat p0)
]
len :: SL -> SInteger
len = uninterpret "len"
p0 :: Symbolic SBool
p0 = do
[l, l0, l1] <- symbolics ["l", "l0", "l1"]
constrain $ len l0 .== 0
constrain $ len l1 .== 1
x :: SInteger <- symbolic "x"
constrain $ x .== 0 .|| x.== 1
return $ l .== l0 .|| l .== l1
|
