ProveDepQBF.hs revision c56a356d3fcc5e123efa790aab320781d94df3c7
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
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederhttp://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 (..))
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport Data.Time (timeToTimeOfDay)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport Data.Time.LocalTime (TimeOfDay (..))
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroederimport Data.Time.Clock (UTCTime (..), secondsToDiffTime, getCurrentTime)
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"
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , proverOutput = "" -- ^ prover doesn't output any files
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder , 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
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -> 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 ())
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -- ^ fst: identifier of the batch thread for killing it
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -- 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
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -- ^ logical part containing the input Sign and axioms and possibly
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder -- 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 =
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder saveFile = thName ++ '_' : AS_Anno.senAttr nGoal
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder tmpFile = reverse (fst $ span (/= '/') $ reverse thName) ++
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)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder t <- getCurrentTime
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder let stpTmpFile = "/tmp/" ++ tmpFile ++ show (utctDay t) ++
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder "-" ++ show (utctDayTime t) ++ ".qdimacs"
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder writeFile stpTmpFile prob
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder let command = "depqbf " ++ show tl ++ " "
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder ++ simpleOptions ++ " " ++ stpTmpFile
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder t_start <- epochTime
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder (_, stdouth, stderrh, proch) <- runInteractiveCommand command
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder exitCode <- waitForProcess proch
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder t_end <- epochTime
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder removeFile stpTmpFile
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder let t_t = (round (realToFrac
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder (t_end - t_start + 1) :: Double) :: Integer)
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder let t_u = timeToTimeOfDay $ secondsToDiffTime $
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)