diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -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 diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -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 [] diff --git a/Math/SMT/Yices/Pipe.hs b/Math/SMT/Yices/Pipe.hs --- a/Math/SMT/Yices/Pipe.hs +++ b/Math/SMT/Yices/Pipe.hs @@ -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) ) diff --git a/Math/SMT/Yices/Syntax.hs b/Math/SMT/Yices/Syntax.hs --- a/Math/SMT/Yices/Syntax.hs +++ b/Math/SMT/Yices/Syntax.hs @@ -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" diff --git a/yices.cabal b/yices.cabal --- a/yices.cabal +++ b/yices.cabal @@ -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