Эффективный способ выполнять n-арные ветвления / табличные функции?

Я пытаюсь получить базовую информацию о характеристиках производительности веток в SBV.

Предположим, у меня есть SInt16 и очень разреженная таблица поиска Map Int16 a. Я могу реализовать поиск с помощью вложенныхite:

sCase :: (Mergeable a) => SInt16 -> a -> Map Int16 a -> a
sCase x def = go . toList
  where
    go [] = def
    go ((k,v):kvs) = ite (x .== literal k) v (go kvs)

Однако это означает, что сгенерированное дерево будет очень глубоким.

  1. Это имеет значение?
  2. Если да, то лучше ли вместо этого создать сбалансированное дерево ветвей, эффективно отражающее Mapструктура? Или есть какая-то другая схема, которая дала бы еще лучшую производительность?
  3. Если на карте меньше 256 записей, изменится ли она что-нибудь, чтобы "сжать" ее так, чтобы sCase работает над SInt8 и Map Int8 a?
  4. Есть ли какой-нибудь встроенный комбинатор SBV для этого варианта использования, который работает лучше, чем повторение ite?

РЕДАКТИРОВАТЬ: Оказывается, очень важно то, что у меняaесть, поэтому позвольте мне добавить к этому несколько деталей. Я сейчас используюsCase для перехода в вычислении с сохранением состояния, смоделированном как RWS r w s a, со следующими экземплярами:

instance forall a. Mergeable a => Mergeable (Identity a) where
    symbolicMerge force cond thn els = Identity $ symbolicMerge force cond (runIdentity thn) (runIdentity els)

instance (Mergeable s, Mergeable w, Mergeable a, forall a. Mergeable a => Mergeable (m a)) => Mergeable (RWST r w s m a) where
        symbolicMerge force cond thn els = Lazy.RWST $
            symbolicMerge force cond (runRWST thn) (runRWST els)

Так что убирая все newtypes, я хотел бы перейти к чему-нибудь типа r -> s -> (a, s, w) ул Mergeable s, Mergeable w а также Mergeable a.

Источник

1 ответ

Решение

Символический поиск стоит дорого

Поиск в символьном массиве будет дорогостоящим независимо от того, какую структуру данных вы используете. Это сводится к тому факту, что механизму символического выполнения не доступна информация, позволяющая сократить пространство состояний, поэтому он в конечном итоге выполняет более или менее то, что вы сами кодировали.

SMTLib Массивы

Однако лучшим решением в таких случаях является использование поддержки SMT для массивов: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml

Массивы SMTLib отличаются от того, что вы бы рассматривали как массив на обычном языке программирования: они не имеют границ. В этом смысле это скорее карта от входов к выходам, охватывающая весь домен. (т. е. они эквивалентны функциям.) Но у SMT есть собственные теории для работы с массивами, и поэтому они могут справляться с проблемами, связанными с массивами, гораздо более эффективно. (С другой стороны, нет понятия выхода индекса за границы или какого-либо управления диапазоном элементов, к которым вы можете получить доступ. Однако вы можете закодировать их самостоятельно поверх абстракции, оставив вам решать, как вы хотите обрабатывать такие недействительные доступы.)

Если вам интересно узнать больше о том, как решатели SMT работают с массивами, классическая ссылка: http://theory.stanford.edu/~arbrad/papers/arrays.pdf

Массивы в SBV

SBV поддерживает массивы через SymArrayкласс: https://hackage.haskell.org/package/sbv-8.7/docs/Data-SBV.html

Между этими типами есть некоторые различия, и приведенные выше ссылки описывают их. Однако для большинства целей вы можете использовать их как взаимозаменяемые.

Преобразование карты Haskell в массив SBV

Возвращаясь к вашему исходному вопросу, я бы хотел использовать SArrayсмоделировать такой взгляд. Я бы закодировал это как:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import qualified Data.Map as M
import Data.Int

-- Fill an SBV array from a map
mapToSArray :: (SymArray array, SymVal a, SymVal b) => M.Map a (SBV b) -> array a b -> array a b
mapToSArray m a = foldl (\arr (k, v) -> writeArray arr (literal k) v) a (M.toList m)

И используйте его как:

g :: Symbolic SBool
g = do let def = 0

       -- get a symbolic array, initialized with def
       arr <- newArray "myArray" (Just def)

       let m :: M.Map Int16 SInt16
           m = M.fromList [(5, 2), (10, 5)]

       -- Fill the array from the map
       let arr' :: SArray Int16 Int16 = mapToSArray m arr

       -- A simple problem:
       idx1 <- free "idx1"
       idx2 <- free "idx2"

       pure $ 2 * readArray arr' idx1 + 1 .== readArray arr' idx2

Когда я запускаю это, я получаю:

*Main> sat g
Satisfiable. Model:
  idx1 =  5 :: Int16
  idx2 = 10 :: Int16

Вы можете запустить его как satWith z3{verbose=True} g чтобы увидеть выходные данные SMTLib, которые он генерирует, что позволяет избежать дорогостоящих поисков, просто делегируя эти задачи бэкэнд-решателю.

Эффективность

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

Массивы в контексте запроса

Функция newArrayработает в символическом контексте. Если вы находитесь в контексте запроса, вместо этого используйтеfreshArray: https://hackage.haskell.org/package/sbv-8.7/docs/Data-SBV-Control.html

Источник
Другие вопросы по тегам