Символические поиски стоят дорого
Поиск символьного массива будет дорогим независимо от того, какую структуру данных вы используете. Это сводится к тому факту, что механизму символьного выполнения недоступна информация для сокращения пространства состояний, поэтому он в конечном итоге делает более или менее то, что вы написали сами.
Массивы SMTLib
Однако лучшим решением в этих случаях является использование поддержки SMT для массивов: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
Массивы SMTLib отличаются от того, что вы считаете массивом в обычном языке программирования: он не имеет границ. В этом смысле это скорее карта от входов к выходам, охватывающая всю область. (т. е. они эквивалентны функциям.) Но у SMT есть специальные теории для работы с массивами, и поэтому они могут гораздо эффективнее решать проблемы, связанные с массивами. (С другой стороны, нет понятия индекса за пределами границ или какого-либо контроля диапазона элементов, к которым вы можете получить доступ. Однако вы можете кодировать их самостоятельно поверх абстракции, оставляя вам решать, как вы хотите обрабатывать такие недопустимые обращения.)
Если вам интересно узнать больше о том, как решатели SMT работают с массивами, классический справочник: http://theory.stanford.edu/%7Earbrad/papers/arrays.pdf
Массивы в SBV
SBV поддерживает массивы через класс SymArray: https://hackage.haskell.org/package/sbv-8.7/docs/Data-SBV.html#t:SymArray
Между этими типами есть некоторые различия, и приведенные выше ссылки описывают их. Однако в большинстве случаев вы можете использовать их взаимозаменяемо.
Преобразование карты 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#v:freshArray
person
alias
schedule
08.07.2020
