jwaldmann

A value of type `Ersatz.Bit` denotes a Boolean formula, with sharing, so actually, a circuit. I made this to draw the circuit diagram (with graphviz) https://git.imn.htwk-leipzig.de/waldmann/ersatz-viz and perhaps it's useful.

more flexible way of calling other solvers

3

We have `minisatPath` and `cryptominisat5Path` but that does not allow me to call, e.g., glucose, because it needs an extra option to print the model. I am thinking of ```...

this needs to be renamed as well: "see implementations of exists and forall." https://hackage.haskell.org/package/ersatz-0.5/docs/Ersatz-Variable.html

some hlint suggestions I don't agree with

1

Current CI config treats hlint warnings as errors? I agree with most suggestions, and will apply them in my branch where I currently work, but I don't like it that...

sum types: encoding, pattern matching

1

SAT encoding of product types is easy: just concatenate encodings of components. Ersatz already has this. For sum types like `Either a b`, `Maybe a`, we can encode the discriminant...

`class Boolean b` has implication as `(==>) :: b -> b -> b`. I wanted to write reverse implication `

We implement `atmost 1 bs` as (essentially) `sumBits bs

automatic derivation of `instance Codec`?

7

(As #45, this is a request for comments) Can we automate `instance Codec a` in some cases? Examples: if `Decoded a` is ... * a tuple, we just concatenate the...

I am using ersatz's Boolean typeclass in https://hackage.haskell.org/package/obdd (to get names for Boolean operations) I want to also use Ersatz.Counting.exactly (etc.) but they are monorphic (`[Bit] -> Bit`) while the...

https://github.com/ekmett/ersatz/blob/master/src/Ersatz/Bit.hs#L60 ``` data Bit = ... | Run ( forall m s . MonadSAT s m => m Bit ) ``` the idea was to have clause output as a...