{- |
Module      :  ./Propositional/ProveMinisat.hs
Description :  Provers for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

This is the connection of the SAT-Solver minisat to Hets
-}

module Propositional.ProveMinisat
  ( MiniSatVer (..)
  , minisatProver
  , minisatConsChecker
  ) where

import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import qualified Propositional.Conversions as Cons
import qualified Propositional.Conversions as PC
import qualified Propositional.Morphism as PMorphism
import qualified Propositional.ProverState as PState
import qualified Propositional.Sign as Sig
import Propositional.Sublogic (PropSL, top)

import Proofs.BatchProcessing

import qualified Logic.Prover as LP

import Interfaces.GenericATPState
import GUI.GenericATP

import Common.ProofTree
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.OrderedMap as OMap
import qualified Common.Result as Result
import Common.Utils
import Common.Timing

import Control.Monad (when)
import Control.Concurrent

import Data.Char
import Data.Maybe (fromMaybe)
import Data.Time (timeToTimeOfDay, midnight)
import Data.Time.Clock

import System.Directory
import System.Exit

-- * Prover implementation

minisatHelpText :: String
minisatHelpText :: String
minisatHelpText = "minisat is a very fast SAT-Solver \n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                  "No additional Options are available" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                  "for it!"

data MiniSatVer = Minisat | Minisat2 deriving Int -> MiniSatVer -> String -> String
[MiniSatVer] -> String -> String
MiniSatVer -> String
(Int -> MiniSatVer -> String -> String)
-> (MiniSatVer -> String)
-> ([MiniSatVer] -> String -> String)
-> Show MiniSatVer
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [MiniSatVer] -> String -> String
$cshowList :: [MiniSatVer] -> String -> String
show :: MiniSatVer -> String
$cshow :: MiniSatVer -> String
showsPrec :: Int -> MiniSatVer -> String -> String
$cshowsPrec :: Int -> MiniSatVer -> String -> String
Show

msatName :: MiniSatVer -> String
msatName :: MiniSatVer -> String
msatName = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String)
-> (MiniSatVer -> String) -> MiniSatVer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MiniSatVer -> String
forall a. Show a => a -> String
show

{- |
  The Prover implementation.

  Implemented are: a prover GUI, and both commandline prover interfaces.
-}
minisatProver :: MiniSatVer
  -> LP.Prover Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism PropSL ProofTree
minisatProver :: MiniSatVer -> Prover Sign FORMULA Morphism PropSL ProofTree
minisatProver v :: MiniSatVer
v = String
-> String
-> PropSL
-> (String
    -> Theory Sign FORMULA ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO [ProofStatus ProofTree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory Sign FORMULA ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO (ThreadId, MVar ()))
-> Prover Sign FORMULA Morphism PropSL ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus proof_tree])
    -> String
    -> TacticScript
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
LP.mkAutomaticProver (MiniSatVer -> String
msatName MiniSatVer
v) (MiniSatVer -> String
msatName MiniSatVer
v) PropSL
top
  (MiniSatVer
-> String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO [ProofStatus ProofTree]
minisatProveGUI MiniSatVer
v) ((Bool
  -> Bool
  -> MVar (Result [ProofStatus ProofTree])
  -> String
  -> TacticScript
  -> Theory Sign FORMULA ProofTree
  -> [FreeDefMorphism FORMULA Morphism]
  -> IO (ThreadId, MVar ()))
 -> Prover Sign FORMULA Morphism PropSL ProofTree)
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory Sign FORMULA ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO (ThreadId, MVar ()))
-> Prover Sign FORMULA Morphism PropSL ProofTree
forall a b. (a -> b) -> a -> b
$ MiniSatVer
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (ThreadId, MVar ())
minisatProveCMDLautomaticBatch MiniSatVer
v

{- |
   The Consistency Cheker.
-}
minisatConsChecker :: MiniSatVer
  -> LP.ConsChecker Sig.Sign AS_BASIC.FORMULA PropSL PMorphism.Morphism
     ProofTree
minisatConsChecker :: MiniSatVer -> ConsChecker Sign FORMULA PropSL Morphism ProofTree
minisatConsChecker v :: MiniSatVer
v =
  String
