Add `class Unknown` for all types that have a complete allocator

[jwaldmann]

(Happy New Year!)

I find the following quite useful - but before I make a PR, I'd like to collect opinions.

An allocator produces Bits that encode some unknown value. E.g., exists is an allocator for Bit. A complete allocator just depends on the result type (and on nothing else). This can be expressed by

class Unknown a where unknown :: MonadSAT s m => m a
instance Unknown Bit where unknown = exists
instance (Unknown a, Unknown b) => Unknown (a,b,c) where
  unknown = (,,) <$> unknown <*> unknown <*> unknown

and for arrays - in case the index type is complete

instance (Bounded i, Ix i, Unknown e) => Unknown (A.Array i e)

Examples:

• https://gitlab.imn.htwk-leipzig.de/waldmann/misc/tree/master/cal/2019/12
• https://github.com/ekmett/ersatz/blob/master/tests/Z001.hs#L19

Can we have something like this in ersatz? Or do we already have it?

[glguy]

Is the Variable class what you're looking for? exists :: (Variable a, MonadState s m, HasSAT s) => m a

[jwaldmann]

Ah yes. Variable.exists is my Unknown.unknown.

exists is not a class method, to avoid duplication in its implementation (with the implementation of forall). This design separates these issues:

• introduce a variable (literally)
• declare its quantifier (exist/forall) Structural recursion (for compound types) is used for implementing literally (only).

Perhaps the above can be added to the documentation?