{- |

Module : $Header$

Description : Provers for propositional logic

Copyright : (c) Dominik Luecke, Uni Bremen 2007

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : luecke@informatik.uni-bremen.de

Stability : experimental

Portability : portable

This is the connection of the SAT-Solver minisat to Hets

-}

module Propositional.Prove

(

zchaffProver, -- the zChaff II Prover

propConsChecker

)

where

import qualified Propositional.AS_BASIC_Propositional as AS_BASIC

import qualified Propositional.Conversions as Cons

import qualified Propositional.Conversions as PC

import qualified Propositional.Morphism as PMorphism

import qualified Propositional.ProverState as PState

import qualified Propositional.Sign as Sig

import Propositional.Sublogic(PropSL,top)

import Propositional.ChildMessage

import Proofs.BatchProcessing

import qualified Logic.Prover as LP

import Interfaces.GenericATPState

import GUI.GenericATP

import Common.UniUtils as CP

import Common.ProofTree

import Common.Utils (readMaybe)

import qualified Common.AS_Annotation as AS_Anno

import qualified Common.Id as Id

import qualified Common.OrderedMap as OMap

import qualified Common.Result as Result

import Control.Monad (when)

import qualified Control.Concurrent as Concurrent

import qualified Common.Exception as Exception

import Data.List

import Data.Maybe

import Data.Time (TimeOfDay, timeToTimeOfDay, midnight)

import System.Directory

import System.Cmd

import System.Exit

import System.IO

-- * Prover implementation

zchaffHelpText :: String

zchaffHelpText = "Zchaff is a very fast SAT-Solver \n"++

"No additional Options are available"++

"for it!"

-- | the name of the prover

zchaffS :: String

zchaffS = "zchaff"

{- |

The Prover implementation.

Implemented are: a prover GUI, and both commandline prover interfaces.

-}

zchaffProver

:: LP.Prover Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism PropSL ProofTree

zchaffProver = (LP.mkProverTemplate zchaffS top zchaffProveGUI)

{ LP.proveCMDLautomatic = Just $ zchaffProveCMDLautomatic

, LP.proveCMDLautomaticBatch = Just $ zchaffProveCMDLautomaticBatch }

{- |

The Consistency Cheker.

-}

propConsChecker :: LP.ConsChecker Sig.Sign AS_BASIC.FORMULA PropSL

PMorphism.Morphism ProofTree

propConsChecker = LP.ConsChecker zchaffS top consCheck

consCheck :: String -> LP.TacticScript

-> LP.TheoryMorphism Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree

-> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]

-- ^ free definitions

-> IO (LP.CCStatus ProofTree)

consCheck thName _ tm _ =

case LP.tTarget tm of

LP.Theory sig nSens -> do

let axioms = getAxioms $ snd $ unzip $ OMap.toList nSens

thName_clean = map (\c -> if c == '/' then '_' else c) thName

tmpFile = "/tmp/" ++ (thName_clean ++ "_cc.dimacs")

resultFile = tmpFile ++ ".result"

dimacsOutput <- PC.ioDIMACSProblem (thName ++ "_cc")

sig ( [(AS_Anno.makeNamed "myAxioms" $

AS_BASIC.Implication

(

AS_BASIC.Conjunction

(map (AS_Anno.sentence) axioms)

Id.nullRange

)

(AS_BASIC.False_atom Id.nullRange)

Id.nullRange

)

{

AS_Anno.isAxiom = True

, AS_Anno.isDef = False

, AS_Anno.wasTheorem = False

}

]

)[]

outputHf <- openFile tmpFile ReadWriteMode

hPutStr outputHf dimacsOutput

hClose outputHf

exitCode <- system ("zchaff " ++ tmpFile ++ " >> " ++ resultFile)

removeFile tmpFile

if exitCode /= ExitSuccess then return $ LP.CCStatus

(ProofTree $ "error by call zchaff " ++ thName)

midnight Nothing

else do

resultHf <- readFile resultFile

let isSAT = searchResult resultHf

when (length resultHf > 0) $ removeFile resultFile

return $ LP.CCStatus (ProofTree resultHf) midnight isSAT

where

getAxioms :: [LP.SenStatus AS_BASIC.FORMULA (LP.ProofStatus ProofTree)]

-> [AS_Anno.Named AS_BASIC.FORMULA]

getAxioms f = map (AS_Anno.makeNamed "consistency" . AS_Anno.sentence)

$ filter AS_Anno.isAxiom f

searchResult :: String -> Maybe Bool

searchResult hf = let ls = lines hf in

if any (== "RESULT:\tUNSAT") ls then Just True else

if any (== "RESULT:\tSAT") ls then Just False else Nothing

-- ** GUI

