Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

script parser working

  • Loading branch information...
commit 20ca034b0b1522095e1a4bac85927110924c9a45 1 parent 99fe75a
Tom authored
Showing with 279 additions and 25 deletions.
  1. +263 −9 Language/SMTLIB.hs
  2. +14 −15 Language/SMTLIB/Lexer.x
  3. +2 −1  smt-lib.cabal
View
272 Language/SMTLIB.hs
@@ -44,13 +44,17 @@ module Language.SMTLIB
, Gta_response
-- * Parsing
, parseScript
+ -- * Parsing Verification
+ , checkParser
) where
import Data.List hiding (group)
-import Text.ParserCombinators.Poly.Lazy hiding (Success)
+import System.Directory
+import System.IO
+import Text.ParserCombinators.Poly.Plain hiding (Success)
import Text.Printf
-import qualified Language.SMTLIB.Lexer as L
+import Language.SMTLIB.Lexer
type Numeral = Integer
type Symbol = String
@@ -71,6 +75,19 @@ instance Show Spec_constant where
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 $ read $ "0x" ++ a --XXX Leading 0s will be dropped.
+ Bin a -> return $ Spec_constant_binary $ map (== '1') a
+ _ -> undefined
+ ]
+
data S_expr
= S_expr_constant Spec_constant
| S_expr_symbol Symbol
@@ -84,6 +101,14 @@ instance Show S_expr where
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]
@@ -93,6 +118,12 @@ instance Show Identifier where
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
@@ -104,6 +135,13 @@ instance Show Sort where
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
@@ -115,6 +153,13 @@ instance Show Attribute_value where
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
@@ -124,6 +169,12 @@ instance Show Attribute where
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
@@ -133,6 +184,12 @@ instance Show Qual_identifier where
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
@@ -140,6 +197,9 @@ 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
@@ -147,6 +207,9 @@ 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
@@ -168,6 +231,18 @@ instance Show Term where
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]
@@ -175,6 +250,9 @@ 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
@@ -186,6 +264,13 @@ instance Show Meta_spec_constant where
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]
@@ -197,6 +282,13 @@ instance Show Fun_symbol_decl where
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]
@@ -206,8 +298,14 @@ instance Show Par_fun_symbol_decl where
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 [Symbol]
+ = Theory_attribute_sorts [Sort_symbol_decl]
| Theory_attribute_funs [Par_fun_symbol_decl]
| Theory_attribute_sorts_desc String
| Theory_attribute_funs_desc String
@@ -227,6 +325,18 @@ instance Show Theory_attribute where
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]
@@ -234,6 +344,9 @@ 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
@@ -251,6 +364,16 @@ instance Show Logic_attribute where
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]
@@ -258,6 +381,9 @@ 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
@@ -287,6 +413,22 @@ instance Show Option where
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
@@ -308,6 +450,18 @@ instance Show Info_flag where
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
@@ -353,7 +507,25 @@ instance Show Command where
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]
@@ -442,11 +614,93 @@ group a = "( " ++ intercalate " " a ++ " )"
showBool :: Bool -> String
showBool a = if a then "true" else "false"
-type SMTLIB a = Parser L.Token a
-
-tok :: L.Token -> SMTLIB ()
-tok a = satisfy (== a) >> return ()
+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 }
+ ]
+-- | Parses an SMT-LIB command script.
parseScript :: String -> Script
-parseScript = fst . runParser script . L.lexSMTLIB
+parseScript s = case runParser script $ lexSMTLIB s of
+ (Left msg, _) -> error msg
+ (Right a, _) -> a
+
+-- | Checks the parsing of a command script.
+checkScript :: String -> Bool
+checkScript script = clean script == clean (show $ parseScript script)
+ where
+ clean = filter (flip notElem " \r\n\t") . unlines . map (takeWhile (/= ';')) . lines
+
+-- | Recursively searches current directory for *.smt2 files to test the parser.
+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
+ a <- readFile f
+ let pass = checkScript a
+ putStrLn (if pass then "pass" else "FAIL")
+ hFlush stdout
+ return pass
+ else return True
+
+
+
+
+
View
29 Language/SMTLIB/Lexer.x
@@ -23,19 +23,19 @@ $bin = 0-1
tokens :-
- $white+ ;
- \;.* ;
- [$sym # $digit]$sym* { Symbol }
- \|[$printable # \|]*\| { Symbol }
- \:$sym+ { Keyword }
- $digit+\.$digit+ { Decimal . read }
- $digit { Numeral . read }
- \( { const LeftParen }
- \) { const RightParen }
- \"(([$printable#\\]|\\.)*)\" { String . read }
- "#x"$hex+ { Hex . drop 2 }
- "#b"$bin+ { Bin . drop 2 }
- . { \ s -> error $ "unexpected character: '" ++ s ++ "'" }
+ $white+ ;
+ \;.* ;
+ [$sym # $digit]$sym* { Symbol }
+ \|[$printable \n # \|]*\| { Symbol }
+ \:$sym+ { Keyword }
+ $digit+\.$digit+ { Decimal . read }
+ $digit { Numeral . read }
+ \( { const LeftParen }
+ \) { const RightParen }
+ \"(([$printable \n # \\]|\\.)*)\" { String . read }
+ "#x"$hex+ { Hex . drop 2 }
+ "#b"$bin+ { Bin . drop 2 }
+ . { \ s -> error $ "unexpected character: '" ++ s ++ "'" }
{
data Token
@@ -48,9 +48,8 @@ data Token
| Keyword String
| LeftParen
| RightParen
- | EOF
deriving (Eq,Show)
lexSMTLIB :: String -> [Token]
-lexSMTLIB a = alexScanTokens a ++ [EOF]
+lexSMTLIB a = alexScanTokens a
}
View
3  smt-lib.cabal
@@ -6,7 +6,7 @@ category: Language
synopsis: Parsing and printing SMT-LIB.
description:
- SMT-LIB (http://goedel.cs.uiowa.edu/smtlib/) is a common language used by many SMT solvers.
+ SMT-LIB is a common language used by many SMT solvers.
This library provides an SMT-LIB AST with parsing and printing utilities.
author: Tom Hawkins <tomahawkins@gmail.com>
@@ -23,6 +23,7 @@ cabal-version: >= 1.6
library
build-depends:
base >= 4.0 && < 5.0,
+ directory >= 1.0 && < 1.1,
array >= 0.3 && < 0.4,
polyparse >= 1.4
Please sign in to comment.
Something went wrong with that request. Please try again.