Changelog for ersatz-0.5
0.5 [2023.09.08]
-
The
forall
function inErsatz.Variable
has been renamed toforall_
, since a future version of GHC will make the use offorall
as an identifier an error. -
The types of
decode
andsolveWith
have been slightly less general:-decode :: MonadPlus f => Solution -> a -> f (Decoded a) +decode :: Solution -> a -> Maybe (Decoded a) -solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a)) +solveWith :: (Monad m, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
That is, these functions now use
Maybe
instead of an arbitraryMonadPlus
. This change came about because:- Practically all uses of
solveWith
in the wild are already pickingn
to beMaybe
, and - The behavior of
decode
andsolveWith
forMonadPlus
instances besidesMaybe
could produce surprising results, as this behavior was not well specified.
- Practically all uses of
-
Fix a bug in which
decode
could return inconsistent results with solution that underconstrain variables. For instance:do b <- exists pure [b, not b]
Previously, this could decode to
[False, False]
(an invalid assignment).ersatz
now adopts the convention that unconstrained non-negativeLiteral
s will always be assignedFalse
, and unconstrained negativeLiteral
s will always be assignedTrue
. This means that the example above would now decode to[False, True]
.
0.4.13 [2022.11.01]
- Make the examples compile with
mtl-2.3.*
. - Add more documentation to the
Ersatz.Relation.*
modules, theVariable
class, and the data types inErsatz.Bits
.
0.4.12 [2022.08.11]
- Add
Equatable
andOrderable
instances for more base and containers types - Add solver support for
z3
0.4.11 [2022.05.18]
- Allow building with
mtl-2.3.*
andtransformers-0.6.*
.
0.4.10 [2021.11.16]
- Allow the test suite to build with recent GHCs.
- Drop support for pre-8.0 versions of GHC.
0.4.9 [2021.02.17]
- Allow building with
lens-5.*
. - Change to
build-type: Simple
0.4.8 [2020.01.29]
- Add
MonadSAT
andMonadQSAT
- Achieve forward compatibility with GHC proposal 229.
0.4.7 [2019.06.01]
- Add
anyminisat
andtrySolvers
0.4.6 [2019.05.20]
- Add support for
cryptominisat5
0.4.5 [2019.05.02]
- Allow
ersatz-regexp-grid
to build withbase-4.13
(GHC 8.8).
0.4.4 [2018.08.13]
- Avoid the use of failable pattern matches in
do
-notation to support building with GHC 8.6, which enablesMonadFailDesugaring
.
0.4.3 [2018.07.03]
- Make the test suite compile on GHC 8.6.
- Allow building with
containers-0.6
.
0.4.2
- Add
Semigroup
instances forClause
andFormula
. - Generalize
regular
,regular_in_degree
,regular_out_degree
,max_in_degree
,min_in_degree
,max_out_degree
, andmin_out_degree
to work over heterogeneous relations. - Add
buildFrom
toErsatz.Relation.Data
. - Add
difference
,reflexive_closure
, andsymmetric_closure
toErsatz.Relation.Op
. - Add
anti_symmetric
andtotal
toErsatz.Relation.Prop
.
0.4.1
- Add a library dependency on the
doctests
test suite
0.4
- Performance improvements for CNF printing and parsing
- Add the
Ersatz.Counting
,Ersatz.Relation
,Ersatz.Relation.Data
,Ersatz.Relation.Prop
, andErsatz.Relation.Op
modules - Eliminate the
Or
constructor fromBit
towards using AIG - Fix error in the SAT encoding of the
choose
function - Revamp
Setup.hs
to usecabal-doctest
. This makes it build withCabal-2.0
, and makes thedoctest
s work withcabal new-build
and sandboxes.
0.3.1
- Removed the explicit
Safe
annotations. They can't be maintained by mere mortals. Patches to mark packages upstream asTrustworthy
will be accepted as needed.
0.3
- Unified
Encoding
andDecoding
intoCodec
- Unified the
forall
andexists
implementations into a singleliterally
method inVariable
class. - Added
Orderable
type class and instances - Added
Ersatz.Bits.Bits
for variable-sized bit arithmetic. - Renamed
Ersatz.Bits.half_adder
tohalfAdder
- Renamed
Ersatz.Bits.full_adder
tofullAdder
- Added new examples
- Dropped
blaze
package dependency in favor of newerbytestring
- Significantly shrank the number of "Trustworthy" modules
- Added various generic
V1
instances - Added
Equatable
instances forMap
andIntMap
- Added
Ersatz.BitChar
module for computing withChar
andString
- Wider version bounds for
transformers
andmtl
.
0.2.6.1
- Exported
Ersatz.Variable.GVariable
0.2.6
temporary 1.2
support
0.2.5.1
- Slightly faster builds due to dropping the need for
template-haskell
.
0.2.5
- Support for GHC 7.8 and
lens
4.x
0.2.3
- SafeHaskell support
0.2.2
- Added examples to the documentation.
- Made the examples build as
ersatz-sudoku
andersatz-regexp-grid
.
0.2.1
- Added
examples/sudoku
, a sudoku solver.
0.2.0.1
- Fixed an overly conservative bound on
containers
.
0.2
- Converted to
Control.Lens
internally. - Added
Ersatz.Solver.DepQBF
- Added a bunch of example dimacs files
- The types now prevent one from applying a solver that does not support QSAT to a problem that requires it
- Added
examples/regexp-grid
, a program that solves the regular expression crossword - Made some optimizations to the formula generation.
regexp-grid
went from 71737 literals and 427725 clauses to 8618 literals and 172100 clauses and got much faster - Based
and
andor
inBoolean
onFoldable
; addedall
andany
0.1.0.2
- Added correct links to the source repository and issue tracker to the cabal project
0.1
- Repository Initialized