jwaldmann

Default implementation is ``` class Boolean b where ... choose f t s = (f && not s) || (t && s) ``` This is strict in f. It's overridden...

(note to self, and implementation plan) in Satchmo, I have "non-overflowing" numbers, cf. https://hackage.haskell.org/package/satchmo-2.9.9.3/docs/Satchmo-Binary-Op-Fixed.html where the implementation emits extra clauses that assert that overflow does not happen. This is useful...

feature req: bit vector with type-indexed length

1

using type-lits and possibly https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2 even if all the operations are fixed-width it would already be an improvement because we could remove all the individual Bit types.

There are Num instances for Bit1, Bit2, Bits. Semantics should be clarified: how do the handle overflow? It seems - Bit{1,2} silently ignore overflow (so Bit arithmetical semantics is "modulo...

wanted: assertClause :: [Bit] -> m ()

3

(Note: I will investigate, but I welcome comments. See also #33) Currently, there seems to be no way to assert a clause. I want this: ``` assertClause :: (HasSAT s,...

I was surprised that `Bit3` (and later) has no Num instance. Easiest way is to go via `Bits`, as in ``` instance Num Bit3 where fromInteger = fromBits . fromInteger...

improve documentation of Ersatz.Counting

3

(I will do this) The functions in this module are trivial ``` exactly :: Int -> [ Bit ] -> Bit exactly k bs = encode (fromIntegral k) === sumBit...

view the actual heap structure with ghc-debug

1

`ersatz` realizes observable sharing. Sometimes I find it hard to imagine the actual DAG that this creates. And even harder if some rewriting is applied. In such cases it'd be...

reading the satisfying assignment is way too slow

7

(see test case in issue #16)

CNF output is way too slow

4

Run the following (it creates and solves a formula that is not hard). Take the total time, and compare to actual solver time. E.g., argument 100000, on my machine: total...