    -----------------------------------------------------------------------------
    -- |
    -- 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 PatternGuards #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

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

    import Data.Bits  (bit)
    import Data.List  (intercalate, partition, nub, sort)
    import Data.Maybe (listToMaybe, fromMaybe, 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.Symbolic (QueryContext(..), SetOp(..))
    import Data.SBV.Core.Kind (smtType, needsFlattening)
    import Data.SBV.SMT.Utils
    import Data.SBV.Control.Types

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

    tbd :: String -> a
    tbd :: String -> a
    tbd e :: String
    e = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "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 ctx :: QueryContext
    ctx kindInfo :: Set Kind
    kindInfo isSat :: Bool
    isSat comments :: [String]
    comments (inputs :: [(Quantifier, NamedSymVar)]
    inputs, trackerVars :: [NamedSymVar]
    trackerVars) skolemInps :: [Either SV (SV, [SV])]
    skolemInps consts :: [(SV, CV)]
    consts tbls :: [((Int, Kind, Kind), [SV])]
    tbls arrs :: [(Int, ArrayInfo)]
    arrs uis :: [(String, SBVType)]
    uis axs :: [(String, [String])]
    axs (SBVPgm asgnsSeq :: Seq (SV, SBVExpr)
    asgnsSeq) cstrs :: Seq (Bool, [(String, String)], SV)
    cstrs out :: SV
    out cfg :: 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
            hasFloat :: Bool
    hasFloat       = Kind
    KFloat     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
            hasChar :: Bool
    hasChar        = Kind
    KChar      Kind -> Set Kind -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Kind
    kindInfo
            hasDouble :: Bool
    hasDouble      = Kind
    KDouble    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 (t :: * -> *) a. Foldable t => t a -> Bool
    null [String
    s | (s :: String
    s, _) <- [(String, Either String [String])]
    usorts, String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == "RoundingMode"]
            hasBVs :: Bool
    hasBVs         = Bool
    hasChar Bool -> Bool -> Bool
    || Bool -> Bool
    not ([()] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [() | KBounded{} <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    kindInfo])   -- Remember, characters map to Word8
            usorts :: [(String, Either String [String])]
    usorts         = [(String
    s, Either String [String]
    dt) | KUninterpreted s :: String
    s dt :: Either String [String]
    dt <- Set Kind -> [Kind]
    forall a. Set a -> [a]
    Set.toList Set Kind
    kindInfo]
            trueUSorts :: [String]
    trueUSorts     = [String
    s | (s :: String
    s, _) <- [(String, Either String [String])]
    usorts, String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    /= "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 (t :: * -> *) a. Foldable t => t a -> Bool
    null) [() | (_, (_, (k1 :: Kind
    k1, k2 :: Kind
    k2), _)) <- [(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 (t :: * -> *) a. Foldable t => t a -> Bool
    null) [() | (_, (_, _, ArrayFree (Just _))) <- [(Int, ArrayInfo)]
    arrs]
            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 (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
            rm :: RoundingMode
    rm             = SMTConfig -> RoundingMode
    roundingMode SMTConfig
    cfg
            solverCaps :: SolverCapabilities
    solverCaps     = SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)

            -- 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 | (w :: String
    w, have :: Bool
    have, need :: Bool
    need) <- [(String, Bool, Bool)]
    checks, Bool
    need Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    have]
               where checks :: [(String, Bool, Bool)]
    checks = [ ("data types",     SolverCapabilities -> Bool
    supportsDataTypes SolverCapabilities
    solverCaps, Bool
    hasTuples Bool -> Bool -> Bool
    || Bool
    hasEither Bool -> Bool -> Bool
    || Bool
    hasMaybe)
                              , ("set operations", SolverCapabilities -> Bool
    supportsSets      SolverCapabilities
    solverCaps, Bool
    hasSets)
                              ]

                     nope :: String -> [String]
    nope w :: String
    w = [ "***     Given problem requires support for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w
                              , "***     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]
    ++ ") doesn't support this feature."
                              ]

            -- Determining the logic is surprisingly tricky!
            logic :: [String]
    logic
               -- user told us what to do: so just take it:
               | Just l :: Logic
    l <- case [Logic
    l | SetLogic l :: Logic
    l <- SMTConfig -> [SMTOption]
    solverSetOptions SMTConfig
    cfg] of
                             []  -> Maybe Logic
    forall a. Maybe a
    Nothing
                             [l :: Logic
    l] -> Logic -> Maybe Logic
    forall a. a -> Maybe a
    Just Logic
    l
                             ls :: [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 [ ""
                                                    , "*** 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 (t :: * -> *) a. Foldable t => t a -> Int
    length [Logic]
    ls)
                                                    , "***  " 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_NONE -> ["; NB. Not setting the logic per user request of Logic_NONE"]
                   _          -> ["(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]
    ++ ") ; NB. User specified."]

               -- There's a reason why we can't handle this problem:
               | Just cantDo :: [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
    $   [ ""
                                     , "*** SBV is unable to choose a proper solver configuration:"
                                     , "***"
                                     ]
                                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    cantDo
                                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "***"
                                    , "*** 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
    hasInteger Bool -> Bool -> Bool
    || Bool
    hasReal Bool -> Bool -> Bool
    || Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    trueUSorts) Bool -> Bool -> Bool
    || Bool
    hasNonBVArrays Bool -> Bool -> Bool
    || Bool
    hasTuples Bool -> Bool -> Bool
    || Bool
    hasEither Bool -> Bool -> Bool
    || Bool
    hasMaybe Bool -> Bool -> Bool
    || Bool
    hasSets Bool -> Bool -> Bool
    || Bool
    hasList Bool -> Bool -> Bool
    || Bool
    hasString Bool -> Bool -> Bool
    || Bool
    hasArrayInits
               = let why :: String
    why | Bool
    hasInteger            = "has unbounded values"
                         | Bool
    hasReal               = "has algebraic reals"
                         | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    trueUSorts) = "has user-defined sorts"
                         | Bool
    hasNonBVArrays        = "has non-bitvector arrays"
                         | Bool
    hasTuples             = "has tuples"
                         | Bool
    hasEither             = "has either type"
                         | Bool
    hasMaybe              = "has maybe type"
                         | Bool
    hasSets               = "has sets"
                         | Bool
    hasList               = "has lists"
                         | Bool
    hasString             = "has strings"
                         | Bool
    hasArrayInits         = "has array initializers"
                         | Bool
    True                  = "cannot determine the SMTLib-logic to use"
                 in ["(set-logic ALL) ; "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    why String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", using catch-all."]

               | Bool
    hasDouble Bool -> Bool -> Bool
    || Bool
    hasFloat Bool -> Bool -> Bool
    || Bool
    hasRounding
               = if Bool -> Bool
    not ([SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls)
                 then ["(set-logic ALL)"]
                 else if Bool
    hasBVs
                      then ["(set-logic QF_FPBV)"]
                      else ["(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
                   QueryExternal -> ["(set-logic ALL) ; external query, using all logics."]
                   QueryInternal -> ["(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]
    ++ "BV)"]
              where qs :: String
    qs  | [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls Bool -> Bool -> Bool
    && [(String, [String])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, [String])]
    axs = "QF_"  -- axioms are likely to contain quantifiers
                        | Bool
    True                     = ""
                    as :: String
    as  | [(Int, ArrayInfo)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Int, ArrayInfo)]
    arrs                = ""
                        | Bool
    True                     = "A"
                    ufs :: String
    ufs | [(String, SBVType)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, SBVType)]
    uis Bool -> Bool -> Bool
    && [((Int, Kind, Kind), [SV])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [((Int, Kind, Kind), [SV])]
    tbls    = ""     -- we represent tables as UFs
                        | Bool
    True                     = "UF"

            -- SBV always requires the production of models!
            getModels :: [String]
    getModels   = "(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 flattenConfig :: [String]
    flattenConfig <- [SolverCapabilities -> Maybe [String]
    supportsFlattenedModels SolverCapabilities
    solverCaps]]

            -- process all other settings we're given
            userSettings :: [String]
    userSettings = (SMTOption -> [String]) -> [SMTOption] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap SMTOption -> [String]
    opts ([SMTOption] -> [String]) -> [SMTOption] -> [String]
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> [SMTOption]
    solverSetOptions SMTConfig
    cfg
               where opts :: SMTOption -> [String]
    opts SetLogic{} = []     -- processed already
                     opts o :: SMTOption
    o          = [SMTOption -> String
    setSMTOption SMTOption
    o]

            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

            pgm :: [String]
    pgm  =  (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ("; " 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]
    ++ [ "; --- uninterpreted sorts ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, Either String [String]) -> [String])
    -> [(String, Either String [String])] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (String, Either String [String]) -> [String]
    declSort [(String, Either String [String])]
    usorts
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "; --- 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]
    ++ [ "; --- 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]
    ++ [ "; --- 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]
    ++ [ "; --- skolem constants ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [SV] -> SV -> String
    svFunType [SV]
    ss SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    userName SV
    s | Right (s :: SV
    s, ss :: [SV]
    ss) <- [Either SV (SV, [SV])]
    skolemInps]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "; --- optimization tracker variables ---" | Bool -> Bool
    not ([NamedSymVar] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [NamedSymVar]
    trackerVars) ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [SV] -> SV -> String
    svFunType [] SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") ; tracks " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm | (s :: SV
    s, nm :: String
    nm) <- [NamedSymVar]
    trackerVars]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "; --- 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 (((Int, Kind, Kind), [SV]), [String]) -> [String]
    constTable [(((Int, Kind, Kind), [SV]), [String])]
    constTables
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "; --- skolemized 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 (String -> (((Int, Kind, Kind), [SV]), [String]) -> String
    skolemTable ([String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    svType [SV]
    foralls))) [(((Int, Kind, Kind), [SV]), [String])]
    skolemTables
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "; --- 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]
    ++ [ "; --- uninterpreted constants ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, SBVType) -> [String]) -> [(String, SBVType)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (String, SBVType) -> [String]
    declUI [(String, SBVType)]
    uis
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "; --- user given axioms ---" ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, [String]) -> String) -> [(String, [String])] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, [String]) -> String
    declAx [(String, [String])]
    axs
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "; --- formula ---" ]

                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, SBVExpr) -> String) -> [(SV, SBVExpr)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> String
    declDef SMTConfig
    cfg SkolemMap
    skolemMap TableMap
    tableMap) [(SV, SBVExpr)]
    preQuantifierAssigns
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["(assert (forall (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n                 "
                                            ["(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    svType SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")" | SV
    s <- [SV]
    foralls] String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                    | Bool -> Bool
    not ([SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls)
                    ]
                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, SBVExpr) -> String) -> [(SV, SBVExpr)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, SBVExpr) -> String
    mkAssign [(SV, SBVExpr)]
    postQuantifierAssigns

                 [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]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    arraySetups

                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String] -> [String]
    delayedAsserts [String]
    delayedEqualities

                 [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    finalAssert

            -- identify the assignments that can come before the first quantifier
            (preQuantifierAssigns :: [(SV, SBVExpr)]
    preQuantifierAssigns, postQuantifierAssigns :: [(SV, SBVExpr)]
    postQuantifierAssigns)
               | [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls
               = ([], [(SV, SBVExpr)]
    asgns)  -- the apparent "switch" here is OK; rest of the code works correctly if there are no foralls.
               | Bool
    True
               = ((SV, SBVExpr) -> Bool)
    -> [(SV, SBVExpr)] -> ([(SV, SBVExpr)], [(SV, SBVExpr)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (SV, SBVExpr) -> Bool
    forall b. (SV, b) -> Bool
    pre [(SV, SBVExpr)]
    asgns
               where first :: NodeId
    first      = SV -> NodeId
    nodeId ([SV] -> SV
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum [SV]
    foralls)
                     pre :: (SV, b) -> Bool
    pre (s :: SV
    s, _) = SV -> NodeId
    nodeId SV
    s NodeId -> NodeId -> Bool
    forall a. Ord a => a -> a -> Bool
    < NodeId
    first

                     nodeId :: SV -> NodeId
    nodeId (SV _ n :: NodeId
    n) = NodeId
    n

            noOfCloseParens :: Int
    noOfCloseParens
              | [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls = 0
              | Bool
    True         = [(SV, SBVExpr)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(SV, SBVExpr)]
    postQuantifierAssigns Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + (if [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    delayedEqualities then 0 else 1)

            foralls :: [SV]
    foralls    = [SV
    s | Left s :: SV
    s <- [Either SV (SV, [SV])]
    skolemInps]
            forallArgs :: String
    forallArgs = (SV -> String) -> [SV] -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((" " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> String) -> (SV -> String) -> SV -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SV -> String
    forall a. Show a => a -> String
    show) [SV]
    foralls

            (constTables :: [(((Int, Kind, Kind), [SV]), [String])]
    constTables, skolemTables :: [(((Int, Kind, Kind), [SV]), [String])]
    skolemTables) = ([(((Int, Kind, Kind), [SV])
    t, [String]
    d) | (t :: ((Int, Kind, Kind), [SV])
    t, Left d :: [String]
    d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
    allTables], [(((Int, Kind, Kind), [SV])
    t, [String]
    d) | (t :: ((Int, Kind, Kind), [SV])
    t, Right d :: [String]
    d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
    allTables])
            allTables :: [(((Int, Kind, Kind), [SV]), Either [String] [String])]
    allTables = [(((Int, Kind, Kind), [SV])
    t, RoundingMode
    -> SkolemMap
    -> (Bool, String)
    -> [SV]
    -> ((Int, Kind, Kind), [SV])
    -> Either [String] [String]
    genTableData RoundingMode
    rm SkolemMap
    skolemMap (Bool -> Bool
    not ([SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls), String
    forallArgs) (((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]
            (arrayConstants :: [[String]]
    arrayConstants, arrayDelayeds :: [[String]]
    arrayDelayeds, arraySetups :: [[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
    -> Bool
    -> [(SV, CV)]
    -> SkolemMap
    -> (Int, ArrayInfo)
    -> ([String], [String], [String])
    declArray SMTConfig
    cfg (Bool -> Bool
    not ([SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls)) [(SV, CV)]
    consts SkolemMap
    skolemMap) [(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])]
    skolemTables

            delayedAsserts :: [String] -> [String]
    delayedAsserts []              = []
            delayedAsserts ds :: [String]
    ds@(deH :: String
    deH : deTs :: [String]
    deTs)
              | [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls = (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\s :: String
    s -> "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")") [String]
    ds
              | Bool
    True         = (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    letShift (("(and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    deH) String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> String -> String
    align 5) [String]
    deTs)

            letShift :: String -> String
    letShift = Int -> String -> String
    align 12

            finalAssert :: [String]
    finalAssert
              | [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls Bool -> Bool -> Bool
    && Bool
    noConstraints
              = []
              | [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls
              =    (([(String, String)], Either SV SV) -> String)
    -> [([(String, String)], Either SV SV)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(attr :: [(String, String)]
    attr, v :: Either SV SV
    v) -> "(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)], 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 (\(attr :: [(String, String)]
    attr, v :: Either SV SV
    v) -> "(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)], Either SV SV)]
    softAsserts
              | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    namedAsserts)
              = String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" [ "SBV: Constraints with attributes and quantifiers cannot be mixed!"
                                         , "   Quantified variables: " 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
    forall a. Show a => a -> String
    show [SV]
    foralls)
                                         , "   Named constraints   : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " ((String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    forall a. Show a => a -> String
    show [String]
    namedAsserts)
                                         ]
              | Bool -> Bool
    not ([([(String, String)], Either SV SV)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([(String, String)], Either SV SV)]
    softAsserts)
              = String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" [ "SBV: Soft constraints and quantifiers cannot be mixed!"
                                         , "   Quantified variables: " 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
    forall a. Show a => a -> String
    show [SV]
    foralls)
                                         , "   Soft constraints    : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " ((([(String, String)], Either SV SV) -> String)
    -> [([(String, String)], Either SV SV)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ([(String, String)], Either SV SV) -> String
    forall a. Show a => a -> String
    show [([(String, String)], Either SV SV)]
    softAsserts)
                                         ]
              | Bool
    True
              = [String -> String
    impAlign (String -> String
    letShift String
    combined) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    noOfCloseParens ')']
              where mkLiteral :: Either SV SV -> String
    mkLiteral (Left  v :: SV
    v) =            SkolemMap -> SV -> String
    cvtSV SkolemMap
    skolemMap SV
    v
                    mkLiteral (Right v :: SV
    v) = "(not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SkolemMap -> SV -> String
    cvtSV SkolemMap
    skolemMap SV
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

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

                    namedAsserts :: [String]
    namedAsserts = [[(String, String)] -> String
    findName [(String, String)]
    attrs | (_, attrs :: [(String, String)]
    attrs, _) <- [(Bool, [(String, String)], Either SV SV)]
    assertions, Bool -> Bool
    not ([(String, String)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, String)]
    attrs)]
                     where findName :: [(String, String)] -> String
    findName attrs :: [(String, String)]
    attrs = String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe "<anonymous>" ([String] -> Maybe String
    forall a. [a] -> Maybe a
    listToMaybe [String
    nm | (":named", nm :: String
    nm) <- [(String, String)]
    attrs])

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

                    combined :: String
    combined = case [Either SV SV]
    lits of
                                 []               -> "true"
                                 [x :: Either SV SV
    x]              -> Either SV SV -> String
    mkLiteral Either SV SV
    x
                                 xs :: [Either SV SV]
    xs  | (Either SV SV -> Bool) -> [Either SV SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Either SV SV -> Bool
    bad [Either SV SV]
    xs -> "false"
                                     | Bool
    True       -> "(and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((Either SV SV -> String) -> [Either SV SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Either SV SV -> String
    mkLiteral [Either SV SV]
    xs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                      where lits :: [Either SV SV]
    lits = (Either SV SV -> Bool) -> [Either SV SV] -> [Either SV SV]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Either SV SV -> Bool) -> Either SV SV -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Either SV SV -> Bool
    redundant) ([Either SV SV] -> [Either SV SV])
    -> [Either SV SV] -> [Either SV SV]
    forall a b. (a -> b) -> a -> b
    $ [Either SV SV] -> [Either SV SV]
    forall a. Eq a => [a] -> [a]
    nub ([Either SV SV] -> [Either SV SV]
    forall a. Ord a => [a] -> [a]
    sort ((([(String, String)], Either SV SV) -> Either SV SV)
    -> [([(String, String)], Either SV SV)] -> [Either SV SV]
    forall a b. (a -> b) -> [a] -> [b]
    map ([(String, String)], Either SV SV) -> Either SV SV
    forall a b. (a, b) -> b
    snd [([(String, String)], Either SV SV)]
    hardAsserts))
                            redundant :: Either SV SV -> Bool
    redundant (Left v :: SV
    v)  = SV
    v SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV
                            redundant (Right v :: SV
    v) = SV
    v SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV
                            bad :: Either SV SV -> Bool
    bad (Left  v :: SV
    v) = SV
    v SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV
                            bad (Right v :: SV
    v) = SV
    v SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV

            impAlign :: String -> String
    impAlign s :: String
    s
              | [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    delayedEqualities = String
    s
              | Bool
    True                   = "     " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

            align :: Int -> String -> String
    align n :: Int
    n s :: String
    s = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    n ' ' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

            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 (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 [] (\r :: 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') | (isSoft :: Bool
    isSoft, attrs :: [(String, String)]
    attrs, c :: SV
    c) <- Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (Bool, [(String, String)], SV)
    cstrs, Just c' :: 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 s :: 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 s :: 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

            skolemMap :: SkolemMap
    skolemMap = [(SV, [SV])] -> SkolemMap
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList [(SV
    s, [SV]
    ss) | Right (s :: SV
    s, ss :: [SV]
    ss) <- [Either SV (SV, [SV])]
    skolemInps, Bool -> Bool
    not ([SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    ss)]
            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)
    mkConstTable [(((Int, Kind, Kind), [SV]), [String])]
    constTables [(Int, String)] -> [(Int, String)] -> [(Int, String)]
    forall a. [a] -> [a] -> [a]
    ++ ((((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)
    mkSkTable [(((Int, Kind, Kind), [SV]), [String])]
    skolemTables
              where mkConstTable :: (((a, b, c), b), b) -> (a, String)
    mkConstTable (((t :: a
    t, _, _), _), _) = (a
    t, "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    t)
                    mkSkTable :: (((a, b, c), b), b) -> (a, String)
    mkSkTable    (((t :: a
    t, _, _), _), _) = (a
    t, "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    forallArgs)
            asgns :: [(SV, SBVExpr)]
    asgns = Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (SV, SBVExpr)
    asgnsSeq

            mkAssign :: (SV, SBVExpr) -> String
    mkAssign a :: (SV, SBVExpr)
    a
              | [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    foralls = SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> String
    declDef SMTConfig
    cfg SkolemMap
    skolemMap TableMap
    tableMap (SV, SBVExpr)
    a
              | Bool
    True         = String -> String
    letShift ((SV, SBVExpr) -> String
    forall a. Show a => (a, SBVExpr) -> String
    mkLet (SV, SBVExpr)
    a)

            mkLet :: (a, SBVExpr) -> String
    mkLet (s :: a
    s, SBVApp (Label m :: String
    m) [e :: SV
    e]) = "(let ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SkolemMap -> SV -> String
    cvtSV                SkolemMap
    skolemMap          SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")) ; " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    m
            mkLet (s :: a
    s, e :: SBVExpr
    e)                    = "(let ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SolverCapabilities
    -> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String
    cvtExp SolverCapabilities
    solverCaps RoundingMode
    rm SkolemMap
    skolemMap TableMap
    tableMap SBVExpr
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"

            userNameMap :: Map SV String
    userNameMap = [NamedSymVar] -> Map SV String
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList (((Quantifier, NamedSymVar) -> NamedSymVar)
    -> [(Quantifier, NamedSymVar)] -> [NamedSymVar]
    forall a b. (a -> b) -> [a] -> [b]
    map (Quantifier, NamedSymVar) -> NamedSymVar
    forall a b. (a, b) -> b
    snd [(Quantifier, NamedSymVar)]
    inputs)
            userName :: SV -> String
    userName s :: 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 u :: 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 -> " ; tracks user variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    u
                            _ -> ""

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

    -- | 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 arity :: Int
    arity
      | Int
    arity Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 = ["(declare-datatypes ((SBVTuple0 0)) (((mkSBVTuple0))))"]
      | Int
    arity Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1 = String -> [String]
    forall a. HasCallStack => String -> a
    error "Data.SBV.declTuple: Unexpected one-tuple"
      | Bool
    True       =    (String
    l1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "(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 <- [1..Int
    arity]] String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")")
                     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 <- [1..Int
    arity]]
      where l1 :: String
    l1     = "(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
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    arity String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")) ("
            l2 :: String
    l2     = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    l1) ' ' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "((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]
    ++ " "
            tab :: String
    tab    = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    l2) ' '

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

            proj :: a -> String
    proj i :: a
    i = "(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]
    ++ "_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
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    param a
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

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

            param :: a -> String
    param i :: a
    i = "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 ks :: 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 (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 tupKs :: [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

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

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

    -- | 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 inps :: [NamedSymVar]
    inps newKs :: Set Kind
    newKs consts :: [(SV, CV)]
    consts arrs :: [(Int, ArrayInfo)]
    arrs tbls :: [((Int, Kind, Kind), [SV])]
    tbls uis :: [(String, SBVType)]
    uis (SBVPgm asgnsSeq :: Seq (SV, SBVExpr)
    asgnsSeq) cstrs :: Seq (Bool, [(String, String)], SV)
    cstrs cfg :: SMTConfig
    cfg =
                -- any new settings?
                   [String]
    settings
                -- sorts
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((String, Either String [String]) -> [String])
    -> [(String, Either String [String])] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (String, Either String [String]) -> [String]
    declSort [(String
    s, Either String [String]
    dt) | KUninterpreted s :: String
    s dt :: Either String [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 a b. (a -> b) -> [a] -> [b]
    map NamedSymVar -> String
    forall b. (SV, b) -> 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, SBVType) -> [String]) -> [(String, SBVType)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (String, SBVType) -> [String]
    declUI [(String, SBVType)]
    uis
                -- 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 (((Int, Kind, Kind), [SV]), [String]) -> [String]
    constTable [(((Int, Kind, Kind), [SV]), [String])]
    allTables
                -- expressions
                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ((SV, SBVExpr) -> String) -> [(SV, SBVExpr)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map  (SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> String
    declDef SMTConfig
    cfg SkolemMap
    forall k a. Map k a
    skolemMap TableMap
    tableMap) (Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
    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
                -- 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 (\(isSoft :: Bool
    isSoft, attr :: [(String, String)]
    attr, v :: SV
    v) -> "(assert" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (if Bool
    isSoft then "-soft " else " ") String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)] -> String -> String
    addAnnotations [(String, String)]
    attr (SkolemMap -> SV -> String
    cvtSV SkolemMap
    forall k a. Map k a
    skolemMap SV
    v) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")") (Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (Bool, [(String, String)], SV)
    cstrs)
      where -- NB. The below setting of skolemMap to empty is OK, since we do
            -- not support queries in the context of skolemized variables
            skolemMap :: Map k a
    skolemMap = 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 :: (SV, b) -> String
    declInp (s :: SV
    s, _) = "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    svType SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            (arrayConstants :: [[String]]
    arrayConstants, arrayDelayeds :: [[String]]
    arrayDelayeds, arraySetups :: [[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
    -> Bool
    -> [(SV, CV)]
    -> SkolemMap
    -> (Int, ArrayInfo)
    -> ([String], [String], [String])
    declArray SMTConfig
    cfg Bool
    False [(SV, CV)]
    consts SkolemMap
    forall k a. Map k a
    skolemMap) [(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
    -> SkolemMap
    -> (Bool, String)
    -> [SV]
    -> ((Int, Kind, Kind), [SV])
    -> Either [String] [String]
    genTableData RoundingMode
    rm SkolemMap
    forall k a. Map k a
    skolemMap (Bool
    False, []) (((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]
            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)
    mkTable [(((Int, Kind, Kind), [SV]), [String])]
    allTables
              where mkTable :: (((a, b, c), b), b) -> (a, String)
    mkTable (((t :: a
    t, _, _), _), _) = (a
    t, "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 :: SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> String
    declDef :: SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> String
    declDef cfg :: SMTConfig
    cfg skolemMap :: SkolemMap
    skolemMap tableMap :: TableMap
    tableMap (s :: SV
    s, expr :: SBVExpr
    expr) =
            case SBVExpr
    expr of
              SBVApp  (Label m :: String
    m) [e :: SV
    e] -> NamedSymVar -> Maybe String -> String
    defineFun (SV
    s, SkolemMap -> SV -> String
    cvtSV          SkolemMap
    skolemMap          SV
    e) (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    m)
              e :: SBVExpr
    e                     -> NamedSymVar -> Maybe String -> String
    defineFun (SV
    s, SolverCapabilities
    -> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String
    cvtExp SolverCapabilities
    caps RoundingMode
    rm SkolemMap
    skolemMap TableMap
    tableMap 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 :: (SV, String) -> Maybe String -> String
    defineFun :: NamedSymVar -> Maybe String -> String
    defineFun (s :: SV
    s, def :: String
    def) mbComment :: Maybe String
    mbComment = "(define-fun "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    varT String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    def String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cmnt
      where varT :: String
    varT      = SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " 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
    forall a. [a] -> [a] -> [a]
    ++) Maybe String
    mbComment

    -- 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 cfg :: SMTConfig
    cfg (s :: SV
    s, c :: 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
      = [NamedSymVar -> Maybe String -> String
    defineFun (SV
    s, RoundingMode -> CV -> String
    cvtCV (SMTConfig -> RoundingMode
    roundingMode SMTConfig
    cfg) CV
    c) Maybe String
    forall a. Maybe a
    Nothing]

    declUI :: (String, SBVType) -> [String]
    declUI :: (String, SBVType) -> [String]
    declUI (i :: String
    i, t :: SBVType
    t) = ["(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVType -> String
    cvtType SBVType
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"]

    -- NB. We perform no check to as to whether the axiom is meaningful in any way.
    declAx :: (String, [String]) -> String
    declAx :: (String, [String]) -> String
    declAx (nm :: String
    nm, ls :: [String]
    ls) = (";; -- user given axiom: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "\n") String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" [String]
    ls

    constTable :: (((Int, Kind, Kind), [SV]), [String]) -> [String]
    constTable :: (((Int, Kind, Kind), [SV]), [String]) -> [String]
    constTable (((i :: Int
    i, ak :: Kind
    ak, rk :: Kind
    rk), _elts :: [SV]
    _elts), is :: [String]
    is) = String
    decl 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 [(0::Int)..] [String]
    is [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    setup
      where t :: String
    t       = "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
            decl :: String
    decl    = "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    ak String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    rk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

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

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

            lis :: Int
    lis  = [String] -> 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
    == 0       = [ "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () Bool true) ; no initializiation needed"
                                 ]
              | Int
    lis Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1       = [ "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () Bool " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkInit 0 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                 , "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                 ]
              | Bool
    True           = [ "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () 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 [0..Int
    lis Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                                 , "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                 ]

    skolemTable :: String -> (((Int, Kind, Kind), [SV]), [String]) -> String
    skolemTable :: String -> (((Int, Kind, Kind), [SV]), [String]) -> String
    skolemTable qsIn :: String
    qsIn (((i :: Int
    i, ak :: Kind
    ak, rk :: Kind
    rk), _elts :: [SV]
    _elts), _) = String
    decl
      where qs :: String
    qs   = if String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    qsIn then "" else String
    qsIn String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " "
            t :: String
    t    = "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
            decl :: String
    decl = "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    qs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    ak String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    rk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

    -- Left if all constants, Right if otherwise
    genTableData :: RoundingMode -> SkolemMap -> (Bool, String) -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String]
    genTableData :: RoundingMode
    -> SkolemMap
    -> (Bool, String)
    -> [SV]
    -> ((Int, Kind, Kind), [SV])
    -> Either [String] [String]
    genTableData rm :: RoundingMode
    rm skolemMap :: SkolemMap
    skolemMap (_quantified :: Bool
    _quantified, args :: String
    args) consts :: [SV]
    consts ((i :: Int
    i, aknd :: Kind
    aknd, _), elts :: [SV]
    elts)
      | [(Bool, (String, String))] -> 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
    topLevel ((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
    nested   ((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 ssv :: SV -> String
    ssv = SkolemMap -> SV -> String
    cvtSV SkolemMap
    skolemMap
            (pre :: [(Bool, (String, String))]
    pre, post :: [(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 a. Integral a => SV -> a -> (Bool, (String, String))
    mkElt [SV]
    elts [(0::Int)..])
            t :: String
    t           = "table" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i

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

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

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

    -- TODO: We currently do not support non-constant arrays when quantifiers are present, as
    -- we might have to skolemize those. Implement this properly.
    -- The difficulty is with the Mutate/Merge: We have to postpone an init if
    -- the components are themselves postponed, so this cannot be implemented as a simple map.
    declArray :: SMTConfig -> Bool -> [(SV, CV)] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String])
    declArray :: SMTConfig
    -> Bool
    -> [(SV, CV)]
    -> SkolemMap
    -> (Int, ArrayInfo)
    -> ([String], [String], [String])
    declArray cfg :: SMTConfig
    cfg quantified :: Bool
    quantified consts :: [(SV, CV)]
    consts skolemMap :: SkolemMap
    skolemMap (i :: Int
    i, (_, (aKnd :: Kind
    aKnd, bKnd :: Kind
    bKnd), ctx :: 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 [(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 constNames :: [SV]
    constNames = ((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
            topLevel :: Bool
    topLevel = Bool -> Bool
    not Bool
    quantified Bool -> Bool -> Bool
    || case ArrayContext
    ctx of
                                           ArrayFree mbi :: Maybe SV
    mbi      -> Bool -> (SV -> Bool) -> Maybe SV -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True (SV -> [SV] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [SV]
    constNames) Maybe SV
    mbi
                                           ArrayMutate _ a :: SV
    a b :: SV
    b  -> (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (SV -> [SV] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [SV]
    constNames) [SV
    a, SV
    b]
                                           ArrayMerge c :: SV
    c _ _   -> SV
    c SV -> [SV] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [SV]
    constNames
            (pre :: [(Bool, String)]
    pre, post :: [(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 = "array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i

            ssv :: SV -> String
    ssv sv :: SV
    sv
             | Bool
    topLevel Bool -> Bool -> Bool
    || SV
    sv SV -> [SV] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [SV]
    constNames
             = SkolemMap -> SV -> String
    cvtSV SkolemMap
    skolemMap SV
    sv
             | Bool
    True
             = String -> String
    forall a. String -> a
    tbd "Non-constant array initializer in a quantified context"

            atyp :: String
    atyp  = "(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
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    bKnd String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            adecl :: String
    adecl = case ArrayContext
    ctx of
                      ArrayFree (Just v :: SV
    v) -> "(define-fun "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    atyp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " ((as const " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    atyp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    constInit SV
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                      _                  -> "(declare-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    atyp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++                                                  ")"

            -- 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 v :: SV
    v = case SV
    v SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    consts of
                            Nothing -> SV -> String
    ssv SV
    v                      -- Z3 will work, CVC4 will choke. Others don't even support this.
                            Just c :: 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 _       -> []
                        ArrayMutate j :: ArrayIndex
    j a :: SV
    a b :: SV
    b -> [((SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (SV -> [SV] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [SV]
    constNames) [SV
    a, SV
    b], "(= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " (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
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))")]
                        ArrayMerge  t :: SV
    t j :: ArrayIndex
    j k :: ArrayIndex
    k -> [(SV
    t SV -> [SV] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [SV]
    constNames,            "(= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " (ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " 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]
    ++ " 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]
    ++ "))")]

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

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

            lpre :: Int
    lpre          = [(Bool, String)] -> 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 (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
    == 0      = [ "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () Bool true) ; no initializiation needed" | Bool -> Bool
    not Bool
    quantified]
              | Int
    lAll Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1      = [ "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () Bool " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkInit 0 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                 , "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                 ]
              | Bool
    True           = [ "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () 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 [0..Int
    lAll Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                                 , "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    initializer String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                 ]

    svType :: SV -> String
    svType :: SV -> String
    svType s :: 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 ss :: [SV]
    ss s :: SV
    s = "(" 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
    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 "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!"
    cvtType (SBVType xs :: [Kind]
    xs) = "(" 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
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    ret
      where (body :: [Kind]
    body, ret :: Kind
    ret) = ([Kind] -> [Kind]
    forall a. [a] -> [a]
    init [Kind]
    xs, [Kind] -> Kind
    forall a. [a] -> a
    last [Kind]
    xs)

    type SkolemMap = M.Map SV [SV]
    type TableMap  = IM.IntMap String

    -- Present an SV; inline true/false as needed
    cvtSV :: SkolemMap -> SV -> String
    cvtSV :: SkolemMap -> SV -> String
    cvtSV skolemMap :: SkolemMap
    skolemMap s :: SV
    s@(SV _ (NodeId n :: Int
    n))
      | Just ss :: [SV]
    ss <- SV
    s SV -> SkolemMap -> Maybe [SV]
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` SkolemMap
    skolemMap
      = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (SV -> String) -> [SV] -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((" " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> String) -> (SV -> String) -> SV -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SV -> String
    forall a. Show a => a -> String
    show) [SV]
    ss String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV
      = "true"
      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV
      = "false"
      | Bool
    True
      = 's' Char -> String -> String
    forall a. a -> [a] -> [a]
    : Int -> String
    forall a. Show a => a -> String
    show Int
    n

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

    getTable :: TableMap -> Int -> String
    getTable :: TableMap -> Int -> String
    getTable m :: TableMap
    m i :: Int
    i
      | Just tn :: String
    tn <- Int
    i Int -> TableMap -> Maybe String
    forall a. Int -> IntMap a -> Maybe a
    `IM.lookup` TableMap
    m = String
    tn
      | Bool
    True                       = "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 :: SolverCapabilities -> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String
    cvtExp :: SolverCapabilities
    -> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String
    cvtExp caps :: SolverCapabilities
    caps rm :: RoundingMode
    rm skolemMap :: SkolemMap
    skolemMap tableMap :: TableMap
    tableMap expr :: SBVExpr
    expr@(SBVApp _ arguments :: [SV]
    arguments) = SBVExpr -> String
    sh SBVExpr
    expr
      where ssv :: SV -> String
    ssv = SkolemMap -> SV -> String
    cvtSV SkolemMap
    skolemMap

            supportsPB :: Bool
    supportsPB = SolverCapabilities -> Bool
    supportsPseudoBooleans SolverCapabilities
    caps

            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
            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
            doubleOp :: Bool
    doubleOp = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    isDouble    [SV]
    arguments
            floatOp :: Bool
    floatOp  = (SV -> Bool) -> [SV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any SV -> Bool
    forall a. HasKind a => a -> Bool
    isFloat     [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 :: p
    bad | Bool
    intOp = String -> p
    forall a. HasCallStack => String -> a
    error (String -> p) -> String -> p
    forall a b. (a -> b) -> a -> b
    $ "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 -> p
    forall a. HasCallStack => String -> a
    error (String -> p) -> String -> p
    forall a b. (a -> b) -> a -> b
    $ "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 p. p
    bad
            ensureBV :: Bool
    ensureBV       = Bool
    bvOp Bool -> Bool -> Bool
    || Bool
    forall p. p
    bad

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

            -- lift a binary op
            lift2 :: String -> p -> [String] -> String
    lift2  o :: String
    o _ [x :: String
    x, y :: String
    y] = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            lift2  o :: String
    o _ sbvs :: [String]
    sbvs   = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "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 o :: String
    o _ xs :: [String]
    xs = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            -- lift a binary operation with rounding-mode added; used for floating-point arithmetic
            lift2WM :: String -> String -> p -> [String] -> String
    lift2WM o :: String
    o fo :: String
    fo | Bool
    doubleOp Bool -> Bool -> Bool
    || Bool
    floatOp = 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 o :: String
    o fo :: String
    fo | Bool
    doubleOp Bool -> Bool -> Bool
    || Bool
    floatOp = 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 sgned :: Bool
    sgned args :: [String]
    args | Bool
    doubleOp Bool -> Bool -> Bool
    || Bool
    floatOp = String -> Bool -> [String] -> String
    forall p. String -> p -> [String] -> String
    lift1 "fp.abs" Bool
    sgned [String]
    args
                               | Bool
    intOp               = String -> Bool -> [String] -> String
    forall p. String -> p -> [String] -> String
    lift1 "abs"    Bool
    sgned [String]
    args
                               | Bool
    bvOp, Bool
    sgned         = String -> String -> String -> String
    mkAbs ([String] -> String
    forall a. [a] -> a
    head [String]
    args) "bvslt" "bvneg"
                               | Bool
    bvOp                = [String] -> String
    forall a. [a] -> a
    head [String]
    args
                               | Bool
    True                = String -> String -> String -> String
    mkAbs ([String] -> String
    forall a. [a] -> a
    head [String]
    args) "<"     "-"
              where mkAbs :: String -> String -> String -> String
    mkAbs x :: String
    x cmp :: String
    cmp neg :: String
    neg = "(ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ltz String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nx String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                      where ltz :: String
    ltz = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cmp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    z String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                            nx :: String
    nx  = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    neg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                            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. [a] -> a
    head [SV]
    arguments)) (0::Integer))

            lift2B :: String -> String -> p -> [String] -> String
    lift2B bOp :: String
    bOp vOp :: 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 bOp :: String
    bOp vOp :: 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 "="
            neqBV :: p -> [String] -> String
    neqBV = String -> p -> [String] -> String
    forall p. String -> p -> [String] -> String
    liftN "distinct"

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

            notEqual :: p -> [String] -> String
    notEqual sgn :: p
    sgn sbvs :: [String]
    sbvs
              | Bool
    doubleOp = [String] -> String
    liftP [String]
    sbvs
              | Bool
    floatOp  = [String] -> String
    liftP [String]
    sbvs
              | Bool
    True     = String -> p -> [String] -> String
    forall p. String -> p -> [String] -> String
    liftN "distinct" p
    sgn [String]
    sbvs
              where liftP :: [String] -> String
    liftP [_, _] = "(not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ p -> [String] -> String
    forall p. p -> [String] -> String
    equal p
    sgn [String]
    sbvs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                    liftP args :: [String]
    args   = "(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]
    ++ ")"

                    walk :: [String] -> [String]
    walk []     = []
                    walk (e :: String
    e:es :: [String]
    es) = (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> String -> String
    pair String
    e) [String]
    es [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String] -> [String]
    walk [String]
    es

                    pair :: String -> String -> String
    pair e1 :: String
    e1 e2 :: String
    e2  = "(not (fp.eq " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    e1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    e2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"

            lift2S :: String -> String -> Bool -> [String] -> String
    lift2S oU :: String
    oU oS :: String
    oS sgn :: 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 oU :: String
    oU oS :: String
    oS sgn :: 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 o :: String
    o fo :: String
    fo | Bool
    doubleOp Bool -> Bool -> Bool
    || Bool
    floatOp = 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 o :: String
    o [a :: String
    a, b :: String
    b]
              | KUninterpreted s :: String
    s (Right _) <- SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    arguments)
              = let idx :: String -> String
    idx v :: String
    v = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "_constrIndex " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")" in "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    idx String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    idx String
    b String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            unintComp o :: String
    o sbvs :: [String]
    sbvs = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "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)

            -- NB. String comparisons are currently not supported by Z3; but will be with the new logic.
            stringCmp :: Bool -> String -> [String] -> String
    stringCmp swap :: Bool
    swap o :: String
    o [a :: String
    a, b :: String
    b]
              | Kind
    KString <- SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    arguments)
              = let [a1 :: String
    a1, a2 :: String
    a2] | Bool
    swap = [String
    b, String
    a]
                             | Bool
    True = [String
    a, String
    b]
                in "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            stringCmp _ o :: String
    o sbvs :: [String]
    sbvs = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "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 swap :: Bool
    swap o :: String
    o [a :: String
    a, b :: String
    b]
              | KList{} <- SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ([SV] -> SV
    forall a. [a] -> a
    head [SV]
    arguments)
              = let [a1 :: String
    a1, a2 :: String
    a2] | Bool
    swap = [String
    b, String
    a]
                             | Bool
    True = [String
    a, String
    b]
                in "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a2 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            seqCmp _ o :: String
    o sbvs :: [String]
    sbvs = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "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  o :: String
    o _ [x :: String
    x]    = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            lift1  o :: String
    o _ sbvs :: [String]
    sbvs   = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "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 fld :: String
    fld args :: [SV]
    args res :: Kind
    res = "((as " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fld String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    res String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " 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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            -- Similarly, we fully qualify the accessors with their types to work around type checking issues
            dtAccessor :: String -> [Kind] -> Kind -> String
    dtAccessor fld :: String
    fld params :: [Kind]
    params res :: Kind
    res = String
    result
              where ps :: String
    ps       = " (" 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]
    ++ ") "
                    result :: String
    result   = "(_ 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]
    ++ "))"

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

            sh (SBVApp (LkUp (t :: Int
    t, aKnd :: Kind
    aKnd, _, l :: Int
    l) i :: SV
    i e :: SV
    e) [])
              | Bool
    needsCheck = "(ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cond String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    lkUp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
              | Bool
    True       = String
    lkUp
              where needsCheck :: Bool
    needsCheck = case Kind
    aKnd of
                                  KBool              -> (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 _ n :: Int
    n       -> (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
                                  KUnbounded         -> Bool
    True
                                  KReal              -> String -> Bool
    forall a. HasCallStack => String -> a
    error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index"
                                  KFloat             -> String -> Bool
    forall a. HasCallStack => String -> a
    error "SBV.SMT.SMTLib2.cvtExp: unexpected float valued index"
                                  KDouble            -> String -> Bool
    forall a. HasCallStack => String -> a
    error "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index"
                                  KChar              -> String -> Bool
    forall a. HasCallStack => String -> a
    error "SBV.SMT.SMTLib2.cvtExp: unexpected char valued index"
                                  KString            -> String -> Bool
    forall a. HasCallStack => String -> a
    error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                  KList k :: Kind
    k            -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "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  k :: Kind
    k            -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "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 k :: [Kind]
    k           -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "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 k :: Kind
    k           -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "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 k1 :: Kind
    k1 k2 :: Kind
    k2      -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "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)
                                  KUninterpreted s :: String
    s _ -> String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

                    lkUp :: String
    lkUp = "(" 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
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

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

                    (less :: String
    less, leq :: String
    leq) = case Kind
    aKnd of
                                    KBool              -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index"
                                    KBounded{}         -> if SV -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SV
    i then ("bvslt", "bvsle") else ("bvult", "bvule")
                                    KUnbounded         -> ("<", "<=")
                                    KReal              -> ("<", "<=")
                                    KFloat             -> ("fp.lt", "fp.leq")
                                    KDouble            -> ("fp.lt", "fp.geq")
                                    KChar              -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                    KString            -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                    KList k :: Kind
    k            -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ "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  k :: Kind
    k            -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ "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 k :: [Kind]
    k           -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ "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 k :: Kind
    k           -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ "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 k1 :: Kind
    k1 k2 :: Kind
    k2      -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ "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)
                                    KUninterpreted s :: String
    s _ -> String -> (String, String)
    forall a. HasCallStack => String -> a
    error (String -> (String, String)) -> String -> (String, String)
    forall a b. (a -> b) -> a -> b
    $ "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
    forall a. [a] -> [a] -> [a]
    ++ String
    less String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkCnst 0 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                    gtl :: String
    gtl  = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    leq  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    mkCnst Int
    l String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            sh (SBVApp (KindCast f :: Kind
    f t :: Kind
    t) [a :: SV
    a]) = Kind -> Kind -> String -> String
    handleKindCast Kind
    f Kind
    t (SV -> String
    ssv SV
    a)

            sh (SBVApp (ArrEq i :: ArrayIndex
    i j :: ArrayIndex
    j) [])  = "(= 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]
    ++ " 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]
    ++")"
            sh (SBVApp (ArrRead i :: ArrayIndex
    i) [a :: SV
    a]) = "(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
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            sh (SBVApp (Uninterpreted nm :: String
    nm) [])   = String
    nm
            sh (SBVApp (Uninterpreted nm :: String
    nm) args :: [SV]
    args) = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " 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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

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

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

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

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

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

            sh (SBVApp op :: Op
    op args :: [SV]
    args)
              | Just f :: 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
    ssv [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 "and" "bvand")
                                   , (Op
    Or,   String -> String -> p -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift2B "or"  "bvor")
                                   , (Op
    XOr,  String -> String -> p -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift2B "xor" "bvxor")
                                   , (Op
    Not,  String -> String -> p -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift1B "not" "bvnot")
                                   , (Op
    Join, String -> p -> [String] -> String
    forall p. String -> p -> [String] -> String
    lift2 "concat")
                                   ]

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

            sh (SBVApp (IEEEFP (FP_Cast kFrom :: Kind
    kFrom kTo :: Kind
    kTo m :: SV
    m)) args :: [SV]
    args) = Kind -> Kind -> String -> String -> String
    handleFPCast Kind
    kFrom Kind
    kTo (SV -> String
    ssv SV
    m) ([String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    ssv [SV]
    args))
            sh (SBVApp (IEEEFP w :: FPOp
    w                    ) args :: [SV]
    args) = "(" 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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            sh (SBVApp (PseudoBoolean pb :: PBOp
    pb) args :: [SV]
    args)
              | Bool
    supportsPB = 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
    ssv [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 op :: OvOp
    op) args :: [SV]
    args) = "(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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"

            -- Note the unfortunate reversal in StrInRe..
            sh (SBVApp (StrOp (StrInRe r :: RegExp
    r)) args :: [SV]
    args) = "(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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ RegExp -> String
    forall a. Show a => a -> String
    show RegExp
    r String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (StrOp op :: StrOp
    op)          args :: [SV]
    args) = "(" 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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            sh (SBVApp (SeqOp op :: SeqOp
    op) args :: [SV]
    args) = "(" 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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            sh (SBVApp (SetOp SetEqual)      args :: [SV]
    args)   = "(= "      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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (SetOp SetMember)     [e :: SV
    e, s :: SV
    s]) = "(select " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (SetOp SetInsert)     [e :: SV
    e, s :: SV
    s]) = "(store "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " true)"
            sh (SBVApp (SetOp SetDelete)     [e :: SV
    e, s :: SV
    s]) = "(store "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    e String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " false)"
            sh (SBVApp (SetOp SetIntersect)  args :: [SV]
    args)   = "(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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (SetOp SetUnion)      args :: [SV]
    args)   = "(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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (SetOp SetSubset)     args :: [SV]
    args)   = "(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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (SetOp SetDifference) args :: [SV]
    args)   = "(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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (SetOp SetComplement) args :: [SV]
    args)   = "(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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (SetOp SetHasSize)    args :: [SV]
    args)   = "(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
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            sh (SBVApp (TupleConstructor 0)   [])    = "mkSBVTuple0"
            sh (SBVApp (TupleConstructor n :: Int
    n)   args :: [SV]
    args)  = "(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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    ssv [SV]
    args) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (SBVApp (TupleAccess      i :: Int
    i n :: Int
    n) [tup :: SV
    tup]) = "(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]
    ++ "_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
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    tup String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

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

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

            sh inp :: SBVExpr
    inp@(SBVApp op :: Op
    op args :: [SV]
    args)
              | Bool
    intOp, Just f :: 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
    ssv [SV]
    args)
              | Bool
    boolOp, Just f :: [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
    ssv [SV]
    args)
              | Bool
    bvOp, Just f :: 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
    ssv [SV]
    args)
              | Bool
    realOp, Just f :: 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
    ssv [SV]
    args)
              | Bool
    floatOp Bool -> Bool -> Bool
    || Bool
    doubleOp, Just f :: 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
    ssv [SV]
    args)
              | Bool
    charOp, Just f :: 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)]
    smtCharTable
              = Bool -> [String] -> String
    f Bool
    False ((SV -> String) -> [SV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> String
    ssv [SV]
    args)
              | Bool
    stringOp, Just f :: [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
    ssv [SV]
    args)
              | Bool
    listOp, Just f :: [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
    ssv [SV]
    args)
              | Just f :: [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
    ssv [SV]
    args)
              | Bool
    True
              = if Bool -> Bool
    not ([SV] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SV]
    args) Bool -> Bool -> Bool
    && SV -> Bool
    forall a. HasKind a => a -> Bool
    isUninterpreted ([SV] -> SV
    forall a. [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 [ ""
                                     , "*** Cannot translate operator        : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Op -> String
    forall a. Show a => a -> String
    show Op
    op
                                     , "*** 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]
    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))
                                     , "*** 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
                                     , "***"
                                     , "*** Note that uninterpreted kinds only support equality."
                                     , "*** 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
    $ "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   "bvadd")
                                    , (Op
    Minus,         String -> Bool -> [String] -> String
    forall p. String -> p -> [String] -> String
    lift2   "bvsub")
                                    , (Op
    Times,         String -> Bool -> [String] -> String
    forall p. String -> p -> [String] -> String
    lift2   "bvmul")
                                    , (Op
    UNeg,          String -> String -> Bool -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift1B  "not"    "bvneg")
                                    , (Op
    Abs,           Bool -> [String] -> String
    liftAbs)
                                    , (Op
    Quot,          String -> String -> Bool -> [String] -> String
    lift2S  "bvudiv" "bvsdiv")
                                    , (Op
    Rem,           String -> String -> Bool -> [String] -> String
    lift2S  "bvurem" "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  "bvult" "bvslt")
                                    , (Op
    GreaterThan,   String -> String -> Bool -> [String] -> String
    lift2S  "bvugt" "bvsgt")
                                    , (Op
    LessEq,        String -> String -> Bool -> [String] -> String
    lift2S  "bvule" "bvsle")
                                    , (Op
    GreaterEq,     String -> String -> Bool -> [String] -> String
    lift2S  "bvuge" "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 [x :: String
    x, y :: String
    y] = "(and (not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                         blt xs :: [String]
    xs     = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "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 [x :: String
    x, y :: String
    y] = "(or (not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    y String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                         blq xs :: [String]
    xs     = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "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 [x :: a
    x, y :: a
    y] = [a
    y, a
    x]
                                         swp xs :: [a]
    xs     = String -> [a]
    forall a. HasCallStack => String -> a
    error (String -> [a]) -> String -> [a]
    forall a b. (a -> b) -> a -> b
    $ "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 "/" "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   "div")
                                      , (Op
    Rem,         String -> Bool -> [String] -> String
    forall p. String -> p -> [String] -> String
    lift2   "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 "/" "fp.div")]
                    smtIntRealShared :: [(Op, Bool -> [String] -> String)]
    smtIntRealShared  = [ (Op
    Plus,          String -> String -> Bool -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift2WM "+" "fp.add")
                                        , (Op
    Minus,         String -> String -> Bool -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift2WM "-" "fp.sub")
                                        , (Op
    Times,         String -> String -> Bool -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift2WM "*" "fp.mul")
                                        , (Op
    UNeg,          String -> String -> Bool -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift1FP "-" "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  "<"  "fp.lt")
                                        , (Op
    GreaterThan,   String -> String -> Bool -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift2Cmp  ">"  "fp.gt")
                                        , (Op
    LessEq,        String -> String -> Bool -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift2Cmp  "<=" "fp.leq")
                                        , (Op
    GreaterEq,     String -> String -> Bool -> [String] -> String
    forall p. String -> String -> p -> [String] -> String
    lift2Cmp  ">=" "fp.geq")
                                        ]
                    -- 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 "="        "="        Bool
    True)
                                         , (Op
    NotEqual,    String -> String -> Bool -> [String] -> String
    liftNS "distinct" "distinct" Bool
    True)
                                         , (Op
    LessThan,    String -> [String] -> String
    unintComp "<")
                                         , (Op
    GreaterThan, String -> [String] -> String
    unintComp ">")
                                         , (Op
    LessEq,      String -> [String] -> String
    unintComp "<=")
                                         , (Op
    GreaterEq,   String -> [String] -> String
    unintComp ">=")
                                         ]
                    -- For chars, the underlying type is currently SWord8, so we go with the regular bit-vector operations
                    -- TODO: This will change when we move to unicode!
                    smtCharTable :: [(Op, Bool -> [String] -> String)]
    smtCharTable = [ (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  "bvult" (String -> String
    forall a. HasCallStack => String -> a
    error "smtChar.<: did-not expect signed char here!"))
                                   , (Op
    GreaterThan,   String -> String -> Bool -> [String] -> String
    lift2S  "bvugt" (String -> String
    forall a. HasCallStack => String -> a
    error "smtChar.>: did-not expect signed char here!"))
                                   , (Op
    LessEq,        String -> String -> Bool -> [String] -> String
    lift2S  "bvule" (String -> String
    forall a. HasCallStack => String -> a
    error "smtChar.<=: did-not expect signed char here!"))
                                   , (Op
    GreaterEq,     String -> String -> Bool -> [String] -> String
    lift2S  "bvuge" (String -> String
    forall a. HasCallStack => String -> a
    error "smtChar.>=: did-not expect signed char here!"))
                                   ]
                    -- For strings, equality and comparisons are the only operators
                    -- TODO: The string comparison operators will most likely change with the new theory!
                    smtStringTable :: [(Op, [String] -> String)]
    smtStringTable = [ (Op
    Equal,       String -> String -> Bool -> [String] -> String
    lift2S "="        "="        Bool
    True)
                                     , (Op
    NotEqual,    String -> String -> Bool -> [String] -> String
    liftNS "distinct" "distinct" Bool
    True)
                                     , (Op
    LessThan,    Bool -> String -> [String] -> String
    stringCmp Bool
    False "str.<")
                                     , (Op
    GreaterThan, Bool -> String -> [String] -> String
    stringCmp Bool
    True  "str.<")
                                     , (Op
    LessEq,      Bool -> String -> [String] -> String
    stringCmp Bool
    False "str.<=")
                                     , (Op
    GreaterEq,   Bool -> String -> [String] -> String
    stringCmp Bool
    True  "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 "="        "="        Bool
    True)
                                   , (Op
    NotEqual,    String -> String -> Bool -> [String] -> String
    liftNS "distinct" "distinct" Bool
    True)
                                   , (Op
    LessThan,    Bool -> String -> [String] -> String
    seqCmp Bool
    False "seq.<")
                                   , (Op
    GreaterThan, Bool -> String -> [String] -> String
    seqCmp Bool
    True  "seq.<")
                                   , (Op
    LessEq,      Bool -> String -> [String] -> String
    seqCmp Bool
    False "seq.<=")
                                   , (Op
    GreaterEq,   Bool -> String -> [String] -> String
    seqCmp Bool
    True  "seq.<=")
                                   ]

    -----------------------------------------------------------------------------------------------
    -- 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 kFrom :: Kind
    kFrom kTo :: Kind
    kTo rm :: String
    rm input :: String
    input
      | Kind
    kFrom Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    kTo
      = String
    input
      | Bool
    True
      = "(" 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]
    ++ ")"
      where addRM :: String -> String -> String
    addRM a :: String
    a s :: String
    s = String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a

            -- To go and back from Ints, we detour through reals
            cast :: Kind -> Kind -> String -> String
    cast KUnbounded         KFloat             a :: String
    a = "(_ to_fp 8 24) "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " (to_real " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            cast KUnbounded         KDouble            a :: String
    a = "(_ to_fp 11 53) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " (to_real " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            cast KFloat             KUnbounded         a :: String
    a = "to_int (fp.to_real " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            cast KDouble            KUnbounded         a :: String
    a = "to_int (fp.to_real " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            -- To float/double
            cast (KBounded False _) KFloat             a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp_unsigned 8 24)"
            cast (KBounded False _) KDouble            a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp_unsigned 11 53)"
            cast (KBounded True  _) KFloat             a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp 8 24)"
            cast (KBounded True  _) KDouble            a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp 11 53)"
            cast KReal              KFloat             a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp 8 24)"
            cast KReal              KDouble            a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp 11 53)"

            -- Between floats
            cast KFloat             KFloat             a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp 8 24)"
            cast KFloat             KDouble            a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp 11 53)"
            cast KDouble            KFloat             a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp 8 24)"
            cast KDouble            KDouble            a :: String
    a = String -> String -> String
    addRM String
    a "(_ to_fp 11 53)"

            -- From float/double
            cast KFloat             (KBounded False m :: Int
    m) a :: String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "(_ 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]
    ++ ")"
            cast KDouble            (KBounded False m :: Int
    m) a :: String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "(_ 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]
    ++ ")"
            cast KFloat             (KBounded True  m :: Int
    m) a :: String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "(_ 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]
    ++ ")"
            cast KDouble            (KBounded True  m :: Int
    m) a :: String
    a = String -> String -> String
    addRM String
    a (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "(_ 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]
    ++ ")"

            cast KFloat             KReal              a :: String
    a = "fp.to_real" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a
            cast KDouble            KReal              a :: String
    a = "fp.to_real" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a

            -- Nothing else should come up:
            cast f :: Kind
    f                  d :: Kind
    d                  _ = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "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]
    ++ " to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    d

    rot :: (SV -> String) -> String -> Int -> SV -> String
    rot :: (SV -> String) -> String -> Int -> SV -> String
    rot ssv :: SV -> String
    ssv o :: String
    o c :: Int
    c x :: SV
    x = "((_ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " 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
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

    shft :: (SV -> String) -> String -> String -> SV -> SV -> String
    shft :: (SV -> String) -> String -> String -> SV -> SV -> String
    shft ssv :: SV -> String
    ssv oW :: String
    oW oS :: String
    oS x :: SV
    x c :: SV
    c = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    ssv SV
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
       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 :: Kind -> Kind -> String -> String
    handleKindCast :: Kind -> Kind -> String -> String
    handleKindCast kFrom :: Kind
    kFrom kTo :: Kind
    kTo a :: 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 s :: Bool
    s m :: Int
    m -> case Kind
    kTo of
                            KBounded _ n :: 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
                            KUnbounded   -> Bool -> Int -> String
    forall b. (Integral b, Show b) => Bool -> b -> String
    b2i Bool
    s Int
    m
                            _            -> String
    tryFPCast

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

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

          _            -> 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 (\k :: 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
    $ "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]
    ++ " 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 upConv :: a -> String
    upConv m :: a
    m n :: 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
    - 1)

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

            signExtend :: a -> String
    signExtend i :: a
    i = "((_ 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
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            zeroExtend :: a -> String
    zeroExtend i :: a
    i = "((_ 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
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            extract :: a -> String
    extract    i :: a
    i = "((_ 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]
    ++ " 0) " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            -- NB. The following 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.
            --
            -- NB2. (TODO) There is an SMTLib equivalent of this function, called int2bv. However, it
            -- used to be uninterpreted for a long time by Z3; though I think that got fixed. We
            -- might want to simply use that if it's reliably available across the board in solvers.
            i2b :: Int -> String
    i2b n :: Int
    n = "(let (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    reduced String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") (let (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    defs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    body String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
              where b :: Int -> String
    b i :: 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  = "(__a (mod " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    b Int
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                    mkBit :: Int -> String
    mkBit 0  = "(__a0 (ite (= (mod __a 2) 0) #b0 #b1))"
                    mkBit i :: Int
    i  = "(__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]
    ++ " (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]
    ++ ") 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 [0 .. Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1])
                    body :: String
    body     = (String -> String -> String) -> [String] -> String
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 (\c :: String
    c r :: String
    r -> "(concat " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    r String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")") ["__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
    -1, Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -2 .. 0]]

    -- Translation of pseudo-booleans, in case the solver supports them
    handlePB :: PBOp -> [String] -> String
    handlePB :: PBOp -> [String] -> String
    handlePB (PB_AtMost  k :: Int
    k) args :: [String]
    args = "((_ 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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
    handlePB (PB_AtLeast k :: Int
    k) args :: [String]
    args = "((_ 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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
    handlePB (PB_Exactly k :: Int
    k) args :: [String]
    args = "((_ 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 (t :: * -> *) a. Foldable t => t a -> Int
    length [String]
    args) 1)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
    handlePB (PB_Eq cs :: [Int]
    cs   k :: Int
    k) args :: [String]
    args = "((_ 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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
    handlePB (PB_Le cs :: [Int]
    cs   k :: Int
    k) args :: [String]
    args = "((_ 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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
    handlePB (PB_Ge cs :: [Int]
    cs   k :: Int
    k) args :: [String]
    args = "((_ 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
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

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

      where addIf :: [Int] -> String
            addIf :: [Int] -> String
    addIf cs :: [Int]
    cs = "(+ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ["(ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " 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]
    ++ " 0)" | (a :: String
    a, c :: 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]
    ++ ")"