Вне пределов `select`, хотя я` ограничиваю` индекс

Question

У меня есть список значений статической длины ks :: [SInt16] и индекс x :: SInt16. Я хочу проиндексировать список, используяx:

(.!) :: (Mergeable a) => [a] -> SInt16 -> a
xs .! i = select xs (error "(.!) : out of bounds") i

Я ожидал, что смогу использовать (.!) с достаточно стесненным x как это:

sat $ do
    let ks = [1, 3, 5, 2, 4]      

    x <- sInt16 "x"
    constrain $ 0 .<= x .&& x .< literal (fromIntegral $ length ks)

    let y = ks .! x
    return $ y .< x

Однако это не удается из-за ошибки, исходящей от (.!).

Конечно, в моей реальной программе я использую (.!) повсюду в местах, где нет подходящего значения по умолчанию для использования в select.Как я могу индексировать в список с ограниченным индексом?

Answer 1

Простое решение

selectполностью расширяется SBV во время символьного выполнения, поэтому, как вы выяснили, вы должны указать правильное значение по умолчанию. Итак, если вы хотите использоватьselect вы должны найти здесь реальное значение.

Чтобы удовлетворить вашу неотложную потребность, я предлагаю просто определить:

(.!) :: (Mergeable a) => [a] -> SInt16 -> a
[]       .! _ = error "(.!): Empty list!"
xs@(x:_) .! i = select xs x i

Если вы убедитесь, что наложили достаточно ограничений на i, это должно работать нормально.

Немного лучший подход

Вышеупомянутое требует, чтобы ваш пользователь следил за правильными ограничениями на индексную переменную, и это может стать довольно непростым делом. В этих случаях можно использовать простой прием - вместо этого использовать "умный" конструктор. Сначала определите:

import Data.SBV

mkIndex :: SIntegral b => String -> [a] -> Symbolic (SBV b)
mkIndex nm lst = do i <- free nm
                    constrain $ 0 .<= i .&& i .< literal (fromIntegral (length lst))
                    pure i

(.!) :: (Mergeable a) => [a] -> SInt16 -> a
[]       .! _ = error "(.!): Empty list!"
xs@(x:_) .! i = select xs x i

Теперь вы можете сказать:

p = sat $ do let ks = [1, 3, 5, 2, 4]

             x <- mkIndex "x" ks

             let y = ks .! x
             return $ y .< x

Он немного более подробный, чем ваш оригинал (так как вам нужно передать список, который вы хотите проиндексировать), но он может сэкономить много головной боли в будущем. Кроме того, вы можете изменить свойmkIndex поставить диагностику или при необходимости установить дополнительные ограничения.

Более оборонительный подход

Приведенный выше "лучший" подход требует, чтобы вы заранее знали длину списка, в который вы будете индексировать. В вашем примере это очевидно, но я могу представить себе ситуации, когда эта информация будет недоступна. Если это так, я бы порекомендовал создать символическое значение для элемента доступа за границу и самостоятельно отслеживать его. Это более сложно, но вы можете скрыть большую часть этого за простым типом данных. Что-то типа:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

newtype Index a b = Index (SBV a, SBV b)

mkIndex :: (SymVal a, SymVal b) => String -> Symbolic (Index a b)
mkIndex nm = do def <- free $ nm ++ "_access_out_of_bounds_value"
                idx <- free nm
                pure $ Index (def, idx)

(.!) :: (SymVal a, SIntegral b) => [SBV a] -> Index a b -> SBV a
xs .! Index (i, i') = select xs i i'

Теперь предположим, что вы пытаетесь сделать sat, но поставьте неверные ограничения на ваш индекс:

p = sat $ do let ks = [1, 3, 5, 2, 4]

             xi@(Index (_, x)) :: Index Int16 Int16 <- mkIndex "x"

             -- incorrectly constrain x here to do out-of-bounds
             constrain $ x .> 10

             let y = ks .! xi

             pure $ y .< x

Ты получишь:

*Main> p
Satisfiable. Model:
  x_access_out_of_bounds_value =     0 :: Int16
  x                            = 16386 :: Int16

Таким образом, вы можете увидеть, что что-то пошло не так, и какое значение выбрал решатель для удовлетворения случая доступа за пределы.

Резюме

Какой подход вы выберете, действительно зависит от ваших реальных потребностей. Но я бы порекомендовал выбрать хотя бы вторую альтернативу, если это возможно, поскольку решатель SMT всегда может "умно" выбрать значения, чтобы дать вам неожиданные модели. Таким образом вы защитили себя, по крайней мере, от самых очевидных ошибок. В производственной системе я бы настаивал на третьем подходе, поскольку отладка ошибок, возникающих из-за сложных ограничений, на практике может быть довольно сложной. Чем больше "отслеживающих" переменных вы оставите для себя, тем лучше.