yices 0.0.0.4 → 0.0.0.6
raw patch · 5 files changed
+149/−92 lines, 5 files
Files
- ChangeLog +10/−0
- Main.hs +1/−1
- Math/SMT/Yices/Pipe.hs +37/−4
- Math/SMT/Yices/Syntax.hs +99/−85
- yices.cabal +2/−2
ChangeLog view
@@ -1,3 +1,13 @@+2010-01-01 José Iborra pepeiborra@gmail.com+ * Math/SMT/Yices/Syntax.hs: Avoided quadratic complexity in the pretty+ printer and fixed a bug in the pretty printer+ * Math/SMT/Yices/Pipe.hs (checkY) : display Yices errors and extraneous+ output handling of "unknown" answers+ * Math/SMT/Yices/Pipe.hs (quickCheckY, quickCheckY') : Added a driver+ which does not use the yices interactive prompt.+ The interactive prompt has problems parsing large expressions,+ as warned in the Yices FAQ.+ 2009-08-04 Ahn, Ki Yung kya@pdx.edu * Math/SMT/Yices/Parser.hs (echo, include): fix obvious parser error * Math/SMT/Yices/Pipe.hs (hGetReadyString, hGetReadyString1): comment
Main.hs view
@@ -11,7 +11,7 @@ import Monad -- import Random -yicesPath = "/home/kyagrd/ames/yices-1.0.21/bin/yices" -- your yices path+yicesPath = "/home/kyagrd/yices/bin/yices" -- your yices path main = do yp@(Just hin, Just hout, Nothing, p) <- createYicesPipe yicesPath []
Math/SMT/Yices/Pipe.hs view
@@ -13,7 +13,8 @@ -} module Math.SMT.Yices.Pipe ( YicesIPC, ResY(..), createYicesPipe,- runCmdsY', runCmdsY, checkY, exitY, flushY+ runCmdsY', runCmdsY, checkY, exitY, flushY,+ quickCheckY, quickCheckY' ) where import Math.SMT.Yices.Syntax@@ -29,6 +30,7 @@ -- | To read in the result of the (check) command data ResY = Sat [ExpY]+ | Unknown [ExpY] | UnSat [Integer] | InCon [String] deriving Show@@ -70,15 +72,46 @@ checkY yp@(_, Just hout, _, _) = do runCmdsY yp [ECHO('\n':_BEGIN_OUTPUT), CHECK, ECHO('\n':_END_OUTPUT)] (s:ss) <- hGetOutLines hout+ hPutStrLn stderr s return $ case s of- "sat" -> Sat (map parseExpY ss)- "unsat" -> UnSat (map read.words.tail.dropWhile (/=':').head $ ss)- _ -> InCon (s:ss)+ "sat" -> Sat (map parseExpY ss)+ "unknown"-> Unknown (map parseExpY ss)+ "unsat" -> UnSat (map read.words.tail.dropWhile (/=':').head $ ss)+ _ -> InCon (s:ss) +-- | sends a bunch of commands followed by a check command and reads the resulting model.+-- This function should be the preferred option when large expressions are involved.+quickCheckY :: String -> [String] -> [CmdY] -> IO ResY+quickCheckY yPath yOpts cmds = quickCheckY' yPath yOpts (cmds ++ [CHECK])++-- | sends a bunch of commands and reads the result.+-- This function is similar to 'quickCheckY' but does not append a check command.+-- It can be useful if you intend to +quickCheckY' :: String -> [String] -> [CmdY] -> IO ResY+quickCheckY' yPath yOpts cmds = do+ (code, out, err) <- readProcessWithExitCode yPath ("-e" : yOpts) (unlines $ map show cmds)+ when (not $ null err) $ hPutStrLn stderr err+ return $+ case lines out of+ "sat" : ss -> Sat (map parseExpY $ filter (not.null) ss)+ "unknown" : ss -> Unknown (map parseExpY $ filter (not.null) ss)+ "unsat" : ss -> UnSat (map read.words.tail.dropWhile (/=':').head $ ss)+ other -> InCon other++ stripYicesPrompt line | yprompt `isPrefixOf` line = drop (length yprompt) line | otherwise = line where yprompt = "yices > "++{- -- for debugging echoing to stderr+hGetOutLines h = do+ ll <- (hGetLinesWhile (/= _END_OUTPUT) h)+ mapM_ (hPutStrLn stderr) (filter (not.null) . map stripYicesPrompt . takeWhile (/= _BEGIN_OUTPUT) $ ll)+ return $ ( filter (not . null) . map stripYicesPrompt .+ tail . dropWhile (/=_BEGIN_OUTPUT) )+ ll+-} hGetOutLines h = liftM ( filter (not . null) . map stripYicesPrompt . tail . dropWhile (/=_BEGIN_OUTPUT) )
Math/SMT/Yices/Syntax.hs view
@@ -15,8 +15,10 @@ module Math.SMT.Yices.Syntax ( TypY(..) , ExpY(..) , CmdY(..) ) where import Char+import Data.Monoid import List import Ratio+import Text.Show -- | yices types data TypY@@ -94,107 +96,119 @@ | DUMP | EXIT -paren s = "("++s++")"+paren :: ShowS -> ShowS+paren = showParen True -showListSepByWith showFun sep = concat . intersperse sep . map showFun+space = showChar ' ' -showListSepBy :: (Show a) => String -> [a] -> String-showListSepBy = showListSepByWith show+showListSepByWith :: (a -> ShowS) -> String -> [a] -> ShowS+showListSepByWith showsFun sep = foldr1 (.) . intersperse (showString sep) . map showsFun -showStringsSepBy = showListSepByWith id+showListSepBy :: (Show a) => String -> [a] -> ShowS+showListSepBy = showListSepByWith (showsPrec 0) -showIdTyp (tname,t) = tname++"::"++show t+showStringsSepBy = showListSepByWith showString -showIdVal (fname,e) = fname++"::"++show e+showIdTyp, showIdVal :: Show a => (String, a) -> ShowS+showIdTyp (tname,t) = showString tname . showString "::" . showsPrec 0 t -showCtorDef (c,[]) = c-showCtorDef (c,idtyps) = paren $ c++" "++showListSepByWith showIdTyp " " idtyps+showIdVal = showIdTyp -showBinding ((x,Just t),e) = paren $ showIdTyp(x,t) ++ " " ++ show e-showBinding ((x,Nothing),e) = paren $ x ++ " " ++ show e+showCtorDef (c,[]) = showString c+showCtorDef (c,idtyps) = paren $ showString c . space . showListSepByWith showIdTyp " " idtyps +showBinding ((x,Just t),e) = paren $ showIdTyp(x,t) . space . showsPrec 0 e+showBinding ((x,Nothing),e) = paren $ showString x . space . showsPrec 0 e+ instance Show TypY where- show (VarT tname) = tname- show (SUBTYPE idty e) = paren $ "subtype " ++ showIdTyp idty ++ " " ++ show e- show (SUBRANGE e1 e2) = paren $ "subrange " ++ show e1 ++ " " ++ show e2- show (ARR ts) = paren $ "-> " ++ showListSepBy " " ts- show (TUP ts) = paren $ "tuple " ++ showListSepBy " " ts- show (REC idtyps) = paren $ "record " ++ showListSepByWith showIdTyp " " idtyps- show (DEP idty) = showIdTyp idty- show (DATATYPE ctordefs) =- paren $ "datatype " ++ showListSepByWith showCtorDef " " ctordefs- show (SCALAR tnames) = paren $ "scalar " ++ showStringsSepBy " " tnames- -- show (BITVECTOR n) = paren $ "bitvector " ++ show n+ showsPrec _ = showTypY +{-# INLINE showTypY #-}+showTypY (VarT tname) = showString tname+showTypY (SUBTYPE idty e) = paren $ showString "subtype " . showIdTyp idty . space . showsPrec 0 e+showTypY (SUBRANGE e1 e2) = paren $ showString "subrange " . showsPrec 0 e1 . space . showsPrec 0 e2+showTypY (ARR ts) = paren $ showString "-> " . showListSepBy " " ts+showTypY (TUP ts) = paren $ showString "tuple " . showListSepBy " " ts+showTypY (REC idtyps) = paren $ showString "record " . showListSepByWith showIdTyp " " idtyps+showTypY (DEP idty) = showIdTyp idty+showTypY (DATATYPE ctordefs) =+ paren $ showString "datatype " . showListSepByWith showCtorDef " " ctordefs+showTypY (SCALAR tnames) = paren $ showString "scalar " . showStringsSepBy " " tnames+ -- showsPrec _ (BITVECTOR n) = paren $ "bitvector " ++ show n+ instance Show ExpY where- show (VarE x) = x- show (LitB True) = "true"- show (LitB False) = "false"- show (LitI n) = show n- show (LitR r) = show (numerator r) ++ "/" ++ show (denominator r)- show (AND es) = paren $ "and " ++ showListSepBy " " es- show (OR es) = paren $ "or " ++ showListSepBy " " es- show (NOT e) = paren $ "not " ++ show e- show (e1 :=> e2) = paren $ "=> " ++ show e1 ++ " " ++ show e2- show (e1 := e2) = paren $ "= " ++ show e1 ++ " " ++ show e2- show (e1 :/= e2) = paren $ "/= " ++ show e1 ++ " " ++ show e2- show (e1 :< e2) = paren $ "< " ++ show e1 ++ " " ++ show e2- show (e1 :<= e2) = paren $ "<= " ++ show e1 ++ " " ++ show e2- show (e1 :> e2) = paren $ "> " ++ show e1 ++ " " ++ show e2- show (e1 :>= e2) = paren $ ">= " ++ show e1 ++ " " ++ show e2- show (e1 :+: e2) = paren $ "+ " ++ show e1 ++ " " ++ show e2- show (e1 :-: e2) = paren $ "- " ++ show e1 ++ " " ++ show e2- show (e1 :*: e2) = paren $ "* " ++ show e1 ++ " " ++ show e2- show (e1 :/: e2) = paren $ "/ " ++ show e1 ++ " " ++ show e2- show (DIV e1 e2) = paren $ "div " ++ show e1 ++ " " ++ show e2- show (MOD e1 e2) = paren $ "mod " ++ show e1 ++ " " ++ show e2- show (IF eb et ef) = paren $ "if " ++ showListSepBy " " [eb,et,ef]- show (ITE eb et ef) = paren $ "ite " ++ showListSepBy " " [eb,et,ef]- show (LET bindings e) = paren $ "let " ++ (paren $ showListSepByWith showBinding " " bindings) ++ " "++ show e+ showsPrec _ = showExpY++{-# INLINE showExpY #-}+showExpY (VarE x) = showString x+showExpY (LitB True) = showString "true"+showExpY (LitB False) = showString "false"+showExpY (LitI n) = showsPrec 0 n+showExpY (LitR r) = showsPrec 0 (numerator r) . showChar '/' . showsPrec 0 (denominator r)+showExpY (AND es) = paren (showString "and " . showListSepBy " " es)+showExpY (OR es) = paren $ showString "or " . showListSepBy " " es+showExpY (NOT e) = paren $ showString "not " . showsPrec 0 e+showExpY (e1 :=> e2) = paren $ showString "=> " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 := e2) = paren $ showString "= " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :/= e2) = paren $ showString "/= " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :< e2) = paren $ showString "< " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :<= e2) = paren $ showString "<= " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :> e2) = paren $ showString "> " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :>= e2) = paren $ showString ">= " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :+: e2) = paren $ showString "+ " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :-: e2) = paren $ showString "- " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :*: e2) = paren $ showString "* " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (e1 :/: e2) = paren $ showString "/ " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (DIV e1 e2) = paren $ showString "div " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (MOD e1 e2) = paren $ showString "mod " . showsPrec 0 e1 . space . showsPrec 0 e2+showExpY (IF eb et ef) = paren $ showString "if " . showListSepBy " " [eb,et,ef]+showExpY (ITE eb et ef) = paren $ showString "ite " . showListSepBy " " [eb,et,ef]+showExpY (LET bindings e) = paren $ showString "let " . (paren $ showListSepByWith showBinding " " bindings) . space . showsPrec 0 e -- quantifires- show (FORALL idtyps e) = paren $ "forall "- ++ (paren $ showListSepByWith showIdTyp " " idtyps) ++ " " ++ show e- show (EXISTS idtyps e) = paren $ "exists "- ++ (paren $ showListSepByWith showIdTyp " " idtyps) ++ " " ++ show e+showExpY (FORALL idtyps e) = paren $ showString "forall "+ . (paren $ showListSepByWith showIdTyp " " idtyps) . space . showsPrec 0 e+showExpY (EXISTS idtyps e) = paren $ showString "exists "+ . (paren $ showListSepByWith showIdTyp " " idtyps) . space . showsPrec 0 e -- functions- show (APP e es) = paren $ showListSepBy " " (e:es)- show (UPDATE_F e es v) = paren $ "update "- ++ show e ++ " " ++ (paren $ showListSepBy " " es) ++ show v- show (LAMBDA idtyps e) = paren $ "lambda "- ++ (paren $ showListSepByWith showIdTyp " " idtyps) ++ show e+showExpY (APP e es) = paren $ showListSepBy " " (e:es)+showExpY (UPDATE_F e es v) = paren $ showString "update "+ . showsPrec 0 e . space . (paren $ showListSepBy " " es) . showsPrec 0 v+showExpY (LAMBDA idtyps e) = paren $ showString "lambda "+ . (paren $ showListSepByWith showIdTyp " " idtyps) . showsPrec 0 e -- tuples- show (MKTUP es) = paren $ "mk-tuple " ++ showListSepBy " " es- show (SELECT_T e i) = paren $ "select " ++ show e ++ " " ++ show i- show (UPDATE_T e i v) = paren $ "update "- ++ show e ++ " " ++ show i ++ " " ++ show v+showExpY (MKTUP es) = paren $ showString "mk-tuple " . showListSepBy " " es+showExpY (SELECT_T e i) = paren $ showString "select " . showsPrec 0 e . space . showsPrec 0 i+showExpY (UPDATE_T e i v) = paren $ showString "update "+ . showsPrec 0 e . space . showsPrec 0 i . space . showsPrec 0 v -- records- show (MKREC idvals) = paren $ "mk-record "- ++ showListSepByWith showIdVal " " idvals- show (SELECT_R e s) = paren $ "select " ++ show e ++ " " ++ s- show (UPDATE_R e s v) = paren $ "update "- ++ show e ++ " " ++ s ++ " " ++ show v+showExpY (MKREC idvals) = paren $ showString "mk-record " . showListSepByWith showIdVal " " idvals+showExpY (SELECT_R e s) = paren $ showString "select " . showsPrec 0 e . space . showString s+showExpY (UPDATE_R e s v) = paren $ showString "update " . showsPrec 0 e . space . showString s . space . showsPrec 0 v -- bitvectors -- TODO instance Show CmdY where- show (DEFTYP tname Nothing) = paren $ "define-type " ++ tname- show (DEFTYP tname (Just t)) = paren $ "define-type "++ tname ++ " " ++ show t- show (DEFINE idty Nothing) = paren $ "define " ++ showIdTyp idty- show (DEFINE idty (Just e)) = paren $ "define " ++ showIdTyp idty ++ show e- show (ASSERT e) = paren $ "assert " ++ show e- show (ASSERT_P e Nothing) = paren $ "assert+ " ++ show e- show (ASSERT_P e (Just w)) = paren $ "assert+ " ++ show e ++ " " ++ show w- show (RETRACT i) = paren $ "retract " ++ show i- show (CHECK) = paren "check"- show (MAXSAT) = paren "max-sat"- show (SETE b) = paren $ "set-evidence! " ++ show (LitB b)- show (SETV k) = paren $ "set-verbosity! " ++ show k- show (SETAO b) = paren $ "set-arith-only! " ++ show (LitB b)- show (PUSH) = paren "push"- show (POP) = paren "pop"- show (ECHO s) = paren $ "echo " ++ show s -- not exact since Haskell string- show (INCLUDE s) = paren $ "include " ++ show s -- not exact same reason- show (RESET) = paren "reset"- show (STATUS) = paren "status"- show (DUMP) = paren "dump-context"- show (EXIT) = paren "exit"+ showsPrec _ = showCmdY++{-# INLINE showCmdY #-}+showCmdY (DEFTYP tname Nothing) = paren $ showString "define-type " . showString tname+showCmdY (DEFTYP tname (Just t)) = paren $ showString "define-type ". showString tname . space . showsPrec 0 t+showCmdY (DEFINE idty Nothing) = paren $ showString "define " . showIdTyp idty+showCmdY (DEFINE idty (Just e)) = paren $ showString "define " . showIdTyp idty . space . showsPrec 0 e+showCmdY (ASSERT e) = paren $ showString "assert " . showsPrec 0 e+showCmdY (ASSERT_P e Nothing) = paren $ showString "assert+ " . showsPrec 0 e+showCmdY (ASSERT_P e (Just w)) = paren $ showString "assert+ " . showsPrec 0 e . space . showsPrec 0 w+showCmdY (RETRACT i) = paren $ showString "retract " . showsPrec 0 i+showCmdY (CHECK) = paren $ showString "check"+showCmdY (MAXSAT) = paren $ showString "max-sat"+showCmdY (SETE b) = paren $ showString "set-evidence! " . showsPrec 0 (LitB b)+showCmdY (SETV k) = paren $ showString "set-verbosity! " . showsPrec 0 k+showCmdY (SETAO b) = paren $ showString "set-arith-only! " . showsPrec 0 (LitB b)+showCmdY (PUSH) = paren $ showString "push"+showCmdY (POP) = paren $ showString "pop"+showCmdY (ECHO s) = paren $ showString "echo " . showsPrec 0 s -- not exact since Haskell string+showCmdY (INCLUDE s) = paren $ showString "include " . showsPrec 0 s -- not exact same reason+showCmdY (RESET) = paren $ showString "reset"+showCmdY (STATUS) = paren $ showString "status"+showCmdY (DUMP) = paren $ showString "dump-context"+showCmdY (EXIT) = paren $ showString "exit"
yices.cabal view
@@ -1,5 +1,5 @@ name: yices-version: 0.0.0.4+version: 0.0.0.6 synopsis: Haskell programming interface to Yices SMT solver description: Incomplete (no bitvectors) syntax, parser, and inter process communication to Yices from Haskell through pipe.@@ -23,4 +23,4 @@ Math.SMT.Yices.Parser, Math.SMT.Yices.Pipe ghc-options: -Wall-+ghc-prof-options: -auto-all