{-  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 <http://www.gnu.org/licenses/>. -}

{-
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 <paufil@di.uminho.pt>
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"]