{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Trustworthy #-}
module Copilot.Theorem.Kind2.Prover
( module Data.Default
, Options (..)
, kind2Prover
) where
import Copilot.Theorem.Prove
import Copilot.Theorem.Kind2.Output
import Copilot.Theorem.Kind2.PrettyPrint
import Copilot.Theorem.Kind2.Translate
import System.IO hiding (openTempFile)
import Copilot.Theorem.Misc.Utils (openTempFile)
import System.Process
import System.Directory
import Data.Default
import qualified Copilot.Theorem.TransSys as TS
data Options = Options
{ Options -> Int
bmcMax :: Int
}
instance Default Options where
def :: Options
def = Options :: Int -> Options
Options { bmcMax :: Int
bmcMax = Int
0 }
data ProverST = ProverST
{ ProverST -> Options
options :: Options
, ProverST -> TransSys
transSys :: TS.TransSys }
kind2Prover :: Options -> Prover
kind2Prover :: Options -> Prover
kind2Prover Options
opts = Prover :: forall r.
String
-> (Spec -> IO r)
-> (r -> [String] -> [String] -> IO Output)
-> (r -> IO ())
-> Prover
Prover
{ proverName :: String
proverName = String
"Kind2"
, startProver :: Spec -> IO ProverST
startProver = ProverST -> IO ProverST
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverST -> IO ProverST)
-> (Spec -> ProverST) -> Spec -> IO ProverST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options -> TransSys -> ProverST
ProverST Options
opts (TransSys -> ProverST) -> (Spec -> TransSys) -> Spec -> ProverST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> TransSys
TS.translate
, askProver :: ProverST -> [String] -> [String] -> IO Output
askProver = ProverST -> [String] -> [String] -> IO Output
askKind2
, closeProver :: ProverST -> IO ()
closeProver = IO () -> ProverST -> IO ()
forall a b. a -> b -> a
const (IO () -> ProverST -> IO ()) -> IO () -> ProverST -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }
kind2Prog :: String
kind2Prog = String
"kind2"
kind2BaseOptions :: [String]
kind2BaseOptions = [String
"--input-format", String
"native", String
"-xml"]
askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output
askKind2 :: ProverST -> [String] -> [String] -> IO Output
askKind2 (ProverST Options
opts TransSys
spec) [String]
assumptions [String]
toCheck = do
let kind2Input :: String
kind2Input = File -> String
prettyPrint (File -> String) -> (TransSys -> File) -> TransSys -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Style -> [String] -> [String] -> TransSys -> File
toKind2 Style
Inlined [String]
assumptions [String]
toCheck (TransSys -> String) -> TransSys -> String
forall a b. (a -> b) -> a -> b
$ TransSys
spec
(String
tempName, Handle
tempHandle) <- String -> String -> String -> IO (String, Handle)
openTempFile String
"." String
"out" String
"kind"
Handle -> String -> IO ()
hPutStr Handle
tempHandle String
kind2Input
Handle -> IO ()
hClose Handle
tempHandle
let kind2Options :: [String]
kind2Options =
[String]
kind2BaseOptions [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"--bmc_max", Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Options -> Int
bmcMax Options
opts, String
tempName]
(ExitCode
_, String
output, String
_) <- String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
kind2Prog [String]
kind2Options String
""
String -> IO ()
putStrLn String
kind2Input
String -> IO ()
removeFile String
tempName
Output -> IO Output
forall (m :: * -> *) a. Monad m => a -> m a
return (Output -> IO Output) -> Output -> IO Output
forall a b. (a -> b) -> a -> b
$ String -> String -> Output
parseOutput ([String] -> String
forall a. [a] -> a
head [String]
toCheck) String
output