-> String
-> PropSL
-> (String
    -> TacticScript
    -> TheoryMorphism Sign FORMULA Morphism ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign FORMULA PropSL Morphism ProofTree
forall sublogics sign sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
LP.mkUsableConsChecker (MiniSatVer -> String
msatName MiniSatVer
v) (MiniSatVer -> String
msatName MiniSatVer
v) PropSL
top ((String
  -> TacticScript
  -> TheoryMorphism Sign FORMULA Morphism ProofTree
  -> [FreeDefMorphism FORMULA Morphism]
  -> IO (CCStatus ProofTree))
 -> ConsChecker Sign FORMULA PropSL Morphism ProofTree)
-> (String
    -> TacticScript
    -> TheoryMorphism Sign FORMULA Morphism ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign FORMULA PropSL Morphism ProofTree
forall a b. (a -> b) -> a -> b
$ MiniSatVer
-> String
-> TacticScript
-> TheoryMorphism Sign FORMULA Morphism ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (CCStatus ProofTree)
consCheck MiniSatVer
v

consCheck :: MiniSatVer -> String -> LP.TacticScript
  -> LP.TheoryMorphism Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree
  -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]
  -- ^ free definitions
  -> IO (LP.CCStatus ProofTree)
consCheck :: MiniSatVer
-> String
-> TacticScript
-> TheoryMorphism Sign FORMULA Morphism ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (CCStatus ProofTree)
consCheck v :: MiniSatVer
v thName :: String
thName _ tm :: TheoryMorphism Sign FORMULA Morphism ProofTree
tm _ = case TheoryMorphism Sign FORMULA Morphism ProofTree
-> Theory Sign FORMULA ProofTree
forall sign sen mor proof_tree.
TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
LP.tTarget TheoryMorphism Sign FORMULA Morphism ProofTree
tm of
  LP.Theory sig :: Sign
sig nSens :: ThSens FORMULA (ProofStatus ProofTree)
nSens -> do
    let axioms :: [Named FORMULA]
axioms = [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
getAxioms ([SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA])
-> [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
forall a b. (a -> b) -> a -> b
$ ([String], [SenStatus FORMULA (ProofStatus ProofTree)])
-> [SenStatus FORMULA (ProofStatus ProofTree)]
forall a b. (a, b) -> b
snd (([String], [SenStatus FORMULA (ProofStatus ProofTree)])
 -> [SenStatus FORMULA (ProofStatus ProofTree)])
-> ([String], [SenStatus FORMULA (ProofStatus ProofTree)])
-> [SenStatus FORMULA (ProofStatus ProofTree)]
forall a b. (a -> b) -> a -> b
$ [(String, SenStatus FORMULA (ProofStatus ProofTree))]
-> ([String], [SenStatus FORMULA (ProofStatus ProofTree)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(String, SenStatus FORMULA (ProofStatus ProofTree))]
 -> ([String], [SenStatus FORMULA (ProofStatus ProofTree)]))
-> [(String, SenStatus FORMULA (ProofStatus ProofTree))]
-> ([String], [SenStatus FORMULA (ProofStatus ProofTree)])
forall a b. (a -> b) -> a -> b
$ ThSens FORMULA (ProofStatus ProofTree)
-> [(String, SenStatus FORMULA (ProofStatus ProofTree))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens FORMULA (ProofStatus ProofTree)
nSens
        tmpl :: String
tmpl = String -> String
basename String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_cc.minisat.dimacs"
        bin :: String
bin = MiniSatVer -> String
msatName MiniSatVer
v
    String
dimacsOutput <- String
-> Sign -> [Named FORMULA] -> Maybe (Named FORMULA) -> IO String
PC.showDIMACSProblem (String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_cc") Sign
sig
          [Named FORMULA]
axioms Maybe (Named FORMULA)
forall a. Maybe a
Nothing
    String
tmpFile <- String -> String -> IO String
getTempFile String
dimacsOutput String
tmpl
    (exitCode :: ExitCode
exitCode, _, err :: String
err) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
bin [String
tmpFile] ""
    String -> IO ()
removeFile String
tmpFile
    (res :: Maybe Bool
res, out :: String
out) <- case ExitCode
exitCode of
      ExitFailure 10 -> (Maybe Bool, String) -> IO (Maybe Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, "consistent.")
      ExitFailure 20 -> (Maybe Bool, String) -> IO (Maybe Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, "inconsistent.")
      ExitFailure 127 -> (Maybe Bool, String) -> IO (Maybe Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Bool
forall a. Maybe a
Nothing, String
err)
      _ -> (Maybe Bool, String) -> IO (Maybe Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Bool
forall a. Maybe a
Nothing, "error by calling " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bin String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thName)
    CCStatus ProofTree -> IO (CCStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return CCStatus :: forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
LP.CCStatus { ccResult :: Maybe Bool
LP.ccResult = Maybe Bool
res
                       , ccUsedTime :: TimeOfDay
LP.ccUsedTime = TimeOfDay
midnight
                       , ccProofTree :: ProofTree
LP.ccProofTree = String -> ProofTree
ProofTree String
out }
  where
    getAxioms :: [LP.SenStatus AS_BASIC.FORMULA (LP.ProofStatus ProofTree)]
              -> [AS_Anno.Named AS_BASIC.FORMULA]
    getAxioms :: [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
getAxioms = (SenStatus FORMULA (ProofStatus ProofTree) -> Named FORMULA)
-> [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (String -> FORMULA -> Named FORMULA
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed "axn" (FORMULA -> Named FORMULA)
-> (SenStatus FORMULA (ProofStatus ProofTree) -> FORMULA)
-> SenStatus FORMULA (ProofStatus ProofTree)
-> Named FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenStatus FORMULA (ProofStatus ProofTree) -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence)
      ([SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA])
-> ([SenStatus FORMULA (ProofStatus ProofTree)]
    -> [SenStatus FORMULA (ProofStatus ProofTree)])
-> [SenStatus FORMULA (ProofStatus ProofTree)]
-> [Named FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SenStatus FORMULA (ProofStatus ProofTree) -> Bool)
-> [SenStatus FORMULA (ProofStatus ProofTree)]
-> [SenStatus FORMULA (ProofStatus ProofTree)]
forall a. (a -> Bool) -> [a] -> [a]
filter SenStatus FORMULA (ProofStatus ProofTree) -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom

-- ** GUI

{- |
  Invokes the generic prover GUI.
-}

minisatProveGUI :: MiniSatVer -- ^ choosen minisat version
  -> String -- ^ theory name
  -> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree
  -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]
  -- ^ free definitions
  -> IO [LP.ProofStatus ProofTree]
  -- ^ proof status for each goal
minisatProveGUI :: MiniSatVer
-> String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO [ProofStatus ProofTree]
minisatProveGUI v :: MiniSatVer
v thName :: String
thName th :: Theory Sign FORMULA ProofTree
th freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs =
  ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
-> Bool
-> String
-> String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> ProofTree
-> IO [ProofStatus ProofTree]
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui (MiniSatVer
-> String
-> ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
atpFun MiniSatVer
v String
thName) Bool
True (MiniSatVer -> String
msatName MiniSatVer
v) String
thName Theory Sign FORMULA ProofTree
th
                [FreeDefMorphism FORMULA Morphism]
freedefs ProofTree
emptyProofTree
{- |
  Parses a given default tactic script into a
  'Interfaces.GenericATPState.ATPTacticScript' if possible.
-}
parseminisatTacticScript :: LP.TacticScript -> ATPTacticScript
parseminisatTacticScript :: TacticScript -> ATPTacticScript
parseminisatTacticScript = Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit []

-- ** command line function

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the minisat prover.
  minisat specific functions are omitted by data type ATPFunctions.
-}
minisatProveCMDLautomaticBatch :: MiniSatVer
  -> Bool -- ^ True means include proved theorems
  -> Bool -- ^ True means save problem file
  -> MVar (Result.Result [LP.ProofStatus ProofTree])
  -- ^ used to store the result of the batch run
  -> String -- ^ theory name
  -> LP.TacticScript -- ^ default tactic script
  -> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree
  -- ^ theory consisting of a signature and a list of Named sentences
  -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]
  -- ^ free definitions
  -> IO (ThreadId, MVar ())
  {- ^ fst: identifier of the batch thread for killing it
  snd: MVar to wait for the end of the thread -}
minisatProveCMDLautomaticBatch :: MiniSatVer
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (ThreadId, MVar ())
minisatProveCMDLautomaticBatch v :: MiniSatVer
v inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus ProofTree])
resultMVar
                               thName :: String
thName defTS :: TacticScript
defTS th :: Theory Sign FORMULA ProofTree
th freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs =
  ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> ProofTree
-> IO (ThreadId, MVar ())
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> String
-> ATPTacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO (ThreadId, MVar ())
genericCMDLautomaticBatch (MiniSatVer
-> String
-> ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
atpFun MiniSatVer
v String
thName) Bool
inclProvedThs Bool
saveProblem_batch
    MVar (Result [ProofStatus ProofTree])
resultMVar (MiniSatVer -> String
msatName MiniSatVer
v) String
thName
    (TacticScript -> ATPTacticScript
parseminisatTacticScript TacticScript
defTS) Theory Sign FORMULA ProofTree
th [FreeDefMorphism FORMULA Morphism]
freedefs ProofTree
emptyProofTree

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: MiniSatVer
       -> String -- ^ Theory name
       -> ATPFunctions Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree
                       PState.PropProverState
atpFun :: MiniSatVer
-> String
-> ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
atpFun v :: MiniSatVer
v thName :: String
thName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> (String -> String)
-> (pst -> Named sentence -> pst)
-> (pst -> Named sentence -> [String] -> IO String)
-> String
-> String
-> FileExtensions
-> RunProver sentence proof_tree pst
-> (GenericConfig proof_tree -> [String])
-> ATPFunctions sign sentence morphism proof_tree pst
ATPFunctions
                { initialProverState :: InitialProverState Sign FORMULA Morphism PropProverState
initialProverState = InitialProverState Sign FORMULA Morphism PropProverState
PState.propProverState
                , goalOutput :: PropProverState -> Named FORMULA -> [String] -> IO String
goalOutput = String -> PropProverState -> Named FORMULA -> [String] -> IO String
Cons.goalDIMACSProblem String
thName
                , atpTransSenName :: String -> String
atpTransSenName = String -> String
PState.transSenName
                , atpInsertSentence :: PropProverState -> Named FORMULA -> PropProverState
atpInsertSentence = PropProverState -> Named FORMULA -> PropProverState
PState.insertSentence
                , proverHelpText :: String
proverHelpText = String
minisatHelpText
                , runProver :: RunProver FORMULA ProofTree PropProverState
runProver = MiniSatVer -> RunProver FORMULA ProofTree PropProverState
runminisat MiniSatVer
v
                , batchTimeEnv :: String
batchTimeEnv = "HETS_MINISAT_BATCH_TIME_LIMIT"
                , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions
                    { problemOutput :: String
problemOutput = ".dimacs"
                    , proverOutput :: String
proverOutput = ".minisat"
                    , theoryConfiguration :: String
theoryConfiguration = ".cminisat"}
                , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
createminisatOptions }

{- |
  Runs minisat. minisat is assumed to reside in PATH.
-}

runminisat :: MiniSatVer -> PState.PropProverState
           {- logical part containing the input Sign and
           axioms and possibly goals that have been proved
           earlier as additional axioms -}
           -> GenericConfig ProofTree
           -- configuration to use
           -> Bool
           -- True means save DIMACS file
           -> String
           -- Name of the theory
           -> AS_Anno.Named AS_BASIC.FORMULA
           -- Goal to prove
           -> IO (ATPRetval, GenericConfig ProofTree)
           -- (retval, configuration with proof status and complete output)
runminisat :: MiniSatVer -> RunProver FORMULA ProofTree PropProverState
runminisat v :: MiniSatVer
v pState :: PropProverState
pState cfg :: GenericConfig ProofTree
cfg saveDIMACS :: Bool
saveDIMACS thName :: String
thName nGoal :: Named FORMULA
nGoal = do
  String
prob <- String -> PropProverState -> Named FORMULA -> [String] -> IO String
Cons.goalDIMACSProblem String
thName PropProverState
pState Named FORMULA
nGoal []
  let thName_clean :: String
thName_clean = String -> String
basename String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".dimacs"
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveDIMACS (String -> String -> IO ()
writeFile String
thName_clean String
prob)
  String
zFileName <- String -> String -> IO String
getTempFile String
prob String
thName_clean
  String -> Int -> IO (ATPRetval, GenericConfig ProofTree)
runStuff String
zFileName (Int -> IO (ATPRetval, GenericConfig ProofTree))
-> Int -> IO (ATPRetval, GenericConfig ProofTree)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 100 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit GenericConfig ProofTree
cfg
  where
    bin :: String
bin = MiniSatVer -> String
msatName MiniSatVer
v
    defaultProofStatus :: [String] -> ProofStatus ProofTree
defaultProofStatus opts :: [String]
opts =
      (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
LP.openProofStatus (Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal) String
bin
                          ProofTree
emptyProofTree)
      { tacticScript :: TacticScript
LP.tacticScript = String -> TacticScript
LP.TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
        { tsTimeLimit :: Int
tsTimeLimit = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg
        , tsExtraOpts :: [String]
tsExtraOpts = [String]
opts } }
    runStuff :: String -> Int -> IO (ATPRetval, GenericConfig ProofTree)
runStuff zFileName :: String
zFileName t :: Int
t = do
      HetsTime
startTime <- IO HetsTime
getHetsTime
      Maybe (ExitCode, String, String)
mExit <- Int -> String -> [String] -> IO (Maybe (ExitCode, String, String))
timeoutCommand Int
t String
bin [String
zFileName]
      case Maybe (ExitCode, String, String)
mExit of
        Just (exCode :: ExitCode
exCode, out :: String
out, _) -> do
          HetsTime
endTime <- IO HetsTime
getHetsTime
          let usedTime :: TimeOfDay
usedTime = HetsTime -> HetsTime -> TimeOfDay
diffHetsTime HetsTime
endTime HetsTime
startTime
          (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATPRetval, GenericConfig ProofTree)
 -> IO (ATPRetval, GenericConfig ProofTree))
-> (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall a b. (a -> b) -> a -> b
$ case ExitCode
exCode of
            ExitFailure 20 -> (ATPRetval
ATPSuccess, GenericConfig ProofTree
cfg
              { proofStatus :: ProofStatus ProofTree
proofStatus = ([String] -> ProofStatus ProofTree
defaultProofStatus [])
                { goalStatus :: GoalStatus
LP.goalStatus = Bool -> GoalStatus
LP.Proved Bool
True
                , usedAxioms :: [String]
LP.usedAxioms = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal)
                  ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Named FORMULA -> String) -> [Named FORMULA] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr ([Named FORMULA] -> [String]) -> [Named FORMULA] -> [String]
forall a b. (a -> b) -> a -> b
$ PropProverState -> [Named FORMULA]
PState.initialAxioms PropProverState
pState
                , proofTree :: ProofTree
LP.proofTree = String -> ProofTree
ProofTree String
out }
              , timeUsed :: TimeOfDay
timeUsed = TimeOfDay
usedTime })
            ExitFailure 10 -> (ATPRetval
ATPSuccess, GenericConfig ProofTree
cfg
              { proofStatus :: ProofStatus ProofTree
proofStatus = ([String] -> ProofStatus ProofTree
defaultProofStatus [])
                { goalStatus :: GoalStatus
LP.goalStatus = GoalStatus
LP.Disproved
                , proofTree :: ProofTree
LP.proofTree = String -> ProofTree
ProofTree String
out }})
            ExitSuccess -> (ATPRetval
ATPSuccess, GenericConfig ProofTree
cfg
              { proofStatus :: ProofStatus ProofTree
proofStatus = ([String] -> ProofStatus ProofTree
defaultProofStatus [])
                { goalStatus :: GoalStatus
LP.goalStatus = GoalStatus
LP.openGoalStatus
                , proofTree :: ProofTree
LP.proofTree = String -> ProofTree
ProofTree "Unkown"
                , usedTime :: TimeOfDay
LP.usedTime = DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime 0 }})
            _ -> (String -> ATPRetval
ATPError "Internal error.", GenericConfig ProofTree
cfg
              { proofStatus :: ProofStatus ProofTree
proofStatus = [String] -> ProofStatus ProofTree
defaultProofStatus [] })
        Nothing -> (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
ATPTLimitExceeded, GenericConfig ProofTree
cfg
          { proofStatus :: ProofStatus ProofTree
proofStatus = ([String] -> ProofStatus ProofTree
defaultProofStatus [])
            { goalName :: String
LP.goalName = String
thName
            , goalStatus :: GoalStatus
LP.goalStatus = GoalStatus
LP.openGoalStatus
            , usedAxioms :: [String]
LP.usedAxioms = []
            , usedProver :: String
LP.usedProver = String
bin
            , proofTree :: ProofTree
LP.proofTree = String -> ProofTree
ProofTree "Timeout"
            , usedTime :: TimeOfDay
LP.usedTime = DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime 0
            , tacticScript :: TacticScript
LP.tacticScript = String -> TacticScript
LP.TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
              { tsTimeLimit :: Int
tsTimeLimit = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg
              , tsExtraOpts :: [String]
tsExtraOpts = [] } }
          , timeLimitExceeded :: Bool
timeLimitExceeded = Bool
True })

{- |
  Creates a list of all options the minisat prover runs with.
  Only Option is the timelimit
-}
createminisatOptions :: GenericConfig ProofTree -> [String]
createminisatOptions :: GenericConfig ProofTree -> [String]
createminisatOptions cfg :: GenericConfig ProofTree
cfg = [Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg]