hasmtlib 1.0.1 → 1.0.2

raw patch · 5 files changed

+22/−18 lines, 5 filesdep ~smtlib-backendsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: smtlib-backends

API changes (from Hackage documentation)

Files

• README.md +2/−0
• hasmtlib.cabal +2/−2
• src/Language/Hasmtlib/Type/MonadSMT.hs +13/−11
• src/Language/Hasmtlib/Type/SMT.hs +1/−1
• src/Language/Hasmtlib/Type/Solver.hs +4/−4

@@ -94,6 +94,8 @@   ```haskell       cvc5Living <- interactiveSolver cvc5       interactiveWith cvc5Living $ do+        setLogic "QF_LIA"    +        setOption $ ProduceModels True         x <- var @IntSort         assert $ x === 42         result <- checkSat

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               1.0.1+version:               1.0.2 synopsis:              A monad for interfacing with external SMT solvers description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.@@ -59,7 +59,7 @@                      , text                         >= 2.0.2  && < 3                      , data-default                 >= 0.7.1  && < 1                      , lens                         >= 5      && < 6-                     , smtlib-backends              >= 0.3    && < 1+                     , smtlib-backends              >= 0.4    && < 1                      , smtlib-backends-process      >= 0.3    && < 1                      , utf8-string                  >= 1.0.2  && < 2                      , bitvec                       >= 1.1.5  && < 2

@@ -13,18 +13,20 @@ -- | A 'MonadState' that holds an SMT-Problem. class MonadState s m => MonadSMT s m where   -- | Construct a variable.-  -- +  --   This is mainly intended for internal use.+  --   In the API use 'var'' instead.+  --      -- @   -- x :: SMTVar RealType <- smtvar' (Proxy @RealType)   -- @-  smtvar'    :: forall t. KnownSMTSort t => Proxy t -> m (SMTVar t)+  smtvar' :: forall t. KnownSMTSort t => Proxy t -> m (SMTVar t)      -- | Construct a variable as expression.   --    -- @   -- x :: Expr RealType <- var' (Proxy @RealType)   -- @-  var'       :: forall t. KnownSMTSort t => Proxy t -> m (Expr t)+  var' :: forall t. KnownSMTSort t => Proxy t -> m (Expr t)    -- | Assert a boolean expression.   -- @@ -32,7 +34,7 @@   -- x :: Expr IntType <- var @IntType   -- assert $ x + 5 === 42   -- @-  assert    :: Expr BoolSort -> m ()+  assert :: Expr BoolSort -> m ()    -- | Set an SMT-Solver-Option.   -- @@ -44,9 +46,9 @@   -- | Set the logic for the SMT-Solver to use.   --    -- @-  -- setLogic "QF_LRA"+  -- setLogic \"QF_LRA\"   -- @-  setLogic  :: String -> m ()+  setLogic :: String -> m ()  -- | Wrapper for 'var'' which hides the 'Proxy'. var :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (Expr t)@@ -54,8 +56,8 @@ {-# INLINE var #-}  -- | Wrapper for 'smtvar'' which hides the 'Proxy'.--- | This is mainly intended for internal use.--- | In the API use 'var' instead.+--   This is mainly intended for internal use.+--   In the API use 'var' instead. smtvar :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (SMTVar t) smtvar = smtvar' (Proxy @t) {-# INLINE smtvar #-}@@ -116,10 +118,10 @@   --   -- @   -- x <- var @RealSort-  -- y <- var @RealSort+  -- y <- var   -- assert $ x >? y && y <? (-1)   -- res <- checkSat-  -- case checkSat of+  -- case res of   --   Unsat -> print "Unsat. Cannot get model."   --   r     -> do   --     model <- getModel@@ -134,7 +136,7 @@   -- x <- var @RealSort   -- assert $ x >? 10   -- res <- checkSat-  -- case checkSat of+  -- case res of   --   Unsat -> print "Unsat. Cannot get value for 'x'."   --   r     -> do   --     x' <- getValue x

@@ -27,7 +27,7 @@ $(makeLenses ''SMT)  instance Default SMT where-  def = SMT 0 mempty mempty mempty mempty+  def = SMT 0 mempty mempty mempty [ProduceModels True]  instance MonadState SMT m => MonadSMT SMT m where   smtvar' _ = fmap coerce $ lastVarId <+= 1

@@ -10,7 +10,7 @@ import Data.Default import Control.Monad.State --- | Data that can have a 'B.Solver'+-- | Data that can have a 'B.Solver'. class WithSolver a where   withSolver :: B.Solver -> a @@ -36,7 +36,7 @@ -- main :: IO () -- main = do --   res <- solveWith (solver cvc5) $ do---     setLogic "QF_LIA"+--     setLogic \"QF_LIA\" --  --     x <- var @IntSort -- @@ -59,14 +59,14 @@ --  -- @ -- import Language.Hasmtlib--- import Data.Proxy -- import Control.Monad.IO.Class --  -- main :: IO () -- main = do --   cvc5Living <- interactiveSolver cvc5 --   interactiveWith cvc5Living $ do---     setLogic "QF_LIA"+--     setOption $ ProduceModels True+--     setLogic \"QF_LIA\" --  --     x <- var @IntSort --