module Language.SMTLIB
(
Numeral
, Symbol
, Keyword
, Spec_constant (..)
, S_expr (..)
, Identifier (..)
, Sort (..)
, Attribute_value (..)
, Attribute (..)
, Qual_identifier (..)
, Var_binding (..)
, Sorted_var (..)
, Term (..)
, Sort_symbol_decl (..)
, Meta_spec_constant (..)
, Fun_symbol_decl (..)
, Par_fun_symbol_decl (..)
, Theory_attribute (..)
, Theory_decl (..)
, Logic_attribute (..)
, Logic (..)
, Option (..)
, Info_flag (..)
, Command (..)
, Script (..)
, Gen_response (..)
, Error_behavior (..)
, Reason_unknown (..)
, Status (..)
, Info_response (..)
, Proof
, Valuation_pair
, T_valuation_pair
, Command_response (..)
, parseScript
, parseResponses
, parseTheory
, parseLogic
, checkScript
, checkResponses
, checkParser
) where
import Data.List hiding (group)
import System.Directory
import System.IO
import Text.ParserCombinators.Poly.Lazy hiding (Success)
import Text.Printf
import Language.SMTLIB.Lexer
type Numeral = Integer
type Symbol = String
type Keyword = String
data Spec_constant
= Spec_constant_numeral Numeral
| Spec_constant_decimal Rational
| Spec_constant_hexadecimal String
| Spec_constant_binary [Bool]
| Spec_constant_string String
instance Show Spec_constant where
show a = case a of
Spec_constant_numeral a -> show a
Spec_constant_decimal a -> show (realToFrac a :: Double)
Spec_constant_hexadecimal a -> printf "#x%s" a
Spec_constant_binary a -> printf "#b%s" [ if a then '1' else '0' | a <- a ]
Spec_constant_string a -> show a
spec_constant :: SMTLIB Spec_constant
spec_constant = oneOf
[ numeral >>= return . Spec_constant_numeral
, string >>= return . Spec_constant_string
, do
a <- satisfy (\ a -> case a of { Decimal _ -> True; Hex _ -> True; Bin _ -> True; _ -> False })
case a of
Decimal a -> return $ Spec_constant_decimal $ toRational a
Hex a -> return $ Spec_constant_hexadecimal a
Bin a -> return $ Spec_constant_binary $ map (== '1') a
_ -> undefined
]
data S_expr
= S_expr_constant Spec_constant
| S_expr_symbol Symbol
| S_expr_keyword Keyword
| S_exprs [S_expr]
instance Show S_expr where
show a = case a of
S_expr_constant a -> show a
S_expr_symbol a -> a
S_expr_keyword a -> a
S_exprs a -> group $ map show a
s_expr :: SMTLIB S_expr
s_expr = oneOf
[ spec_constant >>= return . S_expr_constant
, symbol >>= return . S_expr_symbol
, keyword >>= return . S_expr_keyword
, do { left; a <- many s_expr; right; return $ S_exprs a }
]
data Identifier
= Identifier Symbol
| Identifier_ Symbol [Numeral]
instance Show Identifier where
show a = case a of
Identifier a -> a
Identifier_ a b -> group $ ["_", a] ++ map show b
identifier :: SMTLIB Identifier
identifier = oneOf
[ symbol >>= return . Identifier
, do { left; tok (Symbol "_"); a <- symbol; b <- many1 numeral; right; return $ Identifier_ a b }
]
data Sort
= Sort_bool
| Sort_identifier Identifier
| Sort_identifiers Identifier [Sort]
instance Show Sort where
show a = case a of
Sort_bool -> "Bool"
Sort_identifier a -> show a
Sort_identifiers a b -> group $ show a : map show b
sort' :: SMTLIB Sort
sort' = oneOf
[ tok (Symbol "Bool") >> return Sort_bool
, identifier >>= return . Sort_identifier
, do { left; a <- identifier; b <- many1 sort'; right; return $ Sort_identifiers a b }
]
data Attribute_value
= Attribute_value_spec_constant Spec_constant
| Attribute_value_symbol Symbol
| Attribute_value_s_expr [S_expr]
instance Show Attribute_value where
show a = case a of
Attribute_value_spec_constant a -> show a
Attribute_value_symbol a -> a
Attribute_value_s_expr a -> group $ map show a
attribute_value :: SMTLIB Attribute_value
attribute_value = oneOf
[ spec_constant >>= return . Attribute_value_spec_constant
, symbol >>= return . Attribute_value_symbol
, do { left; a <- many s_expr; right; return $ Attribute_value_s_expr a }
]
data Attribute
= Attribute Keyword
| Attribute_s_expr Keyword S_expr
instance Show Attribute where
show a = case a of
Attribute a -> a
Attribute_s_expr a b -> a ++ " " ++ show b
attribute :: SMTLIB Attribute
attribute = oneOf
[ do { a <- keyword; b <- s_expr; return $ Attribute_s_expr a b }
, keyword >>= return . Attribute
]
data Qual_identifier
= Qual_identifier Identifier
| Qual_identifier_sort Identifier Sort
instance Show Qual_identifier where
show a = case a of
Qual_identifier a -> show a
Qual_identifier_sort a b -> group ["as", show a, show b]
qual_identifier :: SMTLIB Qual_identifier
qual_identifier = oneOf
[ identifier >>= return . Qual_identifier
, do { left; tok $ Symbol "as"; a <- identifier; b <- sort'; right; return $ Qual_identifier_sort a b }
]
data Var_binding
= Var_binding Symbol Term
instance Show Var_binding where
show a = case a of
Var_binding a b -> group [a, show b]
var_binding :: SMTLIB Var_binding
var_binding = do { left; a <- symbol; b <- term; right; return $ Var_binding a b }
data Sorted_var
= Sorted_var Symbol Sort
instance Show Sorted_var where
show a = case a of
Sorted_var a b -> group [a, show b]
sorted_var :: SMTLIB Sorted_var
sorted_var = do { left; a <- symbol; b <- sort'; right; return $ Sorted_var a b }
data Term
= Term_spec_constant Spec_constant
| Term_qual_identifier Qual_identifier
| Term_qual_identifier_ Qual_identifier [Term]
| Term_distinct Term [Term]
| Term_let [Var_binding] Term
| Term_forall [Sorted_var] Term
| Term_exists [Sorted_var] Term
| Term_attributes Term [Attribute]
instance Show Term where
show a = case a of
Term_spec_constant a -> show a
Term_qual_identifier a -> show a
Term_qual_identifier_ a b -> group $ show a : map show b
Term_distinct a b -> group $ ["distinct", show a] ++ map show b
Term_let a b -> group $ ["let", group $ map show a, show b]
Term_forall a b -> group $ ["forall", group $ map show a, show b]
Term_exists a b -> group $ ["exists", group $ map show a, show b]
Term_attributes a b -> group $ ["!", show a] ++ map show b
term :: SMTLIB Term
term = oneOf
[ spec_constant >>= return . Term_spec_constant
, qual_identifier >>= return . Term_qual_identifier
, do { left; a <- qual_identifier; b <- many1 term; right; return $ Term_qual_identifier_ a b }
, do { left; tok $ Symbol "distinct"; a <- term; b <- many1 term; right; return $ Term_distinct a b }
, do { left; tok $ Symbol "let"; left; a <- many1 var_binding; right; b <- term; right; return $ Term_let a b }
, do { left; tok $ Symbol "forall"; left; a <- many1 sorted_var; right; b <- term; right; return $ Term_forall a b }
, do { left; tok $ Symbol "exists"; left; a <- many1 sorted_var; right; b <- term; right; return $ Term_exists a b }
, do { left; tok $ Symbol "!"; a <- term; b <- many1 attribute; right; return $ Term_attributes a b }
]
data Sort_symbol_decl
= Sort_symbol_decl Identifier Numeral [Attribute]
instance Show Sort_symbol_decl where
show a = case a of
Sort_symbol_decl a b c -> group $ [show a, show b] ++ map show c
sort_symbol_decl :: SMTLIB Sort_symbol_decl
sort_symbol_decl = do { left; a <- identifier; b <- numeral; c <- many attribute; right; return $ Sort_symbol_decl a b c }
data Meta_spec_constant
= Meta_spec_constant_numeral
| Meta_spec_constant_decimal
| Meta_spec_constant_string
instance Show Meta_spec_constant where
show a = case a of
Meta_spec_constant_numeral -> "NUMERAL"
Meta_spec_constant_decimal -> "DECIMAL"
Meta_spec_constant_string -> "STRING"
meta_spec_constant :: SMTLIB Meta_spec_constant
meta_spec_constant = oneOf
[ do { tok $ Symbol "NUMERAL"; return Meta_spec_constant_numeral }
, do { tok $ Symbol "DECIMAL"; return Meta_spec_constant_decimal }
, do { tok $ Symbol "STRING" ; return Meta_spec_constant_string }
]
data Fun_symbol_decl
= Fun_symbol_decl_spec_constant Spec_constant Sort [Attribute]
| Fun_symbol_decl_meta_spec_constant Meta_spec_constant Sort [Attribute]
| Fun_symbol_decl Identifier [Sort] [Attribute]
instance Show Fun_symbol_decl where
show a = case a of
Fun_symbol_decl_spec_constant a b c -> group $ [show a, show b] ++ map show c
Fun_symbol_decl_meta_spec_constant a b c -> group $ [show a, show b] ++ map show c
Fun_symbol_decl a b c -> group $ [show a] ++ map show b ++ map show c
fun_symbol_decl :: SMTLIB Fun_symbol_decl
fun_symbol_decl = oneOf
[ do { left; a <- spec_constant; b <- sort'; c <- many attribute; right; return $ Fun_symbol_decl_spec_constant a b c }
, do { left; a <- meta_spec_constant; b <- sort'; c <- many attribute; right; return $ Fun_symbol_decl_meta_spec_constant a b c }
, do { left; a <- identifier; b <- many1 sort'; c <- many attribute; right; return $ Fun_symbol_decl a b c }
]
data Par_fun_symbol_decl
= Par_fun_symbol_decl Fun_symbol_decl
| Par_fun_symbol_decl_symbols [Symbol] Identifier [Sort] [Attribute]
instance Show Par_fun_symbol_decl where
show a = case a of
Par_fun_symbol_decl a -> show a
Par_fun_symbol_decl_symbols a b c d -> group ["par", group $ map show a, group $ [show b] ++ map show c ++ map show d]
par_fun_symbol_decl :: SMTLIB Par_fun_symbol_decl
par_fun_symbol_decl = oneOf
[ fun_symbol_decl >>= return . Par_fun_symbol_decl
, do { left; tok $ Symbol "par"; left; a <- many1 symbol; right; left; b <- identifier; c <- many1 sort'; d <- many attribute; right; right; return $ Par_fun_symbol_decl_symbols a b c d }
]
data Theory_attribute
= Theory_attribute_sorts [Sort_symbol_decl]
| Theory_attribute_funs [Par_fun_symbol_decl]
| Theory_attribute_sorts_desc String
| Theory_attribute_funs_desc String
| Theory_attribute_definition String
| Theory_attribute_values String
| Theory_attribute_notes String
| Theory_attribute Attribute
instance Show Theory_attribute where
show a = case a of
Theory_attribute_sorts a -> ":sorts " ++ group (map show a)
Theory_attribute_funs a -> ":funs " ++ group (map show a)
Theory_attribute_sorts_desc a -> ":sorts-description " ++ show a
Theory_attribute_funs_desc a -> ":funs-description " ++ show a
Theory_attribute_definition a -> ":definition " ++ show a
Theory_attribute_values a -> ":values " ++ show a
Theory_attribute_notes a -> ":notes " ++ show a
Theory_attribute a -> show a
theory_attribute :: SMTLIB Theory_attribute
theory_attribute = oneOf
[ do { tok $ Keyword ":sorts"; left; a <- many1 sort_symbol_decl; right; return $ Theory_attribute_sorts a }
, do { tok $ Keyword ":funs"; left; a <- many1 par_fun_symbol_decl; right; return $ Theory_attribute_funs a }
, do { tok $ Keyword ":sorts-description"; a <- string; return $ Theory_attribute_sorts_desc a }
, do { tok $ Keyword ":funs-description"; a <- string; return $ Theory_attribute_funs_desc a }
, do { tok $ Keyword ":definition"; a <- string; return $ Theory_attribute_definition a }
, do { tok $ Keyword ":values"; a <- string; return $ Theory_attribute_values a }
, do { tok $ Keyword ":notes"; a <- string; return $ Theory_attribute_notes a }
, attribute >>= return . Theory_attribute
]
data Theory_decl
= Theory_decl Symbol [Theory_attribute]
instance Show Theory_decl where
show a = case a of
Theory_decl a b -> group $ ["theory", show a] ++ map show b
theory_decl :: SMTLIB Theory_decl
theory_decl = do { left; tok $ Symbol "theory"; a <- symbol; b <- many1 theory_attribute; right; return $ Theory_decl a b }
data Logic_attribute
= Logic_attribute_theories [Symbol]
| Logic_attribute_language String
| Logic_attribute_extensions String
| Logic_attribute_values String
| Logic_attribute_notes String
| Logic_attribute Attribute
instance Show Logic_attribute where
show a = case a of
Logic_attribute_theories a -> ":theories " ++ group (map show a)
Logic_attribute_language a -> ":language " ++ show a
Logic_attribute_extensions a -> ":extensions " ++ show a
Logic_attribute_values a -> ":values " ++ show a
Logic_attribute_notes a -> ":notes " ++ show a
Logic_attribute a -> show a
logic_attribute :: SMTLIB Logic_attribute
logic_attribute = oneOf
[ do { tok $ Keyword ":theories"; left; a <- many1 symbol; right; return $ Logic_attribute_theories a }
, do { tok $ Keyword ":language"; left; a <- string; right; return $ Logic_attribute_language a }
, do { tok $ Keyword ":extensions"; left; a <- string; right; return $ Logic_attribute_extensions a }
, do { tok $ Keyword ":values"; left; a <- string; right; return $ Logic_attribute_values a }
, do { tok $ Keyword ":notes"; left; a <- string; right; return $ Logic_attribute_notes a }
, attribute >>= return . Logic_attribute
]
data Logic
= Logic Symbol [Logic_attribute]
instance Show Logic where
show a = case a of
Logic a b -> group $ ["logic", a] ++ map show b
logic :: SMTLIB Logic
logic = do { left; tok $ Symbol "logic"; a <- symbol; b <- many1 logic_attribute; right; return $ Logic a b }
data Option
= Print_success Bool
| Expand_definitions Bool
| Interactive_mode Bool
| Produce_proofs Bool
| Produce_unsat_cores Bool
| Produce_models Bool
| Produce_assignments Bool
| Regular_output_channel String
| Diagnostic_output_channel String
| Random_seed Int
| Verbosity Int
| Option_attribute Attribute
instance Show Option where
show a = case a of
Print_success a -> ":print-success " ++ showBool a
Expand_definitions a -> ":expand-definitions " ++ showBool a
Interactive_mode a -> ":interactive-mode " ++ showBool a
Produce_proofs a -> ":produce-proofs " ++ showBool a
Produce_unsat_cores a -> ":produce-unsat-cores " ++ showBool a
Produce_models a -> ":produce-models " ++ showBool a
Produce_assignments a -> ":produce-assignments " ++ showBool a
Regular_output_channel a -> ":regular-output-channel " ++ show a
Diagnostic_output_channel a -> ":diagnostic-output-channel " ++ show a
Random_seed a -> ":random-seed " ++ show a
Verbosity a -> ":verbosity " ++ show a
Option_attribute a -> show a
option :: SMTLIB Option
option = oneOf
[ do { tok $ Symbol ":print-success"; a <- b_value; return $ Print_success a }
, do { tok $ Symbol ":expand-definitions"; a <- b_value; return $ Expand_definitions a }
, do { tok $ Symbol ":interactive-mode"; a <- b_value; return $ Interactive_mode a }
, do { tok $ Symbol ":produce-proofs"; a <- b_value; return $ Produce_proofs a }
, do { tok $ Symbol ":produce-unsat-cores"; a <- b_value; return $ Produce_unsat_cores a }
, do { tok $ Symbol ":produce-models"; a <- b_value; return $ Produce_models a }
, do { tok $ Symbol ":produce-assignments"; a <- b_value; return $ Produce_assignments a }
, do { tok $ Symbol ":regular-output-channel"; a <- string; return $ Regular_output_channel a }
, do { tok $ Symbol ":diagnostic-output-channel"; a <- string; return $ Diagnostic_output_channel a }
, do { tok $ Symbol ":random-seed"; a <- numeral; return $ Random_seed $ fromIntegral a }
, do { tok $ Symbol ":verbosity"; a <- numeral; return $ Verbosity $ fromIntegral a }
, attribute >>= return . Option_attribute
]
data Info_flag
= Error_behavior
| Name
| Authors
| Version
| Status
| Reason_unknown
| Info_flag Keyword
| All_statistics
instance Show Info_flag where
show a = case a of
Error_behavior -> ":error-behavior"
Name -> ":name"
Authors -> ":authors"
Version -> ":version"
Status -> ":status"
Reason_unknown -> ":reason-unknown"
Info_flag a -> a
All_statistics -> ":all-statistics"
info_flag :: SMTLIB Info_flag
info_flag = oneOf
[ do { tok $ Keyword ":error-behavior"; return Error_behavior }
, do { tok $ Keyword ":name" ; return Name }
, do { tok $ Keyword ":authors" ; return Authors }
, do { tok $ Keyword ":version" ; return Version }
, do { tok $ Keyword ":status" ; return Status }
, do { tok $ Keyword ":reason-unknown"; return Reason_unknown }
, do { tok $ Keyword ":all-statistics"; return All_statistics }
, keyword >>= return . Info_flag
]
data Command
= Set_logic Symbol
| Set_option Option
| Set_info Attribute
| Declare_sort Symbol Numeral
| Define_sort Symbol [Symbol] Sort
| Declare_fun Symbol [Sort] Sort
| Define_fun Symbol [Sorted_var] Sort Term
| Push Int
| Pop Int
| Assert Term
| Check_sat
| Get_assertions
| Get_proof
| Get_unsat_core
| Get_value [Term]
| Get_assignment
| Get_option Keyword
| Get_info Info_flag
| Exit
instance Show Command where
show a = case a of
Set_logic a -> group ["set-logic", a]
Set_option a -> group ["set-option", show a]
Set_info a -> group ["set-info", show a]
Declare_sort a b -> group ["declare-sort", a, show b]
Define_sort a b c -> group ["define-sort", a, group (map show b), show c]
Declare_fun a b c -> group ["declare-fun", a, group (map show b), show c]
Define_fun a b c d -> group ["define_fun", a, group (map show b), show c, show d]
Push a -> group ["push", show a]
Pop a -> group ["pop", show a]
Assert a -> group ["assert", show a]
Check_sat -> group ["check-sat"]
Get_assertions -> group ["get-assertions"]
Get_proof -> group ["get-proof"]
Get_unsat_core -> group ["get-unsat-core"]
Get_value a -> group ["get-value", group $ map show a]
Get_assignment -> group ["get-assignment"]
Get_option a -> group ["get-option", a]
Get_info a -> group ["get-info", show a]
Exit -> group ["exit"]
command :: SMTLIB Command
command = oneOf
[ do { left; tok $ Symbol "set-logic"; a <- symbol; right; return $ Set_logic a }
, do { left; tok $ Symbol "set-option"; a <- option; right; return $ Set_option a }
, do { left; tok $ Symbol "set-info"; a <- attribute; right; return $ Set_info a }
, do { left; tok $ Symbol "declare-sort"; a <- symbol; b <- numeral; right; return $ Declare_sort a b }
, do { left; tok $ Symbol "define-sort"; a <- symbol; left; b <- many symbol; right; c <- sort'; right; return $ Define_sort a b c }
, do { left; tok $ Symbol "declare-fun"; a <- symbol; left; b <- many sort'; right; c <- sort'; right; return $ Declare_fun a b c }
, do { left; tok $ Symbol "define-fun"; a <- symbol; left; b <- many sorted_var; right; c <- sort'; d <- term; right; return $ Define_fun a b c d }
, do { left; tok $ Symbol "push"; a <- numeral; right; return $ Push $ fromIntegral a }
, do { left; tok $ Symbol "pop"; a <- numeral; right; return $ Pop $ fromIntegral a }
, do { left; tok $ Symbol "assert"; a <- term; right; return $ Assert a }
, do { left; tok $ Symbol "check-sat"; right; return $ Check_sat }
, do { left; tok $ Symbol "get-assertions"; right; return $ Get_assertions }
, do { left; tok $ Symbol "get-proof"; right; return $ Get_proof }
, do { left; tok $ Symbol "get-unsat-core"; right; return $ Get_unsat_core }
, do { left; tok $ Symbol "get-value"; left; a <- many1 term; right; right; return $ Get_value a }
, do { left; tok $ Symbol "get-assignment"; right; return $ Get_assignment }
, do { left; tok $ Symbol "get-option"; a <- keyword; right; return $ Get_option a }
, do { left; tok $ Symbol "get-info"; a <- info_flag; right; return $ Get_info a }
, do { left; tok $ Symbol "exit"; right; return $ Exit }
]
data Script = Script [Command]
instance Show Script where
show (Script a) = unlines $ map show a
script :: SMTLIB Script
script = return Script `apply` many command `discard` eof
data Gen_response
= Unsupported
| Success
| Error String
instance Show Gen_response where
show a = case a of
Unsupported -> "unsupported"
Success -> "sucess"
Error a -> group ["error", show a]
gen_response :: SMTLIB Gen_response
gen_response = oneOf
[ do { tok $ Symbol "unsupported"; return Unsupported }
, do { tok $ Symbol "success"; return Success }
, do { left; tok $ Symbol "error"; a <- string; right; return $ Error a }
]
data Error_behavior
= Immediate_exit
| Continued_execution
instance Show Error_behavior where
show a = case a of
Immediate_exit -> "immediate-exit"
Continued_execution -> "continued-execution"
error_behavior :: SMTLIB Error_behavior
error_behavior = oneOf
[ do { tok $ Symbol "immediate-exit"; return Immediate_exit }
, do { tok $ Symbol "continued-execution"; return Continued_execution }
]
data Reason_unknown
= Timeout
| Memout
| Incomplete
instance Show Reason_unknown where
show a = case a of
Timeout -> "timeout"
Memout -> "memout"
Incomplete -> "incomplete"
reason_unknown :: SMTLIB Reason_unknown
reason_unknown = oneOf
[ do { tok $ Symbol "timeout"; return Timeout }
, do { tok $ Symbol "memout"; return Memout }
, do { tok $ Symbol "incomplete"; return Incomplete }
]
data Status
= Sat
| Unsat
| Unknown
instance Show Status where
show a = case a of
Sat -> "sat"
Unsat -> "unsat"
Unknown -> "unknown"
status :: SMTLIB Status
status = oneOf
[ do { tok $ Symbol "sat"; return Sat }
, do { tok $ Symbol "unsat"; return Unsat }
, do { tok $ Symbol "unknown"; return Unknown }
]
data Info_response
= Info_response_error_behavior Error_behavior
| Info_response_name String
| Info_response_authors String
| Info_response_version String
| Info_response_status Status
| Info_response_reason_unknown Reason_unknown
| Info_response_attribute Attribute
instance Show Info_response where
show a = case a of
Info_response_error_behavior a -> ":error-behavior " ++ show a
Info_response_name a -> ":name " ++ show a
Info_response_authors a -> ":authors " ++ show a
Info_response_version a -> ":version " ++ show a
Info_response_status a -> ":status " ++ show a
Info_response_reason_unknown a -> ":reason-unknown " ++ show a
Info_response_attribute a -> show a
info_response :: SMTLIB Info_response
info_response = oneOf
[ do { tok $ Keyword ":error-behavior"; a <- error_behavior; return $ Info_response_error_behavior a }
, do { tok $ Keyword ":name"; a <- string; return $ Info_response_name a }
, do { tok $ Keyword ":authors"; a <- string; return $ Info_response_authors a }
, do { tok $ Keyword ":version"; a <- string; return $ Info_response_version a }
, do { tok $ Keyword ":status"; a <- status; return $ Info_response_status a }
, do { tok $ Keyword ":reason-unknown"; a <- reason_unknown; return $ Info_response_reason_unknown a }
, do attribute >>= return . Info_response_attribute
]
type Proof = S_expr
type Valuation_pair = (Term, Term)
type T_valuation_pair = (Symbol, Bool)
data Command_response
= Gen_response Gen_response
| Info_response Info_response
| Gi_response [Info_response]
| Cs_response Status
| Ga_response [Term]
| Gp_response Proof
| Guc_response [Symbol]
| Gv_response [Valuation_pair]
| Gta_response [T_valuation_pair]
instance Show Command_response where
show a = case a of
Gen_response a -> show a
Info_response a -> show a
Gi_response a -> group $ map show a
Cs_response a -> show a
Ga_response a -> group $ map show a
Gp_response a -> show a
Guc_response a -> group $ map show a
Gv_response a -> group $ [ group [(show a), (show b)] | (a, b) <- a ]
Gta_response a -> group $ [ group [(show a), (showBool b)] | (a, b) <- a ]
command_response :: SMTLIB Command_response
command_response = oneOf
[ gen_response >>= return . Gen_response
, info_response >>= return . Info_response
, do { left; a <- many1 info_response; right; return $ Gi_response a }
, status >>= return . Cs_response
, do { left; a <- many term; right; return $ Ga_response a }
, s_expr >>= return . Gp_response
, do { left; a <- many symbol; right; return $ Guc_response a }
, do { left; a <- many1 (do { left; a <- term; b <- term; return (a, b) }); right; return $ Gv_response a }
, do { left; a <- many (do { left; a <- symbol; b <- b_value; return (a, b) }); right; return $ Gta_response a }
]
responses :: SMTLIB [Command_response]
responses = return id `apply` many command_response `discard` eof
group :: [String] -> String
group a = "( " ++ intercalate " " a ++ " )"
showBool :: Bool -> String
showBool a = if a then "true" else "false"
type SMTLIB a = Parser Token a
tok :: Token -> SMTLIB ()
tok a = satisfy (== a) >> return ()
left :: SMTLIB ()
left = tok LeftParen
right :: SMTLIB ()
right = tok RightParen
numeral :: SMTLIB Numeral
numeral = do
a <- satisfy (\ a -> case a of { Numeral _ -> True; _ -> False })
case a of
Numeral a -> return a
_ -> undefined
string :: SMTLIB String
string = do
a <- satisfy (\ a -> case a of { String _ -> True; _ -> False })
case a of
String a -> return a
_ -> undefined
symbol :: SMTLIB Symbol
symbol = do
a <- satisfy (\ a -> case a of { Symbol _ -> True; _ -> False })
case a of
Symbol a -> return a
_ -> undefined
keyword :: SMTLIB Keyword
keyword = do
a <- satisfy (\ a -> case a of { Keyword _ -> True; _ -> False })
case a of
Keyword a -> return a
_ -> undefined
b_value :: SMTLIB Bool
b_value = oneOf
[ do { tok $ Symbol "true"; return True }
, do { tok $ Symbol "false"; return False }
]
parseScript :: String -> Script
parseScript s = fst $ runParser script $ lexSMTLIB s
parseResponses :: String -> [Command_response]
parseResponses s = fst $ runParser responses $ lexSMTLIB s
parseTheory :: String -> Theory_decl
parseTheory s = fst $ runParser theory_decl $ lexSMTLIB s
parseLogic :: String -> Logic
parseLogic s = fst $ runParser logic $ lexSMTLIB s
checkScript :: FilePath -> IO Bool
checkScript file = do
script <- readFile file
let orig = clean script
parsed = clean $ show $ parseScript script
if orig == parsed then return True else do
writeFile (file ++ ".fail") $ show $ parseScript script
return False
checkResponses :: FilePath -> IO Bool
checkResponses file = do
script <- readFile file
let orig = clean script
parsed = clean $ show $ parseResponses script
if orig == parsed then return True else do
writeFile (file ++ ".fail") $ show $ parseResponses script
return False
clean :: String -> String
clean = filter (flip notElem " \t\r\n") . unlines . map (takeWhile (/= ';')) . lines
checkParser :: IO ()
checkParser = do
result <- checkDir "."
if result
then putStrLn "\nall tests passed\n"
else putStrLn "\nTESTS FAILED\n"
where
checkDir :: FilePath -> IO Bool
checkDir dir = getDirectoryContents dir >>= mapM checkFile >>= return . and
where
checkFile :: FilePath -> IO Bool
checkFile file = do
let f = dir ++ "/" ++ file
a <- doesDirectoryExist f
if (a && notElem file [".", ".."])
then checkDir f
else if (isSuffixOf ".smt2" f)
then do
putStr $ "testing file " ++ f ++ " ... "
hFlush stdout
pass <- checkScript f
putStrLn (if pass then "pass" else "FAIL")
hFlush stdout
return pass
else return True