    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tuple
    -- Copyright : (c) Joel Burget
    --                 Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Accessing symbolic tuple fields and deconstruction.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DataKinds              #-}
    {-# LANGUAGE FlexibleContexts       #-}
    {-# LANGUAGE FlexibleInstances      #-}
    {-# LANGUAGE FunctionalDependencies #-}
    {-# LANGUAGE KindSignatures         #-}
    {-# LANGUAGE Rank2Types             #-}
    {-# LANGUAGE ScopedTypeVariables    #-}
    {-# LANGUAGE TypeApplications       #-}

    {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

    module Data.SBV.Tuple (
      -- * Symbolic field access
        (^.), _1, _2, _3, _4, _5, _6, _7, _8
      -- * Tupling and untupling
      , tuple, untuple
      -- * Swapping, only for 2-tuples
      , swap
      ) where

    import GHC.TypeLits

    import Data.SBV.Core.Data
    import Data.SBV.Core.Symbolic
    import Data.SBV.Core.Model

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> :set -XTypeApplications
    -- >>> import Data.SBV

    -- | Field access, inspired by the lens library. This is merely reverse
    -- application, but allows us to write things like @(1, 2)^._1@ which is
    -- likely to be familiar to most Haskell programmers out there. Note that
    -- this is precisely equivalent to @_1 (1, 2)@, but perhaps it reads a little
    -- nicer.
    (^.) :: a -> (a -> b) -> b
    a
    t ^. :: forall a b. a -> (a -> b) -> b
    ^. a -> b
    f = a -> b
    f a
    t
    infixl 8 ^.

    -- | Swap the elements of a 2-tuple
    swap :: (SymVal a, SymVal b) => STuple a b -> STuple b a
    swap :: forall a b. (SymVal a, SymVal b) => STuple a b -> STuple b a
    swap STuple a b
    t = (SBV b, SBV a) -> SBV (b, a)
    forall tup a. Tuple tup a => a -> SBV tup
    tuple (SBV b
    b, SBV a
    a)
      where (SBV a
    a, SBV b
    b) = STuple a b -> (SBV a, SBV b)
    forall tup a. Tuple tup a => SBV tup -> a
    untuple STuple a b
    t

    -- | Dynamic interface to exporting tuples, this function is not
    -- exported on purpose; use it only via the field functions '_1', '_2', etc.
    symbolicFieldAccess :: (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess :: forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    i SBV tup
    tup
      | Int
    1 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    i Bool -> Bool -> Bool
    || Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    lks
      = String -> SBV a
    forall a. String -> a
    bad (String -> SBV a) -> String -> SBV a
    forall a b. (a -> b) -> a -> b
    $ String
    "Index is out of bounds, " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is outside [1," String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    lks String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"
      | SBV (SVal Kind
    kval (Left CV
    v)) <- SBV tup
    tup
      = case CV -> CVal
    cvVal CV
    v of
          CTuple [CVal]
    vs | Kind
    kval      Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    ktup -> String -> SBV a
    forall a. String -> a
    bad (String -> SBV a) -> String -> SBV a
    forall a b. (a -> b) -> a -> b
    $ String
    "Kind/value mismatch: "      String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    kval
                    | [CVal] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [CVal]
    vs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    lks  -> String -> SBV a
    forall a. String -> a
    bad (String -> SBV a) -> String -> SBV a
    forall a b. (a -> b) -> a -> b
    $ String
    "Value has fewer elements: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    forall a. Show a => a -> String
    show (Kind -> CVal -> CV
    CV Kind
    kval ([CVal] -> CVal
    CTuple [CVal]
    vs))
                    | Bool
    True              -> a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal (a -> SBV a) -> a -> SBV a
    forall a b. (a -> b) -> a -> b
    $ CV -> a
    forall a. SymVal a => CV -> a
    fromCV (CV -> a) -> CV -> a
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    kElem ([CVal]
    vs [CVal] -> Int -> CVal
    forall a. HasCallStack => [a] -> Int -> a
    !! (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))
          CVal
    _                             -> String -> SBV a
    forall a. String -> a
    bad (String -> SBV a) -> String -> SBV a
    forall a b. (a -> b) -> a -> b
    $ String
    "Kind/value mismatch: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    forall a. Show a => a -> String
    show CV
    v
      | Bool
    True
      = SBV a
    forall a. SBV a
    symAccess
      where ktup :: Kind
    ktup = SBV tup -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV tup
    tup

            (Int
    lks, [Kind]
    eks) = case Kind
    ktup of
                           KTuple [Kind]
    ks -> ([Kind] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    ks, [Kind]
    ks)
                           Kind
    _         -> String -> (Int, [Kind])
    forall a. String -> a
    bad String
    "Was expecting to receive a tuple!"

            kElem :: Kind
    kElem = [Kind]
    eks [Kind] -> Int -> Kind
    forall a. HasCallStack => [a] -> Int -> a
    !! (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)

            bad :: String -> a
            bad :: forall a. String -> a
    bad String
    problem = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "*** Data.SBV.field: Impossible happened"
                                          , String
    "***   Accessing element: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
                                          , String
    "***   Argument kind    : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ktup
                                          , String
    "***   Problem          : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    problem
                                          , String
    "*** Please report this as a bug!"
                                          ]

            symAccess :: SBV a
            symAccess :: forall a. SBV a
    symAccess = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    kElem (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    y
              where y :: State -> IO SV
    y State
    st = do SV
    sv <- State -> SVal -> IO SV
    svToSV State
    st (SVal -> IO SV) -> SVal -> IO SV
    forall a b. (a -> b) -> a -> b
    $ SBV tup -> SVal
    forall a. SBV a -> SVal
    unSBV SBV tup
    tup
                              State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    kElem (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Int -> Op
    TupleAccess Int
    i Int
    lks) [SV
    sv])

    -- | Field labels
    data Label (l :: Symbol) = Get

    -- | The class 'HasField' captures the notion that a type has a certain field
    class (SymVal elt, HasKind tup) => HasField l elt tup | l tup -> elt where
      field :: Label l -> SBV tup -> SBV elt

    instance (HasKind a, HasKind b                                                                  , SymVal a) => HasField "_1" a (a, b)                   where field :: Label "_1" -> SBV (a, b) -> SBV a
    field Label "_1"
    _ = Int -> SBV (a, b) -> SBV a
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    1
    instance (HasKind a, HasKind b, HasKind c                                                       , SymVal a) => HasField "_1" a (a, b, c)                where field :: Label "_1" -> SBV (a, b, c) -> SBV a
    field Label "_1"
    _ = Int -> SBV (a, b, c) -> SBV a
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    1
    instance (HasKind a, HasKind b, HasKind c, HasKind d                                            , SymVal a) => HasField "_1" a (a, b, c, d)             where field :: Label "_1" -> SBV (a, b, c, d) -> SBV a
    field Label "_1"
    _ = Int -> SBV (a, b, c, d) -> SBV a
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    1
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal a) => HasField "_1" a (a, b, c, d, e)          where field :: Label "_1" -> SBV (a, b, c, d, e) -> SBV a
    field Label "_1"
    _ = Int -> SBV (a, b, c, d, e) -> SBV a
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    1
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f                      , SymVal a) => HasField "_1" a (a, b, c, d, e, f)       where field :: Label "_1" -> SBV (a, b, c, d, e, f) -> SBV a
    field Label "_1"
    _ = Int -> SBV (a, b, c, d, e, f) -> SBV a
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    1
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g           , SymVal a) => HasField "_1" a (a, b, c, d, e, f, g)    where field :: Label "_1" -> SBV (a, b, c, d, e, f, g) -> SBV a
    field Label "_1"
    _ = Int -> SBV (a, b, c, d, e, f, g) -> SBV a
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    1
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal a) => HasField "_1" a (a, b, c, d, e, f, g, h) where field :: Label "_1" -> SBV (a, b, c, d, e, f, g, h) -> SBV a
    field Label "_1"
    _ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV a
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    1

    instance (HasKind a, HasKind b                                                                  , SymVal b) => HasField "_2" b (a, b)                   where field :: Label "_2" -> SBV (a, b) -> SBV b
    field Label "_2"
    _ = Int -> SBV (a, b) -> SBV b
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    2
    instance (HasKind a, HasKind b, HasKind c                                                       , SymVal b) => HasField "_2" b (a, b, c)                where field :: Label "_2" -> SBV (a, b, c) -> SBV b
    field Label "_2"
    _ = Int -> SBV (a, b, c) -> SBV b
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    2
    instance (HasKind a, HasKind b, HasKind c, HasKind d                                            , SymVal b) => HasField "_2" b (a, b, c, d)             where field :: Label "_2" -> SBV (a, b, c, d) -> SBV b
    field Label "_2"
    _ = Int -> SBV (a, b, c, d) -> SBV b
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    2
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal b) => HasField "_2" b (a, b, c, d, e)          where field :: Label "_2" -> SBV (a, b, c, d, e) -> SBV b
    field Label "_2"
    _ = Int -> SBV (a, b, c, d, e) -> SBV b
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    2
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f                      , SymVal b) => HasField "_2" b (a, b, c, d, e, f)       where field :: Label "_2" -> SBV (a, b, c, d, e, f) -> SBV b
    field Label "_2"
    _ = Int -> SBV (a, b, c, d, e, f) -> SBV b
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    2
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g           , SymVal b) => HasField "_2" b (a, b, c, d, e, f, g)    where field :: Label "_2" -> SBV (a, b, c, d, e, f, g) -> SBV b
    field Label "_2"
    _ = Int -> SBV (a, b, c, d, e, f, g) -> SBV b
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    2
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal b) => HasField "_2" b (a, b, c, d, e, f, g, h) where field :: Label "_2" -> SBV (a, b, c, d, e, f, g, h) -> SBV b
    field Label "_2"
    _ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV b
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    2

    instance (HasKind a, HasKind b, HasKind c                                                       , SymVal c) => HasField "_3" c (a, b, c)                where field :: Label "_3" -> SBV (a, b, c) -> SBV c
    field Label "_3"
    _ = Int -> SBV (a, b, c) -> SBV c
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    3
    instance (HasKind a, HasKind b, HasKind c, HasKind d                                            , SymVal c) => HasField "_3" c (a, b, c, d)             where field :: Label "_3" -> SBV (a, b, c, d) -> SBV c
    field Label "_3"
    _ = Int -> SBV (a, b, c, d) -> SBV c
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    3
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal c) => HasField "_3" c (a, b, c, d, e)          where field :: Label "_3" -> SBV (a, b, c, d, e) -> SBV c
    field Label "_3"
    _ = Int -> SBV (a, b, c, d, e) -> SBV c
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    3
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f                      , SymVal c) => HasField "_3" c (a, b, c, d, e, f)       where field :: Label "_3" -> SBV (a, b, c, d, e, f) -> SBV c
    field Label "_3"
    _ = Int -> SBV (a, b, c, d, e, f) -> SBV c
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    3
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g           , SymVal c) => HasField "_3" c (a, b, c, d, e, f, g)    where field :: Label "_3" -> SBV (a, b, c, d, e, f, g) -> SBV c
    field Label "_3"
    _ = Int -> SBV (a, b, c, d, e, f, g) -> SBV c
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    3
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal c) => HasField "_3" c (a, b, c, d, e, f, g, h) where field :: Label "_3" -> SBV (a, b, c, d, e, f, g, h) -> SBV c
    field Label "_3"
    _ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV c
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    3

    instance (HasKind a, HasKind b, HasKind c, HasKind d                                            , SymVal d) => HasField "_4" d (a, b, c, d)             where field :: Label "_4" -> SBV (a, b, c, d) -> SBV d
    field Label "_4"
    _ = Int -> SBV (a, b, c, d) -> SBV d
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    4
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal d) => HasField "_4" d (a, b, c, d, e)          where field :: Label "_4" -> SBV (a, b, c, d, e) -> SBV d
    field Label "_4"
    _ = Int -> SBV (a, b, c, d, e) -> SBV d
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    4
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f                      , SymVal d) => HasField "_4" d (a, b, c, d, e, f)       where field :: Label "_4" -> SBV (a, b, c, d, e, f) -> SBV d
    field Label "_4"
    _ = Int -> SBV (a, b, c, d, e, f) -> SBV d
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    4
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g           , SymVal d) => HasField "_4" d (a, b, c, d, e, f, g)    where field :: Label "_4" -> SBV (a, b, c, d, e, f, g) -> SBV d
    field Label "_4"
    _ = Int -> SBV (a, b, c, d, e, f, g) -> SBV d
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    4
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal d) => HasField "_4" d (a, b, c, d, e, f, g, h) where field :: Label "_4" -> SBV (a, b, c, d, e, f, g, h) -> SBV d
    field Label "_4"
    _ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV d
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    4

    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal e) => HasField "_5" e (a, b, c, d, e)          where field :: Label "_5" -> SBV (a, b, c, d, e) -> SBV e
    field Label "_5"
    _ = Int -> SBV (a, b, c, d, e) -> SBV e
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    5
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f                      , SymVal e) => HasField "_5" e (a, b, c, d, e, f)       where field :: Label "_5" -> SBV (a, b, c, d, e, f) -> SBV e
    field Label "_5"
    _ = Int -> SBV (a, b, c, d, e, f) -> SBV e
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    5
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g           , SymVal e) => HasField "_5" e (a, b, c, d, e, f, g)    where field :: Label "_5" -> SBV (a, b, c, d, e, f, g) -> SBV e
    field Label "_5"
    _ = Int -> SBV (a, b, c, d, e, f, g) -> SBV e
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    5
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal e) => HasField "_5" e (a, b, c, d, e, f, g, h) where field :: Label "_5" -> SBV (a, b, c, d, e, f, g, h) -> SBV e
    field Label "_5"
    _ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV e
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    5

    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f                      , SymVal f) => HasField "_6" f (a, b, c, d, e, f)       where field :: Label "_6" -> SBV (a, b, c, d, e, f) -> SBV f
    field Label "_6"
    _ = Int -> SBV (a, b, c, d, e, f) -> SBV f
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    6
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g           , SymVal f) => HasField "_6" f (a, b, c, d, e, f, g)    where field :: Label "_6" -> SBV (a, b, c, d, e, f, g) -> SBV f
    field Label "_6"
    _ = Int -> SBV (a, b, c, d, e, f, g) -> SBV f
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    6
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal f) => HasField "_6" f (a, b, c, d, e, f, g, h) where field :: Label "_6" -> SBV (a, b, c, d, e, f, g, h) -> SBV f
    field Label "_6"
    _ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV f
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    6

    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g           , SymVal g) => HasField "_7" g (a, b, c, d, e, f, g)    where field :: Label "_7" -> SBV (a, b, c, d, e, f, g) -> SBV g
    field Label "_7"
    _ = Int -> SBV (a, b, c, d, e, f, g) -> SBV g
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    7
    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal g) => HasField "_7" g (a, b, c, d, e, f, g, h) where field :: Label "_7" -> SBV (a, b, c, d, e, f, g, h) -> SBV g
    field Label "_7"
    _ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV g
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    7

    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal h) => HasField "_8" h (a, b, c, d, e, f, g, h) where field :: Label "_8" -> SBV (a, b, c, d, e, f, g, h) -> SBV h
    field Label "_8"
    _ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV h
    forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
    symbolicFieldAccess Int
    8

    -- | Access the 1st element of an @STupleN@, @2 <= N <= 8@. Also see '^.'.
    _1 :: HasField "_1" b a => SBV a -> SBV b
    _1 :: forall b a. HasField "_1" b a => SBV a -> SBV b
    _1 = Label "_1" -> SBV a -> SBV b
    forall (l :: Symbol) elt tup.
    HasField l elt tup =>
    Label l -> SBV tup -> SBV elt
    field (forall (l :: Symbol). Label l
    Get @"_1")

    -- | Access the 2nd element of an @STupleN@, @2 <= N <= 8@. Also see '^.'.
    _2 :: HasField "_2" b a => SBV a -> SBV b
    _2 :: forall b a. HasField "_2" b a => SBV a -> SBV b
    _2 = Label "_2" -> SBV a -> SBV b
    forall (l :: Symbol) elt tup.
    HasField l elt tup =>
    Label l -> SBV tup -> SBV elt
    field (forall (l :: Symbol). Label l
    Get @"_2")

    -- | Access the 3rd element of an @STupleN@, @3 <= N <= 8@. Also see '^.'.
    _3 :: HasField "_3" b a => SBV a -> SBV b
    _3 :: forall b a. HasField "_3" b a => SBV a -> SBV b
    _3 = Label "_3" -> SBV a -> SBV b
    forall (l :: Symbol) elt tup.
    HasField l elt tup =>
    Label l -> SBV tup -> SBV elt
    field (forall (l :: Symbol). Label l
    Get @"_3")

    -- | Access the 4th element of an @STupleN@, @4 <= N <= 8@. Also see '^.'.
    _4 :: HasField "_4" b a => SBV a -> SBV b
    _4 :: forall b a. HasField "_4" b a => SBV a -> SBV b
    _4 = Label "_4" -> SBV a -> SBV b
    forall (l :: Symbol) elt tup.
    HasField l elt tup =>
    Label l -> SBV tup -> SBV elt
    field (forall (l :: Symbol). Label l
    Get @"_4")

    -- | Access the 5th element of an @STupleN@, @5 <= N <= 8@. Also see '^.'.
    _5 :: HasField "_5" b a => SBV a -> SBV b
    _5 :: forall b a. HasField "_5" b a => SBV a -> SBV b
    _5 = Label "_5" -> SBV a -> SBV b
    forall (l :: Symbol) elt tup.
    HasField l elt tup =>
    Label l -> SBV tup -> SBV elt
    field (forall (l :: Symbol). Label l
    Get @"_5")

    -- | Access the 6th element of an @STupleN@, @6 <= N <= 8@. Also see '^.'.
    _6 :: HasField "_6" b a => SBV a -> SBV b
    _6 :: forall b a. HasField "_6" b a => SBV a -> SBV b
    _6 = Label "_6" -> SBV a -> SBV b
    forall (l :: Symbol) elt tup.
    HasField l elt tup =>
    Label l -> SBV tup -> SBV elt
    field (forall (l :: Symbol). Label l
    Get @"_6")

    -- | Access the 7th element of an @STupleN@, @7 <= N <= 8@. Also see '^.'.
    _7 :: HasField "_7" b a => SBV a -> SBV b
    _7 :: forall b a. HasField "_7" b a => SBV a -> SBV b
    _7 = Label "_7" -> SBV a -> SBV b
    forall (l :: Symbol) elt tup.
    HasField l elt tup =>
    Label l -> SBV tup -> SBV elt
    field (forall (l :: Symbol). Label l
    Get @"_7")

    -- | Access the 8th element of an @STupleN@, @8 <= N <= 8@. Also see '^.'.
    _8 :: HasField "_8" b a => SBV a -> SBV b
    _8 :: forall b a. HasField "_8" b a => SBV a -> SBV b
    _8 = Label "_8" -> SBV a -> SBV b
    forall (l :: Symbol) elt tup.
    HasField l elt tup =>
    Label l -> SBV tup -> SBV elt
    field (forall (l :: Symbol). Label l
    Get @"_8")

    -- | Constructing a tuple from its parts and deconstructing back.
    class Tuple tup a | a -> tup, tup -> a where
      -- | Deconstruct a tuple, getting its constituent parts apart. Forms an
      -- isomorphism pair with 'tuple':
      --
      -- >>> prove $ \p -> tuple @(Integer, Bool, (String, Char)) (untuple p) .== p
      -- Q.E.D.
      untuple :: SBV tup -> a

      -- | Constructing a tuple from its parts. Forms an isomorphism pair with 'untuple':
      --
      -- >>> prove $ \p -> untuple @(Integer, Bool, (String, Char)) (tuple p) .== p
      -- Q.E.D.
      tuple   :: a -> SBV tup

    instance (SymVal a, SymVal b) => Tuple (a, b) (SBV a, SBV b) where
      untuple :: SBV (a, b) -> (SBV a, SBV b)
    untuple SBV (a, b)
    p = (SBV (a, b)
    pSBV (a, b) -> (SBV (a, b) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1, SBV (a, b)
    pSBV (a, b) -> (SBV (a, b) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)

      tuple :: (SBV a, SBV b) -> SBV (a, b)
    tuple p :: (SBV a, SBV b)
    p@(SBV a
    sa, SBV b
    sb)
        | Just a
    a <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    sa, Just b
    b <- SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    sb
        = (a, b) -> SBV (a, b)
    forall a. SymVal a => a -> SBV a
    literal (a
    a, b
    b)
        | Bool
    True
        = SVal -> SBV (a, b)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (a, b)) -> SVal -> SBV (a, b)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
        where k :: Kind
    k      = (SBV a, SBV b) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (SBV a, SBV b)
    p
              res :: State -> IO SV
    res State
    st = do SV
    asv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    sa
                          SV
    bsv <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    sb
                          State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Op
    TupleConstructor Int
    2) [SV
    asv, SV
    bsv])

    instance (SymVal a, SymVal b, SymVal c)
          => Tuple (a, b, c) (SBV a, SBV b, SBV c) where
      untuple :: SBV (a, b, c) -> (SBV a, SBV b, SBV c)
    untuple SBV (a, b, c)
    p = (SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1, SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2, SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)

      tuple :: (SBV a, SBV b, SBV c) -> SBV (a, b, c)
    tuple p :: (SBV a, SBV b, SBV c)
    p@(SBV a
    sa, SBV b
    sb, SBV c
    sc)
        | Just a
    a <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    sa, Just b
    b <- SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    sb, Just c
    c <- SBV c -> Maybe c
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV c
    sc
        = (a, b, c) -> SBV (a, b, c)
    forall a. SymVal a => a -> SBV a
    literal (a
    a, b
    b, c
    c)
        | Bool
    True
        = SVal -> SBV (a, b, c)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (a, b, c)) -> SVal -> SBV (a, b, c)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
        where k :: Kind
    k      = (SBV a, SBV b, SBV c) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (SBV a, SBV b, SBV c)
    p
              res :: State -> IO SV
    res State
    st = do SV
    asv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    sa
                          SV
    bsv <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    sb
                          SV
    csv <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    sc
                          State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Op
    TupleConstructor Int
    3) [SV
    asv, SV
    bsv, SV
    csv])

    instance (SymVal a, SymVal b, SymVal c, SymVal d)
          => Tuple (a, b, c, d) (SBV a, SBV b, SBV c, SBV d) where
      untuple :: SBV (a, b, c, d) -> (SBV a, SBV b, SBV c, SBV d)
    untuple SBV (a, b, c, d)
    p = (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1, SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2, SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3, SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)

      tuple :: (SBV a, SBV b, SBV c, SBV d) -> SBV (a, b, c, d)
    tuple p :: (SBV a, SBV b, SBV c, SBV d)
    p@(SBV a
    sa, SBV b
    sb, SBV c
    sc, SBV d
    sd)
        | Just a
    a <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    sa, Just b
    b <- SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    sb, Just c
    c <- SBV c -> Maybe c
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV c
    sc, Just d
    d <- SBV d -> Maybe d
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV d
    sd
        = (a, b, c, d) -> SBV (a, b, c, d)
    forall a. SymVal a => a -> SBV a
    literal (a
    a, b
    b, c
    c, d
    d)
        | Bool
    True
        = SVal -> SBV (a, b, c, d)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (a, b, c, d)) -> SVal -> SBV (a, b, c, d)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
        where k :: Kind
    k      = (SBV a, SBV b, SBV c, SBV d) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (SBV a, SBV b, SBV c, SBV d)
    p
              res :: State -> IO SV
    res State
    st = do SV
    asv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    sa
                          SV
    bsv <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    sb
                          SV
    csv <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    sc
                          SV
    dsv <- State -> SBV d -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV d
    sd
                          State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Op
    TupleConstructor Int
    4) [SV
    asv, SV
    bsv, SV
    csv, SV
    dsv])

    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e)
          => Tuple (a, b, c, d, e) (SBV a, SBV b, SBV c, SBV d, SBV e) where
      untuple :: SBV (a, b, c, d, e) -> (SBV a, SBV b, SBV c, SBV d, SBV e)
    untuple SBV (a, b, c, d, e)
    p = (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1, SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2, SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3, SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4, SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)

      tuple :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> SBV (a, b, c, d, e)
    tuple p :: (SBV a, SBV b, SBV c, SBV d, SBV e)
    p@(SBV a
    sa, SBV b
    sb, SBV c
    sc, SBV d
    sd, SBV e
    se)
        | Just a
    a <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    sa, Just b
    b <- SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    sb, Just c
    c <- SBV c -> Maybe c
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV c
    sc, Just d
    d <- SBV d -> Maybe d
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV d
    sd, Just e
    e <- SBV e -> Maybe e
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV e
    se
        = (a, b, c, d, e) -> SBV (a, b, c, d, e)
    forall a. SymVal a => a -> SBV a
    literal (a
    a, b
    b, c
    c, d
    d, e
    e)
        | Bool
    True
        = SVal -> SBV (a, b, c, d, e)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (a, b, c, d, e)) -> SVal -> SBV (a, b, c, d, e)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
        where k :: Kind
    k      = (SBV a, SBV b, SBV c, SBV d, SBV e) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (SBV a, SBV b, SBV c, SBV d, SBV e)
    p
              res :: State -> IO SV
    res State
    st = do SV
    asv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    sa
                          SV
    bsv <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    sb
                          SV
    csv <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    sc
                          SV
    dsv <- State -> SBV d -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV d
    sd
                          SV
    esv <- State -> SBV e -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV e
    se
                          State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Op
    TupleConstructor Int
    5) [SV
    asv, SV
    bsv, SV
    csv, SV
    dsv, SV
    esv])

    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f)
          => Tuple (a, b, c, d, e, f) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where
      untuple :: SBV (a, b, c, d, e, f)
    -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)
    untuple SBV (a, b, c, d, e, f)
    p = (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1, SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2, SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3, SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4, SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5, SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6)

      tuple :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)
    -> SBV (a, b, c, d, e, f)
    tuple p :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)
    p@(SBV a
    sa, SBV b
    sb, SBV c
    sc, SBV d
    sd, SBV e
    se, SBV f
    sf)
        | Just a
    a <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    sa, Just b
    b <- SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    sb, Just c
    c <- SBV c -> Maybe c
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV c
    sc, Just d
    d <- SBV d -> Maybe d
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV d
    sd, Just e
    e <- SBV e -> Maybe e
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV e
    se, Just f
    f <- SBV f -> Maybe f
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV f
    sf
        = (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f)
    forall a. SymVal a => a -> SBV a
    literal (a
    a, b
    b, c
    c, d
    d, e
    e, f
    f)
        | Bool
    True
        = SVal -> SBV (a, b, c, d, e, f)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (a, b, c, d, e, f)) -> SVal -> SBV (a, b, c, d, e, f)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
        where k :: Kind
    k      = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)
    p
              res :: State -> IO SV
    res State
    st = do SV
    asv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    sa
                          SV
    bsv <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    sb
                          SV
    csv <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    sc
                          SV
    dsv <- State -> SBV d -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV d
    sd
                          SV
    esv <- State -> SBV e -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV e
    se
                          SV
    fsv <- State -> SBV f -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV f
    sf
                          State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Op
    TupleConstructor Int
    6) [SV
    asv, SV
    bsv, SV
    csv, SV
    dsv, SV
    esv, SV
    fsv])

    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g)
          => Tuple (a, b, c, d, e, f, g) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where
      untuple :: SBV (a, b, c, d, e, f, g)
    -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
    untuple SBV (a, b, c, d, e, f, g)
    p = (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1, SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2, SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3, SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4, SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5, SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6, SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV g) -> SBV g
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV g
    forall b a. HasField "_7" b a => SBV a -> SBV b
    _7)

      tuple :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
    -> SBV (a, b, c, d, e, f, g)
    tuple p :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
    p@(SBV a
    sa, SBV b
    sb, SBV c
    sc, SBV d
    sd, SBV e
    se, SBV f
    sf, SBV g
    sg)
        | Just a
    a <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    sa, Just b
    b <- SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    sb, Just c
    c <- SBV c -> Maybe c
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV c
    sc, Just d
    d <- SBV d -> Maybe d
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV d
    sd, Just e
    e <- SBV e -> Maybe e
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV e
    se, Just f
    f <- SBV f -> Maybe f
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV f
    sf, Just g
    g <- SBV g -> Maybe g
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV g
    sg
        = (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g)
    forall a. SymVal a => a -> SBV a
    literal (a
    a, b
    b, c
    c, d
    d, e
    e, f
    f, g
    g)
        | Bool
    True
        = SVal -> SBV (a, b, c, d, e, f, g)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (a, b, c, d, e, f, g))
    -> SVal -> SBV (a, b, c, d, e, f, g)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
        where k :: Kind
    k      = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
    p
              res :: State -> IO SV
    res State
    st = do SV
    asv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    sa
                          SV
    bsv <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    sb
                          SV
    csv <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    sc
                          SV
    dsv <- State -> SBV d -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV d
    sd
                          SV
    esv <- State -> SBV e -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV e
    se
                          SV
    fsv <- State -> SBV f -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV f
    sf
                          SV
    gsv <- State -> SBV g -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV g
    sg
                          State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Op
    TupleConstructor Int
    7) [SV
    asv, SV
    bsv, SV
    csv, SV
    dsv, SV
    esv, SV
    fsv, SV
    gsv])

    instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h)
          => Tuple (a, b, c, d, e, f, g, h) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) where
      untuple :: SBV (a, b, c, d, e, f, g, h)
    -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h)
    untuple SBV (a, b, c, d, e, f, g, h)
    p = (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1, SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2, SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3, SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4, SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5, SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6, SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV g) -> SBV g
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV g
    forall b a. HasField "_7" b a => SBV a -> SBV b
    _7, SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV h) -> SBV h
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV h
    forall b a. HasField "_8" b a => SBV a -> SBV b
    _8)

      tuple :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h)
    -> SBV (a, b, c, d, e, f, g, h)
    tuple p :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h)
    p@(SBV a
    sa, SBV b
    sb, SBV c
    sc, SBV d
    sd, SBV e
    se, SBV f
    sf, SBV g
    sg, SBV h
    sh)
        | Just a
    a <- SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    sa, Just b
    b <- SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    sb, Just c
    c <- SBV c -> Maybe c
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV c
    sc, Just d
    d <- SBV d -> Maybe d
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV d
    sd, Just e
    e <- SBV e -> Maybe e
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV e
    se, Just f
    f <- SBV f -> Maybe f
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV f
    sf, Just g
    g <- SBV g -> Maybe g
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV g
    sg, Just h
    h <- SBV h -> Maybe h
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV h
    sh
        = (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h)
    forall a. SymVal a => a -> SBV a
    literal (a
    a, b
    b, c
    c, d
    d, e
    e, f
    f, g
    g, h
    h)
        | Bool
    True
        = SVal -> SBV (a, b, c, d, e, f, g, h)
    forall a. SVal -> SBV a
    SBV (SVal -> SBV (a, b, c, d, e, f, g, h))
    -> SVal -> SBV (a, b, c, d, e, f, g, h)
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    res
        where k :: Kind
    k      = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h)
    p
              res :: State -> IO SV
    res State
    st = do SV
    asv <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    sa
                          SV
    bsv <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    sb
                          SV
    csv <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    sc
                          SV
    dsv <- State -> SBV d -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV d
    sd
                          SV
    esv <- State -> SBV e -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV e
    se
                          SV
    fsv <- State -> SBV f -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV f
    sf
                          SV
    gsv <- State -> SBV g -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV g
    sg
                          SV
    hsv <- State -> SBV h -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV h
    sh
                          State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (Int -> Op
    TupleConstructor Int
    8) [SV
    asv, SV
    bsv, SV
    csv, SV
    dsv, SV
    esv, SV
    fsv, SV
    gsv, SV
    hsv])

    -- Optimization for tuples

    -- 2-tuple
    instance ( SymVal a, Metric a
             , SymVal b, Metric b)
             => Metric (a, b) where
       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b) -> m ()
    msMinimize String
    nm SBV (a, b)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b)
    pSBV (a, b) -> (SBV (a, b) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b)
    pSBV (a, b) -> (SBV (a, b) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b) -> m ()
    msMaximize String
    nm SBV (a, b)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b)
    pSBV (a, b) -> (SBV (a, b) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b)
    pSBV (a, b) -> (SBV (a, b) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)

    -- 3-tuple
    instance ( SymVal a, Metric a
             , SymVal b, Metric b
             , SymVal c, Metric c)
             => Metric (a, b, c) where
       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c) -> m ()
    msMinimize String
    nm SBV (a, b, c)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c) -> m ()
    msMaximize String
    nm SBV (a, b, c)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c)
    pSBV (a, b, c) -> (SBV (a, b, c) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)

    -- 4-tuple
    instance ( SymVal a, Metric a
             , SymVal b, Metric b
             , SymVal c, Metric c
             , SymVal d, Metric d)
             => Metric (a, b, c, d) where
       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d) -> m ()
    msMinimize String
    nm SBV (a, b, c, d)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d) -> m ()
    msMaximize String
    nm SBV (a, b, c, d)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d)
    pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)

    -- 5-tuple
    instance ( SymVal a, Metric a
             , SymVal b, Metric b
             , SymVal c, Metric c
             , SymVal d, Metric d
             , SymVal e, Metric e)
             => Metric (a, b, c, d, e) where
       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d, e) -> m ()
    msMinimize String
    nm SBV (a, b, c, d, e)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
                            String -> SBV e -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV e -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._5") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)
       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d, e) -> m ()
    msMaximize String
    nm SBV (a, b, c, d, e)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
                            String -> SBV e -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV e -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._5") (SBV (a, b, c, d, e)
    pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)

    -- 6-tuple
    instance ( SymVal a, Metric a
             , SymVal b, Metric b
             , SymVal c, Metric c
             , SymVal d, Metric d
             , SymVal e, Metric e
             , SymVal f, Metric f)
             => Metric (a, b, c, d, e, f) where
       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d, e, f) -> m ()
    msMinimize String
    nm SBV (a, b, c, d, e, f)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
                            String -> SBV e -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV e -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._5") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)
                            String -> SBV f -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV f -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._6") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6)
       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d, e, f) -> m ()
    msMaximize String
    nm SBV (a, b, c, d, e, f)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
                            String -> SBV e -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV e -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._5") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)
                            String -> SBV f -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV f -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._6") (SBV (a, b, c, d, e, f)
    pSBV (a, b, c, d, e, f)
    -> (SBV (a, b, c, d, e, f) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6)

    -- 7-tuple
    instance ( SymVal a, Metric a
             , SymVal b, Metric b
             , SymVal c, Metric c
             , SymVal d, Metric d
             , SymVal e, Metric e
             , SymVal f, Metric f
             , SymVal g, Metric g)
             => Metric (a, b, c, d, e, f, g) where
       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d, e, f, g) -> m ()
    msMinimize String
    nm SBV (a, b, c, d, e, f, g)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
                            String -> SBV e -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV e -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._5") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)
                            String -> SBV f -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV f -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._6") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6)
                            String -> SBV g -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV g -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._7") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV g) -> SBV g
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV g
    forall b a. HasField "_7" b a => SBV a -> SBV b
    _7)
       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d, e, f, g) -> m ()
    msMaximize String
    nm SBV (a, b, c, d, e, f, g)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
                            String -> SBV e -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV e -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._5") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)
                            String -> SBV f -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV f -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._6") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6)
                            String -> SBV g -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV g -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._7") (SBV (a, b, c, d, e, f, g)
    pSBV (a, b, c, d, e, f, g)
    -> (SBV (a, b, c, d, e, f, g) -> SBV g) -> SBV g
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g) -> SBV g
    forall b a. HasField "_7" b a => SBV a -> SBV b
    _7)

    -- 8-tuple
    instance ( SymVal a, Metric a
             , SymVal b, Metric b
             , SymVal c, Metric c
             , SymVal d, Metric d
             , SymVal e, Metric e
             , SymVal f, Metric f
             , SymVal g, Metric g
             , SymVal h, Metric h)
             => Metric (a, b, c, d, e, f, g, h) where
       msMinimize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d, e, f, g, h) -> m ()
    msMinimize String
    nm SBV (a, b, c, d, e, f, g, h)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
                            String -> SBV e -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV e -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._5") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)
                            String -> SBV f -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV f -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._6") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6)
                            String -> SBV g -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV g -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._7") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV g) -> SBV g
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV g
    forall b a. HasField "_7" b a => SBV a -> SBV b
    _7)
                            String -> SBV h -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV h -> m ()
    msMinimize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._8") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV h) -> SBV h
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV h
    forall b a. HasField "_8" b a => SBV a -> SBV b
    _8)
       msMaximize :: forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV (a, b, c, d, e, f, g, h) -> m ()
    msMaximize String
    nm SBV (a, b, c, d, e, f, g, h)
    p = do String -> SBV a -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._1") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1)
                            String -> SBV b -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV b -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._2") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV b) -> SBV b
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV b
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2)
                            String -> SBV c -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV c -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._3") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV c) -> SBV c
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV c
    forall b a. HasField "_3" b a => SBV a -> SBV b
    _3)
                            String -> SBV d -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV d -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._4") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV d) -> SBV d
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV d
    forall b a. HasField "_4" b a => SBV a -> SBV b
    _4)
                            String -> SBV e -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV e -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._5") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV e) -> SBV e
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV e
    forall b a. HasField "_5" b a => SBV a -> SBV b
    _5)
                            String -> SBV f -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV f -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._6") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV f) -> SBV f
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV f
    forall b a. HasField "_6" b a => SBV a -> SBV b
    _6)
                            String -> SBV g -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV g -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._7") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV g) -> SBV g
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV g
    forall b a. HasField "_7" b a => SBV a -> SBV b
    _7)
                            String -> SBV h -> m ()
    forall a (m :: * -> *).
    (Metric a, MonadSymbolic m, SolverContext m) =>
    String -> SBV a -> m ()
    forall (m :: * -> *).
    (MonadSymbolic m, SolverContext m) =>
    String -> SBV h -> m ()
    msMaximize (String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "^._8") (SBV (a, b, c, d, e, f, g, h)
    pSBV (a, b, c, d, e, f, g, h)
    -> (SBV (a, b, c, d, e, f, g, h) -> SBV h) -> SBV h
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, b, c, d, e, f, g, h) -> SBV h
    forall b a. HasField "_8" b a => SBV a -> SBV b
    _8)

    {- HLint ignore module "Reduce duplication" -}