{- |
Module : ./Propositional/Prove.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.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 Proofs.BatchProcessing
import qualified Logic.Prover as LP
import Interfaces.GenericATPState
import GUI.GenericATP
import Common.IO
import Common.ProofTree
import Common.Utils
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.OrderedMap as OMap
import qualified Common.Result as Result
import Control.Monad (when)
import qualified Control.Concurrent as Concurrent
import Data.List
import Data.Maybe
import Data.Time (TimeOfDay, timeToTimeOfDay, midnight)
import System.Directory
import System.Exit
-- * 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.mkAutomaticProver zchaffS zchaffS top zchaffProveGUI
zchaffProveCMDLautomaticBatch
{- |
The Consistency Cheker.
-}
PMorphism.Morphism ProofTree
propConsChecker = LP.mkUsableConsChecker zchaffS zchaffS top consCheck
consCheck :: String -> LP.TacticScript
-- ^ free definitions
-> IO (LP.CCStatus ProofTree)
consCheck thName _ tm _ =
case LP.tTarget tm of
LP.Theory sig nSens -> do
let axioms = getAxioms $ snd $ unzip $ OMap.toList nSens
thName_clean = basename thName ++ "_cc.zchaff.dimacs"
dimacsOutput <- PC.showDIMACSProblem (thName ++ "_cc")
sig axioms Nothing
tmpFile <- getTempFile dimacsOutput thName_clean
(exitCode, resultHf, err) <-
executeProcess zchaffS [tmpFile] ""
return $ if exitCode /= ExitSuccess then LP.CCStatus
(ProofTree $ (if null err then "" else err ++ "\n")
++ "error by call zchaff " ++ thName)
midnight Nothing
else LP.CCStatus (ProofTree resultHf) midnight
$ searchResult resultHf
where
getAxioms f = map (AS_Anno.makeNamed "consistency" . AS_Anno.sentence)
$ filter AS_Anno.isAxiom f
searchResult :: String -> Maybe Bool
searchResult hf = let ls = lines hf in
if any (isInfixOf reUNSAT) ls then Just False else
if any (isInfixOf reSAT) ls then Just True
else Nothing
-- ** 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 function
{- |
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 []
let thName_clean =
basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".dimacs"
when saveDIMACS (writeFile thName_clean prob)
zFileName <- getTempFile prob thName_clean
(_, zchaffOut, _) <- executeProcess zchaffS
(zFileName : createZchaffOptions cfg) ""
(res, usedAxs, tUsed) <- analyzeZchaff zchaffOut pState
let defaultProofStatus =
(LP.openProofStatus (AS_Anno.senAttr nGoal) zchaffS
emptyProofTree)
{LP.tacticScript = LP.TacticScript $ show
ATPTacticScript
{ tsTimeLimit = configTimeLimit cfg
, tsExtraOpts = []} }
(err, retval) = case res of
Right p -> (ATPSuccess,
defaultProofStatus
{LP.goalStatus = p
, LP.usedAxioms = filter
(/= AS_Anno.senAttr nGoal) usedAxs
, LP.proofTree = ProofTree zchaffOut })
Left a -> (a, defaultProofStatus)
catchIOException () $ removeFile zFileName
return (err, cfg
{ proofStatus = retval
, resultOutput = [zchaffOut]
, timeUsed = tUsed })
-- | analysis of output
analyzeZchaff :: String -> PState.PropProverState
-> IO (Either ATPRetval LP.GoalStatus, [String], TimeOfDay)
analyzeZchaff str' pState =
let unsat = isInfixOf reUNSAT str'
sat = isInfixOf reSAT str'
timeLine = fromMaybe "0" $ stripPrefix reTIME str'
timeout = isInfixOf reEndto str' || isInfixOf reEndmo str'
time = calculateTime timeLine
usedAx = map AS_Anno.senAttr $ PState.initialAxioms pState
in return (case () of
_ | timeout -> Left ATPTLimitExceeded
_ | sat && not unsat -> Right LP.Disproved
_ | not sat && unsat -> Right $ LP.Proved True
_ -> Left $ ATPError "Internal error.", usedAx, time)
-- | Calculated the time need for the proof in seconds
calculateTime :: String -> TimeOfDay
calculateTime timeLine =
timeToTimeOfDay $ realToFrac (fromMaybe
(error $ "calculateTime " ++ timeLine) $ readMaybe timeLine
:: Double)
reUNSAT :: String
reUNSAT = "RESULT:\tUNSAT"
reSAT :: String
reSAT = "RESULT:\tSAT"
reTIME :: String
reTIME = "Total Run Time"
reEndto :: String
reEndto = "TIME OUT"
reEndmo :: String
reEndmo = "MEM OUT"
{- |
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]