    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Control.Utils
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Query related utils.
    -----------------------------------------------------------------------------

    {-# LANGUAGE BangPatterns           #-}
    {-# LANGUAGE FlexibleContexts       #-}
    {-# LANGUAGE FlexibleInstances      #-}
    {-# LANGUAGE FunctionalDependencies #-}
    {-# LANGUAGE LambdaCase             #-}
    {-# LANGUAGE NamedFieldPuns         #-}
    {-# LANGUAGE ScopedTypeVariables    #-}
    {-# LANGUAGE TupleSections          #-}
    {-# LANGUAGE TypeApplications       #-}

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

    module Data.SBV.Control.Utils (
           io
         , ask, send, getValue, getFunction, getUninterpretedValue
         , getValueCV, getUIFunCVAssoc, getUnsatAssumptions
         , SMTFunction(..), registerUISMTFunction
         , getQueryState, modifyQueryState, getConfig, getObjectives, getUIs
         , getSBVAssertions, getSBVPgm, getQuantifiedInputs, getObservables
         , checkSat, checkSatUsing, getAllSatResult
         , inNewContext, freshVar, freshVar_, freshArray, freshArray_
         , parse
         , unexpected
         , timeout
         , queryDebug
         , retrieveResponse
         , recoverKindedValue
         , runProofOn
         , executeQuery
         ) where

    import Data.List  (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort, isPrefixOf)

    import Data.Char     (isPunctuation, isSpace, chr, ord, isDigit)
    import Data.Function (on)

    import Data.Proxy

    import qualified Data.Map.Strict    as Map
    import qualified Data.IntMap.Strict as IMap
    import qualified Data.Sequence      as S

    import Control.Monad            (join, unless, zipWithM, when, replicateM)
    import Control.Monad.IO.Class   (MonadIO, liftIO)
    import Control.Monad.Trans      (lift)
    import Control.Monad.Reader     (runReaderT)

    import Data.IORef (readIORef, writeIORef)

    import Data.Time (getZonedTime)

    import Data.SBV.Core.Data     ( SV(..), trueSV, falseSV, CV(..), trueCV, falseCV, SBV, sbvToSV, kindOf, Kind(..)
                                  , HasKind(..), mkConstCV, CVal(..), SMTResult(..)
                                  , NamedSymVar, SMTConfig(..), SMTModel(..)
                                  , QueryState(..), SVal(..), Quantifier(..), cache
                                  , newExpr, SBVExpr(..), Op(..), FPOp(..), SBV(..), SymArray(..)
                                  , SolverContext(..), SBool, Objective(..), SolverCapabilities(..), capabilities
                                  , Result(..), SMTProblem(..), trueSV, SymVal(..), SBVPgm(..), SMTSolver(..), SBVRunMode(..)
                                  , SBVType(..), forceSVArg, RoundingMode(RoundNearestTiesToEven), (.=>)
                                  , RCSet(..)
                                  )

    import Data.SBV.Core.Symbolic ( IncState(..), withNewIncState, State(..), svToSV, symbolicEnv, SymbolicT
                                  , MonadQuery(..), QueryContext(..), Queriable(..), Fresh(..)
                                  , registerLabel, svMkSymVar, validationRequested
                                  , isSafetyCheckingIStage, isSetupIStage, isRunIStage, IStage(..), QueryT(..)
                                  , extractSymbolicSimulationState, MonadSymbolic(..), newUninterpreted
                                  )

    import Data.SBV.Core.AlgReals   (mergeAlgReals)
    import Data.SBV.Core.Kind       (smtType, hasUninterpretedSorts)
    import Data.SBV.Core.Operations (svNot, svNotEqual, svOr)

    import Data.SBV.SMT.SMT     (showModel, parseCVs, SatModel)
    import Data.SBV.SMT.SMTLib  (toIncSMTLib, toSMTLib)
    import Data.SBV.SMT.Utils   (showTimeoutValue, addAnnotations, alignPlain, debug, mergeSExpr, SBVException(..))

    import Data.SBV.Utils.ExtractIO
    import Data.SBV.Utils.Lib       (qfsToString)
    import Data.SBV.Utils.SExpr
    import Data.SBV.Utils.PrettyNum (cvToSMTLib)

    import Data.SBV.Control.Types

    import qualified Data.Set as Set (empty, fromList, toAscList)

    import qualified Control.Exception as C

    import GHC.Stack

    -- | 'Data.SBV.Trans.Control.QueryT' as a 'SolverContext'.
    instance MonadIO m => SolverContext (QueryT m) where
       constrain :: SBool -> QueryT m ()
    constrain              = Bool -> [(String, String)] -> SBool -> QueryT m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> [(String, String)] -> SBool -> m ()
    addQueryConstraint Bool
    False []
       softConstrain :: SBool -> QueryT m ()
    softConstrain          = Bool -> [(String, String)] -> SBool -> QueryT m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> [(String, String)] -> SBool -> m ()
    addQueryConstraint Bool
    True  []
       namedConstraint :: String -> SBool -> QueryT m ()
    namedConstraint nm :: String
    nm     = Bool -> [(String, String)] -> SBool -> QueryT m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> [(String, String)] -> SBool -> m ()
    addQueryConstraint Bool
    False [(":named", String
    nm)]
       constrainWithAttribute :: [(String, String)] -> SBool -> QueryT m ()
    constrainWithAttribute = Bool -> [(String, String)] -> SBool -> QueryT m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> [(String, String)] -> SBool -> m ()
    addQueryConstraint Bool
    False
       addAxiom :: String -> [String] -> QueryT m ()
    addAxiom               = String -> [String] -> QueryT m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> [String] -> m ()
    addQueryAxiom
       contextState :: QueryT m State
    contextState           = QueryT m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState

       setOption :: SMTOption -> QueryT m ()
    setOption o :: SMTOption
    o
         | SMTOption -> Bool
    isStartModeOption SMTOption
    o = String -> QueryT m ()
    forall a. HasCallStack => String -> a
    error (String -> QueryT m ()) -> String -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                 , "*** Data.SBV: '" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SMTOption -> String
    forall a. Show a => a -> String
    show SMTOption
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "' can only be set at start-up time."
                                                 , "*** Hint: Move the call to 'setOption' before the query."
                                                 ]
         | Bool
    True                = Bool -> String -> QueryT m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True (String -> QueryT m ()) -> String -> QueryT m ()
    forall a b. (a -> b) -> a -> b
    $ SMTOption -> String
    setSMTOption SMTOption
    o

    -- | Adding a constraint, possibly with attributes and possibly soft. Only used internally.
    -- Use 'constrain' and 'namedConstraint' from user programs.
    addQueryConstraint :: (MonadIO m, MonadQuery m) => Bool -> [(String, String)] -> SBool -> m ()
    addQueryConstraint :: Bool -> [(String, String)] -> SBool -> m ()
    addQueryConstraint isSoft :: Bool
    isSoft atts :: [(String, String)]
    atts b :: SBool
    b = do SV
    sv <- (State -> IO SV) -> m SV
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (State -> IO a) -> m a
    inNewContext (\st :: State
    st -> IO SV -> IO SV
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SV -> IO SV) -> IO SV -> IO SV
    forall a b. (a -> b) -> a -> b
    $ do (String -> IO ()) -> [String] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (String -> State -> String -> IO ()
    registerLabel "Constraint" State
    st) [String
    nm | (":named", nm :: String
    nm) <- [(String, String)]
    atts]
                                                                                 State -> SBool -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBool
    b)

                                          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([(String, String)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(String, String)]
    atts Bool -> Bool -> Bool
    && SV
    sv SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                                                 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 -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    asrt String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)] -> String -> String
    addAnnotations [(String, String)]
    atts (SV -> String
    forall a. Show a => a -> String
    show SV
    sv)  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
       where asrt :: String
    asrt | Bool
    isSoft = "assert-soft"
                  | Bool
    True   = "assert"

    addQueryAxiom :: (MonadIO m, MonadQuery m) => String -> [String] -> m ()
    addQueryAxiom :: String -> [String] -> m ()
    addQueryAxiom nm :: String
    nm ls :: [String]
    ls = 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
    $ "; -- user given axiom: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm
                             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] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" [String]
    ls

    -- | Get the current configuration
    getConfig :: (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig :: m SMTConfig
    getConfig = QueryState -> SMTConfig
    queryConfig (QueryState -> SMTConfig) -> m QueryState -> m SMTConfig
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState

    -- | Get the objectives
    getObjectives :: (MonadIO m, MonadQuery m) => m [Objective (SV, SV)]
    getObjectives :: m [Objective (SV, SV)]
    getObjectives = do State{IORef [Objective (SV, SV)]
    rOptGoals :: State -> IORef [Objective (SV, SV)]
    rOptGoals :: IORef [Objective (SV, SV)]
    rOptGoals} <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
                       IO [Objective (SV, SV)] -> m [Objective (SV, SV)]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO [Objective (SV, SV)] -> m [Objective (SV, SV)])
    -> IO [Objective (SV, SV)] -> m [Objective (SV, SV)]
    forall a b. (a -> b) -> a -> b
    $ [Objective (SV, SV)] -> [Objective (SV, SV)]
    forall a. [a] -> [a]
    reverse ([Objective (SV, SV)] -> [Objective (SV, SV)])
    -> IO [Objective (SV, SV)] -> IO [Objective (SV, SV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [Objective (SV, SV)] -> IO [Objective (SV, SV)]
    forall a. IORef a -> IO a
    readIORef IORef [Objective (SV, SV)]
    rOptGoals

    -- | Get the program
    getSBVPgm :: (MonadIO m, MonadQuery m) => m SBVPgm
    getSBVPgm :: m SBVPgm
    getSBVPgm = do State{IORef SBVPgm
    spgm :: State -> IORef SBVPgm
    spgm :: IORef SBVPgm
    spgm} <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
                   IO SBVPgm -> m SBVPgm
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO SBVPgm -> m SBVPgm) -> IO SBVPgm -> m SBVPgm
    forall a b. (a -> b) -> a -> b
    $ IORef SBVPgm -> IO SBVPgm
    forall a. IORef a -> IO a
    readIORef IORef SBVPgm
    spgm

    -- | Get the assertions put in via 'Data.SBV.sAssert'
    getSBVAssertions :: (MonadIO m, MonadQuery m) => m [(String, Maybe CallStack, SV)]
    getSBVAssertions :: m [(String, Maybe CallStack, SV)]
    getSBVAssertions = do State{IORef [(String, Maybe CallStack, SV)]
    rAsserts :: State -> IORef [(String, Maybe CallStack, SV)]
    rAsserts :: IORef [(String, Maybe CallStack, SV)]
    rAsserts} <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
                          IO [(String, Maybe CallStack, SV)]
    -> m [(String, Maybe CallStack, SV)]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO [(String, Maybe CallStack, SV)]
     -> m [(String, Maybe CallStack, SV)])
    -> IO [(String, Maybe CallStack, SV)]
    -> m [(String, Maybe CallStack, SV)]
    forall a b. (a -> b) -> a -> b
    $ [(String, Maybe CallStack, SV)] -> [(String, Maybe CallStack, SV)]
    forall a. [a] -> [a]
    reverse ([(String, Maybe CallStack, SV)]
     -> [(String, Maybe CallStack, SV)])
    -> IO [(String, Maybe CallStack, SV)]
    -> IO [(String, Maybe CallStack, SV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [(String, Maybe CallStack, SV)]
    -> IO [(String, Maybe CallStack, SV)]
    forall a. IORef a -> IO a
    readIORef IORef [(String, Maybe CallStack, SV)]
    rAsserts

    -- | Generalization of 'Data.SBV.Control.io'
    io :: MonadIO m => IO a -> m a
    io :: IO a -> m a
    io = IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO

    -- | Sync-up the external solver with new context we have generated
    syncUpSolver :: (MonadIO m, MonadQuery m) => IncState -> m ()
    syncUpSolver :: IncState -> m ()
    syncUpSolver is :: IncState
    is = do
            SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
            [String]
    ls  <- IO [String] -> m [String]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO [String] -> m [String]) -> IO [String] -> m [String]
    forall a b. (a -> b) -> a -> b
    $ do let swap :: (b, a) -> (a, b)
    swap  (a :: b
    a, b :: a
    b)        = (a
    b, b
    a)
                               cmp :: (a, b) -> (a, b) -> Ordering
    cmp   (a :: a
    a, _) (b :: a
    b, _) = a
    a a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` a
    b
                               arrange :: (a, (b, c, b)) -> ((a, b, c), b)
    arrange (i :: a
    i, (at :: b
    at, rt :: c
    rt, es :: b
    es)) = ((a
    i, b
    at, c
    rt), b
    es)
                           [NamedSymVar]
    inps        <- [NamedSymVar] -> [NamedSymVar]
    forall a. [a] -> [a]
    reverse ([NamedSymVar] -> [NamedSymVar])
    -> IO [NamedSymVar] -> IO [NamedSymVar]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [NamedSymVar] -> IO [NamedSymVar]
    forall a. IORef a -> IO a
    readIORef (IncState -> IORef [NamedSymVar]
    rNewInps IncState
    is)
                           KindSet
    ks          <- IORef KindSet -> IO KindSet
    forall a. IORef a -> IO a
    readIORef (IncState -> IORef KindSet
    rNewKinds IncState
    is)
                           [(SV, CV)]
    cnsts       <- ((SV, CV) -> (SV, CV) -> Ordering) -> [(SV, CV)] -> [(SV, CV)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (SV, CV) -> (SV, CV) -> Ordering
    forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
    cmp ([(SV, CV)] -> [(SV, CV)])
    -> (Map CV SV -> [(SV, CV)]) -> Map CV SV -> [(SV, CV)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((CV, SV) -> (SV, CV)) -> [(CV, SV)] -> [(SV, CV)]
    forall a b. (a -> b) -> [a] -> [b]
    map (CV, SV) -> (SV, CV)
    forall b a. (b, a) -> (a, b)
    swap ([(CV, SV)] -> [(SV, CV)])
    -> (Map CV SV -> [(CV, SV)]) -> Map CV SV -> [(SV, CV)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map CV SV -> [(CV, SV)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map CV SV -> [(SV, CV)]) -> IO (Map CV SV) -> IO [(SV, CV)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef (Map CV SV) -> IO (Map CV SV)
    forall a. IORef a -> IO a
    readIORef (IncState -> IORef (Map CV SV)
    rNewConsts IncState
    is)
                           [(Key, ArrayInfo)]
    arrs        <- IntMap ArrayInfo -> [(Key, ArrayInfo)]
    forall a. IntMap a -> [(Key, a)]
    IMap.toAscList (IntMap ArrayInfo -> [(Key, ArrayInfo)])
    -> IO (IntMap ArrayInfo) -> IO [(Key, ArrayInfo)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo)
    forall a. IORef a -> IO a
    readIORef (IncState -> IORef (IntMap ArrayInfo)
    rNewArrs IncState
    is)
                           [((Key, Kind, Kind), [SV])]
    tbls        <- ((Key, (Kind, Kind, [SV])) -> ((Key, Kind, Kind), [SV]))
    -> [(Key, (Kind, Kind, [SV]))] -> [((Key, Kind, Kind), [SV])]
    forall a b. (a -> b) -> [a] -> [b]
    map (Key, (Kind, Kind, [SV])) -> ((Key, Kind, Kind), [SV])
    forall a b c b. (a, (b, c, b)) -> ((a, b, c), b)
    arrange ([(Key, (Kind, Kind, [SV]))] -> [((Key, Kind, Kind), [SV])])
    -> (Map (Kind, Kind, [SV]) Key -> [(Key, (Kind, Kind, [SV]))])
    -> Map (Kind, Kind, [SV]) Key
    -> [((Key, Kind, Kind), [SV])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Key, (Kind, Kind, [SV]))
     -> (Key, (Kind, Kind, [SV])) -> Ordering)
    -> [(Key, (Kind, Kind, [SV]))] -> [(Key, (Kind, Kind, [SV]))]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (Key, (Kind, Kind, [SV])) -> (Key, (Kind, Kind, [SV])) -> Ordering
    forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
    cmp ([(Key, (Kind, Kind, [SV]))] -> [(Key, (Kind, Kind, [SV]))])
    -> (Map (Kind, Kind, [SV]) Key -> [(Key, (Kind, Kind, [SV]))])
    -> Map (Kind, Kind, [SV]) Key
    -> [(Key, (Kind, Kind, [SV]))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (((Kind, Kind, [SV]), Key) -> (Key, (Kind, Kind, [SV])))
    -> [((Kind, Kind, [SV]), Key)] -> [(Key, (Kind, Kind, [SV]))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Kind, Kind, [SV]), Key) -> (Key, (Kind, Kind, [SV]))
    forall b a. (b, a) -> (a, b)
    swap ([((Kind, Kind, [SV]), Key)] -> [(Key, (Kind, Kind, [SV]))])
    -> (Map (Kind, Kind, [SV]) Key -> [((Kind, Kind, [SV]), Key)])
    -> Map (Kind, Kind, [SV]) Key
    -> [(Key, (Kind, Kind, [SV]))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map (Kind, Kind, [SV]) Key -> [((Kind, Kind, [SV]), Key)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map (Kind, Kind, [SV]) Key -> [((Key, Kind, Kind), [SV])])
    -> IO (Map (Kind, Kind, [SV]) Key)
    -> IO [((Key, Kind, Kind), [SV])]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef (Map (Kind, Kind, [SV]) Key)
    -> IO (Map (Kind, Kind, [SV]) Key)
    forall a. IORef a -> IO a
    readIORef (IncState -> IORef (Map (Kind, Kind, [SV]) Key)
    rNewTbls IncState
    is)
                           [(String, SBVType)]
    uis         <- Map String SBVType -> [(String, SBVType)]
    forall k a. Map k a -> [(k, a)]
    Map.toAscList (Map String SBVType -> [(String, SBVType)])
    -> IO (Map String SBVType) -> IO [(String, SBVType)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef (Map String SBVType) -> IO (Map String SBVType)
    forall a. IORef a -> IO a
    readIORef (IncState -> IORef (Map String SBVType)
    rNewUIs IncState
    is)
                           SBVPgm
    as          <- IORef SBVPgm -> IO SBVPgm
    forall a. IORef a -> IO a
    readIORef (IncState -> IORef SBVPgm
    rNewAsgns IncState
    is)
                           Seq (Bool, [(String, String)], SV)
    constraints <- IORef (Seq (Bool, [(String, String)], SV))
    -> IO (Seq (Bool, [(String, String)], SV))
    forall a. IORef a -> IO a
    readIORef (IncState -> IORef (Seq (Bool, [(String, String)], SV))
    rNewConstraints IncState
    is)

                           [String] -> IO [String]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([String] -> IO [String]) -> [String] -> IO [String]
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> SMTLibIncConverter [String]
    toIncSMTLib SMTConfig
    cfg [NamedSymVar]
    inps KindSet
    ks [(SV, CV)]
    cnsts [(Key, ArrayInfo)]
    arrs [((Key, Kind, Kind), [SV])]
    tbls [(String, SBVType)]
    uis SBVPgm
    as Seq (Bool, [(String, String)], SV)
    constraints SMTConfig
    cfg
            (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]
    mergeSExpr [String]
    ls

    -- | Retrieve the query context
    getQueryState :: (MonadIO m, MonadQuery m) => m QueryState
    getQueryState :: m QueryState
    getQueryState = do State
    state <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
                       Maybe QueryState
    mbQS  <- IO (Maybe QueryState) -> m (Maybe QueryState)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO (Maybe QueryState) -> m (Maybe QueryState))
    -> IO (Maybe QueryState) -> m (Maybe QueryState)
    forall a b. (a -> b) -> a -> b
    $ IORef (Maybe QueryState) -> IO (Maybe QueryState)
    forall a. IORef a -> IO a
    readIORef (State -> IORef (Maybe QueryState)
    rQueryState State
    state)
                       case Maybe QueryState
    mbQS of
                         Nothing -> String -> m QueryState
    forall a. HasCallStack => String -> a
    error (String -> m QueryState) -> String -> m QueryState
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                    , "*** Data.SBV: Impossible happened: Query context required in a non-query mode."
                                                    , "Please report this as a bug!"
                                                    ]
                         Just qs :: QueryState
    qs -> QueryState -> m QueryState
    forall (m :: * -> *) a. Monad m => a -> m a
    return QueryState
    qs

    -- | Generalization of 'Data.SBV.Control.modifyQueryState'
    modifyQueryState :: (MonadIO m, MonadQuery m) => (QueryState -> QueryState) -> m ()
    modifyQueryState :: (QueryState -> QueryState) -> m ()
    modifyQueryState f :: QueryState -> QueryState
    f = do State
    state <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
                            Maybe QueryState
    mbQS  <- IO (Maybe QueryState) -> m (Maybe QueryState)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO (Maybe QueryState) -> m (Maybe QueryState))
    -> IO (Maybe QueryState) -> m (Maybe QueryState)
    forall a b. (a -> b) -> a -> b
    $ IORef (Maybe QueryState) -> IO (Maybe QueryState)
    forall a. IORef a -> IO a
    readIORef (State -> IORef (Maybe QueryState)
    rQueryState State
    state)
                            case Maybe QueryState
    mbQS of
                              Nothing -> String -> m ()
    forall a. HasCallStack => String -> a
    error (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                         , "*** Data.SBV: Impossible happened: Query context required in a non-query mode."
                                                         , "Please report this as a bug!"
                                                         ]
                              Just qs :: QueryState
    qs -> let fqs :: QueryState
    fqs = QueryState -> QueryState
    f QueryState
    qs
                                         in QueryState
    fqs QueryState -> m () -> m ()
    forall a b. a -> b -> b
    `seq` IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ IORef (Maybe QueryState) -> Maybe QueryState -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (State -> IORef (Maybe QueryState)
    rQueryState State
    state) (Maybe QueryState -> IO ()) -> Maybe QueryState -> IO ()
    forall a b. (a -> b) -> a -> b
    $ QueryState -> Maybe QueryState
    forall a. a -> Maybe a
    Just QueryState
    fqs

    -- | Generalization of 'Data.SBV.Control.inNewContext'
    inNewContext :: (MonadIO m, MonadQuery m) => (State -> IO a) -> m a
    inNewContext :: (State -> IO a) -> m a
    inNewContext act :: State -> IO a
    act = do State
    st <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
                          (is :: IncState
    is, r :: a
    r) <- IO (IncState, a) -> m (IncState, a)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO (IncState, a) -> m (IncState, a))
    -> IO (IncState, a) -> m (IncState, a)
    forall a b. (a -> b) -> a -> b
    $ State -> (State -> IO a) -> IO (IncState, a)
    forall a. State -> (State -> IO a) -> IO (IncState, a)
    withNewIncState State
    st State -> IO a
    act
                          IncState -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => IncState -> m ()
    syncUpSolver IncState
    is
                          a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r

    -- | Generic 'Queriable' instance for 'SymVal'/'SMTValue' values
    instance (MonadIO m, SymVal a) => Queriable m (SBV a) a where
      create :: QueryT m (SBV a)
    create  = QueryT m (SBV a)
    forall a (m :: * -> *).
    (MonadIO m, MonadQuery m, SymVal a) =>
    m (SBV a)
    freshVar_
      project :: SBV a -> QueryT m a
    project = SBV a -> QueryT m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m, SymVal a) =>
    SBV a -> m a
    getValue
      embed :: a -> QueryT m (SBV a)
    embed   = SBV a -> QueryT m (SBV a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBV a -> QueryT m (SBV a))
    -> (a -> SBV a) -> a -> QueryT m (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal

    -- | Generic 'Queriable' instance for things that are 'Fresh' and look like containers:
    instance (MonadIO m, SymVal a, Foldable t, Traversable t, Fresh m (t (SBV a))) => Queriable m (t (SBV a)) (t a) where
      create :: QueryT m (t (SBV a))
    create  = QueryT m (t (SBV a))
    forall (m :: * -> *) a. Fresh m a => QueryT m a
    fresh
      project :: t (SBV a) -> QueryT m (t a)
    project = (SBV a -> QueryT m a) -> t (SBV a) -> QueryT m (t a)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SBV a -> QueryT m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m, SymVal a) =>
    SBV a -> m a
    getValue
      embed :: t a -> QueryT m (t (SBV a))
    embed   = t (SBV a) -> QueryT m (t (SBV a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (t (SBV a) -> QueryT m (t (SBV a)))
    -> (t a -> t (SBV a)) -> t a -> QueryT m (t (SBV a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> SBV a) -> t a -> t (SBV a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal

    -- | Generalization of 'Data.SBV.Control.freshVar_'
    freshVar_ :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => m (SBV a)
    freshVar_ :: m (SBV a)
    freshVar_ = (State -> IO (SBV a)) -> m (SBV a)
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (State -> IO a) -> m a
    inNewContext ((State -> IO (SBV a)) -> m (SBV a))
    -> (State -> IO (SBV a)) -> m (SBV a)
    forall a b. (a -> b) -> a -> b
    $ (SVal -> SBV a) -> IO SVal -> IO (SBV a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (IO SVal -> IO (SBV a))
    -> (State -> IO SVal) -> State -> IO (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    EX) Kind
    k Maybe String
    forall a. Maybe a
    Nothing
      where k :: Kind
    k = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)

    -- | Generalization of 'Data.SBV.Control.freshVar'
    freshVar :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => String -> m (SBV a)
    freshVar :: String -> m (SBV a)
    freshVar nm :: String
    nm = (State -> IO (SBV a)) -> m (SBV a)
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (State -> IO a) -> m a
    inNewContext ((State -> IO (SBV a)) -> m (SBV a))
    -> (State -> IO (SBV a)) -> m (SBV a)
    forall a b. (a -> b) -> a -> b
    $ (SVal -> SBV a) -> IO SVal -> IO (SBV a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (IO SVal -> IO (SBV a))
    -> (State -> IO SVal) -> State -> IO (SBV a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    EX) Kind
    k (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm)
      where k :: Kind
    k = Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)

    -- | Generalization of 'Data.SBV.Control.freshArray_'
    freshArray_ :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
    freshArray_ :: Maybe (SBV b) -> m (array a b)
    freshArray_ = Maybe String -> Maybe (SBV b) -> m (array a b)
    forall (m :: * -> *) (array :: * -> * -> *) a b.
    (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
    Maybe String -> Maybe (SBV b) -> m (array a b)
    mkFreshArray Maybe String
    forall a. Maybe a
    Nothing

    -- | Generalization of 'Data.SBV.Control.freshArray'
    freshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
    freshArray :: String -> Maybe (SBV b) -> m (array a b)
    freshArray nm :: String
    nm = Maybe String -> Maybe (SBV b) -> m (array a b)
    forall (m :: * -> *) (array :: * -> * -> *) a b.
    (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
    Maybe String -> Maybe (SBV b) -> m (array a b)
    mkFreshArray (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    nm)

    -- | Creating arrays, internal use only.
    mkFreshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> m (array a b)
    mkFreshArray :: Maybe String -> Maybe (SBV b) -> m (array a b)
    mkFreshArray mbNm :: Maybe String
    mbNm mbVal :: Maybe (SBV b)
    mbVal = (State -> IO (array a b)) -> m (array a b)
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    (State -> IO a) -> m a
    inNewContext ((State -> IO (array a b)) -> m (array a b))
    -> (State -> IO (array a b)) -> m (array a b)
    forall a b. (a -> b) -> a -> b
    $ Maybe String -> Maybe (SBV b) -> State -> IO (array a b)
    forall (array :: * -> * -> *) a b.
    (SymArray array, HasKind a, HasKind b) =>
    Maybe String -> Maybe (SBV b) -> State -> IO (array a b)
    newArrayInState Maybe String
    mbNm Maybe (SBV b)
    mbVal

    -- | Generalization of 'Data.SBV.Control.queryDebug'
    queryDebug :: (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug :: [String] -> m ()
    queryDebug msgs :: [String]
    msgs = do QueryState{SMTConfig
    queryConfig :: SMTConfig
    queryConfig :: QueryState -> SMTConfig
    queryConfig} <- m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState
                         IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> [String] -> IO ()
    forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
    debug SMTConfig
    queryConfig [String]
    msgs

    -- | Generalization of 'Data.SBV.Control.ask'
    ask :: (MonadIO m, MonadQuery m) => String -> m String
    ask :: String -> m String
    ask s :: String
    s = do QueryState{Maybe Key -> String -> IO String
    queryAsk :: QueryState -> Maybe Key -> String -> IO String
    queryAsk :: Maybe Key -> String -> IO String
    queryAsk, Maybe Key
    queryTimeOutValue :: QueryState -> Maybe Key
    queryTimeOutValue :: Maybe Key
    queryTimeOutValue} <- m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState

               case Maybe Key
    queryTimeOutValue of
                 Nothing -> [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[SEND] " String -> String -> String
    `alignPlain` String
    s]
                 Just i :: Key
    i  -> [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[SEND, TimeOut: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    showTimeoutValue Key
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "] " String -> String -> String
    `alignPlain` String
    s]
               String
    r <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ Maybe Key -> String -> IO String
    queryAsk Maybe Key
    queryTimeOutValue String
    s
               [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[RECV] " String -> String -> String
    `alignPlain` String
    r]

               String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    r

    -- | Send a string to the solver, and return the response. Except, if the response
    -- is one of the "ignore" ones, keep querying.
    askIgnoring :: (MonadIO m, MonadQuery m) => String -> [String] -> m String
    askIgnoring :: String -> [String] -> m String
    askIgnoring s :: String
    s ignoreList :: [String]
    ignoreList = do

               QueryState{Maybe Key -> String -> IO String
    queryAsk :: Maybe Key -> String -> IO String
    queryAsk :: QueryState -> Maybe Key -> String -> IO String
    queryAsk, Maybe Key -> IO String
    queryRetrieveResponse :: QueryState -> Maybe Key -> IO String
    queryRetrieveResponse :: Maybe Key -> IO String
    queryRetrieveResponse, Maybe Key
    queryTimeOutValue :: Maybe Key
    queryTimeOutValue :: QueryState -> Maybe Key
    queryTimeOutValue} <- m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState

               case Maybe Key
    queryTimeOutValue of
                 Nothing -> [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[SEND] " String -> String -> String
    `alignPlain` String
    s]
                 Just i :: Key
    i  -> [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[SEND, TimeOut: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    showTimeoutValue Key
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "] " String -> String -> String
    `alignPlain` String
    s]
               String
    r <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ Maybe Key -> String -> IO String
    queryAsk Maybe Key
    queryTimeOutValue String
    s
               [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[RECV] " String -> String -> String
    `alignPlain` String
    r]

               let loop :: String -> m String
    loop currentResponse :: String
    currentResponse
                     | String
    currentResponse String -> [String] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [String]
    ignoreList
                     = String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    currentResponse
                     | Bool
    True
                     = do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[WARN] Previous response is explicitly ignored, beware!"]
                          String
    newResponse <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ Maybe Key -> IO String
    queryRetrieveResponse Maybe Key
    queryTimeOutValue
                          [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[RECV] " String -> String -> String
    `alignPlain` String
    newResponse]
                          String -> m String
    loop String
    newResponse

               String -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> m String
    loop String
    r

    -- | Generalization of 'Data.SBV.Control.send'
    send :: (MonadIO m, MonadQuery m) => Bool -> String -> m ()
    send :: Bool -> String -> m ()
    send requireSuccess :: Bool
    requireSuccess s :: String
    s = do

                QueryState{Maybe Key -> String -> IO String
    queryAsk :: Maybe Key -> String -> IO String
    queryAsk :: QueryState -> Maybe Key -> String -> IO String
    queryAsk, Maybe Key -> String -> IO ()
    querySend :: QueryState -> Maybe Key -> String -> IO ()
    querySend :: Maybe Key -> String -> IO ()
    querySend, SMTConfig
    queryConfig :: SMTConfig
    queryConfig :: QueryState -> SMTConfig
    queryConfig, Maybe Key
    queryTimeOutValue :: Maybe Key
    queryTimeOutValue :: QueryState -> Maybe Key
    queryTimeOutValue} <- m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState

                if Bool
    requireSuccess Bool -> Bool -> Bool
    && SolverCapabilities -> Bool
    supportsCustomQueries (SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    queryConfig))
                   then do String
    r <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ Maybe Key -> String -> IO String
    queryAsk Maybe Key
    queryTimeOutValue String
    s

                           case String -> [String]
    words String
    r of
                             ["success"] -> [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[GOOD] " String -> String -> String
    `alignPlain` String
    s]
                             _           -> do case Maybe Key
    queryTimeOutValue of
                                                 Nothing -> [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[FAIL] " String -> String -> String
    `alignPlain` String
    s]
                                                 Just i :: Key
    i  -> [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug [("[FAIL, TimeOut: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    showTimeoutValue Key
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "]  ") String -> String -> String
    `alignPlain` String
    s]

                                               let cmd :: String
    cmd = case String -> [String]
    words ((Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (\c :: Char
    c -> Char -> Bool
    isSpace Char
    c Bool -> Bool -> Bool
    || Char -> Bool
    isPunctuation Char
    c) String
    s) of
                                                           (c :: String
    c:_) -> String
    c
                                                           _     -> "Command"

                                               String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m ()
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected String
    cmd String
    s "success" Maybe [String]
    forall a. Maybe a
    Nothing String
    r Maybe [String]
    forall a. Maybe a
    Nothing

                   else do -- fire and forget. if you use this, you're on your own!
                           [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[FIRE] " String -> String -> String
    `alignPlain` String
    s]
                           IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Maybe Key -> String -> IO ()
    querySend Maybe Key
    queryTimeOutValue String
    s

    -- | Generalization of 'Data.SBV.Control.retrieveResponse'
    retrieveResponse :: (MonadIO m, MonadQuery m) => String -> Maybe Int -> m [String]
    retrieveResponse :: String -> Maybe Key -> m [String]
    retrieveResponse userTag :: String
    userTag mbTo :: Maybe Key
    mbTo = do
                 String
    ts  <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (ZonedTime -> String
    forall a. Show a => a -> String
    show (ZonedTime -> String) -> IO ZonedTime -> IO String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO ZonedTime
    getZonedTime)

                 let synchTag :: String
    synchTag = String -> String
    forall a. Show a => a -> String
    show (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    userTag String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " (at: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ts String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                     cmd :: String
    cmd = "(echo " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    synchTag String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

                 [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[SYNC] Attempting to synchronize with tag: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    synchTag]

                 Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    False String
    cmd

                 QueryState{Maybe Key -> IO String
    queryRetrieveResponse :: Maybe Key -> IO String
    queryRetrieveResponse :: QueryState -> Maybe Key -> IO String
    queryRetrieveResponse} <- m QueryState
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
    getQueryState

                 let loop :: [String] -> m [String]
    loop sofar :: [String]
    sofar = do
                      String
    s <- IO String -> m String
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO String -> m String) -> IO String -> m String
    forall a b. (a -> b) -> a -> b
    $ Maybe Key -> IO String
    queryRetrieveResponse Maybe Key
    mbTo

                      -- strictly speaking SMTLib requires solvers to print quotes around
                      -- echo'ed strings, but they don't always do. Accommodate for that
                      -- here, though I wish we didn't have to.
                      if String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    synchTag Bool -> Bool -> Bool
    || String -> String
    forall a. Show a => a -> String
    show String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    synchTag
                         then do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[SYNC] Synchronization achieved using tag: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    synchTag]
                                 [String] -> m [String]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([String] -> m [String]) -> [String] -> m [String]
    forall a b. (a -> b) -> a -> b
    $ [String] -> [String]
    forall a. [a] -> [a]
    reverse [String]
    sofar
                         else do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["[RECV] " String -> String -> String
    `alignPlain` String
    s]
                                 [String] -> m [String]
    loop (String
    s String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)

                 [String] -> m [String]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [String] -> m [String]
    loop []

    -- | Generalization of 'Data.SBV.Control.getValue'
    getValue :: (MonadIO m, MonadQuery m, SymVal a) => SBV a -> m a
    getValue :: SBV a -> m a
    getValue s :: SBV a
    s = 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
    s)
                    CV
    cv <- Maybe Key -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> SV -> m CV
    getValueCV Maybe Key
    forall a. Maybe a
    Nothing SV
    sv
                    a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> m a) -> a -> m a
    forall a b. (a -> b) -> a -> b
    $ CV -> a
    forall a. SymVal a => CV -> a
    fromCV CV
    cv

    -- | A class which allows for sexpr-conversion to functions
    class (HasKind r, SatModel r) => SMTFunction fun a r | fun -> a r where
      sexprToArg     :: fun -> [SExpr] -> Maybe a
      smtFunName     :: (MonadIO m, SolverContext m, MonadSymbolic m) => fun -> m String
      smtFunSaturate :: fun -> SBV r
      smtFunType     :: fun -> SBVType
      smtFunDefault  :: fun -> Maybe r
      sexprToFun     :: (MonadIO m, SolverContext m, MonadQuery m, MonadSymbolic m, SymVal r) => fun -> SExpr -> m (Maybe ([(a, r)], r))

      {-# MINIMAL sexprToArg, smtFunSaturate, smtFunType  #-}

      -- Given the function, figure out a default "return value"
      smtFunDefault _
        | Just v :: CV
    v <- Kind -> Maybe CV
    defaultKindedValue (Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)), Just (res :: r
    res, []) <- [CV] -> Maybe (r, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV
    v]
        = r -> Maybe r
    forall a. a -> Maybe a
    Just r
    res
        | Bool
    True
        = Maybe r
    forall a. Maybe a
    Nothing

      -- Given the function, determine what its name is and do some sanity checks
      smtFunName f :: fun
    f = do st :: State
    st@State{IORef (Map String SBVType)
    rUIMap :: State -> IORef (Map String SBVType)
    rUIMap :: IORef (Map String SBVType)
    rUIMap} <- m State
    forall (m :: * -> *). SolverContext m => m State
    contextState
                        Map String SBVType
    uiMap <- IO (Map String SBVType) -> m (Map String SBVType)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Map String SBVType) -> m (Map String SBVType))
    -> IO (Map String SBVType) -> m (Map String SBVType)
    forall a b. (a -> b) -> a -> b
    $ IORef (Map String SBVType) -> IO (Map String SBVType)
    forall a. IORef a -> IO a
    readIORef IORef (Map String SBVType)
    rUIMap
                        State -> Map String SBVType -> m String
    forall (m :: * -> *) b.
    MonadIO m =>
    State -> Map String b -> m String
    findName State
    st Map String SBVType
    uiMap
        where findName :: State -> Map String b -> m String
    findName st :: State
    st@State{IORef SBVPgm
    spgm :: IORef SBVPgm
    spgm :: State -> IORef SBVPgm
    spgm} uiMap :: Map String b
    uiMap = do
                 SV
    r <- IO SV -> m SV
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SV -> m SV) -> IO SV -> m SV
    forall a b. (a -> b) -> a -> b
    $ State -> SBV r -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st (fun -> SBV r
    forall fun a r. SMTFunction fun a r => fun -> SBV r
    smtFunSaturate fun
    f)
                 IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ SV -> IO ()
    forceSVArg SV
    r
                 SBVPgm asgns :: Seq (SV, SBVExpr)
    asgns <- IO SBVPgm -> m SBVPgm
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBVPgm -> m SBVPgm) -> IO SBVPgm -> m SBVPgm
    forall a b. (a -> b) -> a -> b
    $ IORef SBVPgm -> IO SBVPgm
    forall a. IORef a -> IO a
    readIORef IORef SBVPgm
    spgm

                 let cantFind :: a
    cantFind = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $    [ ""
                                                     , "*** Data.SBV.getFunction: Must be called on an uninterpreted function!"
                                                     , "***"
                                                     , "***    Expected to receive a function created by \"uninterpret\""
                                                     ]
                                                  [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    tag
                                                  [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "***"
                                                     , "*** Make sure to call getFunction on uninterpreted functions only!"
                                                     , "*** If that is already the case, please report this as a bug."
                                                     ]
                          where tag :: [String]
    tag = case ((String, b) -> String) -> [(String, b)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, b) -> String
    forall a b. (a, b) -> a
    fst (Map String b -> [(String, b)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map String b
    uiMap) of
                                        []    -> [ "***    But, there are no matching uninterpreted functions in the context." ]
                                        [x :: String
    x]   -> [ "***    The only possible candidate is: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x ]
                                        cands :: [String]
    cands -> [ "***    Candidates are:"
                                                 , "***        " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    cands
                                                 ]

                 case ((SV, SBVExpr) -> Bool) -> Seq (SV, SBVExpr) -> Maybe Key
    forall a. (a -> Bool) -> Seq a -> Maybe Key
    S.findIndexR ((SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    r) (SV -> Bool) -> ((SV, SBVExpr) -> SV) -> (SV, SBVExpr) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SV, SBVExpr) -> SV
    forall a b. (a, b) -> a
    fst) Seq (SV, SBVExpr)
    asgns of
                   Nothing -> m String
    forall a. a
    cantFind
                   Just i :: Key
    i  -> case Seq (SV, SBVExpr)
    asgns Seq (SV, SBVExpr) -> Key -> (SV, SBVExpr)
    forall a. Seq a -> Key -> a
    `S.index` Key
    i of
                                (sv :: SV
    sv, SBVApp (Uninterpreted nm :: String
    nm) _) | SV
    r SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    sv -> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    nm
                                _                                           -> m String
    forall a. a
    cantFind

      sexprToFun f :: fun
    f e :: SExpr
    e = do String
    nm <- fun -> m String
    forall fun a r (m :: * -> *).
    (SMTFunction fun a r, MonadIO m, SolverContext m,
     MonadSymbolic m) =>
    fun -> m String
    smtFunName fun
    f
                          case SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    parseSExprFunction SExpr
    e of
                            Just (Left nm' :: String
    nm') -> case (String
    nm String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm', fun -> Maybe r
    forall fun a r. SMTFunction fun a r => fun -> Maybe r
    smtFunDefault fun
    f) of
                                                 (True, Just v :: r
    v)  -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
    -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
    forall a b. (a -> b) -> a -> b
    $ ([(a, r)], r) -> Maybe ([(a, r)], r)
    forall a. a -> Maybe a
    Just ([], r
    v)
                                                 _               -> String -> m (Maybe ([(a, r)], r))
    forall a a. Show a => a -> a
    bailOut String
    nm
                            Just (Right v :: ([([SExpr], SExpr)], SExpr)
    v)  -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
    -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
    forall a b. (a -> b) -> a -> b
    $ ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
    forall (t :: * -> *) a r a a.
    (Traversable t, SMTFunction fun a r, SymVal a, SymVal a) =>
    (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
    convert ([([SExpr], SExpr)], SExpr)
    v
                            Nothing         -> do Maybe ([([SExpr], SExpr)], SExpr)
    mbPVS <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
    pointWiseExtract String
    nm (fun -> SBVType
    forall fun a r. SMTFunction fun a r => fun -> SBVType
    smtFunType fun
    f)
                                                  Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
    -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
    forall a b. (a -> b) -> a -> b
    $ Maybe ([([SExpr], SExpr)], SExpr)
    mbPVS Maybe ([([SExpr], SExpr)], SExpr)
    -> (([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r))
    -> Maybe ([(a, r)], r)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
    forall (t :: * -> *) a r a a.
    (Traversable t, SMTFunction fun a r, SymVal a, SymVal a) =>
    (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
    convert
        where convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
    convert    (vs :: t ([SExpr], SExpr)
    vs, d :: SExpr
    d) = (,) (t (a, a) -> a -> (t (a, a), a))
    -> Maybe (t (a, a)) -> Maybe (a -> (t (a, a), a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (([SExpr], SExpr) -> Maybe (a, a))
    -> t ([SExpr], SExpr) -> Maybe (t (a, a))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ([SExpr], SExpr) -> Maybe (a, a)
    forall a r a.
    (SMTFunction fun a r, SymVal a) =>
    ([SExpr], SExpr) -> Maybe (a, a)
    sexprPoint t ([SExpr], SExpr)
    vs Maybe (a -> (t (a, a), a)) -> Maybe a -> Maybe (t (a, a), a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    d
              sexprPoint :: ([SExpr], SExpr) -> Maybe (a, a)
    sexprPoint (as :: [SExpr]
    as, v :: SExpr
    v) = (,) (a -> a -> (a, a)) -> Maybe a -> Maybe (a -> (a, a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> fun -> [SExpr] -> Maybe a
    forall fun a r. SMTFunction fun a r => fun -> [SExpr] -> Maybe a
    sexprToArg fun
    f [SExpr]
    as    Maybe (a -> (a, a)) -> Maybe a -> Maybe (a, a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    v

              bailOut :: a -> a
    bailOut nm :: a
    nm = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                           , "*** Data.SBV.getFunction: Unable to extract an interpretation for function " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    nm
                                           , "***"
                                           , "*** Failed while trying to extract a pointwise interpretation."
                                           , "***"
                                           , "*** This could be a bug with SBV or the backend solver. Please report!"
                                           ]

    -- | Registering an uninterpreted SMT function. This is typically not necessary as uses of the UI
    -- function itself will register it automatically. But there are cases where doing this explicitly can
    -- come in handy.
    registerUISMTFunction :: (MonadIO m, SolverContext m, MonadSymbolic m) => SMTFunction fun a r => fun -> m ()
    registerUISMTFunction :: fun -> m ()
    registerUISMTFunction f :: fun
    f = do State
    st <- m State
    forall (m :: * -> *). SolverContext m => m State
    contextState
                                 String
    nm <- fun -> m String
    forall fun a r (m :: * -> *).
    (SMTFunction fun a r, MonadIO m, SolverContext m,
     MonadSymbolic m) =>
    fun -> m String
    smtFunName fun
    f
                                 IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ State -> String -> SBVType -> Maybe [String] -> IO ()
    newUninterpreted State
    st String
    nm (fun -> SBVType
    forall fun a r. SMTFunction fun a r => fun -> SBVType
    smtFunType fun
    f) Maybe [String]
    forall a. Maybe a
    Nothing

    -- | Pointwise function value extraction. If we get unlucky and can't parse z3's output (happens
    -- when we have all booleans and z3 decides to spit out an expression), just brute force our
    -- way out of it. Note that we only do this if we have a pure boolean type, as otherwise we'd blow
    -- up. And I think it'll only be necessary then, I haven't seen z3 try anything smarter in other scenarios.
    pointWiseExtract ::  forall m. (MonadIO m, MonadQuery m) => String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
    pointWiseExtract :: String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
    pointWiseExtract nm :: String
    nm typ :: SBVType
    typ
       | Bool
    isBoolFunc
       = m (Maybe ([([SExpr], SExpr)], SExpr))
    tryPointWise
       | Bool
    True
       = String -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall a. HasCallStack => String -> a
    error (String -> m (Maybe ([([SExpr], SExpr)], SExpr)))
    -> String -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                         , "*** Data.SBV.getFunction: Unsupported: Extracting interpretation for function:"
                         , "***"
                         , "***     " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVType -> String
    forall a. Show a => a -> String
    show SBVType
    typ
                         , "***"
                         , "*** At this time, the expression returned by the solver is too complicated for SBV!"
                         , "***"
                         , "*** You can ignore uninterpreted function models for sat models using the 'satTrackUFs' parameter:"
                         , "***"
                         , "***             satWith    z3{satTrackUFs = False}"
                         , "***             allSatWith z3{satTrackUFs = False}"
                         , "***"
                         , "*** You can see the response from the solver by running with '{verbose = True}' option."
                         , "***"
                         , "*** NB. If this is a use case you'd like SBV to support, please get in touch!"
                         ]
      where trueSExpr :: SExpr
    trueSExpr  = (Integer, Maybe Key) -> SExpr
    ENum (1, Maybe Key
    forall a. Maybe a
    Nothing)
            falseSExpr :: SExpr
    falseSExpr = (Integer, Maybe Key) -> SExpr
    ENum (0, Maybe Key
    forall a. Maybe a
    Nothing)

            isTrueSExpr :: SExpr -> Bool
    isTrueSExpr (ENum (1, Nothing)) = Bool
    True
            isTrueSExpr (ENum (0, Nothing)) = Bool
    False
            isTrueSExpr s :: SExpr
    s                   = String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.pointWiseExtract: Impossible happened: Received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    s

            (nArgs :: Key
    nArgs, isBoolFunc :: Bool
    isBoolFunc) = case SBVType
    typ of
                                    SBVType ts :: [Kind]
    ts -> ([Kind] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [Kind]
    ts Key -> Key -> Key
    forall a. Num a => a -> a -> a
    - 1, (Kind -> Bool) -> [Kind] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KBool) [Kind]
    ts)

            getBVal :: [SExpr] -> m ([SExpr], SExpr)
            getBVal :: [SExpr] -> m ([SExpr], SExpr)
    getBVal args :: [SExpr]
    args = do let shc :: SExpr -> String
    shc c :: SExpr
    c | SExpr -> Bool
    isTrueSExpr SExpr
    c = "true"
                                        | Bool
    True          = "false"

                                  as :: String
    as = [String] -> String
    unwords ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ (SExpr -> String) -> [SExpr] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map SExpr -> String
    shc [SExpr]
    args

                                  cmd :: String
    cmd   = "(get-value ((" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    as String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")))"

                                  bad :: String -> Maybe [String] -> m a
    bad   = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "get-value" String
    cmd ("pointwise value of boolean function " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " on " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    as) 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 ([SExpr], SExpr))
    -> (SExpr -> m ([SExpr], SExpr))
    -> m ([SExpr], SExpr)
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m ([SExpr], SExpr)
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m ([SExpr], SExpr)) -> m ([SExpr], SExpr))
    -> (SExpr -> m ([SExpr], SExpr)) -> m ([SExpr], SExpr)
    forall a b. (a -> b) -> a -> b
    $ \case EApp [EApp [_, e :: SExpr
    e]] -> ([SExpr], SExpr) -> m ([SExpr], SExpr)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([SExpr]
    args, SExpr
    e)
                                                  _                  -> String -> Maybe [String] -> m ([SExpr], SExpr)
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

            getBVals :: m [([SExpr], SExpr)]
            getBVals :: m [([SExpr], SExpr)]
    getBVals = ([SExpr] -> m ([SExpr], SExpr))
    -> [[SExpr]] -> m [([SExpr], SExpr)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM [SExpr] -> m ([SExpr], SExpr)
    getBVal ([[SExpr]] -> m [([SExpr], SExpr)])
    -> [[SExpr]] -> m [([SExpr], SExpr)]
    forall a b. (a -> b) -> a -> b
    $ Key -> [SExpr] -> [[SExpr]]
    forall (m :: * -> *) a. Applicative m => Key -> m a -> m [a]
    replicateM Key
    nArgs [SExpr
    falseSExpr, SExpr
    trueSExpr]

            tryPointWise :: m (Maybe ([([SExpr], SExpr)], SExpr))
    tryPointWise
              | Bool -> Bool
    not Bool
    isBoolFunc
              = Maybe ([([SExpr], SExpr)], SExpr)
    -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ([([SExpr], SExpr)], SExpr)
    forall a. Maybe a
    Nothing
              | Key
    nArgs Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    < 1
              = String -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall a. HasCallStack => String -> a
    error (String -> m (Maybe ([([SExpr], SExpr)], SExpr)))
    -> String -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.pointWiseExtract: Impossible happened, nArgs < 1: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    nArgs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " type: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVType -> String
    forall a. Show a => a -> String
    show SBVType
    typ
              | Bool
    True
              = do [([SExpr], SExpr)]
    vs <- m [([SExpr], SExpr)]
    getBVals
                   -- Pick the value that will give us the fewer entries
                   let (trues :: [([SExpr], SExpr)]
    trues, falses :: [([SExpr], SExpr)]
    falses) = (([SExpr], SExpr) -> Bool)
    -> [([SExpr], SExpr)] -> ([([SExpr], SExpr)], [([SExpr], SExpr)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (\(_, v :: SExpr
    v) -> SExpr -> Bool
    isTrueSExpr SExpr
    v) [([SExpr], SExpr)]
    vs
                   Maybe ([([SExpr], SExpr)], SExpr)
    -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ([([SExpr], SExpr)], SExpr)
     -> m (Maybe ([([SExpr], SExpr)], SExpr)))
    -> Maybe ([([SExpr], SExpr)], SExpr)
    -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall a b. (a -> b) -> a -> b
    $ ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
    forall a. a -> Maybe a
    Just (([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr))
    -> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
    forall a b. (a -> b) -> a -> b
    $ if [([SExpr], SExpr)] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [([SExpr], SExpr)]
    trues Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    <= [([SExpr], SExpr)] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [([SExpr], SExpr)]
    falses
                                   then ([([SExpr], SExpr)]
    trues,  SExpr
    falseSExpr)
                                   else ([([SExpr], SExpr)]
    falses, SExpr
    trueSExpr)

    -- | For saturation purposes, get a proper argument. The forall quantification
    -- is safe here since we only use in smtFunSaturate calls, which looks at the
    -- kind stored inside only.
    mkArg :: forall a. Kind -> SBV a
    mkArg :: Kind -> SBV a
    mkArg k :: Kind
    k = case Kind -> Maybe CV
    defaultKindedValue Kind
    k of
                Nothing -> String -> SBV a
    forall a. HasCallStack => String -> a
    error (String -> SBV a) -> String -> SBV a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                           , "*** Data.SBV.smtFunSaturate: Impossible happened!"
                                           , "*** Unable to create a valid parameter for kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                           , "*** Please report this as an SBV bug!"
                                           ]
                Just c :: CV
    c -> SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left CV
    c)

    -- | Functions of arity 1
    instance ( SymVal a, HasKind a
             , SatModel r, HasKind r
             ) => SMTFunction (SBV a -> SBV r) a r
             where
      sexprToArg :: (SBV a -> SBV r) -> [SExpr] -> Maybe a
    sexprToArg _ [a0 :: SExpr
    a0] = SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a0
      sexprToArg _ _    = Maybe a
    forall a. Maybe a
    Nothing

      smtFunType :: (SBV a -> SBV r) -> SBVType
    smtFunType _ = [Kind] -> SBVType
    SBVType [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)]

      smtFunSaturate :: (SBV a -> SBV r) -> SBV r
    smtFunSaturate f :: SBV a -> SBV r
    f = SBV a -> SBV r
    f (SBV a -> SBV r) -> SBV a -> SBV r
    forall a b. (a -> b) -> a -> b
    $ Kind -> SBV a
    forall a. Kind -> SBV a
    mkArg (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a))

    -- | Functions of arity 2
    instance ( SymVal a,  HasKind a
             , SymVal b,  HasKind b
             , SatModel r, HasKind r
             ) => SMTFunction (SBV a -> SBV b -> SBV r) (a, b) r
             where
      sexprToArg :: (SBV a -> SBV b -> SBV r) -> [SExpr] -> Maybe (a, b)
    sexprToArg _ [a0 :: SExpr
    a0, a1 :: SExpr
    a1] = (,) (a -> b -> (a, b)) -> Maybe a -> Maybe (b -> (a, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a0 Maybe (b -> (a, b)) -> Maybe b -> Maybe (a, b)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe b
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a1
      sexprToArg _ _        = Maybe (a, b)
    forall a. Maybe a
    Nothing

      smtFunType :: (SBV a -> SBV b -> SBV r) -> SBVType
    smtFunType _ = [Kind] -> SBVType
    SBVType [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)]

      smtFunSaturate :: (SBV a -> SBV b -> SBV r) -> SBV r
    smtFunSaturate f :: SBV a -> SBV b -> SBV r
    f = SBV a -> SBV b -> SBV r
    f (Kind -> SBV a
    forall a. Kind -> SBV a
    mkArg (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)))
                           (Kind -> SBV b
    forall a. Kind -> SBV a
    mkArg (Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)))

    -- | Functions of arity 3
    instance ( SymVal a,   HasKind a
             , SymVal b,   HasKind b
             , SymVal c,   HasKind c
             , SatModel r, HasKind r
             ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV r) (a, b, c) r
             where
      sexprToArg :: (SBV a -> SBV b -> SBV c -> SBV r) -> [SExpr] -> Maybe (a, b, c)
    sexprToArg _ [a0 :: SExpr
    a0, a1 :: SExpr
    a1, a2 :: SExpr
    a2] = (,,) (a -> b -> c -> (a, b, c))
    -> Maybe a -> Maybe (b -> c -> (a, b, c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a0 Maybe (b -> c -> (a, b, c)) -> Maybe b -> Maybe (c -> (a, b, c))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe b
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a1 Maybe (c -> (a, b, c)) -> Maybe c -> Maybe (a, b, c)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe c
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a2
      sexprToArg _ _            = Maybe (a, b, c)
    forall a. Maybe a
    Nothing

      smtFunType :: (SBV a -> SBV b -> SBV c -> SBV r) -> SBVType
    smtFunType _ = [Kind] -> SBVType
    SBVType [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)]

      smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV r) -> SBV r
    smtFunSaturate f :: SBV a -> SBV b -> SBV c -> SBV r
    f = SBV a -> SBV b -> SBV c -> SBV r
    f (Kind -> SBV a
    forall a. Kind -> SBV a
    mkArg (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)))
                           (Kind -> SBV b
    forall a. Kind -> SBV a
    mkArg (Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)))
                           (Kind -> SBV c
    forall a. Kind -> SBV a
    mkArg (Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)))

    -- | Functions of arity 4
    instance ( SymVal a,   HasKind a
             , SymVal b,   HasKind b
             , SymVal c,   HasKind c
             , SymVal d,   HasKind d
             , SatModel r, HasKind r
             ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV r) (a, b, c, d) r
             where
      sexprToArg :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV r)
    -> [SExpr] -> Maybe (a, b, c, d)
    sexprToArg _ [a0 :: SExpr
    a0, a1 :: SExpr
    a1, a2 :: SExpr
    a2, a3 :: SExpr
    a3] = (,,,) (a -> b -> c -> d -> (a, b, c, d))
    -> Maybe a -> Maybe (b -> c -> d -> (a, b, c, d))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a0 Maybe (b -> c -> d -> (a, b, c, d))
    -> Maybe b -> Maybe (c -> d -> (a, b, c, d))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe b
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a1 Maybe (c -> d -> (a, b, c, d))
    -> Maybe c -> Maybe (d -> (a, b, c, d))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe c
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a2 Maybe (d -> (a, b, c, d)) -> Maybe d -> Maybe (a, b, c, d)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe d
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a3
      sexprToArg _ _               = Maybe (a, b, c, d)
    forall a. Maybe a
    Nothing

      smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV r) -> SBVType
    smtFunType _ = [Kind] -> SBVType
    SBVType [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)]

      smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV r) -> SBV r
    smtFunSaturate f :: SBV a -> SBV b -> SBV c -> SBV d -> SBV r
    f = SBV a -> SBV b -> SBV c -> SBV d -> SBV r
    f (Kind -> SBV a
    forall a. Kind -> SBV a
    mkArg (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)))
                           (Kind -> SBV b
    forall a. Kind -> SBV a
    mkArg (Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)))
                           (Kind -> SBV c
    forall a. Kind -> SBV a
    mkArg (Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)))
                           (Kind -> SBV d
    forall a. Kind -> SBV a
    mkArg (Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d)))

    -- | Functions of arity 5
    instance ( SymVal a,   HasKind a
             , SymVal b,   HasKind b
             , SymVal c,   HasKind c
             , SymVal d,   HasKind d
             , SymVal e,   HasKind e
             , SatModel r, HasKind r
             ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) (a, b, c, d, e) r
             where
      sexprToArg :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r)
    -> [SExpr] -> Maybe (a, b, c, d, e)
    sexprToArg _ [a0 :: SExpr
    a0, a1 :: SExpr
    a1, a2 :: SExpr
    a2, a3 :: SExpr
    a3, a4 :: SExpr
    a4] = (,,,,) (a -> b -> c -> d -> e -> (a, b, c, d, e))
    -> Maybe a -> Maybe (b -> c -> d -> e -> (a, b, c, d, e))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a0 Maybe (b -> c -> d -> e -> (a, b, c, d, e))
    -> Maybe b -> Maybe (c -> d -> e -> (a, b, c, d, e))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe b
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a1 Maybe (c -> d -> e -> (a, b, c, d, e))
    -> Maybe c -> Maybe (d -> e -> (a, b, c, d, e))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe c
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a2 Maybe (d -> e -> (a, b, c, d, e))
    -> Maybe d -> Maybe (e -> (a, b, c, d, e))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe d
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a3 Maybe (e -> (a, b, c, d, e)) -> Maybe e -> Maybe (a, b, c, d, e)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe e
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a4
      sexprToArg _ _                    = Maybe (a, b, c, d, e)
    forall a. Maybe a
    Nothing

      smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) -> SBVType
    smtFunType _ = [Kind] -> SBVType
    SBVType [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e), Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)]

      smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) -> SBV r
    smtFunSaturate f :: SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r
    f = SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r
    f (Kind -> SBV a
    forall a. Kind -> SBV a
    mkArg (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)))
                           (Kind -> SBV b
    forall a. Kind -> SBV a
    mkArg (Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)))
                           (Kind -> SBV c
    forall a. Kind -> SBV a
    mkArg (Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)))
                           (Kind -> SBV d
    forall a. Kind -> SBV a
    mkArg (Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d)))
                           (Kind -> SBV e
    forall a. Kind -> SBV a
    mkArg (Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e)))

    -- | Functions of arity 6
    instance ( SymVal a,   HasKind a
             , SymVal b,   HasKind b
             , SymVal c,   HasKind c
             , SymVal d,   HasKind d
             , SymVal e,   HasKind e
             , SymVal f,   HasKind f
             , SatModel r, HasKind r
             ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r) (a, b, c, d, e, f) r
             where
      sexprToArg :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
    -> [SExpr] -> Maybe (a, b, c, d, e, f)
    sexprToArg _ [a0 :: SExpr
    a0, a1 :: SExpr
    a1, a2 :: SExpr
    a2, a3 :: SExpr
    a3, a4 :: SExpr
    a4, a5 :: SExpr
    a5] = (,,,,,) (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
    -> Maybe a -> Maybe (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a0 Maybe (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
    -> Maybe b -> Maybe (c -> d -> e -> f -> (a, b, c, d, e, f))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe b
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a1 Maybe (c -> d -> e -> f -> (a, b, c, d, e, f))
    -> Maybe c -> Maybe (d -> e -> f -> (a, b, c, d, e, f))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe c
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a2 Maybe (d -> e -> f -> (a, b, c, d, e, f))
    -> Maybe d -> Maybe (e -> f -> (a, b, c, d, e, f))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe d
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a3 Maybe (e -> f -> (a, b, c, d, e, f))
    -> Maybe e -> Maybe (f -> (a, b, c, d, e, f))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe e
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a4 Maybe (f -> (a, b, c, d, e, f))
    -> Maybe f -> Maybe (a, b, c, d, e, f)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe f
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a5
      sexprToArg _ _                        = Maybe (a, b, c, d, e, f)
    forall a. Maybe a
    Nothing

      smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
    -> SBVType
    smtFunType _ = [Kind] -> SBVType
    SBVType [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    forall k (t :: k). Proxy t
    Proxy @f), Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)]

      smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
    -> SBV r
    smtFunSaturate f :: SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
    f = SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
    f (Kind -> SBV a
    forall a. Kind -> SBV a
    mkArg (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)))
                           (Kind -> SBV b
    forall a. Kind -> SBV a
    mkArg (Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)))
                           (Kind -> SBV c
    forall a. Kind -> SBV a
    mkArg (Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)))
                           (Kind -> SBV d
    forall a. Kind -> SBV a
    mkArg (Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d)))
                           (Kind -> SBV e
    forall a. Kind -> SBV a
    mkArg (Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e)))
                           (Kind -> SBV f
    forall a. Kind -> SBV a
    mkArg (Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    forall k (t :: k). Proxy t
    Proxy @f)))

    -- | Functions of arity 7
    instance ( SymVal a,   HasKind a
             , SymVal b,   HasKind b
             , SymVal c,   HasKind c
             , SymVal d,   HasKind d
             , SymVal e,   HasKind e
             , SymVal f,   HasKind f
             , SymVal g,   HasKind g
             , SatModel r, HasKind r
             ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r) (a, b, c, d, e, f, g) r
             where
      sexprToArg :: (SBV a
     -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
    -> [SExpr] -> Maybe (a, b, c, d, e, f, g)
    sexprToArg _ [a0 :: SExpr
    a0, a1 :: SExpr
    a1, a2 :: SExpr
    a2, a3 :: SExpr
    a3, a4 :: SExpr
    a4, a5 :: SExpr
    a5, a6 :: SExpr
    a6] = (,,,,,,) (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
    -> Maybe a
    -> Maybe (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a0 Maybe (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
    -> Maybe b
    -> Maybe (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe b
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a1 Maybe (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
    -> Maybe c -> Maybe (d -> e -> f -> g -> (a, b, c, d, e, f, g))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe c
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a2 Maybe (d -> e -> f -> g -> (a, b, c, d, e, f, g))
    -> Maybe d -> Maybe (e -> f -> g -> (a, b, c, d, e, f, g))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe d
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a3 Maybe (e -> f -> g -> (a, b, c, d, e, f, g))
    -> Maybe e -> Maybe (f -> g -> (a, b, c, d, e, f, g))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe e
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a4 Maybe (f -> g -> (a, b, c, d, e, f, g))
    -> Maybe f -> Maybe (g -> (a, b, c, d, e, f, g))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe f
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a5 Maybe (g -> (a, b, c, d, e, f, g))
    -> Maybe g -> Maybe (a, b, c, d, e, f, g)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe g
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a6
      sexprToArg _ _                            = Maybe (a, b, c, d, e, f, g)
    forall a. Maybe a
    Nothing

      smtFunType :: (SBV a
     -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
    -> SBVType
    smtFunType _ = [Kind] -> SBVType
    SBVType [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    forall k (t :: k). Proxy t
    Proxy @f), Proxy g -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy g
    forall k (t :: k). Proxy t
    Proxy @g), Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)]

      smtFunSaturate :: (SBV a
     -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
    -> SBV r
    smtFunSaturate f :: SBV a
    -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r
    f = SBV a
    -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r
    f (Kind -> SBV a
    forall a. Kind -> SBV a
    mkArg (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)))
                           (Kind -> SBV b
    forall a. Kind -> SBV a
    mkArg (Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)))
                           (Kind -> SBV c
    forall a. Kind -> SBV a
    mkArg (Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)))
                           (Kind -> SBV d
    forall a. Kind -> SBV a
    mkArg (Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d)))
                           (Kind -> SBV e
    forall a. Kind -> SBV a
    mkArg (Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e)))
                           (Kind -> SBV f
    forall a. Kind -> SBV a
    mkArg (Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    forall k (t :: k). Proxy t
    Proxy @f)))
                           (Kind -> SBV g
    forall a. Kind -> SBV a
    mkArg (Proxy g -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy g
    forall k (t :: k). Proxy t
    Proxy @g)))

    -- | Functions of arity 8
    instance ( SymVal a,   HasKind a
             , SymVal b,   HasKind b
             , SymVal c,   HasKind c
             , SymVal d,   HasKind d
             , SymVal e,   HasKind e
             , SymVal f,   HasKind f
             , SymVal g,   HasKind g
             , SymVal h,   HasKind h
             , SatModel r, HasKind r
             ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> SBV r) (a, b, c, d, e, f, g, h) r
             where
      sexprToArg :: (SBV a
     -> SBV b
     -> SBV c
     -> SBV d
     -> SBV e
     -> SBV f
     -> SBV g
     -> SBV h
     -> SBV r)
    -> [SExpr] -> Maybe (a, b, c, d, e, f, g, h)
    sexprToArg _ [a0 :: SExpr
    a0, a1 :: SExpr
    a1, a2 :: SExpr
    a2, a3 :: SExpr
    a3, a4 :: SExpr
    a4, a5 :: SExpr
    a5, a6 :: SExpr
    a6, a7 :: SExpr
    a7] = (,,,,,,,) (a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    -> Maybe a
    -> Maybe
         (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a0 Maybe (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    -> Maybe b
    -> Maybe (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe b
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a1 Maybe (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    -> Maybe c
    -> Maybe (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe c
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a2 Maybe (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    -> Maybe d -> Maybe (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe d
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a3 Maybe (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
    -> Maybe e -> Maybe (f -> g -> h -> (a, b, c, d, e, f, g, h))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe e
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a4 Maybe (f -> g -> h -> (a, b, c, d, e, f, g, h))
    -> Maybe f -> Maybe (g -> h -> (a, b, c, d, e, f, g, h))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe f
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a5 Maybe (g -> h -> (a, b, c, d, e, f, g, h))
    -> Maybe g -> Maybe (h -> (a, b, c, d, e, f, g, h))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe g
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a6 Maybe (h -> (a, b, c, d, e, f, g, h))
    -> Maybe h -> Maybe (a, b, c, d, e, f, g, h)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe h
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    a7
      sexprToArg _ _                                = Maybe (a, b, c, d, e, f, g, h)
    forall a. Maybe a
    Nothing

      smtFunType :: (SBV a
     -> SBV b
     -> SBV c
     -> SBV d
     -> SBV e
     -> SBV f
     -> SBV g
     -> SBV h
     -> SBV r)
    -> SBVType
    smtFunType _ = [Kind] -> SBVType
    SBVType [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    forall k (t :: k). Proxy t
    Proxy @f), Proxy g -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy g
    forall k (t :: k). Proxy t
    Proxy @g), Proxy h -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy h
    forall k (t :: k). Proxy t
    Proxy @h), Proxy r -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy r
    forall k (t :: k). Proxy t
    Proxy @r)]

      smtFunSaturate :: (SBV a
     -> SBV b
     -> SBV c
     -> SBV d
     -> SBV e
     -> SBV f
     -> SBV g
     -> SBV h
     -> SBV r)
    -> SBV r
    smtFunSaturate f :: SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV r
    f = SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV r
    f (Kind -> SBV a
    forall a. Kind -> SBV a
    mkArg (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)))
                           (Kind -> SBV b
    forall a. Kind -> SBV a
    mkArg (Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)))
                           (Kind -> SBV c
    forall a. Kind -> SBV a
    mkArg (Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)))
                           (Kind -> SBV d
    forall a. Kind -> SBV a
    mkArg (Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d)))
                           (Kind -> SBV e
    forall a. Kind -> SBV a
    mkArg (Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e)))
                           (Kind -> SBV f
    forall a. Kind -> SBV a
    mkArg (Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    forall k (t :: k). Proxy t
    Proxy @f)))
                           (Kind -> SBV g
    forall a. Kind -> SBV a
    mkArg (Proxy g -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy g
    forall k (t :: k). Proxy t
    Proxy @g)))
                           (Kind -> SBV h
    forall a. Kind -> SBV a
    mkArg (Proxy h -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy h
    forall k (t :: k). Proxy t
    Proxy @h)))

    -- | Generalization of 'Data.SBV.Control.getFunction'
    getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SymVal a, SymVal r, SMTFunction fun a r) => fun -> m ([(a, r)], r)
    getFunction :: fun -> m ([(a, r)], r)
    getFunction f :: fun
    f = do String
    nm <- fun -> m String
    forall fun a r (m :: * -> *).
    (SMTFunction fun a r, MonadIO m, SolverContext m,
     MonadSymbolic m) =>
    fun -> m String
    smtFunName fun
    f

                       let cmd :: String
    cmd = "(get-value (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                           bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getFunction" String
    cmd "a function 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 ([(a, r)], r))
    -> (SExpr -> m ([(a, r)], r))
    -> m ([(a, r)], r)
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m ([(a, r)], r)
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m ([(a, r)], r)) -> m ([(a, r)], r))
    -> (SExpr -> m ([(a, r)], r)) -> m ([(a, r)], r)
    forall a b. (a -> b) -> a -> b
    $ \case EApp [EApp [ECon o :: String
    o, e :: SExpr
    e]] | String
    o String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm -> do Maybe ([(a, r)], r)
    mbAssocs <- fun -> SExpr -> m (Maybe ([(a, r)], r))
    forall fun a r (m :: * -> *).
    (SMTFunction fun a r, MonadIO m, SolverContext m, MonadQuery m,
     MonadSymbolic m, SymVal r) =>
    fun -> SExpr -> m (Maybe ([(a, r)], r))
    sexprToFun fun
    f SExpr
    e
                                                                                   case Maybe ([(a, r)], r)
    mbAssocs of
                                                                                     Just assocs :: ([(a, r)], r)
    assocs -> ([(a, r)], r) -> m ([(a, r)], r)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(a, r)], r)
    assocs
                                                                                     Nothing     -> do Maybe ([([SExpr], SExpr)], SExpr)
    mbPVS <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
    pointWiseExtract String
    nm (fun -> SBVType
    forall fun a r. SMTFunction fun a r => fun -> SBVType
    smtFunType fun
    f)
                                                                                                       case Maybe ([([SExpr], SExpr)], SExpr)
    mbPVS Maybe ([([SExpr], SExpr)], SExpr)
    -> (([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r))
    -> Maybe ([(a, r)], r)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
    forall (t :: * -> *) a r a a.
    (Traversable t, SMTFunction fun a r, SymVal a, SymVal a) =>
    (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
    convert of
                                                                                                         Just x :: ([(a, r)], r)
    x  -> ([(a, r)], r) -> m ([(a, r)], r)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(a, r)], r)
    x
                                                                                                         Nothing -> String -> Maybe [String] -> m ([(a, r)], r)
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing
                                           _                                 -> String -> Maybe [String] -> m ([(a, r)], r)
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing
        where convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
    convert    (vs :: t ([SExpr], SExpr)
    vs, d :: SExpr
    d) = (,) (t (a, a) -> a -> (t (a, a), a))
    -> Maybe (t (a, a)) -> Maybe (a -> (t (a, a), a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (([SExpr], SExpr) -> Maybe (a, a))
    -> t ([SExpr], SExpr) -> Maybe (t (a, a))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ([SExpr], SExpr) -> Maybe (a, a)
    forall a r a.
    (SMTFunction fun a r, SymVal a) =>
    ([SExpr], SExpr) -> Maybe (a, a)
    sexprPoint t ([SExpr], SExpr)
    vs Maybe (a -> (t (a, a), a)) -> Maybe a -> Maybe (t (a, a), a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    d
              sexprPoint :: ([SExpr], SExpr) -> Maybe (a, a)
    sexprPoint (as :: [SExpr]
    as, v :: SExpr
    v) = (,) (a -> a -> (a, a)) -> Maybe a -> Maybe (a -> (a, a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> fun -> [SExpr] -> Maybe a
    forall fun a r. SMTFunction fun a r => fun -> [SExpr] -> Maybe a
    sexprToArg fun
    f [SExpr]
    as    Maybe (a -> (a, a)) -> Maybe a -> Maybe (a, a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe a
    forall a. SymVal a => SExpr -> Maybe a
    sexprToVal SExpr
    v

    -- | Generalization of 'Data.SBV.Control.getUninterpretedValue'
    getUninterpretedValue :: (MonadIO m, MonadQuery m, HasKind a) => SBV a -> m String
    getUninterpretedValue :: SBV a -> m String
    getUninterpretedValue s :: SBV a
    s =
            case SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    s of
              KUninterpreted _ (Left _) -> 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
    s)

                                              let nm :: String
    nm  = SV -> String
    forall a. Show a => a -> String
    show SV
    sv
                                                  cmd :: String
    cmd = "(get-value (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                                                  bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getValue" String
    cmd "a model 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 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 [EApp [ECon o :: String
    o,  ECon v :: String
    v]] | String
    o String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV -> String
    forall a. Show a => a -> String
    show SV
    sv -> String -> m String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    v
                                                                  _                                            -> String -> Maybe [String] -> m String
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

              k :: Kind
    k                         -> String -> m String
    forall a. HasCallStack => String -> a
    error (String -> m String) -> String -> m String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [""
                                                           , "*** SBV.getUninterpretedValue: Called on an 'interpreted' kind"
                                                           , "*** "
                                                           , "***    Kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                                           , "***    Hint: Use 'getValue' to extract value for interpreted kinds."
                                                           , "*** "
                                                           , "*** Only truly uninterpreted sorts should be used with 'getUninterpretedValue.'"
                                                           ]

    -- | Get the value of a term, but in CV form. Used internally. The model-index, in particular is extremely Z3 specific!
    getValueCVHelper :: (MonadIO m, MonadQuery m) => Maybe Int -> SV -> m CV
    getValueCVHelper :: Maybe Key -> SV -> m CV
    getValueCVHelper mbi :: Maybe Key
    mbi s :: SV
    s
      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    trueSV
      = CV -> m CV
    forall (m :: * -> *) a. Monad m => a -> m a
    return CV
    trueCV
      | SV
    s SV -> SV -> Bool
    forall a. Eq a => a -> a -> Bool
    == SV
    falseSV
      = CV -> m CV
    forall (m :: * -> *) a. Monad m => a -> m a
    return CV
    falseCV
      | Bool
    True
      = do let nm :: String
    nm  = SV -> String
    forall a. Show a => a -> String
    show SV
    s
               k :: Kind
    k   = SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s

               modelIndex :: String
    modelIndex = case Maybe Key
    mbi of
                              Nothing -> ""
                              Just i :: Key
    i  -> " :model_index " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    i

               cmd :: String
    cmd        = "(get-value (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    modelIndex String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

               bad :: String -> Maybe [String] -> m a
    bad = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "getModel" String
    cmd ("a value binding for kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k) 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 CV) -> (SExpr -> m CV) -> m CV
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m CV
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m CV) -> m CV) -> (SExpr -> m CV) -> m CV
    forall a b. (a -> b) -> a -> b
    $ \case EApp [EApp [ECon v :: String
    v, val :: SExpr
    val]] | String
    v String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm -> case Kind -> SExpr -> Maybe CV
    recoverKindedValue (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s) SExpr
    val of
                                                                        Just cv :: CV
    cv -> CV -> m CV
    forall (m :: * -> *) a. Monad m => a -> m a
    return CV
    cv
                                                                        Nothing -> String -> Maybe [String] -> m CV
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing
                               _                                   -> String -> Maybe [String] -> m CV
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

    -- | "Make up" a CV for this type. Like zero, but smarter.
    defaultKindedValue :: Kind -> Maybe CV
    defaultKindedValue :: Kind -> Maybe CV
    defaultKindedValue k :: Kind
    k = Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> Maybe CVal -> Maybe CV
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> Maybe CVal
    cvt Kind
    k
      where cvt :: Kind -> Maybe CVal
            cvt :: Kind -> Maybe CVal
    cvt KBool                 = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ Integer -> CVal
    CInteger 0
            cvt KBounded{}            = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ Integer -> CVal
    CInteger 0
            cvt KUnbounded            = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ Integer -> CVal
    CInteger 0
            cvt KReal                 = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> CVal
    CAlgReal 0
            cvt (KUninterpreted _ ui :: Either String [String]
    ui) = Either String [String] -> Maybe CVal
    forall a. Either a [String] -> Maybe CVal
    uninterp Either String [String]
    ui
            cvt KFloat                = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ Float -> CVal
    CFloat 0
            cvt KDouble               = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ Double -> CVal
    CDouble 0
            cvt KChar                 = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ Char -> CVal
    CChar '\NUL'                -- why not?
            cvt KString               = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ String -> CVal
    CString ""
            cvt (KList  _)            = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ [CVal] -> CVal
    CList []
            cvt (KSet  _)             = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ RCSet CVal -> CVal
    CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
    forall a b. (a -> b) -> a -> b
    $ Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    RegularSet Set CVal
    forall a. Set a
    Set.empty -- why not? Arguably, could be the universal set
            cvt (KTuple ks :: [Kind]
    ks)           = [CVal] -> CVal
    CTuple ([CVal] -> CVal) -> Maybe [CVal] -> Maybe CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Kind -> Maybe CVal) -> [Kind] -> Maybe [CVal]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Kind -> Maybe CVal
    cvt [Kind]
    ks
            cvt (KMaybe _)            = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ Maybe CVal -> CVal
    CMaybe Maybe CVal
    forall a. Maybe a
    Nothing
            cvt (KEither k1 :: Kind
    k1 _)        = Either CVal CVal -> CVal
    CEither (Either CVal CVal -> CVal)
    -> (CVal -> Either CVal CVal) -> CVal -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CVal -> Either CVal CVal
    forall a b. a -> Either a b
    Left (CVal -> CVal) -> Maybe CVal -> Maybe CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> Maybe CVal
    cvt Kind
    k1          -- why not?

            -- Tricky case of uninterpreted
            uninterp :: Either a [String] -> Maybe CVal
    uninterp (Right (c :: String
    c:_)) = CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ (Maybe Key, String) -> CVal
    CUserSort (Key -> Maybe Key
    forall a. a -> Maybe a
    Just 1, String
    c)
            uninterp (Right [])    = Maybe CVal
    forall a. Maybe a
    Nothing                       -- I don't think this can actually happen, but just in case
            uninterp (Left _)      = Maybe CVal
    forall a. Maybe a
    Nothing                       -- Out of luck, truly uninterpreted; we don't even know if it's inhabited.

    -- | Go from an SExpr directly to a value
    sexprToVal :: forall a. SymVal a => SExpr -> Maybe a
    sexprToVal :: SExpr -> Maybe a
    sexprToVal e :: SExpr
    e = CV -> a
    forall a. SymVal a => CV -> a
    fromCV (CV -> a) -> Maybe CV -> Maybe a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> SExpr -> Maybe CV
    recoverKindedValue (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a)) SExpr
    e

    -- | Recover a given solver-printed value with a possible interpretation
    recoverKindedValue :: Kind -> SExpr -> Maybe CV
    recoverKindedValue :: Kind -> SExpr -> Maybe CV
    recoverKindedValue k :: Kind
    k e :: SExpr
    e = case Kind
    k of
                               KBool            | ENum (i :: Integer
    i, _) <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k Integer
    i
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KBounded{}       | ENum (i :: Integer
    i, _) <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k Integer
    i
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KUnbounded       | ENum (i :: Integer
    i, _) <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k Integer
    i
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KReal            | ENum (i :: Integer
    i, _) <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k Integer
    i
                                                | EReal i :: AlgReal
    i     <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KReal (AlgReal -> CVal
    CAlgReal AlgReal
    i)
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KUninterpreted{} | ECon s :: String
    s <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ (Maybe Key, String) -> CVal
    CUserSort (Kind -> String -> Maybe Key
    getUIIndex Kind
    k String
    s, String
    s)
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KFloat           | ENum (i :: Integer
    i, _) <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k Integer
    i
                                                | EFloat i :: Float
    i    <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KFloat (Float -> CVal
    CFloat Float
    i)
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KDouble          | ENum (i :: Integer
    i, _) <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k Integer
    i
                                                | EDouble i :: Double
    i   <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KDouble (Double -> CVal
    CDouble Double
    i)
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KChar            | ENum (i :: Integer
    i, _) <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KChar (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ Char -> CVal
    CChar (Char -> CVal) -> Char -> CVal
    forall a b. (a -> b) -> a -> b
    $ Key -> Char
    chr (Key -> Char) -> Key -> Char
    forall a b. (a -> b) -> a -> b
    $ Integer -> Key
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    i
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KString          | ECon s :: String
    s      <- SExpr
    e -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KString (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ String -> CVal
    CString (String -> CVal) -> String -> CVal
    forall a b. (a -> b) -> a -> b
    $ String -> String
    interpretString String
    s
                                                | Bool
    True             -> Maybe CV
    forall a. Maybe a
    Nothing

                               KList ek :: Kind
    ek                            -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ [CVal] -> CVal
    CList ([CVal] -> CVal) -> [CVal] -> CVal
    forall a b. (a -> b) -> a -> b
    $ Kind -> SExpr -> [CVal]
    interpretList Kind
    ek SExpr
    e

                               KSet ek :: Kind
    ek                             -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ RCSet CVal -> CVal
    CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
    forall a b. (a -> b) -> a -> b
    $ Kind -> SExpr -> RCSet CVal
    interpretSet Kind
    ek SExpr
    e

                               KTuple{}                            -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ [CVal] -> CVal
    CTuple ([CVal] -> CVal) -> [CVal] -> CVal
    forall a b. (a -> b) -> a -> b
    $ SExpr -> [CVal]
    interpretTuple SExpr
    e

                               KMaybe{}                            -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ Maybe CVal -> CVal
    CMaybe (Maybe CVal -> CVal) -> Maybe CVal -> CVal
    forall a b. (a -> b) -> a -> b
    $ Kind -> SExpr -> Maybe CVal
    interpretMaybe Kind
    k SExpr
    e

                               KEither{}                           -> CV -> Maybe CV
    forall a. a -> Maybe a
    Just (CV -> Maybe CV) -> CV -> Maybe CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ Either CVal CVal -> CVal
    CEither (Either CVal CVal -> CVal) -> Either CVal CVal -> CVal
    forall a b. (a -> b) -> a -> b
    $ Kind -> SExpr -> Either CVal CVal
    interpretEither Kind
    k SExpr
    e

      where getUIIndex :: Kind -> String -> Maybe Key
    getUIIndex (KUninterpreted  _ (Right xs :: [String]
    xs)) i :: String
    i = String
    i String -> [String] -> Maybe Key
    forall a. Eq a => a -> [a] -> Maybe Key
    `elemIndex` [String]
    xs
            getUIIndex _                              _ = Maybe Key
    forall a. Maybe a
    Nothing

            stringLike :: String -> Bool
    stringLike xs :: String
    xs = String -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length String
    xs Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 2 Bool -> Bool -> Bool
    && String -> Char
    forall a. [a] -> a
    head String
    xs Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '"' Bool -> Bool -> Bool
    && String -> Char
    forall a. [a] -> a
    last String
    xs Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '"'

            -- Make sure strings are really strings
            interpretString :: String -> String
    interpretString xs :: String
    xs
              | Bool -> Bool
    not (String -> Bool
    stringLike String
    xs)
              = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "Expected a string constant with quotes, received: <" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ">"
              | Bool
    True
              = String -> String
    qfsToString (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String -> String
    forall a. [a] -> [a]
    tail (String -> String
    forall a. [a] -> [a]
    init String
    xs)

            isStringSequence :: Kind -> Bool
    isStringSequence (KList (KBounded _ 8)) = Bool
    True
            isStringSequence _                      = Bool
    False

            -- Lists are tricky since z3 prints the 8-bit variants as strings. See: <http://github.com/Z3Prover/z3/issues/1808>
            interpretList :: Kind -> SExpr -> [CVal]
    interpretList _ (ECon s :: String
    s)
              | Kind -> Bool
    isStringSequence Kind
    k Bool -> Bool -> Bool
    && String -> Bool
    stringLike String
    s
              = (Char -> CVal) -> String -> [CVal]
    forall a b. (a -> b) -> [a] -> [b]
    map (Integer -> CVal
    CInteger (Integer -> CVal) -> (Char -> Integer) -> Char -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Key -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Key -> Integer) -> (Char -> Key) -> Char -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Key
    ord) (String -> [CVal]) -> String -> [CVal]
    forall a b. (a -> b) -> a -> b
    $ String -> String
    interpretString String
    s
            interpretList ek :: Kind
    ek topExpr :: SExpr
    topExpr = SExpr -> [CVal]
    walk SExpr
    topExpr
              where walk :: SExpr -> [CVal]
    walk (EApp [ECon "as", ECon "seq.empty", _]) = []
                    walk (EApp [ECon "seq.unit", v :: SExpr
    v])             = case Kind -> SExpr -> Maybe CV
    recoverKindedValue Kind
    ek SExpr
    v of
                                                                     Just w :: CV
    w -> [CV -> CVal
    cvVal CV
    w]
                                                                     Nothing -> String -> [CVal]
    forall a. HasCallStack => String -> a
    error (String -> [CVal]) -> String -> [CVal]
    forall a b. (a -> b) -> a -> b
    $ "Cannot parse a sequence item of kind " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " from: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    v String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    extra SExpr
    v
                    walk (EApp (ECon "seq.++" : rest :: [SExpr]
    rest))           = (SExpr -> [CVal]) -> [SExpr] -> [CVal]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap SExpr -> [CVal]
    walk [SExpr]
    rest
                    walk cur :: SExpr
    cur                                     = String -> [CVal]
    forall a. HasCallStack => String -> a
    error (String -> [CVal]) -> String -> [CVal]
    forall a b. (a -> b) -> a -> b
    $ "Expected a sequence constant, but received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    cur String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    extra SExpr
    cur

                    extra :: a -> String
    extra cur :: a
    cur | a -> String
    forall a. Show a => a -> String
    show a
    cur String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    t = ""
                              | Bool
    True          = "\nWhile parsing: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t
                              where t :: String
    t = SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    topExpr

            -- Essentially treat sets as functions, since we do allow for store associations
            interpretSet :: Kind -> SExpr -> RCSet CVal
    interpretSet ke :: Kind
    ke setExpr :: SExpr
    setExpr
                 | SExpr -> Bool
    isUniversal SExpr
    setExpr             = Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    ComplementSet Set CVal
    forall a. Set a
    Set.empty
                 | SExpr -> Bool
    isEmpty     SExpr
    setExpr             = Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    RegularSet    Set CVal
    forall a. Set a
    Set.empty
                 | Just (Right assocs :: ([([SExpr], SExpr)], SExpr)
    assocs) <- Maybe (Either String ([([SExpr], SExpr)], SExpr))
    mbAssocs = ([([SExpr], SExpr)], SExpr) -> RCSet CVal
    decode ([([SExpr], SExpr)], SExpr)
    assocs
                 | Bool
    True                            = String -> RCSet CVal
    forall a. String -> a
    tbd "Expected a set value, but couldn't decipher the solver output."

               where tbd :: String -> a
    tbd w :: String
    w = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                             , "*** Data.SBV.interpretSet: Unable to process solver output."
                                             , "***"
                                             , "*** Kind    : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show (Kind -> Kind
    KSet Kind
    ke)
                                             , "*** Received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    setExpr
                                             , "*** Reason  : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w
                                             , "***"
                                             , "*** This is either a bug or something SBV currently does not support."
                                             , "*** Please report this as a feature request!"
                                             ]

                     isTrue :: SExpr -> Bool
    isTrue (ENum (1, Nothing)) = Bool
    True
                     isTrue (ENum (0, Nothing)) = Bool
    False
                     isTrue bad :: SExpr
    bad                 = String -> Bool
    forall a. String -> a
    tbd (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "Non-boolean membership value seen: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    bad

                     isUniversal :: SExpr -> Bool
    isUniversal (EApp [EApp [ECon "as", ECon "const", EApp [ECon "Array", _, ECon "Bool"]], r :: SExpr
    r]) = SExpr -> Bool
    isTrue SExpr
    r
                     isUniversal _                                                                               = Bool
    False

                     isEmpty :: SExpr -> Bool
    isEmpty     (EApp [EApp [ECon "as", ECon "const", EApp [ECon "Array", _, ECon "Bool"]], r :: SExpr
    r]) = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ SExpr -> Bool
    isTrue SExpr
    r
                     isEmpty     _                                                                               = Bool
    False

                     mbAssocs :: Maybe (Either String ([([SExpr], SExpr)], SExpr))
    mbAssocs = SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    parseSExprFunction SExpr
    setExpr

                     decode :: ([([SExpr], SExpr)], SExpr) -> RCSet CVal
    decode (args :: [([SExpr], SExpr)]
    args, r :: SExpr
    r) | SExpr -> Bool
    isTrue SExpr
    r = Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    ComplementSet (Set CVal -> RCSet CVal) -> Set CVal -> RCSet CVal
    forall a b. (a -> b) -> a -> b
    $ [CVal] -> Set CVal
    forall a. Ord a => [a] -> Set a
    Set.fromList [CVal
    x | (x :: CVal
    x, False) <- (([SExpr], SExpr) -> (CVal, Bool))
    -> [([SExpr], SExpr)] -> [(CVal, Bool)]
    forall a b. (a -> b) -> [a] -> [b]
    map ([SExpr], SExpr) -> (CVal, Bool)
    contents [([SExpr], SExpr)]
    args]  -- deletions from universal
                                      | Bool
    True     = Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    RegularSet    (Set CVal -> RCSet CVal) -> Set CVal -> RCSet CVal
    forall a b. (a -> b) -> a -> b
    $ [CVal] -> Set CVal
    forall a. Ord a => [a] -> Set a
    Set.fromList [CVal
    x | (x :: CVal
    x, True)  <- (([SExpr], SExpr) -> (CVal, Bool))
    -> [([SExpr], SExpr)] -> [(CVal, Bool)]
    forall a b. (a -> b) -> [a] -> [b]
    map ([SExpr], SExpr) -> (CVal, Bool)
    contents [([SExpr], SExpr)]
    args]  -- additions to empty

                     contents :: ([SExpr], SExpr) -> (CVal, Bool)
    contents ([v :: SExpr
    v], r :: SExpr
    r) = (SExpr -> CVal
    element SExpr
    v, SExpr -> Bool
    isTrue SExpr
    r)
                     contents bad :: ([SExpr], SExpr)
    bad      = String -> (CVal, Bool)
    forall a. String -> a
    tbd (String -> (CVal, Bool)) -> String -> (CVal, Bool)
    forall a b. (a -> b) -> a -> b
    $ "Multi-valued set member seen: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([SExpr], SExpr) -> String
    forall a. Show a => a -> String
    show ([SExpr], SExpr)
    bad

                     element :: SExpr -> CVal
    element x :: SExpr
    x = case Kind -> SExpr -> Maybe CV
    recoverKindedValue Kind
    ke SExpr
    x of
                                   Just v :: CV
    v  -> CV -> CVal
    cvVal CV
    v
                                   Nothing -> String -> CVal
    forall a. String -> a
    tbd (String -> CVal) -> String -> CVal
    forall a b. (a -> b) -> a -> b
    $ "Unexpected value for kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (SExpr, Kind) -> String
    forall a. Show a => a -> String
    show (SExpr
    x, Kind
    ke)

            interpretTuple :: SExpr -> [CVal]
    interpretTuple te :: SExpr
    te = Key -> [Maybe CV] -> [CVal] -> [CVal]
    forall a. (Num a, Show a) => a -> [Maybe CV] -> [CVal] -> [CVal]
    walk (1 :: Int) ((Kind -> SExpr -> Maybe CV) -> [Kind] -> [SExpr] -> [Maybe CV]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Kind -> SExpr -> Maybe CV
    recoverKindedValue [Kind]
    ks [SExpr]
    args) []
                    where (ks :: [Kind]
    ks, n :: Key
    n) = case Kind
    k of
                                      KTuple eks :: [Kind]
    eks -> ([Kind]
    eks, [Kind] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [Kind]
    eks)
                                      _          -> String -> ([Kind], Key)
    forall a. HasCallStack => String -> a
    error (String -> ([Kind], Key)) -> String -> ([Kind], Key)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "Impossible: Expected a tuple kind, but got: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                                                    , "While trying to parse: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    te
                                                                    ]

                          -- | Convert a sexpr of n-tuple to constituent sexprs. Z3 and CVC4 differ here on how they
                          -- present tuples, so we accommodate both:
                          args :: [SExpr]
    args = SExpr -> [SExpr]
    try SExpr
    te
                            where -- Z3 way
                                  try :: SExpr -> [SExpr]
    try (EApp (ECon f :: String
    f : as :: [SExpr]
    as)) = case Key -> String -> (String, String)
    forall a. Key -> [a] -> ([a], [a])
    splitAt (String -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length "mkSBVTuple") String
    f of
                                                                 ("mkSBVTuple", c :: String
    c) | (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    isDigit String
    c Bool -> Bool -> Bool
    && String -> Key
    forall a. Read a => String -> a
    read String
    c Key -> Key -> Bool
    forall a. Eq a => a -> a -> Bool
    == Key
    n Bool -> Bool -> Bool
    && [SExpr] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [SExpr]
    as Key -> Key -> Bool
    forall a. Eq a => a -> a -> Bool
    == Key
    n -> [SExpr]
    as
                                                                 _  -> [SExpr]
    forall a. a
    bad
                                  -- CVC4 way
                                  try  (EApp (EApp [ECon "as", ECon f :: String
    f, _] : as :: [SExpr]
    as)) = SExpr -> [SExpr]
    try ([SExpr] -> SExpr
    EApp (String -> SExpr
    ECon String
    f SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [SExpr]
    as))
                                  try  _ = [SExpr]
    forall a. a
    bad
                                  bad :: a
    bad = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.sexprToTuple: Impossible: Expected a constructor for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " tuple, but got: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    te

                          walk :: a -> [Maybe CV] -> [CVal] -> [CVal]
    walk _ []           sofar :: [CVal]
    sofar = [CVal] -> [CVal]
    forall a. [a] -> [a]
    reverse [CVal]
    sofar
                          walk i :: a
    i (Just el :: CV
    el:es :: [Maybe CV]
    es) sofar :: [CVal]
    sofar = a -> [Maybe CV] -> [CVal] -> [CVal]
    walk (a
    ia -> a -> a
    forall a. Num a => a -> a -> a
    +1) [Maybe CV]
    es (CV -> CVal
    cvVal CV
    el CVal -> [CVal] -> [CVal]
    forall a. a -> [a] -> [a]
    : [CVal]
    sofar)
                          walk i :: a
    i (Nothing:_)  _     = String -> [CVal]
    forall a. HasCallStack => String -> a
    error (String -> [CVal]) -> String -> [CVal]
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "Couldn't parse a tuple element at position " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i
                                                                      , "Kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                                                                      , "Expr: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    te
                                                                      ]

            -- SMaybe
            interpretMaybe :: Kind -> SExpr -> Maybe CVal
    interpretMaybe (KMaybe _)  (ECon "nothing_SBVMaybe")        = Maybe CVal
    forall a. Maybe a
    Nothing
            interpretMaybe (KMaybe ek :: Kind
    ek) (EApp [ECon "just_SBVMaybe", a :: SExpr
    a]) = case Kind -> SExpr -> Maybe CV
    recoverKindedValue Kind
    ek SExpr
    a of
                                                                            Just (CV _ v :: CVal
    v) -> CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just CVal
    v
                                                                            Nothing       -> String -> Maybe CVal
    forall a. HasCallStack => String -> a
    error (String -> Maybe CVal) -> String -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "Couldn't parse a maybe just value"
                                                                                                             , "Kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                                                                                                             , "Expr: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    a
                                                                                                             ]
            -- CVC4 puts in full ascriptions, handle those:
            interpretMaybe _  (      EApp [ECon "as", ECon "nothing_SBVMaybe", _])     = Maybe CVal
    forall a. Maybe a
    Nothing
            interpretMaybe mk :: Kind
    mk (EApp [EApp [ECon "as", ECon "just_SBVMaybe",    _], a :: SExpr
    a]) = Kind -> SExpr -> Maybe CVal
    interpretMaybe Kind
    mk ([SExpr] -> SExpr
    EApp [String -> SExpr
    ECon "just_SBVMaybe", SExpr
    a])

            interpretMaybe _  other :: SExpr
    other = String -> Maybe CVal
    forall a. HasCallStack => String -> a
    error (String -> Maybe CVal) -> String -> Maybe CVal
    forall a b. (a -> b) -> a -> b
    $ "Expected an SMaybe sexpr, but received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, SExpr) -> String
    forall a. Show a => a -> String
    show (Kind
    k, SExpr
    other)

            -- SEither
            interpretEither :: Kind -> SExpr -> Either CVal CVal
    interpretEither (KEither k1 :: Kind
    k1 _) (EApp [ECon "left_SBVEither",  a :: SExpr
    a]) = case Kind -> SExpr -> Maybe CV
    recoverKindedValue Kind
    k1 SExpr
    a of
                                                                                  Just (CV _ v :: CVal
    v) -> CVal -> Either CVal CVal
    forall a b. a -> Either a b
    Left CVal
    v
                                                                                  Nothing       -> String -> Either CVal CVal
    forall a. HasCallStack => String -> a
    error (String -> Either CVal CVal) -> String -> Either CVal CVal
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "Couldn't parse an either value on the left"
                                                                                                                   , "Kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k1
                                                                                                                   , "Expr: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    a
                                                                                                                   ]
            interpretEither (KEither _ k2 :: Kind
    k2) (EApp [ECon "right_SBVEither", b :: SExpr
    b]) = case Kind -> SExpr -> Maybe CV
    recoverKindedValue Kind
    k2 SExpr
    b of
                                                                                  Just (CV _ v :: CVal
    v) -> CVal -> Either CVal CVal
    forall a b. b -> Either a b
    Right CVal
    v
                                                                                  Nothing       -> String -> Either CVal CVal
    forall a. HasCallStack => String -> a
    error (String -> Either CVal CVal) -> String -> Either CVal CVal
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "Couldn't parse an either value on the right"
                                                                                                                   , "Kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k2
                                                                                                                   , "Expr: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    b
                                                                                                                   ]

            -- CVC4 puts full ascriptions:
            interpretEither ek :: Kind
    ek (EApp [EApp [ECon "as", ECon "left_SBVEither",  _], a :: SExpr
    a]) = Kind -> SExpr -> Either CVal CVal
    interpretEither Kind
    ek ([SExpr] -> SExpr
    EApp [String -> SExpr
    ECon "left_SBVEither", SExpr
    a])
            interpretEither ek :: Kind
    ek (EApp [EApp [ECon "as", ECon "right_SBVEither", _], b :: SExpr
    b]) = Kind -> SExpr -> Either CVal CVal
    interpretEither Kind
    ek ([SExpr] -> SExpr
    EApp [String -> SExpr
    ECon "right_SBVEither", SExpr
    b])

            interpretEither _ other :: SExpr
    other = String -> Either CVal CVal
    forall a. HasCallStack => String -> a
    error (String -> Either CVal CVal) -> String -> Either CVal CVal
    forall a b. (a -> b) -> a -> b
    $ "Expected an SEither sexpr, but received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, SExpr) -> String
    forall a. Show a => a -> String
    show (Kind
    k, SExpr
    other)

    -- | Generalization of 'Data.SBV.Control.getValueCV'
    getValueCV :: (MonadIO m, MonadQuery m) => Maybe Int -> SV -> m CV
    getValueCV :: Maybe Key -> SV -> m CV
    getValueCV mbi :: Maybe Key
    mbi s :: SV
    s
      | SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    s Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    KReal
      = Maybe Key -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> SV -> m CV
    getValueCVHelper Maybe Key
    mbi SV
    s
      | Bool
    True
      = do SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
           if Bool -> Bool
    not (SolverCapabilities -> Bool
    supportsApproxReals (SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)))
              then Maybe Key -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> SV -> m CV
    getValueCVHelper Maybe Key
    mbi SV
    s
              else do Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True "(set-option :pp.decimal false)"
                      CV
    rep1 <- Maybe Key -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> SV -> m CV
    getValueCVHelper Maybe Key
    mbi SV
    s
                      Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True   "(set-option :pp.decimal true)"
                      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
    $ "(set-option :pp.decimal_precision " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show (SMTConfig -> Key
    printRealPrec SMTConfig
    cfg) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                      CV
    rep2 <- Maybe Key -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> SV -> m CV
    getValueCVHelper Maybe Key
    mbi SV
    s

                      let bad :: 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 "getValueCV" "get-value" ("a real-valued binding for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s) Maybe [String]
    forall a. Maybe a
    Nothing ((CV, CV) -> String
    forall a. Show a => a -> String
    show (CV
    rep1, CV
    rep2)) Maybe [String]
    forall a. Maybe a
    Nothing

                      case (CV
    rep1, CV
    rep2) of
                        (CV KReal (CAlgReal a :: AlgReal
    a), CV KReal (CAlgReal b :: AlgReal
    b)) -> CV -> m CV
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CV -> m CV) -> CV -> m CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KReal (AlgReal -> CVal
    CAlgReal (String -> AlgReal -> AlgReal -> AlgReal
    mergeAlgReals ("Cannot merge real-values for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    s) AlgReal
    a AlgReal
    b))
                        _                                              -> m CV
    forall a. m a
    bad

    -- | Generalization of 'Data.SBV.Control.getUIFunCVAssoc'
    getUIFunCVAssoc :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
    getUIFunCVAssoc :: Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
    getUIFunCVAssoc mbi :: Maybe Key
    mbi (nm :: String
    nm, typ :: SBVType
    typ) = do
      let modelIndex :: String
    modelIndex = case Maybe Key
    mbi of
                         Nothing -> ""
                         Just i :: Key
    i  -> " :model_index " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    i

          cmd :: String
    cmd        = "(get-value (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    modelIndex String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

          bad :: String -> Maybe [String] -> m a
    bad        = String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected "get-value" String
    cmd "a function 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

      let (ats :: [Kind]
    ats, rt :: Kind
    rt) = case SBVType
    typ of
                        SBVType as :: [Kind]
    as | [Kind] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [Kind]
    as Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1 -> ([Kind] -> [Kind]
    forall a. [a] -> [a]
    init [Kind]
    as, [Kind] -> Kind
    forall a. [a] -> a
    last [Kind]
    as)
                        _                          -> String -> ([Kind], Kind)
    forall a. HasCallStack => String -> a
    error (String -> ([Kind], Kind)) -> String -> ([Kind], Kind)
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.getUIFunCVAssoc: Expected a function type, got: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVType -> String
    forall a. Show a => a -> String
    show SBVType
    typ

      let convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
    convert (vs :: t ([SExpr], SExpr)
    vs, d :: SExpr
    d) = (,) (t ([CV], CV) -> CV -> (t ([CV], CV), CV))
    -> Maybe (t ([CV], CV)) -> Maybe (CV -> (t ([CV], CV), CV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (([SExpr], SExpr) -> Maybe ([CV], CV))
    -> t ([SExpr], SExpr) -> Maybe (t ([CV], CV))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ([SExpr], SExpr) -> Maybe ([CV], CV)
    toPoint t ([SExpr], SExpr)
    vs Maybe (CV -> (t ([CV], CV), CV))
    -> Maybe CV -> Maybe (t ([CV], CV), CV)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe CV
    toRes SExpr
    d
          toPoint :: ([SExpr], SExpr) -> Maybe ([CV], CV)
    toPoint (as :: [SExpr]
    as, v :: SExpr
    v)
             | [SExpr] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [SExpr]
    as Key -> Key -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Kind] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [Kind]
    ats = (,) ([CV] -> CV -> ([CV], CV))
    -> Maybe [CV] -> Maybe (CV -> ([CV], CV))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Kind -> SExpr -> Maybe CV) -> [Kind] -> [SExpr] -> Maybe [CV]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Kind -> SExpr -> Maybe CV
    recoverKindedValue [Kind]
    ats [SExpr]
    as Maybe (CV -> ([CV], CV)) -> Maybe CV -> Maybe ([CV], CV)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SExpr -> Maybe CV
    toRes SExpr
    v
             | Bool
    True                    = String -> Maybe ([CV], CV)
    forall a. HasCallStack => String -> a
    error (String -> Maybe ([CV], CV)) -> String -> Maybe ([CV], CV)
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV.getUIFunCVAssoc: Mismatching type/value arity, got: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([SExpr], [Kind]) -> String
    forall a. Show a => a -> String
    show ([SExpr]
    as, [Kind]
    ats)

          toRes :: SExpr -> Maybe CV
          toRes :: SExpr -> Maybe CV
    toRes = Kind -> SExpr -> Maybe CV
    recoverKindedValue Kind
    rt

          -- In case we end up in the pointwise scenerio, boolify the result
          -- as that's the only type we support here.
          tryPointWise :: m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
    tryPointWise bailOut :: m ([([CV], CV)], CV)
    bailOut = do Maybe ([([SExpr], SExpr)], SExpr)
    mbSExprs <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
    pointWiseExtract String
    nm SBVType
    typ
                                    case Maybe ([([SExpr], SExpr)], SExpr)
    mbSExprs of
                                      Nothing     -> m ([([CV], CV)], CV)
    bailOut
                                      Just sExprs :: ([([SExpr], SExpr)], SExpr)
    sExprs -> m ([([CV], CV)], CV)
    -> (([([CV], CV)], CV) -> m ([([CV], CV)], CV))
    -> Maybe ([([CV], CV)], CV)
    -> m ([([CV], CV)], CV)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m ([([CV], CV)], CV)
    bailOut ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([([SExpr], SExpr)], SExpr) -> Maybe ([([CV], CV)], CV)
    forall (t :: * -> *).
    Traversable t =>
    (t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
    convert ([([SExpr], SExpr)], SExpr)
    sExprs)

      String
    -> (String -> Maybe [String] -> m ([([CV], CV)], CV))
    -> (SExpr -> m ([([CV], CV)], CV))
    -> m ([([CV], CV)], CV)
    forall a.
    String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse String
    r String -> Maybe [String] -> m ([([CV], CV)], CV)
    forall a. String -> Maybe [String] -> m a
    bad ((SExpr -> m ([([CV], CV)], CV)) -> m ([([CV], CV)], CV))
    -> (SExpr -> m ([([CV], CV)], CV)) -> m ([([CV], CV)], CV)
    forall a b. (a -> b) -> a -> b
    $ \case EApp [EApp [ECon o :: String
    o, e :: SExpr
    e]] | String
    o String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm -> let bailOut :: m a
    bailOut = String -> Maybe [String] -> m a
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing
                                                               in case SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    parseSExprFunction SExpr
    e of
                                                                    Just (Right assocs :: ([([SExpr], SExpr)], SExpr)
    assocs) | Just res :: ([([CV], CV)], CV)
    res <- ([([SExpr], SExpr)], SExpr) -> Maybe ([([CV], CV)], CV)
    forall (t :: * -> *).
    Traversable t =>
    (t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
    convert ([([SExpr], SExpr)], SExpr)
    assocs                   -> ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([([CV], CV)], CV)
    res
                                                                                        | Bool
    True                                         -> m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
    tryPointWise m ([([CV], CV)], CV)
    forall a. m a
    bailOut

                                                                    Just (Left nm' :: String
    nm')     | String
    nm String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm', Just res :: CV
    res <- Kind -> Maybe CV
    defaultKindedValue Kind
    rt -> ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], CV
    res)
                                                                                        | Bool
    True                                         -> String -> Maybe [String] -> m ([([CV], CV)], CV)
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

                                                                    Nothing                                                            -> m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
    tryPointWise m ([([CV], CV)], CV)
    forall a. m a
    bailOut

                          _                                 -> String -> Maybe [String] -> m ([([CV], CV)], CV)
    forall a. String -> Maybe [String] -> m a
    bad String
    r Maybe [String]
    forall a. Maybe a
    Nothing

    -- | Generalization of 'Data.SBV.Control.checkSat'
    checkSat :: (MonadIO m, MonadQuery m) => m CheckSatResult
    checkSat :: m CheckSatResult
    checkSat = do SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig
                  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

    -- | Generalization of 'Data.SBV.Control.checkSatUsing'
    checkSatUsing :: (MonadIO m, MonadQuery m) => String -> m CheckSatResult
    checkSatUsing :: String -> m CheckSatResult
    checkSatUsing cmd :: String
    cmd = do let 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 "checkSat" String
    cmd "one of sat/unsat/unknown" Maybe [String]
    forall a. Maybe a
    Nothing

                               -- Sigh.. Ignore some of the pesky warnings. We only do it as an exception here.
                               ignoreList :: [String]
    ignoreList = ["WARNING: optimization with quantified constraints is not supported"]

                           String
    r <- String -> [String] -> m String
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> [String] -> m String
    askIgnoring String
    cmd [String]
    ignoreList

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

    -- | What are the top level inputs? Trackers are returned as top level existentials
    getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m [(Quantifier, NamedSymVar)]
    getQuantifiedInputs :: m [(Quantifier, NamedSymVar)]
    getQuantifiedInputs = do State{IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps :: State
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps :: IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps} <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
                             ((rQinps :: [(Quantifier, NamedSymVar)]
    rQinps, rTrackers :: [NamedSymVar]
    rTrackers), _) <- IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> m (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
     -> m (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
    -> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> m (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall a b. (a -> b) -> a -> b
    $ IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall a. IORef a -> IO a
    readIORef IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps

                             let qinps :: [(Quantifier, NamedSymVar)]
    qinps    = [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a. [a] -> [a]
    reverse [(Quantifier, NamedSymVar)]
    rQinps
                                 trackers :: [(Quantifier, NamedSymVar)]
    trackers = (NamedSymVar -> (Quantifier, NamedSymVar))
    -> [NamedSymVar] -> [(Quantifier, NamedSymVar)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Quantifier
    EX,) ([NamedSymVar] -> [(Quantifier, NamedSymVar)])
    -> [NamedSymVar] -> [(Quantifier, NamedSymVar)]
    forall a b. (a -> b) -> a -> b
    $ [NamedSymVar] -> [NamedSymVar]
    forall a. [a] -> [a]
    reverse [NamedSymVar]
    rTrackers

                                 -- separate the existential prefix, which will go first
                                 (preQs :: [(Quantifier, NamedSymVar)]
    preQs, postQs :: [(Quantifier, NamedSymVar)]
    postQs) = ((Quantifier, NamedSymVar) -> Bool)
    -> [(Quantifier, NamedSymVar)]
    -> ([(Quantifier, NamedSymVar)], [(Quantifier, NamedSymVar)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (\(q :: Quantifier
    q, _) -> Quantifier
    q Quantifier -> Quantifier -> Bool
    forall a. Eq a => a -> a -> Bool
    == Quantifier
    EX) [(Quantifier, NamedSymVar)]
    qinps

                             [(Quantifier, NamedSymVar)] -> m [(Quantifier, NamedSymVar)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Quantifier, NamedSymVar)] -> m [(Quantifier, NamedSymVar)])
    -> [(Quantifier, NamedSymVar)] -> m [(Quantifier, NamedSymVar)]
    forall a b. (a -> b) -> a -> b
    $ [(Quantifier, NamedSymVar)]
    preQs [(Quantifier, NamedSymVar)]
    -> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a. [a] -> [a] -> [a]
    ++ [(Quantifier, NamedSymVar)]
    trackers [(Quantifier, NamedSymVar)]
    -> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a. [a] -> [a] -> [a]
    ++ [(Quantifier, NamedSymVar)]
    postQs

    -- | Get observables, i.e., those explicitly labeled by the user with a call to 'Data.SBV.observe'.
    getObservables :: (MonadIO m, MonadQuery m) => m [(String, CV)]
    getObservables :: m [(String, CV)]
    getObservables = do State{IORef [(String, CV -> Bool, SV)]
    rObservables :: State -> IORef [(String, CV -> Bool, SV)]
    rObservables :: IORef [(String, CV -> Bool, SV)]
    rObservables} <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState

                        [(String, CV -> Bool, SV)]
    rObs <- IO [(String, CV -> Bool, SV)] -> m [(String, CV -> Bool, SV)]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [(String, CV -> Bool, SV)] -> m [(String, CV -> Bool, SV)])
    -> IO [(String, CV -> Bool, SV)] -> m [(String, CV -> Bool, SV)]
    forall a b. (a -> b) -> a -> b
    $ IORef [(String, CV -> Bool, SV)] -> IO [(String, CV -> Bool, SV)]
    forall a. IORef a -> IO a
    readIORef IORef [(String, CV -> Bool, SV)]
    rObservables

                        -- This intentionally reverses the result; since 'rObs' stores in reversed order
                        let walk :: [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
    walk []             sofar :: [(a, CV)]
    sofar = [(a, CV)] -> m [(a, CV)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(a, CV)]
    sofar
                            walk ((n :: a
    n, f :: CV -> Bool
    f, s :: SV
    s):os :: [(a, CV -> Bool, SV)]
    os) sofar :: [(a, CV)]
    sofar = do CV
    cv <- Maybe Key -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> SV -> m CV
    getValueCV Maybe Key
    forall a. Maybe a
    Nothing SV
    s
                                                           if CV -> Bool
    f CV
    cv
                                                              then [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
    walk [(a, CV -> Bool, SV)]
    os ((a
    n, CV
    cv) (a, CV) -> [(a, CV)] -> [(a, CV)]
    forall a. a -> [a] -> [a]
    : [(a, CV)]
    sofar)
                                                              else [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
    walk [(a, CV -> Bool, SV)]
    os            [(a, CV)]
    sofar

                        [(String, CV -> Bool, SV)] -> [(String, CV)] -> m [(String, CV)]
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m) =>
    [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
    walk [(String, CV -> Bool, SV)]
    rObs []

    -- | Get UIs, both constants and functions. This call returns both the before and after query ones.
    -- | Generalization of 'Data.SBV.Control.getUIs'.
    getUIs :: forall m. (MonadIO m, MonadQuery m) => m [(String, SBVType)]
    getUIs :: m [(String, SBVType)]
    getUIs = do State{IORef (Map String SBVType)
    rUIMap :: IORef (Map String SBVType)
    rUIMap :: State -> IORef (Map String SBVType)
    rUIMap, IORef IncState
    rIncState :: State -> IORef IncState
    rIncState :: IORef IncState
    rIncState} <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState
                Map String SBVType
    prior <- IO (Map String SBVType) -> m (Map String SBVType)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO (Map String SBVType) -> m (Map String SBVType))
    -> IO (Map String SBVType) -> m (Map String SBVType)
    forall a b. (a -> b) -> a -> b
    $ IORef (Map String SBVType) -> IO (Map String SBVType)
    forall a. IORef a -> IO a
    readIORef IORef (Map String SBVType)
    rUIMap
                Map String SBVType
    new   <- IO (Map String SBVType) -> m (Map String SBVType)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO (Map String SBVType) -> m (Map String SBVType))
    -> IO (Map String SBVType) -> m (Map String SBVType)
    forall a b. (a -> b) -> a -> b
    $ IORef IncState -> IO IncState
    forall a. IORef a -> IO a
    readIORef IORef IncState
    rIncState IO IncState
    -> (IncState -> IO (Map String SBVType)) -> IO (Map String SBVType)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IORef (Map String SBVType) -> IO (Map String SBVType)
    forall a. IORef a -> IO a
    readIORef (IORef (Map String SBVType) -> IO (Map String SBVType))
    -> (IncState -> IORef (Map String SBVType))
    -> IncState
    -> IO (Map String SBVType)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IncState -> IORef (Map String SBVType)
    rNewUIs
                [(String, SBVType)] -> m [(String, SBVType)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(String, SBVType)] -> m [(String, SBVType)])
    -> [(String, SBVType)] -> m [(String, SBVType)]
    forall a b. (a -> b) -> a -> b
    $ [(String, SBVType)] -> [(String, SBVType)]
    forall a. Eq a => [a] -> [a]
    nub ([(String, SBVType)] -> [(String, SBVType)])
    -> [(String, SBVType)] -> [(String, SBVType)]
    forall a b. (a -> b) -> a -> b
    $ [(String, SBVType)] -> [(String, SBVType)]
    forall a. Ord a => [a] -> [a]
    sort ([(String, SBVType)] -> [(String, SBVType)])
    -> [(String, SBVType)] -> [(String, SBVType)]
    forall a b. (a -> b) -> a -> b
    $ Map String SBVType -> [(String, SBVType)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map String SBVType
    prior [(String, SBVType)] -> [(String, SBVType)] -> [(String, SBVType)]
    forall a. [a] -> [a] -> [a]
    ++ Map String SBVType -> [(String, SBVType)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map String SBVType
    new

    -- | Repeatedly issue check-sat, after refuting the previous model.
    -- The bool is true if the model is unique upto prefix existentials.
    getAllSatResult :: forall m. (MonadIO m, MonadQuery m, SolverContext m) => m (Bool, Bool, Bool, [SMTResult])
    getAllSatResult :: m (Bool, Bool, Bool, [SMTResult])
    getAllSatResult = do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["*** Checking Satisfiability, all solutions.."]

                         SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig

                         topState :: State
    topState@State{IORef KindSet
    rUsedKinds :: State -> IORef KindSet
    rUsedKinds :: IORef KindSet
    rUsedKinds} <- m State
    forall (m :: * -> *). MonadQuery m => m State
    queryState

                         KindSet
    ki    <- IO KindSet -> m KindSet
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO KindSet -> m KindSet) -> IO KindSet -> m KindSet
    forall a b. (a -> b) -> a -> b
    $ IORef KindSet -> IO KindSet
    forall a. IORef a -> IO a
    readIORef IORef KindSet
    rUsedKinds
                         [(Quantifier, NamedSymVar)]
    qinps <- m [(Quantifier, NamedSymVar)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(Quantifier, NamedSymVar)]
    getQuantifiedInputs

                         [(String, SBVType)]
    allUninterpreteds <- m [(String, SBVType)]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    m [(String, SBVType)]
    getUIs

                          -- Functions have at least two kinds in their type and all components must be "interpreted"
                         let allUiFuns :: [(String, SBVType)]
    allUiFuns = [(String, SBVType)
    u | SMTConfig -> Bool
    satTrackUFs SMTConfig
    cfg                                         -- config says consider UIFs
                                            , u :: (String, SBVType)
    u@(nm :: String
    nm, SBVType as :: [Kind]
    as) <- [(String, SBVType)]
    allUninterpreteds, [Kind] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [Kind]
    as Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1  -- get the function ones
                                            , Bool -> Bool
    not (SMTConfig -> String -> Bool
    isNonModelVar SMTConfig
    cfg String
    nm)                              -- make sure they aren't explicitly ignored
                                         ]

                             -- We can only "allSat" if all component types themselves are interpreted. (Otherwise
                             -- there is no way to reflect back the values to the solver.)
                             collectAcceptable :: [(String, SBVType)] -> [String] -> m [String]
    collectAcceptable []                              sofar :: [String]
    sofar = [String] -> m [String]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [String]
    sofar
                             collectAcceptable ((nm :: String
    nm, t :: SBVType
    t@(SBVType ats :: [Kind]
    ats)):rest :: [(String, SBVType)]
    rest) sofar :: [String]
    sofar
                               | Bool -> Bool
    not ((Kind -> Bool) -> [Kind] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    hasUninterpretedSorts [Kind]
    ats)
                               = [(String, SBVType)] -> [String] -> m [String]
    collectAcceptable [(String, SBVType)]
    rest (String
    nm String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)
                               | Bool
    True
                               = do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug [ "*** SBV.allSat: Uninterpreted function: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVType -> String
    forall a. Show a => a -> String
    show SBVType
    t
                                               , "*** Will *not* be used in allSat consideretions since its type"
                                               , "*** has uninterpreted sorts present."
                                               ]
                                    [(String, SBVType)] -> [String] -> m [String]
    collectAcceptable [(String, SBVType)]
    rest [String]
    sofar

                         [String]
    uiFuns <- [String] -> [String]
    forall a. [a] -> [a]
    reverse ([String] -> [String]) -> m [String] -> m [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(String, SBVType)] -> [String] -> m [String]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    [(String, SBVType)] -> [String] -> m [String]
    collectAcceptable [(String, SBVType)]
    allUiFuns []

                         -- 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] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    uiFuns) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                            let solverCaps :: SolverCapabilities
    solverCaps = SMTSolver -> SolverCapabilities
    capabilities (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)
                            in case SolverCapabilities -> Maybe [String]
    supportsFlattenedModels SolverCapabilities
    solverCaps of
                                 Nothing   -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                 Just cmds :: [String]
    cmds -> (String -> m ()) -> [String] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True) [String]
    cmds

                         let usorts :: [String]
    usorts = [String
    s | us :: Kind
    us@(KUninterpreted s :: String
    s _) <- KindSet -> [Kind]
    forall a. Set a -> [a]
    Set.toAscList KindSet
    ki, Kind -> Bool
    isFree Kind
    us]

                         Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    usorts) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug [ "*** SBV.allSat: Uninterpreted sorts present: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    usorts
                                                           , "***             SBV will use equivalence classes to generate all-satisfying instances."
                                                           ]

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

                             vars :: [(SVal, NamedSymVar)]
                             vars :: [(SVal, NamedSymVar)]
    vars = let sortByNodeId :: [NamedSymVar] -> [NamedSymVar]
                                        sortByNodeId :: [NamedSymVar] -> [NamedSymVar]
    sortByNodeId = (NamedSymVar -> NamedSymVar -> Ordering)
    -> [NamedSymVar] -> [NamedSymVar]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (NodeId -> NodeId -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (NodeId -> NodeId -> Ordering)
    -> (NamedSymVar -> NodeId)
    -> NamedSymVar
    -> NamedSymVar
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (\(SV _ n :: NodeId
    n, _) -> NodeId
    n))

                                        mkSVal :: NamedSymVar -> (SVal, NamedSymVar)
                                        mkSVal :: NamedSymVar -> (SVal, NamedSymVar)
    mkSVal nm :: NamedSymVar
    nm@(sv :: SV
    sv, _) = (Kind -> Either CV (Cached SV) -> SVal
    SVal (SV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SV
    sv) (Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right ((State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache (IO SV -> State -> IO SV
    forall a b. a -> b -> a
    const (SV -> IO SV
    forall (m :: * -> *) a. Monad m => a -> m a
    return SV
    sv)))), NamedSymVar
    nm)

                                        ignored :: String -> Bool
    ignored n :: String
    n = SMTConfig -> String -> Bool
    isNonModelVar SMTConfig
    cfg String
    n Bool -> Bool -> Bool
    || "__internal_sbv" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    n

                                    in (NamedSymVar -> (SVal, NamedSymVar))
    -> [NamedSymVar] -> [(SVal, NamedSymVar)]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedSymVar -> (SVal, NamedSymVar)
    mkSVal ([NamedSymVar] -> [(SVal, NamedSymVar)])
    -> [NamedSymVar] -> [(SVal, NamedSymVar)]
    forall a b. (a -> b) -> a -> b
    $ [NamedSymVar] -> [NamedSymVar]
    sortByNodeId [NamedSymVar
    nv | (_, nv :: NamedSymVar
    nv@(_, n :: String
    n)) <- [(Quantifier, NamedSymVar)]
    allModelInputs, Bool -> Bool
    not (String -> Bool
    ignored String
    n)]

                             -- If we have any universals, then the solutions are unique upto prefix existentials.
                             w :: Bool
    w = Quantifier
    ALL Quantifier -> [Quantifier] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ((Quantifier, NamedSymVar) -> Quantifier)
    -> [(Quantifier, NamedSymVar)] -> [Quantifier]
    forall a b. (a -> b) -> [a] -> [b]
    map (Quantifier, NamedSymVar) -> Quantifier
    forall a b. (a, b) -> a
    fst [(Quantifier, NamedSymVar)]
    qinps

                         (sc :: Bool
    sc, unk :: Bool
    unk, ms :: [SMTResult]
    ms) <- Bool
    -> State
    -> ([(String, SBVType)], [String])
    -> [(Quantifier, NamedSymVar)]
    -> [(SVal, NamedSymVar)]
    -> SMTConfig
    -> m (Bool, Bool, [SMTResult])
    forall (t :: * -> *).
    Foldable t =>
    Bool
    -> State
    -> ([(String, SBVType)], t String)
    -> [(Quantifier, NamedSymVar)]
    -> [(SVal, NamedSymVar)]
    -> SMTConfig
    -> m (Bool, Bool, [SMTResult])
    loop Bool
    grabObservables State
    topState ([(String, SBVType)]
    allUiFuns, [String]
    uiFuns) [(Quantifier, NamedSymVar)]
    qinps [(SVal, NamedSymVar)]
    vars SMTConfig
    cfg
                         (Bool, Bool, Bool, [SMTResult])
    -> m (Bool, Bool, Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    sc, Bool
    w, Bool
    unk, [SMTResult] -> [SMTResult]
    forall a. [a] -> [a]
    reverse [SMTResult]
    ms)

       where isFree :: Kind -> Bool
    isFree (KUninterpreted _ (Left _)) = Bool
    True
             isFree _                           = Bool
    False

             loop :: Bool
    -> State
    -> ([(String, SBVType)], t String)
    -> [(Quantifier, NamedSymVar)]
    -> [(SVal, NamedSymVar)]
    -> SMTConfig
    -> m (Bool, Bool, [SMTResult])
    loop grabObservables :: Bool
    grabObservables topState :: State
    topState (allUiFuns :: [(String, SBVType)]
    allUiFuns, uiFunsToReject :: t String
    uiFunsToReject) qinps :: [(Quantifier, NamedSymVar)]
    qinps vars :: [(SVal, NamedSymVar)]
    vars cfg :: SMTConfig
    cfg = Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
    go (1::Int) []
               where go :: Int -> [SMTResult] -> m (Bool, Bool, [SMTResult])
                     go :: Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
    go !Key
    cnt sofar :: [SMTResult]
    sofar
                       | Just maxModels :: Key
    maxModels <- SMTConfig -> Maybe Key
    allSatMaxModelCount SMTConfig
    cfg, Key
    cnt Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    > Key
    maxModels
                       = do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["*** Maximum model count request of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    maxModels String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " reached, stopping the search."]

                            Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (SMTConfig -> Bool
    allSatPrintAlong SMTConfig
    cfg) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn "Search stopped since model count request was reached."

                            (Bool, Bool, [SMTResult]) -> m (Bool, Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    True, Bool
    False, [SMTResult]
    sofar)
                       | Bool
    True
                       = do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["Looking for solution " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    cnt]

                            let endMsg :: m ()
    endMsg = Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (SMTConfig -> Bool
    allSatPrintAlong SMTConfig
    cfg Bool -> Bool -> Bool
    && Bool -> Bool
    not ([SMTResult] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SMTResult]
    sofar)) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
                                                 let msg :: a -> String
    msg 0 = "No solutions found."
                                                     msg 1 = "This is the only solution."
                                                     msg n :: a
    n = "Found " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " different solutions."
                                                 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 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ Key -> String
    forall a. (Eq a, Num a, Show a) => a -> String
    msg (Key
    cnt Key -> Key -> Key
    forall a. Num a => a -> a -> a
    - 1)

                            CheckSatResult
    cs <- m CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    checkSat

                            case CheckSatResult
    cs of
                              Unsat -> do m ()
    endMsg
                                          (Bool, Bool, [SMTResult]) -> m (Bool, Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, Bool
    False, [SMTResult]
    sofar)

                              Unk   -> do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["*** Solver returned unknown, terminating query."]
                                          m ()
    endMsg
                                          (Bool, Bool, [SMTResult]) -> m (Bool, Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, Bool
    True, [SMTResult]
    sofar)

                              Sat   -> do [(SV, (String, (SVal, CV)))]
    assocs <- ((SVal, NamedSymVar) -> m (SV, (String, (SVal, CV))))
    -> [(SVal, NamedSymVar)] -> m [(SV, (String, (SVal, CV)))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (\(sval :: SVal
    sval, (sv :: SV
    sv, n :: String
    n)) -> do CV
    cv <- Maybe Key -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> SV -> m CV
    getValueCV Maybe Key
    forall a. Maybe a
    Nothing SV
    sv
                                                                                 (SV, (String, (SVal, CV))) -> m (SV, (String, (SVal, CV)))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SV
    sv, (String
    n, (SVal
    sval, CV
    cv)))) [(SVal, NamedSymVar)]
    vars

                                          let getUIFun :: (String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
    getUIFun ui :: (String, SBVType)
    ui@(nm :: String
    nm, t :: SBVType
    t) = do ([([CV], CV)], CV)
    cvs <- Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
    getUIFunCVAssoc Maybe Key
    forall a. Maybe a
    Nothing (String, SBVType)
    ui
                                                                       (String, (SBVType, ([([CV], CV)], CV)))
    -> m (String, (SBVType, ([([CV], CV)], CV)))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String
    nm, (SBVType
    t, ([([CV], CV)], CV)
    cvs))
                                          [(String, (SBVType, ([([CV], CV)], CV)))]
    uiFunVals <- ((String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV))))
    -> [(String, SBVType)]
    -> m [(String, (SBVType, ([([CV], CV)], CV)))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    (String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
    getUIFun [(String, SBVType)]
    allUiFuns

                                          -- Add on observables if we're asked to do so:
                                          [(String, CV)]
    obsvs <- if Bool
    grabObservables
                                                      then m [(String, CV)]
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(String, CV)]
    getObservables
                                                      else do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug ["*** In a quantified context, observables will not be printed."]
                                                              [(String, CV)] -> m [(String, CV)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

                                          Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    bindings <- let grab :: (Quantifier, (SV, b)) -> m ((Quantifier, (SV, b)), Maybe CV)
    grab i :: (Quantifier, (SV, b))
    i@(ALL, _)      = ((Quantifier, (SV, b)), Maybe CV)
    -> m ((Quantifier, (SV, b)), Maybe CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Quantifier, (SV, b))
    i, Maybe CV
    forall a. Maybe a
    Nothing)
                                                          grab i :: (Quantifier, (SV, b))
    i@(EX, (sv :: SV
    sv, _)) = case SV
    sv SV -> [(SV, (String, (SVal, CV)))] -> Maybe (String, (SVal, CV))
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, (String, (SVal, CV)))]
    assocs of
                                                                                   Just (_, (_, cv :: CV
    cv)) -> ((Quantifier, (SV, b)), Maybe CV)
    -> m ((Quantifier, (SV, b)), Maybe CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Quantifier, (SV, b))
    i, CV -> Maybe CV
    forall a. a -> Maybe a
    Just CV
    cv)
                                                                                   Nothing           -> do CV
    cv <- Maybe Key -> SV -> m CV
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Maybe Key -> SV -> m CV
    getValueCV Maybe Key
    forall a. Maybe a
    Nothing SV
    sv
                                                                                                           ((Quantifier, (SV, b)), Maybe CV)
    -> m ((Quantifier, (SV, b)), Maybe CV)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Quantifier, (SV, b))
    i, CV -> Maybe CV
    forall a. a -> Maybe a
    Just CV
    cv)
                                                      in if SMTConfig -> Bool
    validationRequested SMTConfig
    cfg
                                                            then [((Quantifier, NamedSymVar), Maybe CV)]
    -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    forall a. a -> Maybe a
    Just ([((Quantifier, NamedSymVar), Maybe CV)]
     -> Maybe [((Quantifier, NamedSymVar), Maybe CV)])
    -> m [((Quantifier, NamedSymVar), Maybe CV)]
    -> m (Maybe [((Quantifier, NamedSymVar), Maybe CV)])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Quantifier, NamedSymVar)
     -> m ((Quantifier, NamedSymVar), Maybe CV))
    -> [(Quantifier, NamedSymVar)]
    -> m [((Quantifier, NamedSymVar), Maybe CV)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Quantifier, NamedSymVar)
    -> m ((Quantifier, NamedSymVar), Maybe CV)
    forall (m :: * -> *) b.
    (MonadIO m, MonadQuery m) =>
    (Quantifier, (SV, b)) -> m ((Quantifier, (SV, b)), Maybe CV)
    grab [(Quantifier, NamedSymVar)]
    qinps
                                                            else Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    -> m (Maybe [((Quantifier, NamedSymVar), Maybe CV)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    forall a. Maybe a
    Nothing

                                          let model :: SMTModel
    model = SMTModel :: [(String, GeneralizedCV)]
    -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    -> [(String, CV)]
    -> [(String, (SBVType, ([([CV], CV)], CV)))]
    -> SMTModel
    SMTModel { modelObjectives :: [(String, GeneralizedCV)]
    modelObjectives = []
                                                               , modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    modelBindings   = Maybe [((Quantifier, NamedSymVar), Maybe CV)]
    bindings
                                                               , modelAssocs :: [(String, CV)]
    modelAssocs     = ((String, CV) -> String) -> [(String, CV)] -> [(String, CV)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    sortOn (String, CV) -> String
    forall a b. (a, b) -> a
    fst [(String, CV)]
    obsvs [(String, CV)] -> [(String, CV)] -> [(String, CV)]
    forall a. [a] -> [a] -> [a]
    ++ [(String
    n, CV
    cv) | (_, (n :: String
    n, (_, cv :: CV
    cv))) <- [(SV, (String, (SVal, CV)))]
    assocs]
                                                               , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
    modelUIFuns     = [(String, (SBVType, ([([CV], CV)], CV)))]
    uiFunVals
                                                               }
                                              m :: SMTResult
    m = SMTConfig -> SMTModel -> SMTResult
    Satisfiable SMTConfig
    cfg SMTModel
    model

                                              (interpreteds :: [(SVal, CV)]
    interpreteds, uninterpreteds :: [(SVal, CV)]
    uninterpreteds) = ((SVal, CV) -> Bool)
    -> [(SVal, CV)] -> ([(SVal, CV)], [(SVal, CV)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (Bool -> Bool
    not (Bool -> Bool) -> ((SVal, CV) -> Bool) -> (SVal, CV) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Kind -> Bool
    isFree (Kind -> Bool) -> ((SVal, CV) -> Kind) -> (SVal, CV) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (SVal -> Kind) -> ((SVal, CV) -> SVal) -> (SVal, CV) -> Kind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SVal, CV) -> SVal
    forall a b. (a, b) -> a
    fst) (((SV, (String, (SVal, CV))) -> (SVal, CV))
    -> [(SV, (String, (SVal, CV)))] -> [(SVal, CV)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, (SVal, CV)) -> (SVal, CV)
    forall a b. (a, b) -> b
    snd ((String, (SVal, CV)) -> (SVal, CV))
    -> ((SV, (String, (SVal, CV))) -> (String, (SVal, CV)))
    -> (SV, (String, (SVal, CV)))
    -> (SVal, CV)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SV, (String, (SVal, CV))) -> (String, (SVal, CV))
    forall a b. (a, b) -> b
    snd) [(SV, (String, (SVal, CV)))]
    assocs)

                                              -- For each interpreted variable, figure out the model equivalence
                                              -- NB. When the kind is floating, we *have* to be careful, since +/- zero, and NaN's
                                              -- and equality don't get along!
                                              interpretedEqs :: [SVal]
                                              interpretedEqs :: [SVal]
    interpretedEqs = [Kind -> SVal -> SVal -> SVal
    forall a. HasKind a => a -> SVal -> SVal -> SVal
    mkNotEq (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    sv) SVal
    sv (Kind -> Either CV (Cached SV) -> SVal
    SVal (SVal -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SVal
    sv) (CV -> Either CV (Cached SV)
    forall a b. a -> Either a b
    Left CV
    cv)) | (sv :: SVal
    sv, cv :: CV
    cv) <- [(SVal, CV)]
    interpreteds]
                                                 where mkNotEq :: a -> SVal -> SVal -> SVal
    mkNotEq k :: a
    k a :: SVal
    a b :: SVal
    b
                                                        | a -> Bool
    forall a. HasKind a => a -> Bool
    isDouble a
    k Bool -> Bool -> Bool
    || a -> Bool
    forall a. HasKind a => a -> Bool
    isFloat a
    k = SVal -> SVal
    svNot (SVal
    a SVal -> SVal -> SVal
    `fpNotEq` SVal
    b)
                                                        | Bool
    True                    = SVal
    a SVal -> SVal -> SVal
    `svNotEqual` SVal
    b

                                                       fpNotEq :: SVal -> SVal -> SVal
    fpNotEq a :: SVal
    a b :: SVal
    b = Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
                                                           where r :: State -> IO SV
    r st :: State
    st = do SV
    sva <- State -> SVal -> IO SV
    svToSV State
    st SVal
    a
                                                                           SV
    svb <- State -> SVal -> IO SV
    svToSV State
    st SVal
    b
                                                                           State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    KBool (Op -> [SV] -> SBVExpr
    SBVApp (FPOp -> Op
    IEEEFP FPOp
    FP_ObjEqual) [SV
    sva, SV
    svb])

                                              -- For each uninterpreted constant, use equivalence class
                                              uninterpretedEqs :: [SVal]
                                              uninterpretedEqs :: [SVal]
    uninterpretedEqs = ([SVal] -> [SVal]) -> [[SVal]] -> [SVal]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap [SVal] -> [SVal]
    pwDistinct         -- Assert that they are pairwise distinct
                                                               ([[SVal]] -> [SVal])
    -> ([(SVal, CV)] -> [[SVal]]) -> [(SVal, CV)] -> [SVal]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([SVal] -> Bool) -> [[SVal]] -> [[SVal]]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\l :: [SVal]
    l -> [SVal] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [SVal]
    l Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1)  -- Only need this class if it has at least two members
                                                               ([[SVal]] -> [[SVal]])
    -> ([(SVal, CV)] -> [[SVal]]) -> [(SVal, CV)] -> [[SVal]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([(SVal, CV)] -> [SVal]) -> [[(SVal, CV)]] -> [[SVal]]
    forall a b. (a -> b) -> [a] -> [b]
    map (((SVal, CV) -> SVal) -> [(SVal, CV)] -> [SVal]
    forall a b. (a -> b) -> [a] -> [b]
    map (SVal, CV) -> SVal
    forall a b. (a, b) -> a
    fst)                -- throw away values, we only need svals
                                                               ([[(SVal, CV)]] -> [[SVal]])
    -> ([(SVal, CV)] -> [[(SVal, CV)]]) -> [(SVal, CV)] -> [[SVal]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((SVal, CV) -> (SVal, CV) -> Bool)
    -> [(SVal, CV)] -> [[(SVal, CV)]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    groupBy (CV -> CV -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (CV -> CV -> Bool)
    -> ((SVal, CV) -> CV) -> (SVal, CV) -> (SVal, CV) -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (SVal, CV) -> CV
    forall a b. (a, b) -> b
    snd)      -- make sure they belong to the same sort and have the same value
                                                               ([(SVal, CV)] -> [[(SVal, CV)]])
    -> ([(SVal, CV)] -> [(SVal, CV)]) -> [(SVal, CV)] -> [[(SVal, CV)]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((SVal, CV) -> CV) -> [(SVal, CV)] -> [(SVal, CV)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    sortOn (SVal, CV) -> CV
    forall a b. (a, b) -> b
    snd                   -- sort them according to their CV (i.e., sort/value)
                                                               ([(SVal, CV)] -> [SVal]) -> [(SVal, CV)] -> [SVal]
    forall a b. (a -> b) -> a -> b
    $ [(SVal, CV)]
    uninterpreteds
                                                where pwDistinct :: [SVal] -> [SVal]
                                                      pwDistinct :: [SVal] -> [SVal]
    pwDistinct ss :: [SVal]
    ss = [SVal
    x SVal -> SVal -> SVal
    `svNotEqual` SVal
    y | (x :: SVal
    x:ys :: [SVal]
    ys) <- [SVal] -> [[SVal]]
    forall a. [a] -> [[a]]
    tails [SVal]
    ss, SVal
    y <- [SVal]
    ys]

                                              -- For each uninterpreted function, create a disqualifying equation
                                              -- We do this rather brute-force, since we need to create a new function
                                              -- and do an existential assertion.
                                              uninterpretedReject :: Maybe [String]
                                              uninterpretedFuns    :: [String]
                                              (uninterpretedReject :: Maybe [String]
    uninterpretedReject, uninterpretedFuns :: [String]
    uninterpretedFuns) = (Maybe [String]
    uiReject, [[String]] -> [String]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[String]]
    defs)
                                                  where uiReject :: Maybe [String]
    uiReject = case [String]
    rejects of
                                                                     []  -> Maybe [String]
    forall a. Maybe a
    Nothing
                                                                     xs :: [String]
    xs  -> [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [String]
    xs

                                                        (rejects :: [String]
    rejects, defs :: [[String]]
    defs) = [(String, [String])] -> ([String], [[String]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(String, (SBVType, ([([CV], CV)], CV))) -> (String, [String])
    mkNotEq (String, (SBVType, ([([CV], CV)], CV)))
    ui | ui :: (String, (SBVType, ([([CV], CV)], CV)))
    ui@(nm :: String
    nm, _) <- [(String, (SBVType, ([([CV], CV)], CV)))]
    uiFunVals, String
    nm String -> t String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` t String
    uiFunsToReject]

                                                        -- Otherwise, we have things to refute, go for it:
                                                        mkNotEq :: (String, (SBVType, ([([CV], CV)], CV))) -> (String, [String])
    mkNotEq (nm :: String
    nm, (SBVType ts :: [Kind]
    ts, vs :: ([([CV], CV)], CV)
    vs)) = (String
    reject, [String]
    def [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    dif)
                                                          where nm' :: String
    nm' = String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "_model" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    cnt

                                                                reject :: String
    reject = String
    nm' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "_reject"

                                                                -- rounding mode doesn't matter here, just pick one
                                                                scv :: CV -> String
    scv = RoundingMode -> CV -> String
    cvToSMTLib RoundingMode
    RoundNearestTiesToEven

                                                                (ats :: [Kind]
    ats, rt :: Kind
    rt) = ([Kind] -> [Kind]
    forall a. [a] -> [a]
    init [Kind]
    ts, [Kind] -> Kind
    forall a. [a] -> a
    last [Kind]
    ts)

                                                                args :: String
    args = [String] -> String
    unwords ["(x!" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")" | (t :: Kind
    t, i :: Key
    i) <- [Kind] -> [Key] -> [(Kind, Key)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Kind]
    ats [(0::Int)..]]
                                                                res :: String
    res  = Kind -> String
    smtType Kind
    rt

                                                                params :: [String]
    params = ["x!" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    i | (_, i :: Key
    i) <- [Kind] -> [Key] -> [(Kind, Key)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Kind]
    ats [(0::Int)..]]

                                                                uparams :: String
    uparams = [String] -> String
    unwords [String]
    params

                                                                chain :: ([([CV], CV)], CV) -> [String]
    chain (vals :: [([CV], CV)]
    vals, fallThru :: CV
    fallThru) = [([CV], CV)] -> [String]
    walk [([CV], CV)]
    vals
                                                                  where walk :: [([CV], CV)] -> [String]
    walk []               = ["   " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    scv CV
    fallThru String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> Char -> String
    forall a. Key -> a -> [a]
    replicate ([([CV], CV)] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [([CV], CV)]
    vals) ')']
                                                                        walk ((as :: [CV]
    as, r :: CV
    r) : rest :: [([CV], CV)]
    rest) = ("   (ite " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [CV] -> String
    cond [CV]
    as String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    scv CV
    r String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "") String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  [([CV], CV)] -> [String]
    walk [([CV], CV)]
    rest

                                                                        cond :: [CV] -> String
    cond as :: [CV]
    as = "(and " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((String -> CV -> String) -> [String] -> [CV] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith String -> CV -> String
    eq [String]
    params [CV]
    as) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                                                        eq :: String -> CV -> String
    eq p :: String
    p a :: CV
    a  = "(= " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    p String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    scv CV
    a String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"

                                                                def :: [String]
    def =    ("(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    res)
                                                                      String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  ([([CV], CV)], CV) -> [String]
    chain ([([CV], CV)], CV)
    vs
                                                                      [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [")"]

                                                                pad :: String
    pad = Key -> Char -> String
    forall a. Key -> a -> [a]
    replicate (1 Key -> Key -> Key
    forall a. Num a => a -> a -> a
    + String -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length String
    nm' Key -> Key -> Key
    forall a. Num a => a -> a -> a
    - String -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length String
    nm) ' '

                                                                dif :: [String]
    dif = [ "(define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  String
    reject String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () Bool"
                                                                      , "   (exists (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    args String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                                                      , "           (distinct (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    pad String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    uparams String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                                                      , "                     (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    nm' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    uparams String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))))"
                                                                      ]

                                              eqs :: [SVal]
    eqs = [SVal]
    interpretedEqs [SVal] -> [SVal] -> [SVal]
    forall a. [a] -> [a] -> [a]
    ++ [SVal]
    uninterpretedEqs

                                              disallow :: Maybe (SBV a)
    disallow = case [SVal]
    eqs of
                                                           [] -> Maybe (SBV a)
    forall a. Maybe a
    Nothing
                                                           _  -> SBV a -> Maybe (SBV a)
    forall a. a -> Maybe a
    Just (SBV a -> Maybe (SBV a)) -> SBV a -> Maybe (SBV a)
    forall a b. (a -> b) -> a -> b
    $ SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ (SVal -> SVal -> SVal) -> [SVal] -> SVal
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 SVal -> SVal -> SVal
    svOr [SVal]
    eqs

                                          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (SMTConfig -> Bool
    allSatPrintAlong SMTConfig
    cfg) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
                                            IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Solution #" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    cnt String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ":"
                                            IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> SMTModel -> String
    showModel SMTConfig
    cfg SMTModel
    model

                                          let resultsSoFar :: [SMTResult]
    resultsSoFar = SMTResult
    m SMTResult -> [SMTResult] -> [SMTResult]
    forall a. a -> [a] -> [a]
    : [SMTResult]
    sofar

                                              -- This is clunky, but let's not generate a rejector unless we really need it
                                              needMoreIterations :: Bool
    needMoreIterations
                                                    | Just maxModels :: Key
    maxModels <- SMTConfig -> Maybe Key
    allSatMaxModelCount SMTConfig
    cfg, (Key
    cntKey -> Key -> Key
    forall a. Num a => a -> a -> a
    +1) Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    > Key
    maxModels = Bool
    False
                                                    | Bool
    True                                                           = Bool
    True

                                          -- Send function disequalities, if any:
                                          if Bool -> Bool
    not Bool
    needMoreIterations
                                             then Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
    go (Key
    cntKey -> Key -> Key
    forall a. Num a => a -> a -> a
    +1) [SMTResult]
    resultsSoFar
                                             else do let uiFunRejector :: String
    uiFunRejector   = "uiFunRejector_model_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Key -> String
    forall a. Show a => a -> String
    show Key
    cnt
                                                         header :: String
    header          = "define-fun " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    uiFunRejector String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " () Bool "

                                                         defineRejector :: [String] -> m ()
    defineRejector []     = () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                                         defineRejector [x :: String
    x]    = Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    header String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                                         defineRejector (x :: String
    x:xs :: [String]
    xs) = (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]
    mergeSExpr ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $  ("(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    header)
                                                                                                                String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  ("        (or " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    x)
                                                                                                                String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :  ["            " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    e | String
    e <- [String]
    xs]
                                                                                                                [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["        ))"]
                                                     Maybe String
    rejectFuncs <- case Maybe [String]
    uninterpretedReject of
                                                                      Nothing -> Maybe String -> m (Maybe String)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe String
    forall a. Maybe a
    Nothing
                                                                      Just fs :: [String]
    fs -> do (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]
    mergeSExpr [String]
    uninterpretedFuns
                                                                                    [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    defineRejector [String]
    fs
                                                                                    Maybe String -> m (Maybe String)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe String -> m (Maybe String))
    -> Maybe String -> m (Maybe String)
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    uiFunRejector

                                                     -- send the disallow clause and the uninterpreted rejector:
                                                     case (Maybe SBool
    forall a. Maybe (SBV a)
    disallow, Maybe String
    rejectFuncs) of
                                                        (Nothing, Nothing) -> (Bool, Bool, [SMTResult]) -> m (Bool, Bool, [SMTResult])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, Bool
    False, [SMTResult]
    resultsSoFar)
                                                        (Just d :: SBool
    d,  Nothing) -> do SBool -> m ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain SBool
    d
                                                                                 Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
    go (Key
    cntKey -> Key -> Key
    forall a. Num a => a -> a -> a
    +1) [SMTResult]
    resultsSoFar
                                                        (Nothing, Just f :: String
    f)  -> 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
    $ "(assert " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
                                                                                 Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
    go (Key
    cntKey -> Key -> Key
    forall a. Num a => a -> a -> a
    +1) [SMTResult]
    resultsSoFar
                                                        (Just d :: SBool
    d,  Just f :: String
    f)  -> -- This is where it gets ugly. We have an SBV and a string and we need to "or" them.
                                                                              -- But we need a way to force 'd' to be produced. So, go ahead and force it:
                                                                              do SBool -> m ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> m ()) -> SBool -> m ()
    forall a b. (a -> b) -> a -> b
    $ SBool
    d SBool -> SBool -> SBool
    .=> SBool
    d  -- NB: Redundant, but it makes sure the corresponding constraint gets shown
                                                                                 SV
    svd <- IO SV -> m SV
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO SV -> m SV) -> IO SV -> m SV
    forall a b. (a -> b) -> a -> b
    $ State -> SVal -> IO SV
    svToSV State
    topState (SBool -> SVal
    forall a. SBV a -> SVal
    unSBV SBool
    d)
                                                                                 Bool -> String -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    Bool -> String -> m ()
    send Bool
    True (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ "(assert (or " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    svd String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "))"
                                                                                 Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
    go (Key
    cntKey -> Key -> Key
    forall a. Num a => a -> a -> a
    +1) [SMTResult]
    resultsSoFar

    -- | Generalization of 'Data.SBV.Control.getUnsatAssumptions'
    getUnsatAssumptions :: (MonadIO m, MonadQuery m) => [String] -> [(String, a)] -> m [a]
    getUnsatAssumptions :: [String] -> [(String, a)] -> m [a]
    getUnsatAssumptions originals :: [String]
    originals proxyMap :: [(String, a)]
    proxyMap = do
            let cmd :: String
    cmd = "(get-unsat-assumptions)"

                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 "getUnsatAssumptions" String
    cmd "a list of unsatisfiable assumptions"
                               (Maybe [String] -> String -> Maybe [String] -> m a)
    -> Maybe [String] -> String -> Maybe [String] -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [ "Make sure you use:"
                                      , ""
                                      , "       setOption $ ProduceUnsatAssumptions True"
                                      , ""
                                      , "to make sure the solver is ready for producing unsat assumptions,"
                                      , "and that there is a model by first issuing a 'checkSat' call."
                                      ]

                fromECon :: SExpr -> Maybe String
    fromECon (ECon s :: String
    s) = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    s
                fromECon _        = Maybe String
    forall a. Maybe a
    Nothing

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

            -- If unsat-cores are enabled, z3 might end-up printing an assumption that wasn't
            -- in the original list of assumptions for `check-sat-assuming`. So, we walk over
            -- and ignore those that weren't in the original list, and put a warning for those
            -- we couldn't find.
            let walk :: [String] -> [a] -> m [a]
    walk []     sofar :: [a]
    sofar = [a] -> m [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([a] -> m [a]) -> [a] -> m [a]
    forall a b. (a -> b) -> a -> b
    $ [a] -> [a]
    forall a. [a] -> [a]
    reverse [a]
    sofar
                walk (a :: String
    a:as :: [String]
    as) sofar :: [a]
    sofar = case String
    a String -> [(String, a)] -> Maybe a
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(String, a)]
    proxyMap of
                                      Just v :: a
    v  -> [String] -> [a] -> m [a]
    walk [String]
    as (a
    va -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    sofar)
                                      Nothing -> do [String] -> m ()
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
    queryDebug [ "*** In call to 'getUnsatAssumptions'"
                                                               , "***"
                                                               , "***    Unexpected assumption named: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    a
                                                               , "***    Was expecting one of       : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    forall a. Show a => a -> String
    show [String]
    originals
                                                               , "***"
                                                               , "*** This can happen if unsat-cores are also enabled. Ignoring."
                                                               ]
                                                    [String] -> [a] -> m [a]
    walk [String]
    as [a]
    sofar

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

    -- | Generalization of 'Data.SBV.Control.timeout'
    timeout :: (MonadIO m, MonadQuery m) => Int -> m a -> m a
    timeout :: Key -> m a -> m a
    timeout n :: Key
    n q :: m a
    q = do (QueryState -> QueryState) -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    (QueryState -> QueryState) -> m ()
    modifyQueryState (\qs :: QueryState
    qs -> QueryState
    qs {queryTimeOutValue :: Maybe Key
    queryTimeOutValue = Key -> Maybe Key
    forall a. a -> Maybe a
    Just Key
    n})
                     a
    r <- m a
    q
                     (QueryState -> QueryState) -> m ()
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    (QueryState -> QueryState) -> m ()
    modifyQueryState (\qs :: QueryState
    qs -> QueryState
    qs {queryTimeOutValue :: Maybe Key
    queryTimeOutValue = Maybe Key
    forall a. Maybe a
    Nothing})
                     a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r

    -- | Bail out if a parse goes bad
    parse :: String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse :: String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
    parse r :: String
    r fCont :: String -> Maybe [String] -> a
    fCont sCont :: SExpr -> a
    sCont = case String -> Either String SExpr
    parseSExpr String
    r of
                            Left  e :: String
    e   -> String -> Maybe [String] -> a
    fCont String
    r ([String] -> Maybe [String]
    forall a. a -> Maybe a
    Just [String
    e])
                            Right res :: SExpr
    res -> SExpr -> a
    sCont SExpr
    res

    -- | Generalization of 'Data.SBV.Control.unexpected'
    unexpected :: (MonadIO m, MonadQuery m) => String -> String -> String -> Maybe [String] -> String -> Maybe [String] -> m a
    unexpected :: String
    -> String
    -> String
    -> Maybe [String]
    -> String
    -> Maybe [String]
    -> m a
    unexpected ctx :: String
    ctx sent :: String
    sent expected :: String
    expected mbHint :: Maybe [String]
    mbHint received :: String
    received mbReason :: Maybe [String]
    mbReason = do
            -- empty the response channel first
            [String]
    extras <- String -> Maybe Key -> m [String]
    forall (m :: * -> *).
    (MonadIO m, MonadQuery m) =>
    String -> Maybe Key -> m [String]
    retrieveResponse "terminating upon unexpected response" (Key -> Maybe Key
    forall a. a -> Maybe a
    Just 5000000)

            SMTConfig
    cfg <- m SMTConfig
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
    getConfig

            let exc :: SBVException
    exc = SBVException :: String
    -> Maybe String
    -> Maybe String
    -> Maybe String
    -> Maybe String
    -> Maybe String
    -> Maybe ExitCode
    -> SMTConfig
    -> Maybe [String]
    -> Maybe [String]
    -> SBVException
    SBVException { sbvExceptionDescription :: String
    sbvExceptionDescription = "Unexpected response from the solver, context: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ctx
                                   , sbvExceptionSent :: Maybe String
    sbvExceptionSent        = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    sent
                                   , sbvExceptionExpected :: Maybe String
    sbvExceptionExpected    = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    expected
                                   , sbvExceptionReceived :: Maybe String
    sbvExceptionReceived    = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    received
                                   , sbvExceptionStdOut :: Maybe String
    sbvExceptionStdOut      = String -> Maybe String
    forall a. a -> Maybe a
    Just (String -> Maybe String) -> String -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [String]
    extras
                                   , sbvExceptionStdErr :: Maybe String
    sbvExceptionStdErr      = Maybe String
    forall a. Maybe a
    Nothing
                                   , sbvExceptionExitCode :: Maybe ExitCode
    sbvExceptionExitCode    = Maybe ExitCode
    forall a. Maybe a
    Nothing
                                   , sbvExceptionConfig :: SMTConfig
    sbvExceptionConfig      = SMTConfig
    cfg
                                   , sbvExceptionReason :: Maybe [String]
    sbvExceptionReason      = Maybe [String]
    mbReason
                                   , sbvExceptionHint :: Maybe [String]
    sbvExceptionHint        = Maybe [String]
    mbHint
                                   }

            IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    io (IO a -> m a) -> IO a -> m a
    forall a b. (a -> b) -> a -> b
    $ SBVException -> IO a
    forall e a. Exception e => e -> IO a
    C.throwIO SBVException
    exc

    -- | Convert a query result to an SMT Problem
    runProofOn :: SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
    runProofOn :: SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
    runProofOn rm :: SBVRunMode
    rm context :: QueryContext
    context comments :: [String]
    comments res :: Result
    res@(Result ki :: KindSet
    ki _qcInfo :: [(String, CV)]
    _qcInfo _observables :: [(String, CV -> Bool, SV)]
    _observables _codeSegs :: [(String, [String])]
    _codeSegs is :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
    is consts :: [(SV, CV)]
    consts tbls :: [((Key, Kind, Kind), [SV])]
    tbls arrs :: [(Key, ArrayInfo)]
    arrs uis :: [(String, SBVType)]
    uis axs :: [(String, [String])]
    axs pgm :: SBVPgm
    pgm cstrs :: Seq (Bool, [(String, String)], SV)
    cstrs _assertions :: [(String, Maybe CallStack, SV)]
    _assertions outputs :: [SV]
    outputs) =
         let (config :: SMTConfig
    config, isSat :: Bool
    isSat, isSafe :: Bool
    isSafe, isSetup :: Bool
    isSetup) = case SBVRunMode
    rm of
                                                  SMTMode _ stage :: IStage
    stage s :: Bool
    s c :: SMTConfig
    c -> (SMTConfig
    c, Bool
    s, IStage -> Bool
    isSafetyCheckingIStage IStage
    stage, IStage -> Bool
    isSetupIStage IStage
    stage)
                                                  _                   -> String -> (SMTConfig, Bool, Bool, Bool)
    forall a. HasCallStack => String -> a
    error (String -> (SMTConfig, Bool, Bool, Bool))
    -> String -> (SMTConfig, Bool, Bool, Bool)
    forall a b. (a -> b) -> a -> b
    $ "runProofOn: Unexpected run mode: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SBVRunMode -> String
    forall a. Show a => a -> String
    show SBVRunMode
    rm

             flipQ :: (Quantifier, b) -> (Quantifier, b)
    flipQ (ALL, x :: b
    x) = (Quantifier
    EX,  b
    x)
             flipQ (EX,  x :: b
    x) = (Quantifier
    ALL, b
    x)

             skolemize :: [(Quantifier, NamedSymVar)] -> [Either SV (SV, [SV])]
             skolemize :: [(Quantifier, NamedSymVar)] -> [Either SV (SV, [SV])]
    skolemize quants :: [(Quantifier, NamedSymVar)]
    quants = [(Quantifier, NamedSymVar)]
    -> ([SV], [Either SV (SV, [SV])]) -> [Either SV (SV, [SV])]
    forall a b.
    [(Quantifier, (a, b))]
    -> ([a], [Either a (a, [a])]) -> [Either a (a, [a])]
    go [(Quantifier, NamedSymVar)]
    quants ([], [])
               where go :: [(Quantifier, (a, b))]
    -> ([a], [Either a (a, [a])]) -> [Either a (a, [a])]
    go []                   (_,  sofar :: [Either a (a, [a])]
    sofar) = [Either a (a, [a])] -> [Either a (a, [a])]
    forall a. [a] -> [a]
    reverse [Either a (a, [a])]
    sofar
                     go ((ALL, (v :: a
    v, _)):rest :: [(Quantifier, (a, b))]
    rest) (us :: [a]
    us, sofar :: [Either a (a, [a])]
    sofar) = [(Quantifier, (a, b))]
    -> ([a], [Either a (a, [a])]) -> [Either a (a, [a])]
    go [(Quantifier, (a, b))]
    rest (a
    va -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    us, a -> Either a (a, [a])
    forall a b. a -> Either a b
    Left a
    v Either a (a, [a]) -> [Either a (a, [a])] -> [Either a (a, [a])]
    forall a. a -> [a] -> [a]
    : [Either a (a, [a])]
    sofar)
                     go ((EX,  (v :: a
    v, _)):rest :: [(Quantifier, (a, b))]
    rest) (us :: [a]
    us, sofar :: [Either a (a, [a])]
    sofar) = [(Quantifier, (a, b))]
    -> ([a], [Either a (a, [a])]) -> [Either a (a, [a])]
    go [(Quantifier, (a, b))]
    rest ([a]
    us,   (a, [a]) -> Either a (a, [a])
    forall a b. b -> Either a b
    Right (a
    v, [a] -> [a]
    forall a. [a] -> [a]
    reverse [a]
    us) Either a (a, [a]) -> [Either a (a, [a])] -> [Either a (a, [a])]
    forall a. a -> [a] -> [a]
    : [Either a (a, [a])]
    sofar)

             qinps :: [(Quantifier, NamedSymVar)]
    qinps      = if Bool
    isSat then ([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> [(Quantifier, NamedSymVar)]
    forall a b. (a, b) -> a
    fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
    is else ((Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar))
    -> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar)
    forall b. (Quantifier, b) -> (Quantifier, b)
    flipQ (([(Quantifier, NamedSymVar)], [NamedSymVar])
    -> [(Quantifier, NamedSymVar)]
    forall a b. (a, b) -> a
    fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
    is)
             skolemMap :: [Either SV (SV, [SV])]
    skolemMap  = [(Quantifier, NamedSymVar)] -> [Either SV (SV, [SV])]
    skolemize [(Quantifier, NamedSymVar)]
    qinps

             o :: SV
    o | Bool
    isSafe = SV
    trueSV
               | Bool
    True   = case [SV]
    outputs of
                            []  | Bool
    isSetup -> SV
    trueSV
                            [so :: SV
    so]          -> case SV
    so of
                                               SV KBool _ -> SV
    so
                                               _          -> String -> SV
    forall a. HasCallStack => String -> a
    error (String -> SV) -> String -> SV
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "Impossible happened, non-boolean output: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SV -> String
    forall a. Show a => a -> String
    show SV
    so
                                                                             , "Detected while generating the trace:\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Result -> String
    forall a. Show a => a -> String
    show Result
    res
                                                                             ]
                            os :: [SV]
    os  -> String -> SV
    forall a. HasCallStack => String -> a
    error (String -> SV) -> String -> SV
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ "User error: Multiple output values detected: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [SV] -> String
    forall a. Show a => a -> String
    show [SV]
    os
                                                   , "Detected while generating the trace:\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Result -> String
    forall a. Show a => a -> String
    show Result
    res
                                                   , "*** Check calls to \"output\", they are typically not needed!"
                                                   ]

         in SMTProblem :: (SMTConfig -> SMTLibPgm) -> SMTProblem
    SMTProblem { smtLibPgm :: SMTConfig -> SMTLibPgm
    smtLibPgm = SMTConfig -> SMTLibConverter SMTLibPgm
    toSMTLib SMTConfig
    config QueryContext
    context KindSet
    ki Bool
    isSat [String]
    comments ([(Quantifier, NamedSymVar)], [NamedSymVar])
    is [Either SV (SV, [SV])]
    skolemMap [(SV, CV)]
    consts [((Key, Kind, Kind), [SV])]
    tbls [(Key, ArrayInfo)]
    arrs [(String, SBVType)]
    uis [(String, [String])]
    axs SBVPgm
    pgm Seq (Bool, [(String, String)], SV)
    cstrs SV
    o }

    -- | Generalization of 'Data.SBV.Control.executeQuery'
    executeQuery :: forall m a. ExtractIO m => QueryContext -> QueryT m a -> SymbolicT m a
    executeQuery :: QueryContext -> QueryT m a -> SymbolicT m a
    executeQuery queryContext :: QueryContext
    queryContext (QueryT userQuery :: ReaderT State m a
    userQuery) = do
         State
    st <- SymbolicT m State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv
         SBVRunMode
    rm <- IO SBVRunMode -> SymbolicT m SBVRunMode
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBVRunMode -> SymbolicT m SBVRunMode)
    -> IO SBVRunMode -> SymbolicT m SBVRunMode
    forall a b. (a -> b) -> a -> b
    $ IORef SBVRunMode -> IO SBVRunMode
    forall a. IORef a -> IO a
    readIORef (State -> IORef SBVRunMode
    runMode State
    st)

         -- Make sure the phases match:
         () <- IO () -> SymbolicT m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ case (QueryContext
    queryContext, SBVRunMode
    rm) of
                          (QueryInternal, _)                                -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()  -- no worries, internal
                          (QueryExternal, SMTMode QueryExternal ISetup _ _) -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return () -- legitimate runSMT call
                          _                                                 -> SBVRunMode -> IO ()
    forall a a. Show a => a -> a
    invalidQuery SBVRunMode
    rm

         -- If we're doing an external query, then we cannot allow quantifiers to be present. Why?
         -- Consider:
         --
         --      issue = do x :: SBool <- forall_
         --                 y :: SBool <- exists_
         --                 constrain y
         --                 query $ do checkSat
         --                         (,) <$> getValue x <*> getValue y
         --
         -- This is the (simplified/annotated SMTLib we would generate:)
         --
         --     (declare-fun s1 (Bool) Bool)   ; s1 is the function that corresponds to the skolemized 'y'
         --     (assert (forall ((s0 Bool))    ; s0 is 'x'
         --                 (s1 s0)))          ; s1 applied to s0 is the actual 'y'
         --     (check-sat)
         --     (get-value (s0))        ; s0 simply not visible here
         --     (get-value (s1))        ; s1 is visible, but only via 's1 s0', so it is also not available.
         --
         -- And that would be terrible! The scoping rules of our "quantified" variables and how they map to
         -- SMTLib is just not compatible. This is a historical design issue, but too late at this point. (We
         -- should've never allowed general quantification like this, but only in limited contexts.)
         --
         -- So, we check if this is an external-query, and if there are quantified variables. If so, we
         -- cowardly refuse to continue. For details, see: <http://github.com/LeventErkok/sbv/issues/407>
         --
         -- However, as discussed in <https://github.com/LeventErkok/sbv/issues/459>, we'll allow for this
         -- if the user explicitly asks as to do so. In that case, all bets are off!

         let allowQQs :: Bool
    allowQQs = case SBVRunMode
    rm of
                          SMTMode _ _ _ cfg :: SMTConfig
    cfg -> SMTConfig -> Bool
    allowQuantifiedQueries SMTConfig
    cfg
                          CodeGen           -> Bool
    False -- doesn't matter in these two
                          Concrete{}        -> Bool
    False -- cases, but we're being careful

         () <- Bool -> SymbolicT m () -> SymbolicT m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    allowQQs (SymbolicT m () -> SymbolicT m ())
    -> SymbolicT m () -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ IO () -> SymbolicT m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $
                        case QueryContext
    queryContext of
                          QueryInternal -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()         -- we're good, internal usages don't mess with scopes
                          QueryExternal -> do
                            ((userInps :: [(Quantifier, NamedSymVar)]
    userInps, _), _) <- IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    forall a. IORef a -> IO a
    readIORef (State
    -> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    rinps State
    st)
                            let badInps :: [String]
    badInps = [String] -> [String]
    forall a. [a] -> [a]
    reverse [String
    n | (ALL, (_, n :: String
    n)) <- [(Quantifier, NamedSymVar)]
    userInps]
                            case [String]
    badInps of
                              [] -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                              _  -> let plu :: String
    plu | [String] -> Key
    forall (t :: * -> *) a. Foldable t => t a -> Key
    length [String]
    badInps Key -> Key -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1 = "s require"
                                            | Bool
    True               = " requires"
                                    in String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                       , "*** Data.SBV: Unsupported query call in the presence of quantified inputs."
                                                       , "***"
                                                       , "*** The following variable" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    plu String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " explicit quantification: "
                                                       , "***"
                                                       , "***    " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    badInps
                                                       , "***"
                                                       , "*** While quantification and queries can co-exist in principle, SBV currently"
                                                       , "*** does not support this scenario. Avoid using quantifiers with user queries"
                                                       , "*** if possible. Please do get in touch if your use case does require such"
                                                       , "*** a feature to see how we can accommodate such scenarios."
                                                       ]

         case SBVRunMode
    rm of
            -- Transitioning from setup
            SMTMode qc :: QueryContext
    qc stage :: IStage
    stage isSAT :: Bool
    isSAT cfg :: SMTConfig
    cfg | Bool -> Bool
    not (IStage -> Bool
    isRunIStage IStage
    stage) -> do

                                                    let backend :: SMTConfig -> State -> String -> (State -> IO res) -> IO res
    backend = SMTSolver
    -> forall res.
       SMTConfig -> State -> String -> (State -> IO res) -> IO res
    engine (SMTConfig -> SMTSolver
    solver SMTConfig
    cfg)

                                                    Result
    res     <- IO Result -> SymbolicT m Result
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Result -> SymbolicT m Result)
    -> IO Result -> SymbolicT m Result
    forall a b. (a -> b) -> a -> b
    $ State -> IO Result
    extractSymbolicSimulationState State
    st
                                                    [SMTOption]
    setOpts <- IO [SMTOption] -> SymbolicT m [SMTOption]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [SMTOption] -> SymbolicT m [SMTOption])
    -> IO [SMTOption] -> SymbolicT m [SMTOption]
    forall a b. (a -> b) -> a -> b
    $ [SMTOption] -> [SMTOption]
    forall a. [a] -> [a]
    reverse ([SMTOption] -> [SMTOption]) -> IO [SMTOption] -> IO [SMTOption]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IORef [SMTOption] -> IO [SMTOption]
    forall a. IORef a -> IO a
    readIORef (State -> IORef [SMTOption]
    rSMTOptions State
    st)

                                                    let SMTProblem{SMTConfig -> SMTLibPgm
    smtLibPgm :: SMTConfig -> SMTLibPgm
    smtLibPgm :: SMTProblem -> SMTConfig -> SMTLibPgm
    smtLibPgm} = SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
    runProofOn SBVRunMode
    rm QueryContext
    queryContext [] Result
    res
                                                        cfg' :: SMTConfig
    cfg' = SMTConfig
    cfg { solverSetOptions :: [SMTOption]
    solverSetOptions = SMTConfig -> [SMTOption]
    solverSetOptions SMTConfig
    cfg [SMTOption] -> [SMTOption] -> [SMTOption]
    forall a. [a] -> [a] -> [a]
    ++ [SMTOption]
    setOpts }
                                                        pgm :: SMTLibPgm
    pgm  = SMTConfig -> SMTLibPgm
    smtLibPgm SMTConfig
    cfg'

                                                    IO () -> SymbolicT m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
    forall a b. (a -> b) -> a -> b
    $ IORef SBVRunMode -> SBVRunMode -> IO ()
    forall a. IORef a -> a -> IO ()
    writeIORef (State -> IORef SBVRunMode
    runMode State
    st) (SBVRunMode -> IO ()) -> SBVRunMode -> IO ()
    forall a b. (a -> b) -> a -> b
    $ QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
    SMTMode QueryContext
    qc IStage
    IRun Bool
    isSAT SMTConfig
    cfg

                                                    m a -> SymbolicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m a -> SymbolicT m a) -> m a -> SymbolicT m a
    forall a b. (a -> b) -> a -> b
    $ m (m a) -> m a
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (m (m a) -> m a) -> m (m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ IO (m a) -> m (m a)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (m a) -> m (m a)) -> IO (m a) -> m (m a)
    forall a b. (a -> b) -> a -> b
    $ SMTConfig -> State -> String -> (State -> IO (m a)) -> IO (m a)
    forall res.
    SMTConfig -> State -> String -> (State -> IO res) -> IO res
    backend SMTConfig
    cfg' State
    st (SMTLibPgm -> String
    forall a. Show a => a -> String
    show SMTLibPgm
    pgm) ((State -> IO (m a)) -> IO (m a))
    -> (State -> IO (m a)) -> IO (m a)
    forall a b. (a -> b) -> a -> b
    $ m a -> IO (m a)
    forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
    extractIO (m a -> IO (m a)) -> (State -> m a) -> State -> IO (m a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ReaderT State m a -> State -> m a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT State m a
    userQuery

            -- Already in a query, in theory we can just continue, but that causes use-case issues
            -- so we reject it. TODO: Review if we should actually support this. The issue arises with
            -- expressions like this:
            --
            -- In the following t0's output doesn't get recorded, as the output call is too late when we get
            -- here. (The output field isn't "incremental.") So, t0/t1 behave differently!
            --
            --   t0 = satWith z3{verbose=True, transcript=Just "t.smt2"} $ query (return (false::SBool))
            --   t1 = satWith z3{verbose=True, transcript=Just "t.smt2"} $ ((return (false::SBool)) :: Predicate)
            --
            -- Also, not at all clear what it means to go in an out of query mode:
            --
            -- r = runSMTWith z3{verbose=True} $ do
            --         a' <- sInteger "a"
            --
            --        (a, av) <- query $ do _ <- checkSat
            --                              av <- getValue a'
            --                              return (a', av)
            --
            --        liftIO $ putStrLn $ "Got: " ++ show av
            --        -- constrain $ a .> literal av + 1      -- Cant' do this since we're "out" of query. Sigh.
            --
            --        bv <- query $ do constrain $ a .> literal av + 1
            --                         _ <- checkSat
            --                         getValue a
            --
            --        return $ a' .== a' + 1
            --
            -- This would be one possible implementation, alas it has the problems above:
            --
            --    SMTMode IRun _ _ -> liftIO $ evalStateT userQuery st
            --
            -- So, we just reject it.

            SMTMode _ IRun _ _ -> String -> SymbolicT m a
    forall a. HasCallStack => String -> a
    error (String -> SymbolicT m a) -> String -> SymbolicT m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                  , "*** Data.SBV: Unsupported nested query is detected."
                                                  , "***"
                                                  , "*** Please group your queries into one block. Note that this"
                                                  , "*** can also arise if you have a call to 'query' not within 'runSMT'"
                                                  , "*** For instance, within 'sat'/'prove' calls with custom user queries."
                                                  , "*** The solution is to do the sat/prove part in the query directly."
                                                  , "***"
                                                  , "*** While multiple/nested queries should not be necessary in general,"
                                                  , "*** please do get in touch if your use case does require such a feature,"
                                                  , "*** to see how we can accommodate such scenarios."
                                                  ]

            -- Otherwise choke!
            _ -> SBVRunMode -> SymbolicT m a
    forall a a. Show a => a -> a
    invalidQuery SBVRunMode
    rm

      where invalidQuery :: a -> a
    invalidQuery rm :: a
    rm = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                              , "*** Data.SBV: Invalid query call."
                                              , "***"
                                              , "***   Current mode: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    rm
                                              , "***"
                                              , "*** Query calls are only valid within runSMT/runSMTWith calls"
                                              ]

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