hasmtlib 1.0.0 → 1.0.1

raw patch · 3 files changed

+3/−32 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +1/−1
• hasmtlib.cabal +1/−30
• src/Language/Hasmtlib/Type/Solver.hs +1/−1

@@ -1,4 +1,4 @@-![Static Badge](https://img.shields.io/badge/Lang-GHC2021-blue) [![Haskell-CI](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml) [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0)+[![Hackage](https://img.shields.io/hackage/v/hasmtlib.svg)](https://hackage.haskell.org/package/hasmtlib) ![Static Badge](https://img.shields.io/badge/Lang-GHC2021-blue) [![Haskell-CI](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml) [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0)  # Hasmtlib 

@@ -1,41 +1,12 @@ cabal-version:         3.0  name:                  hasmtlib-version:               1.0.0+version:               1.0.1 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.   It is highly inspired by ekmett/ersatz which does the same for QSAT.   Communication with external solvers is handled by tweag/smtlib-backends.-  .-  For example we can utilize existing instances for V3 to symbolically use Num and Metric operations.-  .-  > {-# LANGUAGE DataKinds #-}-  .-  > import Language.Hasmtlib-  > import Linear-  .-  > -- instances with default impl-  > instance Codec a => Codec (V3 a)-  > instance Variable a => Variable (V3 a)-  .-  > main :: IO ()-  > main = do-  >   res <- solveWith (solver cvc5) $ do-  >     setLogic "QF_NRA"-  >-  >     u :: V3 (Expr RealSort) <- variable-  >     v <- variable-  >-  >     assert $ dot u v === 5-  >-  >     return (u,v)-  >-  >   print res-  .-  May print:-  > (Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0)) homepage:              https://github.com/bruderj15/Hasmtlib license:               GPL-3.0-only license-file:          LICENSE

@@ -25,7 +25,7 @@ --    results ('Unknown'). -- -- 2. A 'Decoded' answer that was decoded using the solution to @prob@. Note---    that this answer is only meaningful if the 'Result' is 'Satisfied or Unknown' and+--    that this answer is only meaningful if the 'Result' is 'Sat' or 'Unknown' and --    the answer value is in a 'Just'. -- -- Here is a small example of how to use 'solveWith':