![]() |
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支持阵列,通过
这些类型之间存在一些差异,上面的链接描述了它们。然而,在大多数情况下,您可以互换使用它们。 将Haskell映射转换为SBV数组
回到你最初的问题,我很想用
并将其用作:
当我运行这个时,我得到:
你可以把它当作
效率这是否“有效”的问题实际上取决于你的地图中有多少元素是用来构建数组的。元素的数量越多,约束越复杂,效率就越低。特别是,如果你对一个符号索引进行写操作,我预计求解时间会变慢。如果它们都是常量,那么应该是相对性能的。和符号编程一样,在没有看到实际问题并进行实验的情况下,很难预测任何性能。 查询上下文中的数组
功能
|