yices (empty) → 0.0.0.1
raw patch · 8 files changed
+615/−0 lines, 8 filesdep +basedep +haskell98dep +parsecsetup-changed
Dependencies added: base, haskell98, parsec, process
Files
- LICENSE +12/−0
- Main.hs +56/−0
- Math/SMT/Yices/Parser.hs +219/−0
- Math/SMT/Yices/Pipe.hs +98/−0
- Math/SMT/Yices/Syntax.hs +200/−0
- README +1/−0
- Setup.lhs +3/−0
- yices.cabal +26/−0
+ LICENSE view
@@ -0,0 +1,12 @@+Copyright (c) 2009, Ki Yung Ahn+All rights reserved.++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.+ * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.+ * Neither the name of the Portland State University nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.++
+ Main.hs view
@@ -0,0 +1,56 @@+-- vim:sw=2:ts=2:expandtab:autoindent++module Main where ++-- example of generating three test cases of 6 integer variables+-- l1, u1, i, l2, u2, j sush that l1 < i <= u1 and l2 < j <= u2.++import Math.SMT.Yices.Syntax+import Math.SMT.Yices.Pipe+import List+import Monad+-- import Random++yicesPath = "/home/kyagrd/ames/yices-1.0.21/bin/yices" -- your yices path++main =+ do yp@(Just hin, Just hout, Nothing, p) <- createYicesPipe yicesPath []+ runCmdsY yp (defs ++ ctrs)++ -- gr <- getStdGen+ -- let (rn,gr') = next gr++ Sat ss <- checkY yp+ print ss++ runCmdsY yp [ASSERT_P (NOT $ ss!!0) Nothing]+ Sat ss <- checkY yp+ print ss++ runCmdsY yp [ASSERT_P (NOT $ ss!!0) Nothing]+ Sat ss <- checkY yp+ print ss++ exitY yp+++defs = map (\x -> DEFINE (x,int) Nothing) ["l1","u1","i","l2","u2","j"]++ctrs = map ASSERT [ l1:<u1, l1:<=i, i:<=u1, l2:<u2, l2:<=j, j:<=u2 ]+ -- ++ map (\e -> ASSERT_P e Nothing) [ i:<j, j:<i ]+ where+ l1 = VarE "l1"+ u1 = VarE "u1"+ i = VarE "i"+ l2 = VarE "l2"+ u2 = VarE "u2"+ j = VarE "j"++int = VarT "int"+nat = VarT "nat"+bool = VarT "bool"+real = VarT "real"++true = LitB True+false = LitB False+
+ Math/SMT/Yices/Parser.hs view
@@ -0,0 +1,219 @@+-- vim:sw=2:ts=2:expandtab:autoindent+{-# LANGUAGE NoMonomorphismRestriction #-}++{- |+ Module : Math.SMT.Yices.Parser+ Copyright : (c) 2009 by Ki Yung Ahn+ License : BSD3++ Maintainer : Ahn, Ki Yung <kya@pdx.edu>+ Stability : provisional+ Portability : portable++ Parser for the yices syntax. Yet incomplete since it does not include+ bit vectors, and not heavily tested at all.+ See <http://yices.csl.sri.com/language.shtml> for details.+ -}+module Math.SMT.Yices.Parser (+ typY, expY, cmdY, parseTypY, parseExpY, parseCmdY+ ) where++import Math.SMT.Yices.Syntax+import Monad+import Maybe+import Ratio+import Text.ParserCombinators.Parsec+import Text.ParserCombinators.Parsec.Language+import qualified Text.ParserCombinators.Parsec.Token as T++-- | parse a string of yices type format+parseTypY :: String -> TypY+parseTypY s = case parse typY "parseTypY" s of Right r -> r+ Left msg -> error $ show msg+-- | parse a string of yices expression format+parseExpY :: String -> ExpY+parseExpY s = case parse expY "parseExpY" s of Right r -> r+ Left msg -> error $ show msg+-- | parse a string of yices command format+parseCmdY :: String -> CmdY+parseCmdY s = case parse cmdY "parseCmdY" s of Right r -> r+ Left msg -> error $ show msg+++tp = T.makeTokenParser emptyDef++stringLiteral = T.stringLiteral tp ++lexme p = do spaces+ r <- p+ spaces+ return r++paren = between (lexme $ char '(') (lexme $ char ')')++many2 p = liftM2 (:) p (many1 p)++idStart = identStart emptyDef++idLetter = identLetter emptyDef++ident = liftM2 (:) idStart (many idLetter)++identifier = lexme ident <?> "identifier"+++neg = char '-' >> return negate+++nat = liftM (read :: String -> Integer) (many1 digit)++int = option id neg `ap` nat++integer = lexme int <?> "integer"+++rat = do n <- nat+ char '/'+ d <- nat+ return (n % d)++ratio = option id neg `ap` rat++rational = lexme ratio <?> "rational"+++true = string "true" >> return True++false = string "false" >> return False++bool = true <|> false++boolean = lexme bool <?> "boolean"++tok = try . lexme . string++-- | parsec parser for yices types+typY :: GenParser Char st TypY+typY = typYsimple <|> paren typYinParen+typYinParen = subtype <|> subrange <|> arr <|> tup <|> rec+ <|> datatype <|> scalar++vart = liftM VarT identifier++typYsimple = do x <- identifier+ mt <- optionMaybe $ tok "::" >> (vart <|> paren typYinParen)+ return $ case mt of Nothing -> VarT x+ Just t -> DEP (x,t)++subtype = tok "subtype" >> liftM2 SUBTYPE (paren idty) expY+subrange = tok "subrange" >> liftM2 SUBRANGE expY expY+arr = tok "->" >> liftM ARR (many2 typY)+tup = tok "tuple" >> liftM TUP (many2 typY)+rec = tok "record" >> liftM REC (many1 idty)+datatype = tok "datatype" >> liftM DATATYPE (many1 $ paren ctordef)+scalar = tok "scalar" >> liftM SCALAR (many1 identifier)++ctordef = liftM2 (,) identifier (many idty)++idty = do x <- identifier+ tok "::"+ t <- typY+ return (x,t)++idex = do x <- identifier+ tok "::"+ e <- expY+ return (x,e)++++-- | parsec parser for yices expressions+expY :: GenParser Char st ExpY+expY = litb <|> liti <|> litr <|> vare <|> paren expYinParen++expYinParen = and_ <|> or_ <|> not_ <|> try (=>:) <|> (=:) <|> (/=:)+ <|> try (<:) <|> (<=:) <|> try (>:) <|> (>=:)+ <|> (+:) <|> (-:) <|> (*:) <|> (/:) <|> div_ <|> mod_+ <|> if_ <|> ite <|> let_ <|> forall <|> exists+ <|> lambda <|> mktup <|> mkrec <|> update <|> select+ <|> app++vare = liftM VarE identifier+litb = liftM LitB boolean+liti = liftM LitI integer+litr = liftM LitR rational++and_ = tok "and" >> liftM AND (many1 expY)+or_ = tok "or" >> liftM OR (many1 expY)+not_ = tok "not" >> liftM NOT expY+(=:) = tok "=" >> liftM2 (:=) expY expY+(/=:) = tok "/=" >> liftM2 (:/=) expY expY+(=>:) = tok "=>" >> liftM2 (:=>) expY expY+(<:) = tok "<" >> liftM2 (:<) expY expY+(<=:) = tok "<=" >> liftM2 (:<=) expY expY+(>:) = tok ">" >> liftM2 (:>) expY expY+(>=:) = tok ">=" >> liftM2 (:>=) expY expY+(+:) = tok "+" >> liftM2 (:+:) expY expY+(-:) = tok "-" >> liftM2 (:-:) expY expY+(*:) = tok "*" >> liftM2 (:*:) expY expY+(/:) = tok "/" >> liftM2 (:/:) expY expY+div_ = tok "div" >> liftM2 DIV expY expY+mod_ = tok "mod" >> liftM2 MOD expY expY+if_ = tok "if" >> liftM3 IF expY expY expY+ite = do tok "ite" >> liftM3 ITE expY expY expY+let_ = tok "let" >> liftM2 LET (paren $ many1 binding) expY+forall = tok "forall" >> liftM2 FORALL (paren $ many1 idty) expY+exists = tok "exists" >> liftM2 EXISTS (paren $ many1 idty) expY+lambda = tok "lambda" >> liftM2 LAMBDA (paren $ many1 idty) expY+mktup = tok "mk-tuple" >> liftM MKTUP (many2 expY)+mkrec = tok "mk-record" >> liftM MKREC (many1 idex)+update = do tok "update"+ e <- expY+ ix <- liftM FunIx (paren $ many expY) <|>+ liftM TupIx integer <|>+ liftM RecIx identifier+ v <- expY+ return $ case ix of FunIx es -> UPDATE_F e es v+ TupIx i -> UPDATE_T e i v+ RecIx f -> UPDATE_R e f v+select = do tok "select"+ e <- expY+ ix <- liftM TupIx integer <|>+ liftM RecIx identifier+ return $ case ix of TupIx i -> SELECT_T e i+ RecIx f -> SELECT_R e f+app = liftM2 APP expY (many1 expY)++binding = do x <- identifier+ mt <- optionMaybe $ tok "::" >> (vart <|> paren typYinParen)+ e <- expY+ return ((x,mt),e)++data IndexType = FunIx [ExpY] | TupIx Integer | RecIx String+++-- | parsec parser for yices command+cmdY :: GenParser Char st CmdY+cmdY = paren $ try deftyp <|> define <|> try assert <|> assertp <|> retract <|>+ check <|> maxsat <|> sete <|> setv <|> setao <|> push <|> pop <|>+ echo <|> include <|> status <|> dump <|> exit++deftyp = tok "define-type" >> liftM2 DEFTYP identifier (optionMaybe typY)+define = tok "define" >> liftM2 DEFINE idty (optionMaybe expY)+assert = tok "assert" >> liftM ASSERT expY+assertp = tok "assert+" >> liftM2 ASSERT_P expY (optionMaybe integer)+retract = tok "retract" >> liftM RETRACT integer+check = tok "check" >> return CHECK+maxsat = tok "max-sat" >> return MAXSAT+sete = tok "set-evidence!" >> liftM SETE boolean+setv = tok "set-verbosity!" >> liftM SETV integer+setao = tok "set-arith-only!" >> liftM SETAO boolean+push = tok "push" >> return PUSH+pop = tok "pop" >> return POP+echo = paren $ liftM ECHO stringLiteral+include = paren $ liftM ECHO stringLiteral+reset = tok "reset" >> return RESET+status = tok "status" >> return DUMP+dump = tok "dump-context" >> return DUMP+exit = tok "exit" >> return EXIT+
+ Math/SMT/Yices/Pipe.hs view
@@ -0,0 +1,98 @@+-- vim:sw=2:ts=2:expandtab:autoindent++{- |+ Module : Math.SMT.Yices.Pipe+ Copyright : (c) 2009 by Ki Yung Ahn+ License : BSD3++ Maintainer : Ahn, Ki Yung <kya@pdx.edu>+ Stability : provisional+ Portability : portable++ Inter-process communication to Yices through pipe.+ -}+module Math.SMT.Yices.Pipe (+ YicesIPC, ResY(..), createYicesPipe,+ runCmdsY', runCmdsY, checkY, exitY, flushY+ ) where++import Math.SMT.Yices.Syntax+import Math.SMT.Yices.Parser+import List+import Monad+import System.IO+import System.Process++-- | type abbrevation for IPC handle quadruple+type YicesIPC = (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)++-- | To read in the result of the (check) command+data ResY+ = Sat [ExpY]+ | UnSat [Int]+ | InCon [String]+ deriving Show++-- | Start yices on a given path with given options.+-- The first argumnet yPath is the path binary file of yices+-- (e.g. /home/kyagrd/yices-1.0.21/bin/yices).+-- By default -i and -e options are already present, and+-- yOpts argument appens more options+createYicesPipe :: FilePath -> [String] -> IO YicesIPC+createYicesPipe yPath yOpts = createProcess $+ (proc yPath $ "-i":"-e":yOpts){std_in=CreatePipe,std_out=CreatePipe}++_BEGIN_OUTPUT = "_![<[BEGIN_OUTPUT]>]!_"+_END_OUTPUT = "_![<[END_OUTPUT]>]!_"++runCmdStringY yp s = runCmdStringY' yp s >> flushY yp++runCmdStringY' (Just hin, _, _, _) = hPutStrLn hin++-- | send yices commands and flush+runCmdsY :: YicesIPC -> [CmdY] -> IO ()+runCmdsY yp cmds = runCmdsY' yp cmds >> flushY yp+ +-- | send yices commands without flushing+runCmdsY' :: YicesIPC -> [CmdY] -> IO ()+runCmdsY' (Just hin, _, _, _) = mapM_ (hPutStrLn hin . show)++-- | send exit command and flush+exitY :: YicesIPC -> IO ()+exitY (Just hin, _, _, _) = hPutStrLn hin (show EXIT) >> hFlush hin++-- | flush the input pipe to yices (needed after actions like runCmdsY')+flushY :: YicesIPC -> IO ()+flushY (Just hin, _, _, _) = hFlush hin++-- | send check command and reads the result+checkY :: YicesIPC -> IO ResY+checkY yp@(_, Just hout, _, _) =+ do runCmdsY yp [ECHO('\n':_BEGIN_OUTPUT), CHECK, ECHO('\n':_END_OUTPUT)]+ (s:ss) <- hGetOutLines hout+ return $+ case s of+ "sat" -> Sat (map parseExpY ss)+ "unsat" -> UnSat (map read.words.tail.dropWhile (/=':').head $ ss)+ _ -> InCon (s:ss)++stripYicesPrompt line | yprompt `isPrefixOf` line = drop (length yprompt) line+ | otherwise = line+ where yprompt = "yices > "++hGetOutLines h = liftM ( filter (not . null) . map stripYicesPrompt .+ tail . dropWhile (/=_BEGIN_OUTPUT) )+ (hGetLinesWhile (/= _END_OUTPUT) h)++hGetLinesWhile p h = do line <- hGetLine h+ if p line+ then liftM (line:) (hGetLinesWhile p h)+ else return []++hGetReadyString1 h = liftM2 (:) (hGetChar h) (hGetReadyString h)++hGetReadyString h =+ do ready <- hReady h+ if ready then liftM2 (:) (hGetChar h) (hGetReadyString h) else return []++
+ Math/SMT/Yices/Syntax.hs view
@@ -0,0 +1,200 @@+-- vim:sw=2:ts=2:expandtab:autoindent+{- |+ Module : Math.SMT.Yices.Syntax+ Copyright : (c) 2009 by Ki Yung Ahn+ License : BSD3++ Maintainer : Ahn, Ki Yung <kya@pdx.edu>+ Stability : provisional+ Portability : portable++ Haskell data type definition for the yices syntax. Yet incomplete since+ it does not include bit vectors.+ See <http://yices.csl.sri.com/language.shtml> for details.+ -}+module Math.SMT.Yices.Syntax ( TypY(..) , ExpY(..) , CmdY(..) ) where++import Char+import List+import Ratio++-- | yices types+data TypY+ = VarT String+ | SUBTYPE (String,TypY) ExpY+ | SUBRANGE ExpY ExpY+ | ARR [TypY]+ | TUP [TypY]+ | REC [(String,TypY)]+ | DEP (String,TypY)+ | DATATYPE [(String,[(String,TypY)])]+ | SCALAR [String]+ -- BITVECTOR Integer++-- | yices expressions+data ExpY+ = VarE String+ | LitB Bool+ | LitI Integer+ | LitR Rational+ | AND [ExpY]+ | OR [ExpY]+ | NOT ExpY+ | ExpY :=> ExpY+ | ExpY := ExpY+ | ExpY :/= ExpY+ | ExpY :< ExpY+ | ExpY :<= ExpY+ | ExpY :> ExpY+ | ExpY :>= ExpY+ | ExpY :+: ExpY+ | ExpY :-: ExpY+ | ExpY :*: ExpY+ | ExpY :/: ExpY+ | DIV ExpY ExpY+ | MOD ExpY ExpY+ | IF ExpY ExpY ExpY+ | ITE ExpY ExpY ExpY+ | LET [((String,Maybe TypY),ExpY)] ExpY+ -- quantifires+ | FORALL [(String,TypY)] ExpY+ | EXISTS [(String,TypY)] ExpY+ -- functions+ | APP ExpY [ExpY]+ | UPDATE_F ExpY [ExpY] ExpY+ | LAMBDA [(String,TypY)] ExpY+ -- tuples+ | MKTUP [ExpY]+ | SELECT_T ExpY Integer+ | UPDATE_T ExpY Integer ExpY+ -- records+ | MKREC [(String,ExpY)]+ | SELECT_R ExpY String+ | UPDATE_R ExpY String ExpY+ -- bitvectors -- TODO++-- | yices declarations and commands+data CmdY+ = DEFTYP String (Maybe TypY)+ | DEFINE (String,TypY) (Maybe ExpY)+ | ASSERT ExpY+ | ASSERT_P ExpY (Maybe Integer)+ | RETRACT Integer+ | CHECK+ | MAXSAT+ | SETE Bool+ | SETV Integer+ | SETAO Bool+ | PUSH+ | POP+ | ECHO String+ | INCLUDE String+ | RESET+ | STATUS+ | DUMP+ | EXIT++paren s = "("++s++")"++showListSepByWith showFun sep = concat . intersperse sep . map showFun++showListSepBy :: (Show a) => String -> [a] -> String+showListSepBy = showListSepByWith show++showStringsSepBy = showListSepByWith id++showIdTyp (tname,t) = tname++"::"++show t++showIdVal (fname,e) = fname++"::"++show e++showCtorDef (c,[]) = c+showCtorDef (c,idtyps) = paren $ c++" "++showListSepByWith showIdTyp " " idtyps++showBinding ((x,Just t),e) = paren $ showIdTyp(x,t) ++ " " ++ show e+showBinding ((x,Nothing),e) = paren $ x ++ " " ++ show 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++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+ -- 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+ -- 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+ -- 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+ -- 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+ -- 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"+
+ README view
@@ -0,0 +1,1 @@+See Main.hs for example usage.
+ Setup.lhs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain
+ yices.cabal view
@@ -0,0 +1,26 @@+name: yices+version: 0.0.0.1+synopsis: Haskell programming interface to Yices SMT solver+description: Incomplete (no bitvectors) syntax, parser, and inter+ process communication to Yices from Haskell through pipe.+ Purpose for building and using this library was to generate+ test cases from constraints that SMT solvers can solve. I+ only used it for that particular purpose, so the code in+ general is not yet fully tested. Use at your own risk and+ error reports are welcomed. See <http://yices.csl.sri.com/>+ for further information on Yices.+category: Math+license: BSD3+license-file: LICENSE+author: Ki Yung Ahn <kya@pdx.edu>+maintainer: Ki Yung Ahn <kya@pdx.edu>+build-type: Simple+cabal-version: >=1.2+extra-source-files: Main.hs+data-files: README+build-depends: base >= 2 && < 6, haskell98, process, parsec+exposed-modules: Math.SMT.Yices.Syntax,+ Math.SMT.Yices.Parser,+ Math.SMT.Yices.Pipe+ghc-options: -Wall+