执行 n 元分支/列表函数的有效方法？

Question

我正在尝试获取有关 SBV 分支机构性能特征的一些基本信息。

假设我有一个 SInt16 和一个非常稀疏的查找 table 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)

但是，这意味着生成的树会很深。

这重要吗？
如果是，生成一个平衡的分支树是否更好，有效地反映 Map 的结构？或者是否有其他方案可以提供更好的性能？
如果地图中的条目少于 256 个，它会更改任何内容以“压缩”它以便 sCase 在 SInt8 和 Map Int8 a 上工作吗？
这个用例是否有一些比迭代更好的内置 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)

所以去掉所有 newtype，我想分支成 r -> s -> (a, s, w) s.t 类型的东西。 Mergeable s、Mergeable w 和 Mergeable a。

Answer 1

符号查找很昂贵

无论您使用何种数据结构，符号数组查找都将是昂贵的。归结为这样一个事实，即符号执行引擎没有可用于减少状态的信息-space，因此它最终或多或少地完成了您自己编写的代码。

SMTLib 数组

但是，在这些情况下最好的解决方案是实际使用 SMT 对数组的支持：http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml

SMTLib 数组与您认为的常规编程语言中的数组不同：它没有界限。从这个意义上讲，它更像是一张从输入到输出的映射，跨越整个领域。（即，它们等同于函数。）但是 SMT 具有处理数组的自定义理论，因此它们可以更有效地处理涉及数组的问题。（不利的一面是，没有索引越界的概念，也没有以某种方式控制您可以访问的元素范围的概念。不过，您可以自己在抽象之上编写这些代码，由您自己决定如何您想处理此类无效访问。）

如果您有兴趣了解更多关于 SMT 求解器如何处理数组的信息，classic 参考是：http://theory.stanford.edu/~arbrad/papers/arrays.pdf

SBV 中的数组

SBV支持数组，通过SymArrayclass:https://hackage.haskell.org/package/sbv-8.7/docs/Data-SBV.html#t:SymArray

SFunArray类型实际上并没有使用SMTLib数组。这是为了支持不理解数组的求解器，例如 ABC：https://hackage.haskell.org/package/sbv-8.7/docs/Data-SBV.html#t:SFunArray
SArray 类型完全支持 SMTLib 数组：https://hackage.haskell.org/package/sbv-8.7/docs/Data-SBV.html#t:SArray

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

将 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

执行 n 元分支/列表函数的有效方法？

Efficient way to do n-ary branch / tabulated functions?

haskell

optimization

smt

sat

sbv

符号查找很昂贵

SMTLib 数组

SBV 中的数组

将 Haskell 映射转换为 SBV 数组

效率

查询上下文中的数组