    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.SBV.SMT.SMT
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- Abstraction of SMT solvers
    -----------------------------------------------------------------------------

    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE DefaultSignatures   #-}

    module Data.SBV.SMT.SMT where

    import qualified Control.Exception as C

    import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO)
    import Control.DeepSeq    (NFData(..))
    import Control.Monad      (when, zipWithM)
    import Data.Char          (isSpace)
    import Data.Int           (Int8, Int16, Int32, Int64)
    import Data.Function      (on)
    import Data.List          (intercalate, isPrefixOf, isInfixOf, sortBy)
    import Data.Word          (Word8, Word16, Word32, Word64)
    import System.Directory   (findExecutable)
    import System.Environment (getEnv)
    import System.Exit        (ExitCode(..))
    import System.IO          (hClose, hFlush, hPutStr, hGetContents, hGetLine)
    import System.Process     (runInteractiveProcess, waitForProcess, terminateProcess)

    import qualified Data.Map as M

    import Data.SBV.BitVectors.AlgReals
    import Data.SBV.BitVectors.Data
    import Data.SBV.BitVectors.PrettyNum
    import Data.SBV.BitVectors.Symbolic   (SMTEngine)
    import Data.SBV.SMT.SMTLib            (interpretSolverOutput, interpretSolverModelLine)
    import Data.SBV.Utils.Lib             (joinArgs, splitArgs)
    import Data.SBV.Utils.TDiff

    -- | Extract the final configuration from a result
    resultConfig :: SMTResult -> SMTConfig
    resultConfig (Unsatisfiable c) = c
    resultConfig (Satisfiable c _) = c
    resultConfig (Unknown c _)     = c
    resultConfig (ProofError c _)  = c
    resultConfig (TimeOut c)       = c

    -- | A 'prove' call results in a 'ThmResult'
    newtype ThmResult    = ThmResult    SMTResult

    -- | A 'sat' call results in a 'SatResult'
    -- The reason for having a separate 'SatResult' is to have a more meaningful 'Show' instance.
    newtype SatResult    = SatResult    SMTResult

    -- | A 'safe' call results in a 'SafeResult'
    newtype SafeResult   = SafeResult   (Maybe String, String, SMTResult)

    -- | An 'allSat' call results in a 'AllSatResult'. The boolean says whether
    -- we should warn the user about prefix-existentials.
    newtype AllSatResult = AllSatResult (Bool, [SMTResult])

    -- | User friendly way of printing theorem results
    instance Show ThmResult where
      show (ThmResult r) = showSMTResult "Q.E.D."
                                         "Unknown"     "Unknown. Potential counter-example:\n"
                                         "Falsifiable" "Falsifiable. Counter-example:\n" r

    -- | User friendly way of printing satisfiablity results
    instance Show SatResult where
      show (SatResult r) = showSMTResult "Unsatisfiable"
                                         "Unknown"     "Unknown. Potential model:\n"
                                         "Satisfiable" "Satisfiable. Model:\n" r

    -- | User friendly way of printing safety results
    instance Show SafeResult where
       show (SafeResult (mbLoc, msg, r)) = showSMTResult (tag "No violations detected")
                                                         (tag "Unknown")  (tag "Unknown. Potential violating model:\n")
                                                         (tag "Violated") (tag "Violated. Model:\n") r
            where loc   = maybe "" (++ ": ") mbLoc
                  tag s = loc ++ msg ++ ": " ++ s

    -- | The Show instance of AllSatResults. Note that we have to be careful in being lazy enough
    -- as the typical use case is to pull results out as they become available.
    instance Show AllSatResult where
      show (AllSatResult (e, xs)) = go (0::Int) xs
        where uniqueWarn | e    = " (Unique up to prefix existentials.)"
                         | True = ""
              go c (s:ss) = let c'      = c+1
                                (ok, o) = sh c' s
                            in c' `seq` if ok then o ++ "\n" ++ go c' ss else o
              go c []     = case c of
                              0 -> "No solutions found."
                              1 -> "This is the only solution." ++ uniqueWarn
                              _ -> "Found " ++ show c ++ " different solutions." ++ uniqueWarn
              sh i c = (ok, showSMTResult "Unsatisfiable"
                                          "Unknown" "Unknown. Potential model:\n"
                                          ("Solution #" ++ show i ++ ":\nSatisfiable") ("Solution #" ++ show i ++ ":\n") c)
                  where ok = case c of
                               Satisfiable{} -> True
                               _             -> False

    -- | Instances of 'SatModel' can be automatically extracted from models returned by the
    -- solvers. The idea is that the sbv infrastructure provides a stream of 'CW''s (constant-words)
    -- coming from the solver, and the type @a@ is interpreted based on these constants. Many typical
    -- instances are already provided, so new instances can be declared with relative ease.
    --
    -- Minimum complete definition: 'parseCWs'
    class SatModel a where
      -- | Given a sequence of constant-words, extract one instance of the type @a@, returning
      -- the remaining elements untouched. If the next element is not what's expected for this
      -- type you should return 'Nothing'
      parseCWs  :: [CW] -> Maybe (a, [CW])
      -- | Given a parsed model instance, transform it using @f@, and return the result.
      -- The default definition for this method should be sufficient in most use cases.
      cvtModel  :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW])
      cvtModel f x = x >>= \(a, r) -> f a >>= \b -> return (b, r)

      default parseCWs :: Read a => [CW] -> Maybe (a, [CW])
      parseCWs (CW _ (CWUserSort (_, s)) : r) = Just (read s, r)
      parseCWs _                              = Nothing

    -- | Parse a signed/sized value from a sequence of CWs
    genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
    genParse k (x@(CW _ (CWInteger i)):r) | kindOf x == k = Just (fromIntegral i, r)
    genParse _ _                                          = Nothing

    -- | Base case for 'SatModel' at unit type. Comes in handy if there are no real variables.
    instance SatModel () where
      parseCWs xs = return ((), xs)

    -- | 'Bool' as extracted from a model
    instance SatModel Bool where
      parseCWs xs = do (x, r) <- genParse KBool xs
                       return ((x :: Integer) /= 0, r)

    -- | 'Word8' as extracted from a model
    instance SatModel Word8 where
      parseCWs = genParse (KBounded False 8)

    -- | 'Int8' as extracted from a model
    instance SatModel Int8 where
      parseCWs = genParse (KBounded True 8)

    -- | 'Word16' as extracted from a model
    instance SatModel Word16 where
      parseCWs = genParse (KBounded False 16)

    -- | 'Int16' as extracted from a model
    instance SatModel Int16 where
      parseCWs = genParse (KBounded True 16)

    -- | 'Word32' as extracted from a model
    instance SatModel Word32 where
      parseCWs = genParse (KBounded False 32)

    -- | 'Int32' as extracted from a model
    instance SatModel Int32 where
      parseCWs = genParse (KBounded True 32)

    -- | 'Word64' as extracted from a model
    instance SatModel Word64 where
      parseCWs = genParse (KBounded False 64)

    -- | 'Int64' as extracted from a model
    instance SatModel Int64 where
      parseCWs = genParse (KBounded True 64)

    -- | 'Integer' as extracted from a model
    instance SatModel Integer where
      parseCWs = genParse KUnbounded

    -- | 'AlgReal' as extracted from a model
    instance SatModel AlgReal where
      parseCWs (CW KReal (CWAlgReal i) : r) = Just (i, r)
      parseCWs _                            = Nothing

    -- | 'Float' as extracted from a model
    instance SatModel Float where
      parseCWs (CW KFloat (CWFloat i) : r) = Just (i, r)
      parseCWs _                           = Nothing

    -- | 'Double' as extracted from a model
    instance SatModel Double where
      parseCWs (CW KDouble (CWDouble i) : r) = Just (i, r)
      parseCWs _                             = Nothing

    -- | 'CW' as extracted from a model; trivial definition
    instance SatModel CW where
      parseCWs (cw : r) = Just (cw, r)
      parseCWs []       = Nothing

    -- | A rounding mode, extracted from a model. (Default definition suffices)
    instance SatModel RoundingMode

    -- | A list of values as extracted from a model. When reading a list, we
    -- go as long as we can (maximal-munch). Note that this never fails, as
    -- we can always return the empty list!
    instance SatModel a => SatModel [a] where
      parseCWs [] = Just ([], [])
      parseCWs xs = case parseCWs xs of
                      Just (a, ys) -> case parseCWs ys of
                                        Just (as, zs) -> Just (a:as, zs)
                                        Nothing       -> Just ([], ys)
                      Nothing     -> Just ([], xs)

    -- | Tuples extracted from a model
    instance (SatModel a, SatModel b) => SatModel (a, b) where
      parseCWs as = do (a, bs) <- parseCWs as
                       (b, cs) <- parseCWs bs
                       return ((a, b), cs)

    -- | 3-Tuples extracted from a model
    instance (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) where
      parseCWs as = do (a,      bs) <- parseCWs as
                       ((b, c), ds) <- parseCWs bs
                       return ((a, b, c), ds)

    -- | 4-Tuples extracted from a model
    instance (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) where
      parseCWs as = do (a,         bs) <- parseCWs as
                       ((b, c, d), es) <- parseCWs bs
                       return ((a, b, c, d), es)

    -- | 5-Tuples extracted from a model
    instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) where
      parseCWs as = do (a, bs)            <- parseCWs as
                       ((b, c, d, e), fs) <- parseCWs bs
                       return ((a, b, c, d, e), fs)

    -- | 6-Tuples extracted from a model
    instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) where
      parseCWs as = do (a, bs)               <- parseCWs as
                       ((b, c, d, e, f), gs) <- parseCWs bs
                       return ((a, b, c, d, e, f), gs)

    -- | 7-Tuples extracted from a model
    instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) where
      parseCWs as = do (a, bs)                  <- parseCWs as
                       ((b, c, d, e, f, g), hs) <- parseCWs bs
                       return ((a, b, c, d, e, f, g), hs)

    -- | Various SMT results that we can extract models out of.
    class Modelable a where
      -- | Is there a model?
      modelExists :: a -> Bool
      -- | Extract a model, the result is a tuple where the first argument (if True)
      -- indicates whether the model was "probable". (i.e., if the solver returned unknown.)
      getModel :: SatModel b => a -> Either String (Bool, b)
      -- | Extract a model dictionary. Extract a dictionary mapping the variables to
      -- their respective values as returned by the SMT solver. Also see `getModelDictionaries`.
      getModelDictionary :: a -> M.Map String CW
      -- | Extract a model value for a given element. Also see `getModelValues`.
      getModelValue :: SymWord b => String -> a -> Maybe b
      getModelValue v r = fromCW `fmap` (v `M.lookup` getModelDictionary r)
      -- | Extract a representative name for the model value of an uninterpreted kind.
      -- This is supposed to correspond to the value as computed internally by the
      -- SMT solver; and is unportable from solver to solver. Also see `getModelUninterpretedValues`.
      getModelUninterpretedValue :: String -> a -> Maybe String
      getModelUninterpretedValue v r = case v `M.lookup` getModelDictionary r of
                                         Just (CW _ (CWUserSort (_, s))) -> Just s
                                         _                               -> Nothing

      -- | A simpler variant of 'getModel' to get a model out without the fuss.
      extractModel :: SatModel b => a -> Maybe b
      extractModel a = case getModel a of
                         Right (_, b) -> Just b
                         _            -> Nothing

    -- | Return all the models from an 'allSat' call, similar to 'extractModel' but
    -- is suitable for the case of multiple results.
    extractModels :: SatModel a => AllSatResult -> [a]
    extractModels (AllSatResult (_, xs)) = [ms | Right (_, ms) <- map getModel xs]

    -- | Get dictionaries from an all-sat call. Similar to `getModelDictionary`.
    getModelDictionaries :: AllSatResult -> [M.Map String CW]
    getModelDictionaries (AllSatResult (_, xs)) = map getModelDictionary xs

    -- | Extract value of a variable from an all-sat call. Similar to `getModelValue`.
    getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b]
    getModelValues s (AllSatResult (_, xs)) =  map (s `getModelValue`) xs

    -- | Extract value of an uninterpreted variable from an all-sat call. Similar to `getModelUninterpretedValue`.
    getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
    getModelUninterpretedValues s (AllSatResult (_, xs)) =  map (s `getModelUninterpretedValue`) xs

    -- | 'ThmResult' as a generic model provider
    instance Modelable ThmResult where
      getModel           (ThmResult r) = getModel r
      modelExists        (ThmResult r) = modelExists r
      getModelDictionary (ThmResult r) = getModelDictionary r

    -- | 'SatResult' as a generic model provider
    instance Modelable SatResult where
      getModel           (SatResult r) = getModel r
      modelExists        (SatResult r) = modelExists r
      getModelDictionary (SatResult r) = getModelDictionary r

    -- | 'SMTResult' as a generic model provider
    instance Modelable SMTResult where
      getModel (Unsatisfiable _) = Left "SBV.getModel: Unsatisfiable result"
      getModel (Unknown _ m)     = Right (True, parseModelOut m)
      getModel (ProofError _ s)  = error $ unlines $ "Backend solver complains: " : s
      getModel (TimeOut _)       = Left "Timeout"
      getModel (Satisfiable _ m) = Right (False, parseModelOut m)
      modelExists Satisfiable{}   = True
      modelExists Unknown{}       = False -- don't risk it
      modelExists _               = False
      getModelDictionary (Unsatisfiable _) = M.empty
      getModelDictionary (Unknown _ m)     = M.fromList (modelAssocs m)
      getModelDictionary (ProofError _ _)  = M.empty
      getModelDictionary (TimeOut _)       = M.empty
      getModelDictionary (Satisfiable _ m) = M.fromList (modelAssocs m)

    -- | Extract a model out, will throw error if parsing is unsuccessful
    parseModelOut :: SatModel a => SMTModel -> a
    parseModelOut m = case parseCWs [c | (_, c) <- modelAssocs m] of
                       Just (x, []) -> x
                       Just (_, ys) -> error $ "SBV.getModel: Partially constructed model; remaining elements: " ++ show ys
                       Nothing      -> error $ "SBV.getModel: Cannot construct a model from: " ++ show m

    -- | Given an 'allSat' call, we typically want to iterate over it and print the results in sequence. The
    -- 'displayModels' function automates this task by calling 'disp' on each result, consecutively. The first
    -- 'Int' argument to 'disp' 'is the current model number. The second argument is a tuple, where the first
    -- element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown)
    displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
    displayModels disp (AllSatResult (_, ms)) = do
        inds <- zipWithM display [a | Right a <- map (getModel . SatResult) ms] [(1::Int)..]
        return $ last (0:inds)
      where display r i = disp i r >> return i

    -- | Show an SMTResult; generic version
    showSMTResult :: String -> String -> String -> String -> String -> SMTResult -> String
    showSMTResult unsatMsg unkMsg unkMsgModel satMsg satMsgModel result = case result of
      Unsatisfiable _             -> unsatMsg
      Satisfiable _ (SMTModel []) -> satMsg
      Satisfiable _ m             -> satMsgModel ++ showModel cfg m
      Unknown     _ (SMTModel []) -> unkMsg
      Unknown     _ m             -> unkMsgModel ++ showModel cfg m
      ProofError  _ []            -> "*** An error occurred. No additional information available. Try running in verbose mode"
      ProofError  _ ls            -> "*** An error occurred.\n" ++ intercalate "\n" (map ("***  " ++) ls)
      TimeOut     _               -> "*** Timeout"
     where cfg = resultConfig result

    -- | Show a model in human readable form. Ignore bindings to those variables that start
    -- with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes
    showModel :: SMTConfig -> SMTModel -> String
    showModel cfg model
       | null allVars
       = "[There are no variables bound by the model.]"
       | null relevantVars
       = "[There are no model-variables bound by the model.]"
       | True
       = intercalate "\n" . display . map shM $ relevantVars
      where allVars       = modelAssocs model
            relevantVars  = filter (not . ignore) allVars
            ignore (s, _) = "__internal_sbv_" `isPrefixOf` s || isNonModelVar cfg s
            shM (s, v)    = let vs = shCW cfg v in ((length s, s), (vlength vs, vs))
            display svs   = map line svs
               where line ((_, s), (_, v)) = "  " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - lTrimRight (valPart v)) v
                     nameWidth             = maximum $ 0 : [l | ((l, _), _) <- svs]
                     valWidth              = maximum $ 0 : [l | (_, (l, _)) <- svs]
            right p s = s ++ replicate p ' '
            left  p s = replicate p ' ' ++ s
            vlength s = case dropWhile (/= ':') (reverse (takeWhile (/= '\n') s)) of
                          (':':':':r) -> length (dropWhile isSpace r)
                          _           -> length s -- conservative
            valPart ""          = ""
            valPart (':':':':_) = ""
            valPart (x:xs)      = x : valPart xs
            lTrimRight = length . dropWhile isSpace . reverse

    -- | Show a constant value, in the user-specified base
    shCW :: SMTConfig -> CW -> String
    shCW = sh . printBase
      where sh 2  = binS
            sh 10 = show
            sh 16 = hexS
            sh n  = \w -> show w ++ " -- Ignoring unsupported printBase " ++ show n ++ ", use 2, 10, or 16."

    -- | Print uninterpreted function values from models. Very, very crude..
    shUI :: (String, [String]) -> [String]
    shUI (flong, cases) = ("  -- uninterpreted: " ++ f) : map shC cases
      where tf = dropWhile (/= '_') flong
            f  =  if null tf then flong else tail tf
            shC s = "       " ++ s

    -- | Print uninterpreted array values from models. Very, very crude..
    shUA :: (String, [String]) -> [String]
    shUA (f, cases) = ("  -- array: " ++ f) : map shC cases
      where shC s = "       " ++ s

    -- | Helper function to spin off to an SMT solver.
    pipeProcess :: SMTConfig -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])
    pipeProcess cfg execName opts script cleanErrs = do
            let nm = show (name (solver cfg))
            mbExecPath <- findExecutable execName
            case mbExecPath of
              Nothing       -> return $ Left $ "Unable to locate executable for " ++ nm
                                            ++ "\nExecutable specified: " ++ show execName
              Just execPath ->
                       do solverResult <- dispatchSolver cfg execPath opts script
                          case solverResult of
                            Left s                          -> return $ Left s
                            Right (ec, contents, allErrors) ->
                              let errors = dropWhile isSpace (cleanErrs allErrors)
                              in case (null errors, ec) of
                                    (True, ExitSuccess)  -> return $ Right $ map clean (filter (not . null) (lines contents))
                                    (_, ec')             -> let errors' = if null errors
                                                                          then (if null (dropWhile isSpace contents)
                                                                                then "(No error message printed on stderr by the executable.)"
                                                                                else contents)
                                                                          else errors
                                                                finalEC = case (ec', ec) of
                                                                            (ExitFailure n, _) -> n
                                                                            (_, ExitFailure n) -> n
                                                                            _                  -> 0 -- can happen if ExitSuccess but there is output on stderr
                                                            in return $ Left $  "Failed to complete the call to " ++ nm
                                                                             ++ "\nExecutable   : " ++ show execPath
                                                                             ++ "\nOptions      : " ++ joinArgs opts
                                                                             ++ "\nExit code    : " ++ show finalEC
                                                                             ++ "\nSolver output: "
                                                                             ++ "\n" ++ line ++ "\n"
                                                                             ++ intercalate "\n" (filter (not . null) (lines errors'))
                                                                             ++ "\n" ++ line
                                                                             ++ "\nGiving up.."
      where clean = reverse . dropWhile isSpace . reverse . dropWhile isSpace
            line  = replicate 78 '='

    -- | The standard-model that most SMT solvers should happily work with
    standardModel :: (Bool -> [(Quantifier, NamedSymVar)] -> [String] -> SMTModel, SW -> String -> [String])
    standardModel = (standardModelExtractor, standardValueExtractor)

    -- | Some solvers (Z3) require multiple calls for certain value extractions; as in multi-precision reals. Deal with that here
    standardValueExtractor :: SW -> String -> [String]
    standardValueExtractor _ l = [l]

    -- | A standard post-processor: Reading the lines of solver output and turning it into a model:
    standardModelExtractor :: Bool -> [(Quantifier, NamedSymVar)] -> [String] -> SMTModel
    standardModelExtractor isSat qinps solverLines = SMTModel { modelAssocs = map snd $ sortByNodeId $ concatMap (interpretSolverModelLine inps) solverLines }
             where sortByNodeId :: [(Int, a)] -> [(Int, a)]
                   sortByNodeId = sortBy (compare `on` fst)
                   inps -- for "sat", display the prefix existentials. For completeness, we will drop
                        -- only the trailing foralls. Exception: Don't drop anything if it's all a sequence of foralls
                        | isSat = map snd $ if all (== ALL) (map fst qinps)
                                            then qinps
                                            else reverse $ dropWhile ((== ALL) . fst) $ reverse qinps
                        -- for "proof", just display the prefix universals
                        | True  = map snd $ takeWhile ((== ALL) . fst) qinps

    -- | A standard engine interface. Most solvers follow-suit here in how we "chat" to them..
    standardEngine :: String
                   -> String
                   -> ([String] -> Int -> [String])
                   -> (Bool -> [(Quantifier, NamedSymVar)] -> [String] -> SMTModel, SW -> String -> [String])
                   -> SMTEngine
    standardEngine envName envOptName addTimeOut (extractMap, extractValue) cfg isSat qinps skolemMap pgm = do
        execName <-                    getEnv envName     `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))
        execOpts <- (splitArgs `fmap`  getEnv envOptName) `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))
        let cfg'    = cfg {solver = (solver cfg) {executable = execName, options = maybe execOpts (addTimeOut execOpts) (timeOut cfg)}}
            tweaks  = case solverTweaks cfg' of
                        [] -> ""
                        ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]
            cont rm = intercalate "\n" $ concatMap extract skolemMap
               where extract (Left s)        = extractValue s $ "(echo \"((" ++ show s ++ " " ++ mkSkolemZero rm (kindOf s) ++ "))\")"
                     extract (Right (s, [])) = extractValue s $ "(get-value (" ++ show s ++ "))"
                     extract (Right (s, ss)) = extractValue s $ "(get-value (" ++ show s ++ concat [' ' : mkSkolemZero rm (kindOf a) | a <- ss] ++ "))"
            script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont (roundingMode cfg))}
        standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps))

    -- | A standard solver interface. If the solver is SMT-Lib compliant, then this function should suffice in
    -- communicating with it.
    standardSolver :: SMTConfig -> SMTScript -> (String -> String) -> ([String] -> a) -> ([String] -> a) -> IO a
    standardSolver config script cleanErrs failure success = do
        let msg      = when (verbose config) . putStrLn . ("** " ++)
            smtSolver= solver config
            exec     = executable smtSolver
            opts     = options smtSolver
            isTiming = timing config
            nmSolver = show (name smtSolver)
        msg $ "Calling: " ++ show (unwords (exec:[joinArgs opts]))
        case smtFile config of
          Nothing -> return ()
          Just f  -> do msg $ "Saving the generated script in file: " ++ show f
                        writeFile f (scriptBody script)
        contents <- timeIf isTiming nmSolver $ pipeProcess config  exec opts script cleanErrs
        msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents
        case contents of
          Left e   -> return $ failure (lines e)
          Right xs -> return $ success (mergeSExpr xs)

    -- | Wrap the solver call to protect against any exceptions
    dispatchSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (Either String (ExitCode, String, String))
    dispatchSolver cfg execPath opts script = rnf script `seq` (Right `fmap` runSolver cfg execPath opts script) `C.catch` (\(e::C.SomeException) -> bad (show e))
      where bad s = return $ Left $ unlines [ "Failed to start the external solver: " ++ s
                                            , "Make sure you can start " ++ show execPath
                                            , "from the command line without issues."
                                            ]

    -- | A variant of 'readProcessWithExitCode'; except it knows about continuation strings
    -- and can speak SMT-Lib2 (just a little).
    runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String)
    runSolver cfg execPath opts script
     = do (send, ask, cleanUp, pid) <- do
                    (inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing
                    let send l    = hPutStr inh (l ++ "\n") >> hFlush inh
                        recv      = hGetLine outh
                        ask l     = send l >> recv
                        cleanUp response
                            = do hClose inh
                                 outMVar <- newEmptyMVar
                                 out <- hGetContents outh
                                 _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()
                                 err <- hGetContents errh
                                 _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()
                                 takeMVar outMVar
                                 takeMVar outMVar
                                 hClose outh
                                 hClose errh
                                 ex <- waitForProcess pid
                                 return $ case response of
                                            Nothing        -> (ex, out, err)
                                            Just (r, vals) -> -- if the status is unknown, prepare for the possibility of not having a model
                                                              -- TBD: This is rather crude and potentially Z3 specific
                                                              let finalOut = intercalate "\n" (r : vals)
                                                                  notAvail = "model is not available" `isInfixOf` (finalOut ++ out ++ err)
                                                              in if "unknown" `isPrefixOf` r && notAvail
                                                                 then (ExitSuccess, "unknown"              , "")
                                                                 else (ex,          finalOut ++ "\n" ++ out, err)
                    return (send, ask, cleanUp, pid)
          let executeSolver = do mapM_ send (lines (scriptBody script))
                                 response <- case scriptModel script of
                                               Nothing -> do send $ satCmd cfg
                                                             return Nothing
                                               Just ls -> do r <- ask $ satCmd cfg
                                                             vals <- if any (`isPrefixOf` r) ["sat", "unknown"]
                                                                     then do let mls = lines ls
                                                                             when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:"
                                                                                                     mapM_ putStrLn mls
                                                                             mapM ask mls
                                                                     else return []
                                                             return $ Just (r, vals)
                                 cleanUp response
          executeSolver `C.onException`  (terminateProcess pid >> waitForProcess pid)

    -- | In case the SMT-Lib solver returns a response over multiple lines, compress them so we have
    -- each S-Expression spanning only a single line. We'll ignore things like parentheses inside quotes
    -- etc., as it should not be an issue
    mergeSExpr :: [String] -> [String]
    mergeSExpr []       = []
    mergeSExpr (x:xs)
     | d == 0 = x : mergeSExpr xs
     | True   = let (f, r) = grab d xs in unwords (x:f) : mergeSExpr r
     where d = parenDiff x
           parenDiff :: String -> Int
           parenDiff = go 0
             where go i ""       = i
                   go i ('(':cs) = let i'= i+1 in i' `seq` go i' cs
                   go i (')':cs) = let i'= i-1 in i' `seq` go i' cs
                   go i (_  :cs) = go i cs
           grab i ls
             | i <= 0    = ([], ls)
           grab _ []     = ([], [])
           grab i (l:ls) = let (a, b) = grab (i+parenDiff l) ls in (l:a, b)