ekmett/ersatz

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

Closed this issue · 2 comments

jwaldmann commented

(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:

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

glguy commented

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

jwaldmann commented

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?