-----------------------------------------------------------------------------
-- |
-- 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
  ) 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 ^.

-- | 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 forall a. Ord a => a -> a -> Bool
> Int
i Bool -> Bool -> Bool
|| Int
i forall a. Ord a => a -> a -> Bool
> Int
lks
  = forall a. String -> a
bad forall a b. (a -> b) -> a -> b
$ String
"Index is out of bounds, " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" is outside [1," forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
lks 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      forall a. Eq a => a -> a -> Bool
/= Kind
ktup -> forall a. String -> a
bad forall a b. (a -> b) -> a -> b
$ String
"Kind/value mismatch: "      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
kval
                | forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
vs forall a. Eq a => a -> a -> Bool
/= Int
lks  -> forall a. String -> a
bad forall a b. (a -> b) -> a -> b
$ String
"Value has fewer elements: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Kind -> CVal -> CV
CV Kind
kval ([CVal] -> CVal
CTuple [CVal]
vs))
                | Bool
True              -> forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => CV -> a
fromCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
kElem ([CVal]
vs forall a. [a] -> Int -> a
!! (Int
iforall a. Num a => a -> a -> a
-Int
1))
      CVal
_                             -> forall a. String -> a
bad forall a b. (a -> b) -> a -> b
$ String
"Kind/value mismatch: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CV
v
  | Bool
True
  = forall a. SBV a
symAccess
  where ktup :: Kind
ktup = forall a. HasKind a => a -> Kind
kindOf SBV tup
tup

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

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

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

        symAccess :: SBV a
        symAccess :: forall a. SBV a
symAccess = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kElem forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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"
_ = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b)
pforall a b. a -> (a -> b) -> 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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb
    = forall a. SymVal a => a -> SBV a
literal (a
a, b
b)
    | Bool
True
    = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b)
p
          res :: State -> IO SV
res State
st = do SV
asv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- 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)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c)
pforall a b. a -> (a -> b) -> b
^.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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc
    = forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c)
    | Bool
True
    = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b, SBV c)
p
          res :: State -> IO SV
res State
st = do SV
asv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- 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)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd
    = forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d)
    | Bool
True
    = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = 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 <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- 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)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4, SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd, Just e
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV e
se
    = forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d, e
e)
    | Bool
True
    = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = 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 <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      SV
esv <- 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)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4, SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5, SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd, Just e
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV e
se, Just f
f <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV f
sf
    = forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d, e
e, f
f)
    | Bool
True
    = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = 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 <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      SV
esv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV e
se
                      SV
fsv <- 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)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4, SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5, SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_6" b a => SBV a -> SBV b
_6, SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd, Just e
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV e
se, Just f
f <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV f
sf, Just g
g <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV g
sg
    = forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d, e
e, f
f, g
g)
    | Bool
True
    = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = 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 <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      SV
esv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV e
se
                      SV
fsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV f
sf
                      SV
gsv <- 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)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4, SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5, SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_6" b a => SBV a -> SBV b
_6, SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_7" b a => SBV a -> SBV b
_7, SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd, Just e
e <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV e
se, Just f
f <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV f
sf, Just g
g <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV g
sg, Just h
h <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV h
sh
    = 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
    = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = 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 <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      SV
esv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV e
se
                      SV
fsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV f
sf
                      SV
gsv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV g
sg
                      SV
hsv <- 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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b)
pforall a b. a -> (a -> b) -> 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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b)
pforall a b. a -> (a -> b) -> 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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._7") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._7") (SBV (a, b, c, d, e, f, g)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._7") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_7" b a => SBV a -> SBV b
_7)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._8") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.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 forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._7") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_7" b a => SBV a -> SBV b
_7)
                        forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm forall a. [a] -> [a] -> [a]
++ String
"^._8") (SBV (a, b, c, d, e, f, g, h)
pforall a b. a -> (a -> b) -> b
^.forall b a. HasField "_8" b a => SBV a -> SBV b
_8)

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}