simple-smt 0.8 → 0.9.1

raw patch · 3 files changed

+34/−1 lines, 3 files

Files

• CHANGES +1/−0
• SimpleSMT.hs +32/−0
• simple-smt.cabal +1/−1

@@ -1,3 +1,4 @@+0.9:   Support for working with unsat-cores 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

@@ -26,6 +26,8 @@     -- * Common SmtLib-2 Commands   , setLogic, setLogicMaybe   , setOption, setOptionMaybe+  , produceUnsatCores+  , named   , push, pushMany   , pop, popMany   , inNewScope@@ -39,7 +41,9 @@   , Result(..)   , getExprs, getExpr   , getConsts, getConst+  , getUnsatCore   , Value(..)+  , sexprToVal      -- * Convenience Functions for SmtLib-2 Epxressions   , fam@@ -322,10 +326,14 @@ setLogic :: Solver -> String -> IO () setLogic s x = simpleCommand s [ "set-logic", x ] + -- | Set the solver's logic, returning False if the logic is unsupported. setLogicMaybe :: Solver -> String -> IO Bool setLogicMaybe s x = simpleCommandMaybe s [ "set-logic", x ] +-- | Request unsat cores.  Returns if the solver supports them.+produceUnsatCores :: Solver -> IO Bool+produceUnsatCores s = setOptionMaybe s ":produce-unsat-cores" "true"  -- | Checkpoint state.  A special case of 'pushMany'. push :: Solver -> IO ()@@ -497,7 +505,25 @@ getConst :: Solver -> String -> IO Value getConst proc x = getExpr proc (Atom x) +-- | Returns the names of the (named) formulas involved in a contradiction.+getUnsatCore :: Solver -> IO [String]+getUnsatCore s =+  do res <- command s $ List [ Atom "get-unsat-core" ]+     case res of+       List xs -> mapM fromAtom xs+       _       -> unexpected "a list of atoms" res+  where+  fromAtom x =+    case x of+      Atom a -> return a+      _      -> unexpected "an atom" x +  unexpected x e =+    fail $ unlines [ "Unexpected response from the SMT Solver:"+                   , "  Expected: " ++ x+                   , "  Result: " ++ showsSExpr e ""+                   ]+ --------------------------------------------------------------------------------  @@ -812,6 +838,12 @@          SExpr store x y z = fun "store" [x,y,z] ++--------------------------------------------------------------------------------+-- Attributes++named :: String -> SExpr -> SExpr+named x e = fun "!" [e, Atom ":named", Atom x ]   --------------------------------------------------------------------------------

@@ -1,5 +1,5 @@ name:                simple-smt-version:             0.8+version:             0.9.1 synopsis:            A simple way to interact with an SMT solver process. description:         A simple way to interact with an SMT solver process. license:             BSD3