ProveDepQBF.hs revision e24ad3f655daa60ddabe690e4b11de3187996c16
81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : Interface to the theorem prover e-krhyper in CASC-mode.
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : jonathan.von_schroeder@dfki.de
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : provisional
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederPortability : needs POSIX
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maedersee <http://fmv.jku.at/depqbf/ for more information
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederon the depqbf prover and <http://www.qbflib.org/qdimacs.html>
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederand <http://www.qbflib.org/Draft/qDimacs.ps.gz>
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederfor more information on the qdimacs input format
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule QBF.ProveDepQBF (depQBFProver)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Common.Result as Result
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederimport qualified QBF.AS_BASIC_QBF as AS
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport QBF.Sublogic (QBFSL, top)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport qualified Control.Concurrent as Concurrent
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport System.Exit (ExitCode (..))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Data.Time.LocalTime (TimeOfDay)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaederdepqbfS :: String
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdepqbfS = "depqbf"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | The Prover implementation.
76647324ed70f33b95a881b536d883daccf9568dChristian MaederdepQBFProver :: Prover Sign AS.FORMULA Morphism QBFSL ProofTree
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederdepQBFProver =
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder mkAutomaticProver depqbfS depqbfS top depQBFGUI depQBFCMDLautomaticBatch
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Record for prover specific functions. This is used by both GUI and command
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder line interface.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederatpFun :: String -- ^ theory name
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> ATPFunctions Sign AS.FORMULA Morphism ProofTree QBFProverState
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederatpFun thName = ATPFunctions
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { initialProverState = qbfProverState
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , atpTransSenName = transSenName
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , atpInsertSentence = insertSentence
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , goalOutput = showQDIMACSProblem thName
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , proverHelpText = "for more information visit " ++
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , batchTimeEnv = ""
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , fileExtensions = FileExtensions
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { problemOutput = ".qdimacs"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , proverOutput = "" -- prover doesn't output any files
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , theoryConfiguration = "" -- prover doesn't use any configuration files
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , runProver = runDepQBF
998747cb2ee575cccdd7d865c95d0ef07516a6a5Christian Maeder , createProverOptions = extraOpts }
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder Invokes the generic prover GUI.
07e579405f31fff7f9315685661b5a87cb99c41bChristian MaederdepQBFGUI :: String -- ^ theory name
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> Theory Sign AS.FORMULA ProofTree
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> [FreeDefMorphism AS.FORMULA Morphism] -- ^ freeness constraints
bbcc77a6eb9554dd3092cabafae1e5ca74a054eeChristian Maeder -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdepQBFGUI thName th freedefs =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder genericATPgui (atpFun thName) True (proverName depQBFProver) thName th
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder freedefs emptyProofTree
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder automatic command line interface to the prover.
6b23467258cdc15e05f1845cd400d60ca6eba966Christian MaederdepQBFCMDLautomaticBatch ::
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder Bool -- ^ True means include proved theorems
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -> Bool -- ^ True means save problem file
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- ^ used to store the result of the batch run
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> String -- ^ theory name
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> TacticScript -- ^ default tactic script
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder -> Theory Sign AS.FORMULA ProofTree
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder -> [FreeDefMorphism AS.FORMULA Morphism] -- ^ freeness constraints
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder -> IO (Concurrent.ThreadId, Concurrent.MVar ())
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder {- ^ fst: identifier of the batch thread for killing it
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder snd: MVar to wait for the end of the thread -}
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdepQBFCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder thName defTS th freedefs =
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder resultMVar (proverName depQBFProver) thName
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaederrunDepQBF :: QBFProverState
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder {- ^ logical part containing the input Sign and axioms and possibly
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder goals that have been proved earlier as additional axioms -}
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder -> GenericConfig ProofTree -- ^ configuration to use
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder -> Bool -- ^ True means save QDIMACS file
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder -> String -- ^ name of the theory in the DevGraph
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -> AS_Anno.Named AS.FORMULA -- ^ goal to prove
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -> IO (ATPRetval, GenericConfig ProofTree)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -- ^ (retval, configuration with proof status and complete output)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederrunDepQBF ps cfg saveQDIMACS thName nGoal = do
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder let saveFile = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".qdimacs"
2ca4cb7c4970015237ff434081c2c5bc74284cadChristian Maeder tl = configTimeLimit cfg
2ca4cb7c4970015237ff434081c2c5bc74284cadChristian Maeder prob <- showQDIMACSProblem thName ps nGoal []
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder when saveQDIMACS (writeFile saveFile prob)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder stpTmpFile <- getTempFile prob saveFile
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder t_start <- getHetsTime
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder (exitCode, stdoutC, stderrC) <- executeProcess depqbfS
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder (show tl : extraOpts cfg ++ [stpTmpFile]) ""
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder t_end <- getHetsTime
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder removeFile stpTmpFile
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder let t_u = diffHetsTime t_end t_start
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder exitCode' = case exitCode of
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder ExitSuccess -> 0
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder ExitFailure i -> i
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder (pStat, ret) <- examineProof ps cfg stdoutC stderrC exitCode' nGoal t_u tl
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder return (pStat, cfg
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder { proofStatus = ret
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder , resultOutput = lines (stdoutC ++ stderrC)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder , timeUsed = usedTime ret })
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder-- | examine Prover output
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederexamineProof :: QBFProverState
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -> GenericConfig ProofTree
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> IO (ATPRetval, ProofStatus ProofTree)
61091743da1a9ed6dfd5e077fdcc972553358962Christian MaederexamineProof ps _ stdoutC _ exitCode nGoal tUsed _ =
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder defaultStatus =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ProofStatus { goalName = senAttr nGoal
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder , goalStatus = openGoalStatus
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , usedAxioms = []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , usedProver = proverName depQBFProver
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder , proofTree = emptyProofTree
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , usedTime = tUsed
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , tacticScript = TacticScript "" }
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder getAxioms = map AS_Anno.senAttr (initialAxioms ps)
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder in case getDepQBFResult exitCode stdoutC of
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu DepQBFProved -> return (ATPSuccess, defaultStatus
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder goalStatus = Proved True
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder , usedAxioms = getAxioms
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder DepQBFTimeout -> return (ATPTLimitExceeded, defaultStatus)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder DepQBFDisproved -> return (ATPSuccess, defaultStatus
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder goalStatus = Disproved
405b95208385572f491e1e0207d8d14e31022fa6Christian Maeder , usedAxioms = getAxioms
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu DepQBFError s -> return (ATPError ("Internal Errorr."
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ "\nMessage:\n\n" ++ s)
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder , defaultStatus)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata DepQBFResult = DepQBFProved | DepQBFDisproved
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | DepQBFTimeout | DepQBFError String
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedergetDepQBFResult :: Int -> String -> DepQBFResult
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedergetDepQBFResult exitCode out = case exitCode of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder 10 -> if "SAT" `isPrefixOf` out
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder then DepQBFProved
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else DepQBFError
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder "Unexpected behaviour of prover!"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder 20 -> if "UNSAT" `isPrefixOf` out
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder then DepQBFDisproved
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder else DepQBFError
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder "Unexpected behaviour of prover!"
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder _ -> if "SIGALRM" `isInfixOf` out
4eaf4dc236c387ef179bc7532831a3f15c049baeChristian Maeder then DepQBFTimeout
4eaf4dc236c387ef179bc7532831a3f15c049baeChristian Maeder else DepQBFError
4eaf4dc236c387ef179bc7532831a3f15c049baeChristian Maeder ("Uknown error: " ++ out)