-- Components ("boxes") which can be put together to make tools.
{-# 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)

----------------------------------------------------------------------
-- Some standard flags.

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
showList :: [GlobalFlags] -> ShowS
$cshowList :: [GlobalFlags] -> ShowS
show :: GlobalFlags -> String
$cshow :: GlobalFlags -> String
showsPrec :: Int -> GlobalFlags -> ShowS
$cshowsPrec :: Int -> 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
<$>
    -- Use flag rather than bool to avoid getting a --no-quiet option in the
    -- help message
    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 (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
showList :: [TSTPFlags] -> ShowS
$cshowList :: [TSTPFlags] -> ShowS
show :: TSTPFlags -> String
$cshow :: TSTPFlags -> String
showsPrec :: Int -> TSTPFlags -> ShowS
$cshowsPrec :: Int -> 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

----------------------------------------------------------------------
-- Printing output messages.

-- Print a message as a TPTP comment.
comment :: String -> IO ()
comment :: String -> IO ()
comment 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]

-- Do something only when output is enabled.
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 a piece of text.
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]

----------------------------------------------------------------------
-- Combinators for boxes.

-- Boxes typically have the type OptionParser (a -> IO b).
-- The following two combinators chain boxes together.
(=>>=) :: OptionParser (a -> IO b) -> OptionParser (b -> IO c) -> OptionParser (a -> IO c)
OptionParser (a -> IO b)
f =>>= :: 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) -> OptionParser (a -> IO c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> OptionParser (b -> IO c)
g
infixl 1 =>>= -- same fixity as >=>

(=>>) :: OptionParser (IO a) -> OptionParser (IO b) -> OptionParser (IO b)
OptionParser (IO a)
x =>> :: OptionParser (IO a) -> OptionParser (IO b) -> OptionParser (IO b)
=>> OptionParser (IO b)
y = 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> OptionParser (IO b)
y
infixl 1 =>> -- same fixity as >>

----------------------------------------------------------------------
-- Process all files that were passed in on the command line.

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

----------------------------------------------------------------------
-- Read in a single file without parsing it.

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)

----------------------------------------------------------------------
-- Read in a single problem.

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 (m :: * -> *) a. Monad m => a -> m a
return Problem Form
x

----------------------------------------------------------------------
-- Write output to a file.

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 :: (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 (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 (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

----------------------------------------------------------------------
-- Clausify a problem.

clausifyBox :: OptionParser (Problem Form -> IO CNF)
clausifyBox :: OptionParser (Problem Form -> IO CNF)
clausifyBox =
  (\ClausifyFlags
flags Problem Form
prob -> CNF -> IO CNF
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

----------------------------------------------------------------------
-- Make sure that the problem only has one conjecture.

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 (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. [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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a]
axioms [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
cs))

----------------------------------------------------------------------
-- Turn a set of clauses back into formulas.

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 (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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Form
toForm) Problem Clause
prob)

----------------------------------------------------------------------
-- Solve all conjectures in a problem and report the final SZS status.

-- A solver is given a problem in CNF and should return an answer.
--
-- It is also given a function of type IO () -> IO ().
-- Wrapping an action in this function delays the action until after
-- the answer is printed; this can be useful for e.g. printing a proof
-- when the prover might be running under a timeout.
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
unsatisfiable :: CNF -> Maybe [String] -> Answer
satisfiable :: CNF -> Maybe [String] -> Answer
conjectures :: CNF -> [Problem Clause]
axioms :: CNF -> Problem Clause
unsatisfiable :: Maybe [String] -> Answer
satisfiable :: Maybe [String] -> Answer
conjectures :: [Problem Clause]
axioms :: Problem Clause
..} = do
  IORef (IO ())
todo <- IO () -> IO (IORef (IO ()))
forall a. a -> IO (IORef a)
newIORef (() -> IO ()
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
  -- XXX fix this to properly combine refutations from parts
  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 (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 (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 (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 (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
").")

----------------------------------------------------------------------
-- Convert a problem from TFF to FOF.

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 (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
unsatisfiable :: Maybe [String] -> Answer
satisfiable :: Maybe [String] -> Answer
conjectures :: [Problem Clause]
axioms :: Problem Clause
unsatisfiable :: CNF -> Maybe [String] -> Answer
satisfiable :: CNF -> Maybe [String] -> Answer
conjectures :: CNF -> [Problem Clause]
axioms :: CNF -> Problem Clause
..} <- Problem Form -> IO CNF
clausify Problem Form
f
  -- In some cases we might get better results by considering each
  -- problem (axioms + conjecture) separately, but no big deal.
  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 -- can happen if clausifier removed all clauses about a type
  Problem Form -> IO (Problem Form)
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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Annotated [Flag] ParParser Bool
tagsFlags

----------------------------------------------------------------------
-- Analyse monotonicity.

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 (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 (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 (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))))

----------------------------------------------------------------------
-- Guess an infinite model.

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 (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 (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)

----------------------------------------------------------------------
-- Infer types.

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 (f :: * -> *) a. Applicative f => a -> f a
pure (\Problem Clause
prob -> (Problem Clause, Type -> Type) -> IO (Problem Clause, Type -> Type)
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 (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 (m :: * -> *) a. Monad m => a -> m a
return Problem Clause
prob

----------------------------------------------------------------------
-- Translate Horn problems to unit equality.

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 (m :: * -> *) a. Monad m => a -> m a
return Either Answer (Problem Clause)
prob