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

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

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

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

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

import Data.IORef (readIORef)

import qualified Data.Map.Strict    as M
import qualified Data.IntMap.Strict as IM
import qualified Data.Sequence      as S
import qualified Data.Text          as T
import qualified Data.Foldable      as F


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

import Data.SBV.Core.Data

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

import Data.SBV.Utils.SExpr

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

import Data.SBV.Utils.PrettyNum (showNegativeNumber)

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

-- Remove one pair of surrounding 'c's, if present
noSurrounding :: Char -> String -> String
noSurrounding c (c':cs@(_:_)) | c == c' && c == last cs  = init cs
noSurrounding _ s                                        = s

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

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

-- 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.getInfo'
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 value of the logic!"
                 -- 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, _)) _ = return $ Just $ c False
        bool c (ENum (1, _)) _ = 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   = S.fromList (sortOn fst obsvs) <> fmap removeSV (prepare inputAssocs)

          -- 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, (_, t)) -> (\a -> (nm, (t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns

          uiVals    <- mapM (\ui@(nm, (_, _)) -> (nm,) <$> getUICVal mbi ui) uiRegs

          return 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

                        inputs <- F.toList <$> getTopLevelInputs

                        parse r bad $ \case EApp (ECon "objectives" : es) -> catMaybes <$> mapM (getObjValue (bad r) inputs) es
                                            _                             -> bad r Nothing

  where -- | Parse an objective value out.
        getObjValue :: (forall a. Maybe [String] -> m a) -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
        getObjValue 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 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)
                            aCount <- IM.size <$> (io . readIORef) (rArrayMap st)

                            let tInits = [ "table"  ++ show i ++ "_initializer" | i <- [0 .. tCount - 1]]
                                aInits = [ "array_" ++ show i ++ "_initializer" | i <- [0 .. aCount - 1]]
                                inits  = tInits ++ aInits

                            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_" -}