{-# LANGUAGE OverloadedStrings #-}

{-|
Module       : ATP.Prover
Description  : Models of automated theorem provers.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental

Models of automated theorem provers.
-}

module ATP.Prover (
  Vendor(..),
  Prover(..),
  TimeLimit,
  MemoryLimit,
  proverArguments,
  proverOutput,
  vampire,
  eprover,
  defaultProver
) where

import Data.Text (Text)
import qualified Data.Text as T (isInfixOf)
import System.Exit (ExitCode(..))

import ATP.Error


-- | The automated theorem prover.
data Prover = Prover {
  Prover -> Vendor
vendor :: Vendor,
  Prover -> FilePath
executable :: FilePath
} deriving (Prover -> Prover -> Bool
(Prover -> Prover -> Bool)
-> (Prover -> Prover -> Bool) -> Eq Prover
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prover -> Prover -> Bool
$c/= :: Prover -> Prover -> Bool
== :: Prover -> Prover -> Bool
$c== :: Prover -> Prover -> Bool
Eq, Int -> Prover -> ShowS
[Prover] -> ShowS
Prover -> FilePath
(Int -> Prover -> ShowS)
-> (Prover -> FilePath) -> ([Prover] -> ShowS) -> Show Prover
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Prover] -> ShowS
$cshowList :: [Prover] -> ShowS
show :: Prover -> FilePath
$cshow :: Prover -> FilePath
showsPrec :: Int -> Prover -> ShowS
$cshowsPrec :: Int -> Prover -> ShowS
Show, Eq Prover
Eq Prover
-> (Prover -> Prover -> Ordering)
-> (Prover -> Prover -> Bool)
-> (Prover -> Prover -> Bool)
-> (Prover -> Prover -> Bool)
-> (Prover -> Prover -> Bool)
-> (Prover -> Prover -> Prover)
-> (Prover -> Prover -> Prover)
-> Ord Prover
Prover -> Prover -> Bool
Prover -> Prover -> Ordering
Prover -> Prover -> Prover
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Prover -> Prover -> Prover
$cmin :: Prover -> Prover -> Prover
max :: Prover -> Prover -> Prover
$cmax :: Prover -> Prover -> Prover
>= :: Prover -> Prover -> Bool
$c>= :: Prover -> Prover -> Bool
> :: Prover -> Prover -> Bool
$c> :: Prover -> Prover -> Bool
<= :: Prover -> Prover -> Bool
$c<= :: Prover -> Prover -> Bool
< :: Prover -> Prover -> Bool
$c< :: Prover -> Prover -> Bool
compare :: Prover -> Prover -> Ordering
$ccompare :: Prover -> Prover -> Ordering
$cp1Ord :: Eq Prover
Ord)

-- | The implementation of a theorem prover, supported by @atp@.
data Vendor
  = E
  | Vampire
  deriving (Vendor -> Vendor -> Bool
(Vendor -> Vendor -> Bool)
-> (Vendor -> Vendor -> Bool) -> Eq Vendor
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Vendor -> Vendor -> Bool
$c/= :: Vendor -> Vendor -> Bool
== :: Vendor -> Vendor -> Bool
$c== :: Vendor -> Vendor -> Bool
Eq, Int -> Vendor -> ShowS
[Vendor] -> ShowS
Vendor -> FilePath
(Int -> Vendor -> ShowS)
-> (Vendor -> FilePath) -> ([Vendor] -> ShowS) -> Show Vendor
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Vendor] -> ShowS
$cshowList :: [Vendor] -> ShowS
show :: Vendor -> FilePath
$cshow :: Vendor -> FilePath
showsPrec :: Int -> Vendor -> ShowS
$cshowsPrec :: Int -> Vendor -> ShowS
Show, Eq Vendor
Eq Vendor
-> (Vendor -> Vendor -> Ordering)
-> (Vendor -> Vendor -> Bool)
-> (Vendor -> Vendor -> Bool)
-> (Vendor -> Vendor -> Bool)
-> (Vendor -> Vendor -> Bool)
-> (Vendor -> Vendor -> Vendor)
-> (Vendor -> Vendor -> Vendor)
-> Ord Vendor
Vendor -> Vendor -> Bool
Vendor -> Vendor -> Ordering
Vendor -> Vendor -> Vendor
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Vendor -> Vendor -> Vendor
$cmin :: Vendor -> Vendor -> Vendor
max :: Vendor -> Vendor -> Vendor
$cmax :: Vendor -> Vendor -> Vendor
>= :: Vendor -> Vendor -> Bool
$c>= :: Vendor -> Vendor -> Bool
> :: Vendor -> Vendor -> Bool
$c> :: Vendor -> Vendor -> Bool
<= :: Vendor -> Vendor -> Bool
$c<= :: Vendor -> Vendor -> Bool
< :: Vendor -> Vendor -> Bool
$c< :: Vendor -> Vendor -> Bool
compare :: Vendor -> Vendor -> Ordering
$ccompare :: Vendor -> Vendor -> Ordering
$cp1Ord :: Eq Vendor
Ord, Int -> Vendor
Vendor -> Int
Vendor -> [Vendor]
Vendor -> Vendor
Vendor -> Vendor -> [Vendor]
Vendor -> Vendor -> Vendor -> [Vendor]
(Vendor -> Vendor)
-> (Vendor -> Vendor)
-> (Int -> Vendor)
-> (Vendor -> Int)
-> (Vendor -> [Vendor])
-> (Vendor -> Vendor -> [Vendor])
-> (Vendor -> Vendor -> [Vendor])
-> (Vendor -> Vendor -> Vendor -> [Vendor])
-> Enum Vendor
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Vendor -> Vendor -> Vendor -> [Vendor]
$cenumFromThenTo :: Vendor -> Vendor -> Vendor -> [Vendor]
enumFromTo :: Vendor -> Vendor -> [Vendor]
$cenumFromTo :: Vendor -> Vendor -> [Vendor]
enumFromThen :: Vendor -> Vendor -> [Vendor]
$cenumFromThen :: Vendor -> Vendor -> [Vendor]
enumFrom :: Vendor -> [Vendor]
$cenumFrom :: Vendor -> [Vendor]
fromEnum :: Vendor -> Int
$cfromEnum :: Vendor -> Int
toEnum :: Int -> Vendor
$ctoEnum :: Int -> Vendor
pred :: Vendor -> Vendor
$cpred :: Vendor -> Vendor
succ :: Vendor -> Vendor
$csucc :: Vendor -> Vendor
Enum, Vendor
Vendor -> Vendor -> Bounded Vendor
forall a. a -> a -> Bounded a
maxBound :: Vendor
$cmaxBound :: Vendor
minBound :: Vendor
$cminBound :: Vendor
Bounded)

