Feature: Partitioning all-sat results

[LeventErkok]

It's useful to be able to partition the all-sat results according to arbitrary user given equivalences. We can already express this in SBV, like this:

import Data.SBV

foo = allSatWith z3{ isNonModelVar    = (`notElem` ["p1", "p2"])
                   }
     $ do x <- sInteger "x"
          y <- sInteger "y"

          constrain $ x .> 0
          constrain $ x .< 5

          p1 <- sInteger "p1"
          p2 <- sBool    "p2"
          constrain $ p1 .== x `sMod` 3
          constrain $ p2 .== (y .> 0)

This allows for all-sat to consider equivalence classes amongst all the satisfying states.

Alas, this doesn't print the values of x and y, since we have to make them non-model-vars. We can resolve this in one of two ways:

• Introduce a new config parameter, showTheseVars or similar, so they can be shown again.
• Introduce isPartitionVar parameter, which acts just like isNonModelVar, but otherwise doesn't change printing behavior

I'm inclined towards the second, but perhaps the first one is easier to implement. Need to figure out the most useful form.

[LeventErkok]

Current implementation:

import Data.SBV

foo :: IO AllSatResult
foo = allSatWith z3{allSatMaxModelCount = Just 12} $ do
          x <- sInteger "x"
          y <- sInteger "y"

          partition "p1" $ x .> 0
          partition "p2" $ y .> 0

This prints:

*Main> foo
Solution #1:
  x  =     0 :: Integer
  y  =     1 :: Integer
  p1 = False :: Bool
  p2 =  True :: Bool
Solution #2:
  x  =    1 :: Integer
  y  =    1 :: Integer
  p1 = True :: Bool
  p2 = True :: Bool
Solution #3:
  x  =     1 :: Integer
  y  =     0 :: Integer
  p1 =  True :: Bool
  p2 = False :: Bool
Solution #4:
  x  =     0 :: Integer
  y  =     0 :: Integer
  p1 = False :: Bool
  p2 = False :: Bool
Found 4 different solutions.

If you don't give the partitioning, then you'll get 12 outputs.

[LeventErkok]

Need documentation and an example program, then we can close.