2

基本上我想知道，有没有办法用 SBV 库编写以下类型的函数：

(SBV a, SBV b) -> SBV (a,b)

这似乎应该是可能的：如果我们有两个符号值，我们可以创建一个新的符号值，作为一个具体的对，其元素是两个输入的符号值或具体值。但是我找不到这样的东西，并且该SBV类型没有暴露其构造函数。

这可能吗？

4

1 回答 1

3

听起来你需要这个tuple功能。这是一个例子：

import Data.SBV
import Data.SBV.Tuple

tup :: (SymVal a, SymVal b) => (SBV a, SBV b) -> SBV (a, b)
tup = tuple

tst :: Predicate
tst = do x <- sInteger "x"
         y <- sInteger "y"
         z <- sTuple "xy"

         return $ tup (x, y) .== z

当然，tuple它本身最多可以处理 8 个；以上只是您想要的确切类型的一个实例化。我们有：

$ ghci a.hs
GHCi, version 8.6.4: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( a.hs, interpreted )
Ok, one module loaded.
*Main> sat tst
Satisfiable. Model:
  x  =     0 :: Integer
  y  =     1 :: Integer
  xy = (0,1) :: (Integer, Integer)

还有untuple另一个方向的功能。它们都在Data.SBV.Tuple您必须显式导入的模块中。（您还可以在同一模块中找到类似镜头的访问器，它允许您编写 ,^._1等^._2来提取元组的字段；z^._2如上例所示。）

于 2019-07-03T23:21:28.523 回答