Prove.hs revision 452d66feaf5b4d7f2038bb66b7d22b6ed87d7e79
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : Provers for propositional logic
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCopyright : (c) Dominik Luecke, Uni Bremen 2007
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyMaintainer : luecke@informatik.uni-bremen.de
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyStability : experimental
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPortability : portable
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyThis is the connection of the SAT-Solver minisat to Hets
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly zchaffProver, -- the zChaff II Prover
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder propConsChecker
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maederimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport qualified Propositional.Conversions as Cons
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reillyimport qualified Propositional.Conversions as PC
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maederimport qualified Propositional.Morphism as PMorphism
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maederimport qualified Propositional.ProverState as PState
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport qualified Propositional.Sign as Sig
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport Propositional.Sublogic(PropSL,top)
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reillyimport qualified Logic.Prover as LP
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maederimport qualified Interfaces.GenericATPState as ATPState
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maederimport GUI.Utils (infoDialog)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport ChildProcess as CP
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederimport Destructible
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maederimport Common.Utils (readMaybe)
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maederimport qualified Common.AS_Annotation as AS_Anno
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Id as Id
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reillyimport qualified Common.OrderedMap as OMap
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyimport qualified Common.Result as Result
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport qualified Control.Concurrent as Concurrent
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyimport qualified Control.Exception as Exception
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport Data.Time (TimeOfDay,timeToTimeOfDay)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- * Prover implementation
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederzchaffHelpText :: String
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederzchaffHelpText = "Zchaff is a very fast SAT-Solver \n"++
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly "No additional Options are available"++
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | the name of the prover
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyzchaffS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyzchaffS = "zchaff"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder The Prover implementation.
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder Implemented are: a prover GUI, and both commandline prover interfaces.
1a38107941725211e7c3f051f7a8f5e12199f03acmaederzchaffProver
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly :: LP.Prover Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism PropSL ProofTree
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyzchaffProver = (LP.mkProverTemplate zchaffS top zchaffProveGUI)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly { LP.proveCMDLautomatic = Just $ zchaffProveCMDLautomatic
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , LP.proveCMDLautomaticBatch = Just $ zchaffProveCMDLautomaticBatch }
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder The Consistency Cheker.
fa373bc327620e08861294716b4454be8d25669fChristian MaederpropConsChecker :: LP.ConsChecker Sig.Sign AS_BASIC.FORMULA PropSL
fa373bc327620e08861294716b4454be8d25669fChristian MaederpropConsChecker = LP.mkProverTemplate zchaffS top consCheck
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederconsCheck :: String -> LP.TheoryMorphism Sig.Sign AS_BASIC.FORMULA
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism] -- ^ free definitions
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly -> IO([LP.Proof_status ProofTree])
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'ReillyconsCheck thName tm _ =
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder LP.Theory sig nSens -> do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let axioms = getAxioms $ snd $ unzip $ OMap.toList nSens
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly tmpFile = "/tmp/" ++ (thName ++ "_cc.dimacs")
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maeder resultFile = tmpFile ++ ".result"
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maeder dimacsOutput <- PC.ioDIMACSProblem (thName ++ "_cc")
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maeder sig ( [(AS_Anno.makeNamed "myAxioms" $
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder outputHf <- openFile tmpFile ReadWriteMode
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly hPutStr outputHf dimacsOutput
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder hClose outputHf
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder exitCode <- system ("zchaff " ++ tmpFile ++ " >> " ++ resultFile)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly removeFile tmpFile
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder if exitCode /= ExitSuccess then
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder infoDialog "consistency checker"
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ("error by call zchaff " ++ thName)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder resultHf <- openFile resultFile ReadMode
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder isSAT <- searchResult resultHf
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder hClose resultHf
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder removeFile resultFile
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder if isSAT then
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder infoDialog "consistency checker"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ("consistent.")
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder infoDialog "consistency checker"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ("inconsistent.")
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly getAxioms :: [LP.SenStatus AS_BASIC.FORMULA (LP.Proof_status ProofTree)]
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder getAxioms f = map (AS_Anno.makeNamed "consistency" . AS_Anno.sentence) $ filter AS_Anno.isAxiom f
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder searchResult :: Handle -> IO Bool
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder searchResult hf = do
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder eof <- hIsEOF hf
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder line <- hGetLine hf
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder putStrLn line
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder if line == "RESULT:\tUNSAT" then
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder else if line == "RESULT:\tSAT" then
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder else searchResult hf
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder Invokes the generic prover GUI.
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaederzchaffProveGUI :: String -- ^ theory name
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism] -- ^ free definitions
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maeder -> IO([LP.Proof_status ProofTree]) -- ^ proof status for each goal
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederzchaffProveGUI thName th freedefs =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder genericATPgui (atpFun thName) True (LP.prover_name zchaffProver) thName th
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder freedefs emptyProofTree
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Parses a given default tactic script into a
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder 'Interfaces.GenericATPState.ATPTactic_script' if possible.
bcd914850de931848b86d7728192a149f9c0108bChristian MaederparseZchaffTactic_script :: LP.Tactic_script
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'ReillyparseZchaffTactic_script =
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly parseTactic_script batchTimeLimit
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder Parses a given default tactic script into a
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder 'Interfaces.GenericATPState.ATPTactic_script' if possible. Otherwise a default
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder prover's tactic script is returned.
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'ReillyparseTactic_script :: Int -- ^ default time limit (standard:
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederparseTactic_script tLimit (LP.Tactic_script ts) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder maybe (ATPState.ATPTactic_script { ATPState.ts_timeLimit = tLimit,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder id $ readMaybe ts
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder-- ** command line functions
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder Implementation of 'Logic.Prover.proveCMDLautomatic' which provides an
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder automatic command line interface for a single goal.
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder SPASS specific functions are omitted by data type ATPFunctions.
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian MaederzchaffProveCMDLautomatic ::
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder String -- ^ theory name
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -> LP.Tactic_script -- ^ default tactic script
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree -- ^ theory consisting of a
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -- signature and a list of Named sentence
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism] -- ^ free definitions
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -> IO (Result.Result ([LP.Proof_status ProofTree]))
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -- ^ Proof status for goals and lemmas
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'ReillyzchaffProveCMDLautomatic thName defTS th freedefs =
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder genericCMDLautomatic (atpFun thName) (LP.prover_name zchaffProver) thName
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder (parseZchaffTactic_script defTS) th freedefs emptyProofTree
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly automatic command line interface to the zchaff prover.
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly zchaff specific functions are omitted by data type ATPFunctions.
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'ReillyzchaffProveCMDLautomaticBatch ::
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly Bool -- ^ True means include proved theorems
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -> Bool -- ^ True means save problem file
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -> Concurrent.MVar (Result.Result [LP.Proof_status ProofTree])
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -- ^ used to store the result of the batch run
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -> String -- ^ theory name
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly -> LP.Tactic_script -- ^ default tactic script
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly -> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree -- ^ theory consisting of a
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly -- signature and a list of Named sentences
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism] -- ^ free definitions
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly -> IO (Concurrent.ThreadId,Concurrent.MVar ())
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly -- ^ fst: identifier of the batch thread for killing it
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly -- snd: MVar to wait for the end of the thread
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'ReillyzchaffProveCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder thName defTS th freedefs =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder resultMVar (LP.prover_name zchaffProver) thName
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder (parseZchaffTactic_script defTS) th freedefs emptyProofTree
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder Record for prover specific functions. This is used by both GUI and command
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder line interface.
ee48a7a67da604356b665e51aa7545536a09b737Christian MaederatpFun :: String -- Theory name
45e2bc90dd11147156ddd7f9651ce8b2ec00f2a1Christian Maeder -> ATPState.ATPFunctions Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree PState.PropProverState
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder ATPState.initialProverState = PState.propProverState
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder , ATPState.goalOutput = Cons.goalDIMACSProblem thName
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder , ATPState.atpTransSenName = PState.transSenName
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly , ATPState.atpInsertSentence = PState.insertSentence
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , ATPState.proverHelpText = zchaffHelpText
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , ATPState.batchTimeEnv = "HETS_ZCHAFF_BATCH_TIME_LIMIT"
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , ATPState.fileExtensions = ATPState.FileExtensions{ATPState.problemOutput = ".dimacs",
fa373bc327620e08861294716b4454be8d25669fChristian Maeder , ATPState.createProverOptions = createZchaffOptions
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder Runs zchaff. zchaff is assumed to reside in PATH.