toysolver-0.7.0: app/toysmt/ToySolver/SMT/SMTLIB2Solver.hs
{-# 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 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'