{-# 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
extractAnswer :: String -> Answer
extractAnswer 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 ]