Add the ability to ask for satisfying variables, not just counterexamples

[thoughtpolice]

Problem: The default mode for theorem is to find a counterexample of some equation, i.e. a set of inputs to which the result is False.

But I want to find satisfying assignments, i.e. a set of inputs for which the result is True.

Workaround: The easiest way to do this is to invert the clause; that is, if I want to find if any inputs x and y, such that f x y = ... is True, I can write f' x y = not (f x y) and prove that.

Suggestion: It would be nice to have a sat API utility as well as theorem. There are two API points I can think of, regarding what it would look like:

• Should you return the first satisfying assignment, N-many, or all of them?
• What about multiple theorem provers? Do you race all of them until one gives a single satisfying assignment? What if I want every satisfying assignment from every theorem prover?

I'm not sure exactly how you'd like to approach that, but it'd be great to have this!

[LeventErkok]

@thoughtpolice This isn't quite the use model I had in mind for the plugin, but surely it can be implemented.

I think I'd go with the keyword impossible, since you're essentially interested in cases where something cannot happen? The use case for the plugin is that if there's a model, then GHC should stop compiling and abort. In this case, you want to continue if there's no model, so the impossible interpretation seems to be more appropriate:

{-# ANN foo impossible {options = [IgnoreFailure, AnySolver]} #-}

The implementation would simply be the same as theorem, with the only difference being it wouldn't negate the goal. Should be relatively simple to add. (Essentially implementing your workaround inside the plugin.)

For various options, you'll need to add it to the options list (like above) and implement them. It's impossible to tell ahead of time what variants would be useful. But at that point, it's more or less whatever you need it to be.

I'd be happy to take a patch along these lines if you were to implement it.

I should emphasize that, while this would be a nice addition, the plugin is really not usable as it is due to various issues. I tried to capture them here: https://github.com/LeventErkok/sbvPlugin/issues/21

If you're interesting in helping out, tackling those problems (especially those relating to polymorphic core/dictionaries) would be the most bang for the buck.