代码之家  ›  专栏  ›  技术社区  ›  Cactus

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

  •  0
  • Cactus  · 技术社区  · 4 年前

    我试图获得一些关于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组合器比迭代的更有效 伊特 ?

    编辑 :事实证明,我的工作很重要 a 是的,所以让我补充一些细节。我目前正在使用 斯卡斯 在建模为 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 s、 我想分门别类 r -> s -> (a, s, w) s、 t。 Mergeable s , Mergeable w Mergeable a .

    0 回复  |  直到 4 年前
        1
  •  1
  •   alias    4 年前

    象征性的查找很昂贵

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

    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数组

    回到你最初的问题,我很想用 萨雷 来模拟这样一种仰视。我将其编码为:

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

    推荐文章