{- CAO Compiler
Copyright (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see . -}
{-
Module : $Header$
Description : Interface with a SMT solver (Yices).
Copyright : (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
License : GPL
Maintainer : Paulo Silva
Stability : experimental
Portability : non-portable
-}
module Language.CAO.Typechecker.SMT (
checkValidity
) where
import Control.Monad.Trans
import Math.SMT.Yices.Pipe
import Math.SMT.Yices.Syntax
import Language.CAO.Common.Error
import Language.CAO.Common.Monad
import Language.CAO.Common.SrcLoc (defSrcLoc)
import Language.CAO.Common.State
import Language.CAO.Common.Var
import Language.CAO.Index
import Language.CAO.Translation.Yices
import Language.CAO.Type
import Language.CAO.Typechecker.Heap
checkValidity :: CaoMonad m => ICond Var -> ICond Var -> m Bool
checkValidity hyp prop = do
decl <- getDecl
yices <- getYices
case yices of
Nothing -> do
caoWarning defSrcLoc $ NoProverWarning prop
return True
Just yices' -> do
r <- liftIO $ validity yices' decl (cond2Y hyp :=> cond2Y prop)
return $ either (const False) (const True) r
getDecl :: CaoMonad m => m [CmdY]
getDecl = getHeap >>= return . map worker . getIndexes
where
worker v = case varType v of
Int -> DEFINE (getSymbol v, VarT "int") Nothing
RInt -> DEFINE (getSymbol v, VarT "int") Nothing
Bool -> DEFINE (getSymbol v, VarT "bool") Nothing
_ -> error "getDecl: not defined"
validity :: FilePath -> [CmdY] -> ExpY -> IO (Either String ())
validity yices decls prop = do
res <- runYices yices (decls ++ [ASSERT (NOT prop)])
return $ case res of
Sat c -> Left $ "Assertion failed:\n" ++ show prop
++ "\nCounter example:\n" ++ concatMap show c
Unknown c -> Left $ "Unknown validity:\n" ++ show prop
++ "\nResult:\n" ++ concatMap show c
UnSat _ -> Right ()
InCon c -> Left $ "InCon: " ++ concat c
runYices :: FilePath -> [CmdY] -> IO ResY
runYices yices = quickCheckY yices ["-tc"]