-- | The time limit allocated to the prover, in seconds.
type TimeLimit = Int

-- | The memory limit allocated to the prover, in Mb.
type MemoryLimit = Int

-- | Build the list of command line arguments for the given prover.
proverArguments :: Vendor -> TimeLimit -> MemoryLimit -> [String]
proverArguments :: Vendor -> Int -> Int -> [FilePath]
proverArguments Vendor
E Int
timeLimit Int
memoryLimit =
  [FilePath
"--proof-object",
   FilePath
"--silent",
   FilePath
"--soft-cpu-limit=" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
timeLimit,
   FilePath
"--memory-limit=" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
memoryLimit]
proverArguments Vendor
Vampire Int
timeLimit Int
memoryLimit =
  [FilePath
"--proof", FilePath
"tptp",
   FilePath
"--statistics", FilePath
"none",
   FilePath
"--time_limit", Int -> FilePath
forall a. Show a => a -> FilePath
show Int
timeLimit,
   FilePath
"--memory_limit", Int -> FilePath
forall a. Show a => a -> FilePath
show Int
memoryLimit]

-- | Interpret the output of the theorem prover from its exit code and
-- the contents of the returned stdout and stderr.
proverOutput :: Vendor
             -> ExitCode
             -> Text -- ^ Standard out
             -> Text -- ^ Standard error
             -> Partial Text
proverOutput :: Vendor -> ExitCode -> Text -> Text -> Partial Text
proverOutput Vendor
E ExitCode
exitCode Text
stdout Text
stderr = case ExitCode
exitCode of
  ExitCode
ExitSuccess   -> Text -> Partial Text
forall (m :: * -> *) a. Monad m => a -> m a
return Text
stdout
  ExitFailure Int
1 -> Text -> Partial Text
forall (m :: * -> *) a. Monad m => a -> m a
return Text
stdout
  ExitFailure Int
8 -> Partial Text
forall (m :: * -> *) a. Monad m => PartialT m a
timeLimitError
  ExitFailure Int
c -> Int -> Text -> Partial Text
forall (m :: * -> *) a. Monad m => Int -> Text -> PartialT m a
exitCodeError Int
c Text
stderr
proverOutput Vendor
Vampire ExitCode
exitCode Text
stdout Text
stderr = case ExitCode
exitCode of
  ExitCode
ExitSuccess   -> Text -> Partial Text
forall (m :: * -> *) a. Monad m => a -> m a
return Text
stdout
  ExitFailure Int
1
    | Text
"Time limit reached"    Text -> Text -> Bool
`T.isInfixOf` Text
stdout -> Partial Text
forall (m :: * -> *) a. Monad m => PartialT m a
timeLimitError
    | Text
"Memory limit exceeded" Text -> Text -> Bool
`T.isInfixOf` Text
stdout -> Partial Text
forall (m :: * -> *) a. Monad m => PartialT m a
memoryLimitError
  ExitFailure Int
c -> Int -> Text -> Partial Text
forall (m :: * -> *) a. Monad m => Int -> Text -> PartialT m a
exitCodeError Int
c Text
stderr

-- | The <http://www.eprover.org/ E> theorem prover.
eprover :: Prover
eprover :: Prover
eprover = Prover :: Vendor -> FilePath -> Prover
Prover {
  vendor :: Vendor
vendor = Vendor
E,
  executable :: FilePath
executable = FilePath
"eprover"
}

-- | The <https://vprover.github.io/ Vampire> theorem prover.
vampire :: Prover
vampire :: Prover
vampire = Prover :: Vendor -> FilePath -> Prover
Prover {
  vendor :: Vendor
vendor = Vendor
Vampire,
  executable :: FilePath
executable = FilePath
"vampire"
}

-- | The default prover used by @refute@ and @prove@.
--
-- >>> defaultProver
-- Prover {vendor = E, executable = "eprover"}
defaultProver :: Prover
defaultProver :: Prover
defaultProver = Prover
eprover