smt-lib 0.0.1 → 0.0.2

raw patch · 2 files changed

+125/−30 lines, 2 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/SMTLIB.hs +124/−29
• smt-lib.cabal +1/−1

@@ -32,26 +32,25 @@   , Reason_unknown       (..)   , Status               (..)   , Info_response        (..)-  , Gi_response-  , Cs_response-  , Ga_response   , Proof-  , Gp_response-  , Guc_response   , Valuation_pair-  , Gv_response   , T_valuation_pair-  , Gta_response+  , Command_response     (..)   -- * Parsing   , parseScript+  , parseResponses+  , parseTheory+  , parseLogic   -- * Parsing Verification+  , checkScript+  , checkResponses   , checkParser   ) where  import Data.List hiding (group) import System.Directory import System.IO-import Text.ParserCombinators.Poly.Plain hiding (Success)+import Text.ParserCombinators.Poly.Lazy hiding (Success) import Text.Printf  import Language.SMTLIB.Lexer@@ -63,7 +62,7 @@ data Spec_constant   = Spec_constant_numeral     Numeral   | Spec_constant_decimal     Rational-  | Spec_constant_hexadecimal Integer+  | Spec_constant_hexadecimal String   | Spec_constant_binary      [Bool]   | Spec_constant_string      String @@ -71,7 +70,7 @@   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%x" a+    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 @@ -83,7 +82,7 @@       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.+        Hex     a -> return $ Spec_constant_hexadecimal a         Bin     a -> return $ Spec_constant_binary $ map (== '1') a         _ -> undefined   ]@@ -534,7 +533,7 @@   show (Script a) = unlines $ map show a  script :: SMTLIB Script-script = many command >>= return . Script+script = return Script `apply` many command `discard` eof  data Gen_response   = Unsupported@@ -547,6 +546,13 @@     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@@ -556,6 +562,12 @@     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@@ -567,6 +579,13 @@     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@@ -578,6 +597,13 @@     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@@ -597,17 +623,60 @@     Info_response_reason_unknown a -> ":reason-unknown " ++ show a     Info_response_attribute      a -> show a -type Gi_response      = [Info_response]-type Cs_response      = Status-type Ga_response      = [Term]+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 Gp_response      = Proof-type Guc_response     = [Symbol] type Valuation_pair   = (Term, Term)-type Gv_response      = [Valuation_pair] type T_valuation_pair = (Symbol, Bool)-type Gta_response     = [T_valuation_pair] +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 ++ " )" @@ -659,18 +728,45 @@   , do { tok $ Symbol "false"; return False }   ] --- | Parses an SMT-LIB command script.+-- | Lazily parses an SMT-LIB command script. parseScript :: String -> Script-parseScript s = case runParser script $ lexSMTLIB s of-  (Left msg, _) -> error msg-  (Right a, _)  -> a+parseScript s = fst $ runParser script $ lexSMTLIB s +-- | Lazily parses an SMT-LIB command responses.+parseResponses :: String -> [Command_response]+parseResponses s = fst $ runParser responses $ lexSMTLIB s++-- | Lazily parses an SMT-LIB theory declaration.+parseTheory :: String -> Theory_decl+parseTheory s = fst $ runParser theory_decl $ lexSMTLIB s++-- | Lazily parses an SMT-LIB logic.+parseLogic :: String -> Logic+parseLogic s = fst $ runParser logic $ lexSMTLIB s+ -- | 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+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 +-- | Checks the parsing of command responses.+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+ -- | Recursively searches current directory for *.smt2 files to test the parser. checkParser :: IO () checkParser = do@@ -692,8 +788,7 @@           then do             putStr $ "testing file " ++ f ++ " ... "             hFlush stdout-            a <- readFile f-            let pass = checkScript a+            pass <- checkScript f             putStrLn (if pass then "pass" else "FAIL")             hFlush stdout             return pass

@@ -1,5 +1,5 @@ name:    smt-lib-version: 0.0.1+version: 0.0.2  category: Language