abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- this has to be modified

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-------------------------------------------------------------------------------

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-- GMP

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- Copyright 2007, Lutz Schroeder and Georgel Calin

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu-------------------------------------------------------------------------------

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maedermodule Main where

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederimport Text.ParserCombinators.Parsec

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederimport System.Environment

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederimport IO

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport GMPAS

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport GMPSAT

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport GMPParser

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport ModalLogic

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport ModalK()

d48085f765fca838c1d972d2123601997174583dChristian Maederimport ModalKD()

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport GradedML()

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport CoalitionL()

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport GenericML()

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport Lexer

d48085f765fca838c1d972d2123601997174583dChristian Maeder-------------------------------------------------------------------------------

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder-- Funtion to run parser & print

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder-------------------------------------------------------------------------------

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederrunLex :: (Ord a, Show a, ModalLogic a b) => Parser (Formula a) -> String -> IO ()

72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederrunLex p input = run (do

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder whiteSpace

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder ; x <- p

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ; eof

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder ; return x

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder ) input

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maederrun :: (Ord a, Show a, ModalLogic a b) => Parser (Formula a) -> String -> IO ()

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederrun p input

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder = case (parse p "" input) of

413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Left err -> do putStr "parse error at "

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ;print err

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Right x -> do -- let sat = checksat x

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- print "SAT test answer:"

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- print sat

8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder let ls = guessPV x ----------------------------

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder let h = head(ls) -----------------------------

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder print "Head of PV list:"

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder print h ------------ FOR TESTING -------------

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let lro = roFromPV (h) -----------------------

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder print "Rho val from the above PV:"

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder print lro ------------------------------------

8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder print "the Formula:"

2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder print x

2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder-------------------------------------------------------------------------------

2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder-- For Testing

2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder-------------------------------------------------------------------------------

2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederrunTest :: Int -> FilePath -> IO ()

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederrunTest ml p = do

120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder input <- readFile (p)

120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder case ml of

120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder 1 -> runLex (par5er parseIndex :: Parser (Formula ModalK)) input

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder 2 -> runLex (par5er parseIndex :: Parser (Formula ModalKD)) input

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder 3 -> runLex (par5er parseIndex :: Parser (Formula CL)) input

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder 4 -> runLex (par5er parseIndex :: Parser (Formula Integer)) input

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder _ -> runLex (par5er parseIndex :: Parser (Formula Kars)) input

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder return ()

df33a9af92444f63ad545da6bb326aac9284318eChristian Maederhelp :: IO()

df33a9af92444f63ad545da6bb326aac9284318eChristian Maederhelp = do

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder putStrLn ( "Usage:\n" ++

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder " ./main <ML> <path>\n\n" ++

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder "<ML>: 1 for K ML\n" ++

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder " 2 for KD ML\n" ++

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder " 3 for Coalition L\n" ++

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder " 4 for Graded ML\n" ++

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder " _ for Generic ML\n" ++

df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder "<path>: path to input file\n" )

120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder-------------------------------------------------------------------------------

ce3928e71520030ad0275b72050a8f4377f9313cChristian Maedermain :: IO()

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermain = do

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder args <- getArgs

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder if (args == [])||(head args == "--help")||(length args < 2)

c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder then help

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else let ml = head args

2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder p = head (tail args)

2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder in runTest (read ml) p

2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder