{-# LANGUAGE RecordWildCards, CPP, ScopedTypeVariables #-}
module Jukebox.Toolbox where
import Jukebox.Options
import Jukebox.Form
import Jukebox.Name
import Jukebox.TPTP.Print
import Control.Monad
import Jukebox.TPTP.Parse
import Jukebox.Tools.Clausify hiding (run)
import Jukebox.Tools.AnalyseMonotonicity hiding (guards)
import Jukebox.Tools.EncodeTypes
import Jukebox.Tools.GuessModel
import Jukebox.Tools.InferTypes
import Jukebox.Tools.HornToUnit
import System.Exit
import System.IO
import Control.Exception
import Jukebox.TPTP.FindFile
import qualified Data.Map.Strict as Map
import qualified Jukebox.SMTLIB as SMT
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Data.IORef
import Data.Set(Set)
data GlobalFlags =
GlobalFlags {
GlobalFlags -> Bool
quiet :: Bool }
deriving Int -> GlobalFlags -> ShowS
[GlobalFlags] -> ShowS
GlobalFlags -> String
(Int -> GlobalFlags -> ShowS)
-> (GlobalFlags -> String)
-> ([GlobalFlags] -> ShowS)
-> Show GlobalFlags
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GlobalFlags -> ShowS
showsPrec :: Int -> GlobalFlags -> ShowS
$cshow :: GlobalFlags -> String
show :: GlobalFlags -> String
$cshowList :: [GlobalFlags] -> ShowS
showList :: [GlobalFlags] -> ShowS
Show
globalFlags :: OptionParser GlobalFlags
globalFlags :: OptionParser GlobalFlags
globalFlags =
String -> OptionParser GlobalFlags -> OptionParser GlobalFlags
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Output options" (OptionParser GlobalFlags -> OptionParser GlobalFlags)
-> OptionParser GlobalFlags -> OptionParser GlobalFlags
forall a b. (a -> b) -> a -> b
$
Bool -> GlobalFlags
GlobalFlags (Bool -> GlobalFlags)
-> Annotated [Flag] ParParser Bool -> OptionParser GlobalFlags
forall (f :: * -> *) a b. Functor 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
"quiet"
[String
"Only print essential information."]
Bool
False (Bool -> ArgParser Bool
forall a. a -> Annotated [String] SeqParser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)
data TSTPFlags =
TSTPFlags {
TSTPFlags -> Bool
tstp :: Bool }
deriving Int -> TSTPFlags -> ShowS
[TSTPFlags] -> ShowS
TSTPFlags -> String
(Int -> TSTPFlags -> ShowS)
-> (TSTPFlags -> String)
-> ([TSTPFlags] -> ShowS)
-> Show TSTPFlags
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TSTPFlags -> ShowS
showsPrec :: Int -> TSTPFlags -> ShowS
$cshow :: TSTPFlags -> String
show :: TSTPFlags -> String
$cshowList :: [TSTPFlags] -> ShowS
showList :: [TSTPFlags] -> ShowS
Show
tstpFlags :: OptionParser TSTPFlags
tstpFlags :: OptionParser TSTPFlags
tstpFlags =
String -> OptionParser TSTPFlags -> OptionParser TSTPFlags
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Output options" (OptionParser TSTPFlags -> OptionParser TSTPFlags)
-> OptionParser TSTPFlags -> OptionParser TSTPFlags
forall a b. (a -> b) -> a -> b
$
Bool -> TSTPFlags
TSTPFlags (Bool -> TSTPFlags)
-> Annotated [Flag] ParParser Bool -> OptionParser TSTPFlags
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"tstp"
[String
"Produce TSTP-compatible output (off by default)."]
Bool
False
comment :: String -> IO ()
String
msg = (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String
"% " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
line | String
line <- String -> [String]
lines String
msg]
quietly :: GlobalFlags -> IO () -> IO ()
quietly :: GlobalFlags -> IO () -> IO ()
quietly GlobalFlags
globals IO ()
action = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (GlobalFlags -> Bool
quiet GlobalFlags
globals) IO ()
action
indent :: String -> String
indent :: ShowS
indent String
msg =
[String] -> String
unlines [String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
line | String
line <- String -> [String]
lines String
msg]
(=>>=) :: OptionParser (a -> IO b) -> OptionParser (b -> IO c) -> OptionParser (a -> IO c)
OptionParser (a -> IO b)
f =>>= :: forall a b c.
OptionParser (a -> IO b)
-> OptionParser (b -> IO c) -> OptionParser (a -> IO c)
=>>= OptionParser (b -> IO c)
g = (a -> IO b) -> (b -> IO c) -> a -> IO c
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
(>=>) ((a -> IO b) -> (b -> IO c) -> a -> IO c)
-> OptionParser (a -> IO b)
-> Annotated [Flag] ParParser ((b -> IO c) -> a -> IO c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OptionParser (a -> IO b)
f Annotated [Flag] ParParser ((b -> IO c) -> a -> IO c)
-> OptionParser (b -> IO c)
-> Annotated [Flag] ParParser (a -> IO c)
forall a b.
Annotated [Flag] ParParser (a -> b)
-> Annotated [Flag] ParParser a -> Annotated [Flag] ParParser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> OptionParser (b -> IO c)
g
infixl 1 =>>=
(=>>) :: OptionParser (IO a) -> OptionParser (IO b) -> OptionParser (IO b)
OptionParser (IO a)
x =>> :: forall a b.
OptionParser (IO a) -> OptionParser (IO b) -> OptionParser (IO b)
=>> OptionParser (IO b)
y = IO a -> IO b -> IO b
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>) (IO a -> IO b -> IO b)
-> OptionParser (IO a) -> Annotated [Flag] ParParser (IO b -> IO b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OptionParser (IO a)
x Annotated [Flag] ParParser (IO b -> IO b)
-> OptionParser (IO b) -> OptionParser (IO b)
forall a b.
Annotated [Flag] ParParser (a -> b)
-> Annotated [Flag] ParParser a -> Annotated [Flag] ParParser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> OptionParser (IO b)
y
infixl 1 =>>
forAllFilesBox :: OptionParser ((FilePath -> IO ()) -> IO ())
forAllFilesBox :: OptionParser ((String -> IO ()) -> IO ())
forAllFilesBox = [String] -> (String -> IO ()) -> IO ()
forAllFiles ([String] -> (String -> IO ()) -> IO ())
-> Annotated [Flag] ParParser [String]
-> OptionParser ((String -> IO ()) -> IO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser [String]
filenames
forAllFiles :: [FilePath] -> (FilePath -> IO ()) -> IO ()
forAllFiles :: [String] -> (String -> IO ()) -> IO ()
forAllFiles [String]
xs String -> IO ()
f = (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
f [String]
xs
readTPTPFileBox :: OptionParser (FilePath -> IO String)
readTPTPFileBox :: OptionParser (String -> IO String)
readTPTPFileBox = [String] -> String -> IO String
readTPTPFile ([String] -> String -> IO String)
-> Annotated [Flag] ParParser [String]
-> OptionParser (String -> IO String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser [String]
findFileFlags
readTPTPFile :: [FilePath] -> FilePath -> IO String
readTPTPFile :: [String] -> String -> IO String
readTPTPFile [String]
dirs String
path = do
Maybe String
mfile <- [String] -> String -> IO (Maybe String)
findFileTPTP [String]
dirs String
path
case Maybe String
mfile of
Maybe String
Nothing -> do
Handle -> String -> IO ()
hPutStrLn Handle
stderr (String
"File '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
path String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' not found")
ExitCode -> IO String
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
Just String
file ->
String -> IO String
readFile String
file IO String -> (IOException -> IO String) -> IO String
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \(IOException
e :: IOException) -> do
Handle -> IOException -> IO ()
forall a. Show a => Handle -> a -> IO ()
hPrint Handle
stderr IOException
e
ExitCode -> IO String
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
readProblemBox :: OptionParser (FilePath -> IO (Problem Form))
readProblemBox :: OptionParser (String -> IO (Problem Form))
readProblemBox = [String] -> String -> IO (Problem Form)
readProblem ([String] -> String -> IO (Problem Form))
-> Annotated [Flag] ParParser [String]
-> OptionParser (String -> IO (Problem Form))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser [String]
findFileFlags
readProblem :: [FilePath] -> FilePath -> IO (Problem Form)
readProblem :: [String] -> String -> IO (Problem Form)
readProblem [String]
dirs String
f = do
Either String (Problem Form)
r <- [String] -> String -> IO (Either String (Problem Form))
parseProblem [String]
dirs String
f
case Either String (Problem Form)
r of
Left String
err -> do
Handle -> String -> IO ()
hPutStrLn Handle
stderr String
err
ExitCode -> IO (Problem Form)
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
Right Problem Form
x -> Problem Form -> IO (Problem Form)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Problem Form
x
printProblemBox :: OptionParser (Problem Form -> IO ())
printProblemBox :: OptionParser (Problem Form -> IO ())
printProblemBox = (Problem Form -> String)
-> (String -> IO ()) -> Problem Form -> IO ()
forall a. (a -> String) -> (String -> IO ()) -> a -> IO ()
prettyPrintIO Problem Form -> String
showProblem ((String -> IO ()) -> Problem Form -> IO ())
-> Annotated [Flag] ParParser (String -> IO ())
-> OptionParser (Problem Form -> IO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser (String -> IO ())
writeFileBox
printProblemSMTBox :: OptionParser (Problem Form -> IO ())
printProblemSMTBox :: OptionParser (Problem Form -> IO ())
printProblemSMTBox = (Problem Form -> String)
-> (String -> IO ()) -> Problem Form -> IO ()
forall a. (a -> String) -> (String -> IO ()) -> a -> IO ()
prettyPrintIO Problem Form -> String
SMT.showProblem ((String -> IO ()) -> Problem Form -> IO ())
-> Annotated [Flag] ParParser (String -> IO ())
-> OptionParser (Problem Form -> IO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser (String -> IO ())
writeFileBox
printClausesBox :: OptionParser (Problem Clause -> IO ())
printClausesBox :: OptionParser (Problem Clause -> IO ())
printClausesBox = (Problem Clause -> String)
-> (String -> IO ()) -> Problem Clause -> IO ()
forall a. (a -> String) -> (String -> IO ()) -> a -> IO ()
prettyPrintIO Problem Clause -> String
showClauses ((String -> IO ()) -> Problem Clause -> IO ())
-> Annotated [Flag] ParParser (String -> IO ())
-> OptionParser (Problem Clause -> IO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser (String -> IO ())
writeFileBox
prettyPrintIO :: (a -> String) -> (String -> IO ()) -> a -> IO ()
prettyPrintIO :: forall a. (a -> String) -> (String -> IO ()) -> a -> IO ()
prettyPrintIO a -> String
shw String -> IO ()
write a
prob = do
String -> IO ()
write (a -> String
shw a
prob String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n")
writeFileBox :: OptionParser (String -> IO ())
writeFileBox :: Annotated [Flag] ParParser (String -> IO ())
writeFileBox =
String
-> Annotated [Flag] ParParser (String -> IO ())
-> Annotated [Flag] ParParser (String -> IO ())
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Output options" (Annotated [Flag] ParParser (String -> IO ())
-> Annotated [Flag] ParParser (String -> IO ()))
-> Annotated [Flag] ParParser (String -> IO ())
-> Annotated [Flag] ParParser (String -> IO ())
forall a b. (a -> b) -> a -> b
$
String
-> [String]
-> (String -> IO ())
-> ArgParser (String -> IO ())
-> Annotated [Flag] ParParser (String -> IO ())
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"output"
[String
"Where to write the output file (stdout by default)."]
String -> IO ()
putStr
((String -> String -> IO ())
-> Annotated [String] SeqParser String
-> ArgParser (String -> IO ())
forall a b.
(a -> b)
-> Annotated [String] SeqParser a -> Annotated [String] SeqParser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String -> IO ()
myWriteFile Annotated [String] SeqParser String
argFile)
where myWriteFile :: String -> String -> IO ()
myWriteFile String
"/dev/null" String
_ = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
myWriteFile String
"-" String
contents = String -> IO ()
putStr String
contents
myWriteFile String
file String
contents = String -> String -> IO ()
writeFile String
file String
contents
clausifyBox :: OptionParser (Problem Form -> IO CNF)
clausifyBox :: OptionParser (Problem Form -> IO CNF)
clausifyBox =
(\ClausifyFlags
flags Problem Form
prob -> CNF -> IO CNF
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CNF -> IO CNF) -> CNF -> IO CNF
forall a b. (a -> b) -> a -> b
$! ClausifyFlags -> Problem Form -> CNF
clausify ClausifyFlags
flags Problem Form
prob) (ClausifyFlags -> Problem Form -> IO CNF)
-> Annotated [Flag] ParParser ClausifyFlags
-> OptionParser (Problem Form -> IO CNF)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser ClausifyFlags
clausifyFlags
oneConjectureBox :: OptionParser (CNF -> IO (Problem Clause))
oneConjectureBox :: OptionParser (CNF -> IO (Problem Clause))
oneConjectureBox = Maybe Int -> CNF -> IO (Problem Clause)
oneConjecture (Maybe Int -> CNF -> IO (Problem Clause))
-> Annotated [Flag] ParParser (Maybe Int)
-> OptionParser (CNF -> IO (Problem Clause))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser (Maybe Int)
flags
where
flags :: Annotated [Flag] ParParser (Maybe Int)
flags =
String
-> Annotated [Flag] ParParser (Maybe Int)
-> Annotated [Flag] ParParser (Maybe Int)
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Input and clausifier options" (Annotated [Flag] ParParser (Maybe Int)
-> Annotated [Flag] ParParser (Maybe Int))
-> Annotated [Flag] ParParser (Maybe Int)
-> Annotated [Flag] ParParser (Maybe Int)
forall a b. (a -> b) -> a -> b
$
String
-> [String]
-> Maybe Int
-> ArgParser (Maybe Int)
-> Annotated [Flag] ParParser (Maybe Int)
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"conjecture"
[String
"If the problem has multiple conjectures, take only this one.",
String
"Conjectures are numbered from 1."]
Maybe Int
forall a. Maybe a
Nothing (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int)
-> Annotated [String] SeqParser Int -> ArgParser (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [String] SeqParser Int
forall a. (Read a, Num a) => ArgParser a
argNum)
oneConjecture :: Maybe Int -> CNF -> IO (Problem Clause)
oneConjecture :: Maybe Int -> CNF -> IO (Problem Clause)
oneConjecture Maybe Int
conj CNF
cnf =
CNF -> (CNF -> NameM (IO (Problem Clause))) -> IO (Problem Clause)
forall a b. Symbolic a => a -> (a -> NameM b) -> b
run CNF
cnf ((CNF -> NameM (IO (Problem Clause))) -> IO (Problem Clause))
-> (CNF -> NameM (IO (Problem Clause))) -> IO (Problem Clause)
forall a b. (a -> b) -> a -> b
$ \(CNF Problem Clause
axioms [Problem Clause]
obligs Maybe [String] -> Answer
_ Maybe [String] -> Answer
_) ->
case Maybe Int
conj of
Just Int
n ->
if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Problem Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Problem Clause]
obligs then Problem Clause -> Problem Clause -> NameM (IO (Problem Clause))
forall {m :: * -> *} {m :: * -> *} {a}.
(Monad m, Monad m) =>
[a] -> [a] -> m (m [a])
choose Problem Clause
axioms ([Problem Clause]
obligs [Problem Clause] -> Int -> Problem Clause
forall a. HasCallStack => [a] -> Int -> a
!! (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
else [String] -> NameM (IO (Problem Clause))
forall {m :: * -> *} {t :: * -> *} {b}.
(Monad m, Foldable t) =>
t String -> m (IO b)
err [String
"Conjecture number out of bounds:",
String
"problem after clausification has " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Problem Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Problem Clause]
obligs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" conjectures"]
Maybe Int
Nothing ->
case [Problem Clause]
obligs of
[Problem Clause
cs] -> Problem Clause -> Problem Clause -> NameM (IO (Problem Clause))
forall {m :: * -> *} {m :: * -> *} {a}.
(Monad m, Monad m) =>
[a] -> [a] -> m (m [a])
choose Problem Clause
axioms Problem Clause
cs
[Problem Clause]
_ ->
[String] -> NameM (IO (Problem Clause))
forall {m :: * -> *} {t :: * -> *} {b}.
(Monad m, Foldable t) =>
t String -> m (IO b)
err [String
"Can't handle more than one conjecture in input problem!",
String
"This problem has " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Problem Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Problem Clause]
obligs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" conjectures.",
String
"Try using the --conjecture flag."]
where
err :: t String -> m (IO b)
err t String
msgs = IO b -> m (IO b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IO b -> m (IO b)) -> IO b -> m (IO b)
forall a b. (a -> b) -> a -> b
$ do
(String -> IO ()) -> t String -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Handle -> String -> IO ()
hPutStrLn Handle
stderr) t String
msgs
ExitCode -> IO b
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
choose :: [a] -> [a] -> m (m [a])
choose [a]
axioms [a]
cs = m [a] -> m (m [a])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([a]
axioms [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
cs))
toFormulasBox :: OptionParser (Problem Clause -> IO (Problem Form))
toFormulasBox :: OptionParser (Problem Clause -> IO (Problem Form))
toFormulasBox = (Problem Clause -> IO (Problem Form))
-> OptionParser (Problem Clause -> IO (Problem Form))
forall a. a -> Annotated [Flag] ParParser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Problem Clause -> IO (Problem Form))
-> OptionParser (Problem Clause -> IO (Problem Form)))
-> (Problem Clause -> IO (Problem Form))
-> OptionParser (Problem Clause -> IO (Problem Form))
forall a b. (a -> b) -> a -> b
$ \Problem Clause
prob -> Problem Form -> IO (Problem Form)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Input Clause -> Input Form) -> Problem Clause -> Problem Form
forall a b. (a -> b) -> [a] -> [b]
map ((Clause -> Form) -> Input Clause -> Input Form
forall a b. (a -> b) -> Input a -> Input b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Form
toForm) Problem Clause
prob)
type Solver = (IO () -> IO ()) -> Problem Clause -> IO Answer
forAllConjecturesBox :: OptionParser (Solver -> CNF -> IO ())
forAllConjecturesBox :: OptionParser (Solver -> CNF -> IO ())
forAllConjecturesBox = TSTPFlags -> Solver -> CNF -> IO ()
forAllConjectures (TSTPFlags -> Solver -> CNF -> IO ())
-> OptionParser TSTPFlags -> OptionParser (Solver -> CNF -> IO ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OptionParser TSTPFlags
tstpFlags
forAllConjectures :: TSTPFlags -> Solver -> CNF -> IO ()
forAllConjectures :: TSTPFlags -> Solver -> CNF -> IO ()
forAllConjectures (TSTPFlags Bool
tstp) Solver
solve CNF{[Problem Clause]
Problem Clause
Maybe [String] -> Answer
axioms :: Problem Clause
conjectures :: [Problem Clause]
satisfiable :: Maybe [String] -> Answer
unsatisfiable :: Maybe [String] -> Answer
axioms :: CNF -> Problem Clause
conjectures :: CNF -> [Problem Clause]
satisfiable :: CNF -> Maybe [String] -> Answer
unsatisfiable :: CNF -> Maybe [String] -> Answer
..} = do
IORef (IO ())
todo <- IO () -> IO (IORef (IO ()))
forall a. a -> IO (IORef a)
newIORef (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
Integer
-> IORef (IO ()) -> [Problem Clause] -> Maybe [String] -> IO ()
forall {t}.
(Show t, Num t) =>
t -> IORef (IO ()) -> [Problem Clause] -> Maybe [String] -> IO ()
loop Integer
1 IORef (IO ())
todo [Problem Clause]
conjectures Maybe [String]
forall a. Maybe a
Nothing
where loop :: t -> IORef (IO ()) -> [Problem Clause] -> Maybe [String] -> IO ()
loop t
_ IORef (IO ())
todo [] Maybe [String]
mref =
IORef (IO ()) -> Answer -> IO ()
forall {a}. IORef (IO a) -> Answer -> IO ()
result IORef (IO ())
todo (Maybe [String] -> Answer
unsatisfiable Maybe [String]
mref)
loop t
i IORef (IO ())
todo (Problem Clause
c:[Problem Clause]
cs) Maybe [String]
_ = do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
multi (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IORef (IO ()) -> IO (IO ())
forall a. IORef a -> IO a
readIORef IORef (IO ())
todo)
IORef (IO ()) -> IO () -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (IO ())
todo (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
Answer
answer <- Solver
solve (\IO ()
x -> IORef (IO ()) -> (IO () -> IO ()) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (IO ())
todo (IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
x)) (Problem Clause
axioms Problem Clause -> Problem Clause -> Problem Clause
forall a. [a] -> [a] -> [a]
++ Problem Clause
c)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
multi (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Partial result (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
part t
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"): " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Answer -> String
forall a. Show a => a -> String
show Answer
answer
String -> IO ()
putStrLn String
""
case Answer
answer of
Sat SatReason
_ Maybe [String]
mmodel -> IORef (IO ()) -> Answer -> IO ()
forall {a}. IORef (IO a) -> Answer -> IO ()
result IORef (IO ())
todo (Maybe [String] -> Answer
satisfiable Maybe [String]
mmodel)
Unsat UnsatReason
_ Maybe [String]
mref -> t -> IORef (IO ()) -> [Problem Clause] -> Maybe [String] -> IO ()
loop (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) IORef (IO ())
todo [Problem Clause]
cs Maybe [String]
mref
NoAnswer NoAnswerReason
x -> IORef (IO ()) -> Answer -> IO ()
forall {a}. IORef (IO a) -> Answer -> IO ()
result IORef (IO ())
todo (NoAnswerReason -> Answer
NoAnswer NoAnswerReason
x)
multi :: Bool
multi = [Problem Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Problem Clause]
conjectures Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
part :: a -> String
part a
i = a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"/" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Problem Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Problem Clause]
conjectures)
result :: IORef (IO a) -> Answer -> IO ()
result IORef (IO a)
todo Answer
x = do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
tstp (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
(String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn (Answer -> [String]
answerSZS Answer
x)
String -> IO ()
putStrLn String
""
IO (IO a) -> IO a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IORef (IO a) -> IO (IO a)
forall a. IORef a -> IO a
readIORef IORef (IO a)
todo)
String -> IO ()
putStrLn (String
"RESULT: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Answer -> String
forall a. Show a => a -> String
show Answer
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Answer -> String
explainAnswer Answer
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
").")
toFofBox :: OptionParser (Problem Form -> IO (Problem Form))
toFofBox :: OptionParser (Problem Form -> IO (Problem Form))
toFofBox = (Problem Form -> IO CNF)
-> Scheme -> Problem Form -> IO (Problem Form)
toFof ((Problem Form -> IO CNF)
-> Scheme -> Problem Form -> IO (Problem Form))
-> OptionParser (Problem Form -> IO CNF)
-> Annotated
[Flag] ParParser (Scheme -> Problem Form -> IO (Problem Form))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OptionParser (Problem Form -> IO CNF)
clausifyBox Annotated
[Flag] ParParser (Scheme -> Problem Form -> IO (Problem Form))
-> Annotated [Flag] ParParser Scheme
-> OptionParser (Problem Form -> IO (Problem Form))
forall a b.
Annotated [Flag] ParParser (a -> b)
-> Annotated [Flag] ParParser a -> Annotated [Flag] ParParser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Annotated [Flag] ParParser Scheme
schemeBox
toFof :: (Problem Form -> IO CNF) -> Scheme -> Problem Form -> IO (Problem Form)
toFof :: (Problem Form -> IO CNF)
-> Scheme -> Problem Form -> IO (Problem Form)
toFof Problem Form -> IO CNF
clausify Scheme
scheme Problem Form
f = do
CNF{[Problem Clause]
Problem Clause
Maybe [String] -> Answer
axioms :: CNF -> Problem Clause
conjectures :: CNF -> [Problem Clause]
satisfiable :: CNF -> Maybe [String] -> Answer
unsatisfiable :: CNF -> Maybe [String] -> Answer
axioms :: Problem Clause
conjectures :: [Problem Clause]
satisfiable :: Maybe [String] -> Answer
unsatisfiable :: Maybe [String] -> Answer
..} <- Problem Form -> IO CNF
clausify Problem Form
f
Map Type (Maybe (Map Function Extension))
m <- [Clause] -> IO (Map Type (Maybe (Map Function Extension)))
monotone ((Input Clause -> Clause) -> Problem Clause -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Input Clause -> Clause
forall a. Input a -> a
what (Problem Clause
axioms Problem Clause -> Problem Clause -> Problem Clause
forall a. [a] -> [a] -> [a]
++ [Problem Clause] -> Problem Clause
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Problem Clause]
conjectures))
let isMonotone :: Type -> Bool
isMonotone Type
ty =
case Type
-> Map Type (Maybe (Map Function Extension))
-> Maybe (Maybe (Map Function Extension))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Type
ty Map Type (Maybe (Map Function Extension))
m of
Just Maybe (Map Function Extension)
Nothing -> Bool
False
Just (Just Map Function Extension
_) -> Bool
True
Maybe (Maybe (Map Function Extension))
Nothing -> Bool
True
Problem Form -> IO (Problem Form)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
translate Scheme
scheme Type -> Bool
isMonotone Problem Form
f)
schemeBox :: OptionParser Scheme
schemeBox :: Annotated [Flag] ParParser Scheme
schemeBox =
String
-> Annotated [Flag] ParParser Scheme
-> Annotated [Flag] ParParser Scheme
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Options for encoding types" (Annotated [Flag] ParParser Scheme
-> Annotated [Flag] ParParser Scheme)
-> Annotated [Flag] ParParser Scheme
-> Annotated [Flag] ParParser Scheme
forall a b. (a -> b) -> a -> b
$
String
-> [String]
-> (Bool -> Scheme)
-> ArgParser (Bool -> Scheme)
-> OptionParser (Bool -> Scheme)
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"encoding"
[String
"Which type encoding to use (guards by default)."]
(Scheme -> Bool -> Scheme
forall a b. a -> b -> a
const Scheme
guards)
([(String, Bool -> Scheme)] -> ArgParser (Bool -> Scheme)
forall a. [(String, a)] -> ArgParser a
argOption
[(String
"guards", Scheme -> Bool -> Scheme
forall a b. a -> b -> a
const Scheme
guards),
(String
"tags", Bool -> Scheme
tags)])
OptionParser (Bool -> Scheme)
-> Annotated [Flag] ParParser Bool
-> Annotated [Flag] ParParser Scheme
forall a b.
Annotated [Flag] ParParser (a -> b)
-> Annotated [Flag] ParParser a -> Annotated [Flag] ParParser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Annotated [Flag] ParParser Bool
tagsFlags
analyseMonotonicityBox :: OptionParser (Problem Clause -> IO (Set Type))
analyseMonotonicityBox :: OptionParser (Problem Clause -> IO (Set Type))
analyseMonotonicityBox = (Problem Clause -> IO (Set Type))
-> OptionParser (Problem Clause -> IO (Set Type))
forall a. a -> Annotated [Flag] ParParser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Problem Clause -> IO (Set Type)
analyseMonotonicity
showMonotonicityBox :: OptionParser (Problem Clause -> IO String)
showMonotonicityBox :: OptionParser (Problem Clause -> IO String)
showMonotonicityBox =
(Problem Clause -> IO String)
-> OptionParser (Problem Clause -> IO String)
forall a. a -> Annotated [Flag] ParParser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Problem Clause -> IO String)
-> OptionParser (Problem Clause -> IO String))
-> (Problem Clause -> IO String)
-> OptionParser (Problem Clause -> IO String)
forall a b. (a -> b) -> a -> b
$ \Problem Clause
cs -> do
Map Type (Maybe (Map Function Extension))
m <- [Clause] -> IO (Map Type (Maybe (Map Function Extension)))
monotone ((Input Clause -> Clause) -> Problem Clause -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Input Clause -> Clause
forall a. Input a -> a
what Problem Clause
cs)
let info :: (a, Maybe (Map a Extension)) -> [String]
info (a
ty, Maybe (Map a Extension)
Nothing) = [a -> String
forall a. Named a => a -> String
base a
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": not monotone"]
info (a
ty, Just Map a Extension
m) =
[a -> String
forall a. Pretty a => a -> String
prettyShow a
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": monotone"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ case Extension
ext of
Extension
CopyExtend -> []
Extension
TrueExtend -> [String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Named a => a -> String
base a
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" true-extended"]
Extension
FalseExtend -> [String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Named a => a -> String
base a
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" false-extended"]
| (a
p, Extension
ext) <- Map a Extension -> [(a, Extension)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a Extension
m ]
String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> String
unlines ([[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (((Type, Maybe (Map Function Extension)) -> [String])
-> [(Type, Maybe (Map Function Extension))] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Maybe (Map Function Extension)) -> [String]
forall {a} {a}.
(Pretty a, Named a, Named a) =>
(a, Maybe (Map a Extension)) -> [String]
info (Map Type (Maybe (Map Function Extension))
-> [(Type, Maybe (Map Function Extension))]
forall k a. Map k a -> [(k, a)]
Map.toList Map Type (Maybe (Map Function Extension))
m))))
guessModelBox :: OptionParser (Problem Form -> IO (Problem Form))
guessModelBox :: OptionParser (Problem Form -> IO (Problem Form))
guessModelBox =
String
-> OptionParser (Problem Form -> IO (Problem Form))
-> OptionParser (Problem Form -> IO (Problem Form))
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Options for the model guesser:" (OptionParser (Problem Form -> IO (Problem Form))
-> OptionParser (Problem Form -> IO (Problem Form)))
-> OptionParser (Problem Form -> IO (Problem Form))
-> OptionParser (Problem Form -> IO (Problem Form))
forall a b. (a -> b) -> a -> b
$
(\[String]
expansive Universe
univ Problem Form
prob -> Problem Form -> IO (Problem Form)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> Universe -> Problem Form -> Problem Form
guessModel [String]
expansive Universe
univ Problem Form
prob))
([String] -> Universe -> Problem Form -> IO (Problem Form))
-> Annotated [Flag] ParParser [String]
-> Annotated
[Flag] ParParser (Universe -> Problem Form -> IO (Problem Form))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser [String]
expansive Annotated
[Flag] ParParser (Universe -> Problem Form -> IO (Problem Form))
-> Annotated [Flag] ParParser Universe
-> OptionParser (Problem Form -> IO (Problem Form))
forall a b.
Annotated [Flag] ParParser (a -> b)
-> Annotated [Flag] ParParser a -> Annotated [Flag] ParParser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Annotated [Flag] ParParser Universe
universe
where universe :: Annotated [Flag] ParParser Universe
universe = String
-> [String]
-> Universe
-> ArgParser Universe
-> Annotated [Flag] ParParser Universe
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"universe"
[String
"Which universe to find the model in (peano by default)."]
Universe
Peano
([(String, Universe)] -> ArgParser Universe
forall a. [(String, a)] -> ArgParser a
argOption [(String
"peano", Universe
Peano), (String
"trees", Universe
Trees)])
expansive :: Annotated [Flag] ParParser [String]
expansive = String
-> [String]
-> Annotated [String] SeqParser String
-> Annotated [Flag] ParParser [String]
forall a. String -> [String] -> ArgParser a -> OptionParser [a]
manyFlags String
"expansive"
[String
"Allow a function to construct 'new' terms in its base case."]
(String
-> String
-> (String -> Maybe String)
-> Annotated [String] SeqParser String
forall a. String -> String -> (String -> Maybe a) -> ArgParser a
arg String
"<function>" String
"expected a function name" String -> Maybe String
forall a. a -> Maybe a
Just)
inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))
inferBox :: OptionParser (Problem Clause -> IO (Problem Clause, Type -> Type))
inferBox = (Problem Clause -> IO (Problem Clause, Type -> Type))
-> OptionParser
(Problem Clause -> IO (Problem Clause, Type -> Type))
forall a. a -> Annotated [Flag] ParParser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\Problem Clause
prob -> (Problem Clause, Type -> Type) -> IO (Problem Clause, Type -> Type)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Problem Clause
-> (Problem Clause -> NameM (Problem Clause, Type -> Type))
-> (Problem Clause, Type -> Type)
forall a b. Symbolic a => a -> (a -> NameM b) -> b
run Problem Clause
prob Problem Clause -> NameM (Problem Clause, Type -> Type)
inferTypes))
printInferredBox :: OptionParser ((Problem Clause, Type -> Type) -> IO (Problem Clause))
printInferredBox :: OptionParser
((Problem Clause, Type -> Type) -> IO (Problem Clause))
printInferredBox = ((Problem Clause, Type -> Type) -> IO (Problem Clause))
-> OptionParser
((Problem Clause, Type -> Type) -> IO (Problem Clause))
forall a. a -> Annotated [Flag] ParParser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((Problem Clause, Type -> Type) -> IO (Problem Clause))
-> OptionParser
((Problem Clause, Type -> Type) -> IO (Problem Clause)))
-> ((Problem Clause, Type -> Type) -> IO (Problem Clause))
-> OptionParser
((Problem Clause, Type -> Type) -> IO (Problem Clause))
forall a b. (a -> b) -> a -> b
$ \(Problem Clause
prob, Type -> Type
rep) -> do
[Type] -> (Type -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Problem Clause -> [Type]
forall a. Symbolic a => a -> [Type]
types Problem Clause
prob) ((Type -> IO ()) -> IO ()) -> (Type -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Type
ty ->
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Type -> String
forall a. Show a => a -> String
show Type
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show (Type -> Type
rep Type
ty)
Problem Clause -> IO (Problem Clause)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Problem Clause
prob
hornToUnitBox :: OptionParser (Problem Clause -> IO (Either Answer (Problem Clause)))
hornToUnitBox :: OptionParser
(Problem Clause -> IO (Either Answer (Problem Clause)))
hornToUnitBox = HornFlags -> Problem Clause -> IO (Either Answer (Problem Clause))
hornToUnitIO (HornFlags
-> Problem Clause -> IO (Either Answer (Problem Clause)))
-> Annotated [Flag] ParParser HornFlags
-> OptionParser
(Problem Clause -> IO (Either Answer (Problem Clause)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Annotated [Flag] ParParser HornFlags
hornFlags
hornToUnitIO :: HornFlags -> Problem Clause -> IO (Either Answer (Problem Clause))
hornToUnitIO :: HornFlags -> Problem Clause -> IO (Either Answer (Problem Clause))
hornToUnitIO HornFlags
flags Problem Clause
prob = do
Either (Input Clause) (Either Answer (Problem Clause))
res <- HornFlags
-> Problem Clause
-> IO (Either (Input Clause) (Either Answer (Problem Clause)))
hornToUnit HornFlags
flags Problem Clause
prob
case Either (Input Clause) (Either Answer (Problem Clause))
res of
Left Input Clause
clause -> do
(String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Handle -> String -> IO ()
hPutStrLn Handle
stderr) [
String
"Expected a Horn problem, but the input file contained",
String
"the following non-Horn clause:",
ShowS
indent (Doc -> String
forall a. Show a => a -> String
show (Problem Clause -> Doc
pPrintClauses [Input Clause
clause])) ]
ExitCode -> IO (Either Answer (Problem Clause))
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
Right Either Answer (Problem Clause)
prob -> Either Answer (Problem Clause)
-> IO (Either Answer (Problem Clause))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Either Answer (Problem Clause)
prob