ProveDepQBF.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringModule : $Header$
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringDescription : Interface to the theorem prover e-krhyper in CASC-mode.
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringLicense : GPLv2 or higher, see LICENSE.txt
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringMaintainer : jonathan.von_schroeder@dfki.de
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringStability : provisional
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringPortability : needs POSIX
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringsee <http://fmv.jku.at/depqbf/ for more information
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringon the depqbf prover and <http://www.qbflib.org/qdimacs.html>
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringand <http://www.qbflib.org/Draft/qDimacs.ps.gz>
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringfor more information on the qdimacs input format
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringmodule QBF.ProveDepQBF (depQBFProver)
1693a943ca581aca2beebb4c812ec6c9f17b8164Lennart Poetteringimport qualified Common.Result as Result
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringimport qualified QBF.AS_BASIC_QBF as AS
914d6c09f1a449c60c8495c179a8bbe012315ba2Tom Gundersenimport QBF.Sublogic (QBFSL, top)
3f6fd1ba65f962702753c4ad284b588e59689a23Lennart Poetteringimport qualified Control.Concurrent as Concurrent
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringimport System.Exit (ExitCode (..))
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering-- | The Prover implementation.
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringdepQBFProver :: Prover Sign AS.FORMULA Morphism QBFSL ProofTree
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringdepQBFProver = mkAutomaticProver "depqbf" top depQBFGUI depQBFCMDLautomaticBatch
914d6c09f1a449c60c8495c179a8bbe012315ba2Tom Gundersen Record for prover specific functions. This is used by both GUI and command
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering line interface.
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringatpFun :: String -- ^ theory name
914d6c09f1a449c60c8495c179a8bbe012315ba2Tom Gundersen -> ATPFunctions Sign AS.FORMULA Morphism ProofTree QBFProverState
914d6c09f1a449c60c8495c179a8bbe012315ba2Tom GundersenatpFun thName = ATPFunctions
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering { initialProverState = qbfProverState
732b7f39a2b3b1a2af90102c6262186ae71197acRonny Chevalier , atpTransSenName = transSenName
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering , atpInsertSentence = insertSentence
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering , goalOutput = showQDIMACSProblem thName
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering , proverHelpText = "for more information visit " ++
914d6c09f1a449c60c8495c179a8bbe012315ba2Tom Gundersen , batchTimeEnv = ""
914d6c09f1a449c60c8495c179a8bbe012315ba2Tom Gundersen , fileExtensions = FileExtensions
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering { problemOutput = ".qdimacs"
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering , proverOutput = "" -- prover doesn't output any files
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering , theoryConfiguration = "" -- prover doesn't use any configuration files
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering , runProver = runDepQBF
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering , createProverOptions = extraOpts }
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering Invokes the generic prover GUI.
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringdepQBFGUI :: String -- ^ theory name
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> Theory Sign AS.FORMULA ProofTree
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> [FreeDefMorphism AS.FORMULA Morphism] -- ^ freeness constraints
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringdepQBFGUI thName th freedefs =
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering genericATPgui (atpFun thName) True (proverName depQBFProver) thName th
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering freedefs emptyProofTree
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering automatic command line interface to the prover.
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringdepQBFCMDLautomaticBatch ::
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering Bool -- ^ True means include proved theorems
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> Bool -- ^ True means save problem file
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -- ^ used to store the result of the batch run
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> String -- ^ theory name
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> TacticScript -- ^ default tactic script
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> Theory Sign AS.FORMULA ProofTree
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering -> [FreeDefMorphism AS.FORMULA Morphism] -- ^ freeness constraints
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering -> IO (Concurrent.ThreadId, Concurrent.MVar ())
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering {- ^ fst: identifier of the batch thread for killing it
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering snd: MVar to wait for the end of the thread -}
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart PoetteringdepQBFCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering thName defTS th freedefs =
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering resultMVar (proverName depQBFProver) thName
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart PoetteringuniteOptions :: [String] -> String
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart PoetteringuniteOptions = intercalate " "
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom GundersenrunDepQBF :: QBFProverState
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering {- ^ logical part containing the input Sign and axioms and possibly
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering goals that have been proved earlier as additional axioms -}
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom Gundersen -> GenericConfig ProofTree -- ^ configuration to use
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering -> Bool -- ^ True means save QDIMACS file
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering -> String -- ^ name of the theory in the DevGraph
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom Gundersen -> AS_Anno.Named AS.FORMULA -- ^ goal to prove
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering -> IO (ATPRetval, GenericConfig ProofTree)
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering -- ^ (retval, configuration with proof status and complete output)
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart PoetteringrunDepQBF ps cfg saveQDIMACS thName nGoal =
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering saveFile = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".qdimacs"
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom Gundersen simpleOptions = uniteOptions $ extraOpts cfg
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering tl = configTimeLimit cfg
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering prob <- showQDIMACSProblem thName ps nGoal []
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering when saveQDIMACS
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering (writeFile (saveFile ++ ".qdimacs") prob)
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering tempDir <- getTemporaryDirectory
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering stpTmpFile <- writeTempFile prob tempDir saveFile
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering let command = "depqbf " ++ show tl ++ " "
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering ++ simpleOptions ++ " " ++ stpTmpFile
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom Gundersen t_start <- getHetsTime
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering (_, stdouth, stderrh, proch) <- runInteractiveCommand command
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering exitCode <- waitForProcess proch
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering t_end <- getHetsTime
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering removeFile stpTmpFile
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering let t_u = diffHetsTime t_end t_start
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering stdoutC <- hGetContents stdouth
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering stderrC <- hGetContents stderrh
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering let exitCode' = case exitCode of
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering ExitSuccess -> 0
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering ExitFailure i -> i
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering (pStat, ret) <- examineProof ps cfg
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering stdoutC stderrC exitCode' nGoal t_u tl
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering return (pStat, cfg
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering proofStatus = ret
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering , resultOutput = lines (stdoutC ++ stderrC)
a6a4f528899b1dab47408733b4a423c66ea40f7aThomas Hindoe Paaboel Andersen , timeUsed = usedTime ret
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering-- | examine Prover output
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart PoetteringexamineProof :: QBFProverState
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering -> GenericConfig ProofTree
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering -> IO (ATPRetval, ProofStatus ProofTree)
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart PoetteringexamineProof ps _ stdoutC _ exitCode nGoal tUsed _ =
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering defaultStatus =
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering ProofStatus { goalName = senAttr nGoal
1fc464f6fbecfc5d8ba9f7b98d19e21fb324bfb9Lennart Poettering , goalStatus = openGoalStatus
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering , usedAxioms = []
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering , usedProver = proverName depQBFProver
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering , proofTree = emptyProofTree
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering , usedTime = tUsed
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering , tacticScript = TacticScript "" }
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering getAxioms = map AS_Anno.senAttr (initialAxioms ps)
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering in case getDepQBFResult exitCode stdoutC of
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering DepQBFProved -> return (ATPSuccess, defaultStatus
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering goalStatus = Proved True
1fc464f6fbecfc5d8ba9f7b98d19e21fb324bfb9Lennart Poettering , usedAxioms = getAxioms
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering DepQBFTimeout -> return (ATPTLimitExceeded, defaultStatus)
1fc464f6fbecfc5d8ba9f7b98d19e21fb324bfb9Lennart Poettering DepQBFDisproved -> return (ATPSuccess, defaultStatus
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering goalStatus = Disproved
1fc464f6fbecfc5d8ba9f7b98d19e21fb324bfb9Lennart Poettering , usedAxioms = getAxioms
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering DepQBFError s -> return (ATPError ("Internal Errorr."
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering ++ "\nMessage:\n\n" ++ s)
d57c365bf8f09fbcc649e00f7060ff30809f67c2Lennart Poettering , defaultStatus)
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom Gundersendata DepQBFResult = DepQBFProved | DepQBFDisproved
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom Gundersen | DepQBFTimeout | DepQBFError String
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart PoetteringgetDepQBFResult :: Int -> String -> DepQBFResult
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringgetDepQBFResult exitCode out = case exitCode of
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering 10 -> if "SAT" `isPrefixOf` out
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering then DepQBFProved
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom Gundersen else DepQBFError
f647962d64e844689f3e2acfce6102fc47e76df2Michal Schmidt "Unexpected behaviour of prover!"
f647962d64e844689f3e2acfce6102fc47e76df2Michal Schmidt 20 -> if "UNSAT" `isPrefixOf` out
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering then DepQBFDisproved
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering else DepQBFError
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering "Unexpected behaviour of prover!"
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering _ -> if "SIGALRM" `isInfixOf` out
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering then DepQBFTimeout
1c4baffc1895809bae9ac36b670af90a4cb9cd7dTom Gundersen else DepQBFError
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering ("Uknown error: " ++ out)