Prop2CNF.hs revision 9eb6a481980d81a55898ba418fba72fc3c09d8c8
{- |
Module : $Header$
Description : Helper functions for CNF translation
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : luecke@tzi.de
Stability : experimental
Portability : non-portable (imports Logic.Logic)
Helper functions for the translation of propositional formulae to CNF. We are
using SPASS -Flotter=1 here
-}
{-
Ref.
Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
What is a Logic?.
In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhäuser.
2005.
-}
{-
ToDo: clause formula relation to SPASS Parser + AS
add analysis for clause formula
put the stuff together
-}
module Propositional.Prop2CNF
(
translateToCNF -- CNF conversion via SPASS
,translateSentenceToCNF -- CNF conversion of a sentence
)
where
import qualified SPASS.ProverState as PState
import qualified Propositional.Prop2CASLHelpers as P2C
import qualified Comorphisms.CASL2SPASS as C2S
import qualified Logic.Comorphism as Com
import qualified SPASS.Sign as Sig
import qualified Propositional.Sign as PSign
import qualified Common.Result as Result
import qualified Propositional.AS_BASIC_Propositional as PBasic
import qualified Common.AS_Annotation as AS_Anno
import qualified SPASS.Conversions as Conv
import qualified SPASS.DFGParser as SParse
import qualified Common.Id as Id
import qualified Data.Set as Set
import qualified SPASS.Translate as Translate
import qualified CASL.Logic_CASL as CLogic
import qualified Logic.Coerce as LC
import ChildProcess
import ProcessClasses
import System
import Data.List
import Data.Maybe
import HTk
import qualified Control.Exception as Exception
import Common.DocUtils
import System.IO.Unsafe
safeDFGFiles ::Bool
safeDFGFiles = False
prover_name :: String
prover_name = "SPASS"
-- This hack is needed to break up a cicle in imports :(
map_theory =
\ti1 ->
do ti2 <- P2C.mapTheory ti1
"Mapping theory along comorphism" ti2
-- | Shortcut for the translation of the theory
getTheory = map_theory
-- | forget the internal settings for a while
-- this is no loss, since we have to restore them
-- anyways
dementia :: [AS_Anno.Named PBasic.FORMULA]
dementia frm = map (\xv ->
xv
{
AS_Anno.isAxiom = True
, AS_Anno.isDef = False
, AS_Anno.wasTheorem = False
}
) frm
-- | Initial ProverState for Spass
createInitProverState :: PSign.Sign
createInitProverState sign nForms =
let (osig, oth) =
case Result.maybeResult $ getTheory (sign, dementia nForms) of
Just (xs,ys) -> (xs,ys)
Nothing -> error "Should not happen... Error in Prop2CNF"
in
PState.spassProverState osig oth
{- |
Runs SPASS. SPASS is assumed to reside in PATH.
-}
runSpass :: PState.SPASSProverState -- Spass Prover state... Theory + Sig
-> Bool -- ^ True means save DFG file
-> IO String -- Placeholder
runSpass sps saveDFG =
do
spass <- newChildProcess prover_name [ChildProcess.arguments allOptions]
Exception.catch (runSpassReal spass)
(\ excep -> do
-- kill spass process
destroy spass
_ <- waitForChildProcess spass
return ("SPASS not found... Bailing out!!! Cause was: "
++ show excep
)
)
where
runSpassReal spass = do
-- check if SPASS is running
e <- getToolStatus spass
if isJust e
then error "Something is wrong"
else do
prob <- showDFGProblem "Translation" sps (filteredOptions)
when saveDFG
(writeFile ("FlotterIn.dfg") prob)
sendMsg spass prob
flotterOut <- parseProtected spass
when saveDFG
(writeFile ("FlotterOut.dfg") flotterOut)
return flotterOut
filteredOptions = ["-Auto=0","-Flotter=1","-Stdin=1"]
allOptions = filteredOptions
{- |
Pretty printing SPASS goal in DFG format.
-}
showDFGProblem :: String -- ^ theory name
-> PState.SPASSProverState -- ^ prover state containing
-- initial logical part
-> [String] -- ^ extra options
-> IO String -- ^ formatted output of the goal
showDFGProblem thName pst opts = do
prob <- Conv.genSPASSProblem thName (PState.initialLogicalPart pst) $ Nothing
-- add SPASS command line settings and extra options
let prob' = prob { Sig.settings = (Sig.settings prob) ++
(PState.parseSPASSCommands opts) }
return $ showDoc prob' ""
-- | Helper for reading SPASS output
parseProtected :: ChildProcess -> IO String
parseProtected spass = do
e <- getToolStatus spass
case e of
Nothing ->
do
dfg <- parseIt spass
_ <- waitForChildProcess spass
return dfg
Just (ExitFailure retval) ->
do
_ <- waitForChildProcess spass
return ("Error!!! Cause was: " ++ show retval)
Just ExitSuccess -> return "done"
parseIt :: ChildProcess -> IO String
parseIt spass = do
line <- readMsg spass
msg <- parseItHelp spass $ return line
return msg
parseItHelp :: ChildProcess -> IO String -> IO String
parseItHelp spass inp = do
e <- getToolStatus spass
inT <- inp
case e of
Nothing
->
do
line <- readMsg spass
case isEnd line of
True ->
return inT
_ ->
parseItHelp spass $ return (inT ++ "\n" ++ line)
Just (ExitFailure retval)
-- returned error
-> do
_ <- waitForChildProcess spass
return $ "SPASS returned error: "++(show retval)
Just ExitSuccess
-- completed successfully. read remaining output.
->
do
line <- readMsg spass
case isEnd line of
True ->
return inT
_ ->
parseItHelp spass $ return (inT ++ "\n" ++ line)
-- | We are searching for Flotter needed to determine the end of input
isEnd :: String -> Bool
isEnd inS = isPrefixOf "FLOTTER needed" inS
-- | Main function for run SPASS and Parse
runSPASSandParseDFG :: PState.SPASSProverState -- Spass Prover state... Theory + Sig
-> Bool -- True means save DFG file
-> Sig.SPProblem -- Output AS
runSPASSandParseDFG pstate save =
parseDFG $ unsafePerformIO $ runSpass pstate save
-- | run the DFG Parser
parseDFG :: String -> Sig.SPProblem
parseDFG input
= case (parse SParse.parseSPASS "" input) of
Left err -> error $ "parse error at " ++ show err
Right xv -> xv
-- | Restore the values of the named fields in Formulae
restoreContext :: [AS_Anno.Named PBasic.FORMULA] -- Input Formulae
-> [AS_Anno.Named PBasic.FORMULA] -- Translated Formula
-> [AS_Anno.Named PBasic.FORMULA] -- Output
restoreContext [] [] = []
restoreContext [] _ = []
restoreContext xs (yv:ys) =
let
trName = AS_Anno.senAttr yv
trNm = Translate.transSenName
frm = head $ filter (\xv -> (trNm $ AS_Anno.senAttr xv) == trName) xs
inName = AS_Anno.senAttr frm
isAx = AS_Anno.isAxiom frm
isDef = AS_Anno.isDef frm
wasTh = AS_Anno.wasTheorem frm
sent = AS_Anno.sentence yv
in
[(AS_Anno.makeNamed inName sent)
{
AS_Anno.isAxiom = isAx
, AS_Anno.isDef = isDef
, AS_Anno.wasTheorem = wasTh
}
] ++ restoreContext xs ys
restoreContext _ _ = []
-- | Join different clauses to a single CNF-Formula
joinClause :: Sig.SPClauseType
joinClause inCt inSetting inFrm =
case inFrm of
[]-> []
_ -> joinClauseHelper inCt (determineClauseNames inSetting) inSetting inFrm
-- | Join Clauses according to the Clause-Formula-Relation
joinClauseHelper :: Sig.SPClauseType
-> Set.Set String
joinClauseHelper inCt inSet inSetting inFrm =
case (Set.null inSet) of
True -> []
_ ->
let
smallestElem = Set.findMin inSet
newSet = Set.deleteMin inSet
clauses = filterClauseNames smallestElem inSetting inFrm
nakedForms = map (AS_Anno.sentence) clauses
firstForm = head clauses
inName = smallestElem
isAx = AS_Anno.isAxiom firstForm
isDef = AS_Anno.isDef firstForm
wasTh = AS_Anno.wasTheorem firstForm
in
case inCt of
{
AS_Anno.isAxiom = isAx
, AS_Anno.isDef = isDef
, AS_Anno.wasTheorem = wasTh
}
]
++ (joinClauseHelper inCt newSet inSetting inFrm)
{
AS_Anno.isAxiom = isAx
, AS_Anno.isDef = isDef
, AS_Anno.wasTheorem = wasTh
}
]
++ (joinClauseHelper inCt newSet inSetting inFrm)
-- | get Clauses with a particular name
filterClauseNames :: String -> Sig.SPSetting -> [AS_Anno.Named PBasic.FORMULA] -> [AS_Anno.Named PBasic.FORMULA]
filterClauseNames name setting frms = let clrel =
(\xy -> case xy of
Sig.SPClauseRelation cls -> cls
_ -> error "Wrong type"
)
setting
thisNames = map (Sig.clauseSPR) $ filter (\xv -> Sig.formulaSPR xv == name) clrel
namesSet = foldl (\yv xv -> Set.insert xv yv) Set.empty thisNames
in
filter (\xv -> Set.member (AS_Anno.senAttr xv) namesSet) frms
-- | determine all names for clauses that occur
determineClauseNames :: Sig.SPSetting -> Set.Set String
(
(\xy -> case xy of
Sig.SPClauseRelation cls -> cls
_ -> error "Wrong type"
)
xs
)
-- | Translation of named clauses
translateSPClause :: Sig.SPClauseType -- Clause Type is needed
-> Sig.SPClause -- the named clause
translateSPClause ct nspc =
let
inName = AS_Anno.senAttr nspc
isAx = AS_Anno.isAxiom nspc
isDef = AS_Anno.isDef nspc
wasTh = AS_Anno.wasTheorem nspc
cla = AS_Anno.sentence nspc
transL = translateNSPClause ct cla
diags = Result.diags transL
mres = Result.maybeResult transL
in
case (Result.hasErrors diags) of
True -> Result.fatal_error "Translation impossible" Id.nullRange
"All fine" $
Just $ (AS_Anno.makeNamed inName (unwrapMaybe mres))
{
AS_Anno.isAxiom = isAx
, AS_Anno.isDef = isDef
, AS_Anno.wasTheorem = wasTh
}
-- | Helper to get out of the Maybe Monad
unwrapMaybe :: Maybe a -> a
unwrapMaybe (Just yv) = yv
unwrapMaybe Nothing = error "Cannot unwrap Nothing"
-- | translation of clauses
translateNSPClause :: Sig.SPClauseType -- Clause Type is needed
-> Sig.NSPClause -- the clause
-> Result.Result PBasic.FORMULA -- output Formula can fail
translateNSPClause ct inClause =
case ct of
Sig.SPCNF -> translateCNF inClause
Sig.SPDNF -> translateDNF inClause
-- | the simple translation of Literals
translateLiteral :: Sig.SPLiteral -> PBasic.FORMULA
translateLiteral lt =
case lt of
Sig.NSPNotId idF -> PBasic.Negation
(
)
-- | Enforced translation of CNF clauses
translateCNF frm =
case frm of
"All fine" $
Just $ case (length lits) of
1 -> translateLiteral $ head lits
_ -> PBasic.Disjunction
(map translateLiteral lits)
_ -> Result.fatal_error "Translation impossible" Id.nullRange
-- | Enforced translation of DNF clauses
translateDNF frm =
case frm of
"All fine" $
Just $ case (length lits) of
1 -> translateLiteral $ head lits
_ -> PBasic.Conjunction
(map translateLiteral lits)
_ -> Result.fatal_error "Translation impossible" Id.nullRange
translateClauseList :: Sig.SPClauseList -> Sig.SPSetting -> Result.Result [AS_Anno.Named PBasic.FORMULA]
translateClauseList clist inSetting =
let
clauseType = Sig.clauseType clist
clauses = Sig.clauses clist
tclauses = map (translateSPClause clauseType) clauses
nclauses = map (Result.maybeResult) tclauses
hasErrors = foldl (\xh yh -> xh && (Result.hasErrors $ Result.diags yh)) True tclauses
in
case hasErrors of
True ->
if clauses == []
then
do
Result.maybeToResult Id.nullRange "All fine" $ Just $
joinClause clauseType inSetting []
else
Result.fatal_error ("Cannot translate clause list" ++ show clist) Id.nullRange
False -> let theClauses =
map (\xv -> case xv of
Just yv -> yv
_ -> error "Bailing out in translateClauseList..."
) nclauses
in
do
Result.maybeToResult Id.nullRange "All fine" $ Just $
joinClause clauseType inSetting theClauses
-- | Translation of the logical part of SPASS to Propositional
translateLogicalPart :: Sig.SPLogicalPart -> Sig.SPSetting -> Result.Result [AS_Anno.Named PBasic.FORMULA]
translateLogicalPart spLog inSetting =
let
clauseLists = filterSPCL $ Sig.clauseLists spLog
outLists = map (\xv -> translateClauseList xv inSetting) clauseLists
outForm = map (Result.maybeResult) outLists
hasErrors = foldl (\xh yh -> xh && (Result.hasErrors $ Result.diags yh)) True outLists
in
if clauseLists == []
then
Result.maybeToResult Id.nullRange "All fine" $ Just $
[]
else
case hasErrors of
True -> Result.fatal_error ("Cannot translate logical part" ++ show spLog) Id.nullRange
False ->
let theFormulae = concat $
map (\xv -> case xv of
Just yv -> yv
_ -> error "Bailing out in translateLogicalPart..."
) outForm
in
Result.maybeToResult Id.nullRange "All fine" $ Just $
theFormulae
-- | Determines the output signature
getOutputSign :: Sig.SPSymbolList -> PSign.Sign
getOutputSign inList =
let
preds = Sig.predicates inList
in
{
foldl (\ xv yv -> Set.insert yv xv) Set.empty $
map translateSymbol preds
}
translateSymbol :: Sig.SPSignSym -> Id.Id
translateSymbol inSym =
case inSym of
Sig.SPSignSym name _ ->
Id.simpleIdToId $ Id.mkSimpleId name
Sig.SPSimpleSignSym name ->
Id.simpleIdToId $ Id.mkSimpleId name
-- | Translation of a SPASS Problem to propositional
translateProblem spProb =
let
logicalPart = Sig.logicalPart spProb
setting = head $ Sig.settings spProb
in
translateLogicalPart logicalPart setting
-- | Translation of Propositional theories to CNF
translateToCNF (sig, forms) =
case forms of
[] -> Result.maybeToResult Id.nullRange "Empty" $ Just $ (sig, [])
_ ->
let pState = createInitProverState sig forms
outProb = runSPASSandParseDFG pState safeDFGFiles
translation = translateProblem outProb
pDiags = Result.diags translation
pMaybe = Result.maybeResult translation
hasErrs = Result.hasErrors pDiags
mSymList = Sig.symbolList $ Sig.logicalPart outProb
outSymList =
case mSymList of
Just xsym -> getOutputSign xsym
_ -> sig
in
case hasErrs of
True -> Result.fatal_error ("Translation to CNF encountered errors... Bailing out...") Id.nullRange
False -> let re = (\xv -> case xv of
Just yv -> yv
_ -> error "Bailing out in translateToCNF..."
) pMaybe
in
Result.maybeToResult Id.nullRange "All fine" $ Just $
(outSymList, restoreContext forms re)
-- | Translation of a sentence to CNF
translateSentenceToCNF :: PSign.Sign
translateSentenceToCNF sig form =
let
emptyNamed = AS_Anno.makeNamed "axToTranslate" form
outCNF = translateToCNF (sig, [emptyNamed])
out = Result.maybeResult outCNF
diags = Result.diags outCNF
hasErrors = Result.hasErrors diags
in
case hasErrors of
True -> Result.fatal_error ("Translation of sentence " ++
(show $ pretty form) ++ (" failed"))
_ ->
let
outData = (\xv -> case xv of
Just yv -> yv
_ -> error "Failed!!!"
) out
outFrm = AS_Anno.sentence $ head $ snd outData
in
Result.maybeToResult Id.nullRange "All fine" $ Just $ outFrm
-- | Filtering of empty ClauseLists
emptySPCL :: Sig.SPClauseList -> Bool
emptySPCL clist =
let
clauses = Sig.clauses clist
in
clauses == []
filterSPCL :: [Sig.SPClauseList] -> [Sig.SPClauseList]
filterSPCL clist = filter (\xv -> not $ emptySPCL xv) clist