jukebox 0.1.1 → 0.1.2

raw patch · 2 files changed

+69/−1 lines, 2 files

Files

• Jukebox/Provers/SPASS.hs +67/−0
• jukebox.cabal +2/−1

@@ -0,0 +1,67 @@+{-# LANGUAGE GADTs #-}+module Jukebox.Provers.SPASS where++import Jukebox.Form hiding (tag, Or)+import Jukebox.Name+import Jukebox.Options+import Control.Applicative hiding (Const)+import Control.Monad+import Jukebox.Utils+import Jukebox.TPTP.Parsec+import Jukebox.TPTP.ClauseParser hiding (newFunction, Term)+import Jukebox.TPTP.Print+import Jukebox.TPTP.Lexer hiding (Normal, keyword, Axiom, name, Var)+import Text.PrettyPrint.HughesPJ hiding (parens)+import Data.Maybe+import qualified Data.ByteString.Char8 as BS+import qualified Data.ByteString.Lazy.Char8 as BSL+import qualified Jukebox.Seq as S+import qualified Jukebox.Map as Map+import Jukebox.Map(Map)+import Data.Hashable+import System.Exit++data SPASSFlags =+  SPASSFlags {+    spass   :: String,+    timeout :: Maybe Int,+    sos     :: Bool }++spassFlags =+  inGroup "SPASS prover options" $+  SPASSFlags <$>+    flag "spass"+      ["Path to SPASS.",+       "Default: SPASS"]+      "SPASS"+      argFile <*>+    flag "timeout"+      ["Timeout in seconds.",+       "Default: (none)"]+      Nothing+      (fmap Just argNum) <*>+    flag "sos"+      ["Use set-of-support strategy.",+       "Default: false"]+      False+      (pure True)++runSPASS :: (Pretty a, Symbolic a) => SPASSFlags -> Problem a -> IO Answer+runSPASS flags prob+  | not (isFof (open prob)) = error "runSPASS: SPASS doesn't support many-typed problems"+  | otherwise = do+    (code, str) <- popen (spass flags) spassFlags+                   (BS.pack (render (prettyProblem "cnf" Normal prob)))+    return (extractAnswer (BS.unpack str))+  where+    spassFlags =+      ["-TimeLimit=" ++ show n | Just n <- [timeout flags] ] +++      ["-SOS" | sos flags] +++      ["-TPTP", "-Stdin"]++extractAnswer :: String -> Answer+extractAnswer result =+  head $+    [ Unsatisfiable    | "SPASS beiseite: Proof found." <- lines result ] +++    [ Satisfiable      | "SPASS beiseite: Completion found." <- lines result ] +++    [ NoAnswer Timeout ]

@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.1.1+Version: 0.1.2 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone@@ -38,6 +38,7 @@     Jukebox.Options     Jukebox.ProgressBar     Jukebox.Provers.E+    Jukebox.Provers.SPASS     Jukebox.Sat3     Jukebox.SatEq     Jukebox.Sat