ersatz
ersatz copied to clipboard
ekmett
A monad for interfacing with external SAT solvers
Per @jwaldmann 's comment in #79 , this adds a unary ("bitmap") representation for finite sets and does so by extending existing functionality in `Ersatz.Relation`: ```haskell newtype Set a =...
The example is from #87. I am not quite sure whether to following analysis is correct. Ersatz will fuse `And [And [x,y], z]` into `And [x,y,z]`. This reduces the number...
I am asserting that the sum of two (long) numbers (represented by `Ersatz.Bits`) is small (zero, one). This uses operator `(
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.
This PR adds properties and operations for modeling functional relations to `Ersatz.Relation`. With respect to #78, where #78 uses `error` when two argument relations have mismatched bounds, the functions here...
Per the title, adds a module full of properties related to order-theoretic structures for use with homogeneous binary relations; generally the minimal structure where the definitions make sense is a...
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
- [ ] evaluate & port the funsat solver - [ ] get the ideas from Schoning '99 and its child papers [Moser Derandomized 2010](http://arxiv.org/pdf/1008.4067.pdf) etc. Not a practical solver,...
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...