Prop2CNF.hs revision 4e9e95ba35a68f3c767bc0b23ebf9e904e442517
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : Helper functions for CNF translation
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : luecke@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : experimental
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (imports Logic.Logic)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederHelper functions for the translation of propositional formulae to CNF. We are
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maederusing SPASS -Flotter=1 here
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder http://en.wikipedia.org/wiki/Propositional_logic
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder What is a Logic?.
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ToDo: clause formula relation to SPASS Parser + AS
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder add analysis for clause formula
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder put the stuff together
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder translateToCNF -- CNF conversion via SPASS
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified Comorphisms.SuleCFOL2SoftFOL as C2S
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified Logic.Coerce as LC
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified Logic.Comorphism as Com
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified Propositional.AS_BASIC_Propositional as PBasic
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified Propositional.Prop2CASLHelpers as P2C
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified Propositional.Sign as PSign
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified SoftFOL.Conversions as Conv
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified SoftFOL.DFGParser as SParse
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified SoftFOL.ProverState as PState
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederimport qualified SoftFOL.Sign as Sig
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichimport qualified SoftFOL.Translate as Translate
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified CASL.Logic_CASL as CLogic
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maederimport qualified Common.AS_Annotation as AS_Anno
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified Common.Id as Id
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified Common.Result as Result
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified Common.Exception as Exception
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified Data.Set as Set
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedersafeDFGFiles ::Bool
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedersafeDFGFiles = False
8cacad2a09782249243b80985f28e9387019fe40Christian Maederprover_name :: String
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederprover_name = "SPASS"
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- This hack is needed to break up a cicle in imports :(
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedermap_theory :: (PSign.Sign, [AS_Anno.Named PBasic.FORMULA])
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> Result.Result (Sig.Sign, [AS_Anno.Named Sig.SPTerm])
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder ti2' <- LC.coerceBasicTheory (CLogic.CASL) (Com.sourceLogic C2S.SuleCFOL2SoftFOL)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder "Mapping theory along comorphism" ti2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Com.wrapMapTheory C2S.SuleCFOL2SoftFOL ti2'
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- | Shortcut for the translation of the theory
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedergetTheory :: (PSign.Sign, [AS_Anno.Named PBasic.FORMULA])
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder -> Result.Result (Sig.Sign, [AS_Anno.Named Sig.SPTerm])
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedergetTheory = map_theory
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | forget the internal settings for a while
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- this is no loss, since we have to restore them
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdementia frm = map (\xv ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- | Initial ProverState for Spass
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercreateInitProverState :: PSign.Sign
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedercreateInitProverState sign nForms =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let (osig, oth) =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder case Result.maybeResult $ getTheory (sign, dementia nForms) of
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Just (xs,ys) -> (xs,ys)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Nothing -> error "Should not happen... Error in Prop2CNF"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Runs SPASS. SPASS is assumed to reside in PATH.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederrunSpass :: PState.SoftFOLProverState -- Spass Prover state... Theory + Sig
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> Bool -- ^ True means save DFG file
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> IO String -- Placeholder
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederrunSpass sps saveDFG =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder spass <- newChildProcess prover_name [CP.arguments allOptions]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Exception.catch (runSpassReal spass)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (\ excep -> do
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- kill spass process
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder destroy spass
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder _ <- waitForChildProcess spass
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return ("SPASS not found... Bailing out!!! Cause was: "
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ++ show excep
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder runSpassReal spass = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- check if SPASS is running
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder e <- getToolStatus spass
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder then error "Something is wrong"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder prob <- showDFGProblem "Translation" sps (filteredOptions)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (writeFile ("FlotterIn.dfg") prob)
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder sendMsg spass prob
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder flotterOut <- parseIt spass isEnd
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder (writeFile ("FlotterOut.dfg") flotterOut)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder return flotterOut
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder filteredOptions = ["-Auto=0","-Flotter=1","-Stdin=1", "-CNFOptSkolem=0",
afa6ceaf4359ae437aaa6830949583143ace2752Christian Maeder "-CNFStrSkolem=0"
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich allOptions = filteredOptions
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich Pretty printing SPASS goal in DFG format.
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichshowDFGProblem :: String -- ^ theory name
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> PState.SoftFOLProverState -- ^ prover state containing
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- initial logical part
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> [String] -- ^ extra options
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> IO String -- ^ formatted output of the goal
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedershowDFGProblem thName pst opts = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder prob <- Conv.genSoftFOLProblem thName (PState.initialLogicalPart pst) $ Nothing
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- add SPASS command line settings and extra options
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder let prob' = prob { Sig.settings = (Sig.settings prob) ++
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder return $ showDoc prob' ""
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | We are searching for Flotter needed to determine the end of input
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederisEnd :: String -> Bool
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederisEnd inS = isPrefixOf "FLOTTER needed" inS
b7e6a2daa94ea6370ad121a7b72495dc4d8e6749Christian Maeder-- | Main function for run SPASS and Parse
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederrunSPASSandParseDFG :: PState.SoftFOLProverState -- Spass Prover state... Theory + Sig
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> Bool -- True means save DFG file
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -> IO Sig.SPProblem -- Output AS
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederrunSPASSandParseDFG pstate save =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder fmap parseDFG $ runSpass pstate save
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | run the DFG Parser
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederparseDFG :: String -> Sig.SPProblem
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederparseDFG input
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder = case (parse SParse.parseSPASS "" input) of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Left err -> error $ "parse error at " ++ show err
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder Right xv -> xv
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder-- | Restore the values of the named fields in Formulae
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian MaederrestoreContext :: [AS_Anno.Named PBasic.FORMULA] -- Input Formulae
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -> [AS_Anno.Named PBasic.FORMULA] -- Translated Formula
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus LuettichrestoreContext [] [] = []
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederrestoreContext [] _ = []
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederrestoreContext xs (yv:ys) =
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers frm = head $ filter (\xv -> (trNm $ AS_Anno.senAttr xv) == trName) xs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ] ++ restoreContext xs ys
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederrestoreContext _ _ = []
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Join different clauses to a single CNF-Formula
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederjoinClause inCt inSetting inFrm =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder case inFrm of
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers _ -> joinClauseHelper inCt (determineClauseNames inSetting) inSetting inFrm
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Join Clauses according to the Clause-Formula-Relation
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederjoinClauseHelper :: Sig.SPClauseType
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederjoinClauseHelper inCt inSet inSetting inFrm =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case (Set.null inSet) of
fe37265aaad6667f65d979a6cebbe145ef8b512bChristian Maeder smallestElem = Set.findMin inSet
e2d849b4152a234bc0afaa2ab3a7c17d28de7565Christian Maeder clauses = filterClauseNames smallestElem inSetting inFrm
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder nakedForms = map (AS_Anno.sentence) clauses
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder firstForm = head clauses
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder inName = smallestElem
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder isAx = AS_Anno.isAxiom firstForm
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder isDef = AS_Anno.isDef firstForm
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder wasTh = AS_Anno.wasTheorem firstForm
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Sig.SPCNF -> [(AS_Anno.makeNamed inName (PBasic.Conjunction nakedForms Id.nullRange))
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke ++ (joinClauseHelper inCt newSet inSetting inFrm)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Sig.SPDNF -> [(AS_Anno.makeNamed inName (PBasic.Disjunction nakedForms Id.nullRange))
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ++ (joinClauseHelper inCt newSet inSetting inFrm)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | get Clauses with a particular name
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederfilterClauseNames :: String -> Sig.SPSettingBody -> [AS_Anno.Named PBasic.FORMULA] -> [AS_Anno.Named PBasic.FORMULA]
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian MaederfilterClauseNames name setting frms =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (\xy -> case xy of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- sign of list_of_settings is changed, see
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich _ -> error "Wrong type"
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich thisNames = map (Sig.clauseSPR) $ filter (\xv -> Sig.formulaSPR xv == name) clrel
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich namesSet = foldl (\yv xv -> Set.insert xv yv) Set.empty thisNames
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich filter (\xv -> Set.member (AS_Anno.senAttr xv) namesSet) frms
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- | determine all names for clauses that occur
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederdetermineClauseNames :: Sig.SPSettingBody -> Set.Set String
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaederdetermineClauseNames xs =
b10267ae0a6523b73113fc2dee9ea628266fce60Christian Maeder foldl (\yv xv -> Set.insert (Sig.formulaSPR xv) yv) Set.empty
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder (\xy -> case xy of
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich _ -> error "Wrong type"
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder-- | Translation of named clauses
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedertranslateSPClause :: Sig.SPClauseType -- Clause Type is needed
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -> Result.Result (AS_Anno.Named PBasic.FORMULA)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedertranslateSPClause ct nspc = do
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder cla' <- case AS_Anno.sentence nspc of
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich Sig.QuanClause _ sc -> return sc
08e5741dd8b6bf9b7419e89298e384e18bc57f64Christian Maeder Sig.BriefClause _ (Sig.TWL l1 _) (Sig.TWL l2 _) -> do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let s3 = map (\ (Sig.SPLiteral b s) -> Sig.SPLiteral (not b) s) s2
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return $ Sig.NSPClauseBody Sig.SPCNF $ s1 ++ s3
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder transL <- translateNSPClause ct cla'
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder return nspc { AS_Anno.sentence = transL }
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | the simple translation of Literals
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedertranslateLiteral :: Sig.SPLiteral -> PBasic.FORMULA
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedertranslateLiteral (Sig.SPLiteral b l) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (if b then id else flip PBasic.Negation Id.nullRange)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Sig.SPTrue -> PBasic.True_atom Id.nullRange
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich Sig.SPFalse -> PBasic.False_atom Id.nullRange
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich Sig.SPCustomSymbol idF -> PBasic.Predication idF
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich _ -> PBasic.Predication $ Id.mkSimpleId $ Sig.showSPSymbol l
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | translation of clauses
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian MaedertranslateNSPClause :: Sig.SPClauseType -> Sig.NSPClauseBody
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian MaedertranslateNSPClause ct frm =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Sig.NSPClauseBody ct2 lits | ct == ct2 ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Result.maybeToResult Id.nullRange "All fine" $ Just $ case lits of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [hd] -> translateLiteral hd
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich _ -> (case ct of
5958fabb264ec3f5b2125ac5602121bd34814a79Klaus Luettich (map translateLiteral lits) Id.nullRange
c9e197862d9d8ef2585270dd08f5194b3aed4a9dKlaus Luettich _ -> Result.fatal_error "Translation impossible" Id.nullRange
ef67402074be14deb95e4ff564737d5593144130Klaus LuettichtranslateClauseList :: Sig.SPClauseList -> Sig.SPSettingBody -> Result.Result [AS_Anno.Named PBasic.FORMULA]
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus LuettichtranslateClauseList clist inSetting =
d784803f9c752667b4fcf7393d698002bedf3f89Klaus Luettich clauseType = Sig.clauseType clist
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich clauses = Sig.clauses clist
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich tclauses = map (translateSPClause clauseType) clauses
725a68ec81cba9b8aa8647bebfb5baa449803e7eKlaus Luettich nclauses = map (Result.maybeResult) tclauses
d579f5b263e6c73d466c265f2fbfd45b0e69ca64Klaus Luettich hasErrors = foldl (\xh yh -> xh && (Result.hasErrors $ Result.diags yh)) True tclauses
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case hasErrors of
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder if clauses == []
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder Result.maybeToResult Id.nullRange "All fine" $ Just $
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich joinClause clauseType inSetting []
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Result.fatal_error ("Cannot translate clause list" ++ show clist) Id.nullRange
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder False -> let theClauses =
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich map (\xv -> case xv of
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder Just yv -> yv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder _ -> error "Bailing out in translateClauseList..."
e94af996596c87e8d835094ea6a186e69bf9c489Christian Maeder Result.maybeToResult Id.nullRange "All fine" $ Just $
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder joinClause clauseType inSetting theClauses
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- | Translation of the logical part of SPASS to Propositional
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaedertranslateLogicalPart :: Sig.SPLogicalPart -> Sig.SPSettingBody -> IO [AS_Anno.Named PBasic.FORMULA]
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedertranslateLogicalPart spLog inSetting =
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder clauseLists = filterSPCL $ Sig.clauseLists spLog
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder outLists = map (\xv -> translateClauseList xv inSetting) clauseLists
9c3edf2b283c09d33b2820696886d1ed32fcadc8Christian Maeder outForm = map (Result.maybeResult) outLists
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder hasErrors = foldl (\xh yh -> xh && (Result.hasErrors $ Result.diags yh)) True outLists
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder if clauseLists == []
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case hasErrors of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder True -> fail ("Cannot translate logical part" ++ show spLog)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder let theFormulae = concat $
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder map (\xv -> case xv of
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder Just yv -> yv
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder _ -> error "Bailing out in translateLogicalPart..."
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder return theFormulae
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder-- | Determines the output signature
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus LuettichgetOutputSign :: Sig.SPSymbolList -> PSign.Sign
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus LuettichgetOutputSign inList =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder foldl (\ xv yv -> Set.insert yv xv) Set.empty $
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder map translateSymbol preds
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedertranslateSymbol inSym = case inSym of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Sig.SPSignSym name _ -> Id.simpleIdToId name
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Sig.SPSimpleSignSym name -> Id.simpleIdToId name
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- | Translation of a SPASS Problem to propositional
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedertranslateProblem :: Sig.SPProblem -> IO [AS_Anno.Named PBasic.FORMULA]
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedertranslateProblem spProb =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder logicalPart = Sig.logicalPart spProb
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder setting = head $ Sig.settings spProb
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- data of setting of list_of_setting is changed, see
afa6ceaf4359ae437aaa6830949583143ace2752Christian Maeder case setting of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder translateLogicalPart logicalPart (head sb)
afa6ceaf4359ae437aaa6830949583143ace2752Christian Maeder _ -> error "clause formula relation is not set."
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- | Translation of Propositional theories to CNF
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedertranslateToCNF :: (PSign.Sign, [AS_Anno.Named PBasic.FORMULA])
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -> IO (PSign.Sign, [AS_Anno.Named PBasic.FORMULA])
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedertranslateToCNF (sig, forms) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case forms of
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder [] -> return (sig, [])
ba0ec5e897ef99d420c8c14c2374e0f32b7043dbKlaus Luettich let pState = createInitProverState sig forms
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder outProb <- runSPASSandParseDFG pState safeDFGFiles
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder mSymList = Sig.symbolList $ Sig.logicalPart outProb
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich case mSymList of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just xsym -> getOutputSign xsym
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder re <- translateProblem outProb
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return $ (outSymList, restoreContext forms re)
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder-- | Filtering of empty ClauseLists
b9625461755578f3eed04676d42a63fd2caebd0cChristian MaederemptySPCL :: Sig.SPClauseList -> Bool
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederemptySPCL clist =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder clauses = Sig.clauses clist
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder clauses == []
d67a33b40578beef2e255a274f89bb9c34aaf056Christian MaederfilterSPCL :: [Sig.SPClauseList] -> [Sig.SPClauseList]
23ab8855c58adfbd03a0730584b917b24c603901Christian MaederfilterSPCL clist = filter (\xv -> not $ emptySPCL xv) clist