问题描述
我有如下符号枚举:
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
的长度为n
,第二个声明的状态是每个seq !! i
与i /= 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]
-- or this: [Start,Dot]
-- actual result: [Dot,Dot]
我不明白的地方:
- 为什么实际结果不能满足约束
Dot
仅应遵循Start
- 特别是我在
validSequence
中做错什么了吗? - 或者,我是否以错误的方式使用了
mapM_
通话?
完整的可复制代码如下(需要SBV library):
{-# 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)
因为sStart
是一个新的本地变量的名称,该变量与具有相同名称的任何其他变量没有关系。在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)