    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.SMT.SMTLib2
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Conversion of symbolic programs to SMTLib format, Using v2 of the standard
    -----------------------------------------------------------------------------

    {-# LANGUAGE NamedFieldPuns      #-}
    {-# LANGUAGE PatternGuards       #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE ViewPatterns        #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.SMT.SMTLib2(cvt, cvtExp, cvtInc, declUserFuns) where

    import Data.Bits  (bit)
    import Data.List  (intercalate, partition, nub, elemIndex)
    import Data.Maybe (listToMaybe, catMaybes)

    import qualified Data.Foldable as F (toList)
    import qualified Data.Map.Strict      as M
    import qualified Data.IntMap.Strict   as IM
    import           Data.Set             (Set)
    import qualified Data.Set             as Set

    import Data.SBV.Core.Data
    import Data.SBV.Core.Kind (smtType, needsFlattening)
    import Data.SBV.SMT.Utils
    import Data.SBV.Control.Types

    import Data.SBV.Core.Symbolic ( QueryContext(..), SetOp(..), CnstMap, getUserName', getSV, regExpToSMTString
                                  , SMTDef(..), ResultInp(..), ProgInfo(..), SpecialRelOp(..)
                                  )

    import Data.SBV.Utils.PrettyNum (smtRoundingMode, cvToSMTLib)

    import qualified Data.Generics.Uniplate.Data as G

    import qualified Data.Graph as DG

    tbd :: String -> a
    tbd :: forall a. String -> a
    tbd String
    e = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2: Not-yet-supported: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    e

    -- | Translate a problem into an SMTLib2 script
    cvt :: SMTLibConverter [String]
    cvt :: SMTLibConverter [String]
    cvt QueryContext
    ctx ProgInfo
    curProgInfo Set Kind
    kindInfo Bool
    isSat [String]
    comments ResultInp
    allInputs (CnstMap
    allConsts, [(SV, CV)]
    consts) [((Int, Kind, Kind), [SV])]
    tbls [(Int, ArrayInfo)]
    arrs [(String, (Maybe [String], SBVType))]
    uis [SMTDef]
    defs (SBVPgm Seq (SV, SBVExpr)
    asgnsSeq) Seq (Bool, [(String, String)], SV)
    cstrs SV
    out SMTConfig
    cfg = [String]
    pgm
      where hasInteger :: Bool
    hasInteger     = Kind
    KUnbounded Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
            hasReal :: Bool
    hasReal        = Kind
    KReal      Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
            hasFP :: Bool
    hasFP          =  Bool -> Bool
    not ([()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [() | KFP{} <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    kindInfo])
                           Bool -> Bool -> Bool
    || Kind
    KFloat     Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
                           Bool -> Bool -> Bool
    || Kind
    KDouble    Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
            hasString :: Bool
    hasString      = Kind
    KString     Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
            hasRegExp :: Bool
    hasRegExp      = (Bool -> Bool
    not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) [() | (RegExOp
    _ :: RegExOp) <- Seq (SV, SBVExpr) -> [RegExOp]
    forall from to. Biplate from to => from -> [to]
    G.universeBi Seq (SV, SBVExpr)
    asgnsSeq]
            hasChar :: Bool
    hasChar        = Kind
    KChar      Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
            hasRounding :: Bool
    hasRounding    = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String
    s | (String
    s, Maybe [String]
    _) <- [(String, Maybe [String])]
    usorts, String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "RoundingMode"]
            hasBVs :: Bool
    hasBVs         = Bool -> Bool
    not ([()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [() | KBounded{} <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    kindInfo])
            usorts :: [(String, Maybe [String])]
    usorts         = [(String
    s, Maybe [String]
    dt) | KUserSort String
    s Maybe [String]
    dt <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    kindInfo]
            trueUSorts :: [String]
    trueUSorts     = [String
    s | (String
    s, Maybe [String]
    _) <- [(String, Maybe [String])]
    usorts, String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    /= String
    "RoundingMode"]
            tupleArities :: [Int]
    tupleArities   = Set Kind -> [Int]
    findTupleArities Set Kind
    kindInfo
            hasNonBVArrays :: Bool
    hasNonBVArrays = (Bool -> Bool
    not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) [() | (Int
    _, (String
    _, (Kind
    k1, Kind
    k2), ArrayContext
    _)) <- [(Int, ArrayInfo)]
    arrs, Bool -> Bool
    not (Kind -> Bool
    forall a. HasKind a => a -> Bool
    isBounded Kind
    k1 Bool -> Bool -> Bool
    && Kind -> Bool
    forall a. HasKind a => a -> Bool
    isBounded Kind
    k2)]
            hasArrayInits :: Bool
    hasArrayInits  = (Bool -> Bool
    not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) ([()] -> Bool) -> [()] -> Bool
    forall a b. (a -> b) -> a -> b
    $  [() | (Int
    _, (String
    _, (Kind, Kind)
    _, ArrayFree (Left  (Just SV
    _)))) <- [(Int, ArrayInfo)]
    arrs]
                                          [()] -> [()] -> [()]
    forall a. [a] -> [a] -> [a]
    ++ [() | (Int
    _, (String
    _, (Kind, Kind)
    _, ArrayFree (Right String
    _       ))) <- [(Int, ArrayInfo)]
    arrs]
            hasOverflows :: Bool
    hasOverflows   = (Bool -> Bool
    not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) [() | (OvOp
    _ :: OvOp) <- Seq (SV, SBVExpr) -> [OvOp]
    forall from to. Biplate from to => from -> [to]
    G.universeBi Seq (SV, SBVExpr)
    asgnsSeq]
            hasList :: Bool
    hasList        = (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isList Set Kind
    kindInfo
            hasSets :: Bool
    hasSets        = (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isSet Set Kind
    kindInfo
            hasTuples :: Bool
    hasTuples      = Bool -> Bool
    not (Bool -> Bool) -> ([Int] -> Bool) -> [Int] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Int] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([Int] -> Bool) -> [Int] -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Int]
    tupleArities
            hasEither :: Bool
    hasEither      = (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isEither Set Kind
    kindInfo
            hasMaybe :: Bool
    hasMaybe       = (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isMaybe  Set Kind
    kindInfo
            hasRational :: Bool
    hasRational    = (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    forall a. HasKind a => a -> Bool
    isRational Set Kind
    kindInfo
            rm :: RoundingMode
    rm             = SMTConfig -> RoundingMode
    roundingMode SMTConfig
    cfg
            solverCaps :: SolverCapabilities
    solverCaps     = SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)
            hasFoldMap :: Bool
    hasFoldMap     = let isFoldMap :: SeqOp -> Bool
    isFoldMap SeqMap{}       = Bool
    True
                                 isFoldMap SeqMapI{}      = Bool
    True
                                 isFoldMap SeqFoldLeft{}  = Bool
    True
                                 isFoldMap SeqFoldLeftI{} = Bool
    True
                                 isFoldMap SeqOp
    _              = Bool
    False
                             in (Bool -> Bool
    not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) [ () | SeqOp
    o :: SeqOp <- Seq (SV, SBVExpr) -> [SeqOp]
    forall from to. Biplate from to => from -> [to]
    G.universeBi Seq (SV, SBVExpr)
    asgnsSeq, SeqOp -> Bool
    isFoldMap SeqOp
    o]

            (Bool
    needsQuantifiers, Bool
    needsSpecialRels) = case ProgInfo
    curProgInfo of
               ProgInfo Bool
    hasQ [SpecialRelOp]
    srs [(String, String)]
    tcs -> (Bool
    hasQ, Bool -> Bool
    not ([SpecialRelOp] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SpecialRelOp]
    srs Bool -> Bool -> Bool
    && [(String, String)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, String)]
    tcs))

            -- Is there a reason why we can't handle this problem?
            -- NB. There's probably a lot more checking we can do here, but this is a start:
            doesntHandle :: Maybe [String]
    doesntHandle = [[String]] -> Maybe [String]
    forall a. [a] -> Maybe a
    listToMaybe [String -> [String]
    nope String
    w | (String
    w, SolverCapabilities -> Bool
    have, Bool
    need) <- [(String, SolverCapabilities -> Bool, Bool)]
    checks, Bool
    need Bool -> Bool -> Bool
    && Bool -> Bool
    not (SolverCapabilities -> Bool
    have SolverCapabilities
    solverCaps)]
               where checks :: [(String, SolverCapabilities -> Bool, Bool)]
    checks = [ (String
    "data types",             SolverCapabilities -> Bool
    supportsDataTypes,          Bool
    hasTuples Bool -> Bool -> Bool
    || Bool
    hasEither Bool -> Bool -> Bool
    || Bool
    hasMaybe)
                              , (String
    "folds and maps",         SolverCapabilities -> Bool
    supportsFoldAndMap,         Bool
    hasFoldMap)
                              , (String
    "set operations",         SolverCapabilities -> Bool
    supportsSets,               Bool
    hasSets)
                              , (String
    "bit vectors",            SolverCapabilities -> Bool
    supportsBitVectors,         Bool
    hasBVs)
                              , (String
    "special relations",      SolverCapabilities -> Bool
    supportsSpecialRels,        Bool
    needsSpecialRels)
                              , (String
    "needs quantifiers",      SolverCapabilities -> Bool
    supportsQuantifiers,        Bool
    needsQuantifiers)
                              , (String
    "unbounded integers",     SolverCapabilities -> Bool
    supportsUnboundedInts,      Bool
    hasInteger)
                              , (String
    "algebraic reals",        SolverCapabilities -> Bool
    supportsReals,              Bool
    hasReal)
                              , (String
    "floating-point numbers", SolverCapabilities -> Bool
    supportsIEEE754,            Bool
    hasFP)
                              , (String
    "uninterpreted sorts",    SolverCapabilities -> Bool
    supportsUninterpretedSorts, Bool -> Bool
    not ([String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    trueUSorts))
                              ]

                     nope :: String -> [String]
    nope String
    w = [ String
    "***     Given problem requires support for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w
                              , String
    "***     But the chosen solver (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Solver -> String
    forall a. Show a => a -> String
    show (SMTSolver -> Solver
    name (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") doesn't support this feature."
                              ]

            -- Some cases require all, some require none. Sigh..
            setAll :: String -> [String]
    setAll String
    reason = [String
    "(set-logic ALL) ; "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    reason String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", using catch-all."]

            -- Determining the logic is surprisingly tricky!
            logic :: [String]
    logic
               -- user told us what to do: so just take it:
               | Just Logic
    l <- case [Logic
    l | SetLogic Logic
    l <- SMTConfig -> [SMTOption]
    solverSetOptions SMTConfig
    cfg] of
                             []  -> Maybe Logic
    forall a. Maybe a
    Nothing
                             [Logic
    l] -> Logic -> Maybe Logic
    forall a. a -> Maybe a
    Just Logic
    l
                             [Logic]
    ls  -> String -> Maybe Logic
    forall a. HasCallStack => String -> a
    error (String -> Maybe Logic) -> String -> Maybe Logic
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                                    , String
    "*** Only one setOption call to 'setLogic' is allowed, found: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([Logic] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Logic]
    ls)
                                                    , String
    "***  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Logic -> String) -> [Logic] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Logic -> String
    forall a. Show a => a -> String
    show [Logic]
    ls)
                                                    ]
               = case Logic
    l of
                   Logic
    Logic_NONE -> [String
    "; NB. Not setting the logic per user request of Logic_NONE"]
                   Logic
    _          -> [String
    "(set-logic " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Logic -> String
    forall a. Show a => a -> String
    show Logic
    l String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") ; NB. User specified."]

               -- There's a reason why we can't handle this problem:
               | Just [String]
    cantDo <- Maybe [String]
    doesntHandle
               = String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $   [ String
    ""
                                     , String
    "*** SBV is unable to choose a proper solver configuration:"
                                     , String
    "***"
                                     ]
                                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    cantDo
                                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "***"
                                    , String
    "*** Please report this as a feature request, either for SBV or the backend solver."
                                    ]

               -- Otherwise, we try to determine the most suitable logic.
               -- NB. This isn't really fool proof!

               -- we never set QF_S (ALL seems to work better in all cases)

               | Bool
    needsSpecialRels      = [String
    "; has special relations, no logic set."]

               -- Things that require ALL
               | Bool
    hasInteger            = String -> [String]
    setAll String
    "has unbounded values"
               | Bool
    hasRational           = String -> [String]
    setAll String
    "has rational values"
               | Bool
    hasReal               = String -> [String]
    setAll String
    "has algebraic reals"
               | Bool -> Bool
    not ([String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    trueUSorts) = String -> [String]
    setAll String
    "has user-defined sorts"
               | Bool
    hasNonBVArrays        = String -> [String]
    setAll String
    "has non-bitvector arrays"
               | Bool
    hasTuples             = String -> [String]
    setAll String
    "has tuples"
               | Bool
    hasEither             = String -> [String]
    setAll String
    "has either type"
               | Bool
    hasMaybe              = String -> [String]
    setAll String
    "has maybe type"
               | Bool
    hasSets               = String -> [String]
    setAll String
    "has sets"
               | Bool
    hasList               = String -> [String]
    setAll String
    "has lists"
               | Bool
    hasChar               = String -> [String]
    setAll String
    "has chars"
               | Bool
    hasString             = String -> [String]
    setAll String
    "has strings"
               | Bool
    hasRegExp             = String -> [String]
    setAll String
    "has regular expressions"
               | Bool
    hasArrayInits         = String -> [String]
    setAll String
    "has array initializers"
               | Bool
    hasOverflows          = String -> [String]
    setAll String
    "has overflow checks"

               | Bool
    hasFP Bool -> Bool -> Bool
    || Bool
    hasRounding
               = if Bool
    needsQuantifiers
                 then [String
    "(set-logic ALL)"]
                 else if Bool
    hasBVs
                      then [String
    "(set-logic QF_FPBV)"]
                      else [String
    "(set-logic QF_FP)"]

               -- If we're in a user query context, we'll pick ALL, otherwise
               -- we'll stick to some bit-vector logic based on what we see in the problem.
               -- This is controversial, but seems to work well in practice.
               | Bool
    True
               = case QueryContext
    ctx of
                   QueryContext
    QueryExternal -> [String
    "(set-logic ALL) ; external query, using all logics."]
                   QueryContext
    QueryInternal -> if SolverCapabilities -> Bool
    supportsBitVectors SolverCapabilities
    solverCaps
                                    then [String
    "(set-logic " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    qs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    as String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ufs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "BV)"]
                                    else [String
    "(set-logic ALL)"] -- fall-thru
              where qs :: String
    qs  | Bool -> Bool
    not Bool
    needsQuantifiers  = String
    "QF_"
                        | Bool
    True                  = String
    ""
                    as :: String
    as  | [(Int, ArrayInfo)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Int, ArrayInfo)]
    arrs             = String
    ""
                        | Bool
    True                  = String
    "A"
                    ufs :: String
    ufs | [(String, (Maybe [String], SBVType))] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, (Maybe [String], SBVType))]
    uis Bool -> Bool -> Bool
    && [((Int, Kind, Kind), [SV])] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [((Int, Kind, Kind), [SV])]
    tbls = String
    ""     -- we represent tables as UFs
                        | Bool
    True                  = String
    "UF"

            -- SBV always requires the production of models!
            getModels :: [String]
    getModels   = String
    "(set-option :produce-models true)"
                        String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]
    flattenConfig | (Kind -> Bool) -> Set Kind -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    needsFlattening Set Kind
    kindInfo, Just [String]
    flattenConfig <- [SolverCapabilities -> Maybe [String]
    supportsFlattenedModels SolverCapabilities
    solverCaps]]

            -- process all other settings we're given. If an option cannot be repeated, we only take the last one.
            userSettings :: [String]
    userSettings = (SMTOption -> String) -> [SMTOption] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SMTOption -> String
    setSMTOption ([SMTOption] -> [String]) -> [SMTOption] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (SMTOption -> Bool) -> [SMTOption] -> [SMTOption]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (SMTOption -> Bool) -> SMTOption -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTOption -> Bool
    isLogic) ([SMTOption] -> [SMTOption]) -> [SMTOption] -> [SMTOption]
    forall a b. (a -> b) -> a -> b
    $ (SMTOption -> [SMTOption] -> [SMTOption])
    -> [SMTOption] -> [SMTOption] -> [SMTOption]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SMTOption -> [SMTOption] -> [SMTOption]
    comb [] ([SMTOption] -> [SMTOption]) -> [SMTOption] -> [SMTOption]
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> [SMTOption]
    solverSetOptions SMTConfig
    cfg
               where -- Logic is already processed, so drop it:
                     isLogic :: SMTOption -> Bool
    isLogic SetLogic{} = Bool
    True
                     isLogic SMTOption
    _          = Bool
    False

                     -- SBV sets diagnostic-output channel on some solvers. If the user also gives it, let's just
                     -- take it by only taking the last one
                     isDiagOutput :: SMTOption -> Bool
    isDiagOutput DiagnosticOutputChannel{} = Bool
    True
                     isDiagOutput SMTOption
    _                         = Bool
    False

                     comb :: SMTOption -> [SMTOption] -> [SMTOption]
    comb SMTOption
    o [SMTOption]
    rest
                       | SMTOption -> Bool
    isDiagOutput SMTOption
    o Bool -> Bool -> Bool
    && (SMTOption -> Bool) -> [SMTOption] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SMTOption -> Bool
    isDiagOutput [SMTOption]
    rest =     [SMTOption]
    rest
                       | Bool
    True                                    = SMTOption
    o SMTOption -> [SMTOption] -> [SMTOption]
    forall a. a -> [a] -> [a]
    : [SMTOption]
    rest

            settings :: [String]
    settings =  [String]
    userSettings        -- NB. Make sure this comes first!
                     [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    getModels
                     [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    logic

            ([NamedSymVar]
    inputs, [NamedSymVar]
    trackerVars)
                = case ResultInp
    allInputs of
                    ResultTopInps ([NamedSymVar], [NamedSymVar])
    ists -> ([NamedSymVar], [NamedSymVar])
    ists
                    ResultLamInps [(Quantifier, NamedSymVar)]
    ps   -> String -> ([NamedSymVar], [NamedSymVar])
    forall a. HasCallStack => String -> a
    error (String -> ([NamedSymVar], [NamedSymVar]))
    -> String -> ([NamedSymVar], [NamedSymVar])
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                                          , String
    "*** Data.SBV.smtLib2: Unexpected lambda inputs in conversion"
                                                          , String
    "***"
                                                          , String
    "*** Saw: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [(Quantifier, NamedSymVar)] -> String
    forall a. Show a => a -> String
    show [(Quantifier, NamedSymVar)]
    ps
                                                          ]

            pgm :: [String]
    pgm  =  (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    "; " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) [String]
    comments
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    settings
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- uninterpreted sorts ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, Maybe [String]) -> [String])
    -> [(String, Maybe [String])] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (String, Maybe [String]) -> [String]
    declSort [(String, Maybe [String])]
    usorts
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- tuples ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (Int -> [String]) -> [Int] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Int -> [String]
    declTuple [Int]
    tupleArities
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- sums ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if Set Kind -> Bool
    containsSum       Set Kind
    kindInfo then [String]
    declSum       else [])
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if Set Kind -> Bool
    containsMaybe     Set Kind
    kindInfo then [String]
    declMaybe     else [])
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if Set Kind -> Bool
    containsRationals Set Kind
    kindInfo then [String]
    declRationals else [])
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- literal constants ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, CV) -> [String]) -> [(SV, CV)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (SMTConfig -> (SV, CV) -> [String]
    declConst SMTConfig
    cfg) [(SV, CV)]
    consts
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- top level inputs ---"]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [SV -> SBVType -> Maybe String -> [String]
    declareFun SV
    s ([Kind] -> SBVType
    SBVType [SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s]) (SV -> Maybe String
    userName SV
    s) | NamedSymVar
    var <- [NamedSymVar]
    inputs, let s :: SV
    s = NamedSymVar -> SV
    getSV NamedSymVar
    var]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- optimization tracker variables ---" | Bool -> Bool
    not ([NamedSymVar] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [NamedSymVar]
    trackerVars) ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [SV -> SBVType -> Maybe String -> [String]
    declareFun SV
    s ([Kind] -> SBVType
    SBVType [SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s]) (String -> Maybe String
    forall a. a -> Maybe a
    Just (String
    "tracks " String -> String -> String
    forall a. Semigroup a => a -> a -> a
    <> String
    nm)) | NamedSymVar
    var <- [NamedSymVar]
    trackerVars, let s :: SV
    s = NamedSymVar -> SV
    getSV NamedSymVar
    var, let nm :: String
    nm = NamedSymVar -> String
    getUserName' NamedSymVar
    var]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- constant tables ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((((Int, Kind, Kind), [SV]), [String]) -> [String])
    -> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((String -> [String] -> [String]) -> (String, [String]) -> [String]
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (:) ((String, [String]) -> [String])
    -> ((((Int, Kind, Kind), [SV]), [String]) -> (String, [String]))
    -> (((Int, Kind, Kind), [SV]), [String])
    -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
    mkTable) [(((Int, Kind, Kind), [SV]), [String])]
    constTables
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- non-constant tables ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((((Int, Kind, Kind), [SV]), [String]) -> String)
    -> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Int, Kind, Kind), [SV]), [String]) -> String
    nonConstTable [(((Int, Kind, Kind), [SV]), [String])]
    nonConstTables
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- arrays ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    arrayConstants
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- uninterpreted constants ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, (Maybe [String], SBVType)) -> [String])
    -> [(String, (Maybe [String], SBVType))] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (ProgInfo -> (String, (Maybe [String], SBVType)) -> [String]
    declUI ProgInfo
    curProgInfo) [(String, (Maybe [String], SBVType))]
    uis
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- SBV Function definitions" | Bool -> Bool
    not (Map Op String -> Bool
    forall a. Map Op a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Map Op String
    funcMap) ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ Op -> String -> [String]
    declSBVFunc Op
    op String
    nm | (Op
    op, String
    nm) <- Map Op String -> [(Op, String)]
    forall k a. Map k a -> [(k, a)]
    M.toAscList Map Op String
    funcMap ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- user defined functions ---"]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [SMTDef] -> [String]
    declUserFuns [SMTDef]
    defs
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- assignments ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, SBVExpr) -> [String]) -> [(SV, SBVExpr)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (ProgInfo
    -> SMTConfig
    -> TableMap
    -> Map Op String
    -> (SV, SBVExpr)
    -> [String]
    declDef ProgInfo
    curProgInfo SMTConfig
    cfg TableMap
    tableMap Map Op String
    funcMap) [(SV, SBVExpr)]
    asgns
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- arrayDelayeds ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    arrayDelayeds
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- arraySetups ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    arraySetups
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- delayedEqualities ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\String
    s -> String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")") [String]
    delayedEqualities
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "; --- formula ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    finalAssert

            allTables :: [(((Int, Kind, Kind), [SV]), Either [String] [String])]
    allTables      = [(((Int, Kind, Kind), [SV])
    t, RoundingMode
    -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String]
    genTableData RoundingMode
    rm (((SV, CV) -> SV) -> [(SV, CV)] -> [SV]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, CV) -> SV
    forall a b. (a, b) -> a
    fst [(SV, CV)]
    consts) ((Int, Kind, Kind), [SV])
    t) | ((Int, Kind, Kind), [SV])
    t <- [((Int, Kind, Kind), [SV])]
    tbls]
            constTables :: [(((Int, Kind, Kind), [SV]), [String])]
    constTables    = [(((Int, Kind, Kind), [SV])
    t, [String]
    d) | (((Int, Kind, Kind), [SV])
    t, Left  [String]
    d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
    allTables]
            nonConstTables :: [(((Int, Kind, Kind), [SV]), [String])]
    nonConstTables = [(((Int, Kind, Kind), [SV])
    t, [String]
    d) | (((Int, Kind, Kind), [SV])
    t, Right [String]
    d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
    allTables]

            ([[String]]
    arrayConstants, [[String]]
    arrayDelayeds, [[String]]
    arraySetups) = [([String], [String], [String])]
    -> ([[String]], [[String]], [[String]])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 ([([String], [String], [String])]
     -> ([[String]], [[String]], [[String]]))
    -> [([String], [String], [String])]
    -> ([[String]], [[String]], [[String]])
    forall a b. (a -> b) -> a -> b
    $ ((Int, ArrayInfo) -> ([String], [String], [String]))
    -> [(Int, ArrayInfo)] -> [([String], [String], [String])]
    forall a b. (a -> b) -> [a] -> [b]
    map (SMTConfig
    -> CnstMap -> (Int, ArrayInfo) -> ([String], [String], [String])
    declArray SMTConfig
    cfg CnstMap
    allConsts) [(Int, ArrayInfo)]
    arrs
            delayedEqualities :: [String]
    delayedEqualities = ((((Int, Kind, Kind), [SV]), [String]) -> [String])
    -> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (((Int, Kind, Kind), [SV]), [String]) -> [String]
    forall a b. (a, b) -> b
    snd [(((Int, Kind, Kind), [SV]), [String])]
    nonConstTables

            finalAssert :: [String]
    finalAssert
              | Bool
    noConstraints = []
              | Bool
    True          =    (([(String, String)], Either SV SV) -> String)
    -> [([(String, String)], Either SV SV)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\([(String, String)]
    attr, Either SV SV
    v) -> String
    "(assert "      String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)] -> String -> String
    addAnnotations [(String, String)]
    attr (Either SV SV -> String
    mkLiteral Either SV SV
    v) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")") [([(String, String)], Either SV SV)]
    hardAsserts
                                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (([(String, String)], Either SV SV) -> String)
    -> [([(String, String)], Either SV SV)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\([(String, String)]
    attr, Either SV SV
    v) -> String
    "(assert-soft " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)] -> String -> String
    addAnnotations [(String, String)]
    attr (Either SV SV -> String
    mkLiteral Either SV SV
    v) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")") [([(String, String)], Either SV SV)]
    softAsserts
              where mkLiteral :: Either SV SV -> String
    mkLiteral (Left  SV
    v) =            SV -> String
    cvtSV SV
    v
                    mkLiteral (Right SV
    v) = String
    "(not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

                    (Bool
    noConstraints, [(Bool, [(String, String)], Either SV SV)]
    assertions) = (Bool, [(Bool, [(String, String)], Either SV SV)])
    finalAssertions

                    hardAsserts, softAsserts :: [([(String, String)], Either SV SV)]
                    hardAsserts :: [([(String, String)], Either SV SV)]
    hardAsserts = [([(String, String)]
    attr, Either SV SV
    v) | (Bool
    False, [(String, String)]
    attr, Either SV SV
    v) <- [(Bool, [(String, String)], Either SV SV)]
    assertions]
                    softAsserts :: [([(String, String)], Either SV SV)]
    softAsserts = [([(String, String)]
    attr, Either SV SV
    v) | (Bool
    True,  [(String, String)]
    attr, Either SV SV
    v) <- [(Bool, [(String, String)], Either SV SV)]
    assertions]

            finalAssertions :: (Bool, [(Bool, [(String, String)], Either SV SV)])  -- If Left: positive, Right: negative
            finalAssertions :: (Bool, [(Bool, [(String, String)], Either SV SV)])
    finalAssertions
               | [(Bool, [(String, String)], Either SV SV)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Bool, [(String, String)], Either SV SV)]
    finals = (Bool
    True,  [(Bool
    False, [], SV -> Either SV SV
    forall a b. a -> Either a b
    Left SV
    trueSV)])
               | Bool
    True        = (Bool
    False, [(Bool, [(String, String)], Either SV SV)]
    finals)

               where finals :: [(Bool, [(String, String)], Either SV SV)]
    finals  = [(Bool, [(String, String)], Either SV SV)]
    forall {b}. [(Bool, [(String, String)], Either SV b)]
    cstrs' [(Bool, [(String, String)], Either SV SV)]
    -> [(Bool, [(String, String)], Either SV SV)]
    -> [(Bool, [(String, String)], Either SV SV)]
    forall a. [a] -> [a] -> [a]
    ++ [(Bool, [(String, String)], Either SV SV)]
    -> (Either SV SV -> [(Bool, [(String, String)], Either SV SV)])
    -> Maybe (Either SV SV)
    -> [(Bool, [(String, String)], Either SV SV)]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] (\Either SV SV
    r -> [(Bool
    False, [], Either SV SV
    r)]) Maybe (Either SV SV)
    mbO

                     cstrs' :: [(Bool, [(String, String)], Either SV b)]
    cstrs' =  [(Bool
    isSoft, [(String, String)]
    attrs, Either SV b
    c') | (Bool
    isSoft, [(String, String)]
    attrs, SV
    c) <- Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (Bool, [(String, String)], SV)
    cstrs, Just Either SV b
    c' <- [SV -> Maybe (Either SV b)
    forall {b}. SV -> Maybe (Either SV b)
    pos SV
    c]]

                     mbO :: Maybe (Either SV SV)
    mbO | Bool
    isSat = SV -> Maybe (Either SV SV)
    forall {b}. SV -> Maybe (Either SV b)
    pos SV
    out
                         | Bool
    True  = SV -> Maybe (Either SV SV)
    neg SV
    out

                     neg :: SV -> Maybe (Either SV SV)
    neg SV
    s
                      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV = Maybe (Either SV SV)
    forall a. Maybe a
    Nothing
                      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV  = Either SV SV -> Maybe (Either SV SV)
    forall a. a -> Maybe a
    Just (Either SV SV -> Maybe (Either SV SV))
    -> Either SV SV -> Maybe (Either SV SV)
    forall a b. (a -> b) -> a -> b
    $ SV -> Either SV SV
    forall a b. a -> Either a b
    Left SV
    falseSV
                      | Bool
    True         = Either SV SV -> Maybe (Either SV SV)
    forall a. a -> Maybe a
    Just (Either SV SV -> Maybe (Either SV SV))
    -> Either SV SV -> Maybe (Either SV SV)
    forall a b. (a -> b) -> a -> b
    $ SV -> Either SV SV
    forall a b. b -> Either a b
    Right SV
    s

                     pos :: SV -> Maybe (Either SV b)
    pos SV
    s
                      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV  = Maybe (Either SV b)
    forall a. Maybe a
    Nothing
                      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV = Either SV b -> Maybe (Either SV b)
    forall a. a -> Maybe a
    Just (Either SV b -> Maybe (Either SV b))
    -> Either SV b -> Maybe (Either SV b)
    forall a b. (a -> b) -> a -> b
    $ SV -> Either SV b
    forall a b. a -> Either a b
    Left SV
    falseSV
                      | Bool
    True         = Either SV b -> Maybe (Either SV b)
    forall a. a -> Maybe a
    Just (Either SV b -> Maybe (Either SV b))
    -> Either SV b -> Maybe (Either SV b)
    forall a b. (a -> b) -> a -> b
    $ SV -> Either SV b
    forall a b. a -> Either a b
    Left SV
    s

            tableMap :: TableMap
    tableMap  = [(Int, String)] -> TableMap
    forall a. [(Int, a)] -> IntMap a
    IM.fromList ([(Int, String)] -> TableMap) -> [(Int, String)] -> TableMap
    forall a b. (a -> b) -> a -> b
    $ ((((Int, Kind, Kind), [SV]), Either [String] [String])
     -> (Int, String))
    -> [(((Int, Kind, Kind), [SV]), Either [String] [String])]
    -> [(Int, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Int, Kind, Kind), [SV]), Either [String] [String])
    -> (Int, String)
    forall {a} {b} {c} {b} {b}.
    Show a =>
    (((a, b, c), b), b) -> (a, String)
    grab [(((Int, Kind, Kind), [SV]), Either [String] [String])]
    allTables
              where grab :: (((a, b, c), b), b) -> (a, String)
    grab (((a
    t, b
    _, c
    _), b
    _), b
    _) = (a
    t, String
    "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    t)

            -- SBV only functions.
            funcMap :: Map Op String
    funcMap = [(Op, String)] -> Map Op String
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList [(Op, String)]
    reverses
              where reverses :: [(Op, String)]
    reverses = [Op] -> [String] -> [(Op, String)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ([Op] -> [Op]
    forall a. Eq a => [a] -> [a]
    nub [Op
    op | op :: Op
    op@(SeqOp SBVReverse{}) <- Seq (SV, SBVExpr) -> [Op]
    forall from to. Biplate from to => from -> [to]
    G.universeBi Seq (SV, SBVExpr)
    asgnsSeq])
                                   [String
    "sbv.reverse_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i | Int
    i <- [(Int
    0::Int)..]]

            asgns :: [(SV, SBVExpr)]
    asgns = Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (SV, SBVExpr)
    asgnsSeq

            userNameMap :: Map SV String
    userNameMap = [(SV, String)] -> Map SV String
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList ([(SV, String)] -> Map SV String)
    -> [(SV, String)] -> Map SV String
    forall a b. (a -> b) -> a -> b
    $ (NamedSymVar -> (SV, String)) -> [NamedSymVar] -> [(SV, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\NamedSymVar
    nSymVar -> (NamedSymVar -> SV
    getSV NamedSymVar
    nSymVar, NamedSymVar -> String
    getUserName' NamedSymVar
    nSymVar)) [NamedSymVar]
    inputs
            userName :: SV -> Maybe String
    userName SV
    s = case SV -> Map SV String -> Maybe String
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup SV
    s Map SV String
    userNameMap of
                            Just String
    u  | SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    /= String
    u -> String -> Maybe String
    forall a. a -> Maybe a
    Just (String -> Maybe String) -> String -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ String
    "tracks user variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    u
                            Maybe String
    _                     -> Maybe String
    forall a. Maybe a
    Nothing

    -- Declare "known" SBV functions here
    declSBVFunc :: Op -> String -> [String]
    declSBVFunc :: Op -> String -> [String]
    declSBVFunc Op
    op String
    nm = case Op
    op of
                          SeqOp (SBVReverse Kind
    KString)   -> [String]
    mkStringRev
                          SeqOp (SBVReverse (KList Kind
    k)) -> Kind -> [String]
    mkSeqRev (Kind -> Kind
    KList Kind
    k)
                          Op
    _                            -> String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.declSBVFunc: Unexpected internal function: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Op, String) -> String
    forall a. Show a => a -> String
    show (Op
    op, String
    nm)
      where mkStringRev :: [String]
    mkStringRev = [ String
    "(define-fun-rec " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " ((str String)) String"
                          , String
    "                (ite (= str \"\")"
                          , String
    "                     \"\""
                          , String
    "                     (str.++ (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (str.substr str 1 (- (str.len str) 1)))"
                          , String
    "                             (str.substr str 0 1))))"
                          ]

            mkSeqRev :: Kind -> [String]
    mkSeqRev Kind
    k = [ String
    "(define-fun-rec " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " ((lst " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t
                         , String
    "                (ite (= lst (as seq.empty " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
                         , String
    "                     (as seq.empty " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                         , String
    "                     (seq.++ (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (seq.extract lst 1 (- (seq.len lst) 1))) (seq.unit (seq.nth lst 0)))))"
                         ]
              where t :: String
    t = Kind -> String
    smtType Kind
    k

    -- | Declare new sorts
    declSort :: (String, Maybe [String]) -> [String]
    declSort :: (String, Maybe [String]) -> [String]
    declSort (String
    s, Maybe [String]
    _)
      | String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "RoundingMode" -- built-in-sort; so don't declare.
      = []
    declSort (String
    s, Maybe [String]
    Nothing) = [ String
    "(declare-sort " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " 0)  ; N.B. Uninterpreted sort."
                            , String
    "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_witness () " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                            ]
    declSort (String
    s, Just [String]
    fs) = [ String
    "(declare-datatypes ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " 0)) ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\String
    c -> String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")") [String]
    fs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")))"
                            , String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_constrIndex ((x " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) Int"
                            ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "   " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> Int -> String
    forall {t}. (Show t, Num t) => [String] -> t -> String
    body [String]
    fs (Int
    0::Int)] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    ")"]
            where body :: [String] -> t -> String
    body []     t
    _ = String
    ""
                  body [String
    _]    t
    i = t -> String
    forall a. Show a => a -> String
    show t
    i
                  body (String
    c:[String]
    cs) t
    i = String
    "(ite (= x " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ t -> String
    forall a. Show a => a -> String
    show t
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> t -> String
    body [String]
    cs (t
    it -> t -> t
    forall a. Num a => a -> a -> a
    +t
    1) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    -- | Declare tuple datatypes
    --
    -- eg:
    --
    -- @
    -- (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
    --                                     ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
    --                                                   (proj_2_SBVTuple2 T2))))))
    -- @
    declTuple :: Int -> [String]
    declTuple :: Int -> [String]
    declTuple Int
    arity
      | Int
    arity Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = [String
    "(declare-datatypes ((SBVTuple0 0)) (((mkSBVTuple0))))"]
      | Int
    arity Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = String -> [String]
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.declTuple: Unexpected one-tuple"
      | Bool
    True       =    (String
    l1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "(par (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [Int -> String
    forall a. Show a => a -> String
    param Int
    i | Int
    i <- [Int
    1..Int
    arity]] String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")")
                     String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  [Int -> String
    forall {a}. (Eq a, Num a) => a -> String
    pre Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    proj Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    post Int
    i    | Int
    i <- [Int
    1..Int
    arity]]
      where l1 :: String
    l1     = String
    "(declare-datatypes ((SBVTuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    arity String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    arity String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) ("
            l2 :: String
    l2     = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    l1) Char
    ' ' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "((mkSBVTuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    arity String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " "
            tab :: String
    tab    = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    l2) Char
    ' '

            pre :: a -> String
    pre a
    1  = String
    l2
            pre a
    _  = String
    tab

            proj :: a -> String
    proj a
    i = String
    "(proj_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_SBVTuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    arity String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    param a
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            post :: Int -> String
    post Int
    i = if Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    arity then String
    ")))))" else String
    ""

            param :: a -> String
    param a
    i = String
    "T" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i

    -- | Find the set of tuple sizes to declare, eg (2-tuple, 5-tuple).
    -- NB. We do *not* need to recursively go into list/tuple kinds here,
    -- because register-kind function automatically registers all subcomponent
    -- kinds, thus everything we need is available at the top-level.
    findTupleArities :: Set Kind -> [Int]
    findTupleArities :: Set Kind -> [Int]
    findTupleArities Set Kind
    ks = Set Int -> [Int]
    forall a. Set a -> [a]
    Set.toAscList
                        (Set Int -> [Int]) -> Set Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ ([Kind] -> Int) -> Set [Kind] -> Set Int
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map [Kind] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length
                        (Set [Kind] -> Set Int) -> Set [Kind] -> Set Int
    forall a b. (a -> b) -> a -> b
    $ [[Kind]] -> Set [Kind]
    forall a. Ord a => [a] -> Set a
    Set.fromList [ [Kind]
    tupKs | KTuple [Kind]
    tupKs <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    ks ]

    -- | Is @Either@ being used?
    containsSum :: Set Kind -> Bool
    containsSum :: Set Kind -> Bool
    containsSum = Bool -> Bool
    not (Bool -> Bool) -> (Set Kind -> Bool) -> Set Kind -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set Kind -> Bool
    forall a. Set a -> Bool
    Set.null (Set Kind -> Bool) -> (Set Kind -> Set Kind) -> Set Kind -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Kind -> Bool) -> Set Kind -> Set Kind
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter Kind -> Bool
    forall a. HasKind a => a -> Bool
    isEither

    -- | Is @Maybe@ being used?
    containsMaybe :: Set Kind -> Bool
    containsMaybe :: Set Kind -> Bool
    containsMaybe = Bool -> Bool
    not (Bool -> Bool) -> (Set Kind -> Bool) -> Set Kind -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set Kind -> Bool
    forall a. Set a -> Bool
    Set.null (Set Kind -> Bool) -> (Set Kind -> Set Kind) -> Set Kind -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Kind -> Bool) -> Set Kind -> Set Kind
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter Kind -> Bool
    forall a. HasKind a => a -> Bool
    isMaybe

    -- | Is @Rational@ being used?
    containsRationals :: Set Kind -> Bool
    containsRationals :: Set Kind -> Bool
    containsRationals = Bool -> Bool
    not (Bool -> Bool) -> (Set Kind -> Bool) -> Set Kind -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set Kind -> Bool
    forall a. Set a -> Bool
    Set.null (Set Kind -> Bool) -> (Set Kind -> Set Kind) -> Set Kind -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Kind -> Bool) -> Set Kind -> Set Kind
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter Kind -> Bool
    forall a. HasKind a => a -> Bool
    isRational

    declSum :: [String]
    declSum :: [String]
    declSum = [ String
    "(declare-datatypes ((SBVEither 2)) ((par (T1 T2)"
              , String
    "                                    ((left_SBVEither  (get_left_SBVEither  T1))"
              , String
    "                                     (right_SBVEither (get_right_SBVEither T2))))))"
              ]

    declMaybe :: [String]
    declMaybe :: [String]
    declMaybe = [ String
    "(declare-datatypes ((SBVMaybe 1)) ((par (T)"
                , String
    "                                    ((nothing_SBVMaybe)"
                , String
    "                                     (just_SBVMaybe (get_just_SBVMaybe T))))))"
                ]

    -- Internally, we do *not* keep the rationals in reduced form! So, the boolean operators explicitly do the math
    -- to make sure equivalent values are treated correctly.
    declRationals :: [String]
    declRationals :: [String]
    declRationals = [ String
    "(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.eq ((x SBVRational) (y SBVRational)) Bool"
                    , String
    "   (= (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                    , String
    "      (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                    , String
    ")"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool"
                    , String
    "   (not (sbv.rat.eq x y))"
                    , String
    ")"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool"
                    , String
    "   (<  (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                    , String
    "       (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                    , String
    ")"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool"
                    , String
    "   (<= (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                    , String
    "       (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                    , String
    ")"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational"
                    , String
    "   (SBV.Rational (+ (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                    , String
    "                    (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                    , String
    "                 (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"
                    , String
    ")"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational"
                    , String
    "   (SBV.Rational (- (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                    , String
    "                    (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                    , String
    "                 (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"
                    , String
    ")"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational"
                    , String
    "   (SBV.Rational (* (sbv.rat.numerator   x) (sbv.rat.numerator y))"
                    , String
    "                 (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"
                    , String
    ")"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.uneg ((x SBVRational)) SBVRational"
                    , String
    "   (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))"
                    , String
    ")"
                    , String
    ""
                    , String
    "(define-fun sbv.rat.abs ((x SBVRational)) SBVRational"
                    , String
    "   (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))"
                    , String
    ")"
                    ]

    -- | Convert in a query context.
    -- NB. We do not store everything in @newKs@ below, but only what we need
    -- to do as an extra in the incremental context. See `Data.SBV.Core.Symbolic.registerKind`
    -- for a list of what we include, in case something doesn't show up
    -- and you need it!
    cvtInc :: SMTLibIncConverter [String]
    cvtInc :: SMTLibIncConverter [String]
    cvtInc ProgInfo
    curProgInfo [NamedSymVar]
    inps Set Kind
    newKs (CnstMap
    allConsts, [(SV, CV)]
    consts) [(Int, ArrayInfo)]
    arrs [((Int, Kind, Kind), [SV])]
    tbls [(String, (Maybe [String], SBVType))]
    uis (SBVPgm Seq (SV, SBVExpr)
    asgnsSeq) Seq (Bool, [(String, String)], SV)
    cstrs SMTConfig
    cfg =
                -- any new settings?
                   [String]
    settings
                -- sorts
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, Maybe [String]) -> [String])
    -> [(String, Maybe [String])] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (String, Maybe [String]) -> [String]
    declSort [(String
    s, Maybe [String]
    dt) | KUserSort String
    s Maybe [String]
    dt <- [Kind]
    newKinds]
                -- tuples. NB. Only declare the new sizes, old sizes persist.
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (Int -> [String]) -> [Int] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Int -> [String]
    declTuple (Set Kind -> [Int]
    findTupleArities Set Kind
    newKs)
                -- sums
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if Set Kind -> Bool
    containsSum   Set Kind
    newKs then [String]
    declSum   else [])
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if Set Kind -> Bool
    containsMaybe Set Kind
    newKs then [String]
    declMaybe else [])
                -- constants
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, CV) -> [String]) -> [(SV, CV)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (SMTConfig -> (SV, CV) -> [String]
    declConst SMTConfig
    cfg) [(SV, CV)]
    consts
                -- inputs
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (NamedSymVar -> [String]) -> [NamedSymVar] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NamedSymVar -> [String]
    declInp [NamedSymVar]
    inps
                -- arrays
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    arrayConstants
                -- uninterpreteds
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, (Maybe [String], SBVType)) -> [String])
    -> [(String, (Maybe [String], SBVType))] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (ProgInfo -> (String, (Maybe [String], SBVType)) -> [String]
    declUI ProgInfo
    curProgInfo) [(String, (Maybe [String], SBVType))]
    uis
                -- table declarations
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    tableDecls
                -- expressions
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, SBVExpr) -> [String]) -> [(SV, SBVExpr)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (ProgInfo
    -> SMTConfig
    -> TableMap
    -> Map Op String
    -> (SV, SBVExpr)
    -> [String]
    declDef ProgInfo
    curProgInfo SMTConfig
    cfg TableMap
    tableMap Map Op String
    forall {k} {a}. Map k a
    funcMap) (Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (SV, SBVExpr)
    asgnsSeq)
                -- delayed equalities
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    arrayDelayeds
                -- table setups
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    tableAssigns
                -- array setups
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    arraySetups
                -- extra constraints
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((Bool, [(String, String)], SV) -> String)
    -> [(Bool, [(String, String)], SV)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Bool
    isSoft, [(String, String)]
    attr, SV
    v) -> String
    "(assert" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (if Bool
    isSoft then String
    "-soft " else String
    " ") String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)] -> String -> String
    addAnnotations [(String, String)]
    attr (SV -> String
    cvtSV SV
    v) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")") (Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (Bool, [(String, String)], SV)
    cstrs)
      where -- The following is not really kosher; if it happens that a "new" variant of a function is used only incrementally.
            -- But we'll punt on this for now, as it should be rare and can be "worked-around" if necessary.
            funcMap :: Map k a
    funcMap = Map k a
    forall {k} {a}. Map k a
    M.empty

            rm :: RoundingMode
    rm = SMTConfig -> RoundingMode
    roundingMode SMTConfig
    cfg

            newKinds :: [Kind]
    newKinds = Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    newKs

            declInp :: NamedSymVar -> [String]
    declInp (NamedSymVar -> SV
    getSV -> SV
    s) = SV -> SBVType -> Maybe String -> [String]
    declareFun SV
    s ([Kind] -> SBVType
    SBVType [SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s]) Maybe String
    forall a. Maybe a
    Nothing

            ([[String]]
    arrayConstants, [[String]]
    arrayDelayeds, [[String]]
    arraySetups) = [([String], [String], [String])]
    -> ([[String]], [[String]], [[String]])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 ([([String], [String], [String])]
     -> ([[String]], [[String]], [[String]]))
    -> [([String], [String], [String])]
    -> ([[String]], [[String]], [[String]])
    forall a b. (a -> b) -> a -> b
    $ ((Int, ArrayInfo) -> ([String], [String], [String]))
    -> [(Int, ArrayInfo)] -> [([String], [String], [String])]
    forall a b. (a -> b) -> [a] -> [b]
    map (SMTConfig
    -> CnstMap -> (Int, ArrayInfo) -> ([String], [String], [String])
    declArray SMTConfig
    cfg CnstMap
    allConsts) [(Int, ArrayInfo)]
    arrs

            allTables :: [(((Int, Kind, Kind), [SV]), [String])]
    allTables = [(((Int, Kind, Kind), [SV])
    t, ([String] -> [String])
    -> ([String] -> [String]) -> Either [String] [String] -> [String]
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either [String] -> [String]
    forall a. a -> a
    id [String] -> [String]
    forall a. a -> a
    id (RoundingMode
    -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String]
    genTableData RoundingMode
    rm (((SV, CV) -> SV) -> [(SV, CV)] -> [SV]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, CV) -> SV
    forall a b. (a, b) -> a
    fst [(SV, CV)]
    consts) ((Int, Kind, Kind), [SV])
    t)) | ((Int, Kind, Kind), [SV])
    t <- [((Int, Kind, Kind), [SV])]
    tbls]
            ([String]
    tableDecls, [[String]]
    tableAssigns) = [(String, [String])] -> ([String], [[String]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(String, [String])] -> ([String], [[String]]))
    -> [(String, [String])] -> ([String], [[String]])
    forall a b. (a -> b) -> a -> b
    $ ((((Int, Kind, Kind), [SV]), [String]) -> (String, [String]))
    -> [(((Int, Kind, Kind), [SV]), [String])] -> [(String, [String])]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
    mkTable [(((Int, Kind, Kind), [SV]), [String])]
    allTables

            tableMap :: TableMap
    tableMap  = [(Int, String)] -> TableMap
    forall a. [(Int, a)] -> IntMap a
    IM.fromList ([(Int, String)] -> TableMap) -> [(Int, String)] -> TableMap
    forall a b. (a -> b) -> a -> b
    $ ((((Int, Kind, Kind), [SV]), [String]) -> (Int, String))
    -> [(((Int, Kind, Kind), [SV]), [String])] -> [(Int, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Int, Kind, Kind), [SV]), [String]) -> (Int, String)
    forall {a} {b} {c} {b} {b}.
    Show a =>
    (((a, b, c), b), b) -> (a, String)
    mkIdx [(((Int, Kind, Kind), [SV]), [String])]
    allTables
              where mkIdx :: (((a, b, c), b), b) -> (a, String)
    mkIdx (((a
    t, b
    _, c
    _), b
    _), b
    _) = (a
    t, String
    "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    t)

            -- If we need flattening in models, do emit the required lines if preset
            settings :: [String]
    settings
              | (Kind -> Bool) -> [Kind] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    needsFlattening [Kind]
    newKinds
              = [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([Maybe [String]] -> [[String]]
    forall a. [Maybe a] -> [a]
    catMaybes [SolverCapabilities -> Maybe [String]
    supportsFlattenedModels SolverCapabilities
    solverCaps])
              | Bool
    True
              = []
              where solverCaps :: SolverCapabilities
    solverCaps = SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)

    declDef :: ProgInfo -> SMTConfig -> TableMap -> FunctionMap -> (SV, SBVExpr) -> [String]
    declDef :: ProgInfo
    -> SMTConfig
    -> TableMap
    -> Map Op String
    -> (SV, SBVExpr)
    -> [String]
    declDef ProgInfo
    curProgInfo SMTConfig
    cfg TableMap
    tableMap Map Op String
    funcMap (SV
    s, SBVExpr
    expr) =
            case SBVExpr
    expr of
              SBVApp  (Label String
    m) [SV
    e] -> SMTConfig -> (SV, String) -> Maybe String -> [String]
    defineFun SMTConfig
    cfg (SV
    s, SV -> String
    cvtSV                                       SV
    e) (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    m)
              SBVExpr
    e                     -> SMTConfig -> (SV, String) -> Maybe String -> [String]
    defineFun SMTConfig
    cfg (SV
    s, ProgInfo
    -> SolverCapabilities
    -> RoundingMode
    -> TableMap
    -> Map Op String
    -> SBVExpr
    -> String
    cvtExp ProgInfo
    curProgInfo SolverCapabilities
    caps RoundingMode
    rm TableMap
    tableMap Map Op String
    funcMap SBVExpr
    e) Maybe String
    forall a. Maybe a
    Nothing
      where caps :: SolverCapabilities
    caps = SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)
            rm :: RoundingMode
    rm   = SMTConfig -> RoundingMode
    roundingMode SMTConfig
    cfg

    defineFun :: SMTConfig -> (SV, String) -> Maybe String -> [String]
    defineFun :: SMTConfig -> (SV, String) -> Maybe String -> [String]
    defineFun SMTConfig
    cfg (SV
    s, String
    def) Maybe String
    mbComment
       | Bool
    hasDefFun = [String
    "(define-fun "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    varT String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    def String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cmnt]
       | Bool
    True      = [ String
    "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    varT String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cmnt
                     , String
    "(assert (= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    var String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    def String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
                     ]
      where var :: String
    var  = SV -> String
    forall a. Show a => a -> String
    show SV
    s
            varT :: String
    varT = String
    var String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [SV] -> SV -> String
    svFunType [] SV
    s
            cmnt :: String
    cmnt = String -> (String -> String) -> Maybe String -> String
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe String
    "" (String
    " ; " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) Maybe String
    mbComment

            hasDefFun :: Bool
    hasDefFun = SolverCapabilities -> Bool
    supportsDefineFun (SolverCapabilities -> Bool) -> SolverCapabilities -> Bool
    forall a b. (a -> b) -> a -> b
    $ SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)

    -- Declare constants. NB. We don't declare true/false; but just inline those as necessary
    declConst :: SMTConfig -> (SV, CV) -> [String]
    declConst :: SMTConfig -> (SV, CV) -> [String]
    declConst SMTConfig
    cfg (SV
    s, CV
    c)
      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV Bool -> Bool -> Bool
    || SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV
      = []
      | Bool
    True
      = SMTConfig -> (SV, String) -> Maybe String -> [String]
    defineFun SMTConfig
    cfg (SV
    s, RoundingMode -> CV -> String
    cvtCV (SMTConfig -> RoundingMode
    roundingMode SMTConfig
    cfg) CV
    c) Maybe String
    forall a. Maybe a
    Nothing

    -- Make a function equality of nm against the internal function fun
    mkRelEq :: String -> (String, String) -> Kind -> String
    mkRelEq :: String -> (String, String) -> Kind -> String
    mkRelEq String
    nm (String
    fun, String
    order) Kind
    ak = String
    res
       where lhs :: String
    lhs = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " x y)"
             rhs :: String
    rhs = String
    "((_ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fun String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    order String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") x y)"
             tk :: String
    tk  = Kind -> String
    smtType Kind
    ak
             res :: String
    res = String
    "(forall ((x " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    tk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") (y " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    tk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) (= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    lhs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rhs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"

    declUI :: ProgInfo -> (String, (Maybe [String], SBVType)) -> [String]
    declUI :: ProgInfo -> (String, (Maybe [String], SBVType)) -> [String]
    declUI ProgInfo{[(String, String)]
    progTransClosures :: [(String, String)]
    progTransClosures :: ProgInfo -> [(String, String)]
    progTransClosures} (String
    i, (Maybe [String]
    _, SBVType
    t)) = String -> SBVType -> Maybe String -> [String]
    declareName String
    i SBVType
    t Maybe String
    forall a. Maybe a
    Nothing [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    declClosure
      where declClosure :: [String]
    declClosure | Just String
    external <- String -> [(String, String)] -> Maybe String
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    i [(String, String)]
    progTransClosures
                        =  String -> SBVType -> Maybe String -> [String]
    declareName String
    external SBVType
    t Maybe String
    forall a. Maybe a
    Nothing
                        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> (String, String) -> Kind -> String
    mkRelEq String
    external (String
    "transitive-closure", String
    i) (SBVType -> Kind
    argKind SBVType
    t) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"]
                        | Bool
    True
                        = []

            argKind :: SBVType -> Kind
    argKind (SBVType [Kind
    ka, Kind
    _, Kind
    KBool]) = Kind
    ka
            argKind SBVType
    _                        = String -> Kind
    forall a. HasCallStack => String -> a
    error (String -> Kind) -> String -> Kind
    forall a b. (a -> b) -> a -> b
    $ String
    "declUI: Unexpected type for name: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, SBVType) -> String
    forall a. Show a => a -> String
    show (String
    i, SBVType
    t)

    -- Note that even though we get all user defined-functions here (i.e., lambda and axiom), we can only have defined-functions
    -- and axioms. We spit axioms as is; and topologically sort the definitions.
    declUserFuns :: [SMTDef] -> [String]
    declUserFuns :: [SMTDef] -> [String]
    declUserFuns [SMTDef]
    ds
      | Bool -> Bool
    not ([SMTDef] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SMTDef]
    lambdas)
      = String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.declUserFuns: Unexpected anonymous functions in declDef:" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (SMTDef -> String) -> [SMTDef] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SMTDef -> String
    forall a. Show a => a -> String
    show [SMTDef]
    lambdas
      | Bool
    True
      = [SMTDef] -> [String]
    declFuncs [SMTDef]
    others
      where ([SMTDef]
    lambdas, [SMTDef]
    others) = (SMTDef -> Bool) -> [SMTDef] -> ([SMTDef], [SMTDef])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition SMTDef -> Bool
    isLam [SMTDef]
    ds
            isLam :: SMTDef -> Bool
    isLam SMTLam{} = Bool
    True
            isLam SMTDef{} = Bool
    False

    -- We need to topologically sort the user given definitions and axioms and put them in the proper order and construct.
    -- Note that there are no anonymous functions at this level.
    declFuncs :: [SMTDef] -> [String]
    declFuncs :: [SMTDef] -> [String]
    declFuncs [SMTDef]
    ds = (SCC SMTDef -> String) -> [SCC SMTDef] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SCC SMTDef -> String
    declGroup [SCC SMTDef]
    sorted
      where mkNode :: SMTDef -> (SMTDef, String, [String])
    mkNode SMTDef
    d = (SMTDef
    d, SMTDef -> String
    getKey SMTDef
    d, SMTDef -> [String]
    getDeps SMTDef
    d)

            getKey :: SMTDef -> String
    getKey SMTDef
    d = case SMTDef
    d of
                         SMTDef String
    n Kind
    _ [String]
    _ Maybe String
    _ Int -> String
    _ -> String
    n
                         SMTLam{}         -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.declFuns: Unexpected definition kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTDef -> String
    forall a. Show a => a -> String
    show SMTDef
    d

            getDeps :: SMTDef -> [String]
    getDeps (SMTDef String
    _ Kind
    _ [String]
    d Maybe String
    _ Int -> String
    _) = [String]
    d
            getDeps l :: SMTDef
    l@SMTLam{}         = String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.declFuns: Unexpected definition kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTDef -> String
    forall a. Show a => a -> String
    show SMTDef
    l

            mkDecl :: Maybe String -> String -> String
    mkDecl Maybe String
    Nothing  String
    rt = String
    "() "    String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rt
            mkDecl (Just String
    p) String
    rt = String
    p String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rt

            sorted :: [SCC SMTDef]
    sorted = [(SMTDef, String, [String])] -> [SCC SMTDef]
    forall key node. Ord key => [(node, key, [key])] -> [SCC node]
    DG.stronglyConnComp ((SMTDef -> (SMTDef, String, [String]))
    -> [SMTDef] -> [(SMTDef, String, [String])]
    forall a b. (a -> b) -> [a] -> [b]
    map SMTDef -> (SMTDef, String, [String])
    mkNode [SMTDef]
    ds)

            declGroup :: SCC SMTDef -> String
    declGroup (DG.AcyclicSCC SMTDef
    b)  = Bool -> SMTDef -> String
    declUserDef Bool
    False SMTDef
    b
            declGroup (DG.CyclicSCC  [SMTDef]
    bs) = case [SMTDef]
    bs of
                                             []  -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.declFuns: Impossible happened: an empty cyclic group was returned!"
                                             [SMTDef
    x] -> Bool -> SMTDef -> String
    declUserDef Bool
    True SMTDef
    x
                                             [SMTDef]
    xs  -> [SMTDef] -> String
    declUserDefMulti [SMTDef]
    xs

            declUserDef :: Bool -> SMTDef -> String
    declUserDef Bool
    _ d :: SMTDef
    d@SMTLam{} = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.declFuns: Unexpected anonymous lambda in user-defined functions: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTDef -> String
    forall a. Show a => a -> String
    show SMTDef
    d
            declUserDef Bool
    isRec (SMTDef String
    nm Kind
    fk [String]
    deps Maybe String
    param Int -> String
    body) = (String
    "; -- user given definition: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    recursive String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    frees String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n") String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
               where (String
    recursive, String
    definer) | Bool
    isRec = (String
    " [Recursive]", String
    "define-fun-rec")
                                          | Bool
    True  = (String
    "",             String
    "define-fun")

                     otherDeps :: [String]
    otherDeps = (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    /= String
    nm) [String]
    deps
                     frees :: String
    frees | [String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    otherDeps = String
    ""
                           | Bool
    True           = String
    " [Refers to: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    otherDeps String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"

                     decl :: String
    decl = Maybe String -> String -> String
    mkDecl Maybe String
    param (Kind -> String
    smtType Kind
    fk)

                     s :: String
    s = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    definer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    decl String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    body Int
    2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            -- declare a bunch of mutually-recursive functions
            declUserDefMulti :: [SMTDef] -> String
    declUserDefMulti [SMTDef]
    bs = [([String], String, String, String)] -> String
    render ([([String], String, String, String)] -> String)
    -> [([String], String, String, String)] -> String
    forall a b. (a -> b) -> a -> b
    $ (SMTDef -> ([String], String, String, String))
    -> [SMTDef] -> [([String], String, String, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map SMTDef -> ([String], String, String, String)
    collect [SMTDef]
    bs
              where collect :: SMTDef -> ([String], String, String, String)
    collect d :: SMTDef
    d@SMTLam{} = String -> ([String], String, String, String)
    forall a. HasCallStack => String -> a
    error (String -> ([String], String, String, String))
    -> String -> ([String], String, String, String)
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.declFuns: Unexpected lambda in user-defined mutual-recursion group: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTDef -> String
    forall a. Show a => a -> String
    show SMTDef
    d
                    collect (SMTDef String
    nm Kind
    fk [String]
    deps Maybe String
    param Int -> String
    body) = ([String]
    deps, String
    nm, Char
    '(' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  String
    decl String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")", Int -> String
    body Int
    3)
                      where decl :: String
    decl = Maybe String -> String -> String
    mkDecl Maybe String
    param (Kind -> String
    smtType Kind
    fk)

                    render :: [([String], String, String, String)] -> String
    render [([String], String, String, String)]
    defs = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
                                      [ String
    "; -- user given mutually-recursive definitions: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String
    n | ([String]
    _, String
    n, String
    _, String
    _) <- [([String], String, String, String)]
    defs]
                                      , String
    "(define-funs-rec"
                                      ]
                                   [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ Int -> String
    forall {a}. (Eq a, Num a) => a -> String
    open Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([String], String, String, String) -> String
    forall {a} {b} {c} {d}. (a, b, c, d) -> c
    param ([String], String, String, String)
    d String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    close1 Int
    i | (Int
    i, ([String], String, String, String)
    d) <- [Int]
    -> [([String], String, String, String)]
    -> [(Int, ([String], String, String, String))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    1..] [([String], String, String, String)]
    defs]
                                   [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ Int -> String
    forall {a}. (Eq a, Num a) => a -> String
    open Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([String], String, String, String) -> String
    forall {c}. ([String], String, c, String) -> String
    dump  ([String], String, String, String)
    d String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    close2 Int
    i | (Int
    i, ([String], String, String, String)
    d) <- [Int]
    -> [([String], String, String, String)]
    -> [(Int, ([String], String, String, String))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    1..] [([String], String, String, String)]
    defs]
                         where open :: a -> String
    open a
    1 = String
    "  ("
                               open a
    _ = String
    "   "

                               param :: (a, b, c, d) -> c
    param (a
    _, b
    _, c
    p, d
    _) = c
    p

                               dump :: ([String], String, c, String) -> String
    dump ([String]
    deps, String
    nm, c
    _, String
    body) = String
    "; Definition of: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ". [Refers to: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    deps String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"
                                                        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    body

                               ld :: Int
    ld = [([String], String, String, String)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [([String], String, String, String)]
    defs

                               close1 :: Int -> String
    close1 Int
    n = if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ld then String
    ")"  else String
    ""
                               close2 :: Int -> String
    close2 Int
    n = if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ld then String
    "))" else String
    ""

    mkTable :: (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
    mkTable :: (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
    mkTable (((Int
    i, Kind
    ak, Kind
    rk), [SV]
    _elts), [String]
    is) = (String
    decl, (Int -> String -> String) -> [Int] -> [String] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> String -> String
    wrap [(Int
    0::Int)..] [String]
    is [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    setup)
      where t :: String
    t       = String
    "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
            decl :: String
    decl    = String
    "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    ak String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    rk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            -- Arrange for initializers
            mkInit :: Int -> String
    mkInit Int
    idx   = String
    "table" 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
    "_initializer_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show (Int
    idx :: Int)
            initializer :: String
    initializer  = String
    "table" 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
    "_initializer"

            wrap :: Int -> String -> String
    wrap Int
    index String
    s = String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkInit Int
    index String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () Bool " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            lis :: Int
    lis  = [String] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [String]
    is

            setup :: [String]
    setup
              | Int
    lis Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0       = [ String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () Bool true) ; no initialization needed"
                                 ]
              | Int
    lis Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1       = [ String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () Bool " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkInit Int
    0 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                 , String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                 ]
              | Bool
    True           = [ String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () Bool (and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Int -> String) -> [Int] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> String
    mkInit [Int
    0..Int
    lis Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
                                 , String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                 ]
    nonConstTable :: (((Int, Kind, Kind), [SV]), [String]) -> String
    nonConstTable :: (((Int, Kind, Kind), [SV]), [String]) -> String
    nonConstTable (((Int
    i, Kind
    ak, Kind
    rk), [SV]
    _elts), [String]
    _) = String
    decl
      where t :: String
    t    = String
    "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
            decl :: String
    decl = String
    "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    ak String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    rk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    -- Left if all constants, Right if otherwise
    genTableData :: RoundingMode -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String]
    genTableData :: RoundingMode
    -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String]
    genTableData RoundingMode
    rm [SV]
    consts ((Int
    i, Kind
    aknd, Kind
    _), [SV]
    elts)
      | [(Bool, (String, String))] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Bool, (String, String))]
    post = [String] -> Either [String] [String]
    forall a b. a -> Either a b
    Left  (((Bool, (String, String)) -> String)
    -> [(Bool, (String, String))] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, String) -> String
    mkEntry ((String, String) -> String)
    -> ((Bool, (String, String)) -> (String, String))
    -> (Bool, (String, String))
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool, (String, String)) -> (String, String)
    forall a b. (a, b) -> b
    snd) [(Bool, (String, String))]
    pre)
      | Bool
    True      = [String] -> Either [String] [String]
    forall a b. b -> Either a b
    Right (((Bool, (String, String)) -> String)
    -> [(Bool, (String, String))] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, String) -> String
    mkEntry ((String, String) -> String)
    -> ((Bool, (String, String)) -> (String, String))
    -> (Bool, (String, String))
    -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool, (String, String)) -> (String, String)
    forall a b. (a, b) -> b
    snd) ([(Bool, (String, String))]
    pre [(Bool, (String, String))]
    -> [(Bool, (String, String))] -> [(Bool, (String, String))]
    forall a. [a] -> [a] -> [a]
    ++ [(Bool, (String, String))]
    post))
      where ([(Bool, (String, String))]
    pre, [(Bool, (String, String))]
    post) = ((Bool, (String, String)) -> Bool)
    -> [(Bool, (String, String))]
    -> ([(Bool, (String, String))], [(Bool, (String, String))])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (Bool, (String, String)) -> Bool
    forall a b. (a, b) -> a
    fst ((SV -> Int -> (Bool, (String, String)))
    -> [SV] -> [Int] -> [(Bool, (String, String))]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith SV -> Int -> (Bool, (String, String))
    forall {p}. Integral p => SV -> p -> (Bool, (String, String))
    mkElt [SV]
    elts [(Int
    0::Int)..])
            t :: String
    t           = String
    "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i

            mkElt :: SV -> p -> (Bool, (String, String))
    mkElt SV
    x p
    k   = (Bool
    isReady, (String
    idx, SV -> String
    cvtSV SV
    x))
              where idx :: String
    idx = RoundingMode -> CV -> String
    cvtCV RoundingMode
    rm (Kind -> p -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    aknd p
    k)
                    isReady :: Bool
    isReady = SV
    x SV -> Set SV -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set SV
    constsSet

            mkEntry :: (String, String) -> String
    mkEntry (String
    idx, String
    v) = String
    "(= (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    idx String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            constsSet :: Set SV
    constsSet = [SV] -> Set SV
    forall a. Ord a => [a] -> Set a
    Set.fromList [SV]
    consts

    -- Declare arrays
    declArray :: SMTConfig -> CnstMap -> (Int, ArrayInfo) -> ([String], [String], [String])
    declArray :: SMTConfig
    -> CnstMap -> (Int, ArrayInfo) -> ([String], [String], [String])
    declArray SMTConfig
    cfg CnstMap
    consts (Int
    i, (String
    _, (Kind
    aKnd, Kind
    bKnd), ArrayContext
    ctx)) = ( String
    adecl String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (Int -> String -> String) -> [Int] -> [String] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> String -> String
    wrap [(Int
    0::Int)..] (((Bool, String) -> String) -> [(Bool, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bool, String) -> String
    forall a b. (a, b) -> b
    snd [(Bool, String)]
    pre)
                                                       , (Int -> String -> String) -> [Int] -> [String] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> String -> String
    wrap [Int
    lpre..] (((Bool, String) -> String) -> [(Bool, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bool, String) -> String
    forall a b. (a, b) -> b
    snd [(Bool, String)]
    post)
                                                       , [String]
    setup
                                                       )
      where constMapping :: Map SV CV
    constMapping = [(SV, CV)] -> Map SV CV
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList [(SV
    s, CV
    c) | (CV
    c, SV
    s) <- CnstMap -> [(CV, SV)]
    forall k a. Map k a -> [(k, a)]
    M.assocs CnstMap
    consts]
            constNames :: [SV]
    constNames   = Map SV CV -> [SV]
    forall k a. Map k a -> [k]
    M.keys Map SV CV
    constMapping
            ([(Bool, String)]
    pre, [(Bool, String)]
    post) = ((Bool, String) -> Bool)
    -> [(Bool, String)] -> ([(Bool, String)], [(Bool, String)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (Bool, String) -> Bool
    forall a b. (a, b) -> a
    fst [(Bool, String)]
    ctxInfo
            nm :: String
    nm = String
    "array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i

            atyp :: String
    atyp  = String
    "(Array " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    aKnd String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    bKnd String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            adecl :: String
    adecl = case ArrayContext
    ctx of
                      ArrayFree (Right String
    lam)     -> String
    "(define-fun "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    atyp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    lam String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                      ArrayFree (Left (Just SV
    v)) -> String
    "(define-fun "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    atyp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " ((as const " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    atyp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    constInit SV
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
                      ArrayFree (Left Maybe SV
    Nothing)
                        | Kind
    bKnd Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KChar  ->  -- Can't support yet, because we need to make sure all the elements are length-1 strings. So, punt for now.
                                             String -> String
    forall a. String -> a
    tbd String
    "Free array declarations containing SChars"
                      ArrayContext
    _                  -> String
    "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    atyp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++                                                  String
    ")"

            -- CVC4 chokes if the initializer is not a constant. (Z3 is ok with it.) So, print it as
            -- a constant if we have it in the constants; otherwise, we merely print it and hope for the best.
            constInit :: SV -> String
    constInit SV
    v = case SV
    v SV -> Map SV CV -> Maybe CV
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` Map SV CV
    constMapping of
                            Maybe CV
    Nothing -> SV -> String
    cvtSV SV
    v                    -- Z3 will work, CVC4 will choke. Others don't even support this.
                            Just CV
    c  -> RoundingMode -> CV -> String
    cvtCV (SMTConfig -> RoundingMode
    roundingMode SMTConfig
    cfg) CV
    c -- Z3 and CVC4 will work. Other's don't support this.

            ctxInfo :: [(Bool, String)]
    ctxInfo = case ArrayContext
    ctx of
                        ArrayFree Either (Maybe SV) String
    _       -> []
                        ArrayMutate ArrayIndex
    j SV
    a SV
    b -> [((SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (SV -> [SV] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [SV]
    constNames) [SV
    a, SV
    b], String
    "(= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (store array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    j String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))")]
                        ArrayMerge  SV
    t ArrayIndex
    j ArrayIndex
    k -> [(SV
    t SV -> [SV] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [SV]
    constNames,            String
    "(= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    j String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))")]

            -- Arrange for initializers
            mkInit :: Int -> String
    mkInit Int
    idx    = String
    "array_" 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
    "_initializer_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show (Int
    idx :: Int)
            initializer :: String
    initializer   = String
    "array_" 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
    "_initializer"

            wrap :: Int -> String -> String
    wrap Int
    index String
    s = String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkInit Int
    index String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () Bool " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            lpre :: Int
    lpre          = [(Bool, String)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Bool, String)]
    pre
            lAll :: Int
    lAll          = Int
    lpre Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + [(Bool, String)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Bool, String)]
    post

            setup :: [String]
    setup
              | Int
    lAll Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = [ String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () Bool true) ; no initialization needed" ]
              | Int
    lAll Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = [ String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () Bool " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkInit Int
    0 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                            , String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                            ]
              | Bool
    True      = [ String
    "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " () Bool (and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Int -> String) -> [Int] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> String
    mkInit [Int
    0..Int
    lAll Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
                            , String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                            ]

    svType :: SV -> String
    svType :: SV -> String
    svType SV
    s = Kind -> String
    smtType (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s)

    svFunType :: [SV] -> SV -> String
    svFunType :: [SV] -> SV -> String
    svFunType [SV]
    ss SV
    s = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    svType [SV]
    ss) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    svType SV
    s

    cvtType :: SBVType -> String
    cvtType :: SBVType -> String
    cvtType (SBVType []) = String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!"
    cvtType (SBVType [Kind]
    xs) = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Kind -> String) -> [Kind] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Kind -> String
    smtType [Kind]
    body) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    ret
      where ([Kind]
    body, Kind
    ret) = ([Kind] -> [Kind]
    forall a. HasCallStack => [a] -> [a]
    init [Kind]
    xs, [Kind] -> Kind
    forall a. HasCallStack => [a] -> a
    last [Kind]
    xs)

    type TableMap    = IM.IntMap String
    type FunctionMap = M.Map Op String

    -- Present an SV, simply show
    cvtSV :: SV -> String
    cvtSV :: SV -> String
    cvtSV = SV -> String
    forall a. Show a => a -> String
    show

    cvtCV :: RoundingMode -> CV -> String
    cvtCV :: RoundingMode -> CV -> String
    cvtCV = RoundingMode -> CV -> String
    cvToSMTLib

    getTable :: TableMap -> Int -> String
    getTable :: TableMap -> Int -> String
    getTable TableMap
    m Int
    i
      | Just String
    tn <- Int
    i Int -> TableMap -> Maybe String
    forall a. Int -> IntMap a -> Maybe a
    `IM.lookup` TableMap
    m = String
    tn
      | Bool
    True                       = String
    "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i  -- constant tables are always named this way

    cvtExp :: ProgInfo -> SolverCapabilities -> RoundingMode -> TableMap -> FunctionMap -> SBVExpr -> String
    cvtExp :: ProgInfo
    -> SolverCapabilities
    -> RoundingMode
    -> TableMap
    -> Map Op String
    -> SBVExpr
    -> String
    cvtExp ProgInfo
    curProgInfo SolverCapabilities
    caps RoundingMode
    rm TableMap
    tableMap Map Op String
    functionMap expr :: SBVExpr
    expr@(SBVApp Op
    _ [SV]
    arguments) = SBVExpr -> String
    sh SBVExpr
    expr
      where hasPB :: Bool
    hasPB       = SolverCapabilities -> Bool
    supportsPseudoBooleans SolverCapabilities
    caps
            hasInt2bv :: Bool
    hasInt2bv   = SolverCapabilities -> Bool
    supportsInt2bv         SolverCapabilities
    caps
            hasDistinct :: Bool
    hasDistinct = SolverCapabilities -> Bool
    supportsDistinct       SolverCapabilities
    caps
            specialRels :: [SpecialRelOp]
    specialRels = ProgInfo -> [SpecialRelOp]
    progSpecialRels        ProgInfo
    curProgInfo

            bvOp :: Bool
    bvOp     = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all SV -> Bool
    forall a. HasKind a => a -> Bool
    isBounded   [SV]
    arguments
            intOp :: Bool
    intOp    = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    isUnbounded [SV]
    arguments
            ratOp :: Bool
    ratOp    = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    isRational  [SV]
    arguments
            realOp :: Bool
    realOp   = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    isReal      [SV]
    arguments
            fpOp :: Bool
    fpOp     = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (\SV
    a -> SV -> Bool
    forall a. HasKind a => a -> Bool
    isDouble SV
    a Bool -> Bool -> Bool
    || SV -> Bool
    forall a. HasKind a => a -> Bool
    isFloat SV
    a Bool -> Bool -> Bool
    || SV -> Bool
    forall a. HasKind a => a -> Bool
    isFP SV
    a) [SV]
    arguments
            boolOp :: Bool
    boolOp   = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all SV -> Bool
    forall a. HasKind a => a -> Bool
    isBoolean   [SV]
    arguments
            charOp :: Bool
    charOp   = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    isChar      [SV]
    arguments
            stringOp :: Bool
    stringOp = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    isString    [SV]
    arguments
            listOp :: Bool
    listOp   = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    isList      [SV]
    arguments

            bad :: a
    bad | Bool
    intOp = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2: Unsupported operation on unbounded integers: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVExpr -> String
    forall a. Show a => a -> String
    show SBVExpr
    expr
                | Bool
    True  = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2: Unsupported operation on real values: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVExpr -> String
    forall a. Show a => a -> String
    show SBVExpr
    expr

            ensureBVOrBool :: Bool
    ensureBVOrBool = Bool
    bvOp Bool -> Bool -> Bool
    || Bool
    boolOp Bool -> Bool -> Bool
    || Bool
    forall {a}. a
    bad
            ensureBV :: Bool
    ensureBV       = Bool
    bvOp Bool -> Bool -> Bool
    || Bool
    forall {a}. a
    bad

            addRM :: String -> String
    addRM String
    s = String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ RoundingMode -> String
    smtRoundingMode RoundingMode
    rm

            -- lift a binary op
            lift2 :: String -> p -> [String] -> String
    lift2  String
    o p
    _ [String
    x, String
    y] = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            lift2  String
    o p
    _ [String]
    sbvs   = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2.sh.lift2: Unexpected arguments: "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, [String]) -> String
    forall a. Show a => a -> String
    show (String
    o, [String]
    sbvs)

            -- lift an arbitrary arity operator
            liftN :: String -> p -> [String] -> String
    liftN String
    o p
    _ [String]
    xs = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            -- lift a binary operation with rounding-mode added; used for floating-point arithmetic
            lift2WM :: String -> String -> p -> [String] -> String
    lift2WM String
    o String
    fo | Bool
    fpOp = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 (String -> String
    addRM String
    fo)
                         | Bool
    True = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    o

            lift1FP :: String -> String -> p -> [String] -> String
    lift1FP String
    o String
    fo | Bool
    fpOp = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift1 String
    fo
                         | Bool
    True = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift1 String
    o

            liftAbs :: Bool -> [String] -> String
    liftAbs Bool
    sgned [String]
    args | Bool
    fpOp        = String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift1 String
    "fp.abs" Bool
    sgned [String]
    args
                               | Bool
    intOp       = String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift1 String
    "abs"    Bool
    sgned [String]
    args
                               | Bool
    bvOp, Bool
    sgned = String -> String -> String -> String
    mkAbs ([String] -> String
    forall a. HasCallStack => [a] -> a
    head [String]
    args) String
    "bvslt" String
    "bvneg"
                               | Bool
    bvOp        = [String] -> String
    forall a. HasCallStack => [a] -> a
    head [String]
    args
                               | Bool
    True        = String -> String -> String -> String
    mkAbs ([String] -> String
    forall a. HasCallStack => [a] -> a
    head [String]
    args) String
    "<"     String
    "-"
              where mkAbs :: String -> String -> String -> String
    mkAbs String
    x String
    cmp String
    neg = String
    "(ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ltz String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nx String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                      where ltz :: String
    ltz = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cmp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    z String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                            nx :: String
    nx  = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    neg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                            z :: String
    z   = RoundingMode -> CV -> String
    cvtCV RoundingMode
    rm (Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    arguments)) (Integer
    0::Integer))

            lift2B :: String -> String -> p -> [String] -> String
    lift2B String
    bOp String
    vOp
              | Bool
    boolOp = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    bOp
              | Bool
    True   = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    vOp

            lift1B :: String -> String -> p -> [String] -> String
    lift1B String
    bOp String
    vOp
              | Bool
    boolOp = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift1 String
    bOp
              | Bool
    True   = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift1 String
    vOp

            eqBV :: p -> [String] -> String
    eqBV  = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    "="
            neqBV :: p -> [String] -> String
    neqBV = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    liftN String
    "distinct"

            equal :: p -> [String] -> String
    equal p
    sgn [String]
    sbvs
              | Bool
    fpOp = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    "fp.eq" p
    sgn [String]
    sbvs
              | Bool
    True = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    "="     p
    sgn [String]
    sbvs

            -- Do not use distinct on floats; because +0/-0, and NaNs mess
            -- up the meaning. Just go with reqular equals.
            notEqual :: p -> [String] -> String
    notEqual p
    sgn [String]
    sbvs
              | Bool
    fpOp Bool -> Bool -> Bool
    || Bool -> Bool
    not Bool
    hasDistinct = [String] -> String
    liftP [String]
    sbvs
              | Bool
    True                    = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    liftN String
    "distinct" p
    sgn [String]
    sbvs
              where liftP :: [String] -> String
    liftP xs :: [String]
    xs@[String
    _, String
    _] = String
    "(not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ p -> [String] -> String
    forall {p}. p -> [String] -> String
    equal p
    sgn [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                    liftP [String]
    args      = String
    "(and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ([String] -> [String]
    walk [String]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

                    walk :: [String] -> [String]
    walk []     = []
                    walk (String
    e:[String]
    es) = (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\String
    e' -> [String] -> String
    liftP [String
    e, String
    e']) [String]
    es [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String] -> [String]
    walk [String]
    es

            lift2S :: String -> String -> Bool -> [String] -> String
    lift2S String
    oU String
    oS Bool
    sgn = String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 (if Bool
    sgn then String
    oS else String
    oU) Bool
    sgn
            liftNS :: String -> String -> Bool -> [String] -> String
    liftNS String
    oU String
    oS Bool
    sgn = String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    liftN (if Bool
    sgn then String
    oS else String
    oU) Bool
    sgn

            lift2Cmp :: String -> String -> p -> [String] -> String
    lift2Cmp String
    o String
    fo | Bool
    fpOp = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    fo
                          | Bool
    True = String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    o

            unintComp :: String -> [String] -> String
    unintComp String
    o [String
    a, String
    b]
              | KUserSort String
    s (Just [String]
    _) <- SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    arguments)
              = let idx :: String -> String
    idx String
    v = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_constrIndex " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" in String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    idx String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    idx String
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            unintComp String
    o [String]
    sbvs = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.sh.unintComp: Unexpected arguments: "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, [String], [Kind]) -> String
    forall a. Show a => a -> String
    show (String
    o, [String]
    sbvs, (SV -> Kind) -> [SV] -> [Kind]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf [SV]
    arguments)

            stringOrChar :: Kind -> Bool
    stringOrChar Kind
    KString = Bool
    True
            stringOrChar Kind
    KChar   = Bool
    True
            stringOrChar Kind
    _       = Bool
    False
            stringCmp :: Bool -> String -> [String] -> String
    stringCmp Bool
    swap String
    o [String
    a, String
    b]
              | Kind -> Bool
    stringOrChar (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    arguments))
              = let (String
    a1, String
    a2) | Bool
    swap = (String
    b, String
    a)
                             | Bool
    True = (String
    a, String
    b)
                in String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            stringCmp Bool
    _ String
    o [String]
    sbvs = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.sh.stringCmp: Unexpected arguments: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, [String]) -> String
    forall a. Show a => a -> String
    show (String
    o, [String]
    sbvs)

            -- NB. Likewise for sequences
            seqCmp :: Bool -> String -> [String] -> String
    seqCmp Bool
    swap String
    o [String
    a, String
    b]
              | KList{} <- SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    arguments)
              = let (String
    a1, String
    a2) | Bool
    swap = (String
    b, String
    a)
                             | Bool
    True = (String
    a, String
    b)
                in String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            seqCmp Bool
    _ String
    o [String]
    sbvs = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.sh.seqCmp: Unexpected arguments: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, [String]) -> String
    forall a. Show a => a -> String
    show (String
    o, [String]
    sbvs)

            lift1 :: String -> p -> [String] -> String
    lift1  String
    o p
    _ [String
    x]    = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            lift1  String
    o p
    _ [String]
    sbvs   = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, [String]) -> String
    forall a. Show a => a -> String
    show (String
    o, [String]
    sbvs)

            -- We fully qualify the constructor with their types to work around type checking issues
            -- Note that this is rather bizarre, as we're tagging the constructor with its *result* type,
            -- not its full function type as one would expect. But this is per the spec: Pg. 27 of SMTLib 2.6 spec
            -- says:
            --
            --    To simplify sort checking, a function symbol in a term can be annotated with one of its result sorts sigma.
            --
            -- I wish it was the full type here not just the result, but we go with the spec. Also see: <http://github.com/Z3Prover/z3/issues/2135>
            -- and in particular <http://github.com/Z3Prover/z3/issues/2135#issuecomment-477636435>
            dtConstructor :: String -> [SV] -> Kind -> String
    dtConstructor String
    fld [SV]
    args Kind
    res = String
    "((as " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fld String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    res String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            -- Similarly, we fully qualify the accessors with their types to work around type checking issues
            -- Unfortunately, z3 and CVC4 are behaving differently, so we tie this ascription to a solver capability.
            dtAccessor :: String -> [Kind] -> Kind -> String
    dtAccessor String
    fld [Kind]
    params Kind
    res
               | SolverCapabilities -> Bool
    supportsDirectAccessors SolverCapabilities
    caps = String
    dResult
               | Bool
    True                         = String
    aResult
              where dResult :: String
    dResult = String
    "(_ is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fld String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                    ps :: String
    ps      = String
    " (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Kind -> String) -> [Kind] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Kind -> String
    smtType [Kind]
    params) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") "
                    aResult :: String
    aResult = String
    "(_ is (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fld String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ps String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    res String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"

            sh :: SBVExpr -> String
    sh (SBVApp Op
    Ite [SV
    a, SV
    b, SV
    c]) = String
    "(ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (LkUp (Int
    t, Kind
    aKnd, Kind
    _, Int
    l) SV
    i SV
    e) [])
              | Bool
    needsCheck = String
    "(ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cond String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    lkUp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
              | Bool
    True       = String
    lkUp
              where needsCheck :: Bool
    needsCheck = case Kind
    aKnd of
                                  Kind
    KBool         -> (Integer
    2::Integer) Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    l
                                  KBounded Bool
    _ Int
    n  -> (Integer
    2::Integer)Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    l
                                  Kind
    KUnbounded    -> Bool
    True
                                  Kind
    KReal         -> String -> Bool
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index"
                                  Kind
    KFloat        -> String -> Bool
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected float valued index"
                                  Kind
    KDouble       -> String -> Bool
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index"
                                  KFP{}         -> String -> Bool
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected arbitrary float valued index"
                                  KRational{}   -> String -> Bool
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected rational valued index"
                                  Kind
    KChar         -> String -> Bool
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected char valued index"
                                  Kind
    KString       -> String -> Bool
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                  KList Kind
    k       -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected list valued: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                  KSet  Kind
    k       -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected set valued: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                  KTuple [Kind]
    k      -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected tuple valued: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> String
    forall a. Show a => a -> String
    show [Kind]
    k
                                  KMaybe Kind
    k      -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected maybe valued: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                  KEither Kind
    k1 Kind
    k2 -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected sum valued: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    k1, Kind
    k2)
                                  KUserSort String
    s Maybe [String]
    _ -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

                    lkUp :: String
    lkUp = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ TableMap -> Int -> String
    getTable TableMap
    tableMap Int
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

                    cond :: String
    cond
                     | SV -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SV
    i = String
    "(or " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    le0 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    gtl String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") "
                     | Bool
    True      = String
    gtl String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " "

                    (String
    less, String
    leq) = case Kind
    aKnd of
                                    Kind
    KBool         -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index"
                                    KBounded{}    -> if SV -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SV
    i then (String
    "bvslt", String
    "bvsle") else (String
    "bvult", String
    "bvule")
                                    Kind
    KUnbounded    -> (String
    "<", String
    "<=")
                                    Kind
    KReal         -> (String
    "<", String
    "<=")
                                    Kind
    KFloat        -> (String
    "fp.lt", String
    "fp.leq")
                                    Kind
    KDouble       -> (String
    "fp.lt", String
    "fp.leq")
                                    Kind
    KRational     -> (String
    "sbv.rat.lt", String
    "sbv.rat.leq")
                                    KFP{}         -> (String
    "fp.lt", String
    "fp.leq")
                                    Kind
    KChar         -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                    Kind
    KString       -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error String
    "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                    KList Kind
    k       -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected sequence valued index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                    KSet  Kind
    k       -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected set valued index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                    KTuple [Kind]
    k      -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected tuple valued index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> String
    forall a. Show a => a -> String
    show [Kind]
    k
                                    KMaybe Kind
    k      -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected maybe valued index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                    KEither Kind
    k1 Kind
    k2 -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected sum valued index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    k1, Kind
    k2)
                                    KUserSort String
    s Maybe [String]
    _ -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

                    mkCnst :: Int -> String
    mkCnst = RoundingMode -> CV -> String
    cvtCV RoundingMode
    rm (CV -> String) -> (Int -> CV) -> Int -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> Int -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    i)
                    le0 :: String
    le0  = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    less String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkCnst Int
    0 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                    gtl :: String
    gtl  = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    leq  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkCnst Int
    l String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (KindCast Kind
    f Kind
    t) [SV
    a]) = Bool -> Kind -> Kind -> String -> String
    handleKindCast Bool
    hasInt2bv Kind
    f Kind
    t (SV -> String
    cvtSV SV
    a)

            sh (SBVApp (ArrEq ArrayIndex
    i ArrayIndex
    j) [])  = String
    "(= array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    j String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++String
    ")"
            sh (SBVApp (ArrRead ArrayIndex
    i) [SV
    a]) = String
    "(select array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ArrayIndex -> String
    forall a. Show a => a -> String
    show ArrayIndex
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (Uninterpreted String
    nm) [])   = String
    nm
            sh (SBVApp (Uninterpreted String
    nm) [SV]
    args) = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (QuantifiedBool String
    i) [])   = String
    i
            sh (SBVApp (QuantifiedBool String
    i) [SV]
    args) = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected arguments to quantified boolean: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, [SV]) -> String
    forall a. Show a => a -> String
    show (String
    i, [SV]
    args)

            sh a :: SBVExpr
    a@(SBVApp (SpecialRelOp Kind
    k SpecialRelOp
    o) [SV]
    args)
              | Bool -> Bool
    not ([SV] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    args)
              = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp: unexpected arguments to special op: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVExpr -> String
    forall a. Show a => a -> String
    show SBVExpr
    a
              | Bool
    True
              = let order :: Int
    order = case SpecialRelOp
    o SpecialRelOp -> [SpecialRelOp] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    `elemIndex` [SpecialRelOp]
    specialRels of
                              Just Int
    i -> Int
    i
                              Maybe Int
    Nothing -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "SBV.SMT.SMTLib2.cvtExp: Cannot find " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SpecialRelOp -> String
    forall a. Show a => a -> String
    show SpecialRelOp
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " in the special-relations list."
                                                         , String
    "Known relations: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((SpecialRelOp -> String) -> [SpecialRelOp] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SpecialRelOp -> String
    forall a. Show a => a -> String
    show [SpecialRelOp]
    specialRels)
                                                         ]
                    asrt :: String -> String -> String
    asrt String
    nm String
    fun = String -> (String, String) -> Kind -> String
    mkRelEq String
    nm (String
    fun, Int -> String
    forall a. Show a => a -> String
    show Int
    order) Kind
    k
                in case SpecialRelOp
    o of
                     IsPartialOrder         String
    nm -> String -> String -> String
    asrt String
    nm String
    "partial-order"
                     IsLinearOrder          String
    nm -> String -> String -> String
    asrt String
    nm String
    "linear-order"
                     IsTreeOrder            String
    nm -> String -> String -> String
    asrt String
    nm String
    "tree-order"
                     IsPiecewiseLinearOrder String
    nm -> String -> String -> String
    asrt String
    nm String
    "piecewise-linear-order"

            sh (SBVApp (Extract Int
    i Int
    j) [SV
    a]) | Bool
    ensureBV = String
    "((_ extract " 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
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    j String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (Rol Int
    i) [SV
    a])
               | Bool
    bvOp  = String -> Int -> SV -> String
    rot String
    "rotate_left"  Int
    i SV
    a
               | Bool
    True  = String
    forall {a}. a
    bad

            sh (SBVApp (Ror Int
    i) [SV
    a])
               | Bool
    bvOp  = String -> Int -> SV -> String
    rot  String
    "rotate_right" Int
    i SV
    a
               | Bool
    True  = String
    forall {a}. a
    bad

            sh (SBVApp Op
    Shl [SV
    a, SV
    i])
               | Bool
    bvOp   = String -> String -> SV -> SV -> String
    shft String
    "bvshl"  String
    "bvshl" SV
    a SV
    i
               | Bool
    True   = String
    forall {a}. a
    bad

            sh (SBVApp Op
    Shr [SV
    a, SV
    i])
               | Bool
    bvOp  = String -> String -> SV -> SV -> String
    shft String
    "bvlshr" String
    "bvashr" SV
    a SV
    i
               | Bool
    True  = String
    forall {a}. a
    bad

            sh (SBVApp (ZeroExtend Int
    i) [SV
    a])
              | Bool
    bvOp = String
    "((_ zero_extend " 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
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
              | Bool
    True = String
    forall {a}. a
    bad

            sh (SBVApp (SignExtend Int
    i) [SV
    a])
              | Bool
    bvOp = String
    "((_ sign_extend " 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
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
              | Bool
    True = String
    forall {a}. a
    bad

            sh (SBVApp Op
    op [SV]
    args)
              | Just Bool -> [String] -> String
    f <- Op
    -> [(Op, Bool -> [String] -> String)]
    -> Maybe (Bool -> [String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, Bool -> [String] -> String)]
    forall {p}. [(Op, p -> [String] -> String)]
    smtBVOpTable, Bool
    ensureBVOrBool
              = Bool -> [String] -> String
    f ((SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    hasSign [SV]
    args) ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              where -- The first 4 operators below do make sense for Integer's in Haskell, but there's
                    -- no obvious counterpart for them in the SMTLib translation.
                    -- TODO: provide support for these.
                    smtBVOpTable :: [(Op, p -> [String] -> String)]
    smtBVOpTable = [ (Op
    And,  String -> String -> p -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2B String
    "and" String
    "bvand")
                                   , (Op
    Or,   String -> String -> p -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2B String
    "or"  String
    "bvor")
                                   , (Op
    XOr,  String -> String -> p -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2B String
    "xor" String
    "bvxor")
                                   , (Op
    Not,  String -> String -> p -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift1B String
    "not" String
    "bvnot")
                                   , (Op
    Join, String -> p -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2 String
    "concat")
                                   ]

            sh (SBVApp (Label String
    _) [SV
    a]) = SV -> String
    cvtSV SV
    a  -- This won't be reached; but just in case!

            sh (SBVApp (IEEEFP (FP_Cast Kind
    kFrom Kind
    kTo SV
    m)) [SV]
    args) = Kind -> Kind -> String -> String -> String
    handleFPCast Kind
    kFrom Kind
    kTo (SV -> String
    cvtSV SV
    m) ([String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args))
            sh (SBVApp (IEEEFP FPOp
    w                    ) [SV]
    args) = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FPOp -> String
    forall a. Show a => a -> String
    show FPOp
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (NonLinear NROp
    w) [SV]
    args) = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NROp -> String
    forall a. Show a => a -> String
    show NROp
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (PseudoBoolean PBOp
    pb) [SV]
    args)
              | Bool
    hasPB = PBOp -> [String] -> String
    handlePB PBOp
    pb [String]
    args'
              | Bool
    True  = PBOp -> [String] -> String
    reducePB PBOp
    pb [String]
    args'
              where args' :: [String]
    args' = (SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args

            -- NB: Z3 semantics have the predicates reversed: i.e., it returns true if overflow isn't possible. Hence the not.
            sh (SBVApp (OverflowOp OvOp
    op) [SV]
    args) = String
    "(not (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ OvOp -> String
    forall a. Show a => a -> String
    show OvOp
    op String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"

            -- Note the unfortunate reversal in StrInRe..
            sh (SBVApp (StrOp (StrInRe RegExp
    r)) [SV]
    args) = String
    "(str.in.re " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    regExpToSMTString RegExp
    r String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            -- StrUnit is no-op, since a character in SMTLib is the same as a string
            sh (SBVApp (StrOp StrOp
    StrUnit)     [SV
    a])  = SV -> String
    cvtSV SV
    a
            sh (SBVApp (StrOp StrOp
    op)          [SV]
    args) = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ StrOp -> String
    forall a. Show a => a -> String
    show StrOp
    op String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (RegExOp o :: RegExOp
    o@RegExEq{})  []) = RegExOp -> String
    forall a. Show a => a -> String
    show RegExOp
    o
            sh (SBVApp (RegExOp o :: RegExOp
    o@RegExNEq{}) []) = RegExOp -> String
    forall a. Show a => a -> String
    show RegExOp
    o

            -- Reverse is special, since we need to generate call to the internally generated function
            sh inp :: SBVExpr
    inp@(SBVApp op :: Op
    op@(SeqOp SBVReverse{}) [SV]
    args) = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ops String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
              where ops :: String
    ops = case Op
    op Op -> Map Op String -> Maybe String
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` Map Op String
    functionMap of
                            Just String
    s  -> String
    s
                            Maybe String
    Nothing -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVExpr -> String
    forall a. Show a => a -> String
    show SBVExpr
    inp

            sh (SBVApp (SeqOp SeqOp
    op) [SV]
    args) = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SeqOp -> String
    forall a. Show a => a -> String
    show SeqOp
    op String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (SetOp SetOp
    SetEqual)      [SV]
    args)   = String
    "(= "      String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (SetOp SetOp
    SetMember)     [SV
    e, SV
    s]) = String
    "(select " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (SetOp SetOp
    SetInsert)     [SV
    e, SV
    s]) = String
    "(store "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " true)"
            sh (SBVApp (SetOp SetOp
    SetDelete)     [SV
    e, SV
    s]) = String
    "(store "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " false)"
            sh (SBVApp (SetOp SetOp
    SetIntersect)  [SV]
    args)   = String
    "(intersection " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (SetOp SetOp
    SetUnion)      [SV]
    args)   = String
    "(union "        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (SetOp SetOp
    SetSubset)     [SV]
    args)   = String
    "(subset "       String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (SetOp SetOp
    SetDifference) [SV]
    args)   = String
    "(setminus "     String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (SetOp SetOp
    SetComplement) [SV]
    args)   = String
    "(complement "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (SetOp SetOp
    SetHasSize)    [SV]
    args)   = String
    "(set-has-size " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (TupleConstructor Int
    0)   [])    = String
    "mkSBVTuple0"
            sh (SBVApp (TupleConstructor Int
    n)   [SV]
    args)  = String
    "((as mkSBVTuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType ([Kind] -> Kind
    KTuple ((SV -> Kind) -> [SV] -> [Kind]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf [SV]
    args)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (TupleAccess      Int
    i Int
    n) [SV
    tup]) = String
    "(proj_" 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
    "_SBVTuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    tup String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (EitherConstructor Kind
    k1 Kind
    k2 Bool
    False) [SV
    arg]) =       String -> [SV] -> Kind -> String
    dtConstructor String
    "left_SBVEither"  [SV
    arg] (Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2)
            sh (SBVApp (EitherConstructor Kind
    k1 Kind
    k2 Bool
    True ) [SV
    arg]) =       String -> [SV] -> Kind -> String
    dtConstructor String
    "right_SBVEither" [SV
    arg] (Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2)
            sh (SBVApp (EitherIs          Kind
    k1 Kind
    k2 Bool
    False) [SV
    arg]) = Char
    '(' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> [Kind] -> Kind -> String
    dtAccessor    String
    "left_SBVEither"  [Kind
    k1]  (Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    arg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (EitherIs          Kind
    k1 Kind
    k2 Bool
    True ) [SV
    arg]) = Char
    '(' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> [Kind] -> Kind -> String
    dtAccessor    String
    "right_SBVEither" [Kind
    k2]  (Kind -> Kind -> Kind
    KEither Kind
    k1 Kind
    k2) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    arg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (EitherAccess            Bool
    False) [SV
    arg]) = String
    "(get_left_SBVEither "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    arg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (EitherAccess            Bool
    True ) [SV
    arg]) = String
    "(get_right_SBVEither " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    arg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp  Op
    RationalConstructor    [SV
    t, SV
    b]) = String
    "(SBV.Rational " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp (MaybeConstructor Kind
    k Bool
    False) [])    =       String -> [SV] -> Kind -> String
    dtConstructor String
    "nothing_SBVMaybe" []    (Kind -> Kind
    KMaybe Kind
    k)
            sh (SBVApp (MaybeConstructor Kind
    k Bool
    True)  [SV
    arg]) =       String -> [SV] -> Kind -> String
    dtConstructor String
    "just_SBVMaybe"    [SV
    arg] (Kind -> Kind
    KMaybe Kind
    k)
            sh (SBVApp (MaybeIs          Kind
    k Bool
    False) [SV
    arg]) = Char
    '(' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> [Kind] -> Kind -> String
    dtAccessor    String
    "nothing_SBVMaybe" []    (Kind -> Kind
    KMaybe Kind
    k) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    arg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp (MaybeIs          Kind
    k Bool
    True ) [SV
    arg]) = Char
    '(' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String -> [Kind] -> Kind -> String
    dtAccessor    String
    "just_SBVMaybe"    [Kind
    k]   (Kind -> Kind
    KMaybe Kind
    k) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    arg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (SBVApp Op
    MaybeAccess                [SV
    arg]) = String
    "(get_just_SBVMaybe " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    arg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh (SBVApp Op
    Implies [SV
    a, SV
    b]) = String
    "(=> " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            sh inp :: SBVExpr
    inp@(SBVApp Op
    op [SV]
    args)
              | Bool
    intOp, Just Bool -> [String] -> String
    f <- Op
    -> [(Op, Bool -> [String] -> String)]
    -> Maybe (Bool -> [String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, Bool -> [String] -> String)]
    smtOpIntTable
              = Bool -> [String] -> String
    f Bool
    True ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Bool
    boolOp, Just [String] -> String
    f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, [String] -> String)]
    boolComps
              = [String] -> String
    f ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Bool
    bvOp, Just Bool -> [String] -> String
    f <- Op
    -> [(Op, Bool -> [String] -> String)]
    -> Maybe (Bool -> [String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, Bool -> [String] -> String)]
    smtOpBVTable
              = Bool -> [String] -> String
    f ((SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    hasSign [SV]
    args) ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Bool
    realOp, Just Bool -> [String] -> String
    f <- Op
    -> [(Op, Bool -> [String] -> String)]
    -> Maybe (Bool -> [String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, Bool -> [String] -> String)]
    smtOpRealTable
              = Bool -> [String] -> String
    f ((SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    hasSign [SV]
    args) ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Bool
    ratOp, Just [String] -> String
    f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, [String] -> String)]
    ratOpTable
              = [String] -> String
    f ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Bool
    fpOp, Just Bool -> [String] -> String
    f <- Op
    -> [(Op, Bool -> [String] -> String)]
    -> Maybe (Bool -> [String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, Bool -> [String] -> String)]
    smtOpFloatDoubleTable
              = Bool -> [String] -> String
    f ((SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    hasSign [SV]
    args) ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Bool
    charOp Bool -> Bool -> Bool
    || Bool
    stringOp, Just [String] -> String
    f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, [String] -> String)]
    smtStringTable
              = [String] -> String
    f ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Bool
    listOp, Just [String] -> String
    f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, [String] -> String)]
    smtListTable
              = [String] -> String
    f ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Just [String] -> String
    f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Op
    op [(Op, [String] -> String)]
    uninterpretedTable
              = [String] -> String
    f ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    cvtSV [SV]
    args)
              | Bool
    True
              = if Bool -> Bool
    not ([SV] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    args) Bool -> Bool -> Bool
    && SV -> Bool
    forall a. HasKind a => a -> Bool
    isUserSort ([SV] -> SV
    forall a. HasCallStack => [a] -> a
    head [SV]
    args)
                then String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                     , String
    "*** Cannot translate operator        : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Op -> String
    forall a. Show a => a -> String
    show Op
    op
                                     , String
    "*** When applied to arguments of kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ([String] -> [String]
    forall a. Eq a => [a] -> [a]
    nub ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Kind -> String
    forall a. Show a => a -> String
    show (Kind -> String) -> (SV -> Kind) -> SV -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf) [SV]
    args))
                                     , String
    "*** Found as part of the expression  : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVExpr -> String
    forall a. Show a => a -> String
    show SBVExpr
    inp
                                     , String
    "***"
                                     , String
    "*** Note that uninterpreted kinds only support equality."
                                     , String
    "*** If you believe this is in error, please report!"
                                     ]
                else String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVExpr -> String
    forall a. Show a => a -> String
    show SBVExpr
    inp
              where smtOpBVTable :: [(Op, Bool -> [String] -> String)]
    smtOpBVTable  = [ (Op
    Plus,          String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2   String
    "bvadd")
                                    , (Op
    Minus,         String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2   String
    "bvsub")
                                    , (Op
    Times,         String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2   String
    "bvmul")
                                    , (Op
    UNeg,          String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift1B  String
    "not"    String
    "bvneg")
                                    , (Op
    Abs,           Bool -> [String] -> String
    liftAbs)
                                    , (Op
    Quot,          String -> String -> Bool -> [String] -> String
    lift2S  String
    "bvudiv" String
    "bvsdiv")
                                    , (Op
    Rem,           String -> String -> Bool -> [String] -> String
    lift2S  String
    "bvurem" String
    "bvsrem")
                                    , (Op
    Equal,         Bool -> [String] -> String
    forall {p}. p -> [String] -> String
    eqBV)
                                    , (Op
    NotEqual,      Bool -> [String] -> String
    forall {p}. p -> [String] -> String
    neqBV)
                                    , (Op
    LessThan,      String -> String -> Bool -> [String] -> String
    lift2S  String
    "bvult" String
    "bvslt")
                                    , (Op
    GreaterThan,   String -> String -> Bool -> [String] -> String
    lift2S  String
    "bvugt" String
    "bvsgt")
                                    , (Op
    LessEq,        String -> String -> Bool -> [String] -> String
    lift2S  String
    "bvule" String
    "bvsle")
                                    , (Op
    GreaterEq,     String -> String -> Bool -> [String] -> String
    lift2S  String
    "bvuge" String
    "bvsge")
                                    ]

                    -- Boolean comparisons.. SMTLib's bool type doesn't do comparisons, but Haskell does.. Sigh
                    boolComps :: [(Op, [String] -> String)]
    boolComps      = [ (Op
    LessThan,      [String] -> String
    blt)
                                     , (Op
    GreaterThan,   [String] -> String
    blt ([String] -> String)
    -> ([String] -> [String]) -> [String] -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [String]
    forall {a}. Show a => [a] -> [a]
    swp)
                                     , (Op
    LessEq,        [String] -> String
    blq)
                                     , (Op
    GreaterEq,     [String] -> String
    blq ([String] -> String)
    -> ([String] -> [String]) -> [String] -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [String]
    forall {a}. Show a => [a] -> [a]
    swp)
                                     ]
                                   where blt :: [String] -> String
    blt [String
    x, String
    y] = String
    "(and (not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                         blt [String]
    xs     = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.boolComps.blt: Impossible happened, incorrect arity (expected 2): " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    forall a. Show a => a -> String
    show [String]
    xs
                                         blq :: [String] -> String
    blq [String
    x, String
    y] = String
    "(or (not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                         blq [String]
    xs     = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.boolComps.blq: Impossible happened, incorrect arity (expected 2): " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    forall a. Show a => a -> String
    show [String]
    xs
                                         swp :: [a] -> [a]
    swp [a
    x, a
    y] = [a
    y, a
    x]
                                         swp [a]
    xs     = String -> [a]
    forall a. HasCallStack => String -> a
    error (String -> [a]) -> String -> [a]
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMT.SMTLib2.boolComps.swp: Impossible happened, incorrect arity (expected 2): " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [a] -> String
    forall a. Show a => a -> String
    show [a]
    xs

                    smtOpRealTable :: [(Op, Bool -> [String] -> String)]
    smtOpRealTable =  [(Op, Bool -> [String] -> String)]
    smtIntRealShared
                                   [(Op, Bool -> [String] -> String)]
    -> [(Op, Bool -> [String] -> String)]
    -> [(Op, Bool -> [String] -> String)]
    forall a. [a] -> [a] -> [a]
    ++ [ (Op
    Quot,        String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2WM String
    "/" String
    "fp.div")
                                      ]

                    smtOpIntTable :: [(Op, Bool -> [String] -> String)]
    smtOpIntTable  = [(Op, Bool -> [String] -> String)]
    smtIntRealShared
                                   [(Op, Bool -> [String] -> String)]
    -> [(Op, Bool -> [String] -> String)]
    -> [(Op, Bool -> [String] -> String)]
    forall a. [a] -> [a] -> [a]
    ++ [ (Op
    Quot,        String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2   String
    "div")
                                      , (Op
    Rem,         String -> Bool -> [String] -> String
    forall {p}. String -> p -> [String] -> String
    lift2   String
    "mod")
                                      ]

                    smtOpFloatDoubleTable :: [(Op, Bool -> [String] -> String)]
    smtOpFloatDoubleTable = [(Op, Bool -> [String] -> String)]
    smtIntRealShared
                                      [(Op, Bool -> [String] -> String)]
    -> [(Op, Bool -> [String] -> String)]
    -> [(Op, Bool -> [String] -> String)]
    forall a. [a] -> [a] -> [a]
    ++ [(Op
    Quot, String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2WM String
    "/" String
    "fp.div")]

                    smtIntRealShared :: [(Op, Bool -> [String] -> String)]
    smtIntRealShared  = [ (Op
    Plus,          String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2WM String
    "+" String
    "fp.add")
                                        , (Op
    Minus,         String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2WM String
    "-" String
    "fp.sub")
                                        , (Op
    Times,         String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2WM String
    "*" String
    "fp.mul")
                                        , (Op
    UNeg,          String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift1FP String
    "-" String
    "fp.neg")
                                        , (Op
    Abs,           Bool -> [String] -> String
    liftAbs)
                                        , (Op
    Equal,         Bool -> [String] -> String
    forall {p}. p -> [String] -> String
    equal)
                                        , (Op
    NotEqual,      Bool -> [String] -> String
    forall {p}. p -> [String] -> String
    notEqual)
                                        , (Op
    LessThan,      String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2Cmp  String
    "<"  String
    "fp.lt")
                                        , (Op
    GreaterThan,   String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2Cmp  String
    ">"  String
    "fp.gt")
                                        , (Op
    LessEq,        String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2Cmp  String
    "<=" String
    "fp.leq")
                                        , (Op
    GreaterEq,     String -> String -> Bool -> [String] -> String
    forall {p}. String -> String -> p -> [String] -> String
    lift2Cmp  String
    ">=" String
    "fp.geq")
                                        ]

                    ratOpTable :: [(Op, [String] -> String)]
    ratOpTable = [ (Op
    Plus,        String -> [String] -> String
    lift2Rat String
    "sbv.rat.plus")
                                 , (Op
    Minus,       String -> [String] -> String
    lift2Rat String
    "sbv.rat.minus")
                                 , (Op
    Times,       String -> [String] -> String
    lift2Rat String
    "sbv.rat.times")
                                 , (Op
    UNeg,        String -> [String] -> String
    liftRat  String
    "sbv.rat.uneg")
                                 , (Op
    Abs,         String -> [String] -> String
    liftRat  String
    "sbv.rat.abs")
                                 , (Op
    Equal,       String -> [String] -> String
    lift2Rat String
    "sbv.rat.eq")
                                 , (Op
    NotEqual,    String -> [String] -> String
    lift2Rat String
    "sbv.rat.notEq")
                                 , (Op
    LessThan,    String -> [String] -> String
    lift2Rat String
    "sbv.rat.lt")
                                 , (Op
    GreaterThan, String -> [String] -> String
    lift2Rat String
    "sbv.rat.lt" ([String] -> String)
    -> ([String] -> [String]) -> [String] -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [String]
    forall {a}. Show a => [a] -> [a]
    swap)
                                 , (Op
    LessEq,      String -> [String] -> String
    lift2Rat String
    "sbv.rat.leq")
                                 , (Op
    GreaterEq,   String -> [String] -> String
    lift2Rat String
    "sbv.rat.leq" ([String] -> String)
    -> ([String] -> [String]) -> [String] -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [String]
    forall {a}. Show a => [a] -> [a]
    swap)
                                 ]
                            where lift2Rat :: String -> [String] -> String
    lift2Rat String
    o [String
    x, String
    y] = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                  lift2Rat String
    o [String]
    sbvs   = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2.sh.lift2Rat: Unexpected arguments: "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, [String]) -> String
    forall a. Show a => a -> String
    show (String
    o, [String]
    sbvs)
                                  liftRat :: String -> [String] -> String
    liftRat  String
    o [String
    x]    = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                  liftRat  String
    o [String]
    sbvs   = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2.sh.lift2Rat: Unexpected arguments: "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String, [String]) -> String
    forall a. Show a => a -> String
    show (String
    o, [String]
    sbvs)
                                  swap :: [a] -> [a]
    swap [a
    x, a
    y]       = [a
    y, a
    x]
                                  swap [a]
    sbvs         = String -> [a]
    forall a. HasCallStack => String -> a
    error (String -> [a]) -> String -> [a]
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2.sh.swap: Unexpected arguments: "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [a] -> String
    forall a. Show a => a -> String
    show [a]
    sbvs

                    -- equality and comparisons are the only thing that works on uninterpreted sorts and pretty much everything else
                    uninterpretedTable :: [(Op, [String] -> String)]
    uninterpretedTable = [ (Op
    Equal,       String -> String -> Bool -> [String] -> String
    lift2S String
    "="        String
    "="        Bool
    True)
                                         , (Op
    NotEqual,    String -> String -> Bool -> [String] -> String
    liftNS String
    "distinct" String
    "distinct" Bool
    True)
                                         , (Op
    LessThan,    String -> [String] -> String
    unintComp String
    "<")
                                         , (Op
    GreaterThan, String -> [String] -> String
    unintComp String
    ">")
                                         , (Op
    LessEq,      String -> [String] -> String
    unintComp String
    "<=")
                                         , (Op
    GreaterEq,   String -> [String] -> String
    unintComp String
    ">=")
                                         ]

                    -- For strings, equality and comparisons are the only operators
                    smtStringTable :: [(Op, [String] -> String)]
    smtStringTable = [ (Op
    Equal,       String -> String -> Bool -> [String] -> String
    lift2S String
    "="        String
    "="        Bool
    True)
                                     , (Op
    NotEqual,    String -> String -> Bool -> [String] -> String
    liftNS String
    "distinct" String
    "distinct" Bool
    True)
                                     , (Op
    LessThan,    Bool -> String -> [String] -> String
    stringCmp Bool
    False String
    "str.<")
                                     , (Op
    GreaterThan, Bool -> String -> [String] -> String
    stringCmp Bool
    True  String
    "str.<")
                                     , (Op
    LessEq,      Bool -> String -> [String] -> String
    stringCmp Bool
    False String
    "str.<=")
                                     , (Op
    GreaterEq,   Bool -> String -> [String] -> String
    stringCmp Bool
    True  String
    "str.<=")
                                     ]

                    -- For lists, equality is really the only operator
                    -- Likewise here, things might change for comparisons
                    smtListTable :: [(Op, [String] -> String)]
    smtListTable = [ (Op
    Equal,       String -> String -> Bool -> [String] -> String
    lift2S String
    "="        String
    "="        Bool
    True)
                                   , (Op
    NotEqual,    String -> String -> Bool -> [String] -> String
    liftNS String
    "distinct" String
    "distinct" Bool
    True)
                                   , (Op
    LessThan,    Bool -> String -> [String] -> String
    seqCmp Bool
    False String
    "seq.<")
                                   , (Op
    GreaterThan, Bool -> String -> [String] -> String
    seqCmp Bool
    True  String
    "seq.<")
                                   , (Op
    LessEq,      Bool -> String -> [String] -> String
    seqCmp Bool
    False String
    "seq.<=")
                                   , (Op
    GreaterEq,   Bool -> String -> [String] -> String
    seqCmp Bool
    True  String
    "seq.<=")
                                   ]

    declareFun :: SV -> SBVType -> Maybe String -> [String]
    declareFun :: SV -> SBVType -> Maybe String -> [String]
    declareFun = String -> SBVType -> Maybe String -> [String]
    declareName (String -> SBVType -> Maybe String -> [String])
    -> (SV -> String) -> SV -> SBVType -> Maybe String -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SV -> String
    forall a. Show a => a -> String
    show

    -- If we have a char, we have to make sure it's and SMTLib string of length exactly one
    -- If we have a rational, we have to make sure the denominator is > 0
    -- Otherwise, we just declare the name
    declareName :: String -> SBVType -> Maybe String -> [String]
    declareName :: String -> SBVType -> Maybe String -> [String]
    declareName String
    s t :: SBVType
    t@(SBVType [Kind]
    inputKS) Maybe String
    mbCmnt = String
    decl String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    restrict
      where decl :: String
    decl        = String
    "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVType -> String
    cvtType SBVType
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> (String -> String) -> Maybe String -> String
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe String
    "" (String
    " ; " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) Maybe String
    mbCmnt

            ([Kind]
    args, Kind
    result) = case [Kind]
    inputKS of
                              [] -> String -> ([Kind], Kind)
    forall a. HasCallStack => String -> a
    error (String -> ([Kind], Kind)) -> String -> ([Kind], Kind)
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.declareName: Unexpected empty type for: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    s
                              [Kind]
    _  -> ([Kind] -> [Kind]
    forall a. HasCallStack => [a] -> [a]
    init [Kind]
    inputKS, [Kind] -> Kind
    forall a. HasCallStack => [a] -> a
    last [Kind]
    inputKS)

            -- Does the kind KChar and KRational *not* occur in the kind anywhere?
            charRatFree :: Kind -> Bool
    charRatFree Kind
    k = [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([()] -> Bool) -> [()] -> Bool
    forall a b. (a -> b) -> a -> b
    $ [() | Kind
    KChar <- Kind -> [Kind]
    forall on. Uniplate on => on -> [on]
    G.universe Kind
    k] [()] -> [()] -> [()]
    forall a. [a] -> [a] -> [a]
    ++ [() | Kind
    KRational <- Kind -> [Kind]
    forall on. Uniplate on => on -> [on]
    G.universe Kind
    k]
            noCharOrRat :: Bool
    noCharOrRat   = Kind -> Bool
    charRatFree Kind
    result
            needsQuant :: Bool
    needsQuant    = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Kind] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Kind]
    args

            resultVar :: String
    resultVar | Bool
    needsQuant = String
    "result"
                      | Bool
    True       = String
    s

            argList :: [String]
    argList   = [String
    "a" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i | (Int
    i, Kind
    _) <- [Int] -> [Kind] -> [(Int, Kind)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    1::Int ..] [Kind]
    args]
            argTList :: [String]
    argTList  = [String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" | (String
    a, Kind
    k) <- [String] -> [Kind] -> [(String, Kind)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    argList [Kind]
    args]
            resultExp :: String
    resultExp = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    argList String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            restrict :: [String]
    restrict | Bool
    noCharOrRat = []
                     | Bool
    needsQuant  =    [               String
    "(assert (forall (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    argTList String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                        ,               String
    "                (let ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    resultVar String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    resultExp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
                                        ]
                                     [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (case [String]
    constraints of
                                           []     ->  [ String
    "                     true"]
                                           [String
    x]    ->  [ String
    "                     " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x]
                                           (String
    x:[String]
    xs) ->  ( String
    "                     (and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x)
                                                   String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  [ String
    "                          " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c | String
    c <- [String]
    xs]
                                                   [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "                     )"])
                                     [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [        String
    "                )))"]
                     | Bool
    True        = case [String]
    constraints of
                                      []     -> []
                                      [String
    x]    -> [String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"]
                                      (String
    x:[String]
    xs) -> ( String
    "(assert (and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x)
                                             String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  [ String
    "             " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c | String
    c <- [String]
    xs]
                                             [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "        ))"]

            constraints :: [String]
    constraints = Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
    walk Int
    0 String
    resultVar Kind -> String -> [String]
    cstr Kind
    result
              where cstr :: Kind -> String -> [String]
    cstr Kind
    KChar     String
    nm = [String
    "(= 1 (str.len " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"]
                    cstr Kind
    KRational String
    nm = [String
    "(< 0 (sbv.rat.denominator " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"]
                    cstr Kind
    _         String
    _  = []

            mkAnd :: [String] -> String
    mkAnd []  = String
    "true"
            mkAnd [String
    c] = String
    c
            mkAnd [String]
    cs  = String
    "(and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    cs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            walk :: Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
            walk :: Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
    walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KBool     {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KBounded  {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KUnbounded{}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KReal     {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KUserSort {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KFloat    {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KDouble   {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KRational {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KFP       {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KChar     {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk Int
    _d String
    nm Kind -> String -> [String]
    f k :: Kind
    k@KString   {}         = Kind -> String -> [String]
    f Kind
    k String
    nm
            walk  Int
    d String
    nm Kind -> String -> [String]
    f  (KList Kind
    k)
              | Kind -> Bool
    charRatFree Kind
    k                 = []
              | Bool
    True                          = let fnm :: String
    fnm   = String
    "seq" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    d
                                                    cstrs :: [String]
    cstrs = Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
    walk (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) (String
    "(seq.nth " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fnm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")") Kind -> String -> [String]
    f Kind
    k
                                                in [String
    "(forall ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fnm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    KUnbounded String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "(=> (and (>= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fnm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " 0) (< " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fnm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (seq.len " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    mkAnd [String]
    cstrs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"]
            walk  Int
    d  String
    nm Kind -> String -> [String]
    f (KSet Kind
    k)
              | Kind -> Bool
    charRatFree Kind
    k                 = []
              | Bool
    True                          = let fnm :: String
    fnm    = String
    "set" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    d
                                                    cstrs :: [String]
    cstrs  = Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
    walk (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) String
    nm (\Kind
    sk String
    snm -> [String
    "(=> (select " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    snm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fnm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" | String
    c <- Kind -> String -> [String]
    f Kind
    sk String
    fnm]) Kind
    k
                                                in [String
    "(forall ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fnm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    mkAnd [String]
    cstrs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"]
            walk  Int
    d  String
    nm  Kind -> String -> [String]
    f (KTuple [Kind]
    ks)        = let tt :: String
    tt        = String
    "SBVTuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([Kind] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    ks)
                                                    project :: a -> String
    project a
    i = String
    "(proj_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    tt String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                                    nmks :: [(String, Kind)]
    nmks      = [(Int -> String
    forall a. Show a => a -> String
    project Int
    i, Kind
    k) | (Int
    i, Kind
    k) <- [Int] -> [Kind] -> [(Int, Kind)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    1::Int ..] [Kind]
    ks]
                                                in ((String, Kind) -> [String]) -> [(String, Kind)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\(String
    n, Kind
    k) -> Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
    walk (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) String
    n Kind -> String -> [String]
    f Kind
    k) [(String, Kind)]
    nmks
            walk  Int
    d  String
    nm  Kind -> String -> [String]
    f km :: Kind
    km@(KMaybe Kind
    k)      = let n :: String
    n = String
    "(get_just_SBVMaybe " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                                in  [String
    "(=> " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "((_ is (just_SBVMaybe (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    km String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" | String
    c <- Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
    walk (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) String
    n Kind -> String -> [String]
    f Kind
    k]
            walk  Int
    d  String
    nm  Kind -> String -> [String]
    f ke :: Kind
    ke@(KEither Kind
    k1 Kind
    k2) = let n1 :: String
    n1 = String
    "(get_left_SBVEither "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                                    n2 :: String
    n2 = String
    "(get_right_SBVEither " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                                    c1 :: [String]
    c1 = [String
    "(=> " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "((_ is (left_SBVEither ("  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    ke String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" | String
    c <- Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
    walk (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) String
    n1 Kind -> String -> [String]
    f Kind
    k1]
                                                    c2 :: [String]
    c2 = [String
    "(=> " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "((_ is (right_SBVEither (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    ke String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")" | String
    c <- Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
    walk (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) String
    n2 Kind -> String -> [String]
    f Kind
    k2]
                                                in [String]
    c1 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    c2

    -----------------------------------------------------------------------------------------------
    -- Casts supported by SMTLib. (From: <http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml>)
    --   ; from another floating point sort
    --   ((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb))
    --
    --   ; from real
    --   ((_ to_fp eb sb) RoundingMode Real (_ FloatingPoint eb sb))
    --
    --   ; from signed machine integer, represented as a 2's complement bit vector
    --   ((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))
    --
    --   ; from unsigned machine integer, represented as bit vector
    --   ((_ to_fp_unsigned eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))
    --
    --   ; to unsigned machine integer, represented as a bit vector
    --   ((_ fp.to_ubv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))
    --
    --   ; to signed machine integer, represented as a 2's complement bit vector
    --   ((_ fp.to_sbv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))
    --
    --   ; to real
    --   (fp.to_real (_ FloatingPoint eb sb) Real)
    -----------------------------------------------------------------------------------------------

    handleFPCast :: Kind -> Kind -> String -> String -> String
    handleFPCast :: Kind -> Kind -> String -> String -> String
    handleFPCast Kind
    kFromIn Kind
    kToIn String
    rm String
    input
      | Kind
    kFrom Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    kTo
      = String
    input
      | Bool
    True
      = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> Kind -> String -> String
    cast Kind
    kFrom Kind
    kTo String
    input String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
      where addRM :: String -> String -> String
    addRM String
    a String
    s = String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a

            kFrom :: Kind
    kFrom = Kind -> Kind
    simplify Kind
    kFromIn
            kTo :: Kind
    kTo   = Kind -> Kind
    simplify Kind
    kToIn

            simplify :: Kind -> Kind
    simplify Kind
    KFloat  = Int -> Int -> Kind
    KFP   Int
    8 Int
    24
            simplify Kind
    KDouble = Int -> Int -> Kind
    KFP  Int
    11 Int
    53
            simplify Kind
    k       = Kind
    k

            size :: (a, a) -> String
    size (a
    eb, a
    sb) = a -> String
    forall a. Show a => a -> String
    show a
    eb String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    sb

            -- To go and back from Ints, we detour through reals
            cast :: Kind -> Kind -> String -> String
    cast Kind
    KUnbounded (KFP Int
    eb Int
    sb) String
    a = String
    "(_ to_fp " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int) -> String
    forall {a} {a}. (Show a, Show a) => (a, a) -> String
    size (Int
    eb, Int
    sb) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (to_real " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            cast KFP{}      Kind
    KUnbounded  String
    a = String
    "to_int (fp.to_real " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            -- To floats
            cast (KBounded Bool
    False Int
    _) (KFP Int
    eb Int
    sb) String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "(_ to_fp_unsigned " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int) -> String
    forall {a} {a}. (Show a, Show a) => (a, a) -> String
    size (Int
    eb, Int
    sb) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            cast (KBounded Bool
    True  Int
    _) (KFP Int
    eb Int
    sb) String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "(_ to_fp "          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int) -> String
    forall {a} {a}. (Show a, Show a) => (a, a) -> String
    size (Int
    eb, Int
    sb) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            cast Kind
    KReal              (KFP Int
    eb Int
    sb) String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "(_ to_fp "          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int) -> String
    forall {a} {a}. (Show a, Show a) => (a, a) -> String
    size (Int
    eb, Int
    sb) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            cast KFP{}              (KFP Int
    eb Int
    sb) String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "(_ to_fp "          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int) -> String
    forall {a} {a}. (Show a, Show a) => (a, a) -> String
    size (Int
    eb, Int
    sb) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            -- From float/double
            cast KFP{} (KBounded Bool
    False Int
    m) String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "(_ fp.to_ubv " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    m String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            cast KFP{} (KBounded Bool
    True  Int
    m) String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "(_ fp.to_sbv " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    m String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            -- To real
            cast KFP{} Kind
    KReal String
    a = String
    "fp.to_real" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a

            -- Nothing else should come up:
            cast Kind
    f  Kind
    d  String
    _ = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2: Unexpected FPCast from: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    d

    rot :: String -> Int -> SV -> String
    rot :: String -> Int -> SV -> String
    rot String
    o Int
    c SV
    x = String
    "((_ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    shft :: String -> String -> SV -> SV -> String
    shft :: String -> String -> SV -> SV -> String
    shft String
    oW String
    oS SV
    x SV
    c = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    cvtSV SV
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
       where o :: String
    o = if SV -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SV
    x then String
    oS else String
    oW

    -- Various casts
    handleKindCast :: Bool -> Kind -> Kind -> String -> String
    handleKindCast :: Bool -> Kind -> Kind -> String -> String
    handleKindCast Bool
    hasInt2bv Kind
    kFrom Kind
    kTo String
    a
      | Kind
    kFrom Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    kTo
      = String
    a
      | Bool
    True
      = case Kind
    kFrom of
          KBounded Bool
    s Int
    m -> case Kind
    kTo of
                            KBounded Bool
    _ Int
    n -> (Int -> String) -> Int -> Int -> String
    forall {a}.
    (Ord a, Num a, Show a) =>
    (a -> String) -> a -> a -> String
    fromBV (if Bool
    s then Int -> String
    forall a. Show a => a -> String
    signExtend else Int -> String
    forall a. Show a => a -> String
    zeroExtend) Int
    m Int
    n
                            Kind
    KUnbounded   -> Bool -> Int -> String
    forall {b}. (Integral b, Show b) => Bool -> b -> String
    b2i Bool
    s Int
    m
                            Kind
    _            -> String
    tryFPCast

          Kind
    KUnbounded   -> case Kind
    kTo of
                            Kind
    KReal        -> String
    "(to_real " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                            KBounded Bool
    _ Int
    n -> Int -> String
    i2b Int
    n
                            Kind
    _            -> String
    tryFPCast

          Kind
    KReal        -> case Kind
    kTo of
                            Kind
    KUnbounded   -> String
    "(to_int " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                            Kind
    _            -> String
    tryFPCast

          Kind
    _            -> String
    tryFPCast

      where -- See if we can push this down to a float-cast, using sRNE. This happens if one of the kinds is a float/double.
            -- Otherwise complain
            tryFPCast :: String
    tryFPCast
              | (Kind -> Bool) -> [Kind] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (\Kind
    k -> Kind -> Bool
    forall a. HasKind a => a -> Bool
    isFloat Kind
    k Bool -> Bool -> Bool
    || Kind -> Bool
    forall a. HasKind a => a -> Bool
    isDouble Kind
    k) [Kind
    kFrom, Kind
    kTo]
              = Kind -> Kind -> String -> String -> String
    handleFPCast Kind
    kFrom Kind
    kTo (RoundingMode -> String
    smtRoundingMode RoundingMode
    RoundNearestTiesToEven) String
    a
              | Bool
    True
              = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.SMTLib2: Unexpected cast from: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    kFrom String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    kTo

            fromBV :: (a -> String) -> a -> a -> String
    fromBV a -> String
    upConv a
    m a
    n
             | a
    n a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    > a
    m  = a -> String
    upConv  (a
    n a -> a -> a
    forall a. Num a => a -> a -> a
    - a
    m)
             | a
    m a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    n = String
    a
             | Bool
    True   = a -> String
    forall a. Show a => a -> String
    extract (a
    n a -> a -> a
    forall a. Num a => a -> a -> a
    - a
    1)

            b2i :: Bool -> b -> String
    b2i Bool
    False b
    _ = String
    "(bv2nat " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            b2i Bool
    True  b
    1 = String
    "(ite (= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " #b0) 0 (- 1))"
            b2i Bool
    True  b
    m = String
    "(ite (= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    msb String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " #b0" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ifPos String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ifNeg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
              where offset :: Integer
                    offset :: Integer
    offset = Integer
    2Integer -> b -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(b
    mb -> b -> b
    forall a. Num a => a -> a -> a
    -b
    1)
                    rest :: String
    rest   = b -> String
    forall a. Show a => a -> String
    extract (b
    m b -> b -> b
    forall a. Num a => a -> a -> a
    - b
    2)

                    msb :: String
    msb    = let top :: String
    top = b -> String
    forall a. Show a => a -> String
    show (b
    mb -> b -> b
    forall a. Num a => a -> a -> a
    -b
    1) in String
    "((_ extract " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    top String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    top String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                    ifPos :: String
    ifPos  = String
    "(bv2nat " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rest String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++String
    ")"
                    ifNeg :: String
    ifNeg  = String
    "(- " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ifPos String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    offset String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            signExtend :: a -> String
    signExtend a
    i = String
    "((_ sign_extend " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  String
    ") "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            zeroExtend :: a -> String
    zeroExtend a
    i = String
    "((_ zero_extend " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  String
    ") "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            extract :: a -> String
    extract    a
    i = String
    "((_ extract "     String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " 0) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

            -- Some solvers support int2bv, but not all. So, we use a capability to determine.
            --
            -- NB. The "manual" implementation works regardless n < 0 or not, because the first thing we
            -- do is to compute "reduced" to bring it down to the correct range. It also works
            -- regardless were mapping to signed or unsigned bit-vector; because the representation
            -- is the same.
            i2b :: Int -> String
    i2b Int
    n
              | Bool
    hasInt2bv
              = String
    "((_ int2bv " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
              | Bool
    True
              = String
    "(let (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    reduced String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") (let (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    defs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    body String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
              where b :: Int -> String
    b Int
    i      = Integer -> String
    forall a. Show a => a -> String
    show (Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    i :: Integer)
                    reduced :: String
    reduced  = String
    "(__a (mod " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    b Int
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
                    mkBit :: Int -> String
    mkBit Int
    0  = String
    "(__a0 (ite (= (mod __a 2) 0) #b0 #b1))"
                    mkBit Int
    i  = String
    "(__a" 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
    " (ite (= (mod (div __a " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    b Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") 2) 0) #b0 #b1))"
                    defs :: String
    defs     = [String] -> String
    unwords ((Int -> String) -> [Int] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> String
    mkBit [Int
    0 .. Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1])
                    body :: String
    body     = (String -> String -> String) -> [String] -> String
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 (\String
    c String
    r -> String
    "(concat " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    r String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")") [String
    "__a" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i | Int
    i <- [Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1, Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    2 .. Int
    0]]

    -- Translation of pseudo-booleans, in case the solver supports them
    handlePB :: PBOp -> [String] -> String
    handlePB :: PBOp -> [String] -> String
    handlePB (PB_AtMost  Int
    k) [String]
    args = String
    "((_ at-most "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    k                                             String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    handlePB (PB_AtLeast Int
    k) [String]
    args = String
    "((_ at-least " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    k                                             String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    handlePB (PB_Exactly Int
    k) [String]
    args = String
    "((_ pbeq "     String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Int -> String) -> [Int] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> String
    forall a. Show a => a -> String
    show (Int
    k Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : Int -> Int -> [Int]
    forall a. Int -> a -> [a]
    replicate ([String] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [String]
    args) Int
    1)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    handlePB (PB_Eq [Int]
    cs   Int
    k) [String]
    args = String
    "((_ pbeq "     String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Int -> String) -> [Int] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> String
    forall a. Show a => a -> String
    show (Int
    k Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [Int]
    cs))                        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    handlePB (PB_Le [Int]
    cs   Int
    k) [String]
    args = String
    "((_ pble "     String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Int -> String) -> [Int] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> String
    forall a. Show a => a -> String
    show (Int
    k Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [Int]
    cs))                        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    handlePB (PB_Ge [Int]
    cs   Int
    k) [String]
    args = String
    "((_ pbge "     String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Int -> String) -> [Int] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> String
    forall a. Show a => a -> String
    show (Int
    k Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [Int]
    cs))                        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    -- Translation of pseudo-booleans, in case the solver does *not* support them
    reducePB :: PBOp -> [String] -> String
    reducePB :: PBOp -> [String] -> String
    reducePB PBOp
    op [String]
    args = case PBOp
    op of
                         PB_AtMost  Int
    k -> String
    "(<= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> String
    addIf (Int -> [Int]
    forall a. a -> [a]
    repeat Int
    1) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                         PB_AtLeast Int
    k -> String
    "(>= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> String
    addIf (Int -> [Int]
    forall a. a -> [a]
    repeat Int
    1) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                         PB_Exactly Int
    k -> String
    "(=  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> String
    addIf (Int -> [Int]
    forall a. a -> [a]
    repeat Int
    1) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                         PB_Le [Int]
    cs   Int
    k -> String
    "(<= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> String
    addIf [Int]
    cs         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                         PB_Ge [Int]
    cs   Int
    k -> String
    "(>= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> String
    addIf [Int]
    cs         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                         PB_Eq [Int]
    cs   Int
    k -> String
    "(=  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Int] -> String
    addIf [Int]
    cs         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

      where addIf :: [Int] -> String
            addIf :: [Int] -> String
    addIf [Int]
    cs = String
    "(+ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String
    "(ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " 0)" | (String
    a, Int
    c) <- [String] -> [Int] -> [(String, Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    args [Int]
    cs] String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"