    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Control.Query
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Querying a solver interactively.
    -----------------------------------------------------------------------------

    {-# LANGUAGE LambdaCase          #-}
    {-# LANGUAGE NamedFieldPuns      #-}
    {-# LANGUAGE Rank2Types          #-}
    {-# LANGUAGE ScopedTypeVariables #-}

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

    module Data.SBV.Control.Query (
           send, ask, retrieveResponse
         , CheckSatResult(..), checkSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
         , getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3, getAssignment, getOption, freshVar, freshVar_, freshArray, freshArray_, push, pop, getAssertionStackDepth
         , inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getValue, getUninterpretedValue, getModel, getSMTResult
         , getLexicographicOptResults, getIndependentOptResults, getParetoOptResults, getAllSatResult, getUnknownReason, getObservables, ensureSat
         , SMTOption(..), SMTInfoFlag(..), SMTErrorBehavior(..), SMTReasonUnknown(..), SMTInfoResponse(..), getInfo
         , Logic(..), Assignment(..)
         , ignoreExitCode, timeout
         , (|->)
         , mkSMTResult
         , io
         ) where

    import Control.Monad          (unless, when, zipWithM)
    import Control.Monad.IO.Class (MonadIO)

    import Data.IORef (readIORef)

    import qualified Data.Map.Strict    as M
    import qualified Data.IntMap.Strict as IM

    import Data.Char     (toLower)
    import Data.List     (intercalate, nubBy, sortBy, sortOn)
    import Data.Maybe    (listToMaybe, catMaybes)
    import Data.Function (on)

    import Data.SBV.Core.Data

    import Data.SBV.Core.Symbolic   ( MonadQuery(..), State(..)
                                    , incrementInternalCounter, validationRequested
                                    )

    import Data.SBV.Utils.SExpr

    import Data.SBV.Control.Types
    import Data.SBV.Control.Utils

    -- | An Assignment of a model binding
    data Assignment = Assign SVal CV

    -- Remove one pair of surrounding 'c's, if present
    noSurrounding :: Char -> String -> String
    noSurrounding :: Char -> String -> String
    noSurrounding c :: Char
    c (c' :: Char
    c':cs :: String
    cs@(_:_)) | Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    c' Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == String -> Char
    forall a. [a] -> a
    last String
    cs  = String -> String
    forall a. [a] -> [a]
    init String
    cs
    noSurrounding _ s :: String
    s                                        = String
    s

    -- Remove a pair of surrounding quotes
    unQuote :: String -> String
    unQuote :: String -> String
    unQuote = Char -> String -> String
    noSurrounding '"'

    -- Remove a pair of surrounding bars
    unBar :: String -> String
    unBar :: String -> String
    unBar = Char -> String -> String
    noSurrounding '|'

    -- Is this a string? If so, return it, otherwise fail in the Maybe monad.
    fromECon :: SExpr -> Maybe String
    fromECon :: SExpr -> Maybe String
    fromECon (ECon s :: String
    s) = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    s
    fromECon _        = Maybe String
    forall a. Maybe a
    Nothing

    -- Collect strings appearing, used in 'getOption' only
    stringsOf :: SExpr -> [String]
    stringsOf :: SExpr -> [String]
    stringsOf (ECon s :: String
    s)      = [String
    s]
    stringsOf (ENum (i :: Integer
    i, _)) = [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i]
    stringsOf (EReal   r :: AlgReal
    r)   = [AlgReal -> String
    forall a. Show a => a -> String
    show AlgReal
    r]
    stringsOf (EFloat  f :: Float
    f)   = [Float -> String
    forall a. Show a => a -> String
    show Float
    f]
    stringsOf (EDouble d :: Double
    d)   = [Double -> String
    forall a. Show a => a -> String
    show Double
    d]
    stringsOf (EApp ss :: [SExpr]
    ss)     = (SExpr -> [String]) -> [SExpr] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap SExpr -> [String]
    stringsOf [SExpr]
    ss

    -- Sort of a light-hearted show for SExprs, for better consumption at the user level.
    serialize :: Bool -> SExpr -> String
    serialize :: Bool -> SExpr -> String
    serialize removeQuotes :: Bool
    removeQuotes = SExpr -> String
    go
      where go :: SExpr -> String
    go (ECon s :: String
    s)      = if Bool
    removeQuotes then String -> String
    unQuote String
    s else String
    s
            go (ENum (i :: Integer
    i, _)) = Integer -> String
    forall a. (Show a, Num a, Ord a) => a -> String
    shNN Integer
    i
            go (EReal   r :: AlgReal
    r)   = AlgReal -> String
    forall a. (Show a, Num a, Ord a) => a -> String
    shNN AlgReal
    r
            go (EFloat  f :: Float
    f)   = Float -> String
    forall a. (Show a, Num a, Ord a) => a -> String
    shNN Float
    f
            go (EDouble d :: Double
    d)   = Double -> String
    forall a. (Show a, Num a, Ord a) => a -> String
    shNN Double
    d
            go (EApp [x :: SExpr
    x])    = SExpr -> String
    go SExpr
    x
            go (EApp ss :: [SExpr]
    ss)     = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((SExpr -> String) -> [SExpr] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SExpr -> String
    go [SExpr]
    ss) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

            -- be careful with negative number printing in SMT-Lib..
            shNN :: (Show a, Num a, Ord a) => a -> String
            shNN :: a -> String
    shNN i :: a
    i
              | a
    i a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    < 0 = "(- " 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]
    ++ ")"
              | Bool
    True  = a -> String
    forall a. Show a => a -> String
    show a
    i

    -- | Generalization of 'Data.SBV.Control.getInfo'
    getInfo :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse
    getInfo :: SMTInfoFlag -> m SMTInfoResponse
    getInfo flag :: SMTInfoFlag
    flag = do
        let cmd :: String
    cmd = "(get-info " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTInfoFlag -> String
    forall a. Show a => a -> String
    show SMTInfoFlag
    flag String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getInfo" String
    cmd "a valid get-info response" Maybe [String]
    forall a. Maybe a
    Nothing

            isAllStatistics :: SMTInfoFlag -> Bool
    isAllStatistics AllStatistics = Bool
    True
            isAllStatistics _             = Bool
    False

            isAllStat :: Bool
    isAllStat = SMTInfoFlag -> Bool
    isAllStatistics SMTInfoFlag
    flag

            grabAllStat :: SExpr -> SExpr -> (String, String)
    grabAllStat k :: SExpr
    k v :: SExpr
    v = (SExpr -> String
    render SExpr
    k, SExpr -> String
    render SExpr
    v)

            -- we're trying to do our best to get key-value pairs here, but this
            -- is necessarily a half-hearted attempt.
            grabAllStats :: SExpr -> [(String, String)]
    grabAllStats (EApp xs :: [SExpr]
    xs) = [SExpr] -> [(String, String)]
    walk [SExpr]
    xs
               where walk :: [SExpr] -> [(String, String)]
    walk []             = []
                     walk [t :: SExpr
    t]            = [SExpr -> SExpr -> (String, String)
    grabAllStat SExpr
    t (String -> SExpr
    ECon "")]
                     walk (t :: SExpr
    t : v :: SExpr
    v : rest :: [SExpr]
    rest) =  SExpr -> SExpr -> (String, String)
    grabAllStat SExpr
    t SExpr
    v          (String, String) -> [(String, String)] -> [(String, String)]
    forall a. a -> [a] -> [a]
    : [SExpr] -> [(String, String)]
    walk [SExpr]
    rest
            grabAllStats o :: SExpr
    o = [SExpr -> SExpr -> (String, String)
    grabAllStat SExpr
    o (String -> SExpr
    ECon "")]

        String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

        String
    -> (String -> Maybe [String] -> m SMTInfoResponse)
    -> (SExpr -> m SMTInfoResponse)
    -> m SMTInfoResponse
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m SMTInfoResponse
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m SMTInfoResponse) -> m SMTInfoResponse)
    -> (SExpr -> m SMTInfoResponse) -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ \pe :: SExpr
    pe ->
           if Bool
    isAllStat
              then SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ [(String, String)] -> SMTInfoResponse
    Resp_AllStatistics ([(String, String)] -> SMTInfoResponse)
    -> [(String, String)] -> SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ SExpr -> [(String, String)]
    grabAllStats SExpr
    pe
              else case SExpr
    pe of
                     ECon "unsupported"                                        -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTInfoResponse
    Resp_Unsupported
                     EApp [ECon ":assertion-stack-levels", ENum (i :: Integer
    i, _)]        -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ Integer -> SMTInfoResponse
    Resp_AssertionStackLevels Integer
    i
                     EApp (ECon ":authors" : ns :: [SExpr]
    ns)                               -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ [String] -> SMTInfoResponse
    Resp_Authors ((SExpr -> String) -> [SExpr] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SExpr -> String
    render [SExpr]
    ns)
                     EApp [ECon ":error-behavior", ECon "immediate-exit"]      -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ SMTErrorBehavior -> SMTInfoResponse
    Resp_Error SMTErrorBehavior
    ErrorImmediateExit
                     EApp [ECon ":error-behavior", ECon "continued-execution"] -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ SMTErrorBehavior -> SMTInfoResponse
    Resp_Error SMTErrorBehavior
    ErrorContinuedExecution
                     EApp (ECon ":name" : o :: [SExpr]
    o)                                   -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ String -> SMTInfoResponse
    Resp_Name (SExpr -> String
    render ([SExpr] -> SExpr
    EApp [SExpr]
    o))
                     EApp (ECon ":reason-unknown" : o :: [SExpr]
    o)                         -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ SMTReasonUnknown -> SMTInfoResponse
    Resp_ReasonUnknown ([SExpr] -> SMTReasonUnknown
    unk [SExpr]
    o)
                     EApp (ECon ":version" : o :: [SExpr]
    o)                                -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ String -> SMTInfoResponse
    Resp_Version (SExpr -> String
    render ([SExpr] -> SExpr
    EApp [SExpr]
    o))
                     EApp (ECon s :: String
    s : o :: [SExpr]
    o)                                         -> SMTInfoResponse -> m SMTInfoResponse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTInfoResponse -> m SMTInfoResponse)
    -> SMTInfoResponse -> m SMTInfoResponse
    forall a b. (a -> b) -> a -> b
    $ String -> [String] -> SMTInfoResponse
    Resp_InfoKeyword String
    s ((SExpr -> String) -> [SExpr] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SExpr -> String
    render [SExpr]
    o)
                     _                                                         -> String -> Maybe [String] -> m SMTInfoResponse
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

      where render :: SExpr -> String
    render = Bool -> SExpr -> String
    serialize Bool
    True

            unk :: [SExpr] -> SMTReasonUnknown
    unk [ECon s :: String
    s] | Just d :: SMTReasonUnknown
    d <- String -> Maybe SMTReasonUnknown
    getUR String
    s = SMTReasonUnknown
    d
            unk o :: [SExpr]
    o                            = String -> SMTReasonUnknown
    UnknownOther (SExpr -> String
    render ([SExpr] -> SExpr
    EApp [SExpr]
    o))

            getUR :: String -> Maybe SMTReasonUnknown
    getUR s :: String
    s = (Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    toLower (String -> String
    unQuote String
    s) String -> [(String, SMTReasonUnknown)] -> Maybe SMTReasonUnknown
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [((Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    toLower String
    k, SMTReasonUnknown
    d) | (k :: String
    k, d :: SMTReasonUnknown
    d) <- [(String, SMTReasonUnknown)]
    unknownReasons]

            -- As specified in Section 4.1 of the SMTLib document. Note that we're adding the
            -- extra timeout as it is useful in this context.
            unknownReasons :: [(String, SMTReasonUnknown)]
    unknownReasons = [ ("memout",     SMTReasonUnknown
    UnknownMemOut)
                             , ("incomplete", SMTReasonUnknown
    UnknownIncomplete)
                             , ("timeout",    SMTReasonUnknown
    UnknownTimeOut)
                             ]

    -- | Generalization of 'Data.SBV.Control.getInfo'
    getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption)
    getOption :: (a -> SMTOption) -> m (Maybe SMTOption)
    getOption f :: a -> SMTOption
    f = case a -> SMTOption
    f a
    forall a. HasCallStack => a
    undefined of
                     DiagnosticOutputChannel{}   -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "DiagnosticOutputChannel"   ":diagnostic-output-channel"   ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (String -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (String -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    string     String -> SMTOption
    DiagnosticOutputChannel
                     ProduceAssertions{}         -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "ProduceAssertions"         ":produce-assertions"          ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Bool -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Bool -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    bool       Bool -> SMTOption
    ProduceAssertions
                     ProduceAssignments{}        -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "ProduceAssignments"        ":produce-assignments"         ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Bool -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Bool -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    bool       Bool -> SMTOption
    ProduceAssignments
                     ProduceProofs{}             -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "ProduceProofs"             ":produce-proofs"              ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Bool -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Bool -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    bool       Bool -> SMTOption
    ProduceProofs
                     ProduceInterpolants{}       -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "ProduceInterpolants"       ":produce-interpolants"        ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Bool -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Bool -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    bool       Bool -> SMTOption
    ProduceInterpolants
                     ProduceUnsatAssumptions{}   -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "ProduceUnsatAssumptions"   ":produce-unsat-assumptions"   ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Bool -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Bool -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    bool       Bool -> SMTOption
    ProduceUnsatAssumptions
                     ProduceUnsatCores{}         -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "ProduceUnsatCores"         ":produce-unsat-cores"         ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Bool -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Bool -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    bool       Bool -> SMTOption
    ProduceUnsatCores
                     RandomSeed{}                -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "RandomSeed"                ":random-seed"                 ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Integer -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    integer    Integer -> SMTOption
    RandomSeed
                     ReproducibleResourceLimit{} -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "ReproducibleResourceLimit" ":reproducible-resource-limit" ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Integer -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    integer    Integer -> SMTOption
    ReproducibleResourceLimit
                     SMTVerbosity{}              -> String
    -> String
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor "SMTVerbosity"              ":verbosity"                   ((SExpr
      -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr
        -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SMTOption)
    -> SExpr
    -> (Maybe [String] -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a.
    Monad m =>
    (Integer -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    integer    Integer -> SMTOption
    SMTVerbosity
                     OptionKeyword nm :: String
    nm _          -> String
    -> String
    -> (SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall (m :: * -> *) a a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor ("OptionKeyword" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm)     String
    nm                             ((SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption))
     -> m (Maybe SMTOption))
    -> (SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption))
    -> m (Maybe SMTOption)
    forall a b. (a -> b) -> a -> b
    $ ([String] -> SMTOption)
    -> SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption)
    forall (m :: * -> *) a p.
    Monad m =>
    ([String] -> a) -> SExpr -> p -> m (Maybe a)
    stringList (String -> [String] -> SMTOption
    OptionKeyword String
    nm)
                     SetLogic{}                  -> String -> m (Maybe SMTOption)
    forall a. HasCallStack => String -> a
    error "Data.SBV.Query: SMTLib does not allow querying value of the logic!"
                     -- Not to be confused by getInfo, which is totally irrelevant!
                     SetInfo{}                   -> String -> m (Maybe SMTOption)
    forall a. HasCallStack => String -> a
    error "Data.SBV.Query: SMTLib does not allow querying value of meta-info!"

      where askFor :: String
    -> String
    -> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
    -> m (Maybe a)
    askFor sbvName :: String
    sbvName smtLibName :: String
    smtLibName continue :: SExpr -> (Maybe [String] -> m a) -> m (Maybe a)
    continue = do
                    let cmd :: String
    cmd = "(get-option " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    smtLibName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                        bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected ("getOption " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    sbvName) String
    cmd "a valid option value" Maybe [String]
    forall a. Maybe a
    Nothing

                    String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

                    String
    -> (String -> Maybe [String] -> m (Maybe a))
    -> (SExpr -> m (Maybe a))
    -> m (Maybe a)
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m (Maybe a)
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m (Maybe a)) -> m (Maybe a))
    -> (SExpr -> m (Maybe a)) -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ \case ECon "unsupported" -> Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
                                        e :: SExpr
    e                  -> SExpr -> (Maybe [String] -> m a) -> m (Maybe a)
    continue SExpr
    e (String -> Maybe [String] -> m a
    forall a. String -> Maybe [String] -> m a
    bad String
    r)

            string :: (String -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    string c :: String -> a
    c (ECon s :: String
    s) _ = Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ String -> a
    c String
    s
            string _ e :: SExpr
    e        k :: Maybe [String] -> m (Maybe a)
    k = Maybe [String] -> m (Maybe a)
    k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just ["Expected string, but got: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show (Bool -> SExpr -> String
    serialize Bool
    False SExpr
    e)]

            bool :: (Bool -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    bool c :: Bool -> a
    c (ENum (0, _)) _ = Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Bool -> a
    c Bool
    False
            bool c :: Bool -> a
    c (ENum (1, _)) _ = Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Bool -> a
    c Bool
    True
            bool _ e :: SExpr
    e             k :: Maybe [String] -> m (Maybe a)
    k = Maybe [String] -> m (Maybe a)
    k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just ["Expected boolean, but got: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show (Bool -> SExpr -> String
    serialize Bool
    False SExpr
    e)]

            integer :: (Integer -> a)
    -> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
    integer c :: Integer -> a
    c (ENum (i :: Integer
    i, _)) _ = Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Integer -> a
    c Integer
    i
            integer _ e :: SExpr
    e             k :: Maybe [String] -> m (Maybe a)
    k = Maybe [String] -> m (Maybe a)
    k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just ["Expected integer, but got: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show (Bool -> SExpr -> String
    serialize Bool
    False SExpr
    e)]

            -- free format, really
            stringList :: ([String] -> a) -> SExpr -> p -> m (Maybe a)
    stringList c :: [String] -> a
    c e :: SExpr
    e _ = Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ [String] -> a
    c ([String] -> a) -> [String] -> a
    forall a b. (a -> b) -> a -> b
    $ SExpr -> [String]
    stringsOf SExpr
    e

    -- | Generalization of 'Data.SBV.Control.getUnknownReason'
    getUnknownReason :: (MonadIO m, MonadQuery m) => m SMTReasonUnknown
    getUnknownReason :: m SMTReasonUnknown
    getUnknownReason = do SMTInfoResponse
    ru <- SMTInfoFlag -> m SMTInfoResponse
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    SMTInfoFlag -> m SMTInfoResponse
    getInfo SMTInfoFlag
    ReasonUnknown
                          case SMTInfoResponse
    ru of
                            Resp_Unsupported     -> SMTReasonUnknown -> m SMTReasonUnknown
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTReasonUnknown -> m SMTReasonUnknown)
    -> SMTReasonUnknown -> m SMTReasonUnknown
    forall a b. (a -> b) -> a -> b
    $ String -> SMTReasonUnknown
    UnknownOther "Solver responded: Unsupported."
                            Resp_ReasonUnknown r :: SMTReasonUnknown
    r -> SMTReasonUnknown -> m SMTReasonUnknown
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTReasonUnknown
    r
                            -- Shouldn't happen, but just in case:
                            _                    -> String -> m SMTReasonUnknown
    forall a. HasCallStack => String -> a
    error (String -> m SMTReasonUnknown) -> String -> m SMTReasonUnknown
    forall a b. (a -> b) -> a -> b
    $ "Unexpected reason value received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTInfoResponse -> String
    forall a. Show a => a -> String
    show SMTInfoResponse
    ru

    -- | Generalization of 'Data.SBV.Control.ensureSat'
    ensureSat :: (MonadIO m, MonadQuery m) => m ()
    ensureSat :: m ()
    ensureSat = do SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
                   CheckSatResult
    cs <- String -> m CheckSatResult
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m CheckSatResult
    checkSatUsing (String -> m CheckSatResult) -> String -> m CheckSatResult
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> String
    satCmd SMTConfig
    cfg
                   case CheckSatResult
    cs of
                     Sat -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                     Unk -> do SMTReasonUnknown
    s <- m SMTReasonUnknown
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m SMTReasonUnknown
    getUnknownReason
                               String -> m ()
    forall a. HasCallStack => String -> a
    error (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                               , "*** Data.SBV.ensureSat: Solver reported Unknown!"
                                               , "*** Reason: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTReasonUnknown -> String
    forall a. Show a => a -> String
    show SMTReasonUnknown
    s
                                               ]
                     Unsat -> String -> m ()
    forall a. HasCallStack => String -> a
    error "Data.SBV.ensureSat: Solver reported Unsat!"

    -- | Generalization of 'Data.SBV.Control.getSMTResult'
    getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult
    getSMTResult :: m SMTResult
    getSMTResult = do SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
                      CheckSatResult
    cs  <- m CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    checkSat
                      case CheckSatResult
    cs of
                        Unsat -> SMTConfig -> Maybe [String] -> SMTResult
    Unsatisfiable SMTConfig
    cfg (Maybe [String] -> SMTResult) -> m (Maybe [String]) -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe [String])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m (Maybe [String])
    getUnsatCoreIfRequested
                        Sat   -> SMTConfig -> SMTModel -> SMTResult
    Satisfiable   SMTConfig
    cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m SMTModel
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
    getModel
                        Unk   -> SMTConfig -> SMTReasonUnknown -> SMTResult
    Unknown       SMTConfig
    cfg (SMTReasonUnknown -> SMTResult)
    -> m SMTReasonUnknown -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m SMTReasonUnknown
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m SMTReasonUnknown
    getUnknownReason

    -- | Classify a model based on whether it has unbound objectives or not.
    classifyModel :: SMTConfig -> SMTModel -> SMTResult
    classifyModel :: SMTConfig -> SMTModel -> SMTResult
    classifyModel cfg :: SMTConfig
    cfg m :: SMTModel
    m
      | ((String, GeneralizedCV) -> Bool)
    -> [(String, GeneralizedCV)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (String, GeneralizedCV) -> Bool
    forall a. (a, GeneralizedCV) -> Bool
    isExt (SMTModel -> [(String, GeneralizedCV)]
    modelObjectives SMTModel
    m) = SMTConfig -> SMTModel -> SMTResult
    SatExtField SMTConfig
    cfg SMTModel
    m
      | Bool
    True                          = SMTConfig -> SMTModel -> SMTResult
    Satisfiable SMTConfig
    cfg SMTModel
    m
      where isExt :: (a, GeneralizedCV) -> Bool
    isExt (_, v :: GeneralizedCV
    v) = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ GeneralizedCV -> Bool
    isRegularCV GeneralizedCV
    v

    -- | Generalization of 'Data.SBV.Control.getLexicographicOptResults'
    getLexicographicOptResults :: (MonadIO m, MonadQuery m) => m SMTResult
    getLexicographicOptResults :: m SMTResult
    getLexicographicOptResults = do SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
                                    CheckSatResult
    cs  <- m CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    checkSat
                                    case CheckSatResult
    cs of
                                      Unsat -> SMTConfig -> Maybe [String] -> SMTResult
    Unsatisfiable SMTConfig
    cfg (Maybe [String] -> SMTResult) -> m (Maybe [String]) -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe [String])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m (Maybe [String])
    getUnsatCoreIfRequested
                                      Sat   -> SMTConfig -> SMTModel -> SMTResult
    classifyModel SMTConfig
    cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m SMTModel
    getModelWithObjectives
                                      Unk   -> SMTConfig -> SMTReasonUnknown -> SMTResult
    Unknown       SMTConfig
    cfg (SMTReasonUnknown -> SMTResult)
    -> m SMTReasonUnknown -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m SMTReasonUnknown
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m SMTReasonUnknown
    getUnknownReason
       where getModelWithObjectives :: m SMTModel
    getModelWithObjectives = do [(String, GeneralizedCV)]
    objectiveValues <- m [(String, GeneralizedCV)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(String, GeneralizedCV)]
    getObjectiveValues
                                         SMTModel
    m               <- m SMTModel
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
    getModel
                                         SMTModel -> m SMTModel
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTModel
    m {modelObjectives :: [(String, GeneralizedCV)]
    modelObjectives = [(String, GeneralizedCV)]
    objectiveValues}

    -- | Generalization of 'Data.SBV.Control.getIndependentOptResults'
    getIndependentOptResults :: forall m. (MonadIO m, MonadQuery m) => [String] -> m [(String, SMTResult)]
    getIndependentOptResults :: [String] -> m [(String, SMTResult)]
    getIndependentOptResults objNames :: [String]
    objNames = do SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
                                           CheckSatResult
    cs  <- m CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    checkSat

                                           case CheckSatResult
    cs of
                                             Unsat -> m (Maybe [String])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m (Maybe [String])
    getUnsatCoreIfRequested m (Maybe [String])
    -> (Maybe [String] -> m [(String, SMTResult)])
    -> m [(String, SMTResult)]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \mbUC :: Maybe [String]
    mbUC -> [(String, SMTResult)] -> m [(String, SMTResult)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(String
    nm, SMTConfig -> Maybe [String] -> SMTResult
    Unsatisfiable SMTConfig
    cfg Maybe [String]
    mbUC) | String
    nm <- [String]
    objNames]
                                             Sat   -> (SMTModel -> SMTResult) -> m [(String, SMTResult)]
    forall b. (SMTModel -> b) -> m [(String, b)]
    continue (SMTConfig -> SMTModel -> SMTResult
    classifyModel SMTConfig
    cfg)
                                             Unk   -> do SMTResult
    ur <- SMTConfig -> SMTReasonUnknown -> SMTResult
    Unknown SMTConfig
    cfg (SMTReasonUnknown -> SMTResult)
    -> m SMTReasonUnknown -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m SMTReasonUnknown
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m SMTReasonUnknown
    getUnknownReason
                                                         [(String, SMTResult)] -> m [(String, SMTResult)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(String
    nm, SMTResult
    ur) | String
    nm <- [String]
    objNames]

      where continue :: (SMTModel -> b) -> m [(String, b)]
    continue classify :: SMTModel -> b
    classify = do [(String, GeneralizedCV)]
    objectiveValues <- m [(String, GeneralizedCV)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(String, GeneralizedCV)]
    getObjectiveValues
                                   [(String, SMTModel)]
    nms <- (Int -> String -> m (String, SMTModel))
    -> [Int] -> [String] -> m [(String, SMTModel)]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Int -> String -> m (String, SMTModel)
    getIndependentResult [0..] [String]
    objNames
                                   [(String, b)] -> m [(String, b)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(String
    n, SMTModel -> b
    classify (SMTModel
    m {modelObjectives :: [(String, GeneralizedCV)]
    modelObjectives = [(String, GeneralizedCV)]
    objectiveValues})) | (n :: String
    n, m :: SMTModel
    m) <- [(String, SMTModel)]
    nms]

            getIndependentResult :: Int -> String -> m (String, SMTModel)
            getIndependentResult :: Int -> String -> m (String, SMTModel)
    getIndependentResult i :: Int
    i s :: String
    s = do SMTModel
    m <- Maybe Int -> m SMTModel
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> m SMTModel
    getModelAtIndex (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i)
                                          (String, SMTModel) -> m (String, SMTModel)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String
    s, SMTModel
    m)

    -- | Generalization of 'Data.SBV.Control.getParetoOptResults'
    getParetoOptResults :: (MonadIO m, MonadQuery m) => Maybe Int -> m (Bool, [SMTResult])
    getParetoOptResults :: Maybe Int -> m (Bool, [SMTResult])
    getParetoOptResults (Just i :: Int
    i)
            | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0             = (Bool, [SMTResult]) -> m (Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    True, [])
    getParetoOptResults mbN :: Maybe Int
    mbN      = do SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
                                      CheckSatResult
    cs  <- m CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    checkSat

                                      case CheckSatResult
    cs of
                                        Unsat -> (Bool, [SMTResult]) -> m (Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, [])
                                        Sat   -> (SMTModel -> SMTResult) -> m (Bool, [SMTResult])
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (SMTModel -> a) -> m (Bool, [a])
    continue (SMTConfig -> SMTModel -> SMTResult
    classifyModel SMTConfig
    cfg)
                                        Unk   -> do SMTReasonUnknown
    ur <- m SMTReasonUnknown
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m SMTReasonUnknown
    getUnknownReason
                                                    (Bool, [SMTResult]) -> m (Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, [SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
    ProofError SMTConfig
    cfg [SMTReasonUnknown -> String
    forall a. Show a => a -> String
    show SMTReasonUnknown
    ur] Maybe SMTResult
    forall a. Maybe a
    Nothing])

      where continue :: (SMTModel -> a) -> m (Bool, [a])
    continue classify :: SMTModel -> a
    classify = do SMTModel
    m <- m SMTModel
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
    getModel
                                   (limReached :: Bool
    limReached, fronts :: [SMTModel]
    fronts) <- Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
    getParetoFronts (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    subtract 1 (Int -> Int) -> Maybe Int -> Maybe Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Int
    mbN) [SMTModel
    m]
                                   (Bool, [a]) -> m (Bool, [a])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    limReached, [a] -> [a]
    forall a. [a] -> [a]
    reverse ((SMTModel -> a) -> [SMTModel] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map SMTModel -> a
    classify [SMTModel]
    fronts))

            getParetoFronts :: (MonadIO m, MonadQuery m) => Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
            getParetoFronts :: Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
    getParetoFronts (Just i :: Int
    i) sofar :: [SMTModel]
    sofar | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0 = (Bool, [SMTModel]) -> m (Bool, [SMTModel])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    True, [SMTModel]
    sofar)
            getParetoFronts mbi :: Maybe Int
    mbi      sofar :: [SMTModel]
    sofar          = do CheckSatResult
    cs <- m CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    checkSat
                                                         let more :: m (Bool, [SMTModel])
    more = m SMTModel
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
    getModel m SMTModel
    -> (SMTModel -> m (Bool, [SMTModel])) -> m (Bool, [SMTModel])
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \m :: SMTModel
    m -> Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
    getParetoFronts (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    subtract 1 (Int -> Int) -> Maybe Int -> Maybe Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Int
    mbi) (SMTModel
    m SMTModel -> [SMTModel] -> [SMTModel]
    forall a. a -> [a] -> [a]
    : [SMTModel]
    sofar)
                                                         case CheckSatResult
    cs of
                                                           Unsat -> (Bool, [SMTModel]) -> m (Bool, [SMTModel])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, [SMTModel]
    sofar)
                                                           Sat   -> m (Bool, [SMTModel])
    more
                                                           Unk   -> m (Bool, [SMTModel])
    more

    -- | Generalization of 'Data.SBV.Control.getModel'
    getModel :: (MonadIO m, MonadQuery m) => m SMTModel
    getModel :: m SMTModel
    getModel = Maybe Int -> m SMTModel
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> m SMTModel
    getModelAtIndex Maybe Int
    forall a. Maybe a
    Nothing

    -- | Get a model stored at an index. This is likely very Z3 specific!
    getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel
    getModelAtIndex :: Maybe Int -> m SMTModel
    getModelAtIndex mbi :: Maybe Int
    mbi = do
        State{IORef SBVRunMode
    runMode :: State -> IORef SBVRunMode
    runMode :: IORef SBVRunMode
    runMode} <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
        SBVRunMode
    rm     <- IO SBVRunMode -> m SBVRunMode
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO SBVRunMode -> m SBVRunMode) -> IO SBVRunMode -> m SBVRunMode
    forall a b. (a -> b) -> a -> b
    $ IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef IORef SBVRunMode
    runMode
        case SBVRunMode
    rm of
          m :: SBVRunMode
    m@SBVRunMode
    CodeGen           -> String -> m SMTModel
    forall a. HasCallStack => String -> a
    error (String -> m SMTModel) -> String -> m SMTModel
    forall a b. (a -> b) -> a -> b
    $ "SBV.getModel: Model is not available in mode: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVRunMode -> String
    forall a. Show a => a -> String
    show SBVRunMode
    m
          m :: SBVRunMode
    m@Concrete{}        -> String -> m SMTModel
    forall a. HasCallStack => String -> a
    error (String -> m SMTModel) -> String -> m SMTModel
    forall a b. (a -> b) -> a -> b
    $ "SBV.getModel: Model is not available in mode: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVRunMode -> String
    forall a. Show a => a -> String
    show SBVRunMode
    m
          SMTMode _ _ isSAT :: Bool
    isSAT _ -> do
              SMTConfig
    cfg   <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
              [(Quantifier, NamedSymVar)]
    qinps <- m [(Quantifier, NamedSymVar)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(Quantifier, NamedSymVar)]
    getQuantifiedInputs
              [(String, SBVType)]
    uis   <- m [(String, SBVType)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(String, SBVType)]
    getUIs

               -- for "sat", display the prefix existentials. for "proof", display the prefix universals
              let allModelInputs :: [(Quantifier, NamedSymVar)]
    allModelInputs = if Bool
    isSAT then ((Quantifier, NamedSymVar) -> Bool)
    -> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile ((Quantifier -> Quantifier -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Quantifier
    ALL) (Quantifier -> Bool)
    -> ((Quantifier, NamedSymVar) -> Quantifier)
    -> (Quantifier, NamedSymVar)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Quantifier, NamedSymVar) -> Quantifier
    forall a b. (a, b) -> a
    fst) [(Quantifier, NamedSymVar)]
    qinps
                                            else ((Quantifier, NamedSymVar) -> Bool)
    -> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile ((Quantifier -> Quantifier -> Bool
    forall a. Eq a => a -> a -> Bool
    == Quantifier
    ALL) (Quantifier -> Bool)
    -> ((Quantifier, NamedSymVar) -> Quantifier)
    -> (Quantifier, NamedSymVar)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Quantifier, NamedSymVar) -> Quantifier
    forall a b. (a, b) -> a
    fst) [(Quantifier, NamedSymVar)]
    qinps

                  -- Add on observables only if we're not in a quantified context
                  grabObservables :: Bool
    grabObservables = [(Quantifier, NamedSymVar)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Quantifier, NamedSymVar)]
    allModelInputs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [(Quantifier, NamedSymVar)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Quantifier, NamedSymVar)]
    qinps -- i.e., we didn't drop anything

              [(String, CV)]
    obsvs <- if Bool
    grabObservables
                          then m [(String, CV)]
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(String, CV)]
    getObservables
                          else do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["*** In a quantified context, obvservables will not be printed."]
                                  [(String, CV)] -> m [(String, CV)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

              let sortByNodeId :: [(SV, (String, CV))] -> [(String, CV)]
                  sortByNodeId :: [(SV, (String, CV))] -> [(String, CV)]
    sortByNodeId = ((SV, (String, CV)) -> (String, CV))
    -> [(SV, (String, CV))] -> [(String, CV)]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, (String, CV)) -> (String, CV)
    forall a b. (a, b) -> b
    snd ([(SV, (String, CV))] -> [(String, CV)])
    -> ([(SV, (String, CV))] -> [(SV, (String, CV))])
    -> [(SV, (String, CV))]
    -> [(String, CV)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((SV, (String, CV)) -> (SV, (String, CV)) -> Ordering)
    -> [(SV, (String, CV))] -> [(SV, (String, CV))]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (NodeId -> NodeId -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (NodeId -> NodeId -> Ordering)
    -> ((SV, (String, CV)) -> NodeId)
    -> (SV, (String, CV))
    -> (SV, (String, CV))
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (\(SV _ nid :: NodeId
    nid, _) -> NodeId
    nid))

                  grab :: (SV, b) -> f (SV, (b, CV))
    grab (sv :: SV
    sv, nm :: b
    nm) = CV -> (SV, (b, CV))
    forall b. b -> (SV, (b, b))
    wrap (CV -> (SV, (b, CV))) -> f CV -> f (SV, (b, CV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Int -> SV -> f CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> SV -> m CV
    getValueCV Maybe Int
    mbi SV
    sv
                     where wrap :: b -> (SV, (b, b))
    wrap c :: b
    c = (SV
    sv, (b
    nm, b
    c))

              [(SV, (String, CV))]
    inputAssocs <- ((Quantifier, NamedSymVar) -> m (SV, (String, CV)))
    -> [(Quantifier, NamedSymVar)] -> m [(SV, (String, CV))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (NamedSymVar -> m (SV, (String, CV))
    forall (f :: * -> *) b.
    (MonadIO f, MonadQuery f) =>
    (SV, b) -> f (SV, (b, CV))
    grab (NamedSymVar -> m (SV, (String, CV)))
    -> ((Quantifier, NamedSymVar) -> NamedSymVar)
    -> (Quantifier, NamedSymVar)
    -> m (SV, (String, CV))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Quantifier, NamedSymVar) -> NamedSymVar
    forall a b. (a, b) -> b
    snd) [(Quantifier, NamedSymVar)]
    allModelInputs

              let assocs :: [(String, CV)]
    assocs =  ((String, CV) -> String) -> [(String, CV)] -> [(String, CV)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    sortOn (String, CV) -> String
    forall a b. (a, b) -> a
    fst [(String, CV)]
    obsvs
                         [(String, CV)] -> [(String, CV)] -> [(String, CV)]
    forall a. [a] -> [a] -> [a]
    ++ [(SV, (String, CV))] -> [(String, CV)]
    sortByNodeId [(SV, (String, CV))
    p | p :: (SV, (String, CV))
    p@(_, (nm :: String
    nm, _)) <- [(SV, (String, CV))]
    inputAssocs, Bool -> Bool
    not (SMTConfig -> String -> Bool
    isNonModelVar SMTConfig
    cfg String
    nm)]

              -- collect UIs if requested
              let uiFuns :: [(String, SBVType)]
    uiFuns = [(String, SBVType)
    ui | ui :: (String, SBVType)
    ui@(_, SBVType as :: [Kind]
    as) <- [(String, SBVType)]
    uis, [Kind] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    as Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1, SMTConfig -> Bool
    satTrackUFs SMTConfig
    cfg] -- functions have at least two things in their type!

              -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out
              -- as cex's tend to get larger
              Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([(String, SBVType)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, SBVType)]
    uiFuns) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                 let solverCaps :: SolverCapabilities
    solverCaps = SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)
                 in case SolverCapabilities -> Maybe [String]
    supportsFlattenedModels SolverCapabilities
    solverCaps of
                      Nothing   -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                      Just cmds :: [String]
    cmds -> (String -> m ()) -> [String] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True) [String]
    cmds

              Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    bindings <- let get :: (Quantifier, (SV, b)) -> m ((Quantifier, (SV, b)), Maybe CV)
    get i :: (Quantifier, (SV, b))
    i@(ALL, _)      = ((Quantifier, (SV, b)), Maybe CV)
    -> m ((Quantifier, (SV, b)), Maybe CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Quantifier, (SV, b))
    i, Maybe CV
    forall a. Maybe a
    Nothing)
                              get i :: (Quantifier, (SV, b))
    i@(EX, (sv :: SV
    sv, _)) = case SV
    sv SV -> [(SV, (String, CV))] -> Maybe (String, CV)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, (String, CV))]
    inputAssocs of
                                                      Just (_, cv :: CV
    cv) -> ((Quantifier, (SV, b)), Maybe CV)
    -> m ((Quantifier, (SV, b)), Maybe CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Quantifier, (SV, b))
    i, CV -> Maybe CV
    forall a. a -> Maybe a
    Just CV
    cv)
                                                      Nothing      -> do CV
    cv <- Maybe Int -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> SV -> m CV
    getValueCV Maybe Int
    mbi SV
    sv
                                                                         ((Quantifier, (SV, b)), Maybe CV)
    -> m ((Quantifier, (SV, b)), Maybe CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Quantifier, (SV, b))
    i, CV -> Maybe CV
    forall a. a -> Maybe a
    Just CV
    cv)

                              flipQ :: (Quantifier, b) -> (Quantifier, b)
    flipQ i :: (Quantifier, b)
    i@(q :: Quantifier
    q, sv :: b
    sv) = case (Bool
    isSAT, Quantifier
    q) of
                                                 (True,  _ )  -> (Quantifier, b)
    i
                                                 (False, EX)  -> (Quantifier
    ALL, b
    sv)
                                                 (False, ALL) -> (Quantifier
    EX,  b
    sv)

                          in if SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                             then [((Quantifier, NamedSymVar), Maybe CV)]
    -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    forall a. a -> Maybe a
    Just ([((Quantifier, NamedSymVar), Maybe CV)]
     -> Maybe [((Quantifier, NamedSymVar), Maybe CV)])
    -> m [((Quantifier, NamedSymVar), Maybe CV)]
    -> m (Maybe [((Quantifier, NamedSymVar), Maybe CV)])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Quantifier, NamedSymVar)
     -> m ((Quantifier, NamedSymVar), Maybe CV))
    -> [(Quantifier, NamedSymVar)]
    -> m [((Quantifier, NamedSymVar), Maybe CV)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Quantifier, NamedSymVar)
    -> m ((Quantifier, NamedSymVar), Maybe CV)
    forall (m :: * -> *) b.
    (MonadIO m, MonadQuery m) =>
    (Quantifier, (SV, b)) -> m ((Quantifier, (SV, b)), Maybe CV)
    get ((Quantifier, NamedSymVar)
     -> m ((Quantifier, NamedSymVar), Maybe CV))
    -> ((Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar))
    -> (Quantifier, NamedSymVar)
    -> m ((Quantifier, NamedSymVar), Maybe CV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar)
    forall b. (Quantifier, b) -> (Quantifier, b)
    flipQ) [(Quantifier, NamedSymVar)]
    qinps
                             else Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    -> m (Maybe [((Quantifier, NamedSymVar), Maybe CV)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    forall a. Maybe a
    Nothing

              [(String, (SBVType, ([([CV], CV)], CV)))]
    uivs <- ((String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV))))
    -> [(String, SBVType)]
    -> m [(String, (SBVType, ([([CV], CV)], CV)))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (\ui :: (String, SBVType)
    ui@(nm :: String
    nm, t :: SBVType
    t) -> (\a :: ([([CV], CV)], CV)
    a -> (String
    nm, (SBVType
    t, ([([CV], CV)], CV)
    a))) (([([CV], CV)], CV) -> (String, (SBVType, ([([CV], CV)], CV))))
    -> m ([([CV], CV)], CV)
    -> m (String, (SBVType, ([([CV], CV)], CV)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
    getUIFunCVAssoc Maybe Int
    mbi (String, SBVType)
    ui) [(String, SBVType)]
    uiFuns

              SMTModel -> m SMTModel
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTModel :: [(String, GeneralizedCV)]
    -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    -> [(String, CV)]
    -> [(String, (SBVType, ([([CV], CV)], CV)))]
    -> SMTModel
    SMTModel { modelObjectives :: [(String, GeneralizedCV)]
    modelObjectives = []
                              , modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    modelBindings   = Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    bindings
                              , modelAssocs :: [(String, CV)]
    modelAssocs     = [(String, CV)]
    assocs
                              , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
    modelUIFuns     = [(String, (SBVType, ([([CV], CV)], CV)))]
    uivs
                              }

    -- | Just after a check-sat is issued, collect objective values. Used
    -- internally only, not exposed to the user.
    getObjectiveValues :: forall m. (MonadIO m, MonadQuery m) => m [(String, GeneralizedCV)]
    getObjectiveValues :: m [(String, GeneralizedCV)]
    getObjectiveValues = do let cmd :: String
    cmd = "(get-objectives)"

                                bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getObjectiveValues" String
    cmd "a list of objective values" Maybe [String]
    forall a. Maybe a
    Nothing

                            String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

                            [NamedSymVar]
    inputs <- ((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)] -> [NamedSymVar])
    -> m [(Quantifier, NamedSymVar)] -> m [NamedSymVar]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [(Quantifier, NamedSymVar)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(Quantifier, NamedSymVar)]
    getQuantifiedInputs

                            String
    -> (String -> Maybe [String] -> m [(String, GeneralizedCV)])
    -> (SExpr -> m [(String, GeneralizedCV)])
    -> m [(String, GeneralizedCV)]
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m [(String, GeneralizedCV)]
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m [(String, GeneralizedCV)])
     -> m [(String, GeneralizedCV)])
    -> (SExpr -> m [(String, GeneralizedCV)])
    -> m [(String, GeneralizedCV)]
    forall a b. (a -> b) -> a -> b
    $ \case EApp (ECon "objectives" : es :: [SExpr]
    es) -> [Maybe (String, GeneralizedCV)] -> [(String, GeneralizedCV)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (String, GeneralizedCV)] -> [(String, GeneralizedCV)])
    -> m [Maybe (String, GeneralizedCV)] -> m [(String, GeneralizedCV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (SExpr -> m (Maybe (String, GeneralizedCV)))
    -> [SExpr] -> m [Maybe (String, GeneralizedCV)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((forall a. Maybe [String] -> m a)
    -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
    getObjValue (String -> Maybe [String] -> m a
    forall a. String -> Maybe [String] -> m a
    bad String
    r) [NamedSymVar]
    inputs) [SExpr]
    es
                                                _                             -> String -> Maybe [String] -> m [(String, GeneralizedCV)]
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

      where -- | Parse an objective value out.
            getObjValue :: (forall a. Maybe [String] -> m a) -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
            getObjValue :: (forall a. Maybe [String] -> m a)
    -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
    getObjValue bailOut :: forall a. Maybe [String] -> m a
    bailOut inputs :: [NamedSymVar]
    inputs expr :: SExpr
    expr =
                    case SExpr
    expr of
                      EApp [_]          -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (String, GeneralizedCV)
    forall a. Maybe a
    Nothing            -- Happens when a soft-assertion has no associated group.
                      EApp [ECon nm :: String
    nm, v :: SExpr
    v] -> String -> SExpr -> m (Maybe (String, GeneralizedCV))
    locate String
    nm SExpr
    v               -- Regular case
                      _                 -> String -> m (Maybe (String, GeneralizedCV))
    forall a. String -> m a
    dontUnderstand (SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    expr)

              where locate :: String -> SExpr -> m (Maybe (String, GeneralizedCV))
    locate nm :: String
    nm v :: SExpr
    v = case [NamedSymVar] -> Maybe NamedSymVar
    forall a. [a] -> Maybe a
    listToMaybe [NamedSymVar
    p | p :: NamedSymVar
    p@(sv :: SV
    sv, _) <- [NamedSymVar]
    inputs, SV -> String
    forall a. Show a => a -> String
    show SV
    sv String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm] of
                                    Nothing               -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (String, GeneralizedCV)
    forall a. Maybe a
    Nothing -- Happens when the soft assertion has a group-id that's not one of the input names
                                    Just (sv :: SV
    sv, actualName :: String
    actualName) -> SV -> SExpr -> m GeneralizedCV
    grab SV
    sv SExpr
    v m GeneralizedCV
    -> (GeneralizedCV -> m (Maybe (String, GeneralizedCV)))
    -> m (Maybe (String, GeneralizedCV))
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \val :: GeneralizedCV
    val -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (String, GeneralizedCV)
     -> m (Maybe (String, GeneralizedCV)))
    -> Maybe (String, GeneralizedCV)
    -> m (Maybe (String, GeneralizedCV))
    forall a b. (a -> b) -> a -> b
    $ (String, GeneralizedCV) -> Maybe (String, GeneralizedCV)
    forall a. a -> Maybe a
    Just (String
    actualName, GeneralizedCV
    val)

                    dontUnderstand :: String -> m a
    dontUnderstand s :: String
    s = Maybe [String] -> m a
    forall a. Maybe [String] -> m a
    bailOut (Maybe [String] -> m a) -> Maybe [String] -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [ "Unable to understand solver output."
                                                      , "While trying to process: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
                                                      ]

                    grab :: SV -> SExpr -> m GeneralizedCV
                    grab :: SV -> SExpr -> m GeneralizedCV
    grab s :: SV
    s topExpr :: SExpr
    topExpr
                      | Just v :: CV
    v <- Kind -> SExpr -> Maybe CV
    recoverKindedValue Kind
    k SExpr
    topExpr = GeneralizedCV -> m GeneralizedCV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GeneralizedCV -> m GeneralizedCV)
    -> GeneralizedCV -> m GeneralizedCV
    forall a b. (a -> b) -> a -> b
    $ CV -> GeneralizedCV
    RegularCV CV
    v
                      | Bool
    True                                   = ExtCV -> GeneralizedCV
    ExtendedCV (ExtCV -> GeneralizedCV) -> m ExtCV -> m GeneralizedCV
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> m ExtCV
    cvt (SExpr -> SExpr
    simplify SExpr
    topExpr)
                      where k :: Kind
    k = SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s

                            -- Convert to an extended expression. Hopefully complete!
                            cvt :: SExpr -> m ExtCV
                            cvt :: SExpr -> m ExtCV
    cvt (ECon "oo")                    = ExtCV -> m ExtCV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
    forall a b. (a -> b) -> a -> b
    $ Kind -> ExtCV
    Infinite  Kind
    k
                            cvt (ECon "epsilon")               = ExtCV -> m ExtCV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
    forall a b. (a -> b) -> a -> b
    $ Kind -> ExtCV
    Epsilon   Kind
    k
                            cvt (EApp [ECon "interval", x :: SExpr
    x, y :: SExpr
    y]) =          ExtCV -> ExtCV -> ExtCV
    Interval  (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> m ExtCV
    cvt SExpr
    x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> m ExtCV
    cvt SExpr
    y
                            cvt (ENum    (i :: Integer
    i, _))               = ExtCV -> m ExtCV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
    forall a b. (a -> b) -> a -> b
    $ CV -> ExtCV
    BoundedCV (CV -> ExtCV) -> CV -> ExtCV
    forall a b. (a -> b) -> a -> b
    $ Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k Integer
    i
                            cvt (EReal   r :: AlgReal
    r)                    = ExtCV -> m ExtCV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
    forall a b. (a -> b) -> a -> b
    $ CV -> ExtCV
    BoundedCV (CV -> ExtCV) -> CV -> ExtCV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> CVal
    CAlgReal AlgReal
    r
                            cvt (EFloat  f :: Float
    f)                    = ExtCV -> m ExtCV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
    forall a b. (a -> b) -> a -> b
    $ CV -> ExtCV
    BoundedCV (CV -> ExtCV) -> CV -> ExtCV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ Float -> CVal
    CFloat   Float
    f
                            cvt (EDouble d :: Double
    d)                    = ExtCV -> m ExtCV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
    forall a b. (a -> b) -> a -> b
    $ CV -> ExtCV
    BoundedCV (CV -> ExtCV) -> CV -> ExtCV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ Double -> CVal
    CDouble  Double
    d
                            cvt (EApp [ECon "+", x :: SExpr
    x, y :: SExpr
    y])        =          ExtCV -> ExtCV -> ExtCV
    AddExtCV (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> m ExtCV
    cvt SExpr
    x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> m ExtCV
    cvt SExpr
    y
                            cvt (EApp [ECon "*", x :: SExpr
    x, y :: SExpr
    y])        =          ExtCV -> ExtCV -> ExtCV
    MulExtCV (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> m ExtCV
    cvt SExpr
    x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> m ExtCV
    cvt SExpr
    y
                            -- Nothing else should show up, hopefully!
                            cvt e :: SExpr
    e = String -> m ExtCV
    forall a. String -> m a
    dontUnderstand (SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    e)

                            -- drop the pesky to_real's that Z3 produces.. Cool but useless.
                            simplify :: SExpr -> SExpr
                            simplify :: SExpr -> SExpr
    simplify (EApp [ECon "to_real", n :: SExpr
    n]) = SExpr
    n
                            simplify (EApp xs :: [SExpr]
    xs)                  = [SExpr] -> SExpr
    EApp ((SExpr -> SExpr) -> [SExpr] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map SExpr -> SExpr
    simplify [SExpr]
    xs)
                            simplify e :: SExpr
    e                          = SExpr
    e

    -- | Generalization of 'Data.SBV.Control.checkSatAssuming'
    checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult
    checkSatAssuming :: [SBool] -> m CheckSatResult
    checkSatAssuming sBools :: [SBool]
    sBools = (CheckSatResult, Maybe [SBool]) -> CheckSatResult
    forall a b. (a, b) -> a
    fst ((CheckSatResult, Maybe [SBool]) -> CheckSatResult)
    -> m (CheckSatResult, Maybe [SBool]) -> m CheckSatResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
    checkSatAssumingHelper Bool
    False [SBool]
    sBools

    -- | Generalization of 'Data.SBV.Control.checkSatAssumingWithUnsatisfiableSet'
    checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])
    checkSatAssumingWithUnsatisfiableSet :: [SBool] -> m (CheckSatResult, Maybe [SBool])
    checkSatAssumingWithUnsatisfiableSet = Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
    checkSatAssumingHelper Bool
    True

    -- | Helper for the two variants of checkSatAssuming we have. Internal only.
    checkSatAssumingHelper :: (MonadIO m, MonadQuery m) => Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
    checkSatAssumingHelper :: Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
    checkSatAssumingHelper getAssumptions :: Bool
    getAssumptions sBools :: [SBool]
    sBools = do
            -- sigh.. SMT-Lib requires the values to be literals only. So, create proxies.
            let mkAssumption :: State -> IO [(String, [String], (String, SBool))]
    mkAssumption st :: State
    st = do [(SV, SBool)]
    swsOriginal <- (SBool -> IO (SV, SBool)) -> [SBool] -> IO [(SV, SBool)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (\sb :: SBool
    sb -> do SV
    sv <- State -> SBool -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBool
    sb
                                                                    (SV, SBool) -> IO (SV, SBool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV
    sv, SBool
    sb)) [SBool]
    sBools

                                     -- drop duplicates and trues
                                     let swbs :: [(SV, SBool)]
    swbs = [(SV, SBool)
    p | p :: (SV, SBool)
    p@(sv :: SV
    sv, _) <- ((SV, SBool) -> (SV, SBool) -> Bool)
    -> [(SV, SBool)] -> [(SV, SBool)]
    forall a. (a -> a -> Bool) -> [a] -> [a]
    nubBy (SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (SV -> SV -> Bool)
    -> ((SV, SBool) -> SV) -> (SV, SBool) -> (SV, SBool) -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (SV, SBool) -> SV
    forall a b. (a, b) -> a
    fst) [(SV, SBool)]
    swsOriginal, SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    /= SV
    trueSV]

                                     -- get a unique proxy name for each
                                     [(SV, (Int, SBool))]
    uniqueSWBs <- ((SV, SBool) -> IO (SV, (Int, SBool)))
    -> [(SV, SBool)] -> IO [(SV, (Int, SBool))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (\(sv :: SV
    sv, sb :: SBool
    sb) -> do Int
    unique <- State -> IO Int
    incrementInternalCounter State
    st
                                                                         (SV, (Int, SBool)) -> IO (SV, (Int, SBool))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV
    sv, (Int
    unique, SBool
    sb))) [(SV, SBool)]
    swbs

                                     let translate :: (a, (a, b)) -> (String, [String], (String, b))
    translate (sv :: a
    sv, (unique :: a
    unique, sb :: b
    sb)) = (String
    nm, [String]
    decls, (String
    proxy, b
    sb))
                                            where nm :: String
    nm    = a -> String
    forall a. Show a => a -> String
    show a
    sv
                                                  proxy :: String
    proxy = "__assumption_proxy_" 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]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    unique
                                                  decls :: [String]
    decls = [ "(declare-const " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    proxy String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " Bool)"
                                                          , "(assert (= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    proxy String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                                                          ]

                                     [(String, [String], (String, SBool))]
    -> IO [(String, [String], (String, SBool))]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(String, [String], (String, SBool))]
     -> IO [(String, [String], (String, SBool))])
    -> [(String, [String], (String, SBool))]
    -> IO [(String, [String], (String, SBool))]
    forall a b. (a -> b) -> a -> b
    $ ((SV, (Int, SBool)) -> (String, [String], (String, SBool)))
    -> [(SV, (Int, SBool))] -> [(String, [String], (String, SBool))]
    forall a b. (a -> b) -> [a] -> [b]
    map (SV, (Int, SBool)) -> (String, [String], (String, SBool))
    forall a a b.
    (Show a, Show a) =>
    (a, (a, b)) -> (String, [String], (String, b))
    translate [(SV, (Int, SBool))]
    uniqueSWBs

            [(String, [String], (String, SBool))]
    assumptions <- (State -> IO [(String, [String], (String, SBool))])
    -> m [(String, [String], (String, SBool))]
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (State -> IO a) -> m a
    inNewContext State -> IO [(String, [String], (String, SBool))]
    mkAssumption

            let (origNames :: [String]
    origNames, declss :: [[String]]
    declss, proxyMap :: [(String, SBool)]
    proxyMap) = [(String, [String], (String, SBool))]
    -> ([String], [[String]], [(String, SBool)])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 [(String, [String], (String, SBool))]
    assumptions

            let cmd :: String
    cmd = "(check-sat-assuming (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords (((String, SBool) -> String) -> [(String, SBool)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, SBool) -> String
    forall a b. (a, b) -> a
    fst [(String, SBool)]
    proxyMap) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "checkSatAssuming" String
    cmd "one of sat/unsat/unknown"
                               (Maybe [String] -> String -> Maybe [String] -> m a)
    -> Maybe [String] -> String -> Maybe [String] -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [ "Make sure you use:"
                                      , ""
                                      , "       setOption $ ProduceUnsatAssumptions True"
                                      , ""
                                      , "to tell the solver to produce unsat assumptions."
                                      ]

            (String -> m ()) -> [String] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True) ([String] -> m ()) -> [String] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    declss
            String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

            let grabUnsat :: m (CheckSatResult, Maybe [SBool])
    grabUnsat
                 | Bool
    getAssumptions = do [SBool]
    as <- [String] -> [(String, SBool)] -> m [SBool]
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    [String] -> [(String, a)] -> m [a]
    getUnsatAssumptions [String]
    origNames [(String, SBool)]
    proxyMap
                                       (CheckSatResult, Maybe [SBool])
    -> m (CheckSatResult, Maybe [SBool])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CheckSatResult
    Unsat, [SBool] -> Maybe [SBool]
    forall a. a -> Maybe a
    Just [SBool]
    as)
                 | Bool
    True           = (CheckSatResult, Maybe [SBool])
    -> m (CheckSatResult, Maybe [SBool])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CheckSatResult
    Unsat, Maybe [SBool]
    forall a. Maybe a
    Nothing)

            String
    -> (String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool]))
    -> (SExpr -> m (CheckSatResult, Maybe [SBool]))
    -> m (CheckSatResult, Maybe [SBool])
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool])
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m (CheckSatResult, Maybe [SBool]))
     -> m (CheckSatResult, Maybe [SBool]))
    -> (SExpr -> m (CheckSatResult, Maybe [SBool]))
    -> m (CheckSatResult, Maybe [SBool])
    forall a b. (a -> b) -> a -> b
    $ \case ECon "sat"     -> (CheckSatResult, Maybe [SBool])
    -> m (CheckSatResult, Maybe [SBool])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CheckSatResult
    Sat, Maybe [SBool]
    forall a. Maybe a
    Nothing)
                                ECon "unsat"   -> m (CheckSatResult, Maybe [SBool])
    grabUnsat
                                ECon "unknown" -> (CheckSatResult, Maybe [SBool])
    -> m (CheckSatResult, Maybe [SBool])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CheckSatResult
    Unk, Maybe [SBool]
    forall a. Maybe a
    Nothing)
                                _              -> String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool])
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

    -- | Generalization of 'Data.SBV.Control.getAssertionStackDepth'
    getAssertionStackDepth :: (MonadIO m, MonadQuery m) => m Int
    getAssertionStackDepth :: m Int
    getAssertionStackDepth = QueryState -> Int
    queryAssertionStackDepth (QueryState -> Int) -> m QueryState -> m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState

    -- | Upon a pop, we need to restore all arrays and tables. See: http://github.com/LeventErkok/sbv/issues/374
    restoreTablesAndArrays :: (MonadIO m, MonadQuery m) => m ()
    restoreTablesAndArrays :: m ()
    restoreTablesAndArrays = do State
    st <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState

                                Int
    tCount <- Map (Kind, Kind, [SV]) Int -> Int
    forall k a. Map k a -> Int
    M.size  (Map (Kind, Kind, [SV]) Int -> Int)
    -> m (Map (Kind, Kind, [SV]) Int) -> m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (IO (Map (Kind, Kind, [SV]) Int) -> m (Map (Kind, Kind, [SV]) Int)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO (Map (Kind, Kind, [SV]) Int) -> m (Map (Kind, Kind, [SV]) Int))
    -> (IORef (Map (Kind, Kind, [SV]) Int)
        -> IO (Map (Kind, Kind, [SV]) Int))
    -> IORef (Map (Kind, Kind, [SV]) Int)
    -> m (Map (Kind, Kind, [SV]) Int)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IORef (Map (Kind, Kind, [SV]) Int)
    -> IO (Map (Kind, Kind, [SV]) Int)
    forall a. IORef a -> IO a
    readIORef) (State -> IORef (Map (Kind, Kind, [SV]) Int)
    rtblMap   State
    st)
                                Int
    aCount <- IntMap ArrayInfo -> Int
    forall a. IntMap a -> Int
    IM.size (IntMap ArrayInfo -> Int) -> m (IntMap ArrayInfo) -> m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (IO (IntMap ArrayInfo) -> m (IntMap ArrayInfo)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO (IntMap ArrayInfo) -> m (IntMap ArrayInfo))
    -> (IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo))
    -> IORef (IntMap ArrayInfo)
    -> m (IntMap ArrayInfo)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo)
    forall a. IORef a -> IO a
    readIORef) (State -> IORef (IntMap ArrayInfo)
    rArrayMap State
    st)

                                let tInits :: [String]
    tInits = [ "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" | Int
    i <- [0 .. Int
    tCount Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]]
                                    aInits :: [String]
    aInits = [ "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" | Int
    i <- [0 .. Int
    aCount Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1]]
                                    inits :: [String]
    inits  = [String]
    tInits [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    aInits

                                case [String]
    inits of
                                  []  -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()   -- Nothing to do
                                  [x :: String
    x] -> Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                  xs :: [String]
    xs  -> Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "(assert (and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"

    -- | Generalization of 'Data.SBV.Control.inNewAssertionStack'
    inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a
    inNewAssertionStack :: m a -> m a
    inNewAssertionStack q :: m a
    q = do Int -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
    push 1
                               a
    r <- m a
    q
                               Int -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
    pop 1
                               a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r

    -- | Generalization of 'Data.SBV.Control.push'
    push :: (MonadIO m, MonadQuery m) => Int -> m ()
    push :: Int -> m ()
    push i :: Int
    i
     | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0 = String -> m ()
    forall a. HasCallStack => String -> a
    error (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: push requires a strictly positive level argument, received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
     | Bool
    True   = do Int
    depth <- m Int
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
    getAssertionStackDepth
                   Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "(push " 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]
    ++ ")"
                   (QueryState -> QueryState) -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    (QueryState -> QueryState) -> m ()
    modifyQueryState ((QueryState -> QueryState) -> m ())
    -> (QueryState -> QueryState) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \s :: QueryState
    s -> QueryState
    s{queryAssertionStackDepth :: Int
    queryAssertionStackDepth = Int
    depth Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    i}

    -- | Generalization of 'Data.SBV.Control.pop'
    pop :: (MonadIO m, MonadQuery m) => Int -> m ()
    pop :: Int -> m ()
    pop i :: Int
    i
     | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0 = String -> m ()
    forall a. HasCallStack => String -> a
    error (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: pop requires a strictly positive level argument, received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
     | Bool
    True   = do Int
    depth <- m Int
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
    getAssertionStackDepth
                   if Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    depth
                      then String -> m ()
    forall a. HasCallStack => String -> a
    error (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: Illegally trying to pop " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. (Eq a, Num a, Show a) => a -> String
    shl Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", at current level: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    depth
                      else do QueryState{SMTConfig
    queryConfig :: QueryState -> SMTConfig
    queryConfig :: SMTConfig
    queryConfig} <- m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState
                              if Bool -> Bool
    not (SolverCapabilities -> Bool
    supportsGlobalDecls (SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    queryConfig)))
                                 then String -> m ()
    forall a. HasCallStack => String -> a
    error (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                      , "*** Data.SBV: Backend solver does not support global-declarations."
                                                      , "***           Hence, calls to 'pop' are not supported."
                                                      , "***"
                                                      , "*** Request this as a feature for the underlying solver!"
                                                      ]
                                 else do Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "(pop " 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]
    ++ ")"
                                         m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
    restoreTablesAndArrays
                                         (QueryState -> QueryState) -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    (QueryState -> QueryState) -> m ()
    modifyQueryState ((QueryState -> QueryState) -> m ())
    -> (QueryState -> QueryState) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \s :: QueryState
    s -> QueryState
    s{queryAssertionStackDepth :: Int
    queryAssertionStackDepth = Int
    depth Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i}
       where shl :: a -> String
    shl 1 = "one level"
             shl n :: a
    n = a -> String
    forall a. Show a => a -> String
    show a
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " levels"

    -- | Generalization of 'Data.SBV.Control.caseSplit'
    caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
    caseSplit :: Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
    caseSplit printCases :: Bool
    printCases cases :: [(String, SBool)]
    cases = do SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
                                    SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
    go SMTConfig
    cfg ([(String, SBool)]
    cases [(String, SBool)] -> [(String, SBool)] -> [(String, SBool)]
    forall a. [a] -> [a] -> [a]
    ++ [("Coverage", SBool -> SBool
    sNot ([SBool] -> SBool
    sOr (((String, SBool) -> SBool) -> [(String, SBool)] -> [SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, SBool) -> SBool
    forall a b. (a, b) -> b
    snd [(String, SBool)]
    cases)))])
      where msg :: String -> m ()
    msg = Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    printCases (m () -> m ()) -> (String -> m ()) -> String -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO () -> m ()) -> (String -> IO ()) -> String -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> IO ()
    putStrLn

            go :: SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
    go _ []            = Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (String, SMTResult)
    forall a. Maybe a
    Nothing
            go cfg :: SMTConfig
    cfg ((n :: String
    n,c :: SBool
    c):ncs :: [(String, SBool)]
    ncs) = do let notify :: String -> m ()
    notify s :: String
    s = String -> m ()
    msg (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "Case " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

                                    String -> m ()
    notify "Starting"
                                    CheckSatResult
    r <- [SBool] -> m CheckSatResult
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [SBool] -> m CheckSatResult
    checkSatAssuming [SBool
    c]

                                    case CheckSatResult
    r of
                                      Unsat -> do String -> m ()
    notify "Unsatisfiable"
                                                  SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
    go SMTConfig
    cfg [(String, SBool)]
    ncs

                                      Sat   -> do String -> m ()
    notify "Satisfiable"
                                                  SMTResult
    res <- SMTConfig -> SMTModel -> SMTResult
    Satisfiable SMTConfig
    cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m SMTModel
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
    getModel
                                                  Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (String, SMTResult) -> m (Maybe (String, SMTResult)))
    -> Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
    forall a b. (a -> b) -> a -> b
    $ (String, SMTResult) -> Maybe (String, SMTResult)
    forall a. a -> Maybe a
    Just (String
    n, SMTResult
    res)

                                      Unk   -> do String -> m ()
    notify "Unknown"
                                                  SMTResult
    res <- SMTConfig -> SMTReasonUnknown -> SMTResult
    Unknown SMTConfig
    cfg (SMTReasonUnknown -> SMTResult)
    -> m SMTReasonUnknown -> m SMTResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m SMTReasonUnknown
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m SMTReasonUnknown
    getUnknownReason
                                                  Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (String, SMTResult) -> m (Maybe (String, SMTResult)))
    -> Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
    forall a b. (a -> b) -> a -> b
    $ (String, SMTResult) -> Maybe (String, SMTResult)
    forall a. a -> Maybe a
    Just (String
    n, SMTResult
    res)

    -- | Generalization of 'Data.SBV.Control.resetAssertions'
    resetAssertions :: (MonadIO m, MonadQuery m) => m ()
    resetAssertions :: m ()
    resetAssertions = do Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True "(reset-assertions)"
                         (QueryState -> QueryState) -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    (QueryState -> QueryState) -> m ()
    modifyQueryState ((QueryState -> QueryState) -> m ())
    -> (QueryState -> QueryState) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \s :: QueryState
    s -> QueryState
    s{ queryAssertionStackDepth :: Int
    queryAssertionStackDepth = 0 }

                         -- Make sure we restore tables and arrays after resetAssertions: See: https://github.com/LeventErkok/sbv/issues/535
                         m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
    restoreTablesAndArrays

    -- | Generalization of 'Data.SBV.Control.echo'
    echo :: (MonadIO m, MonadQuery m) => String -> m ()
    echo :: String -> m ()
    echo s :: String
    s = do let cmd :: String
    cmd = "(echo \"" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Char -> String) -> String -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Char -> String
    sanitize String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "\")"

                -- we send the command, but otherwise ignore the response
                -- note that 'send True/False' would be incorrect here. 'send True' would
                -- require a success response. 'send False' would fail to consume the
                -- output. But 'ask' does the right thing! It gets "some" response,
                -- and forgets about it immediately.
                String
    _ <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

                () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      where sanitize :: Char -> String
    sanitize '"'  = "\"\""  -- quotes need to be duplicated
            sanitize c :: Char
    c    = [Char
    c]

    -- | Generalization of 'Data.SBV.Control.exit'
    exit :: (MonadIO m, MonadQuery m) => m ()
    exit :: m ()
    exit = do Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True "(exit)"
              (QueryState -> QueryState) -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    (QueryState -> QueryState) -> m ()
    modifyQueryState ((QueryState -> QueryState) -> m ())
    -> (QueryState -> QueryState) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \s :: QueryState
    s -> QueryState
    s{queryAssertionStackDepth :: Int
    queryAssertionStackDepth = 0}

    -- | Generalization of 'Data.SBV.Control.getUnsatCore'
    getUnsatCore :: (MonadIO m, MonadQuery m) => m [String]
    getUnsatCore :: m [String]
    getUnsatCore = do
            let cmd :: String
    cmd = "(get-unsat-core)"
                bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getUnsatCore" String
    cmd "an unsat-core response"
                               (Maybe [String] -> String -> Maybe [String] -> m a)
    -> Maybe [String] -> String -> Maybe [String] -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [ "Make sure you use:"
                                      , ""
                                      , "       setOption $ ProduceUnsatCores True"
                                      , ""
                                      , "so the solver will be ready to compute unsat cores,"
                                      , "and that there is a model by first issuing a 'checkSat' call."
                                      , ""
                                      , "If using z3, you might also optionally want to set:"
                                      , ""
                                      , "       setOption $ OptionKeyword \":smt.core.minimize\" [\"true\"]"
                                      , ""
                                      , "to make sure the unsat core doesn't have irrelevant entries,"
                                      , "though this might incur a performance penalty."

                                      ]

            String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

            String
    -> (String -> Maybe [String] -> m [String])
    -> (SExpr -> m [String])
    -> m [String]
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m [String]
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m [String]) -> m [String])
    -> (SExpr -> m [String]) -> m [String]
    forall a b. (a -> b) -> a -> b
    $ \case
               EApp es :: [SExpr]
    es | Just xs :: [String]
    xs <- (SExpr -> Maybe String) -> [SExpr] -> Maybe [String]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SExpr -> Maybe String
    fromECon [SExpr]
    es -> [String] -> m [String]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([String] -> m [String]) -> [String] -> m [String]
    forall a b. (a -> b) -> a -> b
    $ (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    unBar [String]
    xs
               _                                     -> String -> Maybe [String] -> m [String]
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

    -- | Retrieve the unsat core if it was asked for in the configuration
    getUnsatCoreIfRequested :: (MonadIO m, MonadQuery m) => m (Maybe [String])
    getUnsatCoreIfRequested :: m (Maybe [String])
    getUnsatCoreIfRequested = do
            SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
            if [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or [Bool
    b | ProduceUnsatCores b :: Bool
    b <- SMTConfig -> [SMTOption]
    solverSetOptions SMTConfig
    cfg]
               then [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just ([String] -> Maybe [String]) -> m [String] -> m (Maybe [String])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [String]
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [String]
    getUnsatCore
               else Maybe [String] -> m (Maybe [String])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [String]
    forall a. Maybe a
    Nothing

    -- | Generalization of 'Data.SBV.Control.getProof'
    getProof :: (MonadIO m, MonadQuery m) => m String
    getProof :: m String
    getProof = do
            let cmd :: String
    cmd = "(get-proof)"
                bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getProof" String
    cmd "a get-proof response"
                               (Maybe [String] -> String -> Maybe [String] -> m a)
    -> Maybe [String] -> String -> Maybe [String] -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [ "Make sure you use:"
                                      , ""
                                      , "       setOption $ ProduceProofs True"
                                      , ""
                                      , "to make sure the solver is ready for producing proofs,"
                                      , "and that there is a proof by first issuing a 'checkSat' call."
                                      ]

            String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

            -- we only care about the fact that we can parse the output, so the
            -- result of parsing is ignored.
            String
    -> (String -> Maybe [String] -> m String)
    -> (SExpr -> m String)
    -> m String
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m String
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m String) -> m String)
    -> (SExpr -> m String) -> m String
    forall a b. (a -> b) -> a -> b
    $ \_ -> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    r

    -- | Generalization of 'Data.SBV.Control.getInterpolantMathSAT'. Use this version with MathSAT.
    getInterpolantMathSAT :: (MonadIO m, MonadQuery m) => [String] -> m String
    getInterpolantMathSAT :: [String] -> m String
    getInterpolantMathSAT fs :: [String]
    fs
      | [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    fs
      = String -> m String
    forall a. HasCallStack => String -> a
    error "SBV.getInterpolantMathSAT requires at least one marked constraint, received none!"
      | Bool
    True
      = do let bar :: String -> String
    bar s :: String
    s = '|' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "|"
               cmd :: String
    cmd = "(get-interpolant (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    bar [String]
    fs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
               bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getInterpolant" String
    cmd "a get-interpolant response"
                              (Maybe [String] -> String -> Maybe [String] -> m a)
    -> Maybe [String] -> String -> Maybe [String] -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [ "Make sure you use:"
                                     , ""
                                     , "       setOption $ ProduceInterpolants True"
                                     , ""
                                     , "to make sure the solver is ready for producing interpolants,"
                                     , "and that you have used the proper attributes using the"
                                     , "constrainWithAttribute function."
                                     ]

           String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

           String
    -> (String -> Maybe [String] -> m String)
    -> (SExpr -> m String)
    -> m String
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m String
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m String) -> m String)
    -> (SExpr -> m String) -> m String
    forall a b. (a -> b) -> a -> b
    $ \e :: SExpr
    e -> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ Bool -> SExpr -> String
    serialize Bool
    False SExpr
    e

    -- | Generalization of 'Data.SBV.Control.getInterpolantZ3'. Use this version with Z3.
    getInterpolantZ3 :: (MonadIO m, MonadQuery m) => [SBool] -> m String
    getInterpolantZ3 :: [SBool] -> m String
    getInterpolantZ3 fs :: [SBool]
    fs
      | [SBool] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SBool]
    fs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 2
      = String -> m String
    forall a. HasCallStack => String -> a
    error (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ "SBV.getInterpolantZ3 requires at least two booleans, received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [SBool] -> String
    forall a. Show a => a -> String
    show [SBool]
    fs
      | Bool
    True
      = do [SV]
    ss <- let fAll :: [SBV a] -> [SV] -> m [SV]
    fAll []     sofar :: [SV]
    sofar = [SV] -> m [SV]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([SV] -> m [SV]) -> [SV] -> m [SV]
    forall a b. (a -> b) -> a -> b
    $ [SV] -> [SV]
    forall a. [a] -> [a]
    reverse [SV]
    sofar
                     fAll (b :: SBV a
    b:bs :: [SBV a]
    bs) sofar :: [SV]
    sofar = do SV
    sv <- (State -> IO SV) -> m SV
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (State -> IO a) -> m a
    inNewContext (State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    `sbvToSV` SBV a
    b)
                                            [SBV a] -> [SV] -> m [SV]
    fAll [SBV a]
    bs (SV
    sv SV -> [SV] -> [SV]
    forall a. a -> [a] -> [a]
    : [SV]
    sofar)
                 in [SBool] -> [SV] -> m [SV]
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    [SBV a] -> [SV] -> m [SV]
    fAll [SBool]
    fs []

           let cmd :: String
    cmd = "(get-interpolant " 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]
    ss) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
               bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getInterpolant" String
    cmd "a get-interpolant response" Maybe [String]
    forall a. Maybe a
    Nothing

           String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

           String
    -> (String -> Maybe [String] -> m String)
    -> (SExpr -> m String)
    -> m String
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m String
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m String) -> m String)
    -> (SExpr -> m String) -> m String
    forall a b. (a -> b) -> a -> b
    $ \e :: SExpr
    e -> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ Bool -> SExpr -> String
    serialize Bool
    False SExpr
    e

    -- | Generalization of 'Data.SBV.Control.getAssertions'
    getAssertions :: (MonadIO m, MonadQuery m) => m [String]
    getAssertions :: m [String]
    getAssertions = do
            let cmd :: String
    cmd = "(get-assertions)"
                bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getAssertions" String
    cmd "a get-assertions response"
                               (Maybe [String] -> String -> Maybe [String] -> m a)
    -> Maybe [String] -> String -> Maybe [String] -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [ "Make sure you use:"
                                      , ""
                                      , "       setOption $ ProduceAssertions True"
                                      , ""
                                      , "to make sure the solver is ready for producing assertions."
                                      ]

                render :: SExpr -> String
    render = Bool -> SExpr -> String
    serialize Bool
    False

            String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

            String
    -> (String -> Maybe [String] -> m [String])
    -> (SExpr -> m [String])
    -> m [String]
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m [String]
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m [String]) -> m [String])
    -> (SExpr -> m [String]) -> m [String]
    forall a b. (a -> b) -> a -> b
    $ \pe :: SExpr
    pe -> case SExpr
    pe of
                                    EApp xs :: [SExpr]
    xs -> [String] -> m [String]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([String] -> m [String]) -> [String] -> m [String]
    forall a b. (a -> b) -> a -> b
    $ (SExpr -> String) -> [SExpr] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SExpr -> String
    render [SExpr]
    xs
                                    _       -> [String] -> m [String]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SExpr -> String
    render SExpr
    pe]

    -- | Generalization of 'Data.SBV.Control.getAssignment'
    getAssignment :: (MonadIO m, MonadQuery m) => m [(String, Bool)]
    getAssignment :: m [(String, Bool)]
    getAssignment = do
            let cmd :: String
    cmd = "(get-assignment)"
                bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getAssignment" String
    cmd "a get-assignment response"
                               (Maybe [String] -> String -> Maybe [String] -> m a)
    -> Maybe [String] -> String -> Maybe [String] -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [ "Make sure you use:"
                                      , ""
                                      , "       setOption $ ProduceAssignments True"
                                      , ""
                                      , "to make sure the solver is ready for producing assignments,"
                                      , "and that there is a model by first issuing a 'checkSat' call."
                                      ]

                -- we're expecting boolean assignment to labels, essentially
                grab :: SExpr -> Maybe (String, Bool)
    grab (EApp [ECon s :: String
    s, ENum (0, _)]) = (String, Bool) -> Maybe (String, Bool)
    forall a. a -> Maybe a
    Just (String -> String
    unQuote String
    s, Bool
    False)
                grab (EApp [ECon s :: String
    s, ENum (1, _)]) = (String, Bool) -> Maybe (String, Bool)
    forall a. a -> Maybe a
    Just (String -> String
    unQuote String
    s, Bool
    True)
                grab _                            = Maybe (String, Bool)
    forall a. Maybe a
    Nothing

            String
    r <- String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    ask String
    cmd

            String
    -> (String -> Maybe [String] -> m [(String, Bool)])
    -> (SExpr -> m [(String, Bool)])
    -> m [(String, Bool)]
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m [(String, Bool)]
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m [(String, Bool)]) -> m [(String, Bool)])
    -> (SExpr -> m [(String, Bool)]) -> m [(String, Bool)]
    forall a b. (a -> b) -> a -> b
    $ \case EApp ps :: [SExpr]
    ps | Just vs :: [(String, Bool)]
    vs <- (SExpr -> Maybe (String, Bool))
    -> [SExpr] -> Maybe [(String, Bool)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SExpr -> Maybe (String, Bool)
    grab [SExpr]
    ps -> [(String, Bool)] -> m [(String, Bool)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(String, Bool)]
    vs
                                _                                 -> String -> Maybe [String] -> m [(String, Bool)]
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

    -- | Make an assignment. The type 'Assignment' is abstract, the result is typically passed
    -- to 'mkSMTResult':
    --
    -- @ mkSMTResult [ a |-> 332
    --             , b |-> 2.3
    --             , c |-> True
    --             ]
    -- @
    --
    -- End users should use 'getModel' for automatically constructing models from the current solver state.
    -- However, an explicit 'Assignment' might be handy in complex scenarios where a model needs to be
    -- created manually.
    infix 1 |->
    (|->) :: SymVal a => SBV a -> a -> Assignment
    SBV a :: SVal
    a |-> :: SBV a -> a -> Assignment
    |-> v :: a
    v = case a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    v of
                    SBV (SVal _ (Left cv :: CV
    cv)) -> SVal -> CV -> Assignment
    Assign SVal
    a CV
    cv
                    r :: SBV a
    r                      -> String -> Assignment
    forall a. HasCallStack => String -> a
    error (String -> Assignment) -> String -> Assignment
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: Impossible happened in |->: Cannot construct a CV with literal: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBV a -> String
    forall a. Show a => a -> String
    show SBV a
    r

    -- | Generalization of 'Data.SBV.Control.mkSMTResult'
    -- NB. This function does not allow users to create interpretations for UI-Funs. But that's
    -- probably not a good idea anyhow. Also, if you use the 'validateModel' or 'optimizeValidateConstraints' features, SBV will
    -- fail on models returned via this function.
    mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult
    mkSMTResult :: [Assignment] -> m SMTResult
    mkSMTResult asgns :: [Assignment]
    asgns = do
                 QueryState{SMTConfig
    queryConfig :: SMTConfig
    queryConfig :: QueryState -> SMTConfig
    queryConfig} <- m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState
                 [(Quantifier, NamedSymVar)]
    inps <- m [(Quantifier, NamedSymVar)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(Quantifier, NamedSymVar)]
    getQuantifiedInputs

                 let grabValues :: State -> IO [(String, CV)]
    grabValues st :: State
    st = do let extract :: Assignment -> IO (SV, CV)
    extract (Assign s :: SVal
    s n :: CV
    n) = State -> SBV Any -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st (SVal -> SBV Any
    forall a. SVal -> SBV a
    SBV SVal
    s) IO SV -> (SV -> IO (SV, CV)) -> IO (SV, CV)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \sv :: SV
    sv -> (SV, CV) -> IO (SV, CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV
    sv, CV
    n)

                                        [(SV, CV)]
    modelAssignment <- (Assignment -> IO (SV, CV)) -> [Assignment] -> IO [(SV, CV)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Assignment -> IO (SV, CV)
    extract [Assignment]
    asgns

                                        -- sanity checks
                                        --     - All existentials should be given a value
                                        --     - No duplicates
                                        --     - No bindings to vars that are not inputs
                                        let userSS :: [SV]
    userSS = ((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)]
    modelAssignment

                                            missing, extra, dup :: [String]
                                            missing :: [String]
    missing = [String
    n | (EX, (s :: SV
    s, n :: String
    n)) <- [(Quantifier, NamedSymVar)]
    inps, SV
    s SV -> [SV] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [SV]
    userSS]
                                            extra :: [String]
    extra   = [SV -> String
    forall a. Show a => a -> String
    show SV
    s | SV
    s <- [SV]
    userSS, SV
    s SV -> [SV] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` ((Quantifier, NamedSymVar) -> SV)
    -> [(Quantifier, NamedSymVar)] -> [SV]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamedSymVar -> SV
    forall a b. (a, b) -> a
    fst (NamedSymVar -> SV)
    -> ((Quantifier, NamedSymVar) -> NamedSymVar)
    -> (Quantifier, NamedSymVar)
    -> SV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Quantifier, NamedSymVar) -> NamedSymVar
    forall a b. (a, b) -> b
    snd) [(Quantifier, NamedSymVar)]
    inps]
                                            dup :: [String]
    dup     = let walk :: [a] -> [String]
    walk []     = []
                                                          walk (n :: a
    n:ns :: [a]
    ns)
                                                            | a
    n a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [a]
    ns = a -> String
    forall a. Show a => a -> String
    show a
    n String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [a] -> [String]
    walk ((a -> Bool) -> [a] -> [a]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    n) [a]
    ns)
                                                            | Bool
    True        = [a] -> [String]
    walk [a]
    ns
                                                      in [SV] -> [String]
    forall a. (Eq a, Show a) => [a] -> [String]
    walk [SV]
    userSS

                                        Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([String]
    missing [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    extra [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    dup)) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do

                                              let misTag :: String
    misTag = "***   Missing inputs"
                                                  dupTag :: String
    dupTag = "***   Duplicate bindings"
                                                  extTag :: String
    extTag = "***   Extra bindings"

                                                  maxLen :: Int
    maxLen = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum ([Int] -> Int) -> [Int] -> Int
    forall a b. (a -> b) -> a -> b
    $  0
                                                                    Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : [String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    misTag | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    missing)]
                                                                   [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ [String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    extTag | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    extra)]
                                                                   [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ [String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    dupTag | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    dup)]

                                                  align :: String -> String
    align s :: String
    s = String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (Int
    maxLen Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    s) ' ' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ": "

                                              String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [""
                                                                , "*** Data.SBV: Query model construction has a faulty assignment."
                                                                , "***"
                                                                ]
                                                             [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String -> String
    align String
    misTag String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", "  [String]
    missing | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    missing)]
                                                             [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String -> String
    align String
    extTag String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", "  [String]
    extra   | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    extra)  ]
                                                             [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String -> String
    align String
    dupTag String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", "  [String]
    dup     | Bool -> Bool
    not ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    dup)    ]
                                                             [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "***"
                                                                , "*** Data.SBV: Check your query result construction!"
                                                                ]

                                        let findName :: SV -> String
    findName s :: SV
    s = case [String
    nm | (_, (i :: SV
    i, nm :: String
    nm)) <- [(Quantifier, NamedSymVar)]
    inps, SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    i] of
                                                            [nm :: String
    nm] -> String
    nm
                                                            []   -> String -> String
    forall a. HasCallStack => String -> a
    error "*** Data.SBV: Impossible happened: Cannot find " 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]
    ++ " in the input list"
                                                            nms :: [String]
    nms  -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                                                    , "*** Data.SBV: Impossible happened: Multiple matches for: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s
                                                                                    , "***   Candidates: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    nms
                                                                                    ]

                                        [(String, CV)] -> IO [(String, CV)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(SV -> String
    findName SV
    s, CV
    n) | (s :: SV
    s, n :: CV
    n) <- [(SV, CV)]
    modelAssignment]

                 [(String, CV)]
    assocs <- (State -> IO [(String, CV)]) -> m [(String, CV)]
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (State -> IO a) -> m a
    inNewContext State -> IO [(String, CV)]
    grabValues

                 let m :: SMTModel
    m = SMTModel :: [(String, GeneralizedCV)]
    -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    -> [(String, CV)]
    -> [(String, (SBVType, ([([CV], CV)], CV)))]
    -> SMTModel
    SMTModel { modelObjectives :: [(String, GeneralizedCV)]
    modelObjectives = []
                                  , modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    modelBindings   = Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    forall a. Maybe a
    Nothing
                                  , modelAssocs :: [(String, CV)]
    modelAssocs     = [(String, CV)]
    assocs
                                  , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
    modelUIFuns     = []
                                  }

                 SMTResult -> m SMTResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SMTResult -> m SMTResult) -> SMTResult -> m SMTResult
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> SMTModel -> SMTResult
    Satisfiable SMTConfig
    queryConfig SMTModel
    m

    {-# ANN getModelAtIndex ("HLint: ignore Use forM_"          :: String) #-}