{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Grisette.Backend.TermRewritingTests
  ( termRewritingTests,
    validateSpec,
    bitwuzlaConfig,
  )
where

import Data.Foldable (traverse_)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeLits (KnownNat, type (<=))
import Grisette
  ( AlgReal,
    BitCast (bitCast),
    GrisetteSMTConfig,
    IEEEFPConstants
      ( fpMaxNormalized,
        fpMaxSubnormal,
        fpMinNormalized,
        fpMinSubnormal,
        fpNaN,
        fpNegativeInfinite,
        fpNegativeZero,
        fpPositiveInfinite,
        fpPositiveZero
      ),
    IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
    ITEOp (symIte),
    IntN,
    LinkedRep,
    LogicalOp (symNot, true),
    Solvable (con),
    SymBool (SymBool),
    SymFP,
    SymIEEEFPTraits (symFpIsNaN),
    SymRep (SymType),
    WordN,
    bitwuzla,
    fpIsNaN,
    solve,
    z3,
  )
import Grisette.Backend.TermRewritingGen
  ( BoolOnlySpec (BoolOnlySpec),
    BoolWithFixedSizedBVSpec (BoolWithFixedSizedBVSpec),
    BoolWithLIASpec,
    DifferentSizeBVSpec,
    FPRoundingModeBoolOpSpec,
    FPRoundingModeSpec,
    FixedSizedBVWithBoolSpec (FixedSizedBVWithBoolSpec),
    GeneralSpec,
    IEEEFPBoolOpSpec (IEEEFPBoolOpSpec),
    IEEEFPSpec,
    LIAWithBoolSpec,
    NRAWithBoolSpec,
    TermRewritingSpec
      ( conSpec,
        counterExample,
        norewriteVer,
        rewriteVer,
        same,
        symSpec,
        wrap
      ),
    absNumSpec,
    addNumSpec,
    andBitsSpec,
    andSpec,
    bitCastOrSpec,
    bitCastSpec,
    bvconcatSpec,
    bvextendSpec,
    bvselectSpec,
    complementBitsSpec,
    divIntegralSpec,
    eqvSpec,
    fpBinaryOpSpec,
    fpFMASpec,
    fpRoundingBinarySpec,
    fpRoundingUnaryOpSpec,
    fpTraitSpec,
    fromFPOrSpec,
    iteSpec,
    leOrdSpec,
    modIntegralSpec,
    mulNumSpec,
    negNumSpec,
    notSpec,
    orBitsSpec,
    orSpec,
    quotIntegralSpec,
    remIntegralSpec,
    shiftLeftSpec,
    shiftRightSpec,
    signumNumSpec,
    toFPSpec,
    xorBitsSpec,
  )
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp ((.&&)))
import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((./=), (.==)))
import Grisette.Internal.Core.Data.Class.SymIEEEFP
  ( SymIEEEFPTraits (symFpIsPositiveInfinite),
  )
