simple-smt 0.9.5 → 0.9.6
raw patch · 3 files changed
+71/−3 lines, 3 files
Files
- CHANGES +1/−0
- SimpleSMT.hs +69/−2
- simple-smt.cabal +1/−1
CHANGES view
@@ -1,3 +1,4 @@+0.9.6: Suport for quoated symbols and recursive functions 0.9.5: Expose `loadString` 0.9.4: Add `toInt` and `toReal` 0.9.3: Fix incorrect rendering or `real` literals
SimpleSMT.hs view
@@ -37,6 +37,8 @@ , declareDatatype , define , defineFun+ , defineFunRec+ , defineFunsRec , assert , check , Result(..)@@ -46,11 +48,18 @@ , Value(..) , sexprToVal - -- * Convenience Functions for SmtLib-2 Epxressions+ -- * Convenience Functions for SmtLib-2 Expressions , fam , fun , const+ , app + -- * Convenience Functions for SmtLib-2 identifiers+ , quoteSymbol+ , symbol+ , keyword+ , as + -- ** Types , tInt , tBool@@ -132,7 +141,7 @@ import Prelude hiding (not, and, or, abs, div, mod, concat, const) import qualified Prelude as P-import Data.Char(isSpace)+import Data.Char(isSpace, isDigit) import Data.List(unfoldr,intersperse) import Data.Bits(testBit) import Data.IORef(newIORef, atomicModifyIORef, modifyIORef', readIORef,@@ -212,6 +221,8 @@ readSExpr :: String -> Maybe (SExpr, String) readSExpr (c : more) | isSpace c = readSExpr more readSExpr (';' : more) = readSExpr $ drop 1 $ dropWhile (/= '\n') more+readSExpr ('|' : more) = do (sym, '|' : rest) <- pure (span ((/=) '|') more)+ Just (Atom ('|' : sym ++ ['|']), rest) readSExpr ('(' : more) = do (xs,more1) <- list more return (List xs, more1) where@@ -452,8 +463,34 @@ $ [ Atom f, List [ List [const x,a] | (x,a) <- as ], t, e] return (const f) +-- | Define a recursive function or a constant. For convenience,+-- returns an the defined name as a constant expression. This body+-- takes the function name as an argument.+defineFunRec :: Solver ->+ String {- ^ New symbol -} ->+ [(String,SExpr)] {- ^ Parameters, with types -} ->+ SExpr {- ^ Type of result -} ->+ (SExpr -> SExpr) {- ^ Definition -} ->+ IO SExpr+defineFunRec proc f as t e =+ do let fs = const f+ ackCommand proc $ fun "define-fun-rec"+ $ [ Atom f, List [ List [const x,a] | (x,a) <- as ], t, e fs]+ return fs +-- | Define a recursive function or a constant. For convenience,+-- returns an the defined name as a constant expression. This body+-- takes the function name as an argument.+defineFunsRec :: Solver ->+ [(String, [(String,SExpr)], SExpr, SExpr)] ->+ IO ()+defineFunsRec proc ds = ackCommand proc $ fun "define-funs-rec" [ decls, bodies ]+ where+ oneArg (f, args, t, _) = List [ Atom f, List [ List [const x,a] | (x,a) <- args ], t]+ decls = List (map oneArg ds)+ bodies = List (map (\(_, _, _, body) -> body) ds) + -- | Assume a fact. assert :: Solver -> SExpr -> IO () assert proc e = ackCommand proc $ fun "assert" [e]@@ -575,6 +612,36 @@ const :: String -> SExpr const f = fun f [] +app :: SExpr -> [SExpr] -> SExpr+app f xs = List (f : xs)++-- Identifiers -----------------------------------------------------------------------++-- | Symbols are either simple or quoted (c.f. SMTLIB v2.6 S3.1).+-- This predicate indicates whether a character is allowed in a simple+-- symbol. Note that only ASCII letters are allowed.+allowedSimpleChar :: Char -> Bool+allowedSimpleChar c =+ isDigit c || c `elem` (['a' .. 'z'] ++ ['A' .. 'Z'] ++ "~!@$%^&*_-+=<>.?/")++isSimpleSymbol :: String -> Bool+isSimpleSymbol s@(c : _) = P.not (isDigit c) && all allowedSimpleChar s+isSimpleSymbol _ = False++quoteSymbol :: String -> String+quoteSymbol s + | isSimpleSymbol s = s+ | otherwise = '|' : s ++ "|"++symbol :: String -> SExpr+symbol = Atom . quoteSymbol++keyword :: String -> SExpr+keyword s = Atom (':' : s)++-- | Generate a type annotation for a symbol+as :: SExpr -> SExpr -> SExpr+as s t = fun "as" [s, t] -- Types -----------------------------------------------------------------------
simple-smt.cabal view
@@ -1,5 +1,5 @@ name: simple-smt-version: 0.9.5+version: 0.9.6 synopsis: A simple way to interact with an SMT solver process. description: A simple way to interact with an SMT solver process. license: BSD3