simple-smt 0.7.1 → 0.8
raw patch · 3 files changed
+85/−13 lines, 3 files
Files
- CHANGES +1/−0
- SimpleSMT.hs +83/−12
- simple-smt.cabal +1/−1
CHANGES view
@@ -1,3 +1,4 @@+0.8: Support for declare; loading of strings/files; more sugar for SMT commands 0.6.0: Allow finer-grained logging 0.5.5: Add support for unsupported results 0.5.3: Add 'zeroExtend' and 'signExtend'
SimpleSMT.hs view
@@ -5,13 +5,12 @@ module SimpleSMT ( -- * Basic Solver Interface- Solver+ Solver(..) , newSolver- , command- , stop , ackCommand , simpleCommand , simpleCommandMaybe+ , loadFile -- ** S-Expressions , SExpr(..)@@ -29,8 +28,10 @@ , setOption, setOptionMaybe , push, pushMany , pop, popMany+ , inNewScope , declare , declareFun+ , declareDatatype , define , defineFun , assert@@ -40,7 +41,7 @@ , getConsts, getConst , Value(..) - -- * Convenienct Functoins for SmtLib-2 Epxressions+ -- * Convenience Functions for SmtLib-2 Epxressions , fam , fun , const@@ -63,7 +64,9 @@ -- ** Connectives , not , and+ , andMany , or+ , orMany , xor , implies @@ -72,6 +75,7 @@ -- ** Relational Predicates , eq+ , distinct , gt , lt , geq@@ -83,6 +87,7 @@ -- ** Arithmetic , add+ , addMany , sub , neg , mul@@ -196,7 +201,7 @@ -- | Start a new solver process. newSolver :: String {- ^ Executable -} ->- [String] {- ^ Argumetns -} ->+ [String] {- ^ Arguments -} -> Maybe Logger {- ^ Optional logging here -} -> IO Solver newSolver exe opts mbLog =@@ -248,7 +253,31 @@ return solver +-- | Load the contents of a file.+loadFile :: Solver -> FilePath -> IO ()+loadFile s file = loadString s =<< readFile file +-- | Load a raw SMT string.+loadString :: Solver -> String -> IO ()+loadString s str = go (dropComments str)+ where+ go txt+ | all isSpace txt = return ()+ | otherwise =+ case readSExpr txt of+ Just (e,rest) -> command s e >> go rest+ Nothing -> fail $ unlines [ "Failed to parse SMT file."+ , txt+ ]++ dropComments = unlines . map dropComment . lines+ dropComment xs = case break (== ';') xs of+ (as,_:_) -> as+ _ -> xs++++ -- | A command with no interesting result. ackCommand :: Solver -> SExpr -> IO () ackCommand proc c =@@ -302,7 +331,7 @@ push :: Solver -> IO () push proc = pushMany proc 1 --- | Restore to last check-point. A sepcial case of 'popMany'.+-- | Restore to last check-point. A special case of 'popMany'. pop :: Solver -> IO () pop proc = popMany proc 1 @@ -314,8 +343,14 @@ popMany :: Solver -> Integer -> IO () popMany proc n = simpleCommand proc [ "pop", show n ] +-- | Execute the IO action in a new solver scope (push before, pop after)+inNewScope :: Solver -> IO a -> IO a+inNewScope s m =+ do push s+ m `X.finally` pop s + -- | Declare a constant. A common abbreviation for 'declareFun'. -- For convenience, returns an the declared name as a constant expression. declare :: Solver -> String -> SExpr -> IO SExpr@@ -328,6 +363,30 @@ do ackCommand proc $ fun "declare-fun" [ Atom f, List as, r ] return (const f) +-- | Declare an ADT using the format introduced in SmtLib 2.6.+declareDatatype ::+ Solver ->+ String {- ^ datatype name -} ->+ [String] {- ^ sort parameters -} ->+ [(String, [(String, SExpr)])] {- ^ constructors -} ->+ IO ()+declareDatatype proc t [] cs =+ ackCommand proc $+ fun "declare-datatype" $+ [ Atom t+ , List [ List (Atom c : [ List [Atom s, argTy] | (s, argTy) <- args]) | (c, args) <- cs ]+ ]+declareDatatype proc t ps cs =+ ackCommand proc $+ fun "declare-datatype" $+ [ Atom t+ , fun "par" $+ [ List (map Atom ps)+ , List [ List (Atom c : [ List [Atom s, argTy] | (s, argTy) <- args]) | (c, args) <- cs ]+ ]+ ]++ -- | Declare a constant. A common abbreviation for 'declareFun'. -- For convenience, returns the defined name as a constant expression. define :: Solver ->@@ -495,7 +554,7 @@ int x | x < 0 = neg (int (negate x)) | otherwise = Atom (show x) --- | Real (well, reational) literals.+-- | Real (well, rational) literals. real :: Rational -> SExpr real x = realDiv (int (denominator x)) (int (numerator x)) @@ -542,14 +601,20 @@ not :: SExpr -> SExpr not p = fun "not" [p] --- | Conjucntion.+-- | Conjunction. and :: SExpr -> SExpr -> SExpr and p q = fun "and" [p,q] +andMany :: [SExpr] -> SExpr+andMany xs = if null xs then bool True else fun "and" xs+ -- | Disjunction. or :: SExpr -> SExpr -> SExpr or p q = fun "or" [p,q] +orMany :: [SExpr] -> SExpr+orMany xs = if null xs then bool False else fun "or" xs+ -- | Exclusive-or. xor :: SExpr -> SExpr -> SExpr xor p q = fun "xor" [p,q]@@ -574,7 +639,10 @@ eq :: SExpr -> SExpr -> SExpr eq x y = fun "=" [x,y] --- | Greather-then+distinct :: [SExpr] -> SExpr+distinct xs = if null xs then bool True else fun "distinct" xs++-- | Greater-then gt :: SExpr -> SExpr -> SExpr gt x y = fun ">" [x,y] @@ -614,6 +682,9 @@ add :: SExpr -> SExpr -> SExpr add x y = fun "+" [x,y] +addMany :: [SExpr] -> SExpr+addMany xs = if null xs then int 0 else fun "+" xs+ -- | Subtraction. sub :: SExpr -> SExpr -> SExpr sub x y = fun "-" [x,y]@@ -639,7 +710,7 @@ mod :: SExpr -> SExpr -> SExpr mod x y = fun "mod" [x,y] --- | Is the number divisible by the given constante.+-- | Is the number divisible by the given constant. divisible :: SExpr -> Integer -> SExpr divisible x n = List [ fam "divisible" [n], x ] @@ -672,11 +743,11 @@ bvAnd :: SExpr -> SExpr -> SExpr bvAnd x y = fun "bvand" [x,y] --- | Bitwsie disjucntion.+-- | Bitwise disjunction. bvOr :: SExpr -> SExpr -> SExpr bvOr x y = fun "bvor" [x,y] --- | Bitwsie exclusive or.+-- | Bitwise exclusive or. bvXOr :: SExpr -> SExpr -> SExpr bvXOr x y = fun "bvxor" [x,y]
simple-smt.cabal view
@@ -1,5 +1,5 @@ name: simple-smt-version: 0.7.1+version: 0.8 synopsis: A simple way to interact with an SMT solver process. description: A simple way to interact with an SMT solver process. license: BSD3