import Grisette.Internal.SymPrim.FP
  ( ConvertibleBound (convertibleLowerBound, convertibleUpperBound),
    FP,
    FP32,
    FPRoundingMode,
    ValidFP,
    nextFP,
    prevFP,
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( FPBinaryOp (FPMaximum, FPMaximumNumber, FPMinimum, FPMinimumNumber, FPRem),
    FPRoundingBinaryOp (FPAdd, FPDiv, FPMul, FPSub),
    FPRoundingUnaryOp (FPRoundToIntegral, FPSqrt),
    FPTrait (FPIsPositive),
    PEvalBVTerm,
    PEvalBitCastOrTerm,
    PEvalBitCastTerm,
    PEvalBitwiseTerm (pevalAndBitsTerm, pevalOrBitsTerm),
    PEvalIEEEFPConvertibleTerm,
    PEvalShiftTerm,
    SupportedNonFuncPrim,
    Term,
    andBitsTerm,
    andTerm,
    bvConcatTerm,
    bvExtendTerm,
    complementBitsTerm,
    conTerm,
    eqTerm,
    fpTraitTerm,
    iteTerm,
    notTerm,
    orBitsTerm,
    orTerm,
    pformatTerm,
    ssymTerm,
    xorBitsTerm,
  )
import Grisette.Internal.SymPrim.SymFP (SymFP32)
import Test.Framework (Test, TestName, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (Assertion, assertFailure, (@?=))
import Test.QuickCheck
  ( Arbitrary,
    elements,
    forAll,
    ioProperty,
    mapSize,
    vectorOf,
    withMaxSuccess,
    (==>),
  )
import Type.Reflection (Typeable, typeRep)

validateSpec' ::
  (TermRewritingSpec a av) =>
  GrisetteSMTConfig ->
  SymBool ->
  a ->
  Assertion
validateSpec' config precond a = do
  r <- solve config (precond .&& SymBool (counterExample a))
  rs <- solve config (precond .&& SymBool (same a))
  case (r, rs) of
    (Left _, Right _) -> do
      return ()
    (Left _, Left err) -> do
      print err
      assertFailure $
        "Bad rewriting with unsolvable formula: "
          ++ pformatTerm (norewriteVer a)
          ++ " was rewritten to "
          ++ pformatTerm (rewriteVer a)
          ++ " under precondition"
          ++ show precond
          ++ " corresponding same formula:"
          ++ pformatTerm (same a)
    (Right m, _) -> do
      assertFailure $
        "With model"
          ++ show m
          ++ "Bad rewriting: "
          ++ pformatTerm (norewriteVer a)
          ++ " was rewritten to "
          ++ pformatTerm (rewriteVer a)
          ++ " under precondition"
          ++ show precond
          ++ " corresponding cex formula:"
          ++ pformatTerm (counterExample a)
          ++ "\n"
          ++ show (norewriteVer a)
          ++ "\n"
          ++ show (rewriteVer a)
          ++ "\n"
          ++ show (counterExample a)

validateSpec ::
  (TermRewritingSpec a av) =>
  GrisetteSMTConfig ->
  a ->
  Assertion
validateSpec config = validateSpec' config true

bitwuzlaConfig :: IO (Maybe GrisetteSMTConfig)
bitwuzlaConfig = do
  v <-
    solve bitwuzla $
      (("x" :: SymFP32) ./= "x")
        .&& symNot (symFpIsPositiveInfinite (con $ -4.7e-38 :: SymFP32))
        .&& ( symIte
                "bool"
                (con fpPositiveInfinite :: SymFP32)
                (con fpNegativeInfinite)
                .== "m"
            )
  case v of
    Left _ -> return Nothing
    Right _ -> return $ Just bitwuzla

onlyWhenBitwuzlaIsAvailable :: (GrisetteSMTConfig -> IO ()) -> IO ()
onlyWhenBitwuzlaIsAvailable action = do
  config <- bitwuzlaConfig
  case config of
    Just config -> action config
    Nothing ->
      putStrLn $
        "bitwuzla isn't available in the system, or the dependent sbv"
          <> " library does not work well with it. This test is marked as "
          <> " success."

unboundedConfig = z3

divisionTest ::
  forall a b.
  (TermRewritingSpec a b, Enum b, Num b) =>
  TestName ->
  (a -> a -> a) ->
  Test
divisionTest name f =
  testGroup
    name
    [ testCase "on concrete" $ do
        traverse_
          ( \(x :: b, y :: b) -> do
              validateSpec @a unboundedConfig $ f (conSpec x) (conSpec y)
          )
          [(i, j) | i <- [-3 .. 3], j <- [-3 .. 3]],
      testCase "on single concrete" $ do
        traverse_
          ( \x -> do
              validateSpec @a unboundedConfig $ f (conSpec x) (symSpec "a")
              validateSpec @a unboundedConfig $ f (symSpec "a") (conSpec x)
          )
          [-3 .. 3]
    ]

bvConcatTest ::
  forall bv.
  ( forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (bv n),
    forall n. (KnownNat n, 1 <= n) => PEvalShiftTerm (bv n),
    forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n),
    Typeable bv,
    PEvalBVTerm bv
  ) =>
  Test
bvConcatTest =
  testGroup (show (typeRep @bv) <> "_concat") $
    ( do
        (opName, opSpec, termOp) <-
          [ ("and", andBitsSpec, andBitsTerm),
            ("or", orBitsSpec, orBitsTerm),
            ("xor", xorBitsSpec, xorBitsTerm)
          ]
        [ testCase (opName <> "(const,concat)") $ do
            let lhs = conSpec 0x39 :: FixedSizedBVWithBoolSpec bv 8
            let rhs =
                  bvconcatSpec
                    (symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
                    (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
            let spec = opSpec lhs rhs
            validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec,
          testCase (opName <> "(concat,concat)") $ do
            let lhs =
                  bvconcatSpec
                    (symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
                    (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
            let rhs =
                  bvconcatSpec
                    (symSpec "c" :: FixedSizedBVWithBoolSpec bv 4)
                    (symSpec "d" :: FixedSizedBVWithBoolSpec bv 4)
            let spec@(FixedSizedBVWithBoolSpec _ r) = opSpec lhs rhs
            let expected =
                  ( bvConcatTerm
                      (termOp (ssymTerm "a" :: Term (bv 4)) (ssymTerm "c"))
                      (termOp (ssymTerm "b" :: Term (bv 4)) (ssymTerm "d"))
                  )
            r @?= expected
            validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
          ]
    )
      ++ [ testCase "complement(concat)" $ do
             let lhs =
                   bvconcatSpec
                     (symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
                     (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
             let spec@(FixedSizedBVWithBoolSpec _ r) = complementBitsSpec lhs
             let expected =
                   bvConcatTerm
                     (complementBitsTerm (ssymTerm "a" :: Term (bv 4)))
                     (complementBitsTerm (ssymTerm "b" :: Term (bv 4)))
             r @?= expected
             validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec,
           testCase "complement(sext)" $ do
             let spec@(FixedSizedBVWithBoolSpec _ r) =
                   complementBitsSpec
                     ( bvextendSpec
                         True
                         (Proxy :: Proxy 8)
                         (symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
                     ) ::
                     FixedSizedBVWithBoolSpec bv 8
             let expected =
                   bvExtendTerm
                     True
                     (Proxy :: Proxy 8)
                     (complementBitsTerm (ssymTerm "a" :: Term (bv 4)))
             r @?= expected
             validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec,
           testCase "and(leading_zero_then_all_one, b)" $ do
             let spec =
                   andBitsSpec
                     (conSpec 0x1f)
                     (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
             validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
           testCase "and(leading_one_then_all_zero, b)" $ do
             let spec =
                   andBitsSpec
                     (conSpec 0xf8)
                     (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
             validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
           testCase "or(leading_zero_then_all_one, b)" $ do
             let spec =
                   orBitsSpec
                     (conSpec 0x1f)
                     (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
             validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
           testCase "or(leading_one_then_all_zero, b)" $ do
             let spec =
                   orBitsSpec
                     (conSpec 0xf8)
                     (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
             validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
           testCase "select(sext)with_part_base" $ do
             let spec =
                   bvselectSpec
                     (Proxy @2)
                     (Proxy @4)
                     ( bvextendSpec
                         True
                         (Proxy @8)
                         (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4) ::
                         FixedSizedBVWithBoolSpec bv 8
                     ) ::
                     FixedSizedBVWithBoolSpec bv 4
             validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec,
           testCase "ite(cond,concat(a,b),concat(c,d))" $ do
             let spec@(FixedSizedBVWithBoolSpec _ r) =
                   iteSpec
                     (symSpec "cond" :: BoolWithFixedSizedBVSpec bv 4)
                     ( bvconcatSpec
                         (symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
                         (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
                     )
                     ( bvconcatSpec
                         (symSpec "c" :: FixedSizedBVWithBoolSpec bv 4)
                         (symSpec "d" :: FixedSizedBVWithBoolSpec bv 4)
                     )
             let expected =
                   bvConcatTerm
                     ( iteTerm
                         (ssymTerm "cond" :: Term Bool)
                         (ssymTerm "a" :: Term (bv 4))
                         (ssymTerm "c" :: Term (bv 4))
                     )
                     ( iteTerm
                         (ssymTerm "cond" :: Term Bool)
                         (ssymTerm "b" :: Term (bv 4))
                         (ssymTerm "d" :: Term (bv 4))
                     )
             r @?= expected
             validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
         ]
      ++ ( do
             pos <- [True, False]
             cvalue <- [0 :: Int, -1]
             value <- [0 :: Int, -1]
             let con = conSpec (fromIntegral value) :: FixedSizedBVWithBoolSpec bv 4
             let sym = symSpec "b"
             let t = if pos then con else sym
             let f = if pos then sym else con
             let spec =
                   iteSpec
                     ( eqvSpec
                         (symSpec "c" :: FixedSizedBVWithBoolSpec bv 1)
                         (conSpec $ fromIntegral cvalue) ::
                         BoolWithFixedSizedBVSpec bv 1
                     )
                     t
                     f
             let ts = if pos then show value else "sym"
             let fs = if pos then "sym" else show value
             return
               $ testCase
                 ( "ite(bv1="
                     <> show cvalue
                     <> ","
                     <> ts
                     <> ","
                     <> fs
                     <> ")"
                 )
               $ validateSpec unboundedConfig spec
         )
      ++ ( do
             let cond = symSpec "cond" :: BoolWithFixedSizedBVSpec bv 1
             let condTerm = ssymTerm "cond" :: Term Bool
             (opName, op, opSpec) <-
               [ ("and", andBitsTerm, andBitsSpec),
                 ("or", orBitsTerm, orBitsSpec),
                 ("xor", xorBitsTerm, xorBitsSpec),
                 ("ite", iteTerm condTerm, iteSpec cond)
               ]
             let name = opName <> "(sext,sext)"
             let spec@(FixedSizedBVWithBoolSpec _ r) =
                   opSpec
                     ( bvextendSpec
                         True
                         (Proxy :: Proxy 8)
                         (symSpec "a" :: FixedSizedBVWithBoolSpec bv 4)
                     )
                     ( bvextendSpec
                         True
                         (Proxy :: Proxy 8)
                         (symSpec "b" :: FixedSizedBVWithBoolSpec bv 4)
                     )
             let expected =
                   bvExtendTerm
                     True
                     (Proxy :: Proxy 8)
                     ( op
                         (ssymTerm "a" :: Term (bv 4))
                         (ssymTerm "b" :: Term (bv 4))
                     )
             return $ testCase name $ do
               r @?= expected
               validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
         )
      ++ ( do
             let a = symSpec "a" :: FixedSizedBVWithBoolSpec bv 4
             let b = symSpec "b" :: FixedSizedBVWithBoolSpec bv 4
             let c = symSpec "c" :: FixedSizedBVWithBoolSpec bv 4
             let cond = symSpec "cond" :: BoolWithFixedSizedBVSpec bv 1
             (lhs, rhs, lhsName, rhsName) <-
               [ (andBitsSpec a b, a, "(& a b)", "a"),
                 (andBitsSpec a b, b, "(& a b)", "b"),
                 (a, andBitsSpec a b, "a", "(& a b)"),
                 (b, andBitsSpec a b, "b", "(& a b)"),
                 (orBitsSpec a b, a, "(| a b)", "a"),
                 (orBitsSpec a b, b, "(| a b)", "b"),
                 (a, orBitsSpec a b, "a", "(| a b)"),
                 (b, orBitsSpec a b, "b", "(| a b)"),
                 (andBitsSpec a b, andBitsSpec a c, "(& a b)", "(& a c)"),
                 (andBitsSpec a b, andBitsSpec c a, "(& a b)", "(& c a)"),
                 (andBitsSpec a b, andBitsSpec b c, "(& a b)", "(& b c)"),
                 (andBitsSpec a b, andBitsSpec c b, "(& a b)", "(& c b)"),
                 (orBitsSpec a b, orBitsSpec a c, "(| a b)", "(| a c)"),
                 (orBitsSpec a b, orBitsSpec c a, "(| a b)", "(| c a)"),
                 (orBitsSpec a b, orBitsSpec b c, "(| a b)", "(| b c)"),
                 (orBitsSpec a b, orBitsSpec c b, "(| a b)", "(| c b)")
               ]
             let spec = iteSpec cond lhs rhs
             return $
               testCase ("ite(cond," <> lhsName <> "," <> rhsName <> ")") $
                 validateSpec @(FixedSizedBVWithBoolSpec bv 4) unboundedConfig spec
         )
      ++ ( do
             trueBranch <- [True, False]
             (opName, spec) <-
               [("and", andBitsSpec), ("or", orBitsSpec)]
             let iteName = "ite(cond,const,const)"
             let name =
                   opName
                     <> "("
                     <> (if trueBranch then iteName else "a")
                     <> ","
                     <> (if trueBranch then "b" else iteName)
                     <> ")"
             return $ testProperty name $ \a b -> ioProperty $ do
               let ite =
                     iteSpec
                       (symSpec "cond" :: BoolWithFixedSizedBVSpec bv 4)
                       (conSpec a :: FixedSizedBVWithBoolSpec bv 4)
                       (conSpec b :: FixedSizedBVWithBoolSpec bv 4)
               let s = symSpec "a" :: FixedSizedBVWithBoolSpec bv 4
               let lhs = if trueBranch then ite else s
               let rhs = if trueBranch then s else ite
               let resSpec = spec lhs rhs
               validateSpec unboundedConfig resSpec
         )
      ++ ( do
             a <- [0, 1, 4, 7, 8, 9, 16]
             (opName, opSpec) <-
               [ ("shr", shiftRightSpec),
                 ("shl", shiftLeftSpec)
               ]
             return $ testCase (opName <> "(bv8," <> show a <> ")") $ do
               let spec =
                     opSpec
                       (symSpec "a" :: FixedSizedBVWithBoolSpec bv 8)
                       (conSpec a)
               validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
         )
      ++ ( do
             trueBranch <- [True, False]
             innerTrueBranch <- [True, False]
             let l = symSpec "l" :: FixedSizedBVWithBoolSpec bv 8
             let r = symSpec "r" :: FixedSizedBVWithBoolSpec bv 8
             let cond = symSpec "cond" :: BoolWithFixedSizedBVSpec bv 8
             (absorbing, absorbingTerm, absorbingValueName, opName, opSpec, opTerm) <-
               [ ( conSpec 0 :: FixedSizedBVWithBoolSpec bv 8,
                   conTerm 0 :: Term (bv 8),
                   "0",
                   "and",
                   andBitsSpec,
                   andBitsTerm
                 ),
                 ( conSpec $ -1 :: FixedSizedBVWithBoolSpec bv 8,
                   conTerm $ -1 :: Term (bv 8),
                   "-1",
                   "or",
                   orBitsSpec,
                   orBitsTerm
                 )
               ]
             let condTerm = ssymTerm "cond" :: Term Bool
             let lTerm = ssymTerm "l" :: Term (bv 8)
             let rTerm = ssymTerm "r" :: Term (bv 8)

             let (lhsName, lhs, lhsResultTerm)
                   | trueBranch && innerTrueBranch = ("ite(cond," <> absorbingValueName <> ",l)", iteSpec cond absorbing l, absorbingTerm)
                   | trueBranch && not innerTrueBranch = ("ite(cond,l," <> absorbingValueName <> ")", iteSpec cond l absorbing, opTerm lTerm rTerm)
                   | otherwise = ("l", l, if innerTrueBranch then absorbingTerm else opTerm lTerm rTerm)
             let (rhsName, rhs, rhsResultTerm)
                   | trueBranch = ("r", r, if innerTrueBranch then opTerm lTerm rTerm else absorbingTerm)
                   | innerTrueBranch = ("ite(cond," <> absorbingValueName <> ",r)", iteSpec cond absorbing r, opTerm lTerm rTerm)
                   | otherwise = ("ite(cond,r," <> absorbingValueName <> ")", iteSpec cond r absorbing, absorbingTerm)
             let spec@(FixedSizedBVWithBoolSpec _ rspec) = opSpec lhs rhs
             return $ testCase (opName <> "(" <> lhsName <> "," <> rhsName <> ")") $ do
               rspec @?= iteTerm condTerm lhsResultTerm rhsResultTerm
               validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
         )
      ++ ( do
             innerTrueBranch <- [0 :: Int, -1]
             let innerFalseBranch = -1 - innerTrueBranch
             lhsIsExtend <- [True, False]
             let extendName =
                   "sext(ite(cond,"
                     <> show innerTrueBranch
                     <> ","
                     <> show innerFalseBranch
                     <> "))"
             (opName, opSpec, opTerm) <-
               [ ("and", andBitsSpec, pevalAndBitsTerm),
                 ("or", orBitsSpec, pevalOrBitsTerm)
               ]
             let name =
                   opName
                     <> if lhsIsExtend then "(" <> extendName <> ",c)" else "(c," <> extendName <> ")"
             return $
               testCase name $
                 do
                   let extend =
                         bvextendSpec
                           True
                           (Proxy :: Proxy 8)
                           ( iteSpec
                               (symSpec "cond" :: BoolWithFixedSizedBVSpec bv 1)
                               (conSpec $ fromIntegral innerTrueBranch :: FixedSizedBVWithBoolSpec bv 4)
                               (conSpec $ fromIntegral innerFalseBranch :: FixedSizedBVWithBoolSpec bv 4)
                           ) ::
                           FixedSizedBVWithBoolSpec bv 8
                   let single = symSpec "c" :: FixedSizedBVWithBoolSpec bv 8
                   let spec@(FixedSizedBVWithBoolSpec _ r) =
                         if lhsIsExtend
                           then opSpec extend single
                           else opSpec single extend
                   let expected =
                         iteTerm
                           (ssymTerm "cond" :: Term Bool)
                           (opTerm (conTerm $ fromIntegral innerTrueBranch) (ssymTerm "c"))
                           (opTerm (conTerm $ fromIntegral innerFalseBranch) (ssymTerm "c"))
                   r @?= expected
                   validateSpec @(FixedSizedBVWithBoolSpec bv 8) unboundedConfig spec
         )

bv1Test ::
  forall bv.
  ( SupportedNonFuncPrim (bv 1),
    Num (bv 1),
    Typeable bv,
    PEvalBitwiseTerm (bv 1)
  ) =>
  Test
bv1Test =
  testGroup (show (typeRep @bv) <> " 1") $
    ( do
        (opName, op, v, bvop) <-
          [ ("||", orSpec, 0, andBitsTerm),
            ("||", orSpec, 1, orBitsTerm),
            ("&&", andSpec, 0, orBitsTerm),
            ("&&", andSpec, 1, andBitsTerm)
          ]
        let isV = "==" <> show v
        let name = "(a" <> isV <> ")" <> opName <> "(b" <> isV <> ")"
        let spec@(BoolWithFixedSizedBVSpec _ r) =
              op
                (eqvSpec (symSpec "a" :: FixedSizedBVWithBoolSpec bv 1) (conSpec v))
                (eqvSpec (symSpec "b" :: FixedSizedBVWithBoolSpec bv 1) (conSpec v))
        let expected =
              eqTerm
                ( bvop
                    (ssymTerm "a" :: Term (bv 1))
                    (ssymTerm "b")
                )
                (conTerm v)
        return $ testCase name $ do
          r @?= expected
          validateSpec @(BoolWithFixedSizedBVSpec bv 1) unboundedConfig spec
    )
      ++ ( do
             cond <- [0 :: bv 1, 1]
             t <- [0 :: bv 1, 1]
             let f = 1 - t
             let name = "ite(a==" <> show cond <> "," <> show t <> "," <> show f <> ")"
             let spec@(FixedSizedBVWithBoolSpec _ r) =
                   iteSpec
                     ( eqvSpec
                         (symSpec "a" :: FixedSizedBVWithBoolSpec bv 1)
                         (conSpec cond) ::
                         BoolWithFixedSizedBVSpec bv 1
                     )
                     (conSpec t)
                     (conSpec f)
             let aTerm = ssymTerm "a" :: Term (bv 1)
             let expected =
                   if t == cond
                     then aTerm
                     else complementBitsTerm aTerm
             return $ testCase name $ do
               r @?= expected
               validateSpec @(FixedSizedBVWithBoolSpec bv 1) unboundedConfig spec
         )
      ++ [ testCase "(a==b)==(a==c)" $ do
             let spec@(BoolWithFixedSizedBVSpec _ r) =
                   eqvSpec
                     (eqvSpec (symSpec "a" :: FixedSizedBVWithBoolSpec bv 1) (symSpec "b") :: BoolWithFixedSizedBVSpec bv 1)
                     (eqvSpec (symSpec "a" :: FixedSizedBVWithBoolSpec bv 1) (symSpec "c"))
             validateSpec @(BoolWithFixedSizedBVSpec bv 1)
               unboundedConfig
               spec
             r @?= eqTerm (ssymTerm "b" :: Term (bv 1)) (ssymTerm "c")
         ]

termRewritingTests :: Test
termRewritingTests =
  testGroup
    "TermRewriting"
    [ bv1Test @WordN,
      bv1Test @IntN,
      bvConcatTest @WordN,
      bvConcatTest @IntN,
      testGroup
        "Bool only"
        [ testProperty "Bool only random test" $
            mapSize (`min` 10) $
              ioProperty . \(x :: BoolOnlySpec) -> do
                validateSpec unboundedConfig x,
          testCase "Regression nested ite with (ite a (ite b c d) e) with b is true" $ do
            validateSpec @BoolOnlySpec
              unboundedConfig
              ( iteSpec
                  (symSpec "a" :: BoolOnlySpec)
                  ( iteSpec
                      (orSpec (notSpec (andSpec (symSpec "b1") (symSpec "b2"))) (symSpec "b2") :: BoolOnlySpec)
                      (symSpec "c")
                      (symSpec "d")
                  )
                  (symSpec "e")
              ),
          testCase "Regression for pevalImpliesTerm _ false should be false" $ do
            validateSpec @BoolOnlySpec
              unboundedConfig
              ( iteSpec
                  (symSpec "fbool" :: BoolOnlySpec)
                  ( notSpec
                      ( orSpec
                          (orSpec (notSpec (andSpec (symSpec "gbool" :: BoolOnlySpec) (symSpec "fbool" :: BoolOnlySpec))) (symSpec "gbool" :: BoolOnlySpec))
                          (orSpec (symSpec "abool" :: BoolOnlySpec) (notSpec (andSpec (symSpec "gbool" :: BoolOnlySpec) (symSpec "bbool" :: BoolOnlySpec))))
                      )
                  )
                  (symSpec "xxx" :: BoolOnlySpec)
              ),
          testCase "And absortion" $ do
            let spec@(BoolOnlySpec _ r) =
                  andSpec
                    (orSpec (symSpec "c") (orSpec (symSpec "b") (symSpec "a")))
                    (andSpec (symSpec "a") (andSpec (symSpec "d") (symSpec "e")))
            validateSpec @BoolOnlySpec
              unboundedConfig
              spec
            r @?= andTerm (ssymTerm "a") (andTerm (ssymTerm "d") (ssymTerm "e")),
          testCase "Or absorption" $ do
            let spec@(BoolOnlySpec _ r) =
                  orSpec
                    (andSpec (symSpec "c") (andSpec (symSpec "b") (symSpec "a")))
                    (orSpec (symSpec "a") (orSpec (symSpec "d") (symSpec "e")))
            validateSpec @BoolOnlySpec
              unboundedConfig
              spec
            r @?= orTerm (ssymTerm "a") (orTerm (ssymTerm "d") (ssymTerm "e")),
          testCase "(a==b)==(a==c)" $ do
            let spec@(BoolOnlySpec _ r) =
                  eqvSpec
                    (eqvSpec (symSpec "a" :: BoolOnlySpec) (symSpec "b") :: BoolOnlySpec)
                    (eqvSpec (symSpec "a" :: BoolOnlySpec) (symSpec "c"))
            validateSpec @BoolOnlySpec
              unboundedConfig
              spec
            r @?= eqTerm (ssymTerm "b" :: Term Bool) (ssymTerm "c")
        ],
      testGroup
        "LIA"
        [ testProperty "LIA random test" $
            mapSize (`min` 10) $
              ioProperty . \(x :: LIAWithBoolSpec) -> do
                validateSpec unboundedConfig x,
          testCase "Regression nested ite with (ite a b (ite c d e)) with c implies a" $ do
            validateSpec @LIAWithBoolSpec
              unboundedConfig
              ( iteSpec
                  (notSpec (eqvSpec (symSpec "v" :: LIAWithBoolSpec) (conSpec 1 :: LIAWithBoolSpec) :: BoolWithLIASpec))
                  (symSpec "b")
                  ( iteSpec
                      (eqvSpec (symSpec "v" :: LIAWithBoolSpec) (conSpec 2 :: LIAWithBoolSpec) :: BoolWithLIASpec)
                      (symSpec "d")
                      (symSpec "d")
                  )
              )
        ],
      testGroup
        "NRA"
        [ testProperty "NRA random test" $
            mapSize (`min` 5) $
              ioProperty . \(x :: NRAWithBoolSpec) ->
                validateSpec unboundedConfig x
        ],
      testGroup
        "Different sized signed BV"
        [ testProperty "Random test" $
            withMaxSuccess 1000 . mapSize (`min` 5) $
              ioProperty . \(x :: (DifferentSizeBVSpec IntN 4)) -> do
                validateSpec unboundedConfig x
        ],
      testGroup
        "Fixed sized signed BV"
        [ testProperty "Random test on IntN 1" $
            withMaxSuccess 200 . mapSize (`min` 5) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 1)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on IntN 2" $
            withMaxSuccess 200 . mapSize (`min` 5) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 2)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on IntN 4" $
            withMaxSuccess 200 . mapSize (`min` 5) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 4)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on IntN 63" $
            withMaxSuccess 200 . mapSize (`min` 1) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 63)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on IntN 64" $
            withMaxSuccess 200 . mapSize (`min` 1) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 64)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on IntN 65" $
            withMaxSuccess 200 . mapSize (`min` 1) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 65)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on IntN 128" $
            withMaxSuccess 200 . mapSize (`min` 1) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec IntN 128)) -> do
                validateSpec unboundedConfig x
        ],
      testGroup
        "Different sized unsigned BV"
        [ testProperty "random test" $
            withMaxSuccess 1000 . mapSize (`min` 5) $
              ioProperty . \(x :: (DifferentSizeBVSpec WordN 4)) -> do
                validateSpec unboundedConfig x
        ],
      testGroup
        "Fixed sized unsigned BV"
        [ testProperty "Random test on WordN 1" $
            withMaxSuccess 200 . mapSize (`min` 5) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 1)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on WordN 2" $
            withMaxSuccess 200 . mapSize (`min` 5) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 2)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on WordN 4" $
            withMaxSuccess 200 . mapSize (`min` 5) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 4)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on WordN 63" $
            withMaxSuccess 200 . mapSize (`min` 1) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 63)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on WordN 64" $
            withMaxSuccess 200 . mapSize (`min` 1) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 64)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on WordN 65" $
            withMaxSuccess 200 . mapSize (`min` 1) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 65)) -> do
                validateSpec unboundedConfig x,
          testProperty "Random test on WordN 128" $
            withMaxSuccess 200 . mapSize (`min` 1) $
              ioProperty . \(x :: (FixedSizedBVWithBoolSpec WordN 128)) -> do
                validateSpec unboundedConfig x
        ],
      testCase "Regression: shift twice and the sum of shift amount overflows" $ do
        validateSpec @(FixedSizedBVWithBoolSpec IntN 4)
          unboundedConfig
          ( shiftRightSpec
              (shiftRightSpec (symSpec "fint") (conSpec 0x5))
              (conSpec 0x5)
          ),
      testGroup
        "Regression for abs on unsigned BV"
        [ testCase "abs on negate" $
            validateSpec @(FixedSizedBVWithBoolSpec WordN 4)
              unboundedConfig
              (absNumSpec (negNumSpec (symSpec "a"))),
          testCase "abs on times negate" $
            validateSpec @(FixedSizedBVWithBoolSpec WordN 4)
              unboundedConfig
              (absNumSpec (mulNumSpec (symSpec "a") (negNumSpec (symSpec "b"))))
        ],
      testGroup
        "mulNumSpec on integer"
        [ testCase "times on both concrete" $ do
            traverse_
              (\(x, y) -> validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) (conSpec y))
              [(i, j) | i <- [-3 .. 3], j <- [-3 .. 3]],
          testCase "times on single concrete" $ do
            traverse_
              ( \x -> do
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) (symSpec "a")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (symSpec "a") (conSpec x)
              )
              [-3 .. 3],
          testCase "Two times with two concrete combined" $ do
            traverse_
              ( \(x, y) -> do
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ mulNumSpec (conSpec y) (symSpec "a")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ mulNumSpec (symSpec "a") (conSpec y)
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (conSpec x) (symSpec "a")) (conSpec y)
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (symSpec "a") (conSpec x)) (conSpec y)
              )
              [(i, j) | i <- [-3 .. 3], j <- [-3 .. 3]],
          testCase "Two times with one concrete" $ do
            traverse_
              ( \x -> do
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ mulNumSpec (symSpec "b") (symSpec "a")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (symSpec "b") $ mulNumSpec (symSpec "a") (conSpec x)
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (symSpec "b") $ mulNumSpec (conSpec x) (symSpec "a")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (conSpec x) (symSpec "a")) (symSpec "b")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (symSpec "a") (conSpec x)) (symSpec "b")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (mulNumSpec (symSpec "a") (symSpec "b")) (conSpec x)
              )
              [-3 .. 3],
          testCase "times and add with two concretes combined" $ do
            traverse_
              ( \(x, y) -> do
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ addNumSpec (conSpec y) (symSpec "a")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) $ addNumSpec (symSpec "a") (conSpec y)
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (addNumSpec (conSpec x) (symSpec "a")) (conSpec y)
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (addNumSpec (symSpec "a") (conSpec x)) (conSpec y)
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ addNumSpec (conSpec x) $ mulNumSpec (conSpec y) (symSpec "a")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ addNumSpec (conSpec x) $ mulNumSpec (symSpec "a") (conSpec y)
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ addNumSpec (mulNumSpec (conSpec x) (symSpec "a")) (conSpec y)
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ addNumSpec (mulNumSpec (symSpec "a") (conSpec x)) (conSpec y)
              )
              [(i, j) | i <- [-3 .. 3], j <- [-3 .. 3]],
          testCase "times concrete with negNumSpec symbolic" $ do
            traverse_
              ( \x -> do
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (conSpec x) (negNumSpec $ symSpec "a")
                  validateSpec @(GeneralSpec Integer) unboundedConfig $ mulNumSpec (negNumSpec $ symSpec "a") (conSpec x)
              )
              [-3 .. 3]
        ],
      testGroup
        "divisions on integer"
        [ divisionTest @(GeneralSpec Integer) "div" divIntegralSpec,
          divisionTest @(GeneralSpec Integer) "mod" modIntegralSpec,
          divisionTest @(GeneralSpec Integer) "quot" quotIntegralSpec,
          divisionTest @(GeneralSpec Integer) "rem" remIntegralSpec
        ],
      testGroup
        "divisions on signed bv"
        [ divisionTest @(GeneralSpec (IntN 4)) "div" divIntegralSpec,
          divisionTest @(GeneralSpec (IntN 4)) "mod" modIntegralSpec,
          divisionTest @(GeneralSpec (IntN 4)) "quot" quotIntegralSpec,
          divisionTest @(GeneralSpec (IntN 4)) "rem" remIntegralSpec
        ],
      testGroup
        "divisions on unsigned bv"
        [ divisionTest @(GeneralSpec (WordN 4)) "div" divIntegralSpec,
          divisionTest @(GeneralSpec (WordN 4)) "mod" modIntegralSpec,
          divisionTest @(GeneralSpec (WordN 4)) "quot" quotIntegralSpec,
          divisionTest @(GeneralSpec (WordN 4)) "rem" remIntegralSpec
        ],
      testGroup
        "FP"
        [ testCase "0.0 == -0.0" $
            onlyWhenBitwuzlaIsAvailable
              ( `validateSpec`
                  ( eqvSpec
                      (conSpec 0.0 :: IEEEFPSpec 5 11)
                      (conSpec $ -0.0) ::
                      IEEEFPBoolOpSpec 5 11
                  )
              ),
          testCase "-0.0 <= -0.0" $
            onlyWhenBitwuzlaIsAvailable
              ( `validateSpec`
                  ( leOrdSpec
                      (conSpec 0.0 :: IEEEFPSpec 5 11)
                      (conSpec $ -0.0) ::
                      IEEEFPBoolOpSpec 5 11
                  )
              ),
          testCase "is_pos(nan)" $
            onlyWhenBitwuzlaIsAvailable
              ( `validateSpec`
                  ( fpTraitSpec
                      FPIsPositive
                      (conSpec fpNaN :: IEEEFPSpec 5 11) ::
                      IEEEFPBoolOpSpec 5 11
                  )
              ),
          testCase "is_pos(+inf)" $
            onlyWhenBitwuzlaIsAvailable
              ( `validateSpec`
                  ( fpTraitSpec
                      FPIsPositive
                      ( iteSpec
                          (symSpec "bool" :: BoolOnlySpec)
                          (conSpec fpNegativeInfinite)
                          (conSpec fpPositiveInfinite) ::
                          IEEEFPSpec 5 11
                      ) ::
                      IEEEFPBoolOpSpec 5 11
                  )
              ),
          testCase "regression 2" $
            onlyWhenBitwuzlaIsAvailable
              ( `validateSpec`
                  ( eqvSpec
                      (signumNumSpec (conSpec (1.175e-38) :: IEEEFPSpec 5 11))
                      (symSpec "b") ::
                      IEEEFPBoolOpSpec 5 11
                  )
              ),
          testCase "test sbv bug mitigation sbv#702" $
            onlyWhenBitwuzlaIsAvailable
              ( flip validateSpec $
                  IEEEFPBoolOpSpec
                    ( fpTraitTerm
                        FPIsPositive
                        ( iteTerm
                            (ssymTerm "bool")
                            (conTerm fpNegativeInfinite :: Term FP32)
                            (conTerm fpPositiveInfinite :: Term FP32)
                        )
                    )
                    (notTerm $ ssymTerm "bool")
              ),
          testProperty "FP32BoolOp" $
            withMaxSuccess 1000 . mapSize (`min` 10) $
              ioProperty . \(x :: IEEEFPBoolOpSpec 5 11) ->
                onlyWhenBitwuzlaIsAvailable (`validateSpec` x),
          testProperty "FPRoundingModeBoolOpSpec" $
            mapSize (`min` 10) $
              ioProperty . \(x :: FPRoundingModeBoolOpSpec) ->
                onlyWhenBitwuzlaIsAvailable (`validateSpec` x),
          testGroup "fpBinaryOp" $ do
            op <-
              [FPMaximum, FPMinimum, FPMaximumNumber, FPMinimumNumber, FPRem]
            return $ testCase (show op) $ do
              let lst =
                    [ conSpec fpNegativeInfinite,
                      conSpec fpPositiveInfinite,
                      conSpec fpNaN,
                      conSpec fpPositiveZero,
                      conSpec fpNegativeZero,
                      conSpec 1,
                      conSpec (-1),
                      symSpec "a",
                      symSpec "b"
                    ]
              let ps =
                    [ fpBinaryOpSpec op l r :: IEEEFPSpec 4 4
                    | l <- lst,
                      r <- lst
                    ]
              traverse_ (validateSpec z3) ps,
          testGroup "RoundingOp" $ do
            let rdgen =
                  elements
                    [ conSpec rna :: FPRoundingModeSpec,
                      conSpec rne,
                      conSpec rtz,
                      conSpec rtp,
                      conSpec rtn
                    ]
            let vgen =
                  elements
                    [ conSpec fpNegativeInfinite :: IEEEFPSpec 4 4,
                      conSpec fpPositiveInfinite,
                      conSpec fpNaN,
                      conSpec fpPositiveZero,
                      conSpec fpNegativeZero,
                      conSpec 120,
                      conSpec 60,
                      conSpec 1,
                      conSpec 2,
                      conSpec 3,
                      conSpec 4,
                      conSpec (-1),
                      conSpec (-2),
                      conSpec (-3),
                      conSpec (-4),
                      conSpec 1.5625e-2,
                      conSpec 2.4e2,
                      conSpec 1.953125e-3,
                      conSpec 1.3671875e-2,
                      symSpec "a",
                      symSpec "b"
                    ]
            [ testGroup "fpRoundingUnaryOp" $ do
                op <- [FPSqrt, FPRoundToIntegral]
                return $
                  testProperty (show op) $
                    forAll rdgen $ \rd ->
                      forAll vgen $ \v ->
                        ioProperty $
                          validateSpec z3 $
                            fpRoundingUnaryOpSpec op rd v,
              testGroup "fpRoundingBinaryOp" $ do
                op <- [FPAdd, FPSub, FPMul, FPDiv]
                return $
                  testProperty (show op) $
                    forAll rdgen $ \rd ->
                      forAll (vectorOf 2 vgen) $ \[l, r] ->
                        ioProperty $
                          validateSpec z3 $
                            fpRoundingBinarySpec op rd l r,
              testProperty "fma" $
                forAll rdgen $ \rd ->
                  forAll (vectorOf 3 vgen) $ \[x, y, z] ->
                    ioProperty $
                      validateSpec z3 $
                        fpFMASpec rd x y z
              ]
        ],
      testGroup "bitCast" $ do
        let bitCastCase ::
              forall a b.
              ( Arbitrary a,
                PEvalBitCastTerm a b,
                SupportedNonFuncPrim a,
                SupportedNonFuncPrim b
              ) =>
              Test
            bitCastCase = testProperty
              (show (typeRep @a) <> " -> " <> show (typeRep @b))
              $ \x ->
                withMaxSuccess 10 . ioProperty $
                  validateSpec
                    z3
                    ( bitCastSpec (conSpec x :: GeneralSpec a) ::
                        GeneralSpec b
                    )
        let fromFPCase ::
              forall a b.
              ( Arbitrary a,
                Arbitrary b,
                PEvalBitCastOrTerm a b,
                RealFloat a,
                SupportedNonFuncPrim a,
                SupportedNonFuncPrim b
              ) =>
              Test
            fromFPCase = testProperty
              (show (typeRep @a) <> " -> " <> show (typeRep @b))
              $ \d x ->
                withMaxSuccess 10 . (not (isNaN x) ==>) . ioProperty $
                  validateSpec
                    z3
                    ( bitCastOrSpec
                        (conSpec d :: GeneralSpec b)
                        (conSpec x :: GeneralSpec a)
                    )
        let toFPCase ::
              forall a b.
              ( Arbitrary a,
                PEvalBitCastTerm a b,
                RealFloat b,
                SupportedNonFuncPrim a,
                SupportedNonFuncPrim b
              ) =>
              Test
            toFPCase = testProperty
              (show (typeRep @a) <> " -> " <> show (typeRep @b))
              $ \x ->
                withMaxSuccess 10
                  . (not (isNaN (bitCast x :: b)) ==>)
                  . ioProperty
                  $ validateSpec
                    z3
                    ( bitCastSpec (conSpec x :: GeneralSpec a) ::
                        GeneralSpec b
                    )
        [ bitCastCase @(IntN 4) @(WordN 4),
          bitCastCase @(WordN 4) @(IntN 4),
          bitCastCase @(IntN 1) @Bool,
          bitCastCase @(WordN 1) @Bool,
          bitCastCase @Bool @(IntN 1),
          bitCastCase @Bool @(WordN 1),
          fromFPCase @(FP 3 5) @(IntN 8),
          fromFPCase @(FP 3 5) @(WordN 8),
          toFPCase @(IntN 8) @(FP 3 5),
          toFPCase @(WordN 8) @(FP 3 5)
          ],
      testGroup "FPConvertible" $ do
        let fromFPAssertion ::
              forall eb sb spec b.
              ( ValidFP eb sb,
                PEvalIEEEFPConvertibleTerm b,
                TermRewritingSpec spec b
              ) =>
              b ->
              FPRoundingMode ->
              FP eb sb ->
              IO ()
            fromFPAssertion d rd x
              | fpIsNaN x = return ()
              | otherwise =
                  validateSpec'
                    z3
                    ( con x
                        .== p
                        .&& symNot (symFpIsNaN p)
                    )
                    ( fromFPOrSpec
                        (conSpec d :: spec)
                        (conSpec rd :: GeneralSpec FPRoundingMode)
                        ( wrap (ssymTerm "p") (conTerm x) ::
                            GeneralSpec (FP eb sb)
                        ) ::
                        spec
                    )
              where
                p = "p" :: SymFP eb sb
            fromFPAssertionDirect ::
              forall eb sb spec b.
              ( ValidFP eb sb,
                PEvalIEEEFPConvertibleTerm b,
                TermRewritingSpec spec b
              ) =>
              b ->
              FPRoundingMode ->
              FP eb sb ->
              IO ()
            fromFPAssertionDirect d rd x =
              validateSpec
                z3
                ( fromFPOrSpec
                    (conSpec d :: spec)
                    (conSpec rd :: GeneralSpec FPRoundingMode)
                    (conSpec x :: GeneralSpec (FP eb sb))
                )
            fromFPCase ::
              forall eb sb spec b.
              ( ValidFP eb sb,
                Arbitrary b,
                PEvalIEEEFPConvertibleTerm b,
                TermRewritingSpec spec b
              ) =>
              Bool ->
              Test
            fromFPCase direct = testProperty
              (show (typeRep @(FP eb sb)) <> " -> " <> show (typeRep @b))
              $ \(d :: b) rd (x :: FP eb sb) ->
                withMaxSuccess 10 . ioProperty $
                  ( if direct
                      then fromFPAssertionDirect @eb @sb @spec
                      else fromFPAssertion @eb @sb @spec
                  )
                    d
                    rd
                    x
            toFPAssertion ::
              forall eb sb b bs.
              ( ValidFP eb sb,
                PEvalIEEEFPConvertibleTerm b,
                LinkedRep b bs,
                Solvable b bs,
                SupportedNonFuncPrim b,
                SymEq bs
              ) =>
              FPRoundingMode ->
              b ->
              IO ()
            toFPAssertion rd x =
              validateSpec'
                z3
                ((con x :: SymType b) .== "p")
                ( toFPSpec
                    (conSpec rd :: GeneralSpec FPRoundingMode)
                    (wrap (ssymTerm "p") (conTerm x) :: GeneralSpec b) ::
                    IEEEFPSpec eb sb
                )
            toFPAssertionFP ::
              forall eb sb eb0 sb0.
              ( ValidFP eb sb,
                ValidFP eb0 sb0
              ) =>
              FPRoundingMode ->
              FP eb0 sb0 ->
              IO ()
            toFPAssertionFP _ x | fpIsNaN x = return ()
            toFPAssertionFP rd x =
              validateSpec'
                z3
                ( con x
                    .== p
                    .&& symNot (symFpIsNaN p)
                )
                ( toFPSpec
                    (conSpec rd :: GeneralSpec FPRoundingMode)
                    ( wrap (ssymTerm "p") (conTerm x) ::
                        GeneralSpec (FP eb0 sb0)
                    ) ::
                    IEEEFPSpec eb sb
                )
              where
                p = "p" :: SymFP eb0 sb0
            toFPCase ::
              forall eb sb b bs.
              ( ValidFP eb sb,
                Arbitrary b,
                PEvalIEEEFPConvertibleTerm b,
                SupportedNonFuncPrim b,
                LinkedRep b bs,
                Solvable b bs,
                SymEq bs
              ) =>
              Test
            toFPCase = testProperty
              (show (typeRep @b) <> " -> " <> show (typeRep @(FP eb sb)))
              $ \rd (x :: b) ->
                withMaxSuccess 10 . ioProperty $
                  toFPAssertion @eb @sb rd x
            toFPCaseFP ::
              forall eb sb eb0 sb0.
              ( ValidFP eb sb,
                ValidFP eb0 sb0
              ) =>
              Test
            toFPCaseFP = testProperty
              ( show (typeRep @(FP eb0 sb0))
                  <> " -> "
                  <> show (typeRep @(FP eb sb))
              )
              $ \rd (x :: b) ->
                withMaxSuccess 10 . ioProperty $
                  toFPAssertionFP @eb @sb @eb0 @sb0 rd x
            specialFps :: (ValidFP eb sb) => [FP eb sb]
            specialFps =
              [ fpPositiveZero,
                fpNegativeZero,
                fpPositiveInfinite,
                fpNegativeInfinite,
                fpNaN,
                fpMaxNormalized,
                fpMinNormalized,
                fpMaxSubnormal,
                fpMinSubnormal
              ]
            boundFps ::
              (ConvertibleBound bv, KnownNat n, 1 <= n, ValidFP eb sb) =>
              bv n ->
              FPRoundingMode ->
              [FP eb sb]
            boundFps n mode =
              [ convertibleLowerBound n mode,
                convertibleUpperBound n mode
              ]
            fps ::
              (ConvertibleBound bv, KnownNat n, 1 <= n, ValidFP eb sb) =>
              bv n ->
              FPRoundingMode ->
              [FP eb sb]
            fps n mode =
              specialFps
                ++ boundFps n mode
                ++ (nextFP <$> boundFps n mode)
                ++ (prevFP <$> boundFps n mode)
            boundedFromFPCase ::
              forall bv n eb sb.
              ( ConvertibleBound bv,
                KnownNat n,
                1 <= n,
                ValidFP eb sb,
                PEvalIEEEFPConvertibleTerm (bv n),
                SupportedNonFuncPrim (bv n),
                Num (bv n),
                Typeable bv
              ) =>
              FPRoundingMode ->
              Test
            boundedFromFPCase mode =
              testCase (show (typeRep @bv) ++ "/" ++ show mode) $
                mapM_
                  ( fromFPAssertion @eb @sb @(GeneralSpec (bv n))
                      123
                      mode
                  )
                  (fps (undefined :: (bv n)) mode)
            boundedFromFPTestGroup ::
              forall n eb sb.
              ( KnownNat n,
                1 <= n,
                ValidFP eb sb
              ) =>
              Test
            boundedFromFPTestGroup =
              testGroup
                ( show (typeRep @(FP eb sb))
                    ++ " -> "
                    ++ show (typeRep @(IntN n))
                    ++ "/"
                    ++ show (typeRep @(WordN n))
                )
                $ do
                  mode <- [rna, rne, rtz, rtp, rtn]
                  [ boundedFromFPCase @IntN @n @eb @sb mode,
                    boundedFromFPCase @WordN @n @eb @sb mode
                    ]
        [ -- z3 is buggy with the indirect encoding
          -- https://github.com/Z3Prover/z3/issues/7321
          fromFPCase @4 @4 @(GeneralSpec AlgReal) True,
          toFPCase @4 @4 @AlgReal,
          testCase "FP 4 4 -> Integer" $ do
            sequence_ $
              (fromFPAssertionDirect @4 @4 @(GeneralSpec Integer) 0)
                <$> [rna, rne, rtz, rtp, rtn]
                <*> (specialFps ++ ((/ 4) . fromIntegral <$> [-7 .. 7])),
          toFPCase @4 @4 @Integer,
          fromFPCase @4 @4 @(IEEEFPSpec 3 3) False,
          toFPCaseFP @4 @4 @3 @3,
          fromFPCase @4 @4 @(IEEEFPSpec 5 5) False,
          toFPCaseFP @4 @4 @5 @5,
          toFPCase @4 @4 @(WordN 8),
          toFPCase @4 @4 @(IntN 8),
          boundedFromFPTestGroup @32 @4 @4,
          boundedFromFPTestGroup @12 @4 @16,
          boundedFromFPTestGroup @12 @4 @12,
          boundedFromFPTestGroup @12 @4 @11,
          boundedFromFPTestGroup @12 @4 @10,
          boundedFromFPTestGroup @12 @4 @9,
          boundedFromFPTestGroup @12 @4 @2,
          boundedFromFPTestGroup @10 @4 @16,
          boundedFromFPTestGroup @10 @4 @10,
          boundedFromFPTestGroup @10 @4 @9,
          boundedFromFPTestGroup @10 @4 @8,
          boundedFromFPTestGroup @10 @4 @7,
          boundedFromFPTestGroup @10 @4 @2,
          boundedFromFPTestGroup @9 @4 @16,
          boundedFromFPTestGroup @9 @4 @9,
          boundedFromFPTestGroup @9 @4 @8,
          boundedFromFPTestGroup @9 @4 @7,
          boundedFromFPTestGroup @9 @4 @6,
          boundedFromFPTestGroup @9 @4 @2,
          boundedFromFPTestGroup @8 @4 @16,
          boundedFromFPTestGroup @8 @4 @8,
          boundedFromFPTestGroup @8 @4 @7,
          boundedFromFPTestGroup @8 @4 @6,
          boundedFromFPTestGroup @8 @4 @5,
          boundedFromFPTestGroup @8 @4 @2,
          boundedFromFPTestGroup @7 @4 @16,
          boundedFromFPTestGroup @7 @4 @7,
          boundedFromFPTestGroup @7 @4 @6,
          boundedFromFPTestGroup @7 @4 @5,
          boundedFromFPTestGroup @7 @4 @4,
          boundedFromFPTestGroup @7 @4 @2,
          boundedFromFPTestGroup @5 @4 @16,
          boundedFromFPTestGroup @5 @4 @5,
          boundedFromFPTestGroup @5 @4 @4,
          boundedFromFPTestGroup @5 @4 @3,
          boundedFromFPTestGroup @5 @4 @2
          ]
    ]