Prove.hs revision c3f7e132e0c214b755c6c4b485f4748c4dd1595c
{- |
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@informatik.uni-bremen.de
Stability : experimental
Portability : portable
This is the connection of the SAT-Solver minisat to Hets
-}
module Propositional.Prove
(
zchaffProver, -- the zChaff II Prover
propConsChecker
)
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 Propositional.ChildMessage
import Proofs.BatchProcessing
import qualified Logic.Prover as LP
import Interfaces.GenericATPState
import GUI.GenericATP
import GUI.Utils (infoDialog)
import Common.UniUtils as CP
import Common.ProofTree
import Common.Utils (readMaybe)
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import qualified Common.OrderedMap as OMap
import qualified Common.Result as Result
import Control.Monad (when)
import qualified Control.Concurrent as Concurrent
import qualified Common.Exception as Exception
import Data.List
import Data.Maybe
import Data.Time (TimeOfDay,timeToTimeOfDay)
import System.Directory
import System.Cmd
import System.Exit
import System.IO
-- * Prover implementation
zchaffHelpText :: String
zchaffHelpText = "Zchaff is a very fast SAT-Solver \n"++
"No additional Options are available"++
"for it!"
-- | the name of the prover
zchaffS :: String
zchaffS = "zchaff"
{- |
The Prover implementation.
Implemented are: a prover GUI, and both commandline prover interfaces.
-}
zchaffProver
zchaffProver = (LP.mkProverTemplate zchaffS top zchaffProveGUI)
{ LP.proveCMDLautomatic = Just $ zchaffProveCMDLautomatic
, LP.proveCMDLautomaticBatch = Just $ zchaffProveCMDLautomaticBatch }
{- |
The Consistency Cheker.
-}
PMorphism.Morphism ProofTree
propConsChecker = LP.mkProverTemplate zchaffS top consCheck
PMorphism.Morphism ProofTree
-- ^ free definitions
-> IO([LP.ProofStatus ProofTree])
consCheck thName tm _ =
case LP.tTarget tm of
LP.Theory sig nSens -> do
let axioms = getAxioms $ snd $ unzip $ OMap.toList nSens
thName_clean = map (\c -> if c == '/' then '_' else c) thName
tmpFile = "/tmp/" ++ (thName_clean ++ "_cc.dimacs")
resultFile = tmpFile ++ ".result"
dimacsOutput <- PC.ioDIMACSProblem (thName ++ "_cc")
sig ( [(AS_Anno.makeNamed "myAxioms" $
(
(map (AS_Anno.sentence) axioms)
)
)
{
AS_Anno.isAxiom = True
, AS_Anno.isDef = False
, AS_Anno.wasTheorem = False
}
]
)[]
outputHf <- openFile tmpFile ReadWriteMode
hPutStr outputHf dimacsOutput
hClose outputHf
exitCode <- system ("zchaff " ++ tmpFile ++ " >> " ++ resultFile)
removeFile tmpFile
if exitCode /= ExitSuccess then
infoDialog "consistency checker"
("error by call zchaff " ++ thName)
else do
resultHf <- openFile resultFile ReadMode
isSAT <- searchResult resultHf
hClose resultHf
removeFile resultFile
if isSAT then
infoDialog "consistency checker"
("consistent.")
else
infoDialog "consistency checker"
("inconsistent.")
return []
where
getAxioms f = map (AS_Anno.makeNamed "consistency" . AS_Anno.sentence)
$ filter AS_Anno.isAxiom f
searchResult :: Handle -> IO Bool
searchResult hf = do
eof <- hIsEOF hf
if eof then
return False
else
do
line <- hGetLine hf
putStrLn line
if line == "RESULT:\tUNSAT" then
return True
else if line == "RESULT:\tSAT" then
return False
else searchResult hf
-- ** GUI
{- |
Invokes the generic prover GUI.
-}
zchaffProveGUI :: String -- ^ theory name
-- ^ free definitions
-> IO([LP.ProofStatus ProofTree]) -- ^ proof status for each goal
zchaffProveGUI thName th freedefs =
genericATPgui (atpFun thName) True (LP.proverName zchaffProver) thName th
freedefs emptyProofTree
{- |
Parses a given default tactic script into a
'Interfaces.GenericATPState.ATPTacticScript' if possible.
-}
parseZchaffTacticScript :: LP.TacticScript -> ATPTacticScript
parseZchaffTacticScript = parseTacticScript batchTimeLimit []
-- ** 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.TacticScript -- ^ default tactic script
-- ^ theory consisting of a signature and a list of Named sentence
-- ^ free definitions
-> IO (Result.Result ([LP.ProofStatus ProofTree]))
-- ^ Proof status for goals and lemmas
zchaffProveCMDLautomatic thName defTS th freedefs =
genericCMDLautomatic (atpFun thName) (LP.proverName zchaffProver) thName
(parseZchaffTacticScript defTS) th freedefs emptyProofTree
{- |
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.TacticScript -- ^ default tactic script
-- ^ theory consisting of a signature and a list of Named sentences
-- ^ free definitions
-> 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 freedefs =
genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
resultMVar (LP.proverName zchaffProver) thName
(parseZchaffTacticScript defTS) th freedefs emptyProofTree
{- |
Record for prover specific functions. This is used by both GUI and command
line interface.
-}
atpFun :: String -- Theory name
atpFun thName = ATPFunctions
{ initialProverState = PState.propProverState
, goalOutput = Cons.goalDIMACSProblem thName
, atpTransSenName = PState.transSenName
, atpInsertSentence = PState.insertSentence
, proverHelpText = zchaffHelpText
, runProver = runZchaff
, batchTimeEnv = "HETS_ZCHAFF_BATCH_TIME_LIMIT"
, fileExtensions = FileExtensions
{ problemOutput = ".dimacs"
, proverOutput = ".zchaff"
, theoryConfiguration = ".czchaff"}
, 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
-> GenericConfig ProofTree
-- configuration to use
-> Bool
-- True means save DIMACS file
-> String
-- Name of the theory
-- Goal to prove
-> IO (ATPRetval
, GenericConfig ProofTree
)
-- (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.senAttr nGoal++".dimacs")
prob)
(writeFile (zFileName)
prob)
zchaff <- newChildProcess "zchaff" [CP.arguments allOptions]
Exception.catch (runZchaffReal zchaff)
(\ excep -> do
-- kill zchaff process
destroy zchaff
_ <- waitForChildProcess zchaff
deleteJunk
excepToATPResult (LP.proverName zchaffProver) nGoal excep)
where
deleteJunk = do
catch (removeFile zFileName) (const $ return ())
catch (removeFile "resolve_trace") (const $ return ())
zFileName = "/tmp/problem_"++thName++'_':AS_Anno.senAttr nGoal++".dimacs"
allOptions = zFileName : (createZchaffOptions cfg)
runZchaffReal zchaff =
do
zchaffOut <- parseIt zchaff isEnd
(res, usedAxs, output, tUsed) <- analyzeZchaff zchaffOut pState
let (err, retval) = proofStat res usedAxs [] (head output)
deleteJunk
return (err,
cfg{proofStatus = retval,
resultOutput = output,
timeUsed = tUsed})
where
proofStat res usedAxs options out
| isJust res && elem (fromJust res) proved =
(ATPSuccess,
(defaultProofStatus options)
{LP.goalStatus = LP.Proved $ Nothing
, LP.usedAxioms = filter
(/= AS_Anno.senAttr nGoal) usedAxs
, LP.proofTree = ProofTree $ out })
| isJust res && elem (fromJust res) disproved =
(ATPSuccess,
(defaultProofStatus options)
{LP.goalStatus = LP.Disproved} )
| isJust res && elem (fromJust res) timelimit =
(ATPTLimitExceeded, defaultProofStatus options)
| isNothing res =
(ATPError "Internal error.",
defaultProofStatus options)
| otherwise = (ATPSuccess,
defaultProofStatus options)
defaultProofStatus opts =
(LP.openProofStatus (AS_Anno.senAttr nGoal)
(LP.proverName zchaffProver)
emptyProofTree)
{LP.tacticScript = LP.TacticScript $ show
$ ATPTacticScript
{ tsTimeLimit = configTimeLimit cfg
, tsExtraOpts = 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], TimeOfDay)
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 = isInfixOf re_UNSAT str'
sat = isInfixOf re_SAT str'
timeLine = if isPrefixOf re_TIME str' then
drop (length re_TIME) str' else "0"
timeout = isInfixOf re_end_to str' || isInfixOf re_end_mo str'
time = calculateTime timeLine
usedAx = map (AS_Anno.senAttr) $ PState.initialAxioms pState
in
if timeout
then
return (Just $ head timelimit, usedAx, output, time)
else
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 -> TimeOfDay
calculateTime timeLine =
timeToTimeOfDay $ realToFrac $ (maybe
(error $ "calculateTime " ++ timeLine) id $ readMaybe timeLine
:: Double)
re_UNSAT :: String
re_UNSAT = "RESULT:UNSAT"
re_SAT :: String
re_SAT = "RESULT:SAT"
re_TIME :: String
re_TIME = "Total Run Time"
-- | We are searching for Flotter needed to determine the end of input
isEnd :: String -> Bool
isEnd inS = any (`isInfixOf` inS) [re_end, re_end_to, re_end_mo]
re_end :: String
re_end = "RESULT:"
re_end_to :: String
re_end_to = "TIME OUT"
re_end_mo :: String
re_end_mo = "MEM OUT"
-- | Converts a thrown exception into an ATP result (ATPRetval and proof tree).
excepToATPResult :: String
-- ^ name of running prover
-- ^ goal to prove
-- ^ occured exception
-> IO (ATPRetval,
GenericConfig ProofTree)
-- ^ (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
(ATPError ("Internal error communicating with " ++
prName ++ ".\n"
++ show e), emptyCfg)
(ATPBatchStopped, emptyCfg)
_ -> (ATPError ("Error running " ++ prName ++ ".\n"
++ show excep),
emptyCfg)
where
emptyCfg = emptyConfig prName (AS_Anno.senAttr nGoal)
emptyProofTree
{- |
Creates a list of all options the zChaff prover runs with.
Only Option is the timelimit
-}
createZchaffOptions :: GenericConfig ProofTree -> [String]
createZchaffOptions cfg =
[show $ configTimeLimit cfg]