content: -----------------------------------------------------------------------------
  -- |
  -- Module    : Data.SBV.Control.Query
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Querying a solver interactively.
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE BangPatterns        #-}
  {-# LANGUAGE LambdaCase          #-}
  {-# LANGUAGE NamedFieldPuns      #-}
  {-# LANGUAGE Rank2Types          #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TupleSections       #-}
  {-# LANGUAGE ViewPatterns        #-}
  
  {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
  
  module Data.SBV.Control.Query (
         send, ask, retrieveResponse
       , CheckSatResult(..), checkSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
       , getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3, getAbduct, getAbductNext, getAssignment, getOption
       , push, pop, getAssertionStackDepth
       , inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getModel, getSMTResult
       , getLexicographicOptResults, getIndependentOptResults, getParetoOptResults, getAllSatResult, getUnknownReason, getObservables, ensureSat
       , SMTOption(..), SMTInfoFlag(..), SMTErrorBehavior(..), SMTReasonUnknown(..), SMTInfoResponse(..), getInfo
       , Logic(..), Assignment(..)
       , ignoreExitCode, timeout
       , (|->)
       , mkSMTResult
       , io
       ) where
  
  import Control.Monad          (unless, when, zipWithM)
  import Control.Monad.IO.Class (MonadIO)
  
  import Data.IORef (readIORef)
  
  import qualified Data.Map.Strict as M
  import qualified Data.Sequence   as S
  import qualified Data.Text       as T
  import qualified Data.Foldable   as F
  
  
  import Data.Char      (toLower)
  import Data.List      (intercalate, nubBy, sortOn)
  import Data.Maybe     (listToMaybe, catMaybes, fromMaybe)
  import Data.Function  (on)
  import Data.Bifunctor (first)
  import Data.Foldable  (toList)
  
  import Data.SBV.Core.Data
  
  import Data.SBV.Core.Symbolic (MonadQuery(..), State(..), incrementInternalCounter, validationRequested, getSV, lookupInput, mustIgnoreVar)
  
  import Data.SBV.Utils.SExpr
  
  import Data.SBV.Control.Types
  import Data.SBV.Control.Utils
  
  import Data.SBV.Utils.Lib       (unBar)
  import Data.SBV.Utils.PrettyNum (showNegativeNumber)
  
  -- | An Assignment of a model binding
  data Assignment = Assign SVal CV
  
  -- | Remove the bars from model names; these are (mostly!) automatically inserted
  unBarModel :: SMTModel -> SMTModel
  unBarModel SMTModel {modelObjectives, modelBindings, modelAssocs, modelUIFuns}
     = SMTModel { modelObjectives = ubf       <$> modelObjectives
                , modelBindings   = (ubn <$>) <$> modelBindings
                , modelAssocs     = ubf       <$> modelAssocs
                , modelUIFuns     = ubf       <$> modelUIFuns
                }
     where ubf (n, a) = (unBar n, a)
           ubn (NamedSymVar sv nm, a) = (NamedSymVar sv (T.pack (unBar (T.unpack nm))), a)
  
  -- Is this a string? If so, return it, otherwise fail in the Maybe monad.
  fromECon :: SExpr -> Maybe String
  fromECon (ECon s) = Just s
  fromECon _        = Nothing
  
  -- Collect strings appearing, used in 'getOption' only
  stringsOf :: SExpr -> [String]
  stringsOf (ECon s)           = [s]
  stringsOf (ENum (i, _, _))   = [show i]
  stringsOf (EReal   r)        = [show r]
  stringsOf (EFloat  f)        = [show f]
  stringsOf (EFloatingPoint f) = [show f]
  stringsOf (EDouble d)        = [show d]
  stringsOf (EApp ss)          = concatMap stringsOf ss
  
  -- Sort of a light-hearted show for SExprs, for better consumption at the user level.
  serialize :: Bool -> SExpr -> String
  serialize removeQuotes = go
    where go (ECon s)           = if removeQuotes then unQuote s else s
          go (ENum (i, _, _))   = showNegativeNumber i
          go (EReal   r)        = showNegativeNumber r
          go (EFloat  f)        = showNegativeNumber f
          go (EDouble d)        = showNegativeNumber d
          go (EFloatingPoint f) = show f
          go (EApp [x])         = go x
          go (EApp ss)          = "(" ++ unwords (map go ss) ++ ")"
  
  -- | Generalization of 'Data.SBV.Control.getInfo'
  getInfo :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse
  getInfo flag = do
      let cmd = "(get-info " ++ show flag ++ ")"
          bad = unexpected "getInfo" cmd "a valid get-info response" Nothing
  
          isAllStatistics AllStatistics = True
          isAllStatistics _             = False
  
          isAllStat = isAllStatistics flag
  
          grabAllStat k v = (render k, render v)
  
          -- we're trying to do our best to get key-value pairs here, but this
          -- is necessarily a half-hearted attempt.
          grabAllStats (EApp xs) = walk xs
             where walk []             = []
                   walk [t]            = [grabAllStat t (ECon "")]
                   walk (t : v : rest) =  grabAllStat t v          : walk rest
          grabAllStats o = [grabAllStat o (ECon "")]
  
      r <- ask cmd
  
      parse r bad $ \pe ->
         if isAllStat
            then return $ Resp_AllStatistics $ grabAllStats pe
            else case pe of
                   ECon "unsupported"                                        -> return Resp_Unsupported
                   EApp [ECon ":assertion-stack-levels", ENum (i, _, _)]     -> return $ Resp_AssertionStackLevels i
                   EApp (ECon ":authors" : ns)                               -> return $ Resp_Authors (map render ns)
                   EApp [ECon ":error-behavior", ECon "immediate-exit"]      -> return $ Resp_Error ErrorImmediateExit
                   EApp [ECon ":error-behavior", ECon "continued-execution"] -> return $ Resp_Error ErrorContinuedExecution
                   EApp (ECon ":name" : o)                                   -> return $ Resp_Name (render (EApp o))
                   EApp (ECon ":reason-unknown" : o)                         -> return $ Resp_ReasonUnknown (unk o)
                   EApp (ECon ":version" : o)                                -> return $ Resp_Version (render (EApp o))
                   EApp (ECon s : o)                                         -> return $ Resp_InfoKeyword s (map render o)
                   _                                                         -> bad r Nothing
  
    where render = serialize True
  
          unk [ECon s] | Just d <- getUR s = d
          unk o                            = UnknownOther (render (EApp o))
  
          getUR s = map toLower (unQuote s) `lookup` [(map toLower k, d) | (k, d) <- unknownReasons]
  
          -- As specified in Section 4.1 of the SMTLib document. Note that we're adding the
          -- extra timeout as it is useful in this context.
          unknownReasons = [ ("memout",     UnknownMemOut)
                           , ("incomplete", UnknownIncomplete)
                           , ("timeout",    UnknownTimeOut)
                           ]
  
  -- | Generalization of 'Data.SBV.Control.getOption'
  getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption)
  getOption f = case f undefined of
                   DiagnosticOutputChannel{}   -> askFor "DiagnosticOutputChannel"   ":diagnostic-output-channel"   $ string     DiagnosticOutputChannel
                   ProduceAssertions{}         -> askFor "ProduceAssertions"         ":produce-assertions"          $ bool       ProduceAssertions
                   ProduceAssignments{}        -> askFor "ProduceAssignments"        ":produce-assignments"         $ bool       ProduceAssignments
                   ProduceProofs{}             -> askFor "ProduceProofs"             ":produce-proofs"              $ bool       ProduceProofs
                   ProduceInterpolants{}       -> askFor "ProduceInterpolants"       ":produce-interpolants"        $ bool       ProduceInterpolants
                   ProduceUnsatAssumptions{}   -> askFor "ProduceUnsatAssumptions"   ":produce-unsat-assumptions"   $ bool       ProduceUnsatAssumptions
                   ProduceUnsatCores{}         -> askFor "ProduceUnsatCores"         ":produce-unsat-cores"         $ bool       ProduceUnsatCores
                   ProduceAbducts{}            -> askFor "ProduceAbducts"            ":produce-abducts"             $ bool       ProduceAbducts
                   RandomSeed{}                -> askFor "RandomSeed"                ":random-seed"                 $ integer    RandomSeed
                   ReproducibleResourceLimit{} -> askFor "ReproducibleResourceLimit" ":reproducible-resource-limit" $ integer    ReproducibleResourceLimit
                   SMTVerbosity{}              -> askFor "SMTVerbosity"              ":verbosity"                   $ integer    SMTVerbosity
                   OptionKeyword nm _          -> askFor ("OptionKeyword" ++ nm)     nm                             $ stringList (OptionKeyword nm)
                   SetLogic{}                  -> error "Data.SBV.Query: SMTLib does not allow querying the value of logic!"
                   SetTimeOut{}                -> error "Data.SBV.Query: SMTLib does not allow querying the timeout value!"
                   -- Not to be confused by getInfo, which is totally irrelevant!
                   SetInfo{}                   -> error "Data.SBV.Query: SMTLib does not allow querying value of meta-info!"
  
    where askFor sbvName smtLibName continue = do
                  let cmd = "(get-option " ++ smtLibName ++ ")"
                      bad = unexpected ("getOption " ++ sbvName) cmd "a valid option value" Nothing
  
                  r <- ask cmd
  
                  parse r bad $ \case ECon "unsupported" -> return Nothing
                                      e                  -> continue e (bad r)
  
          string c (ECon s) _ = return $ Just $ c s
          string _ e        k = k $ Just ["Expected string, but got: " ++ show (serialize False e)]
  
          bool c (ENum (0, _, True)) _ = return $ Just $ c False
          bool c (ENum (1, _, True)) _ = return $ Just $ c True
          bool _ e                   k = k $ Just ["Expected boolean, but got: " ++ show (serialize False e)]
  
          integer c (ENum (i, _, _)) _ = return $ Just $ c i
          integer _ e                k = k $ Just ["Expected integer, but got: " ++ show (serialize False e)]
  
          -- free format, really
          stringList c e _ = return $ Just $ c $ stringsOf e
  
  -- | Generalization of 'Data.SBV.Control.getUnknownReason'
  getUnknownReason :: (MonadIO m, MonadQuery m) => m SMTReasonUnknown
  getUnknownReason = do ru <- getInfo ReasonUnknown
                        case ru of
                          Resp_Unsupported     -> return $ UnknownOther "Solver responded: Unsupported."
                          Resp_ReasonUnknown r -> return r
                          -- Shouldn't happen, but just in case:
                          _                    -> error $ "Unexpected reason value received: " ++ show ru
  
  -- | Generalization of 'Data.SBV.Control.ensureSat'
  ensureSat :: (MonadIO m, MonadQuery m) => m ()
  ensureSat = do cfg <- getConfig
                 cs <- checkSatUsing $ satCmd cfg
                 case cs of
                   Sat    -> return ()
                   DSat{} -> return ()
                   Unk    -> do s <- getUnknownReason
                                error $ unlines [ ""
                                                , "*** Data.SBV.ensureSat: Solver reported Unknown!"
                                                , "*** Reason: " ++ show s
                                                ]
                   Unsat  -> error "Data.SBV.ensureSat: Solver reported Unsat!"
  
  -- | Generalization of 'Data.SBV.Control.getSMTResult'
  getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult
  getSMTResult = do cfg <- getConfig
                    cs  <- checkSat
                    case cs of
                      Unsat  -> Unsatisfiable cfg   <$> getUnsatCoreIfRequested
                      Sat    -> Satisfiable   cfg   <$> getModel
                      DSat p -> DeltaSat      cfg p <$> getModel
                      Unk    -> Unknown       cfg   <$> getUnknownReason
  
  -- | Classify a model based on whether it has unbound objectives or not.
  classifyModel :: SMTConfig -> SMTModel -> SMTResult
  classifyModel cfg m
    | any isExt (modelObjectives m) = SatExtField cfg m
    | True                          = Satisfiable cfg m
    where isExt (_, v) = not $ isRegularCV v
  
  -- | Generalization of 'Data.SBV.Control.getLexicographicOptResults'
  getLexicographicOptResults :: (MonadIO m, MonadQuery m) => m SMTResult
  getLexicographicOptResults = do cfg <- getConfig
                                  cs  <- checkSat
                                  case cs of
                                    Unsat  -> Unsatisfiable cfg <$> getUnsatCoreIfRequested
                                    Sat    -> classifyModel cfg <$> getModelWithObjectives
                                    DSat{} -> classifyModel cfg <$> getModelWithObjectives
                                    Unk    -> Unknown       cfg <$> getUnknownReason
     where getModelWithObjectives = do objectiveValues <- getObjectiveValues
                                       m               <- getModel
                                       return m {modelObjectives = objectiveValues}
  
  -- | Generalization of 'Data.SBV.Control.getIndependentOptResults'
  getIndependentOptResults :: forall m. (MonadIO m, MonadQuery m) => [String] -> m [(String, SMTResult)]
  getIndependentOptResults objNames = do cfg <- getConfig
                                         cs  <- checkSat
  
                                         case cs of
                                           Unsat  -> getUnsatCoreIfRequested >>= \mbUC -> return [(nm, Unsatisfiable cfg mbUC) | nm <- objNames]
                                           Sat    -> continue (classifyModel cfg)
                                           DSat{} -> continue (classifyModel cfg)
                                           Unk    -> do ur <- Unknown cfg <$> getUnknownReason
                                                        return [(nm, ur) | nm <- objNames]
  
    where continue classify = do objectiveValues <- getObjectiveValues
                                 nms <- zipWithM getIndependentResult [0..] objNames
                                 return [(n, classify (m {modelObjectives = objectiveValues})) | (n, m) <- nms]
  
          getIndependentResult :: Int -> String -> m (String, SMTModel)
          getIndependentResult i s = do m <- getModelAtIndex (Just i)
                                        return (s, m)
  
  -- | Generalization of 'Data.SBV.Control.getParetoOptResults'
  getParetoOptResults :: (MonadIO m, MonadQuery m) => Maybe Int -> m (Bool, [SMTResult])
  getParetoOptResults (Just i)
          | i <= 0             = return (True, [])
  getParetoOptResults mbN      = do cfg <- getConfig
                                    cs  <- checkSat
  
                                    case cs of
                                      Unsat  -> return (False, [])
                                      Sat    -> continue (classifyModel cfg)
                                      DSat{} -> continue (classifyModel cfg)
                                      Unk    -> do ur <- getUnknownReason
                                                   return (False, [ProofError cfg [show ur] Nothing])
  
    where continue classify = do m <- getModel
                                 (limReached, fronts) <- getParetoFronts (subtract 1 <$> mbN) [m]
                                 return (limReached, reverse (map classify fronts))
  
          getParetoFronts :: (MonadIO m, MonadQuery m) => Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
          getParetoFronts (Just i) sofar | i <= 0 = return (True, sofar)
          getParetoFronts mbi      sofar          = do cs <- checkSat
                                                       let more = getModel >>= \m -> getParetoFronts (subtract 1 <$> mbi) (m : sofar)
                                                       case cs of
                                                         Unsat  -> return (False, sofar)
                                                         Sat    -> more
                                                         DSat{} -> more
                                                         Unk    -> more
  
  -- | Generalization of 'Data.SBV.Control.getModel'
  getModel :: (MonadIO m, MonadQuery m) => m SMTModel
  getModel = getModelAtIndex Nothing
  
  -- | Get a model stored at an index. This is likely very Z3 specific!
  getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel
  getModelAtIndex mbi = do
      State{runMode} <- queryState
      rm <- io $ readIORef runMode
      case rm of
        m@CodeGen     -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
        m@LambdaGen{} -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
        m@Concrete{}  -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
        SMTMode{}     -> do
            cfg <- getConfig
            uis <- getUIs
  
            allModelInputs <- getTopLevelInputs
            obsvs          <- getObservables
  
            inputAssocs <- let grab (NamedSymVar sv nm) = let wrap !c = (sv, (nm, c)) in wrap <$> getValueCV mbi sv
                           in mapM grab allModelInputs
  
            let name     = fst . snd
                removeSV = snd
                prepare  = S.unstableSort . S.filter (not . mustIgnoreVar cfg . T.unpack . name)
                assocs   = fmap removeSV (prepare inputAssocs) <> S.fromList (sortOn fst obsvs)
  
            -- collect UIs, and UI functions if requested
            let uiFuns = [ui | ui@(nm, (_, _, SBVType as)) <- uis, length as >  1, allSatTrackUFs cfg, not (mustIgnoreVar cfg nm)] -- functions have at least two things in their type!
                uiRegs = [ui | ui@(nm, (_, _, SBVType as)) <- uis, length as == 1,                     not (mustIgnoreVar cfg nm)]
  
            -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out
            -- as cex's tend to get larger
            unless (null uiFuns) $
               let solverCaps = capabilities (solver cfg)
               in case supportsFlattenedModels solverCaps of
                    Nothing   -> return ()
                    Just cmds -> mapM_ (send True) cmds
  
            bindings <- let get i@(getSV -> sv) = case lookupInput fst sv inputAssocs of
                                                    Just (_, (_, cv)) -> return (i, cv)
                                                    Nothing           -> do cv <- getValueCV mbi sv
                                                                            return (i, cv)
  
                        in if validationRequested cfg
                           then Just <$> mapM get allModelInputs
                           else return Nothing
  
            uiFunVals <- mapM (\ui@(nm, (c, _, t)) -> (\a -> (nm, (c, t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns
  
            uiVals    <- mapM (\ui@(nm, (_, _, _)) -> (nm,) <$> getUICVal mbi ui) uiRegs
  
            return $ unBarModel $ SMTModel { modelObjectives = []
                                           , modelBindings   = toList <$> bindings
                                           , modelAssocs     = uiVals ++ toList (first T.unpack <$> assocs)
                                           , modelUIFuns     = uiFunVals
                                           }
  
  -- | Just after a check-sat is issued, collect objective values. Used
  -- internally only, not exposed to the user.
  getObjectiveValues :: forall m. (MonadIO m, MonadQuery m) => m [(String, GeneralizedCV)]
  getObjectiveValues = do let cmd = "(get-objectives)"
  
                              bad = unexpected "getObjectiveValues" cmd "a list of objective values" Nothing
  
                          r <- ask cmd
  
                          si <- queryState >>= getSInfo
  
                          inputs <- F.toList <$> getTopLevelInputs
  
                          parse r bad $ \case EApp (ECon "objectives" : es) -> catMaybes <$> mapM (getObjValue si (bad r) inputs) es
                                              _                             -> bad r Nothing
  
    where -- | Parse an objective value out.
          getObjValue :: SInfo -> (forall a. Maybe [String] -> m a) -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
          getObjValue si bailOut inputs expr =
                  case expr of
                    EApp [_]          -> return Nothing            -- Happens when a soft-assertion has no associated group.
                    EApp [ECon nm, v] -> locate nm v               -- Regular case
                    _                 -> dontUnderstand (show expr)
  
            where locate nm v = case listToMaybe [p | p@(NamedSymVar sv _) <- inputs, show sv == nm] of
                                  Nothing                          -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names
                                  Just (NamedSymVar sv actualName) -> grab sv v >>= \val -> return $ Just (T.unpack actualName, val)
  
                  dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."
                                                    , "While trying to process: " ++ s
                                                    ]
  
                  grab :: SV -> SExpr -> m GeneralizedCV
                  grab s topExpr
                    | Just v <- recoverKindedValue si k topExpr = return $ RegularCV v
                    | True                                      = ExtendedCV <$> cvt (simplify topExpr)
                    where k = kindOf s
  
                          -- Convert to an extended expression. Hopefully complete!
                          cvt :: SExpr -> m ExtCV
                          cvt (ECon "oo")                    = return $ Infinite  k
                          cvt (ECon "epsilon")               = return $ Epsilon   k
                          cvt (EApp [ECon "interval", x, y]) =          Interval  <$> cvt x <*> cvt y
                          cvt (ENum    (i, _, _))            = return $ BoundedCV $ mkConstCV k i
                          cvt (EReal   r)                    = return $ BoundedCV $ CV k $ CAlgReal r
                          cvt (EFloat  f)                    = return $ BoundedCV $ CV k $ CFloat   f
                          cvt (EDouble d)                    = return $ BoundedCV $ CV k $ CDouble  d
                          cvt (EApp [ECon "+", x, y])        =          AddExtCV <$> cvt x <*> cvt y
                          cvt (EApp [ECon "*", x, y])        =          MulExtCV <$> cvt x <*> cvt y
                          -- Nothing else should show up, hopefully!
                          cvt e = dontUnderstand (show e)
  
                          -- drop the pesky to_real's that Z3 produces.. Cool but useless.
                          simplify :: SExpr -> SExpr
                          simplify (EApp [ECon "to_real", n]) = n
                          simplify (EApp xs)                  = EApp (map simplify xs)
                          simplify e                          = e
  
  -- | Generalization of 'Data.SBV.Control.checkSatAssuming'
  checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult
  checkSatAssuming sBools = fst <$> checkSatAssumingHelper False sBools
  
  -- | Generalization of 'Data.SBV.Control.checkSatAssumingWithUnsatisfiableSet'
  checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])
  checkSatAssumingWithUnsatisfiableSet = checkSatAssumingHelper True
  
  -- | Helper for the two variants of checkSatAssuming we have. Internal only.
  checkSatAssumingHelper :: (MonadIO m, MonadQuery m) => Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
  checkSatAssumingHelper getAssumptions sBools = do
          -- sigh.. SMT-Lib requires the values to be literals only. So, create proxies.
          let mkAssumption st = do swsOriginal <- mapM (\sb -> do sv <- sbvToSV st sb
                                                                  return (sv, sb)) sBools
  
                                   -- drop duplicates and trues
                                   let swbs = [p | p@(sv, _) <- nubBy ((==) `on` fst) swsOriginal, sv /= trueSV]
  
                                   -- get a unique proxy name for each
                                   uniqueSWBs <- mapM (\(sv, sb) -> do unique <- incrementInternalCounter st
                                                                       return (sv, (unique, sb))) swbs
  
                                   let translate (sv, (unique, sb)) = (nm, decls, (proxy, sb))
                                          where nm    = show sv
                                                proxy = "__assumption_proxy_" ++ nm ++ "_" ++ show unique
                                                decls = [ "(declare-const " ++ proxy ++ " Bool)"
                                                        , "(assert (= " ++ proxy ++ " " ++ nm ++ "))"
                                                        ]
  
                                   return $ map translate uniqueSWBs
  
          assumptions <- inNewContext mkAssumption
  
          let (origNames, declss, proxyMap) = unzip3 assumptions
  
          let cmd = "(check-sat-assuming (" ++ unwords (map fst proxyMap) ++ "))"
              bad = unexpected "checkSatAssuming" cmd "one of sat/unsat/unknown"
                             $ Just [ "Make sure you use:"
                                    , ""
                                    , "       setOption $ ProduceUnsatAssumptions True"
                                    , ""
                                    , "to tell the solver to produce unsat assumptions."
                                    ]
  
          mapM_ (send True) $ concat declss
          r <- ask cmd
  
          let grabUnsat
               | getAssumptions = do as <- getUnsatAssumptions origNames proxyMap
                                     return (Unsat, Just as)
               | True           = return (Unsat, Nothing)
  
          parse r bad $ \case ECon "sat"     -> return (Sat, Nothing)
                              ECon "unsat"   -> grabUnsat
                              ECon "unknown" -> return (Unk, Nothing)
                              _              -> bad r Nothing
  
  -- | Generalization of 'Data.SBV.Control.getAssertionStackDepth'
  getAssertionStackDepth :: (MonadIO m, MonadQuery m) => m Int
  getAssertionStackDepth = queryAssertionStackDepth <$> getQueryState
  
  -- | Upon a pop, we need to restore all arrays and tables. See: http://github.com/LeventErkok/sbv/issues/374
  restoreTablesAndArrays :: (MonadIO m, MonadQuery m) => m ()
  restoreTablesAndArrays = do st <- queryState
  
                              tCount <- M.size  <$> (io . readIORef) (rtblMap   st)
  
                              let inits = [ "table"  ++ show i ++ "_initializer" | i <- [0 .. tCount - 1]]
  
                              case inits of
                                []  -> return ()   -- Nothing to do
                                [x] -> send True $ "(assert " ++ x ++ ")"
                                xs  -> send True $ "(assert (and " ++ unwords xs ++ "))"
  
  -- | Generalization of 'Data.SBV.Control.inNewAssertionStack'
  inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a
  inNewAssertionStack q = do push 1
                             r <- q
                             pop 1
                             return r
  
  -- | Generalization of 'Data.SBV.Control.push'
  push :: (MonadIO m, MonadQuery m) => Int -> m ()
  push i
   | i <= 0 = error $ "Data.SBV: push requires a strictly positive level argument, received: " ++ show i
   | True   = do depth <- getAssertionStackDepth
                 send True $ "(push " ++ show i ++ ")"
                 modifyQueryState $ \s -> s{queryAssertionStackDepth = depth + i}
  
  -- | Generalization of 'Data.SBV.Control.pop'
  pop :: (MonadIO m, MonadQuery m) => Int -> m ()
  pop i
   | i <= 0 = error $ "Data.SBV: pop requires a strictly positive level argument, received: " ++ show i
   | True   = do depth <- getAssertionStackDepth
                 if i > depth
                    then error $ "Data.SBV: Illegally trying to pop " ++ shl i ++ ", at current level: " ++ show depth
                    else do QueryState{queryConfig} <- getQueryState
                            if not (supportsGlobalDecls (capabilities (solver queryConfig)))
                               then error $ unlines [ ""
                                                    , "*** Data.SBV: Backend solver does not support global-declarations."
                                                    , "***           Hence, calls to 'pop' are not supported."
                                                    , "***"
                                                    , "*** Request this as a feature for the underlying solver!"
                                                    ]
                               else do send True $ "(pop " ++ show i ++ ")"
                                       restoreTablesAndArrays
                                       modifyQueryState $ \s -> s{queryAssertionStackDepth = depth - i}
     where shl 1 = "one level"
           shl n = show n ++ " levels"
  
  -- | Generalization of 'Data.SBV.Control.caseSplit'
  caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
  caseSplit printCases cases = do cfg <- getConfig
                                  go cfg (cases ++ [("Coverage", sNot (sOr (map snd cases)))])
    where msg = when printCases . io . putStrLn
  
          go _ []            = return Nothing
          go cfg ((n,c):ncs) = do let notify s = msg $ "Case " ++ n ++ ": " ++ s
  
                                  notify "Starting"
                                  r <- checkSatAssuming [c]
  
                                  case r of
                                    Unsat    -> do notify "Unsatisfiable"
                                                   go cfg ncs
  
                                    Sat      -> do notify "Satisfiable"
                                                   res <- Satisfiable cfg <$> getModel
                                                   return $ Just (n, res)
  
                                    DSat mbP -> do notify $ "Delta satisfiable" ++ maybe "" (" (precision: " ++) mbP
                                                   res <- DeltaSat cfg mbP <$> getModel
                                                   return $ Just (n, res)
  
                                    Unk      -> do notify "Unknown"
                                                   res <- Unknown cfg <$> getUnknownReason
                                                   return $ Just (n, res)
  
  -- | Generalization of 'Data.SBV.Control.resetAssertions'
  resetAssertions :: (MonadIO m, MonadQuery m) => m ()
  resetAssertions = do send True "(reset-assertions)"
                       modifyQueryState $ \s -> s{ queryAssertionStackDepth = 0 }
  
                       -- Make sure we restore tables and arrays after resetAssertions: See: https://github.com/LeventErkok/sbv/issues/535
                       restoreTablesAndArrays
  
  -- | Generalization of 'Data.SBV.Control.echo'
  echo :: (MonadIO m, MonadQuery m) => String -> m ()
  echo s = do let cmd = "(echo \"" ++ concatMap sanitize s ++ "\")"
  
              -- we send the command, but otherwise ignore the response
              -- note that 'send True/False' would be incorrect here. 'send True' would
              -- require a success response. 'send False' would fail to consume the
              -- output. But 'ask' does the right thing! It gets "some" response,
              -- and forgets about it immediately.
              _ <- ask cmd
  
              return ()
    where sanitize '"'  = "\"\""  -- quotes need to be duplicated
          sanitize c    = [c]
  
  -- | Generalization of 'Data.SBV.Control.exit'
  exit :: (MonadIO m, MonadQuery m) => m ()
  exit = do send True "(exit)"
            modifyQueryState $ \s -> s{queryAssertionStackDepth = 0}
  
  -- | Generalization of 'Data.SBV.Control.getUnsatCore'
  getUnsatCore :: (MonadIO m, MonadQuery m) => m [String]
  getUnsatCore = do
          let cmd = "(get-unsat-core)"
              bad = unexpected "getUnsatCore" cmd "an unsat-core response"
                             $ Just [ "Make sure you use:"
                                    , ""
                                    , "       setOption $ ProduceUnsatCores True"
                                    , ""
                                    , "so the solver will be ready to compute unsat cores,"
                                    , "and that there is a model by first issuing a 'checkSat' call."
                                    , ""
                                    , "If using z3, you might also optionally want to set:"
                                    , ""
                                    , "       setOption $ OptionKeyword \":smt.core.minimize\" [\"true\"]"
                                    , ""
                                    , "to make sure the unsat core doesn't have irrelevant entries,"
                                    , "though this might incur a performance penalty."
  
  
                                    ]
  
          r <- ask cmd
  
          parse r bad $ \case
             EApp es | Just xs <- mapM fromECon es -> return $ map unBar xs
             _                                     -> bad r Nothing
  
  -- | Retrieve the unsat core if it was asked for in the configuration
  getUnsatCoreIfRequested :: (MonadIO m, MonadQuery m) => m (Maybe [String])
  getUnsatCoreIfRequested = do
          cfg <- getConfig
          if or [b | ProduceUnsatCores b <- solverSetOptions cfg]
             then Just <$> getUnsatCore
             else return Nothing
  
  -- | Generalization of 'Data.SBV.Control.getProof'
  getProof :: (MonadIO m, MonadQuery m) => m String
  getProof = do
          let cmd = "(get-proof)"
              bad = unexpected "getProof" cmd "a get-proof response"
                             $ Just [ "Make sure you use:"
                                    , ""
                                    , "       setOption $ ProduceProofs True"
                                    , ""
                                    , "to make sure the solver is ready for producing proofs,"
                                    , "and that there is a proof by first issuing a 'checkSat' call."
                                    ]
  
  
          r <- ask cmd
  
          -- we only care about the fact that we can parse the output, so the
          -- result of parsing is ignored.
          parse r bad $ \_ -> return r
  
  -- | Generalization of 'Data.SBV.Control.getInterpolantMathSAT'. Use this version with MathSAT.
  getInterpolantMathSAT :: (MonadIO m, MonadQuery m) => [String] -> m String
  getInterpolantMathSAT fs
    | null fs
    = error "SBV.getInterpolantMathSAT requires at least one marked constraint, received none!"
    | True
    = do let bar s = '|' : s ++ "|"
             cmd = "(get-interpolant (" ++ unwords (map bar fs) ++ "))"
             bad = unexpected "getInterpolant" cmd "a get-interpolant response"
                            $ Just [ "Make sure you use:"
                                   , ""
                                   , "       setOption $ ProduceInterpolants True"
                                   , ""
                                   , "to make sure the solver is ready for producing interpolants,"
                                   , "and that you have used the proper attributes using the"
                                   , "constrainWithAttribute function."
                                   ]
  
         r <- ask cmd
  
         parse r bad $ \e -> return $ serialize False e
  
  
  -- | Generalization of 'Data.SBV.Control.getAbduct'.
  getAbduct :: (SolverContext m, MonadIO m, MonadQuery m) => Maybe String -> String -> SBool -> m String
  getAbduct mbGrammar defName b = do
     s <- inNewContext (`sbvToSV` b)
     let cmd = "(get-abduct " ++ defName ++ " " ++ show s ++ fromMaybe "" mbGrammar ++ ")"
         bad = unexpected "getAbduct" cmd "a get-abduct response" Nothing
  
     r <- ask cmd
  
     parse r bad $ \e -> return $ serialize False e
  
  -- | Generalization of 'Data.SBV.Control.getAbductNext'.
  getAbductNext :: (MonadIO m, MonadQuery m) => m String
  getAbductNext = do
     let cmd = "(get-abduct-next)"
         bad = unexpected "getAbductNext" cmd "a get-abduct-next response" Nothing
  
     r <- ask cmd
  
     parse r bad $ \e -> return $ serialize False e
  
  -- | Generalization of 'Data.SBV.Control.getInterpolantZ3'. Use this version with Z3.
  getInterpolantZ3 :: (MonadIO m, MonadQuery m) => [SBool] -> m String
  getInterpolantZ3 fs
    | length fs < 2
    = error $ "SBV.getInterpolantZ3 requires at least two booleans, received: " ++ show fs
    | True
    = do ss <- let fAll []     sofar = return $ reverse sofar
                   fAll (b:bs) sofar = do sv <- inNewContext (`sbvToSV` b)
                                          fAll bs (sv : sofar)
               in fAll fs []
  
         let cmd = "(get-interpolant " ++ unwords (map show ss) ++ ")"
             bad = unexpected "getInterpolant" cmd "a get-interpolant response" Nothing
  
         r <- ask cmd
  
         parse r bad $ \e -> return $ serialize False e
  
  -- | Generalization of 'Data.SBV.Control.getAssertions'
  getAssertions :: (MonadIO m, MonadQuery m) => m [String]
  getAssertions = do
          let cmd = "(get-assertions)"
              bad = unexpected "getAssertions" cmd "a get-assertions response"
                             $ Just [ "Make sure you use:"
                                    , ""
                                    , "       setOption $ ProduceAssertions True"
                                    , ""
                                    , "to make sure the solver is ready for producing assertions."
                                    ]
  
              render = serialize False
  
          r <- ask cmd
  
          parse r bad $ \pe -> case pe of
                                  EApp xs -> return $ map render xs
                                  _       -> return [render pe]
  
  -- | Generalization of 'Data.SBV.Control.getAssignment'
  getAssignment :: (MonadIO m, MonadQuery m) => m [(String, Bool)]
  getAssignment = do
          let cmd = "(get-assignment)"
              bad = unexpected "getAssignment" cmd "a get-assignment response"
                             $ Just [ "Make sure you use:"
                                    , ""
                                    , "       setOption $ ProduceAssignments True"
                                    , ""
                                    , "to make sure the solver is ready for producing assignments,"
                                    , "and that there is a model by first issuing a 'checkSat' call."
                                    ]
  
              -- we're expecting boolean assignment to labels, essentially
              grab (EApp [ECon s, ENum (0, _, _)]) = Just (unQuote s, False)
              grab (EApp [ECon s, ENum (1, _, _)]) = Just (unQuote s, True)
              grab _                               = Nothing
  
          r <- ask cmd
  
          parse r bad $ \case EApp ps | Just vs <- mapM grab ps -> return vs
                              _                                 -> bad r Nothing
  
  -- | Make an assignment. The type 'Assignment' is abstract, the result is typically passed
  -- to 'mkSMTResult':
  --
  -- @ mkSMTResult [ a |-> 332
  --             , b |-> 2.3
  --             , c |-> True
  --             ]
  -- @
  --
  -- End users should use 'getModel' for automatically constructing models from the current solver state.
  -- However, an explicit 'Assignment' might be handy in complex scenarios where a model needs to be
  -- created manually.
  infix 1 |->
  (|->) :: SymVal a => SBV a -> a -> Assignment
  SBV a |-> v = case literal v of
                  SBV (SVal _ (Left cv)) -> Assign a cv
                  r                      -> error $ "Data.SBV: Impossible happened in |->: Cannot construct a CV with literal: " ++ show r
  
  -- | Generalization of 'Data.SBV.Control.mkSMTResult'
  -- NB. This function does not allow users to create interpretations for UI-Funs. But that's
  -- probably not a good idea anyhow. Also, if you use the 'validateModel' or 'optimizeValidateConstraints' features, SBV will
  -- fail on models returned via this function.
  mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult
  mkSMTResult asgns = do
               QueryState{queryConfig} <- getQueryState
               inps <- F.toList <$> getTopLevelInputs
  
               let grabValues st = do let extract (Assign s n) = sbvToSV st (SBV s) >>= \sv -> return (sv, n)
  
                                      modelAssignment <- mapM extract asgns
  
                                      -- sanity checks
                                      --     - All existentials should be given a value
                                      --     - No duplicates
                                      --     - No bindings to vars that are not inputs
                                      let userSS = map fst modelAssignment
  
                                          missing, extra, dup :: [String]
                                          missing = [T.unpack n | NamedSymVar s n <- inps, s `notElem` userSS]
                                          extra   = [show s | s <- userSS, s `notElem` map getSV inps]
                                          dup     = let walk []     = []
                                                        walk (n:ns)
                                                          | n `elem` ns = show n : walk (filter (/= n) ns)
                                                          | True        = walk ns
                                                    in walk userSS
  
                                      unless (null (missing ++ extra ++ dup)) $ do
  
                                            let misTag = "***   Missing inputs"
                                                dupTag = "***   Duplicate bindings"
                                                extTag = "***   Extra bindings"
  
                                                maxLen = maximum $  0
                                                                  : [length misTag | not (null missing)]
                                                                 ++ [length extTag | not (null extra)]
                                                                 ++ [length dupTag | not (null dup)]
  
                                                align s = s ++ replicate (maxLen - length s) ' ' ++ ": "
  
                                            error $ unlines $ [""
                                                              , "*** Data.SBV: Query model construction has a faulty assignment."
                                                              , "***"
                                                              ]
                                                           ++ [ align misTag ++ intercalate ", "  missing | not (null missing)]
                                                           ++ [ align extTag ++ intercalate ", "  extra   | not (null extra)  ]
                                                           ++ [ align dupTag ++ intercalate ", "  dup     | not (null dup)    ]
                                                           ++ [ "***"
                                                              , "*** Data.SBV: Check your query result construction!"
                                                              ]
  
                                      let findName s = case [T.unpack nm | NamedSymVar i nm <- inps, s == i] of
                                                          [nm] -> nm
                                                          []   -> error "*** Data.SBV: Impossible happened: Cannot find " ++ show s ++ " in the input list"
                                                          nms  -> error $ unlines [ ""
                                                                                  , "*** Data.SBV: Impossible happened: Multiple matches for: " ++ show s
                                                                                  , "***   Candidates: " ++ unwords nms
                                                                                  ]
  
                                      return [(findName s, n) | (s, n) <- modelAssignment]
  
               assocs <- inNewContext grabValues
  
               let m = SMTModel { modelObjectives = []
                                , modelBindings   = Nothing
                                , modelAssocs     = assocs
                                , modelUIFuns     = []
                                }
  
               return $ Satisfiable queryConfig m
  
  {- HLint ignore getModelAtIndex "Use forM_" -}
  