{- |

Invokes the generic prover GUI.

-}

zchaffProveGUI :: String -- ^ theory name

-> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree

-> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]

-- ^ free definitions

-> IO([LP.ProofStatus ProofTree]) -- ^ proof status for each goal

zchaffProveGUI thName th freedefs =

genericATPgui (atpFun thName) True (LP.proverName zchaffProver) thName th

freedefs emptyProofTree

{- |

Parses a given default tactic script into a

'Interfaces.GenericATPState.ATPTacticScript' if possible.

-}

parseZchaffTacticScript :: LP.TacticScript -> ATPTacticScript

parseZchaffTacticScript = parseTacticScript batchTimeLimit []

-- ** command line functions

{- |

Implementation of 'Logic.Prover.proveCMDLautomatic' which provides an

automatic command line interface for a single goal.

SPASS specific functions are omitted by data type ATPFunctions.

-}

zchaffProveCMDLautomatic ::

String -- ^ theory name

-> LP.TacticScript -- ^ default tactic script

-> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree

-- ^ theory consisting of a signature and a list of Named sentence

-> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]

-- ^ free definitions

-> IO (Result.Result ([LP.ProofStatus ProofTree]))

-- ^ Proof status for goals and lemmas

zchaffProveCMDLautomatic thName defTS th freedefs =

genericCMDLautomatic (atpFun thName) (LP.proverName zchaffProver) thName

(parseZchaffTacticScript defTS) th freedefs emptyProofTree

{- |

Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an

automatic command line interface to the zchaff prover.

zchaff specific functions are omitted by data type ATPFunctions.

-}

zchaffProveCMDLautomaticBatch ::

Bool -- ^ True means include proved theorems

-> Bool -- ^ True means save problem file

-> Concurrent.MVar (Result.Result [LP.ProofStatus ProofTree])

-- ^ used to store the result of the batch run

-> String -- ^ theory name

-> LP.TacticScript -- ^ default tactic script

-> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree

-- ^ theory consisting of a signature and a list of Named sentences

-> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]

-- ^ free definitions

-> IO (Concurrent.ThreadId,Concurrent.MVar ())

-- ^ fst: identifier of the batch thread for killing it

-- snd: MVar to wait for the end of the thread

zchaffProveCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar

thName defTS th freedefs =

genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch

resultMVar (LP.proverName zchaffProver) thName

(parseZchaffTacticScript defTS) th freedefs emptyProofTree

{- |

Record for prover specific functions. This is used by both GUI and command

line interface.

-}

atpFun :: String -- Theory name

-> ATPFunctions Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree

PState.PropProverState

atpFun thName = ATPFunctions

{ initialProverState = PState.propProverState

, goalOutput = Cons.goalDIMACSProblem thName

, atpTransSenName = PState.transSenName

, atpInsertSentence = PState.insertSentence

, proverHelpText = zchaffHelpText

, runProver = runZchaff

, batchTimeEnv = "HETS_ZCHAFF_BATCH_TIME_LIMIT"

, fileExtensions = FileExtensions

{ problemOutput = ".dimacs"

, proverOutput = ".zchaff"

, theoryConfiguration = ".czchaff"}

, createProverOptions = createZchaffOptions }

{- |

Runs zchaff. zchaff is assumed to reside in PATH.

-}

runZchaff :: PState.PropProverState

-- logical part containing the input Sign and

-- axioms and possibly goals that have been proved

-- earlier as additional axioms

-> GenericConfig ProofTree

-- configuration to use

-> Bool

-- True means save DIMACS file

-> String

-- Name of the theory

-> AS_Anno.Named AS_BASIC.FORMULA

-- Goal to prove

-> IO (ATPRetval

, GenericConfig ProofTree

)

-- (retval, configuration with proof status and complete output)

runZchaff pState cfg saveDIMACS thName nGoal =

do

prob <- Cons.goalDIMACSProblem thName pState nGoal []

when saveDIMACS

(writeFile (thName++'_':AS_Anno.senAttr nGoal++".dimacs")

prob)

(writeFile (zFileName)

prob)

zchaff <- newChildProcess "zchaff" [CP.arguments allOptions]

Exception.catch (runZchaffReal zchaff)

(\ excep -> do

-- kill zchaff process

destroy zchaff

_ <- waitForChildProcess zchaff

deleteJunk

excepToATPResult (LP.proverName zchaffProver) nGoal excep)

where

deleteJunk = do

catch (removeFile zFileName) (const $ return ())

catch (removeFile "resolve_trace") (const $ return ())

zFileName = "/tmp/problem_"++thName++'_':AS_Anno.senAttr nGoal++".dimacs"

allOptions = zFileName : (createZchaffOptions cfg)

runZchaffReal zchaff =

do

