ProveDepQBF.hs revision f0cb315452faea6fee8144489629e63e9bd7b303
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederModule : $Header$
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederDescription : Interface to the theorem prover e-krhyper in CASC-mode.
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederCopyright : (c) Dominik Luecke, Uni Bremen 2010
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederMaintainer : luecke@informatik.uni-bremen.de
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederStability : provisional
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederPortability : needs POSIX
2a05acb34d2c8563b403733627a761dadf152f7eChristian Maeder<http://www.uni-koblenz.de/~bpelzer/ekrhyper/>
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederfor details. For the ease of maintenance we are using e-krhyper in
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederits CASC-mode, aka tptp-input. It works for single input files and
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroedermodule QBF.ProveDepQBF (depQBFProver)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport qualified Common.Result as Result
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport Common.AS_Annotation as AS_Anno
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport qualified QBF.AS_BASIC_QBF as AS
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport QBF.Sublogic (QBFSL, top)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport qualified Control.Concurrent as Concurrent
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport System.Exit (ExitCode (..))
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport Data.Time.LocalTime (TimeOfDay)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder-- | The Prover implementation.
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederdepQBFProver :: Prover Sign AS.FORMULA Morphism QBFSL ProofTree
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederdepQBFProver = mkAutomaticProver "depqbf" top depQBFGUI depQBFCMDLautomaticBatch
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder Record for prover specific functions. This is used by both GUI and command
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder line interface.
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederatpFun :: String -- ^ theory name
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> ATPFunctions Sign AS.FORMULA Morphism ProofTree QBFProverState
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederatpFun thName = ATPFunctions
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder { initialProverState = qbfProverState
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , atpTransSenName = transSenName
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , atpInsertSentence = insertSentence
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , goalOutput = showQDIMACSProblem thName
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , proverHelpText = "for more information visit " ++
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , batchTimeEnv = ""
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , fileExtensions = FileExtensions
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder { problemOutput = ".qdimacs"
2a05acb34d2c8563b403733627a761dadf152f7eChristian Maeder , proverOutput = "" -- prover doesn't output any files
2a05acb34d2c8563b403733627a761dadf152f7eChristian Maeder , theoryConfiguration = "" -- prover doesn't use any configuration files
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , runProver = runDepQBF
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , createProverOptions = extraOpts }
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder Invokes the generic prover GUI.
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederdepQBFGUI :: String -- ^ theory name
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> Theory Sign AS.FORMULA ProofTree
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> [FreeDefMorphism AS.FORMULA Morphism] -- ^ freeness constraints
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederdepQBFGUI thName th freedefs =
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder genericATPgui (atpFun thName) True (proverName depQBFProver) thName th
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder freedefs emptyProofTree
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder automatic command line interface to the prover.
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederdepQBFCMDLautomaticBatch ::
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder Bool -- ^ True means include proved theorems
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> Bool -- ^ True means save problem file
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -- ^ used to store the result of the batch run
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> String -- ^ theory name
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> TacticScript -- ^ default tactic script
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> Theory Sign AS.FORMULA ProofTree
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> [FreeDefMorphism AS.FORMULA Morphism] -- ^ freeness constraints
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> IO (Concurrent.ThreadId, Concurrent.MVar ())
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder {- ^ fst: identifier of the batch thread for killing it
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder snd: MVar to wait for the end of the thread -}
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederdepQBFCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder thName defTS th freedefs =
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder resultMVar (proverName depQBFProver) thName
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederuniteOptions :: [String] -> String
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederuniteOptions = intercalate " "
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederrunDepQBF :: QBFProverState
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder {- ^ logical part containing the input Sign and axioms and possibly
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder goals that have been proved earlier as additional axioms -}
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> GenericConfig ProofTree -- ^ configuration to use
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> Bool -- ^ True means save QDIMACS file
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> String -- ^ name of the theory in the DevGraph
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> AS_Anno.Named AS.FORMULA -- ^ goal to prove
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> IO (ATPRetval, GenericConfig ProofTree)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -- ^ (retval, configuration with proof status and complete output)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederrunDepQBF ps cfg saveQDIMACS thName nGoal =
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder saveFile = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".qdimacs"
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder simpleOptions = uniteOptions $ extraOpts cfg
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder tl = configTimeLimit cfg
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder prob <- showQDIMACSProblem thName ps nGoal []
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder when saveQDIMACS
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder (writeFile (saveFile ++ ".qdimacs") prob)
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder tempDir <- getTemporaryDirectory
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder stpTmpFile <- writeTempFile prob tempDir saveFile
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder let command = "depqbf " ++ show tl ++ " "
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder ++ simpleOptions ++ " " ++ stpTmpFile
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder t_start <- getHetsTime
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder (_, stdouth, stderrh, proch) <- runInteractiveCommand command
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder exitCode <- waitForProcess proch
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder t_end <- getHetsTime
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder removeFile stpTmpFile
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder let t_u = diffHetsTime t_end t_start
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder stdoutC <- hGetContents stdouth
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder stderrC <- hGetContents stderrh
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder let exitCode' = case exitCode of
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder ExitSuccess -> 0
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder ExitFailure i -> i
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder (pStat, ret) <- examineProof ps cfg
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder stdoutC stderrC exitCode' nGoal t_u tl
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder return (pStat, cfg
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder proofStatus = ret
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , resultOutput = lines (stdoutC ++ stderrC)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , timeUsed = usedTime ret
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder-- | examine Prover output
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederexamineProof :: QBFProverState
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> GenericConfig ProofTree
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> IO (ATPRetval, ProofStatus ProofTree)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederexamineProof ps _ stdoutC _ exitCode nGoal tUsed _ =
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder defaultStatus =
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder ProofStatus { goalName = senAttr nGoal
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , goalStatus = openGoalStatus
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , usedAxioms = []
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , usedProver = proverName depQBFProver
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , proofTree = emptyProofTree
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , usedTime = tUsed
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , tacticScript = TacticScript "" }
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder getAxioms = map AS_Anno.senAttr (initialAxioms ps)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder in case getDepQBFResult exitCode stdoutC of
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder DepQBFProved -> return (ATPSuccess, defaultStatus
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder goalStatus = Proved True
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , usedAxioms = getAxioms
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder DepQBFTimeout -> return (ATPTLimitExceeded, defaultStatus)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder DepQBFDisproved -> return (ATPSuccess, defaultStatus
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder goalStatus = Disproved
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , usedAxioms = getAxioms
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder DepQBFError s -> return (ATPError ("Internal Errorr."
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder ++ "\nMessage:\n\n" ++ s)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , defaultStatus)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederdata DepQBFResult = DepQBFProved | DepQBFDisproved
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder | DepQBFTimeout | DepQBFError String
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroedergetDepQBFResult :: Int -> String -> DepQBFResult
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroedergetDepQBFResult exitCode out = case exitCode of
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder 10 -> if "SAT" `isPrefixOf` out
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder then DepQBFProved
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder else DepQBFError
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder "Unexpected behaviour of prover!"
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder 20 -> if "UNSAT" `isPrefixOf` out
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder then DepQBFDisproved
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder else DepQBFError
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder "Unexpected behaviour of prover!"
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder _ -> if "SIGALRM" `isInfixOf` out
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder then DepQBFTimeout
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder else DepQBFError
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder ("Uknown error: " ++ out)