LeventErkok/sbv — pull request #81 by gridaphobe (2014-02-10 05:06:41+00:00)
Title: assert negation of model + equivalence classes in allSat

Sorry I didn't get around to submitting a pull request sooner! Your code does basically what mine did, with a small difference. I assert the negation of the model and the equivalence classes together, rather than splitting them into two separate assertions. I think this is the right thing to do because the results are more intuitive (to me at least :)). E.G.

```haskell
p0 = do
[l, l0, l1] <- symbolics ["l", "l0", "l1"]
constrain $ len l0 .== 0
constrain $ len l1 .== 1
x :: SInteger <- symbolic "x"
constrain $ x .== 0 ||| x.== 1
return $ l .== l0 ||| l .== l1
```

In my opinion this should have 4 satisfying assignments, but your patch only finds 2.

Thanks!