Ranges over SIntegers

[Torrencem]

I'm trying to construct an SList Integer out of two SIntegers, the equivalent of writing [a..b] in normal haskell, but I'm finding it surprisingly difficult to represent this in SBV.

I first tried to find a builtin function which would accomplish this, with no luck. Obviously I can't do something like implode, because the list [a..b] would have length depending on an SInteger. I also was trying to use something to build it myself using subList over the integers, but I was having trouble constructing the SList [0..] (which is surprising to me as well).

Any suggestions on how to construct the SList [a..b] where a and b are SIntegers? Thanks

[LeventErkok]

I'd go with a recursive function:

import Data.SBV
import Data.SBV.List

range :: SInteger -> SInteger -> SList Integer
range = smtFunction "range" $ \lo hi ->
           ite (lo .> hi)
               nil
               (lo .: range (lo+1) hi)

Now you can say things like:

*Main> range 3 0
[] :: [SInteger]

*Main> range (-12) (-4)
[-12,-11,-10,-9,-8,-7,-6,-5,-4] :: [SInteger]

*Main> range 3 3
[3] :: [SInteger]

*Main> range 5 12
[5,6,7,8,9,10,11,12] :: [SInteger]

*Main> sat $ \a b -> Data.SBV.List.length (range a b) .== 10
Satisfiable. Model:
  s0 = 14458 :: Integer
  s1 = 14467 :: Integer

*Main> sat $ \a b -> Data.SBV.List.length (range a b) .== 0 .&& a .< b
Unsatisfiable

Note that this relies on recursive function definitions on the SMTLib side. What this means is that the logic becomes semi-decidable; so unless your constraints are sufficiently "simple" for the backend solver, you might end-up getting unknown or, (more likely) the solver might run forever. For instance, if you try:

*Main> prove $ \a  ->  Data.SBV.List.length (range a a) .==  1
Q.E.D.

which is nice. You can even do:

*Main> prove $ \a b -> Data.SBV.List.length (range a b) .== (b - a + 1)
Falsifiable. Counter-example:
  s0 =  0 :: Integer
  s1 = -2 :: Integer

But the following won't terminate any time soon:

*Main> prove $ \a b -> a .<= b .=> Data.SBV.List.length (range a b) .== (b - a + 1)
... does not terminate ...

The rule-of-thumb here is that if the solver can prove the property with a finite (and not terribly large!) number of unrollings of the recursive definitions involved, it'll most likely find a model or a proof. But if the proof requires induction, the backend solver will go to an infinite loop.

Hope this helps out!

[Torrencem]

Aha, this is exactly what I was looking for, thank you! I had noticed smtFunction, but the type and documentation were slightly confusing to me as to how to make use of it in a case like this one. This is very much appreciated

[Torrencem]

As to your note at the end, I hope we can give some kind of fact like x \in range a b <--> a <= x <= b to the solver (and prove it somehow) and it'll be a bit more effective. I have to take a look at our application though, since this might suffice for now

[LeventErkok]

Great.. regarding the confusing documentation: Patches are always welcome that improve the documentation or add interesting examples. Send PR's if you can!