a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-------------------------------------------------------------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- GMP

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- Copyright 2007, Lutz Schroeder and Georgel Calin

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-------------------------------------------------------------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule Main where

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Text.ParserCombinators.Parsec

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport System.Environment

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport IO

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport GMPAS

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport GMPSAT

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport GMPParser

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport ModalLogic

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport ModalK()

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport ModalKD()

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport GradedML()

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport CoalitionL()

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport GenericML()

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Lexer

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach--import qualified Data.Set as Set

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-------------------------------------------------------------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- Funtion to run parser & print

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-------------------------------------------------------------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachrunLex :: (Ord a, Show a, ModalLogic a b) => Parser (Formula a) -> String -> IO ()

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachrunLex p input = run (do

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach whiteSpace

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ; x <- p

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ; eof

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ; return x

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ) input

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachrun :: (Ord a, Show a, ModalLogic a b) => Parser (Formula a) -> String -> IO ()

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachrun p input

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach = case (parse p "" input) of

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Left err -> do putStr "parse error at "

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ;print err

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Right x -> do {-print "PV list:"

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach let ls = guessPV x ---------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach print ls{-

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach let h = if ((not.null) ls) then head(ls)------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach else Set.empty-----

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach print h ------------ FOR TESTING -------------}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach let lro = map roFromPV ls --------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach print "Rho val from the above PV:"

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach print lro ------------------------------------}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach print "the Formula:"

print x

let sat = checksat x

if sat then print "is Satisfiable"

else print "is not Satisfiable"

-------------------------------------------------------------------------------

-- For Testing

-------------------------------------------------------------------------------

runTest :: Int -> FilePath -> IO ()

runTest ml p = do

input <- readFile (p)

case ml of

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

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

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

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

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

return ()

help :: IO()

help = do

putStrLn ( "Usage:\n" ++

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

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

" 2 for KD ML\n" ++

" 3 for Coalition L\n" ++

" 4 for Graded ML\n" ++

" _ for Generic ML\n" ++

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

-------------------------------------------------------------------------------

main :: IO()

main = do

args <- getArgs

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

then help

else let ml = head args

p = head (tail args)

in runTest (read ml) p