1

我想用符号表达式（SBV）的条件编写一个 Haskell 列表理解。我用下面的小例子重现了这个问题。

import Data.SBV

allUs :: [SInteger] 
allUs = [0,1,2]  

f :: SInteger -> SBool 
f 0 = sTrue
f 1 = sFalse
f 2 = sTrue

someUs :: [SInteger] 
someUs = [u | u <- allUs, f u == sTrue]

，show someUs这给出了以下错误

*** Data.SBV: Comparing symbolic values using Haskell's Eq class!
***
*** Received:    0 :: SInteger  == 0 :: SInteger
*** Instead use: 0 :: SInteger .== 0 :: SInteger
***
*** The Eq instance for symbolic values are necessiated only because
*** of the Bits class requirement. You must use symbolic equality
*** operators instead. (And complain to Haskell folks that they
*** remove the 'Eq' superclass from 'Bits'!.)

CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Symbolic.hs:1009:23 in sbv-8.8.5-IR852OLMhURGkbvysaJG5x:Data.SBV.Core.Symbolic

将条件更改为f u .== sTrue也会产生错误

<interactive>:8:27: error:
    • Couldn't match type ‘SBV Bool’ with ‘Bool’
      Expected type: Bool
        Actual type: SBool
    • In the expression: f u .== sTrue
      In a stmt of a list comprehension: f u .== sTrue
      In the expression: [u | u <- allUs, f u .== sTrue]

如何解决这个问题？

4

2 回答 2

3

你的f和你的都不someUs是书面的象征性可计算的。理想情况下，这些应该是类型错误，被立即拒绝。这是因为符号值不能是Eq类的实例：为什么？因为确定符号值的相等性需要调用底层求解器；所以结果不能是Bool；它应该是真的SBool。但是 Haskell 不允许在模式匹配中使用广义保护来允许这种可能性。（这也是有充分理由的，所以这并不是 Haskell 的错。只是这两种编程风格不能很好地结合在一起。）

您可以问为什么 SBV 将符号值作为Eq类的实例。它是实例的唯一原因Eq是错误消息告诉您：因为我们希望它们成为Bits类的实例；作为Eq超类的要求。但这完全是另一个讨论。

基于此，如何在 SBV 中编写函数？以下是您f以符号样式编写代码的方式：

f :: SInteger -> SBool
f i = ite (i .== 0) sTrue
    $ ite (i .== 1) sFalse
    $ ite (i .== 2) sTrue
    $               sFalse   -- arbitrarily filled to make the function total

丑，但这是唯一的写法，除非你想玩一些准引用的把戏。

关于someUs：这也不是你可以直接象征性地写的东西：这被称为脊椎混凝土列表。如果不对单个元素实际运行求解器，SBV 就无法知道结果列表的长度。通常，您不能filter在具有符号元素的脊椎混凝土列表上执行类似的功能。

解决方案是使用所谓的符号列表和有界列表抽象。这不是很令人满意，但是您可以做的最好的事情是避免终止问题：

{-# LANGUAGE OverloadedLists #-}

import Data.SBV
import Data.SBV.List
import Data.SBV.Tools.BoundedList

f :: SInteger -> SBool
f i = ite (i .== 0) sTrue
    $ ite (i .== 1) sFalse
    $ ite (i .== 2) sTrue
    $               sFalse   -- arbitrarily filled to make the function total

allUs :: SList Integer
allUs = [0,1,2]

someUs :: SList Integer
someUs = bfilter 10 f allUs

当我运行它时，我得到：

*Main> someUs
[0,2] :: [SInteger]

但是你会问电话中的那个号码10是bfilter什么？好吧，这个想法是假设所有列表的长度都有某种上限，并且Data.SBV.Tools.BoundedList导出了一堆方法来轻松处理它们；都采用绑定参数。只要输入最多这个长度，它们就可以正常工作。如果您的列表长于给定的范围，则无法保证会发生什么。（一般来说，它会在绑定时切断你的列表，但你不应该依赖这种行为。）

在https://hackage.haskell.org/package/sbv-8.12/docs/Documentation-SBV-Examples-Lists-BoundedMutex有一个与 BMC（有界模型检查）协调使用此类列表的示例.html

总而言之，在符号上下文中处理列表会带来一些建模成本以及您可以做多少，这是由于 Haskell 中的限制（其中Bool是固定类型而不是类）以及无法递归处理的底层求解器定义的功能都很好。后者主要是因为这样的证明需要归纳，而 SMT 求解器不能开箱即用地进行归纳。但是，如果您使用类似 BMC 的想法遵循游戏规则，您可以在合理范围内处理问题的实际实例。

于 2021-03-17T19:02:24.003 回答
-1

(.==)接受两个实例EqSymbolic，返回一个SBool. 在列表推导中，条件是使用guard函数实现的。

这是它的样子：

guard :: Alternative f => Bool -> f ()
guard False = empty
guard True = pure ()

对于列表，emptyis[]和pure ()返回单例列表[()]。计算结果为的列表中的任何成员都False将返回一个空列表而不是一个单元项，将其排除在链下的计算之外。

[True, False, True] >>= guard
= concatMap guard [True, False, True]
= concat $ map guard [True, False, True]
= concat $ [[()], [], [()]]
= [(), ()]

当上下文被展平时，第二个分支将被排除，因此它从计算中“修剪”。

似乎您在这里有两个问题 - 当您在 中进行模式匹配时f，您正在使用Eq该类进行比较。这就是 SBV 错误的来源。由于您的值很接近，您可以使用select，它接受一个项目列表、一个默认值、一个计算为索引的表达式，并尝试index从该列表中获取第一个项目。

你可以重写f为

f :: SInteger -> SBool
f = select [sTrue, sFalse, sTrue] sFalse

第二个问题是守卫显式查找Bool，但(.==)仍然返回一个SBool. 看着Data.SBV，您应该能够将其强制转换为常规Boolusing unliteral，它试图将一个SBV值解包为等效的 Haskell 值。

fromSBool :: SBool -> Bool
fromSBool = fromMaybe False . unliteral

someUs :: [SInteger]
someUs = [u | u <- allUs, fromSBool (f u)]
-- [0 :: SInteger, 2 :: SInteger]
于 2021-03-17T19:17:04.933 回答