{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SMT.SMTLIB2Solver
-- Copyright   :  (c) Masahiro Sakai 2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  portable
--
-----------------------------------------------------------------------------
module ToySolver.SMT.SMTLIB2Solver
  ( module Smtlib.Syntax.Syntax
  , ShowSL (..)

  -- * The solver type
  , Solver
  , newSolver

  -- * High-level API
  , execCommand
  , execCommandString
  , runCommand
  , runCommandString
  , printResponse

  -- * Individual commands

  -- ** (Re)starting and terminating
  , reset
  , setLogic
  , setOption
  , exit

  -- ** Modifying the assertion stack
  , push
  , pop
  , resetAssertions

  -- ** Introducing new symbols
  , declareSort
  , defineSort
  , declareConst
  , declareFun
  , defineFun
  , defineFunRec
  , defineFunsRec

  -- ** Asserting and inspecting formulas
  , assert
  , getAssertions

  -- ** Checking for satisfiability
  , checkSat
  , checkSatAssuming

  -- ** Inspecting models
  , getValue
  , getAssignment
  , getModel

  -- ** Inspecting proofs
  , getProof
  , getUnsatCore
  , getUnsatAssumptions

  -- ** Inspecting settings
  , getInfo
  , getOption

  -- ** Script information
  , setInfo
  , echo
  ) where

import Control.Applicative
import qualified Control.Exception as E
import Control.Monad
import Data.Interned (unintern)
import Data.Interned.Text
import Data.IORef
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (catMaybes)
import Data.Ratio
import Data.String
import qualified Data.Text as T
import qualified Data.Version as V
import Numeric (readDec, readFloat, readHex)
import System.Exit
import System.IO
import qualified Text.Parsec as Parsec

import qualified ToySolver.BitVector as BV
import qualified ToySolver.SMT as SMT
import ToySolver.Version
import Smtlib.Syntax.Syntax
import Smtlib.Syntax.ShowSL
import qualified Smtlib.Parsers.CommandsParsers as CommandsParsers

-- ----------------------------------------------------------------------

data Mode
  = ModeStart
  | ModeAssert
  | ModeSat
  | ModeUnsat
  deriving (Eq, Ord, Show)

type EEnv = Map String EEntry
type SortEnv = Map String SortEntry
type Env = (EEnv, SortEnv)

data EEntry
  = EFSymBuiltin InternedText
  | EFSymDeclared SMT.FSym [SMT.Sort] SMT.Sort
  | EExpr SMT.Expr Bool
  | EFunDef EEnv [(String, SMT.Sort)] SMT.Sort Term

data SortEntry
  = SortSym SMT.SSym
  | SortExpr SMT.Sort
  | SortDef SortEnv [String] Sort

interpretSort :: SortEnv -> Sort -> SMT.Sort
interpretSort env s =
  case s of
    SortId ident -> f ident []
    SortIdentifiers ident args -> f ident args
  where
    f ident@(I_Symbol "BitVec" indexes) args
      | not (null args) = E.throw $ SMT.Error (showSL ident ++ ": wrong number of arguments (" ++ show (length args) ++ " for 0)")
      | [IndexNumeral n] <- indexes = SMT.sBitVec n
      | otherwise = E.throw $ SMT.Error ("BitVec: wrong number of indexes (" ++ show (length indexes) ++ " for 1)")
    f ident@(I_Symbol _ _) _ =
      E.throw $ SMT.Error ("unknown sort: " ++ showSL ident)
    f ident@(ISymbol name) args =
      case Map.lookup name env of
        Nothing -> E.throw $ SMT.Error ("unknown sort: " ++ showSL ident)
        Just (SortSym ssym)
          | SMT.ssymArity ssym == length args -> SMT.Sort ssym args'
          | otherwise -> E.throw $ SMT.Error (showSL ident ++ ": wrong number of arguments (" ++ show (length args) ++ " for " ++ show (SMT.ssymArity ssym) ++ ")")
        Just (SortExpr s')
          | null args -> s'
          | otherwise -> E.throw $ SMT.Error (showSL ident ++ ": wrong number of arguments (" ++ show (length args) ++ " for 0)")
        Just (SortDef env' params body) ->
          interpretSort (Map.fromList (zip params (map SortExpr args')) `Map.union` env') body
      where
        args' = map (interpretSort env) args

interpretFun :: Env -> Term -> SMT.Expr
interpretFun (env,senv) t =
  case t of
    TermSpecConstant (SpecConstantNumeral n) -> SMT.EValue $ SMT.ValRational $ fromInteger n
    TermSpecConstant (SpecConstantDecimal s) -> SMT.EValue $ SMT.ValRational $ fst $ head $ readFloat s
    TermSpecConstant (SpecConstantHexadecimal s) -> 
      let n = fst $ head $ readHex s
      in SMT.EValue $ SMT.ValBitVec $ BV.nat2bv (length s * 4) n
    TermSpecConstant (SpecConstantBinary s) -> 
      SMT.EValue $ SMT.ValBitVec $ BV.fromDescBits [c == '1' | c <- s]
    TermSpecConstant c@(SpecConstantString _s) -> E.throw $ SMT.Error (show c)
    TermQualIdentifier qid -> f qid []
    TermQualIdentifierT  qid args -> f qid args
    TermLet bindings body ->
      interpretFun (Map.fromList [(v, EExpr (interpretFun (env,senv) t2) False) | VB v t2 <- bindings] `Map.union` env, senv) body
    TermForall _bindings _body -> E.throw $ SMT.Error "universal quantifiers are not supported yet"
    TermExists _bindings _body -> E.throw $ SMT.Error "existential quantifiers are not supported yet"
    TermAnnot t2 _ -> interpretFun (env,senv) t2 -- annotations are not supported yet
  where
    unIdentifier :: Identifier -> (String, [Index])
    unIdentifier (ISymbol name) = (name, [])
    unIdentifier (I_Symbol name indexes) = (name, indexes)

    f (QIdentifierAs ident sort) args =
      case ident of
        ISymbol ('@':s) | (n,[]):_ <- reads s ->
          SMT.EValue $ SMT.ValUninterpreted n (interpretSort senv sort)
        _ -> f (QIdentifier ident) args
    f (QIdentifier ident) args
      | ('b':'v':xs, [IndexNumeral n]) <- unIdentifier ident
      , ((x,_):_) <- readDec xs
      , x < 2^n
      = if not (null args)
        then E.throw $ SMT.Error (showSL ident ++ " does not take indexes")
        else SMT.EValue $ SMT.ValBitVec $ BV.nat2bv n x
    f qid@(QIdentifier ident) args =
      case Map.lookup name env of
        Nothing -> E.throw $ SMT.Error ("unknown function symbol: " ++ showSL qid)
        Just (EFSymBuiltin name') ->
          SMT.EAp (SMT.FSym name' indexes') (map (interpretFun (env,senv)) args)
        Just _ | not (null indexes) -> E.throw $ SMT.Error (showSL ident ++ " does not take indexes")
        Just (EExpr e _) -> e
        Just (EFSymDeclared fsym _ _) -> SMT.EAp fsym (map (interpretFun (env,senv)) args)
        Just (EFunDef env' params _y body) ->
          interpretFun (Map.fromList [(p,a) | ((p,_s),a) <- zip params (map (\t -> EExpr (interpretFun (env,senv) t) False) args) ] `Map.union` env', senv) body
      where
        (name, indexes) = unIdentifier ident
        indexes' = map g indexes
        g (IndexNumeral n) = SMT.IndexNumeral (fromIntegral n)
        g (IndexSymbol s) = SMT.IndexSymbol (fromString s)

valueToTerm :: SMT.Value -> Term
valueToTerm (SMT.ValRational v) =
  case v `compare` 0 of
    GT -> f v
    EQ -> TermSpecConstant (SpecConstantNumeral 0)
    LT -> TermQualIdentifierT (QIdentifier $ ISymbol "-") [ f (negate v) ]
  where
    f v = TermQualIdentifierT (QIdentifier $ ISymbol "/")
          [ TermSpecConstant (SpecConstantNumeral (numerator v))
          , TermSpecConstant (SpecConstantNumeral (denominator v))
          ]
valueToTerm (SMT.ValBool b) =
  TermQualIdentifier $ QIdentifier $ ISymbol $ if b then "true" else "false"
valueToTerm (SMT.ValBitVec bv) =
  TermSpecConstant (SpecConstantBinary $ [if b then '1' else '0' | b <- BV.toDescBits bv])
valueToTerm (SMT.ValUninterpreted n s) =
  TermQualIdentifier $ QIdentifierAs (ISymbol $ "@" ++ show n) (sortToSortTerm s)

fsymToIdentifier :: SMT.FSym -> Identifier
fsymToIdentifier (SMT.FSym f indexes) = 
  case indexes of
    [] -> ISymbol (T.unpack $ unintern f)
    _ -> I_Symbol (T.unpack $ unintern f) (map g indexes)
  where
    g (SMT.IndexNumeral n) =  IndexNumeral (fromIntegral n)
    g (SMT.IndexSymbol s)  = IndexSymbol (T.unpack $ unintern s)

exprToTerm :: SMT.Expr -> Term
exprToTerm (SMT.EValue v) = valueToTerm v
exprToTerm (SMT.EAp f []) = TermQualIdentifier (QIdentifier (fsymToIdentifier f))
exprToTerm (SMT.EAp f xs) = TermQualIdentifierT (QIdentifier (fsymToIdentifier f)) (map exprToTerm xs)

ssymToSymbol :: SMT.SSym -> Identifier
ssymToSymbol SMT.SSymBool = ISymbol "Bool"
ssymToSymbol SMT.SSymReal = ISymbol "Real"
ssymToSymbol (SMT.SSymBitVec n) = I_Symbol "BitVec" [IndexNumeral n]
ssymToSymbol (SMT.SSymUninterpreted name _) = ISymbol (T.unpack (unintern name))

sortToSortTerm :: SMT.Sort -> Sort
sortToSortTerm (SMT.Sort s []) = SortId (ssymToSymbol s)
sortToSortTerm (SMT.Sort s xs) = SortIdentifiers (ssymToSymbol s) (map sortToSortTerm xs)

-- ----------------------------------------------------------------------

data Solver
  = Solver
  { svSMTSolverRef :: !(IORef SMT.Solver)
  , svEnvRef :: !(IORef Env)
  , svModeRef :: !(IORef Mode)
  , svSavedContextsRef :: !(IORef [(Maybe (EEnv, SortEnv), [Term])])
  , svStatusRef :: IORef (Maybe Bool)
  , svAssertionsRef :: IORef [Term]
  , svRegularOutputChannelRef :: !(IORef (String, Handle))
  , svDiagnosticOutputChannelRef :: !(IORef (String, Handle))
  , svPrintSuccessRef :: !(IORef Bool)
  , svProduceAssertionsRef :: !(IORef Bool)
  , svProduceAssignmentRef :: !(IORef Bool)
  , svProduceModelsRef :: !(IORef Bool)
  , svProduceUnsatAssumptionsRef :: !(IORef Bool)
  , svProduceUnsatCoresRef :: !(IORef Bool)
  , svGlobalDeclarationsRef :: !(IORef Bool)
  , svUnsatAssumptionsRef :: !(IORef [Term])
  }

newSolver :: IO Solver
newSolver = do
  solverRef <- newIORef =<< SMT.newSolver
  envRef <- newIORef initialEnv
  modeRef <- newIORef ModeStart
  savedContextsRef <- newIORef []
  statusRef <- newIORef Nothing
  assertionsRef <- newIORef ([] :: [Term])
  regOutputRef <- newIORef ("stdout", stdout)
  diagOutputRef <- newIORef ("stderr", stderr)
  printSuccessRef <- newIORef True
  produceAssertionsRef <- newIORef False
  produceAssignmentRef <- newIORef False
  produceModelsRef <- newIORef False
  produceUnsatAssumptionsRef <- newIORef False
  produceUnsatCoresRef <- newIORef False  
  globalDeclarationsRef <- newIORef False
  unsatAssumptionsRef <- newIORef undefined
  return $
    Solver
    { svSMTSolverRef = solverRef
    , svEnvRef = envRef
    , svModeRef = modeRef
    , svUnsatAssumptionsRef = unsatAssumptionsRef
    , svSavedContextsRef = savedContextsRef
    , svStatusRef = statusRef
    , svAssertionsRef = assertionsRef
    , svRegularOutputChannelRef = regOutputRef
    , svDiagnosticOutputChannelRef = diagOutputRef
    , svPrintSuccessRef = printSuccessRef
    , svProduceAssertionsRef = produceAssertionsRef
    , svProduceAssignmentRef = produceAssignmentRef
    , svProduceModelsRef = produceModelsRef
    , svProduceUnsatCoresRef = produceUnsatCoresRef
    , svProduceUnsatAssumptionsRef = produceUnsatAssumptionsRef
    , svGlobalDeclarationsRef = globalDeclarationsRef
    }

initialEnv :: Env
initialEnv = (fenv, senv)
  where
    fenv = Map.fromList
      [ (name, EFSymBuiltin (fromString name))
      | name <- ["=", "true", "false", "not", "and", "or", "xor", "ite", "=>", "distinct"
                , "+", "-", "*", "/", ">=", "<=", ">", "<"
                , "extract", "concat", "bvnot", "bvneg"
                , "repeat", "zero_extend", "sign_extend", "rotate_left", "rotate_right"
                , "bvcomp"
                , "bvand", "bvor", "bvxor", "bvnand", "bvnor", "bvxnor"
                , "bvadd", "bvsub", "bvmul", "bvudiv", "bvurem", "bvsdiv", "bvsrem", "bvsmod", "bvshl", "bvlshr", "bvashr"
                , "bvule", "bvult", "bvuge", "bvugt", "bvsle", "bvslt", "bvsge", "bvsgt"
                ]
      ]
    senv = Map.fromList
      [ ("Real", SortSym SMT.SSymReal)
      , ("Bool", SortSym SMT.SSymBool)
      ]

execCommand :: Solver -> Command -> IO ()
execCommand solver cmd = do
  -- putStrLn $ showSL cmd
  printResponse solver =<< runCommand solver cmd

printResponse :: Solver -> CmdResponse -> IO ()
printResponse solver rsp = do
  b <- readIORef (svPrintSuccessRef solver)
  unless (rsp == CmdGenResponse Success && not b) $ do
    (_,h) <- readIORef (svRegularOutputChannelRef solver)
    hPutStrLn h (showSL rsp)

runCommand :: Solver -> Command -> IO CmdResponse
runCommand solver cmd = E.handle h $ do
  case cmd of
    SetLogic logic -> const (CmdGenResponse Success) <$> setLogic solver logic
    SetOption opt -> const (CmdGenResponse Success) <$> setOption solver opt
    GetOption s -> CmdGetOptionResponse <$> getOption solver s
    SetInfo attr -> const (CmdGenResponse Success) <$> setInfo solver attr
    GetInfo flags -> CmdGetInfoResponse <$> getInfo solver flags
    Push n -> const (CmdGenResponse Success) <$> push solver n
    Pop n -> const (CmdGenResponse Success) <$> pop solver n
    DeclareSort name arity -> const (CmdGenResponse Success) <$> declareSort solver name arity
    DefineSort name xs body -> const (CmdGenResponse Success) <$> defineSort solver name xs body
    DeclareConst name y -> const (CmdGenResponse Success) <$> declareConst solver name y
    DeclareFun name xs y -> const (CmdGenResponse Success) <$> declareFun solver name xs y
    DefineFun name xs y body -> const (CmdGenResponse Success) <$> defineFun solver name xs y body
    DefineFunRec name xs y body -> const (CmdGenResponse Success) <$> defineFunRec solver name xs y body
    DefineFunsRec fundecs terms -> const (CmdGenResponse Success) <$> defineFunsRec solver fundecs terms
    Assert tm -> const (CmdGenResponse Success) <$> assert solver tm
    GetAssertions -> CmdGetAssertionsResponse <$> getAssertions solver
    CheckSat -> CmdCheckSatResponse <$> checkSat solver
    CheckSatAssuming ts -> CmdCheckSatResponse <$> checkSatAssuming solver ts
    GetValue ts -> CmdGetValueResponse <$> getValue solver ts
    GetAssignment -> CmdGetAssignmentResponse <$> getAssignment solver
    GetModel -> CmdGetModelResponse <$> getModel solver
    GetProof -> CmdGetProofResponse <$> getProof solver
    GetUnsatCore -> CmdGetUnsatCoreResponse <$> getUnsatCore solver
    GetUnsatAssumptions -> CmdGetUnsatAssumptionsResponse <$> getUnsatAssumptions solver  
    Reset -> const (CmdGenResponse Success) <$> reset solver
    ResetAssertions -> const (CmdGenResponse Success) <$> resetAssertions solver
    Echo s -> CmdEchoResponse <$> echo solver s
    Exit -> const (CmdGenResponse Success) <$> exit solver
  where
    h SMT.Unsupported = return (CmdGenResponse Unsupported)
    h (SMT.Error s) = return $ CmdGenResponse $
     -- GenResponse type uses strings in printed form.
     Error $ "\"" ++ concat [if c == '"' then "\"\"" else [c] | c <- s] ++ "\""

execCommandString :: Solver -> String -> IO ()
execCommandString solver cmd = do
  printResponse solver =<< runCommandString solver cmd

runCommandString :: Solver -> String -> IO CmdResponse
runCommandString solver cmd =
  case Parsec.parse (Parsec.spaces >> CommandsParsers.parseCommand <* Parsec.eof) "" cmd of
    Left err -> 
      -- GenResponse type uses strings in printed form.
      return $ CmdGenResponse $ Error $ "\"" ++ concat [if c == '"' then "\"\"" else [c] | c <- show err] ++ "\""
    Right cmd ->
      runCommand solver cmd

-- ----------------------------------------------------------------------

reset :: Solver -> IO GenResponse
reset solver = do
  writeIORef (svSMTSolverRef solver) =<< SMT.newSolver
  writeIORef (svEnvRef solver) initialEnv
  writeIORef (svModeRef solver) ModeStart
  writeIORef (svSavedContextsRef solver) []
  writeIORef (svStatusRef solver) Nothing
  writeIORef (svRegularOutputChannelRef solver) ("stdout",stdout)
  writeIORef (svDiagnosticOutputChannelRef solver) ("stderr",stderr)
  writeIORef (svPrintSuccessRef solver) True
  writeIORef (svProduceAssertionsRef solver) False
  writeIORef (svProduceAssignmentRef solver) False
  writeIORef (svProduceModelsRef solver) False
  writeIORef (svProduceUnsatAssumptionsRef solver) False
  writeIORef (svProduceUnsatCoresRef solver) False
  writeIORef (svUnsatAssumptionsRef solver) undefined
  return Success

setLogic :: Solver -> String -> IO ()
setLogic solver logic = do
  mode <- readIORef (svModeRef solver)
  if mode /= ModeStart then do
    E.throwIO $ SMT.Error "set-logic can only be used in start mode"
  else do
    writeIORef (svModeRef solver) ModeAssert
    case logic of
      "QF_UFLRA" -> return ()
      "QF_UFRDL" -> return ()
      "QF_UF" -> return ()
      "QF_RDL" -> return ()
      "QF_LRA" -> return ()
      "QF_BV" -> return ()
      "QF_UFBV" -> return ()
      "ALL" -> return ()
      "ALL_SUPPORTED" -> return ()
      _ -> E.throwIO SMT.Unsupported

setOption :: Solver -> Option -> IO ()
setOption solver opt = do
  mode <- readIORef (svModeRef solver)
  case opt of
    PrintSuccess b -> do
      writeIORef (svPrintSuccessRef solver) b
    ExpandDefinitions _b -> do
      -- expand-definitions has been removed in SMT-LIB 2.5.
      E.throwIO SMT.Unsupported
    InteractiveMode b -> do
      -- interactive-mode is the old name for produce-assertions. Deprecated.
      unless (mode == ModeStart) $ do
        E.throwIO $ SMT.Error "interactive-mode option can be set only in start mode"
      writeIORef (svProduceAssertionsRef solver) b
      return ()
    ProduceProofs b -> do
      if mode /= ModeStart then
        E.throwIO $ SMT.Error "produce-proofs option can be set only in start mode"
      else if b then
        E.throwIO SMT.Unsupported
      else
        return ()
    ProduceUnsatCores b -> do
      unless (mode == ModeStart) $ do
        E.throwIO $ SMT.Error "produce-unsat-cores option can be set only in start mode"
      writeIORef (svProduceUnsatCoresRef solver) b
      return ()
    ProduceUnsatAssumptions b -> do
      unless (mode == ModeStart) $ do
        E.throwIO $ SMT.Error "produce-unsat-assumptions option can be set only in start mode"
      writeIORef (svProduceUnsatAssumptionsRef solver) b
      return ()
    ProduceModels b -> do
      unless (mode == ModeStart) $ do
        E.throwIO $ SMT.Error "produce-models option can be set only in start mode"
      writeIORef (svProduceModelsRef solver) b
      return ()
    ProduceAssignments b -> do
      unless (mode == ModeStart) $ do
        E.throwIO $ SMT.Error "produce-assignments option can be set only in start mode"
      writeIORef (svProduceAssignmentRef solver) b
      return ()
    ProduceAssertions b -> do
      unless (mode == ModeStart) $ do
        E.throwIO $ SMT.Error "produce-assertions option can be set only in start mode"
      writeIORef (svProduceAssertionsRef solver) b
      return ()
    GlobalDeclarations b -> do
      unless (mode == ModeStart) $ do
        E.throwIO $ SMT.Error "global-declarations option can be set only in start mode"
      writeIORef (svGlobalDeclarationsRef solver) b
      smt <- readIORef (svSMTSolverRef solver)
      SMT.setGlobalDeclarations smt b
    RegularOutputChannel fname -> do
      h <- if fname == "stdout" then
             return stdout
           else
             openFile fname AppendMode
      writeIORef (svRegularOutputChannelRef solver) (fname, h)
      return ()
    DiagnosticOutputChannel fname -> do
      h <- if fname == "stderr" then
             return stderr
           else
             openFile fname AppendMode
      writeIORef (svDiagnosticOutputChannelRef solver) (fname, h)
      return ()
    RandomSeed _i ->
      if mode /= ModeStart then
        E.throwIO $ SMT.Error "random-seed option can be set only in start mode"
      else
        E.throwIO SMT.Unsupported
    Verbosity _lv -> E.throwIO SMT.Unsupported
    ReproducibleResourceLimit _val -> do
      if mode /= ModeStart then
        E.throwIO $ SMT.Error "reproducible-resource-limit option can be set only in start mode"
      else
        E.throwIO SMT.Unsupported
    OptionAttr _attr -> E.throwIO SMT.Unsupported

getOption :: Solver -> String -> IO GetOptionResponse
getOption solver opt =
  case opt of
    ":expand-definitions" -> do
      -- expand-definitions has been removed in SMT-LIB 2.5.
      let b = False
      return $ AttrValueSymbol (showSL b)
    ":global-declarations" -> do
      b <- readIORef (svGlobalDeclarationsRef solver)
      return $ AttrValueSymbol (showSL b)
    ":interactive-mode" -> do
      -- interactive-mode is the old name for produce-assertions. Deprecated.
      b <- readIORef (svProduceAssertionsRef solver)
      return $ AttrValueSymbol (showSL b)
    ":print-success" -> do
      b <- readIORef (svPrintSuccessRef solver)
      return $ AttrValueSymbol (showSL b) 
    ":produce-assertions" -> do
      b <- readIORef (svProduceAssertionsRef solver)
      return $ AttrValueSymbol (showSL b)
    ":produce-assignments" -> do
      b <- readIORef (svProduceAssignmentRef solver)
      return $ AttrValueSymbol (showSL b)
    ":produce-models" -> do
      b <- readIORef (svProduceModelsRef solver)
      return $ AttrValueSymbol (showSL b)
    ":produce-proofs" -> do
      let b = False -- default value
      return $ AttrValueSymbol (showSL b)
    ":produce-unsat-cores" -> do
      b <- readIORef (svProduceUnsatCoresRef solver)
      return $ AttrValueSymbol (showSL b)
    ":produce-unsat-assumptions" -> do
      b <- readIORef (svProduceUnsatAssumptionsRef solver)
      return $ AttrValueSymbol (showSL b)
    ":regular-output-channel" -> do
      (fname,_) <- readIORef (svRegularOutputChannelRef solver)
      return $ AttrValueConstant (SpecConstantString fname)
    ":diagnostic-output-channel" -> do
      (fname,_) <- readIORef (svDiagnosticOutputChannelRef solver)
      return $ AttrValueConstant (SpecConstantString fname)
    ":random-seed" -> do
      return $ AttrValueConstant (SpecConstantNumeral 0) -- default value
    ":reproducible-resource-limit" -> do
      return $ AttrValueConstant (SpecConstantNumeral 0) -- default value
    ":verbosity" -> do
      return $ AttrValueConstant (SpecConstantNumeral 0) -- default value
    _ -> do
      E.throwIO SMT.Unsupported

setInfo :: Solver -> Attribute -> IO ()
setInfo solver (AttributeVal ":status" (AttrValueSymbol s)) = do
  v <- case s of
         "sat" -> return $ Just True
         "unsat" -> return $ Just False
         "unknown" -> return $ Nothing
         _ -> E.throwIO $ SMT.Error $ "invalid status value: " ++ s
  writeIORef (svStatusRef solver) v
setInfo _solver _ = return ()

getInfo :: Solver -> InfoFlags -> IO GetInfoResponse
getInfo solver flags = do
  mode <- readIORef (svModeRef solver)
  case flags of
    ErrorBehavior -> return [ResponseErrorBehavior ContinuedExecution]
    Name -> return [ResponseName "toysmt"]
    Authors -> return [ResponseName "Masahiro Sakai"]
    Version -> return [ResponseVersion (V.showVersion version)]
    Status -> E.throwIO SMT.Unsupported
    ReasonUnknown -> do
      if mode /= ModeSat then
        E.throwIO $ SMT.Error "Executions of get-info with :reason-unknown are allowed only when the solver is in sat mode following a check command whose response was unknown."
      else
        return [ResponseReasonUnknown Incomplete]
    AllStatistics -> do
      if not (mode == ModeSat || mode == ModeUnsat) then
        E.throwIO $ SMT.Error "Executions of get-info with :all-statistics are allowed only when the solver is in sat or unsat mode."
      else
        E.throwIO SMT.Unsupported
    AssertionStackLevels -> do
      saved <- readIORef (svSavedContextsRef solver)
      let n = length saved
      n `seq` return [ResponseAssertionStackLevels n]
    InfoFlags _s -> do
      E.throwIO SMT.Unsupported

push :: Solver -> Int -> IO ()
push solver n = do
  replicateM_ n $ do
    (env,senv) <- readIORef (svEnvRef solver)
    assertions <- readIORef (svAssertionsRef solver)
    globalDeclarations <- readIORef (svGlobalDeclarationsRef solver)
    if globalDeclarations then
      modifyIORef (svSavedContextsRef solver) ((Nothing, assertions) :)
    else
      modifyIORef (svSavedContextsRef solver) ((Just (env,senv), assertions) :)
    SMT.push =<< readIORef (svSMTSolverRef solver)
    writeIORef (svModeRef solver) ModeAssert

pop :: Solver -> Int -> IO ()
pop solver n = do
  replicateM_ n $ do
    cs <- readIORef (svSavedContextsRef solver)
    case cs of
      [] -> E.throwIO $ SMT.Error "pop from empty context"
      ((m,assertions) : cs) -> do
        case m of
          Just (env,senv) -> writeIORef (svEnvRef solver) (env,senv)
          Nothing -> return ()
        writeIORef (svAssertionsRef solver) assertions
        writeIORef (svSavedContextsRef solver) cs
        SMT.pop =<< readIORef (svSMTSolverRef solver)
        writeIORef (svModeRef solver) ModeAssert

resetAssertions :: Solver -> IO ()
resetAssertions solver = do
  cs <- readIORef (svSavedContextsRef solver)
  pop solver (length cs)

echo :: Solver -> String -> IO String
echo _solver s = return s

declareSort :: Solver -> String -> Int -> IO ()
declareSort solver name arity = do
  smt <- readIORef (svSMTSolverRef solver)
  s <- SMT.declareSSym smt name arity
  insertSort solver name (SortSym s)
  writeIORef (svModeRef solver) ModeAssert

defineSort :: Solver -> String -> [String] -> Sort -> IO ()
defineSort solver name xs body = do
  (_, senv) <- readIORef (svEnvRef solver)
  insertSort solver name (SortDef senv xs body)
  writeIORef (svModeRef solver) ModeAssert

declareConst :: Solver -> String -> Sort -> IO ()
declareConst solver name y = declareFun solver name [] y

declareFun :: Solver -> String -> [Sort] -> Sort -> IO ()
declareFun solver name xs y = do
  smt <- readIORef (svSMTSolverRef solver)
  (_, senv) <- readIORef (svEnvRef solver)
  let argsSorts = map (interpretSort senv) xs
      resultSort = interpretSort senv y
  f <- SMT.declareFSym smt name argsSorts resultSort
  insertFun solver name (EFSymDeclared f argsSorts resultSort)
  writeIORef (svModeRef solver) ModeAssert

defineFun :: Solver -> String -> [SortedVar] -> Sort -> Term -> IO ()
defineFun solver name xs y body = do
  writeIORef (svModeRef solver) ModeAssert
  (_, senv) <- readIORef (svEnvRef solver)
  let xs' = map (\(SV x s) -> (x, interpretSort senv s)) xs
      y'  = interpretSort senv y
  if null xs' then do
    body' <- processNamed solver body
    (fenv, _) <- readIORef (svEnvRef solver)
    -- use EExpr?
    insertFun solver name (EFunDef fenv [] y' body')
  else do
    (fenv, _) <- readIORef (svEnvRef solver)
    insertFun solver name (EFunDef fenv xs' y' body)
  writeIORef (svModeRef solver) ModeAssert

defineFunRec :: Solver -> String -> [SortedVar] -> Sort -> Term -> IO ()
defineFunRec _solver _name _xs _y _body = do
  E.throwIO SMT.Unsupported

defineFunsRec :: Solver -> [FunDec] -> [Term] -> IO ()
defineFunsRec _solver _fundecs _terms = do
  E.throwIO SMT.Unsupported

assert :: Solver -> Term -> IO ()
assert solver tm = do
  let mname =
        case tm of
          TermAnnot _body attrs
            | name:_ <- [name | AttributeVal ":named" (AttrValueSymbol name) <- attrs] ->
                Just name
          _ -> Nothing
  tm' <- processNamed solver tm
  smt <- readIORef (svSMTSolverRef solver)
  env <- readIORef (svEnvRef solver)
  case mname of
    Nothing -> SMT.assert smt (interpretFun env tm')
    Just name -> SMT.assertNamed smt name (interpretFun env tm')
  do b <- readIORef (svProduceAssertionsRef solver)
     when b $ modifyIORef (svAssertionsRef solver) (tm :)
  writeIORef (svModeRef solver) ModeAssert

getAssertions :: Solver -> IO GetAssertionsResponse
getAssertions solver = do
  mode <- readIORef (svModeRef solver)
  when (mode == ModeStart) $ do
    E.throwIO $ SMT.Error "get-assertions cannot be used in start mode"
  b <- readIORef (svProduceAssertionsRef solver)
  unless b $ do
    E.throwIO $ SMT.Error ":produce-assertions is not enabled"
  reverse <$> readIORef (svAssertionsRef solver)

checkSat :: Solver -> IO CheckSatResponse
checkSat solver = checkSatAssuming solver []

checkSatAssuming :: Solver -> [Term] -> IO CheckSatResponse
checkSatAssuming solver xs = do
  smt <- readIORef (svSMTSolverRef solver)

  env <- readIORef (svEnvRef solver)
  ref <- newIORef Map.empty
  ys <- forM xs $ \x -> do
    let y = interpretFun env x
    modifyIORef ref (Map.insert y x)
    return y

  ret <- SMT.checkSATAssuming smt ys

  do expected <- readIORef (svStatusRef solver)
     writeIORef (svStatusRef solver) Nothing -- I'm not sure if we should reset or not.
     h <- snd <$> readIORef (svDiagnosticOutputChannelRef solver)
     case expected of
       Just True | not ret -> hPutStrLn h "WARNING: unexpected unsat; expecting sat"
       Just False | ret -> hPutStrLn h "WARNING: unexpected sat; expecting unsat"
       _ -> return ()
     hFlush h

  if ret then do
    writeIORef (svModeRef solver) ModeSat
    return Sat
  else do
    writeIORef (svModeRef solver) ModeUnsat
    m <- readIORef ref
    es <- SMT.getUnsatAssumptions smt
    writeIORef (svUnsatAssumptionsRef solver) [m Map.! e | e <- es]
    return Unsat

getValue :: Solver -> [Term] -> IO GetValueResponse
getValue solver ts = do
  ts <- mapM (processNamed solver) ts  
  mode <- readIORef (svModeRef solver)
  unless (mode == ModeSat) $ do
    E.throwIO $ SMT.Error "get-value can only be used in sat mode"
  smt <- readIORef (svSMTSolverRef solver)
  m <- SMT.getModel smt
  env <- readIORef (svEnvRef solver)
  forM ts $ \t -> do
    let e = interpretFun env t
    let v = SMT.eval m e
    return $ ValuationPair t (valueToTerm v)

getAssignment :: Solver -> IO GetAssignmentResponse
getAssignment solver = do
  mode <- readIORef (svModeRef solver)
  unless (mode == ModeSat) $ do
    E.throwIO $ SMT.Error "get-assignment can only be used in sat mode"
  smt <- readIORef (svSMTSolverRef solver)
  m <- SMT.getModel smt
  (env, _) <- readIORef (svEnvRef solver)
  liftM concat $ forM (Map.toList env) $ \(name, entry) -> do
    case entry of
      EExpr e True -> do
        s <- SMT.exprSort smt e
        if s /= SMT.sBool then do
          return []
        else do
          let v = SMT.eval m e
          case v of
            (SMT.ValBool b) -> return [TValuationPair name b]
            _ -> E.throwIO $ SMT.Error "get-assignment: should not happen"
      _ -> return []

getModel :: Solver -> IO GetModelResponse
getModel solver = do
  mode <- readIORef (svModeRef solver)
  unless (mode == ModeSat) $ do
    E.throwIO $ SMT.Error "get-model can only be used in sat mode"
  smt <- readIORef (svSMTSolverRef solver)
  m <- SMT.getModel smt
  (env, _) <- readIORef (svEnvRef solver)
  defs <- liftM catMaybes $ forM (Map.toList env) $ \(name, entry) -> do
    case entry of
      EFSymDeclared sym argsSorts resultSort -> do
        case SMT.evalFSym m sym of
          SMT.FunDef [] val ->  do -- constant
            return $ Just $ DefineFun name [] (sortToSortTerm resultSort) (valueToTerm val)
          SMT.FunDef tbl defaultVal -> do -- proper function
            let argsSV :: [SortedVar]
                argsSV = [SV ("x!" ++ show i) (sortToSortTerm s) | (i,s) <- zip [(1::Int)..] argsSorts]
                args :: [Term]
                args = [TermQualIdentifier (QIdentifier (ISymbol x)) | SV x _ <- argsSV]
                f :: ([SMT.Value], SMT.Value) -> Term -> Term
                f (vals,val) tm = 
                  TermQualIdentifierT (QIdentifier (ISymbol "ite")) [cond, valueToTerm val, tm]
                  where
                    cond =
                      case zipWith (\arg val -> TermQualIdentifierT (QIdentifier (ISymbol "=")) [arg, valueToTerm val]) args vals of
                        [c] -> c
                        cs -> TermQualIdentifierT (QIdentifier (ISymbol "and")) cs
            return $ Just $ DefineFun name argsSV (sortToSortTerm resultSort) $
              foldr f (valueToTerm defaultVal) tbl
      _ -> return Nothing
  return $ defs ++ [Assert (exprToTerm x) | x <- SMT.modelGetAssertions m]

getProof :: Solver -> IO GetProofResponse
getProof solver = do
  mode <- readIORef (svModeRef solver)
  if mode /= ModeUnsat then
    E.throwIO $ SMT.Error "get-proof can only be used in unsat mode"
  else
    E.throwIO SMT.Unsupported

getUnsatCore :: Solver -> IO GetUnsatCoreResponse
getUnsatCore solver = do
  smt <- readIORef (svSMTSolverRef solver)
  mode <- readIORef (svModeRef solver)
  unless (mode == ModeUnsat) $ do
    E.throwIO $ SMT.Error "get-unsat-core can only be used in unsat mode"
  SMT.getUnsatCore smt

getUnsatAssumptions :: Solver -> IO [Term]
getUnsatAssumptions solver = do
  mode <- readIORef (svModeRef solver)
  unless (mode == ModeUnsat) $ do
    E.throwIO $ SMT.Error "get-unsat-assumptions can only be used in unsat mode"
  readIORef (svUnsatAssumptionsRef solver)

exit :: Solver -> IO ()
exit _solver = exitSuccess

-- ----------------------------------------------------------------------

insertSort :: Solver -> String -> SortEntry -> IO ()
insertSort solver name sdef = do
  (fenv, senv) <- readIORef (svEnvRef solver)
  case Map.lookup name senv of
    Nothing -> writeIORef (svEnvRef solver) (fenv, Map.insert name sdef senv)
    Just _ -> E.throwIO $ SMT.Error (name ++ " is already used")

insertFun :: Solver -> String -> EEntry -> IO ()
insertFun solver name fdef = do
  (fenv, senv) <- readIORef (svEnvRef solver)
  case Map.lookup name fenv of
    Nothing -> writeIORef (svEnvRef solver) (Map.insert name fdef fenv, senv)
    Just _ -> E.throwIO $ SMT.Error (name ++ " is already used")

-- TODO: check closedness of terms
processNamed :: Solver -> Term -> IO Term
processNamed solver = f
  where
    f t@(TermSpecConstant _) = return t
    f t@(TermQualIdentifier _) = return t
    f (TermQualIdentifierT qid args) = do
      args' <- mapM f args
      return $ TermQualIdentifierT qid args'
    f (TermLet bindings body) = do
      body' <- f body
      return $ TermLet bindings body'
    f (TermForall bindings body) = do
      body' <- f body
      return $ TermForall bindings body'
    f (TermExists bindings body) = do
      body' <- f body
      return $ TermExists bindings body'
    f (TermAnnot body attrs) = do
      body' <- f body
      forM_ attrs $ \attr -> do
        case attr of
          AttributeVal ":named" val ->
            case val of
              AttrValueSymbol name -> do
                env <- readIORef (svEnvRef solver)
                let e = interpretFun env body'
                -- smt <- readIORef (svSMTSolverRef solver)
                -- s <- SMT.exprSort smt e
                insertFun solver name (EExpr e True)
              _ -> E.throwIO $ SMT.Error ":named attribute value should be a symbol"
          _ -> return ()
      let attrs' = [attr | attr <- attrs, attrName attr /= ":named"]
            where
              attrName (Attribute s) = s
              attrName (AttributeVal s _v) = s
      if null attrs' then
        return body'
      else
        return $ TermAnnot body' attrs'