haskell - Haskell SBV 中的状态序列不满足约束
问题描述
我有一个符号枚举,如下所示:
data State = Start | Dot
mkSymbolicEnumeration ''State
评估一个状态在序列中是否有效的函数,相对于前一个状态,被定义为sDot
只能在我们的序列:sStart
sStart
sDot
sStart
sDot
validSequence :: SList State -> SInteger -> SBool
validSequence seq i = case seq .!! i of
sStart -> p1 .== sDot -- sStart can only be preceded by sDot
sDot -> p1 .== sStart -- sDot can only be preceded by sStart
where p1 = seq .!! (i-1)
然后,声明了两组约束。第一个状态seq
应该是 length n
,第二组状态比每个seq !! i
withi /= 0
都应该满足validSequence
:
-- sequence should be of length n
constrain $ L.length seq .== fromIntegral n
-- apply a validSequence constraint for every i in [1..n]
mapM_ (constrain . (validSequence seq) . fromIntegral) [1..n]
当我将此模块加载到ghci
中时,我得到的结果与我期望的不同:
runSMT $ answer 10
-- expecting this: [Dot, Start, Dot, Start, Dot, Start, Dot, Start, Dot, Start]
-- or this: [Start, Dot, Start, Dot, Start, Dot, Start, Dot, Start, Dot]
-- actual result: [Dot, Dot, Dot, Dot, Dot, Dot, Dot, Dot, Dot, Dot]
我不明白的是:
- 为什么实际结果不满足
Dot
只应遵循的约束Start
- 特别是,我做错了
validSequence
什么吗? - 或者,我是否
mapM_
以错误的方式使用呼叫?
完整的可重现代码如下(需要SBV 库):
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
module Sandbox where
import Data.SBV
import Data.SBV.Control
import Data.SBV.List ((.!!))
import qualified Data.SBV.List as L
data State = Start | Dot
mkSymbolicEnumeration ''State
validSequence :: SList State -> SInteger -> SBool
validSequence seq i = case seq .!! i of
sStart -> p1 .== sDot -- sStart can only be preceded by sDot
sDot -> p1 .== sStart -- sDot can only be preceded by sStart
where p1 = seq .!! (i-1)
answer :: Int -> Symbolic [State]
answer n = do
seq <- sList "seq"
-- sequence should be of length n
constrain $ L.length seq .== fromIntegral n
-- apply a validSequence constraint for every i in [1..n]
mapM_ (constrain . (validSequence seq) . fromIntegral) [1..n]
query $ do cs <- checkSat
case cs of
Unk -> error "Solver returned unknown!"
DSat{} -> error "Unexpected dsat result!"
Unsat -> error "Solver couldn't find a satisfiable solution"
Sat -> getValue seq
解决方案
validSequence :: SList State -> SInteger -> SBool
validSequence seq i = case seq .!! i of
sStart -> p1 .== sDot -- sStart can only be preceded by sDot
sDot -> p1 .== sStart -- sDot can only be preceded by sStart
where p1 = seq .!! (i-1)
相当于
validSequence :: SList State -> SInteger -> SBool
validSequence seq i = case seq .!! i of
_ -> p1 .== sDot
where p1 = seq .!! (i-1)
如果是一个新的局部变量,它与任何其他同名变量没有关系, sincesStart
是名称。在 GHC 中打开警告应该报告此名称阴影。
我不能建议如何解决这个问题,因为我不熟悉 SBV。特别是,我看不到(seq .!! i) == sStart
您尝试进行的检查是否可以在 Haskell 级别完成,或者必须在 SBV 级别执行,以便它生成正确的公式以传递给 SMT 求解器。
也许你需要类似(伪代码):
validSequence seq i =
(p2 .== sStart .&& p1 .== sDot) .||
(p1 .== sStart .&& p2 .== sDot)
where p1 = seq .!! (i-1)
p2 = seq .!! i
编辑:基于上述伪代码的实际工作实现,但遵循 SBV 的 DSL:
validSequence :: SList State -> SInteger -> SBool
validSequence seq i =
ite (cur .== sStart) (prev `sElem` [sDot])
$ ite (cur .== sDot) (prev `sElem` [sStart])
sFalse
where cur = seq .!! i
prev = seq .!! (i-1)
推荐阅读
- javascript - Vue - 基于 URL 的自动 API 调用
- java - 在云存储(标准库)等对象之间共享对象中列表的元素
- python - 提取在先前级别嵌套字典中关联的键
- javascript - 如何在自身内部渲染 React 组件
- python - Python数组值分配故障
- r - 在降价到pdf的其他图形标题中引用图形
- python - 使用 matplotlib 的(tk 后端)时出现一个奇怪的错误
- java - 如何在没有 CSR 的情况下在 Tomcat 中安装 GoDaddy SSL 证书?
- hadoop - Yarn Resource Manager UI 中的 Num Off Switch Containers 是什么意思?
- php - JQUERY - 2 个函数不能相互配合