ProveMinisat.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{- |
Module : ./Propositional/ProveMinisat.hs
Description : Provers for propositional logic
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : experimental
Portability : portable
This is the connection of the SAT-Solver minisat to Hets
-}
module Propositional.ProveMinisat
( MiniSatVer (..)
, minisatProver
, minisatConsChecker
) 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 Proofs.BatchProcessing
import qualified Logic.Prover as LP
import Interfaces.GenericATPState
import GUI.GenericATP
import Common.ProofTree
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.OrderedMap as OMap
import qualified Common.Result as Result
import Common.Utils
import Common.Timing
import Control.Monad (when)
import Control.Concurrent
import Data.Char
import Data.Maybe (fromMaybe)
import Data.Time (timeToTimeOfDay, midnight)
import Data.Time.Clock
import System.Directory
import System.Exit
-- * Prover implementation
minisatHelpText :: String
minisatHelpText = "minisat is a very fast SAT-Solver \n" ++
"No additional Options are available" ++
"for it!"
data MiniSatVer = Minisat | Minisat2 deriving Show
msatName :: MiniSatVer -> String
msatName = map toLower . show
{- |
The Prover implementation.
Implemented are: a prover GUI, and both commandline prover interfaces.
-}
minisatProver :: MiniSatVer
minisatProver v = LP.mkAutomaticProver (msatName v) (msatName v) top
(minisatProveGUI v) $ minisatProveCMDLautomaticBatch v
{- |
The Consistency Cheker.
-}
minisatConsChecker :: MiniSatVer
ProofTree
minisatConsChecker v =
LP.mkUsableConsChecker (msatName v) (msatName v) top $ consCheck v
consCheck :: MiniSatVer -> String -> LP.TacticScript
-- ^ free definitions
-> IO (LP.CCStatus ProofTree)
consCheck v thName _ tm _ = case LP.tTarget tm of
LP.Theory sig nSens -> do
let axioms = getAxioms $ snd $ unzip $ OMap.toList nSens
tmpl = basename thName ++ "_cc.minisat.dimacs"
bin = msatName v
dimacsOutput <- PC.showDIMACSProblem (thName ++ "_cc") sig
axioms Nothing
tmpFile <- getTempFile dimacsOutput tmpl
(exitCode, _, err) <- executeProcess bin [tmpFile] ""
removeFile tmpFile
(res, out) <- case exitCode of
ExitFailure 10 -> return (Just True, "consistent.")
ExitFailure 20 -> return (Just False, "inconsistent.")
ExitFailure 127 -> return (Nothing, err)
_ -> return (Nothing, "error by calling " ++ bin ++ " " ++ thName)
return LP.CCStatus { LP.ccResult = res
, LP.ccUsedTime = midnight
, LP.ccProofTree = ProofTree out }
where
getAxioms = map (AS_Anno.makeNamed "axn" . AS_Anno.sentence)
. filter AS_Anno.isAxiom
-- ** GUI
{- |
Invokes the generic prover GUI.
-}
minisatProveGUI :: MiniSatVer -- ^ choosen minisat version
-> String -- ^ theory name
-- ^ free definitions
-> IO [LP.ProofStatus ProofTree]
-- ^ proof status for each goal
minisatProveGUI v thName th freedefs =
genericATPgui (atpFun v thName) True (msatName v) thName th
freedefs emptyProofTree
{- |
Parses a given default tactic script into a
'Interfaces.GenericATPState.ATPTacticScript' if possible.
-}
parseminisatTacticScript :: LP.TacticScript -> ATPTacticScript
parseminisatTacticScript = parseTacticScript batchTimeLimit []
-- ** command line function
{- |
Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
automatic command line interface to the minisat prover.
minisat specific functions are omitted by data type ATPFunctions.
-}
minisatProveCMDLautomaticBatch :: MiniSatVer
-> Bool -- ^ True means include proved theorems
-> Bool -- ^ True means save problem file
-> MVar (Result.Result [LP.ProofStatus ProofTree])
-- ^ used to store the result of the batch run
-> String -- ^ theory name
-> LP.TacticScript -- ^ default tactic script
-- ^ theory consisting of a signature and a list of Named sentences
-- ^ free definitions
-> IO (ThreadId, MVar ())
{- ^ fst: identifier of the batch thread for killing it
snd: MVar to wait for the end of the thread -}
minisatProveCMDLautomaticBatch v inclProvedThs saveProblem_batch resultMVar
thName defTS th freedefs =
genericCMDLautomaticBatch (atpFun v thName) inclProvedThs saveProblem_batch
resultMVar (msatName v) thName
(parseminisatTacticScript defTS) th freedefs emptyProofTree
{- |
Record for prover specific functions. This is used by both GUI and command
line interface.
-}
atpFun :: MiniSatVer
-> String -- ^ Theory name
atpFun v thName = ATPFunctions
{ initialProverState = PState.propProverState
, goalOutput = Cons.goalDIMACSProblem thName
, atpTransSenName = PState.transSenName
, atpInsertSentence = PState.insertSentence
, proverHelpText = minisatHelpText
, runProver = runminisat v
, batchTimeEnv = "HETS_MINISAT_BATCH_TIME_LIMIT"
, fileExtensions = FileExtensions
{ problemOutput = ".dimacs"
, proverOutput = ".minisat"
, theoryConfiguration = ".cminisat"}
, createProverOptions = createminisatOptions }
{- |
Runs minisat. minisat is assumed to reside in PATH.
-}
runminisat :: MiniSatVer -> 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
-- Goal to prove
-> IO (ATPRetval, GenericConfig ProofTree)
-- (retval, configuration with proof status and complete output)
runminisat v pState cfg saveDIMACS thName nGoal = do
prob <- Cons.goalDIMACSProblem thName pState nGoal []
let thName_clean = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".dimacs"
when saveDIMACS (writeFile thName_clean prob)
zFileName <- getTempFile prob thName_clean
runStuff zFileName $ fromMaybe 100 $ timeLimit cfg
where
bin = msatName v
defaultProofStatus opts =
(LP.openProofStatus (AS_Anno.senAttr nGoal) bin
emptyProofTree)
{ LP.tacticScript = LP.TacticScript $ show ATPTacticScript
{ tsTimeLimit = configTimeLimit cfg
, tsExtraOpts = opts } }
runStuff zFileName t = do
startTime <- getHetsTime
mExit <- timeoutCommand t bin [zFileName]
case mExit of
Just (exCode, out, _) -> do
endTime <- getHetsTime
let usedTime = diffHetsTime endTime startTime
return $ case exCode of
ExitFailure 20 -> (ATPSuccess, cfg
{ proofStatus = (defaultProofStatus [])
{ LP.goalStatus = LP.Proved True
, LP.usedAxioms = filter (/= AS_Anno.senAttr nGoal)
$ map AS_Anno.senAttr $ PState.initialAxioms pState
, LP.proofTree = ProofTree out }
, timeUsed = usedTime })
ExitFailure 10 -> (ATPSuccess, cfg
{ proofStatus = (defaultProofStatus [])
, LP.proofTree = ProofTree out }})
ExitSuccess -> (ATPSuccess, cfg
{ proofStatus = (defaultProofStatus [])
, LP.proofTree = ProofTree "Unkown"
, LP.usedTime = timeToTimeOfDay $ secondsToDiffTime 0 }})
_ -> (ATPError "Internal error.", cfg
{ proofStatus = defaultProofStatus [] })
Nothing -> return (ATPTLimitExceeded, cfg
{ proofStatus = (defaultProofStatus [])
{ LP.goalName = thName
, LP.usedAxioms = []
, LP.usedProver = bin
, LP.proofTree = ProofTree "Timeout"
, LP.usedTime = timeToTimeOfDay $ secondsToDiffTime 0
, LP.tacticScript = LP.TacticScript $ show ATPTacticScript
{ tsTimeLimit = configTimeLimit cfg
, tsExtraOpts = [] } }
, timeLimitExceeded = True })
{- |
Creates a list of all options the minisat prover runs with.
Only Option is the timelimit
-}
createminisatOptions :: GenericConfig ProofTree -> [String]
createminisatOptions cfg = [show $ configTimeLimit cfg]