3

我正在尝试获取有关 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's 的结构？还是有其他方案可以提供更好的性能？
  3. 如果地图中的条目少于 256 个，它是否会更改任何内容以“压缩”它以便sCase适用于 anSInt8和 a Map Int8 a？
  4. 对于这个用例，是否有一些内置的 SBV 组合器比 iterated 效果更好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)st和st 类型Mergeable s的东西。Mergeable wMergeable a

4

1 回答 1

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#t:SymArray

这些类型之间存在一些差异，上面的链接描述了它们。但是，对于大多数目的，您可以互换使用它们。

将 Haskell 映射转换为 SBV 数组

回到你原来的问题，我很想用 anSArray来模拟这样的查找。我将其编码为：

{-# 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

于 2020-07-08T15:47:03.553 回答