zchaffOut <- parseIt zchaff isEnd

(res, usedAxs, output, tUsed) <- analyzeZchaff zchaffOut pState

let (err, retval) = proofStat res usedAxs [] (head output)

deleteJunk

return (err,

cfg{proofStatus = retval,

resultOutput = output,

timeUsed = tUsed})

where

proofStat res usedAxs options out

| isJust res && elem (fromJust res) proved =

(ATPSuccess,

(defaultProofStatus options)

{LP.goalStatus = LP.Proved $ Nothing

, LP.usedAxioms = filter

(/= AS_Anno.senAttr nGoal) usedAxs

, LP.proofTree = ProofTree $ out })

| isJust res && elem (fromJust res) disproved =

(ATPSuccess,

(defaultProofStatus options)

{LP.goalStatus = LP.Disproved} )

| isJust res && elem (fromJust res) timelimit =

(ATPTLimitExceeded, defaultProofStatus options)

| isNothing res =

(ATPError "Internal error.",

defaultProofStatus options)

| otherwise = (ATPSuccess,

defaultProofStatus options)

defaultProofStatus opts =

(LP.openProofStatus (AS_Anno.senAttr nGoal)

(LP.proverName zchaffProver)

emptyProofTree)

{LP.tacticScript = LP.TacticScript $ show

$ ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg

, tsExtraOpts = opts} }

proved :: [String]

proved = ["Proof found."]

disproved :: [String]

disproved = ["Completion found."]

timelimit :: [String]

timelimit = ["Ran out of time."]

-- | analysis of output

analyzeZchaff :: String

-> PState.PropProverState

-> IO (Maybe String, [String], [String], TimeOfDay)

analyzeZchaff str pState =

let

str' = foldr (\ch li -> if ch == '\x9'

then ""++li

else ch:li) "" str

str2 = foldr (\ch li -> if ch == '\x9'

then " "++li

else ch:li) "" str

output = [str2]

unsat = isInfixOf re_UNSAT str'

sat = isInfixOf re_SAT str'

timeLine = if isPrefixOf re_TIME str' then

drop (length re_TIME) str' else "0"

timeout = isInfixOf re_end_to str' || isInfixOf re_end_mo str'

time = calculateTime timeLine

usedAx = map (AS_Anno.senAttr) $ PState.initialAxioms pState

in

if timeout

then

return (Just $ head timelimit, usedAx, output, time)

else

if (sat && (not unsat))

then

return (Just $ head $ disproved, usedAx, output, time)

else if ((not sat) && unsat)

then

return (Just $ head $ proved, usedAx, output, time)

else

do

return (Nothing, usedAx, output, time)

-- | Calculated the time need for the proof in seconds

calculateTime :: String -> TimeOfDay

calculateTime timeLine =

timeToTimeOfDay $ realToFrac $ (maybe

(error $ "calculateTime " ++ timeLine) id $ readMaybe timeLine

:: Double)

re_UNSAT :: String

re_UNSAT = "RESULT:UNSAT"

re_SAT :: String

re_SAT = "RESULT:SAT"

re_TIME :: String

re_TIME = "Total Run Time"

-- | We are searching for Flotter needed to determine the end of input

isEnd :: String -> Bool

isEnd inS = any (`isInfixOf` inS) [re_end, re_end_to, re_end_mo]

re_end :: String

re_end = "RESULT:"

re_end_to :: String

re_end_to = "TIME OUT"

re_end_mo :: String

re_end_mo = "MEM OUT"

-- | Converts a thrown exception into an ATP result (ATPRetval and proof tree).

excepToATPResult :: String

-- ^ name of running prover

-> AS_Anno.Named AS_BASIC.FORMULA

-- ^ goal to prove

-> Exception.Exception

-- ^ occured exception

-> IO (ATPRetval,

GenericConfig ProofTree)

-- ^ (retval,

-- configuration with proof status and complete output)

excepToATPResult prName nGoal excep = return $ case excep of

-- this is supposed to distinguish "fd ... vanished"

-- errors from other exceptions

Exception.IOException e ->

(ATPError ("Internal error communicating with " ++

prName ++ ".\n"

++ show e), emptyCfg)

Exception.AsyncException Exception.ThreadKilled ->

(ATPBatchStopped, emptyCfg)

_ -> (ATPError ("Error running " ++ prName ++ ".\n"

++ show excep),

emptyCfg)

where

emptyCfg = emptyConfig prName (AS_Anno.senAttr nGoal)

emptyProofTree

{- |

Creates a list of all options the zChaff prover runs with.

Only Option is the timelimit

-}

createZchaffOptions :: GenericConfig ProofTree -> [String]

createZchaffOptions cfg =

[show $ configTimeLimit cfg]