{-# LANGUAGE GADTs, CPP #-}
module Jukebox.ExternalProvers.SPASS where
import Jukebox.Form hiding (tag, Or)
import Jukebox.Options
import Jukebox.Utils
import Jukebox.TPTP.Print
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
data SPASSFlags =
SPASSFlags {
SPASSFlags -> String
spass :: String,
SPASSFlags -> Maybe Int
timeout :: Maybe Int,
SPASSFlags -> Bool
sos :: Bool }
spassFlags :: OptionParser SPASSFlags
spassFlags =
String -> OptionParser SPASSFlags -> OptionParser SPASSFlags
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"SPASS prover options" (OptionParser SPASSFlags -> OptionParser SPASSFlags)
-> OptionParser SPASSFlags -> OptionParser SPASSFlags
forall a b. (a -> b) -> a -> b
$
String -> Maybe Int -> Bool -> SPASSFlags
SPASSFlags (String -> Maybe Int -> Bool -> SPASSFlags)
-> Annotated [Flag] ParParser String
-> Annotated [Flag] ParParser (Maybe Int -> Bool -> SPASSFlags)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
String
-> [String]
-> String
-> ArgParser String
-> Annotated [Flag] ParParser String
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"spass"
[String
"Path to SPASS (\"SPASS\" by default)."]
String
"SPASS"
ArgParser String
argFile Annotated [Flag] ParParser (Maybe Int -> Bool -> SPASSFlags)
-> Annotated [Flag] ParParser (Maybe Int)
-> Annotated [Flag] ParParser (Bool -> SPASSFlags)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
String
-> [String]
-> Maybe Int
-> ArgParser (Maybe Int)
-> Annotated [Flag] ParParser (Maybe Int)
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"timeout"
[String
"Timeout in seconds (off by default)."]
Maybe Int
forall a. Maybe a
Nothing
((Int -> Maybe Int)
-> Annotated [String] SeqParser Int -> ArgParser (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Maybe Int
forall a. a -> Maybe a
Just Annotated [String] SeqParser Int
forall a. (Read a, Num a) => ArgParser a
argNum) Annotated [Flag] ParParser (Bool -> SPASSFlags)
-> Annotated [Flag] ParParser Bool -> OptionParser SPASSFlags
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
String
-> [String]
-> Bool
-> ArgParser Bool
-> Annotated [Flag] ParParser Bool
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"sos"
[String
"Use set-of-support strategy (off by default)."]
Bool
False
(Bool -> ArgParser Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)
runSPASS :: SPASSFlags -> Problem Form -> IO Answer
runSPASS :: SPASSFlags -> Problem Form -> IO Answer
runSPASS SPASSFlags
flags Problem Form
prob
| Bool -> Bool
not (Problem Form -> Bool
forall a. Symbolic a => a -> Bool
isFof Problem Form
prob) = String -> IO Answer
forall a. HasCallStack => String -> a
error String
"runSPASS: SPASS doesn't support many-typed problems"
| Bool
otherwise = do
(ExitCode
_code, String
str) <- String -> [String] -> String -> IO (ExitCode, String)
popen (SPASSFlags -> String
spass SPASSFlags
flags) [String]
spassFlags (Problem Form -> String
showProblem Problem Form
prob)
Answer -> IO Answer
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Answer
extractAnswer String
str)
where
spassFlags :: [String]
spassFlags =
[String
"-TimeLimit=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n | Just Int
n <- [SPASSFlags -> Maybe Int
timeout SPASSFlags
flags] ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[String
"-SOS" | SPASSFlags -> Bool
sos SPASSFlags
flags] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[String
"-TPTP", String
"-Stdin"]
extractAnswer :: String -> Answer
String
result =
[Answer] -> Answer
forall a. [a] -> a
head ([Answer] -> Answer) -> [Answer] -> Answer
forall a b. (a -> b) -> a -> b
$
[ UnsatReason -> Maybe [String] -> Answer
Unsat UnsatReason
Unsatisfiable Maybe [String]
forall a. Maybe a
Nothing | String
"SPASS beiseite: Proof found." <- String -> [String]
lines String
result ] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
[ SatReason -> Maybe [String] -> Answer
Sat SatReason
Satisfiable Maybe [String]
forall a. Maybe a
Nothing | String
"SPASS beiseite: Completion found." <- String -> [String]
lines String
result ] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
[ NoAnswerReason -> Answer
NoAnswer NoAnswerReason
Timeout ]