c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederDescription : Interface to the theorem prover e-krhyper in CASC-mode.
430e0468d2abb3424e7ba39f2c3929a3007293afJonathan von SchroederCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
430e0468d2abb3424e7ba39f2c3929a3007293afJonathan von SchroederMaintainer : jonathan.von_schroeder@dfki.de
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederStability : provisional
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederPortability : needs POSIX
430e0468d2abb3424e7ba39f2c3929a3007293afJonathan von Schroedersee <http://fmv.jku.at/depqbf/ for more information
430e0468d2abb3424e7ba39f2c3929a3007293afJonathan von Schroederon the depqbf prover and <http://www.qbflib.org/qdimacs.html>
430e0468d2abb3424e7ba39f2c3929a3007293afJonathan von Schroederand <http://www.qbflib.org/Draft/qDimacs.ps.gz>
430e0468d2abb3424e7ba39f2c3929a3007293afJonathan von Schroederfor more information on the qdimacs input format
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)
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederdepqbfS :: String
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederdepqbfS = "depqbf"
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder-- | The Prover implementation.
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von SchroederdepQBFProver :: Prover Sign AS.FORMULA Morphism QBFSL ProofTree
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederdepQBFProver =
e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder mkAutomaticProver depqbfS depqbfS 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 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)
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian MaederrunDepQBF ps cfg saveQDIMACS thName nGoal = do
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder let saveFile = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".qdimacs"
c56a356d3fcc5e123efa790aab320781d94df3c7Jonathan von Schroeder tl = configTimeLimit cfg
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder prob <- showQDIMACSProblem thName ps nGoal []
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder when saveQDIMACS (writeFile saveFile prob)
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder stpTmpFile <- getTempFile prob saveFile
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder t_start <- getHetsTime
e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder (exitCode, stdoutC, stderrC) <- executeProcess depqbfS
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder (show tl : extraOpts cfg ++ [stpTmpFile]) ""
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder t_end <- getHetsTime
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder removeFile stpTmpFile
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder let t_u = diffHetsTime t_end t_start
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder exitCode' = case exitCode of
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder ExitSuccess -> 0
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder ExitFailure i -> i
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder (pStat, ret) <- examineProof ps cfg stdoutC stderrC exitCode' nGoal t_u tl
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder return (pStat, cfg
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder { proofStatus = ret
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder , resultOutput = lines (stdoutC ++ stderrC)
5b2cef942fa60961cd3fb8e2bfd322a621579a50Christian Maeder , 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 _ =
9bbb7fb64b260b735c08c9499f1ebc45e2bb9520Eugen Kuksa defaultStatus = (openProofStatus
9bbb7fb64b260b735c08c9499f1ebc45e2bb9520Eugen Kuksa (senAttr nGoal)
9bbb7fb64b260b735c08c9499f1ebc45e2bb9520Eugen Kuksa (proverName depQBFProver)
9bbb7fb64b260b735c08c9499f1ebc45e2bb9520Eugen Kuksa (emptyProofTree)) { usedTime = tUsed }
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)