hasmtlib 1.1.1 → 1.1.2

raw patch · 4 files changed

+30/−6 lines, 4 filesdep ~smtlib-backendsdep ~smtlib-backends-processPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: smtlib-backends, smtlib-backends-process

API changes (from Hackage documentation)

Files

• CHANGELOG.md +22/−0
• hasmtlib.cabal +6/−5
• src/Language/Hasmtlib/Internal/Expr.hs +1/−0
• src/Language/Hasmtlib/Type/Expr.hs +1/−1

@@ -0,0 +1,22 @@+# Changelog++All notable changes to the hasmtlib library will be documented in this+file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),+and this project adheres to [PVP versioning](https://pvp.haskell.org/).++## v1.1.2 _(2024-07-02)_++### Changed+- Minor internal changes++## v1.1.1 _(2024-06-25)_++### Added+- Added this `CHANGELOG.md` file++## v1.1.0 _(2024-06-21)_++### Added+- Added `ArraySort` and full support for its SMTLib2 standard specification

@@ -1,22 +1,23 @@ cabal-version:         3.0  name:                  hasmtlib-version:               1.1.1+version:               1.1.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.   It is highly inspired by ekmett/ersatz which does the same for QSAT.   Communication with external solvers is handled by tweag/smtlib-backends. homepage:              https://github.com/bruderj15/Hasmtlib+bug-reports:           https://github.com/bruderj15/Hasmtlib/issues license:               GPL-3.0-only license-file:          LICENSE author:                Julian Bruder maintainer:            julian.bruder@outlook.com-copyright:             2024 Julian Bruder+copyright:             © 2024 Julian Bruder category:              SMT build-type:            Simple extra-source-files:    README.md-+extra-doc-files:       CHANGELOG.md tested-with:           GHC == 9.6.5  library@@ -61,8 +62,8 @@                      , text                         >= 2.0.2  && < 3                      , data-default                 >= 0.7.1  && < 1                      , lens                         >= 5      && < 6-                     , smtlib-backends              >= 0.4    && < 1-                     , smtlib-backends-process      >= 0.3    && < 1+                     , smtlib-backends              >= 0.4    && < 0.5+                     , smtlib-backends-process      >= 0.3    && < 0.4                      , some                         >= 1.0.6  && < 1.1                      , utf8-string                  >= 1.0.2  && < 2                      , bitvec                       >= 1.1.5  && < 2

@@ -212,6 +212,7 @@   ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v   ArrStore  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v) +  -- Just v if quantified var has been created already, Nothing otherwise   ForAll    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort   Exists    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort 

@@ -5,7 +5,7 @@  , SMTVar(..), varId  , HaskellType  , Value(..), unwrapValue, wrapValue- , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort+ , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort, AllC  , Expr  , for_all , exists  , select, store