Haskell SBV 中的状态序列不满足约束

Question

我有一个如下所示的符号枚举：

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, 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 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

Answer 1

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)

Haskell SBV 中的状态序列不满足约束

Sequence of states in Haskell SBV doesn't satisfy constraints

haskell

solver

smt

sat

sbv