toysolver-0.10.0: src/ToySolver/SMT/SMTLIB2Solver.hs
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE OverloadedStrings #-}
-----------------------------------------------------------------------------
-- |
-- 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 Language.SMTLIB.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
, defineConst
, 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 Data.Text (Text)
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 ToySolver.BitVector as BV
import qualified ToySolver.SMT as SMT
import ToySolver.Version
import Language.SMTLIB.Syntax
import Language.SMTLIB.Parser (parseCommand')
import Language.SMTLIB.Printer (Pretty, renderText)
-- | Render an SMT-LIB AST node back to its concrete syntax as a 'String'.
showSL :: Pretty a => a -> String
showSL = T.unpack . renderText
-- ----------------------------------------------------------------------
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 (Sort ident args ()) =
case ident of
Identifier "BitVec" indexes ()
| not (null args) -> E.throw $ SMT.Error (showSL ident ++ ": wrong number of arguments (" ++ show (length args) ++ " for 0)")
| [IxNumeral n ()] <- indexes -> SMT.sBitVec (fromInteger n)
| otherwise -> E.throw $ SMT.Error ("BitVec: wrong number of indexes (" ++ show (length indexes) ++ " for 1)")
Identifier _ (_:_) () ->
E.throw $ SMT.Error ("unknown sort: " ++ showSL ident)
Identifier name [] () ->
case Map.lookup (T.unpack 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
TConstant (SCNumeral n ()) () -> SMT.EValue $ SMT.ValRational $ fromInteger n
TConstant (SCDecimal s ()) () -> SMT.EValue $ SMT.ValRational $ fst $ head $ readFloat $ T.unpack s
TConstant (SCHexadecimal s ()) () ->
let n = fst $ head $ readHex $ T.unpack s
in SMT.EValue $ SMT.ValBitVec $ BV.nat2bv (T.length s * 4) n
TConstant (SCBinary s ()) () ->
SMT.EValue $ SMT.ValBitVec $ BV.fromDescBits [c == '1' | c <- T.unpack s]
TConstant c@(SCString _s ()) () -> E.throw $ SMT.Error (show c)
TQualIdent qid () -> f qid []
TApp qid args () -> f qid args
TLet bindings body () ->
interpretFun (Map.fromList [(T.unpack v, EExpr (interpretFun (env,senv) t2) False) | VarBinding v t2 () <- bindings] `Map.union` env, senv) body
TLambda _bindings _body () -> E.throw $ SMT.Error "lambda abstractions are not supported yet"
TForall _bindings _body () -> E.throw $ SMT.Error "universal quantifiers are not supported yet"
TExists _bindings _body () -> E.throw $ SMT.Error "existential quantifiers are not supported yet"
TMatch _e _cases () -> E.throw $ SMT.Error "match expressions are not supported yet"
TAnnot t2 _ () -> interpretFun (env,senv) t2 -- annotations are not supported yet
where
unIdentifier :: Identifier () -> (String, [Index ()])
unIdentifier (Identifier name indexes ()) = (T.unpack name, indexes)
f (QIdentifierAs ident sort ()) args =
case ident of
Identifier sym [] ()
| Just s <- T.stripPrefix "@" sym, ((n,[]):_) <- reads (T.unpack s) ->
SMT.EValue $ SMT.ValUninterpreted n (interpretSort senv sort)
_ -> f (QIdentifier ident ()) args
f (QIdentifier ident ()) args
| ('b':'v':xs, [IxNumeral 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 (fromInteger 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 (\u -> EExpr (interpretFun (env,senv) u) False) args) ] `Map.union` env', senv) body
where
(name, indexes) = unIdentifier ident
indexes' = map g indexes
g (IxNumeral n ()) = SMT.IndexNumeral (fromIntegral n)
g (IxSymbol s ()) = SMT.IndexSymbol (fromString (T.unpack s))
valueToTerm :: SMT.Value -> Term ()
valueToTerm (SMT.ValRational v) =
case v `compare` 0 of
GT -> f v
EQ -> TConstant (SCNumeral 0 ()) ()
LT -> TApp (QIdentifier (simpleId "-") ()) [ f (negate v) ] ()
where
f w = TApp (QIdentifier (simpleId "/") ())
[ TConstant (SCNumeral (numerator w) ()) ()
, TConstant (SCNumeral (denominator w) ()) ()
] ()
valueToTerm (SMT.ValBool b) =
TQualIdent (QIdentifier (simpleId (if b then "true" else "false")) ()) ()
valueToTerm (SMT.ValBitVec bv) =
TConstant (SCBinary (T.pack [if b then '1' else '0' | b <- BV.toDescBits bv]) ()) ()
valueToTerm (SMT.ValUninterpreted n s) =
TQualIdent (QIdentifierAs (simpleId (T.pack ("@" ++ show n))) (sortToSortTerm s) ()) ()
ssymToSymbol :: SMT.SSym -> Identifier ()
ssymToSymbol SMT.SSymBool = simpleId "Bool"
ssymToSymbol SMT.SSymReal = simpleId "Real"
ssymToSymbol (SMT.SSymBitVec n) = Identifier "BitVec" [IxNumeral (fromIntegral n) ()] ()
ssymToSymbol (SMT.SSymUninterpreted name _) = simpleId (unintern name)
sortToSortTerm :: SMT.Sort -> Sort ()
sortToSortTerm (SMT.Sort s xs) = Sort (ssymToSymbol s) (map sortToSortTerm xs) ()
-- | A simple (non-indexed) identifier with a unit annotation.
simpleId :: Text -> Identifier ()
simpleId name = Identifier name [] ()
-- ----------------------------------------------------------------------
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 -> CommandResponse () -> IO ()
printResponse solver rsp = do
b <- readIORef (svPrintSuccessRef solver)
unless (rsp == RSuccess && not b) $ do
(_,h) <- readIORef (svRegularOutputChannelRef solver)
hPutStrLn h (showSL rsp)
runCommand :: Solver -> Command () -> IO (CommandResponse ())
runCommand solver cmd = E.handle h $ do
case cmd of
SetLogic logic () -> const RSuccess <$> setLogic solver (T.unpack logic)
SetOption opt () -> const RSuccess <$> setOption solver opt
GetOption k () -> RGetOption <$> getOption solver (':' : T.unpack k)
SetInfo attr () -> const RSuccess <$> setInfo solver attr
GetInfo flags () -> RGetInfo <$> getInfo solver flags
Push n () -> const RSuccess <$> push solver (fromInteger n)
Pop n () -> const RSuccess <$> pop solver (fromInteger n)
DeclareSort name arity () -> const RSuccess <$> declareSort solver (T.unpack name) (fromInteger arity)
DefineSort name xs body () -> const RSuccess <$> defineSort solver (T.unpack name) (map T.unpack xs) body
DeclareConst name y () -> const RSuccess <$> declareConst solver (T.unpack name) y
DefineConst name y body () -> const RSuccess <$> defineConst solver (T.unpack name) y body
DeclareFun name xs y () -> const RSuccess <$> declareFun solver (T.unpack name) xs y
DefineFun (FunctionDef name xs y body ()) () -> const RSuccess <$> defineFun solver (T.unpack name) xs y body
DefineFunRec (FunctionDef name xs y body ()) () -> const RSuccess <$> defineFunRec solver (T.unpack name) xs y body
DefineFunsRec fundecs terms () -> const RSuccess <$> defineFunsRec solver fundecs terms
Assert tm () -> const RSuccess <$> assert solver tm
GetAssertions () -> RGetAssertions <$> getAssertions solver
CheckSat () -> RCheckSat <$> checkSat solver
CheckSatAssuming ts () -> RCheckSat <$> checkSatAssuming solver ts
GetValue ts () -> RGetValue <$> getValue solver ts
GetAssignment () -> RGetAssignment <$> getAssignment solver
GetModel () -> RGetModel <$> getModel solver
GetProof () -> RGetProof <$> getProof solver
GetUnsatCore () -> RGetUnsatCore <$> getUnsatCore solver
GetUnsatAssumptions () -> RGetUnsatAssumptions <$> getUnsatAssumptions solver
Reset () -> const RSuccess <$> reset solver
ResetAssertions () -> const RSuccess <$> resetAssertions solver
Echo s () -> REcho <$> echo solver s
Exit () -> const RSuccess <$> exit solver
-- Commands without solver support
DeclareDatatype _ _ () -> E.throwIO SMT.Unsupported
DeclareDatatypes _ _ () -> E.throwIO SMT.Unsupported
DeclareSortParameter _ () -> E.throwIO SMT.Unsupported
UnknownCommand _ _ () -> E.throwIO SMT.Unsupported
where
h SMT.Unsupported = return RUnsupported
h (SMT.Error s) = return $ RError $ T.pack s
execCommandString :: Solver -> String -> IO ()
execCommandString solver cmd = do
printResponse solver =<< runCommandString solver cmd
runCommandString :: Solver -> String -> IO (CommandResponse ())
runCommandString solver cmd =
case parseCommand' "<string>" (T.pack cmd) of
Left err ->
return $ RError $ T.pack $ show err
Right cmd' ->
runCommand solver cmd'
-- ----------------------------------------------------------------------
reset :: Solver -> IO ()
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
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
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
let fname' = T.unpack fname
hdl <- if fname' == "stdout" then
return stdout
else
openFile fname' AppendMode
writeIORef (svRegularOutputChannelRef solver) (fname', hdl)
return ()
DiagnosticOutputChannel fname () -> do
let fname' = T.unpack fname
hdl <- if fname' == "stderr" then
return stderr
else
openFile fname' AppendMode
writeIORef (svDiagnosticOutputChannelRef solver) (fname', hdl)
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
OptionAttribute _attr () -> E.throwIO SMT.Unsupported
getOption :: Solver -> String -> IO (AttributeValue ())
getOption solver opt =
case opt of
":expand-definitions" -> do
-- expand-definitions has been removed in SMT-LIB 2.5.
return $ boolValue False
":global-declarations" -> do
b <- readIORef (svGlobalDeclarationsRef solver)
return $ boolValue b
":interactive-mode" -> do
-- interactive-mode is the old name for produce-assertions. Deprecated.
b <- readIORef (svProduceAssertionsRef solver)
return $ boolValue b
":print-success" -> do
b <- readIORef (svPrintSuccessRef solver)
return $ boolValue b
":produce-assertions" -> do
b <- readIORef (svProduceAssertionsRef solver)
return $ boolValue b
":produce-assignments" -> do
b <- readIORef (svProduceAssignmentRef solver)
return $ boolValue b
":produce-models" -> do
b <- readIORef (svProduceModelsRef solver)
return $ boolValue b
":produce-proofs" -> do
let b = False -- default value
return $ boolValue b
":produce-unsat-cores" -> do
b <- readIORef (svProduceUnsatCoresRef solver)
return $ boolValue b
":produce-unsat-assumptions" -> do
b <- readIORef (svProduceUnsatAssumptionsRef solver)
return $ boolValue b
":regular-output-channel" -> do
(fname,_) <- readIORef (svRegularOutputChannelRef solver)
return $ AVConstant (SCString (T.pack fname) ()) ()
":diagnostic-output-channel" -> do
(fname,_) <- readIORef (svDiagnosticOutputChannelRef solver)
return $ AVConstant (SCString (T.pack fname) ()) ()
":random-seed" -> do
return $ AVConstant (SCNumeral 0 ()) () -- default value
":reproducible-resource-limit" -> do
return $ AVConstant (SCNumeral 0 ()) () -- default value
":verbosity" -> do
return $ AVConstant (SCNumeral 0 ()) () -- default value
_ -> do
E.throwIO SMT.Unsupported
where
boolValue b = AVSymbol (if b then "true" else "false") ()
setInfo :: Solver -> Attribute () -> IO ()
setInfo solver (AttributeWith "status" (AVSymbol s ()) ()) = do
v <- case s of
"sat" -> return $ Just True
"unsat" -> return $ Just False
"unknown" -> return $ Nothing
_ -> E.throwIO $ SMT.Error $ "invalid status value: " ++ T.unpack s
writeIORef (svStatusRef solver) v
setInfo _solver _ = return ()
getInfo :: Solver -> InfoFlag () -> IO [InfoResponse ()]
getInfo solver flag = do
mode <- readIORef (svModeRef solver)
case flag of
ErrorBehaviorFlag () -> return [IRErrorBehavior ContinuedExecution]
InfoName () -> return [IRName "toysmt"]
Authors () -> return [IRAuthors "Masahiro Sakai"]
InfoVersion () -> return [IRVersion (T.pack (V.showVersion version))]
ReasonUnknownFlag () -> 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 [IRReasonUnknown RUIncomplete]
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 [IRAssertionStackLevels (fromIntegral n)]
InfoFlagKeyword _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 -> Text -> IO Text
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
-- | @(define-const c σ t)@ is syntactic sugar for @(define-fun c () σ t)@.
defineConst :: Solver -> String -> Sort () -> Term () -> IO ()
defineConst solver name y body = defineFun solver name [] y body
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 (\(SortedVar x s ()) -> (T.unpack 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 -> [FunctionDec ()] -> [Term ()] -> IO ()
defineFunsRec _solver _fundecs _terms = do
E.throwIO SMT.Unsupported
assert :: Solver -> Term () -> IO ()
assert solver tm = do
let mname =
case tm of
TAnnot _body attrs ()
| name:_ <- [name | AttributeWith "named" (AVSymbol name ()) () <- attrs] ->
Just (T.unpack 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 [Term ()]
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 [ValuationPair ()]
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 [(Symbol, Bool)]
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 [(T.pack name, b)]
_ -> E.throwIO $ SMT.Error "get-assignment: should not happen"
_ -> return []
getModel :: Solver -> IO [ModelResponse ()]
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)
let env2 =
case SMT.evalFSym m "/0" of
SMT.FunDef tbl _defaultVal | not (null tbl) -> Map.insert "/0" (EFSymDeclared "/0" [SMT.sReal] SMT.sReal) env
_ -> env
liftM catMaybes $ forM (Map.toList env2) $ \(name, entry) -> do
case entry of
EFSymDeclared sym argsSorts resultSort -> do
case SMT.evalFSym m sym of
SMT.FunDef [] val -> do -- constant
return $ Just $ MRDefineFun (FunctionDef (T.pack name) [] (sortToSortTerm resultSort) (valueToTerm val) ())
SMT.FunDef tbl defaultVal -> do -- proper function
let argsSV :: [SortedVar ()]
argsSV = [SortedVar (T.pack ("x!" ++ show i)) (sortToSortTerm s) () | (i,s) <- zip [(1::Int)..] argsSorts]
args :: [Term ()]
args = [TQualIdent (QIdentifier (simpleId x) ()) () | SortedVar x _ () <- argsSV]
f :: ([SMT.Value], SMT.Value) -> Term () -> Term ()
f (vals,val) tm =
TApp (QIdentifier (simpleId "ite") ()) [cond, valueToTerm val, tm] ()
where
cond =
case zipWith (\arg val' -> TApp (QIdentifier (simpleId "=") ()) [arg, valueToTerm val'] ()) args vals of
[c] -> c
cs -> TApp (QIdentifier (simpleId "and") ()) cs ()
return $ Just $ MRDefineFun $ FunctionDef (T.pack name) argsSV (sortToSortTerm resultSort)
(foldr f (valueToTerm defaultVal) tbl) ()
_ -> return Nothing
getProof :: Solver -> IO (SExpr ())
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 [Symbol]
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"
map T.pack <$> 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@(TConstant _ ()) = return t
f t@(TQualIdent _ ()) = return t
f (TApp qid args ()) = do
args' <- mapM f args
return $ TApp qid args' ()
f (TLet bindings body ()) = do
body' <- f body
return $ TLet bindings body' ()
f (TLambda bindings body ()) = do
body' <- f body
return $ TLambda bindings body' ()
f (TForall bindings body ()) = do
body' <- f body
return $ TForall bindings body' ()
f (TExists bindings body ()) = do
body' <- f body
return $ TExists bindings body' ()
f t@(TMatch _ _ ()) = return t
f (TAnnot body attrs ()) = do
body' <- f body
forM_ attrs $ \attr -> do
case attr of
AttributeWith "named" val () ->
case val of
AVSymbol name () -> do
env <- readIORef (svEnvRef solver)
let e = interpretFun env body'
-- smt <- readIORef (svSMTSolverRef solver)
-- s <- SMT.exprSort smt e
insertFun solver (T.unpack 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 (AttributeWith s _v ()) = s
if null attrs' then
return body'
else
return $ TAnnot body' attrs' ()