Prove.hs revision 92cbfd9dd91a44fd1eb2c7767dbb2138fa36bff9
{- |
Module : $Header$
Description : Provers for propositional logic
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : luecke@tzi.de
Stability : experimental
Portability : portable
This is the connection of the SAT-Solver minisat to Hets
-}
module Propositional.Prove
(
zchaffProver -- the zChaff II Prover
)
where
import qualified Logic.Prover as LP
import qualified Propositional.Sign as Sig
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import qualified Propositional.ProverState as PState
import qualified GUI.GenericATPState as ATPState
import qualified Propositional.Conversions as Cons
import qualified Common.AS_Annotation as AS_Anno
import Proofs.BatchProcessing
import qualified Common.Result as Result
import qualified Control.Exception as Exception
import GHC.Read (readEither)
import qualified Control.Concurrent as Concurrent
import Char
import Data.Maybe
import Data.List
import System
import Directory
import ChildProcess
import ProcessClasses
import Text.Regex
import HTk
import GUI.GenericATP
-- * Prover implementation
zchaffHelpText :: String
zchaffHelpText = "Zchaff is a very fast SAT-Solver \n"++
"No additional Options are available"++
"for it!"
{- |
The Prover implementation.
Implemented are: a prover GUI, and both commandline prover interfaces.
-}
zchaffProver = LP.emptyProverTemplate
{
LP.prover_name = "zchaff"
, LP.prover_sublogic = "Prop"
, LP.proveGUI = Just $ zchaffProveGUI
, LP.proveCMDLautomatic = Just $ zchaffProveCMDLautomatic
, LP.proveCMDLautomaticBatch = Just $ zchaffProveCMDLautomaticBatch
}
-- ** GUI
{- |
Invokes the generic prover GUI.
-}
zchaffProveGUI :: String -- ^ theory name
-> IO([LP.Proof_status Sig.ATP_ProofTree]) -- ^ proof status for each goal
zchaffProveGUI thName th =
genericATPgui (atpFun thName) True (LP.prover_name zchaffProver) thName th
$ Sig.ATP_ProofTree ""
{- |
Parses a given default tactic script into a
'GUI.GenericATPState.ATPTactic_script' if possible.
-}
parseZchaffTactic_script :: LP.Tactic_script
parseZchaffTactic_script =
parseTactic_script batchTimeLimit
{- |
Parses a given default tactic script into a
'GUI.GenericATPState.ATPTactic_script' if possible. Otherwise a default
prover's tactic script is returned.
-}
parseTactic_script :: Int -- ^ default time limit (standard:
parseTactic_script tLimit (LP.Tactic_script ts) =
either (\_ -> ATPState.ATPTactic_script { ATPState.ts_timeLimit = tLimit,
ATPState.ts_extraOpts = [] })
id
(readEither ts :: Either String ATPState.ATPTactic_script)
-- ** command line functions
{- |
Implementation of 'Logic.Prover.proveCMDLautomatic' which provides an
automatic command line interface for a single goal.
SPASS specific functions are omitted by data type ATPFunctions.
-}
zchaffProveCMDLautomatic ::
String -- ^ theory name
-> LP.Tactic_script -- ^ default tactic script
-- signature and a list of Named sentence
-- ^ Proof status for goals and lemmas
zchaffProveCMDLautomatic thName defTS th =
genericCMDLautomatic (atpFun thName) (LP.prover_name zchaffProver) thName
(parseZchaffTactic_script defTS) th (Sig.ATP_ProofTree "")
{- |
Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
automatic command line interface to the zchaff prover.
zchaff specific functions are omitted by data type ATPFunctions.
-}
zchaffProveCMDLautomaticBatch ::
Bool -- ^ True means include proved theorems
-> Bool -- ^ True means save problem file
-- ^ used to store the result of the batch run
-> String -- ^ theory name
-> LP.Tactic_script -- ^ default tactic script
-- 'SPASS.Sign.Sign' and a list of Named 'SPASS.Sign.Sentence'
-> IO (Concurrent.ThreadId,Concurrent.MVar ())
-- ^ fst: identifier of the batch thread for killing it
-- snd: MVar to wait for the end of the thread
zchaffProveCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
thName defTS th =
genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
resultMVar (LP.prover_name zchaffProver) thName
(parseZchaffTactic_script defTS) th (Sig.ATP_ProofTree "")
{- |
Record for prover specific functions. This is used by both GUI and command
line interface.
-}
atpFun :: String -- Theory name
atpFun thName = ATPState.ATPFunctions
{
, ATPState.goalOutput = Cons.goalDIMACSProblem thName
, ATPState.proverHelpText = zchaffHelpText
, ATPState.runProver = runZchaff
, ATPState.batchTimeEnv = "HETS_ZCHAFF_BATCH_TIME_LIMIT"
ATPState.proverOutput = ".zchaff",
ATPState.theoryConfiguration = ".czchaff"}
, ATPState.createProverOptions = createZchaffOptions
}
{- |
Runs zchaff. zchaff is assumed to reside in PATH.
-}
runZchaff :: PState.PropProverState
-- logical part containing the input Sign and
-- axioms and possibly goals that have been proved
-- earlier as additional axioms
-- configuration to use
-> Bool
-- True means save DIMACS file
-> String
-- Name of the theory
-- Goal to prove
-> IO (ATPState.ATPRetval
)
-- (retval, configuration with proof status and complete output)
runZchaff pState cfg saveDIMACS thName nGoal =
do
prob <- Cons.goalDIMACSProblem thName pState nGoal []
when saveDIMACS
(writeFile (thName++'_':AS_Anno.senName nGoal++".dimacs")
prob)
(writeFile (zFileName)
prob)
zchaff <- newChildProcess "zchaff" [ChildProcess.arguments allOptions]
Exception.catch (runZchaffReal zchaff)
(\ excep -> do
-- kill zchaff process
destroy zchaff
_ <- waitForChildProcess zchaff
removeFile (zFileName)
excepToATPResult (LP.prover_name zchaffProver) nGoal excep)
where
zFileName = "/tmp/problem_"++thName++'_':AS_Anno.senName nGoal++".dimacs"
allOptions = zFileName : (createZchaffOptions cfg)
runZchaffReal zchaff =
do
e <- getToolStatus zchaff
if isJust e
then
do
removeFile (zFileName)
return
(ATPState.ATPError "Could not start zchaff. Is zchaff in your $PATH?",
ATPState.emptyConfig (LP.prover_name zchaffProver)
(AS_Anno.senName nGoal) $ Sig.ATP_ProofTree "")
else do
zchaffOut <- parseProtected zchaff
(res, usedAxs, output, tUsed) <- analyzeZchaff zchaffOut pState
let (err, retval) = proof_stat res usedAxs [] (head output)
removeFile (zFileName)
return (err,
cfg{ATPState.proof_status = retval,
ATPState.resultOutput = output,
ATPState.timeUsed = tUsed})
where
proof_stat res usedAxs options out
| isJust res && elem (fromJust res) proved =
(defaultProof_status options)
{LP.goalStatus = LP.Proved $ Nothing
, LP.usedAxioms = filter (/=(AS_Anno.senName nGoal)) usedAxs
, LP.proofTree = Sig.ATP_ProofTree $ out })
| isJust res && elem (fromJust res) disproved =
(defaultProof_status options) {LP.goalStatus = LP.Disproved} )
| isJust res && elem (fromJust res) timelimit =
(ATPState.ATPTLimitExceeded, defaultProof_status options)
| isNothing res =
(ATPState.ATPError "Internal error.", defaultProof_status options)
| otherwise = (ATPState.ATPSuccess, defaultProof_status options)
defaultProof_status opts =
{ATPState.ts_timeLimit = configTimeLimit cfg,
ATPState.ts_extraOpts = opts} }
proved :: [String]
proved = ["Proof found."]
disproved :: [String]
disproved = ["Completion found."]
timelimit :: [String]
timelimit = ["Ran out of time."]
-- | analysis of output
analyzeZchaff :: String
-> IO (Maybe String, [String], [String], Int)
analyzeZchaff str pState =
let
str' = foldr (\ch li -> if ch == '\x9'
then ""++li
else ch:li) "" str
str2 = foldr (\ch li -> if ch == '\x9'
then " "++li
else ch:li) "" str
output = [str2]
unsat = (\xv ->
case xv of
Just _ -> True
Nothing -> False
) $ matchRegex re_UNSAT str'
sat = (\xv ->
case xv of
Just _ -> True
Nothing -> False
) $ matchRegex re_SAT str'
timeLine = (\xv ->
case xv of
Just yv -> head yv
Nothing -> "Total Run Time0"
) $ matchRegex re_TIME str'
time = calculateTime timeLine
usedAx = map (AS_Anno.senAttr) $ PState.initialAxioms pState
in
if (sat && (not unsat))
then
return (Just $ head $ disproved, usedAx, output, time)
else if ((not sat) && unsat)
then
return (Just $ head $ proved, usedAx, output, time)
else
do
return (Nothing, usedAx, output, time)
-- | Calculated the time need for the proof in seconds
calculateTime :: String -> Int
calculateTime timeLine =
let
inAr = reverse $ map digitToInt $
subRegex re_SUBPOINT
(subRegex re_SUBTIME timeLine "") ""
in
calculateHelp inAr 0
where
calculateHelp (inI:inArx) pot =
inI * (10^0) + calculateHelp inArx (pot + 1)
calculateHelp [] _ = 0
re_UNSAT :: Regex
re_UNSAT = mkRegex "(.*)RESULT:UNSAT(.*)"
re_SAT :: Regex
re_SAT = mkRegex "(.*)RESULT:SAT(.*)"
re_TIME :: Regex
re_TIME = mkRegex "Total Run Time(.*)"
re_SUBTIME :: Regex
re_SUBTIME = mkRegex "Total Run Time"
re_SUBPOINT :: Regex
re_SUBPOINT = mkRegex ".(.*)"
-- | Helper for reading zChaff output
parseProtected :: ChildProcess -> IO String
parseProtected zchaff = do
e <- getToolStatus zchaff
case e of
Nothing ->
do
miniOut <- parseIt zchaff
_ <- waitForChildProcess zchaff
return miniOut
Just (ExitFailure retval) ->
do
_ <- waitForChildProcess zchaff
return ("Error!!! Cause was: " ++ show retval)
Just ExitSuccess ->
do
miniOut <- parseIt zchaff
_ <- waitForChildProcess zchaff
return miniOut
-- | Helper function for parsing zChaff output
parseIt :: ChildProcess -> IO String
parseIt zchaff = do
line <- return ""
msg <- parseItHelp zchaff $ return line
return msg
-- | Helper function for parsing zChaff output
parseItHelp :: ChildProcess -> IO String -> IO String
parseItHelp zchaff inp = do
e <- getToolStatus zchaff
inT <- inp
case e of
Nothing
->
do
line <- readMsg zchaff
case isEnd line of
True ->
return (inT ++ "\n" ++ line)
_ ->
do
parseItHelp zchaff $ return (inT ++ "\n" ++ line)
Just (ExitFailure retval)
-- returned error
-> do
_ <- waitForChildProcess zchaff
return $ "zchaff returned error: "++(show retval)
Just ExitSuccess
-- completed successfully. read remaining output.
->
do
line <- readMsg zchaff
case isEnd line of
True ->
return (inT ++ "\n" ++ line)
_ ->
do
parseItHelp zchaff $ return (inT ++ "\n" ++ line)
-- | We are searching for Flotter needed to determine the end of input
isEnd :: String -> Bool
isEnd inS = (\xv ->
case xv of
Just _ -> True
Nothing -> False
) $ matchRegex re_end inS
re_end :: Regex
re_end = mkRegex "(.*)RESULT:(.*)"
-- | Converts a thrown exception into an ATP result (ATPRetval and proof tree).
excepToATPResult :: String
-- ^ name of running prover
-- ^ goal to prove
-- ^ occured exception
-> IO (ATPState.ATPRetval,
-- ^ (retval,
-- configuration with proof status and complete output)
excepToATPResult prName nGoal excep = return $ case excep of
-- this is supposed to distinguish "fd ... vanished"
-- errors from other exceptions
(ATPState.ATPError ("Internal error communicating with " ++
prName ++ ".\n"
++ show e), emptyCfg)
(ATPState.ATPBatchStopped, emptyCfg)
_ -> (ATPState.ATPError ("Error running " ++ prName ++ ".\n"
++ show excep),
emptyCfg)
where
emptyCfg = ATPState.emptyConfig prName (AS_Anno.senName nGoal) $
{- |
Returns the time limit from GenericConfig if available. Otherwise
guiDefaultTimeLimit is returned.
-}
configTimeLimit :: ATPState.GenericConfig Sig.ATP_ProofTree
-> Int
configTimeLimit cfg =
maybe (guiDefaultTimeLimit) id $ ATPState.timeLimit cfg
{- |
Creates a list of all options the zChaff prover runs with.
Only Option is the timelimit
-}
createZchaffOptions :: ATPState.GenericConfig Sig.ATP_ProofTree -> [String]
createZchaffOptions cfg =
[(show $ configTimeLimit cfg)]