CODEWITHSUNDEEP
haskellsbv
lucaspena
lucaspena

Reputation: 11

Writing to a symbolic number of spots in a symbolic array

I have an SArray Integer Integer and I want to write k times to that array. For example, I want to call writeArray arr 1 10, writeArray arr 2 10, ..., writeArray arr k 10. However, I do not know how to do this when k itself is symbolic. Is this even possible?

I tried some things like this:

import qaulified Data.SBV as S
import qualified Data.SBV.List as S

writeBlock :: S.SArray Integer Integer -> S.SInteger -> S.SInteger -> S.SInteger -> S.SArray Integer Integer
writeBlock arr sz k v =
  let keyVals = S.zip (keyList sz k) (valueList sz v)
  in S.foldl writeArray' arr keyVals
  where
    keyList 0 _ = S.nil
    keyList size key = key S..: keyList (size - 1) (key + 1)

    valueList 0 _ = S.nil
    valueList size value = value S..: valueList (size - 1) value

    writeArray' arr (key, value) = S.writeArray arr key value

which fails since SArray is not an SBV a. I also tried using concrete lists, which failed with different errors. Please let me know if there is any way to do this. Thanks, any help is appreciated.

Upvotes: 1

Views: 74

Answers (1)

alias
alias

Reputation: 30428

When symbolically programming, you want to be very careful with what variables are used for control and what variables are used as data. It's perfectly fine to have your data to be completely symbolic. But you want to avoid symbolic variables in your control-flow. That is, data-flow of your program can be completely symbolic, but control-path should be (mostly) concrete.

Since you're using k as a control-variable, any sort of recursion you do on it will fail to terminate. Think about how something like this will execute:

    valueList 0    _     = S.nil
    valueList size value = value S..: valueList (size - 1) value

There are two problems here: First you cannot use pattern-matching on a symbolic variable. (There's really nothing SBV can do about this, Haskell pattern-matching only works on concrete values; and for good reason.) So, the "symbolic" way of writing something like this would be:

    valueList size value = ite (size .== 0)
                               S.nil
                               (value S..: valueList (size - 1) value)

Unfortunately, this won't work either, because it'll fail to terminate. The ite construct (if-then-else) has no clue when the recursion stops, since size is symbolic.

One way to deal with this problem is if you know a concrete upper bound on size. In that case, you can use that to do a bounded-loop. This would be the preferred solution if you know, in advance, such a concrete bound.

You can see an example of using an upper bound in https://hackage.haskell.org/package/sbv-10.3/docs/src/Documentation.SBV.Examples.CodeGeneration.GCD.html#sgcd, where this idea is used to implement GCD symbolically. Perhaps you can use a similar strategy to limit the recursion-depth, making it concretely computable.

Upvotes: 2

Related Questions