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

    {-# LANGUAGE BangPatterns        #-}
    {-# LANGUAGE LambdaCase          #-}
    {-# LANGUAGE NamedFieldPuns      #-}
    {-# LANGUAGE Rank2Types          #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TupleSections       #-}
    {-# LANGUAGE ViewPatterns        #-}

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

    module Data.SBV.Control.Query (
           send, ask, retrieveResponse
         , CheckSatResult(..), checkSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
         , getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3, getAbduct, getAbductNext, getAssignment, getOption
         , freshVar, freshVar_, freshArray, freshArray_, freshLambdaArray, freshLambdaArray_
         , 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 qualified Data.Sequence      as S
    import qualified Data.Text          as T
    import qualified Data.Foldable      as F

    import Data.Char      (toLower)
    import Data.List      (intercalate, nubBy, sortOn)
    import Data.Maybe     (listToMaybe, catMaybes, fromMaybe)
    import Data.Function  (on)
    import Data.Bifunctor (first)
    import Data.Foldable  (toList)

    import Data.SBV.Core.Data

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

    import Data.SBV.Utils.SExpr

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

    import Data.SBV.Utils.PrettyNum (showNegativeNumber)

    -- | 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 Char
    c (Char
    c':cs :: String
    cs@(Char
    _:String
    _)) | 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. HasCallStack => [a] -> a
    last String
    cs  = String -> String
    forall a. HasCallStack => [a] -> [a]
    init String
    cs
    noSurrounding Char
    _ String
    s                                        = String
    s

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

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

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

    -- Collect strings appearing, used in 'getOption' only
    stringsOf :: SExpr -> [String]
    stringsOf :: SExpr -> [String]
    stringsOf (ECon String
    s)           = [String
    s]
    stringsOf (ENum (Integer
    i, Maybe Int
    _))      = [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i]
    stringsOf (EReal   AlgReal
    r)        = [AlgReal -> String
    forall a. Show a => a -> String
    show AlgReal
    r]
    stringsOf (EFloat  Float
    f)        = [Float -> String
    forall a. Show a => a -> String
    show Float
    f]
    stringsOf (EFloatingPoint FP
    f) = [FP -> String
    forall a. Show a => a -> String
    show FP
    f]
    stringsOf (EDouble Double
    d)        = [Double -> String
    forall a. Show a => a -> String
    show Double
    d]
    stringsOf (EApp [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 Bool
    removeQuotes = SExpr -> String
    go
      where go :: SExpr -> String
    go (ECon String
    s)           = if Bool
    removeQuotes then String -> String
    unQuote String
    s else String
    s
            go (ENum (Integer
    i, Maybe Int
    _))      = Integer -> String
    forall a. (Show a, Num a, Ord a) => a -> String
    showNegativeNumber Integer
    i
            go (EReal   AlgReal
    r)        = AlgReal -> String
    forall a. (Show a, Num a, Ord a) => a -> String
    showNegativeNumber AlgReal
    r
            go (EFloat  Float
    f)        = Float -> String
    forall a. (Show a, Num a, Ord a) => a -> String
    showNegativeNumber Float
    f
            go (EDouble Double
    d)        = Double -> String
    forall a. (Show a, Num a, Ord a) => a -> String
    showNegativeNumber Double
    d
            go (EFloatingPoint FP
    f) = FP -> String
    forall a. Show a => a -> String
    show FP
    f
            go (EApp [SExpr
    x])         = SExpr -> String
    go SExpr
    x
            go (EApp [SExpr]
    ss)          = String
    "(" 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]
    ++ String
    ")"

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

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

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

            grabAllStat :: SExpr -> SExpr -> (String, String)
    grabAllStat SExpr
    k 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 [SExpr]
    xs) = [SExpr] -> [(String, String)]
    walk [SExpr]
    xs
               where walk :: [SExpr] -> [(String, String)]
    walk []             = []
                     walk [SExpr
    t]            = [SExpr -> SExpr -> (String, String)
    grabAllStat SExpr
    t (String -> SExpr
    ECon String
    "")]
                     walk (SExpr
    t : SExpr
    v : [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 SExpr
    o = [SExpr -> SExpr -> (String, String)
    grabAllStat SExpr
    o (String -> SExpr
    ECon String
    "")]

        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
    $ \SExpr
    pe ->
           if Bool
    isAllStat
              then SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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 String
    "unsupported"                                        -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTInfoResponse
    Resp_Unsupported
                     EApp [ECon String
    ":assertion-stack-levels", ENum (Integer
    i, Maybe Int
    _)]        -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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 String
    ":authors" : [SExpr]
    ns)                               -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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 String
    ":error-behavior", ECon String
    "immediate-exit"]      -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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 String
    ":error-behavior", ECon String
    "continued-execution"] -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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 String
    ":name" : [SExpr]
    o)                                   -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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 String
    ":reason-unknown" : [SExpr]
    o)                         -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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 String
    ":version" : [SExpr]
    o)                                -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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 String
    s : [SExpr]
    o)                                         -> SMTInfoResponse -> m SMTInfoResponse
    forall a. a -> m a
    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)
                     SExpr
    _                                                         -> 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 String
    s] | Just SMTReasonUnknown
    d <- String -> Maybe SMTReasonUnknown
    getUR String
    s = SMTReasonUnknown
    d
            unk [SExpr]
    o                            = String -> SMTReasonUnknown
    UnknownOther (SExpr -> String
    render ([SExpr] -> SExpr
    EApp [SExpr]
    o))

            getUR :: String -> Maybe SMTReasonUnknown
    getUR 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) | (String
    k, 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 = [ (String
    "memout",     SMTReasonUnknown
    UnknownMemOut)
                             , (String
    "incomplete", SMTReasonUnknown
    UnknownIncomplete)
                             , (String
    "timeout",    SMTReasonUnknown
    UnknownTimeOut)
                             ]

    -- | Generalization of 'Data.SBV.Control.getInfo'
    getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption)
    getOption :: forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (a -> SMTOption) -> m (Maybe SMTOption)
    getOption 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 String
    "DiagnosticOutputChannel"   String
    ":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 String
    "ProduceAssertions"         String
    ":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 String
    "ProduceAssignments"        String
    ":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 String
    "ProduceProofs"             String
    ":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 String
    "ProduceInterpolants"       String
    ":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 String
    "ProduceUnsatAssumptions"   String
    ":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 String
    "ProduceUnsatCores"         String
    ":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
                     ProduceAbducts{}            -> 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 String
    "ProduceAbducts"            String
    ":produce-abducts"             ((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
    ProduceAbducts
                     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 String
    "RandomSeed"                String
    ":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 String
    "ReproducibleResourceLimit" String
    ":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 String
    "SMTVerbosity"              String
    ":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 String
    nm [String]
    _          -> 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 (String
    "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 String
    "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 String
    "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 String
    sbvName String
    smtLibName SExpr -> (Maybe [String] -> m a) -> m (Maybe a)
    continue = do
                    let cmd :: String
    cmd = String
    "(get-option " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    smtLibName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                        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 (String
    "getOption " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    sbvName) String
    cmd String
    "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 String
    "unsupported" -> Maybe a -> m (Maybe a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
                                        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 String -> a
    c (ECon String
    s) Maybe [String] -> m (Maybe a)
    _ = Maybe a -> m (Maybe a)
    forall a. a -> m 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 String -> a
    _ SExpr
    e        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 [String
    "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 Bool -> a
    c (ENum (Integer
    0, Maybe Int
    _)) Maybe [String] -> m (Maybe a)
    _ = Maybe a -> m (Maybe a)
    forall a. a -> m 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 Bool -> a
    c (ENum (Integer
    1, Maybe Int
    _)) Maybe [String] -> m (Maybe a)
    _ = Maybe a -> m (Maybe a)
    forall a. a -> m 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 Bool -> a
    _ SExpr
    e             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 [String
    "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 Integer -> a
    c (ENum (Integer
    i, Maybe Int
    _)) Maybe [String] -> m (Maybe a)
    _ = Maybe a -> m (Maybe a)
    forall a. a -> m 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 Integer -> a
    _ SExpr
    e             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 [String
    "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 [String] -> a
    c SExpr
    e p
    _ = Maybe a -> m (Maybe a)
    forall a. a -> m 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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    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
                            SMTInfoResponse
    Resp_Unsupported     -> SMTReasonUnknown -> m SMTReasonUnknown
    forall a. a -> m a
    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 String
    "Solver responded: Unsupported."
                            Resp_ReasonUnknown SMTReasonUnknown
    r -> SMTReasonUnknown -> m SMTReasonUnknown
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTReasonUnknown
    r
                            -- Shouldn't happen, but just in case:
                            SMTInfoResponse
    _                    -> String -> m SMTReasonUnknown
    forall a. HasCallStack => String -> a
    error (String -> m SMTReasonUnknown) -> String -> m SMTReasonUnknown
    forall a b. (a -> b) -> a -> b
    $ String
    "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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => 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
                     CheckSatResult
    Sat    -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                     DSat{} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                     CheckSatResult
    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 [ String
    ""
                                                  , String
    "*** Data.SBV.ensureSat: Solver reported Unknown!"
                                                  , String
    "*** Reason: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTReasonUnknown -> String
    forall a. Show a => a -> String
    show SMTReasonUnknown
    s
                                                  ]
                     CheckSatResult
    Unsat  -> String -> m ()
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.ensureSat: Solver reported Unsat!"

    -- | Generalization of 'Data.SBV.Control.getSMTResult'
    getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult
    getSMTResult :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => 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
                        CheckSatResult
    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
                        CheckSatResult
    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
                        DSat Maybe String
    p -> SMTConfig -> Maybe String -> SMTModel -> SMTResult
    DeltaSat      SMTConfig
    cfg Maybe String
    p (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
                        CheckSatResult
    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 SMTConfig
    cfg 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 (a
    _, 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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => 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
                                      CheckSatResult
    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
                                      CheckSatResult
    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
                                      DSat{} -> 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
                                      CheckSatResult
    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 a. a -> m a
    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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [String] -> m [(String, SMTResult)]
    getIndependentOptResults [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
                                             CheckSatResult
    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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Maybe [String]
    mbUC -> [(String, SMTResult)] -> m [(String, SMTResult)]
    forall a. a -> m a
    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]
                                             CheckSatResult
    Sat    -> (SMTModel -> SMTResult) -> m [(String, SMTResult)]
    forall {b}. (SMTModel -> b) -> m [(String, b)]
    continue (SMTConfig -> SMTModel -> SMTResult
    classifyModel SMTConfig
    cfg)
                                             DSat{} -> (SMTModel -> SMTResult) -> m [(String, SMTResult)]
    forall {b}. (SMTModel -> b) -> m [(String, b)]
    continue (SMTConfig -> SMTModel -> SMTResult
    classifyModel SMTConfig
    cfg)
                                             CheckSatResult
    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 a. a -> m a
    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 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 [Int
    0..] [String]
    objNames
                                   [(String, b)] -> m [(String, b)]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(String
    n, SMTModel -> b
    classify (SMTModel
    m {modelObjectives :: [(String, GeneralizedCV)]
    modelObjectives = [(String, GeneralizedCV)]
    objectiveValues})) | (String
    n, SMTModel
    m) <- [(String, SMTModel)]
    nms]

            getIndependentResult :: Int -> String -> m (String, SMTModel)
            getIndependentResult :: Int -> String -> m (String, SMTModel)
    getIndependentResult Int
    i 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 a. a -> m a
    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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> m (Bool, [SMTResult])
    getParetoOptResults (Just Int
    i)
            | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0             = (Bool, [SMTResult]) -> m (Bool, [SMTResult])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    True, [])
    getParetoOptResults 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
                                        CheckSatResult
    Unsat  -> (Bool, [SMTResult]) -> m (Bool, [SMTResult])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, [])
                                        CheckSatResult
    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)
                                        DSat{} -> (SMTModel -> SMTResult) -> m (Bool, [SMTResult])
    forall {m :: * -> *} {a}.
    (MonadIO m, MonadQuery m) =>
    (SMTModel -> a) -> m (Bool, [a])
    continue (SMTConfig -> SMTModel -> SMTResult
    classifyModel SMTConfig
    cfg)
                                        CheckSatResult
    Unk    -> do SMTReasonUnknown
    ur <- m SMTReasonUnknown
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m SMTReasonUnknown
    getUnknownReason
                                                     (Bool, [SMTResult]) -> m (Bool, [SMTResult])
    forall a. a -> m a
    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 SMTModel -> a
    classify = do SMTModel
    m <- m SMTModel
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
    getModel
                                   (Bool
    limReached, [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 Int
    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 a. a -> m 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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
    getParetoFronts (Just Int
    i) [SMTModel]
    sofar | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 = (Bool, [SMTModel]) -> m (Bool, [SMTModel])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    True, [SMTModel]
    sofar)
            getParetoFronts Maybe Int
    mbi      [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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \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 Int
    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
                                                           CheckSatResult
    Unsat  -> (Bool, [SMTModel]) -> m (Bool, [SMTModel])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, [SMTModel]
    sofar)
                                                           CheckSatResult
    Sat    -> m (Bool, [SMTModel])
    more
                                                           DSat{} -> m (Bool, [SMTModel])
    more
                                                           CheckSatResult
    Unk    -> m (Bool, [SMTModel])
    more

    -- | Generalization of 'Data.SBV.Control.getModel'
    getModel :: (MonadIO m, MonadQuery m) => m SMTModel
    getModel :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => 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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Int -> m SMTModel
    getModelAtIndex Maybe Int
    mbi = do
        State{IORef SBVRunMode
    runMode :: IORef SBVRunMode
    runMode :: State -> 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
    $ String
    "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@LambdaGen{} -> String -> m SMTModel
    forall a. HasCallStack => String -> a
    error (String -> m SMTModel) -> String -> m SMTModel
    forall a b. (a -> b) -> a -> b
    $ String
    "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
    $ String
    "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{}     -> do
              SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
              [(String, (Maybe [String], SBVType))]
    uis <- m [(String, (Maybe [String], SBVType))]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(String, (Maybe [String], SBVType))]
    getUIs

              UserInputs
    allModelInputs <- m UserInputs
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
    getTopLevelInputs
              [(Name, CV)]
    obsvs          <- m [(Name, CV)]
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(Name, CV)]
    getObservables

              Seq (SV, (Name, CV))
    inputAssocs <- let grab :: NamedSymVar -> f (SV, (Name, CV))
    grab (NamedSymVar SV
    sv Name
    nm) = let wrap :: b -> (SV, (Name, b))
    wrap !b
    c = (SV
    sv, (Name
    nm, b
    c)) in CV -> (SV, (Name, CV))
    forall {b}. b -> (SV, (Name, b))
    wrap (CV -> (SV, (Name, CV))) -> f CV -> f (SV, (Name, 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
                             in (NamedSymVar -> m (SV, (Name, CV)))
    -> UserInputs -> m (Seq (SV, (Name, CV)))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Seq a -> m (Seq b)
    mapM NamedSymVar -> m (SV, (Name, CV))
    forall {f :: * -> *}.
    (MonadIO f, MonadQuery f) =>
    NamedSymVar -> f (SV, (Name, CV))
    grab UserInputs
    allModelInputs

              let name :: (a, (c, b)) -> c
    name     = (c, b) -> c
    forall a b. (a, b) -> a
    fst ((c, b) -> c) -> ((a, (c, b)) -> (c, b)) -> (a, (c, b)) -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a, (c, b)) -> (c, b)
    forall a b. (a, b) -> b
    snd
                  removeSV :: (a, b) -> b
    removeSV = (a, b) -> b
    forall a b. (a, b) -> b
    snd
                  prepare :: Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
    prepare  = Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
    forall a. Ord a => Seq a -> Seq a
    S.unstableSort (Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV)))
    -> (Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV)))
    -> Seq (SV, (Name, CV))
    -> Seq (SV, (Name, CV))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((SV, (Name, CV)) -> Bool)
    -> Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
    forall a. (a -> Bool) -> Seq a -> Seq a
    S.filter (Bool -> Bool
    not (Bool -> Bool)
    -> ((SV, (Name, CV)) -> Bool) -> (SV, (Name, CV)) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SMTConfig -> String -> Bool
    mustIgnoreVar SMTConfig
    cfg (String -> Bool)
    -> ((SV, (Name, CV)) -> String) -> (SV, (Name, CV)) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> String
    T.unpack (Name -> String)
    -> ((SV, (Name, CV)) -> Name) -> (SV, (Name, CV)) -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SV, (Name, CV)) -> Name
    forall {a} {c} {b}. (a, (c, b)) -> c
    name)
                  assocs :: Seq (Name, CV)
    assocs   = [(Name, CV)] -> Seq (Name, CV)
    forall a. [a] -> Seq a
    S.fromList (((Name, CV) -> Name) -> [(Name, CV)] -> [(Name, CV)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    sortOn (Name, CV) -> Name
    forall a b. (a, b) -> a
    fst [(Name, CV)]
    obsvs) Seq (Name, CV) -> Seq (Name, CV) -> Seq (Name, CV)
    forall a. Semigroup a => a -> a -> a
    <> ((SV, (Name, CV)) -> (Name, CV))
    -> Seq (SV, (Name, CV)) -> Seq (Name, CV)
    forall a b. (a -> b) -> Seq a -> Seq b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (SV, (Name, CV)) -> (Name, CV)
    forall a b. (a, b) -> b
    removeSV (Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
    prepare Seq (SV, (Name, CV))
    inputAssocs)

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

              -- 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, (Maybe [String], SBVType))] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, (Maybe [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
                      Maybe [String]
    Nothing   -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                      Just [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 (Seq (NamedSymVar, CV))
    bindings <- let get :: NamedSymVar -> m (NamedSymVar, CV)
    get i :: NamedSymVar
    i@(NamedSymVar -> SV
    getSV -> SV
    sv) = case ((SV, (Name, CV)) -> SV)
    -> SV -> Seq (SV, (Name, CV)) -> Maybe (SV, (Name, CV))
    forall a. Eq a => (a -> SV) -> SV -> Seq a -> Maybe a
    lookupInput (SV, (Name, CV)) -> SV
    forall a b. (a, b) -> a
    fst SV
    sv Seq (SV, (Name, CV))
    inputAssocs of
                                                      Just (SV
    _, (Name
    _, CV
    cv)) -> (NamedSymVar, CV) -> m (NamedSymVar, CV)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NamedSymVar
    i, CV
    cv)
                                                      Maybe (SV, (Name, 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
                                                                              (NamedSymVar, CV) -> m (NamedSymVar, CV)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NamedSymVar
    i, CV
    cv)

                          in if SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                             then Seq (NamedSymVar, CV) -> Maybe (Seq (NamedSymVar, CV))
    forall a. a -> Maybe a
    Just (Seq (NamedSymVar, CV) -> Maybe (Seq (NamedSymVar, CV)))
    -> m (Seq (NamedSymVar, CV)) -> m (Maybe (Seq (NamedSymVar, CV)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NamedSymVar -> m (NamedSymVar, CV))
    -> UserInputs -> m (Seq (NamedSymVar, CV))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Seq a -> m (Seq b)
    mapM NamedSymVar -> m (NamedSymVar, CV)
    forall {m :: * -> *}.
    (MonadIO m, MonadQuery m) =>
    NamedSymVar -> m (NamedSymVar, CV)
    get UserInputs
    allModelInputs
                             else Maybe (Seq (NamedSymVar, CV)) -> m (Maybe (Seq (NamedSymVar, CV)))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Seq (NamedSymVar, CV))
    forall a. Maybe a
    Nothing

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

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

              SMTModel -> m SMTModel
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SMTModel { modelObjectives :: [(String, GeneralizedCV)]
    modelObjectives = []
                              , modelBindings :: Maybe [(NamedSymVar, CV)]
    modelBindings   = Seq (NamedSymVar, CV) -> [(NamedSymVar, CV)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList (Seq (NamedSymVar, CV) -> [(NamedSymVar, CV)])
    -> Maybe (Seq (NamedSymVar, CV)) -> Maybe [(NamedSymVar, CV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Seq (NamedSymVar, CV))
    bindings
                              , modelAssocs :: [(String, CV)]
    modelAssocs     = [(String, CV)]
    uiVals [(String, CV)] -> [(String, CV)] -> [(String, CV)]
    forall a. [a] -> [a] -> [a]
    ++ Seq (String, CV) -> [(String, CV)]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList ((Name -> String) -> (Name, CV) -> (String, CV)
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first Name -> String
    T.unpack ((Name, CV) -> (String, CV)) -> Seq (Name, CV) -> Seq (String, CV)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Seq (Name, CV)
    assocs)
                              , modelUIFuns :: [(String, (SBVType, Either String ([([CV], CV)], CV)))]
    modelUIFuns     = [(String, (SBVType, Either String ([([CV], CV)], CV)))]
    uiFunVals
                              }

    -- | 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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(String, GeneralizedCV)]
    getObjectiveValues = do let cmd :: String
    cmd = String
    "(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 String
    "getObjectiveValues" String
    cmd String
    "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 <- UserInputs -> [NamedSymVar]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList (UserInputs -> [NamedSymVar]) -> m UserInputs -> m [NamedSymVar]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m UserInputs
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
    getTopLevelInputs

                            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 String
    "objectives" : [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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
                                                SExpr
    _                             -> 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 forall a. Maybe [String] -> m a
    bailOut [NamedSymVar]
    inputs SExpr
    expr =
                    case SExpr
    expr of
                      EApp [SExpr
    _]          -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
    forall a. a -> m a
    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 String
    nm, SExpr
    v] -> String -> SExpr -> m (Maybe (String, GeneralizedCV))
    locate String
    nm SExpr
    v               -- Regular case
                      SExpr
    _                 -> 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 String
    nm SExpr
    v = case [NamedSymVar] -> Maybe NamedSymVar
    forall a. [a] -> Maybe a
    listToMaybe [NamedSymVar
    p | p :: NamedSymVar
    p@(NamedSymVar SV
    sv Name
    _) <- [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
                                    Maybe NamedSymVar
    Nothing                          -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
    forall a. a -> m a
    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 (NamedSymVar SV
    sv Name
    actualName) -> SV -> SExpr -> m GeneralizedCV
    grab SV
    sv SExpr
    v m GeneralizedCV
    -> (GeneralizedCV -> m (Maybe (String, GeneralizedCV)))
    -> m (Maybe (String, GeneralizedCV))
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \GeneralizedCV
    val -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
    forall a. a -> m a
    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 (Name -> String
    T.unpack Name
    actualName, GeneralizedCV
    val)

                    dontUnderstand :: String -> m a
    dontUnderstand 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 [ String
    "Unable to understand solver output."
                                                      , String
    "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 SV
    s SExpr
    topExpr
                      | Just CV
    v <- Kind -> SExpr -> Maybe CV
    recoverKindedValue Kind
    k SExpr
    topExpr = GeneralizedCV -> m GeneralizedCV
    forall a. a -> m a
    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 String
    "oo")                    = ExtCV -> m ExtCV
    forall a. a -> m a
    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 String
    "epsilon")               = ExtCV -> m ExtCV
    forall a. a -> m a
    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 String
    "interval", SExpr
    x, 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 a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> m ExtCV
    cvt SExpr
    y
                            cvt (ENum    (Integer
    i, Maybe Int
    _))               = ExtCV -> m ExtCV
    forall a. a -> m a
    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   AlgReal
    r)                    = ExtCV -> m ExtCV
    forall a. a -> m a
    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  Float
    f)                    = ExtCV -> m ExtCV
    forall a. a -> m a
    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 Double
    d)                    = ExtCV -> m ExtCV
    forall a. a -> m a
    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 String
    "+", SExpr
    x, 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 a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> m ExtCV
    cvt SExpr
    y
                            cvt (EApp [ECon String
    "*", SExpr
    x, 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 a b. m (a -> b) -> m a -> m b
    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 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 String
    "to_real", SExpr
    n]) = SExpr
    n
                            simplify (EApp [SExpr]
    xs)                  = [SExpr] -> SExpr
    EApp ((SExpr -> SExpr) -> [SExpr] -> [SExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map SExpr -> SExpr
    simplify [SExpr]
    xs)
                            simplify SExpr
    e                          = SExpr
    e

    -- | Generalization of 'Data.SBV.Control.checkSatAssuming'
    checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult
    checkSatAssuming :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [SBool] -> m CheckSatResult
    checkSatAssuming [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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
    checkSatAssumingHelper Bool
    getAssumptions [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 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\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 a. a -> IO a
    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, SBool
    _) <- ((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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\(SV
    sv, SBool
    sb) -> do Int
    unique <- State -> IO Int
    incrementInternalCounter State
    st
                                                                         (SV, (Int, SBool)) -> IO (SV, (Int, SBool))
    forall a. a -> IO a
    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 (a
    sv, (a
    unique, 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 = String
    "__assumption_proxy_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    unique
                                                  decls :: [String]
    decls = [ String
    "(declare-const " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    proxy String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " Bool)"
                                                          , String
    "(assert (= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    proxy String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"
                                                          ]

                                     [(String, [String], (String, SBool))]
    -> IO [(String, [String], (String, SBool))]
    forall a. a -> IO a
    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 ([String]
    origNames, [[String]]
    declss, [(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 = String
    "(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]
    ++ String
    "))"
                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 String
    "checkSatAssuming" String
    cmd String
    "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 [ String
    "Make sure you use:"
                                      , String
    ""
                                      , String
    "       setOption $ ProduceUnsatAssumptions True"
                                      , String
    ""
                                      , String
    "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 a. a -> m a
    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 a. a -> m a
    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 String
    "sat"     -> (CheckSatResult, Maybe [SBool])
    -> m (CheckSatResult, Maybe [SBool])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CheckSatResult
    Sat, Maybe [SBool]
    forall a. Maybe a
    Nothing)
                                ECon String
    "unsat"   -> m (CheckSatResult, Maybe [SBool])
    grabUnsat
                                ECon String
    "unknown" -> (CheckSatResult, Maybe [SBool])
    -> m (CheckSatResult, Maybe [SBool])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CheckSatResult
    Unk, Maybe [SBool]
    forall a. Maybe a
    Nothing)
                                SExpr
    _              -> 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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => 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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => 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 = [ String
    "table"  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_initializer" | Int
    i <- [Int
    0 .. Int
    tCount Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]]
                                    aInits :: [String]
    aInits = [ String
    "array_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_initializer" | Int
    i <- [Int
    0 .. Int
    aCount Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]]
                                    inits :: [String]
    inits  = [String]
    tInits [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    aInits

                                case [String]
    inits of
                                  []  -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()   -- Nothing to do
                                  [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
    $ String
    "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                                  [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
    $ String
    "(assert (and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "))"

    -- | Generalization of 'Data.SBV.Control.inNewAssertionStack'
    inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a
    inNewAssertionStack :: forall (m :: * -> *) a. (MonadIO m, MonadQuery m) => m a -> m a
    inNewAssertionStack m a
    q = do Int -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
    push Int
    1
                               a
    r <- m a
    q
                               Int -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
    pop Int
    1
                               a -> m a
    forall a. 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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
    push Int
    i
     | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 = String -> m ()
    forall a. HasCallStack => String -> a
    error (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "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
    $ String
    "(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]
    ++ String
    ")"
                   (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
    $ \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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
    pop Int
    i
     | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 = String -> m ()
    forall a. HasCallStack => String -> a
    error (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "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
    $ String
    "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]
    ++ String
    ", 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 :: SMTConfig
    queryConfig :: QueryState -> 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 [ String
    ""
                                                      , String
    "*** Data.SBV: Backend solver does not support global-declarations."
                                                      , String
    "***           Hence, calls to 'pop' are not supported."
                                                      , String
    "***"
                                                      , String
    "*** 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
    $ String
    "(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]
    ++ String
    ")"
                                         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
    $ \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 a
    1 = String
    "one level"
             shl a
    n = a -> String
    forall a. Show a => a -> String
    show a
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " levels"

    -- | Generalization of 'Data.SBV.Control.caseSplit'
    caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
    caseSplit :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
    caseSplit Bool
    printCases [(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]
    ++ [(String
    "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 SMTConfig
    _ []            = Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (String, SMTResult)
    forall a. Maybe a
    Nothing
            go SMTConfig
    cfg ((String
    n,SBool
    c):[(String, SBool)]
    ncs) = do let notify :: String -> m ()
    notify String
    s = String -> m ()
    msg (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Case " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

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

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

                                      CheckSatResult
    Sat      -> do String -> m ()
    notify String
    "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 a. a -> m a
    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)

                                      DSat Maybe String
    mbP -> do String -> m ()
    notify (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Delta satisfiable" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> (String -> String) -> Maybe String -> String
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe String
    "" (String
    " (precision: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) Maybe String
    mbP
                                                     SMTResult
    res <- SMTConfig -> Maybe String -> SMTModel -> SMTResult
    DeltaSat SMTConfig
    cfg Maybe String
    mbP (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 a. a -> m a
    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)

                                      CheckSatResult
    Unk      -> do String -> m ()
    notify String
    "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 a. a -> m a
    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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
    resetAssertions = do Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True String
    "(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
    $ \QueryState
    s -> QueryState
    s{ queryAssertionStackDepth :: Int
    queryAssertionStackDepth = Int
    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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => String -> m ()
    echo String
    s = do let cmd :: String
    cmd = String
    "(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]
    ++ String
    "\")"

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

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

    -- | Generalization of 'Data.SBV.Control.getUnsatCore'
    getUnsatCore :: (MonadIO m, MonadQuery m) => m [String]
    getUnsatCore :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [String]
    getUnsatCore = do
            let cmd :: String
    cmd = String
    "(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 String
    "getUnsatCore" String
    cmd String
    "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 [ String
    "Make sure you use:"
                                      , String
    ""
                                      , String
    "       setOption $ ProduceUnsatCores True"
                                      , String
    ""
                                      , String
    "so the solver will be ready to compute unsat cores,"
                                      , String
    "and that there is a model by first issuing a 'checkSat' call."
                                      , String
    ""
                                      , String
    "If using z3, you might also optionally want to set:"
                                      , String
    ""
                                      , String
    "       setOption $ OptionKeyword \":smt.core.minimize\" [\"true\"]"
                                      , String
    ""
                                      , String
    "to make sure the unsat core doesn't have irrelevant entries,"
                                      , String
    "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 [SExpr]
    es | Just [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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SExpr -> Maybe String
    fromECon [SExpr]
    es -> [String] -> m [String]
    forall a. a -> m a
    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
               SExpr
    _                                     -> 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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    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 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 a. a -> m a
    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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m String
    getProof = do
            let cmd :: String
    cmd = String
    "(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 String
    "getProof" String
    cmd String
    "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 [ String
    "Make sure you use:"
                                      , String
    ""
                                      , String
    "       setOption $ ProduceProofs True"
                                      , String
    ""
                                      , String
    "to make sure the solver is ready for producing proofs,"
                                      , String
    "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
    $ \SExpr
    _ -> String -> m String
    forall a. a -> m a
    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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [String] -> m String
    getInterpolantMathSAT [String]
    fs
      | [String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    fs
      = String -> m String
    forall a. HasCallStack => String -> a
    error String
    "SBV.getInterpolantMathSAT requires at least one marked constraint, received none!"
      | Bool
    True
      = do let bar :: String -> String
    bar String
    s = Char
    '|' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "|"
               cmd :: String
    cmd = String
    "(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]
    ++ String
    "))"
               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 String
    "getInterpolant" String
    cmd String
    "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 [ String
    "Make sure you use:"
                                     , String
    ""
                                     , String
    "       setOption $ ProduceInterpolants True"
                                     , String
    ""
                                     , String
    "to make sure the solver is ready for producing interpolants,"
                                     , String
    "and that you have used the proper attributes using the"
                                     , String
    "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
    $ \SExpr
    e -> String -> m String
    forall a. a -> m a
    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.getAbduct'.
    getAbduct :: (SolverContext m, MonadIO m, MonadQuery m) => Maybe String -> String -> SBool -> m String
    getAbduct :: forall (m :: * -> *).
    (SolverContext m, MonadIO m, MonadQuery m) =>
    Maybe String -> String -> SBool -> m String
    getAbduct Maybe String
    mbGrammar String
    defName SBool
    b = do
       SV
    s <- (State -> IO SV) -> m SV
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (State -> IO a) -> m a
    inNewContext (State -> SBool -> IO SV
    forall a. State -> SBV a -> IO SV
    `sbvToSV` SBool
    b)
       let cmd :: String
    cmd = String
    "(get-abduct " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    defName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe String
    "" Maybe String
    mbGrammar String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
           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 String
    "getAbduct" String
    cmd String
    "a get-abduct 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
    $ \SExpr
    e -> String -> m String
    forall a. a -> m a
    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.getAbductNext'.
    getAbductNext :: (MonadIO m, MonadQuery m) => m String
    getAbductNext :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m String
    getAbductNext = do
       let cmd :: String
    cmd = String
    "(get-abduct-next)"
           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 String
    "getAbductNext" String
    cmd String
    "a get-abduct-next 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
    $ \SExpr
    e -> String -> m String
    forall a. a -> m a
    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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [SBool] -> m String
    getInterpolantZ3 [SBool]
    fs
      | [SBool] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SBool]
    fs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    2
      = String -> m String
    forall a. HasCallStack => String -> a
    error (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 []     [SV]
    sofar = [SV] -> m [SV]
    forall a. a -> m a
    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 (SBV a
    b:[SBV a]
    bs) [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 = String
    "(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]
    ++ String
    ")"
               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 String
    "getInterpolant" String
    cmd String
    "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
    $ \SExpr
    e -> String -> m String
    forall a. a -> m a
    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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [String]
    getAssertions = do
            let cmd :: String
    cmd = String
    "(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 String
    "getAssertions" String
    cmd String
    "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 [ String
    "Make sure you use:"
                                      , String
    ""
                                      , String
    "       setOption $ ProduceAssertions True"
                                      , String
    ""
                                      , String
    "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
    $ \SExpr
    pe -> case SExpr
    pe of
                                    EApp [SExpr]
    xs -> [String] -> m [String]
    forall a. a -> m a
    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
                                    SExpr
    _       -> [String] -> m [String]
    forall a. a -> m a
    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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(String, Bool)]
    getAssignment = do
            let cmd :: String
    cmd = String
    "(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 String
    "getAssignment" String
    cmd String
    "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 [ String
    "Make sure you use:"
                                      , String
    ""
                                      , String
    "       setOption $ ProduceAssignments True"
                                      , String
    ""
                                      , String
    "to make sure the solver is ready for producing assignments,"
                                      , String
    "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 String
    s, ENum (Integer
    0, Maybe Int
    _)]) = (String, Bool) -> Maybe (String, Bool)
    forall a. a -> Maybe a
    Just (String -> String
    unQuote String
    s, Bool
    False)
                grab (EApp [ECon String
    s, ENum (Integer
    1, Maybe Int
    _)]) = (String, Bool) -> Maybe (String, Bool)
    forall a. a -> Maybe a
    Just (String -> String
    unQuote String
    s, Bool
    True)
                grab SExpr
    _                            = 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 [SExpr]
    ps | Just [(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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SExpr -> Maybe (String, Bool)
    grab [SExpr]
    ps -> [(String, Bool)] -> m [(String, Bool)]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(String, Bool)]
    vs
                                SExpr
    _                                 -> 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 SVal
    a |-> :: forall a. SymVal a => SBV a -> a -> Assignment
    |-> a
    v = case a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    v of
                    SBV (SVal Kind
    _ (Left CV
    cv)) -> SVal -> CV -> Assignment
    Assign SVal
    a CV
    cv
                    SBV a
    r                      -> String -> Assignment
    forall a. HasCallStack => String -> a
    error (String -> Assignment) -> String -> Assignment
    forall a b. (a -> b) -> a -> b
    $ String
    "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 :: forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [Assignment] -> m SMTResult
    mkSMTResult [Assignment]
    asgns = do
                 QueryState{SMTConfig
    queryConfig :: QueryState -> SMTConfig
    queryConfig :: SMTConfig
    queryConfig} <- m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState
                 [NamedSymVar]
    inps <- UserInputs -> [NamedSymVar]
    forall a. Seq a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList (UserInputs -> [NamedSymVar]) -> m UserInputs -> m [NamedSymVar]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m UserInputs
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
    getTopLevelInputs

                 let grabValues :: State -> IO [(String, CV)]
    grabValues State
    st = do let extract :: Assignment -> IO (SV, CV)
    extract (Assign SVal
    s 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 a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \SV
    sv -> (SV, CV) -> IO (SV, CV)
    forall a. a -> IO a
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 = [Name -> String
    T.unpack Name
    n | NamedSymVar SV
    s Name
    n <- [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` (NamedSymVar -> SV) -> [NamedSymVar] -> [SV]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedSymVar -> SV
    getSV [NamedSymVar]
    inps]
                                            dup :: [String]
    dup     = let walk :: [a] -> [String]
    walk []     = []
                                                          walk (a
    n:[a]
    ns)
                                                            | a
    n a -> [a] -> Bool
    forall a. Eq a => 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 a. [a] -> 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 = String
    "***   Missing inputs"
                                                  dupTag :: String
    dupTag = String
    "***   Duplicate bindings"
                                                  extTag :: String
    extTag = String
    "***   Extra bindings"

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

                                                  align :: String -> String
    align 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 a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    s) Char
    ' ' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ": "

                                              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
    $ [String
    ""
                                                                , String
    "*** Data.SBV: Query model construction has a faulty assignment."
                                                                , String
    "***"
                                                                ]
                                                             [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
    ", "  [String]
    missing | Bool -> Bool
    not ([String] -> Bool
    forall a. [a] -> 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
    ", "  [String]
    extra   | Bool -> Bool
    not ([String] -> Bool
    forall a. [a] -> 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
    ", "  [String]
    dup     | Bool -> Bool
    not ([String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    dup)    ]
                                                             [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "***"
                                                                , String
    "*** Data.SBV: Check your query result construction!"
                                                                ]

                                        let findName :: SV -> String
    findName SV
    s = case [Name -> String
    T.unpack Name
    nm | NamedSymVar SV
    i Name
    nm <- [NamedSymVar]
    inps, SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    i] of
                                                            [String
    nm] -> String
    nm
                                                            []   -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "*** 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]
    ++ String
    " in the input list"
                                                            [String]
    nms  -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    ""
                                                                                    , String
    "*** 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
                                                                                    , String
    "***   Candidates: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    nms
                                                                                    ]

                                        [(String, CV)] -> IO [(String, CV)]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(SV -> String
    findName SV
    s, CV
    n) | (SV
    s, 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 { modelObjectives :: [(String, GeneralizedCV)]
    modelObjectives = []
                                  , modelBindings :: Maybe [(NamedSymVar, CV)]
    modelBindings   = Maybe [(NamedSymVar, CV)]
    forall a. Maybe a
    Nothing
                                  , modelAssocs :: [(String, CV)]
    modelAssocs     = [(String, CV)]
    assocs
                                  , modelUIFuns :: [(String, (SBVType, Either String ([([CV], CV)], CV)))]
    modelUIFuns     = []
                                  }

                 SMTResult -> m SMTResult
    forall a. a -> m a
    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

    {- HLint ignore getModelAtIndex "Use forM_" -}