liquid-fixpoint-0.9.6.3.4: tests/tasty/ghc-9.12.1/SimplifyKVarTests.hs
{-# LANGUAGE MultilineStrings #-}
module SimplifyKVarTests (tests) where
import Control.Monad (when)
import qualified Data.HashSet as HashSet
import Language.Fixpoint.Parse
import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Solver.Solution as F
import Test.Tasty
import Test.Tasty.HUnit
tests :: TestTree
tests =
testGroup "simplifyKVar" $ map simplificationTest
[ SimplificationTest
{ name = "single elimination"
, expected = """
exists [y : int] . P C y
"""
, input = """
exists [x : int, y : int] . x == C && P x y
"""
}
, SimplificationTest
{ name = "full elimination"
, expected = """
P C D
"""
, input = """
exists [x : int, y : int] . x == C && P x y && y == D
"""
}
, SimplificationTest
{ name = "alpha equivalence"
, expected = """
(exists [w : int, z : int] . Q w z) &&
(exists [w : int, z : int] . P w z)
"""
, input = """
(exists [w : int, z : int] . Q w z) &&
(exists [w : int, z : int] . P w z) &&
(exists [x : int, y : int] . P x y)
"""
}
, SimplificationTest
{ name = "floating"
, expected = """
(exists [x : int, y : int] . P x y) && A == C
"""
, input = """
exists [x : int, y : int] . A == C && P x y
"""
}
, SimplificationTest
{ name = "inner floating"
, expected = """
(exists [x : int] . P x && Q x) && (exists [y : int] . P y)
"""
, input = """
exists [x : int] . P x && (exists [ y : int] . P y && Q x)
"""
}
, largeSimplificationTest
]
data SimplificationTest = SimplificationTest
{ input :: String
, expected :: String
, name :: String
}
simplificationTest :: SimplificationTest -> TestTree
simplificationTest test =
testCase (name test) $ do
let actual =
F.simplifyKVar
HashSet.empty
(doParse'' True predP (name test) (input test))
expectedE = doParse'' True predP (name test) (expected test)
when (not (F.alphaEq HashSet.empty actual expectedE)) $ do
assertFailure $ unlines
[ "output is not as expected"
, "Expected:"
, expected test
, ""
, "Actual:"
, F.showpp actual
]
largeSimplificationTest :: SimplificationTest
largeSimplificationTest =
SimplificationTest
{ name = "large simplification"
, expected = """
exists [w : int] . Test.gt0xy w i##aS7
"""
, input = """
exists [VV##1821##k_ : int,
i##aS7##k_ : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
lq_tmpx##1823##k_ : int,
lq_tmpx##1824##k_ : int]
. (exists [w : int,
w2 : int,
x : int,
y : Tuple0,
VV##F##13 : int]
. VV##1821##k_ == VV##F##13
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1823##k_ == w
&& lq_tmpx##1824##k_ == x
&& (exists [VV##1829 : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
VV##1805##k_ : int,
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
i##aS7##k_ : int]
. VV##1829 == w
&& VV##1805##k_ == w
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& (exists [VV##F##3 : int]
. Test.gt0xy VV##F##3 i##aS7
&& VV##1805##k_ == VV##F##3
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& (exists [VV##1830 : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
i##aS7##k_ : int,
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
VV##1807##k_ : int]
. VV##1830 == w2
&& VV##1807##k_ == w2
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& (exists [w : int,
VV##F##14 : int,
lq_rnmx##255 : Tuple0]
. (exists [VV##1828 : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
VV##1805##k_ : int,
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
i##aS7##k_ : int]
. VV##1828 == w
&& VV##1805##k_ == w
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& (exists [VV##F##3 : int]
. Test.gt0xy VV##F##3 i##aS7
&& VV##1805##k_ == VV##F##3
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& (exists [lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
i##aS7##k_ : int,
lq_tmpx##1812##k_ : Tuple0,
VV##1809##k_ : int,
lq_tmpx##1811##k_ : int,
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int)]
. VV##1809##k_ == VV##F##14
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1811##k_ == w
&& lq_tmpx##1812##k_ == lq_rnmx##255
&& (exists [VV##F##12 : int,
lq_tmpx##1811 : int,
lq_tmpx##1812 : Tuple0,
lq_tmpdb##43 : int,
lq_tmpdb##44 : Tuple0]
. VV##F##12 == i##aS7
&& VV##1809##k_ == VV##F##12
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1811##k_ == lq_tmpx##1811
&& lq_tmpx##1812##k_ == lq_tmpx##1812))
&& (exists [i##aS7##k_ : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
lq_tmpx##1801 : Tuple0,
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
VV##1799##k_ : Tuple0]
. VV##1799##k_ == lq_rnmx##255
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1801 == lq_rnmx##255
&& (exists [VV##F##10 : Tuple0]
. VV##1799##k_ == VV##F##10
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& VV##1807##k_ == VV##F##14
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& (exists [i##aS7##k_ : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
lq_tmpx##1801 : Tuple0,
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
VV##1799##k_ : Tuple0]
. VV##1799##k_ == y
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1801 == y
&& (exists [VV##F##10 : Tuple0]
. VV##1799##k_ == VV##F##10
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& (exists [i##aS7##k_ : int,
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
lq_tmpx##1804 : int,
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
VV##1802##k_ : int]
. VV##1802##k_ == x
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1804 == x
&& (exists [VV##F##6 : int]
. (exists [i##aS7##k_ : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
VV##1796##k_ : int]
. VV##1796##k_ == VV##F##6
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& (exists [VV##F##7 : int]
. (exists [lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
i##aS7##k_ : int,
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
VV##1807##k_ : int]
. VV##1807##k_ == VV##F##7
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& (exists [w : int,
VV##F##14 : int,
lq_rnmx##255 : Tuple0]
. (exists [VV##1828 : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
VV##1805##k_ : int,
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
i##aS7##k_ : int]
. VV##1828 == w
&& VV##1805##k_ == w
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& (exists [VV##F##3 : int]
. Test.gt0xy VV##F##3 i##aS7
&& VV##1805##k_ == VV##F##3
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& (exists [lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
i##aS7##k_ : int,
lq_tmpx##1812##k_ : Tuple0,
VV##1809##k_ : int,
lq_tmpx##1811##k_ : int,
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int)]
. VV##1809##k_ == VV##F##14
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1811##k_ == w
&& lq_tmpx##1812##k_ == lq_rnmx##255
&& (exists [VV##F##12 : int,
lq_tmpx##1811 : int,
lq_tmpx##1812 : Tuple0,
lq_tmpdb##43 : int,
lq_tmpdb##44 : Tuple0]
. VV##F##12 == i##aS7
&& VV##1809##k_ == VV##F##12
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1811##k_ == lq_tmpx##1811
&& lq_tmpx##1812##k_ == lq_tmpx##1812))
&& (exists [i##aS7##k_ : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
lq_tmpx##1801 : Tuple0,
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
VV##1799##k_ : Tuple0]
. VV##1799##k_ == lq_rnmx##255
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1801 == lq_rnmx##255
&& (exists [VV##F##10 : Tuple0]
. VV##1799##k_ == VV##F##10
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& VV##1807##k_ == VV##F##14
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& VV##1796##k_ == VV##F##7
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb))
&& (exists [i##aS7##k_ : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
VV##1793##k_ : int]
. VV##1793##k_ == VV##F##6
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& (exists [VV##F##5 : int]
. VV##1793##k_ == VV##F##5
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb))
&& VV##1802##k_ == VV##F##6
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc))
&& (exists [lq_anf##7205759403792798200##d1cc##k_ : (Test.State int int),
lq_tmpx##1818##k_ : int,
lq_anf##7205759403792798198##d1ca##k_ : (GHC.Internal.Base.Monad (Test.State int)),
lq_tmpx##1817##k_ : int,
VV##1815##k_ : int,
lq_anf##7205759403792798199##d1cb##k_ : (Test.State int Tuple0),
i##aS7##k_ : int]
. VV##1815##k_ == VV##F##13
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1817##k_ == w2
&& lq_tmpx##1818##k_ == x
&& (exists [VV##F##8 : int,
lq_tmpx##1817 : int,
lq_tmpx##1818 : int,
lq_tmpdb##47 : int,
lq_tmpdb##48 : int]
. lq_tmpx##1818 == VV##F##8
&& VV##F##8 == lq_tmpx##1817
&& VV##1815##k_ == VV##F##8
&& i##aS7##k_ == i##aS7
&& lq_anf##7205759403792798198##d1ca##k_ == lq_anf##7205759403792798198##d1ca
&& lq_anf##7205759403792798199##d1cb##k_ == lq_anf##7205759403792798199##d1cb
&& lq_anf##7205759403792798200##d1cc##k_ == lq_anf##7205759403792798200##d1cc
&& lq_tmpx##1817##k_ == lq_tmpx##1817
&& lq_tmpx##1818##k_ == lq_tmpx##1818)))
"""
}