search

ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
63 stars 15 forks source link

Consider a more powerful 'decode' #10

Closed ekmett closed 9 years ago

ekmett commented 9 years ago

We currently use

decode :: Codec a => Solution -> a -> Maybe (Decoded a)

but we could upgrade it to

decode :: (Alternative f, Codec a) => Solution -> a -> f (Decoded a)

Then we'd get the current definition from f = Maybe, but the [] instance could enumerate solutions, while other Alternative instances could might more intelligently.

ekmett commented 9 years ago

Done in HEAD.

glguy commented 9 years ago

I imagine we wouldn't be able to enumerate all solutions, but only those that explore possible choices for the unconstrained bits. There might be other solutions that are not compatible with the particular choices made by the prover

ekmett commented 9 years ago

Sure, it enumerates a subset of possible solutions, definitely.