微信公众号搜"智元新知"关注
微信扫一扫可直接关注哦!

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

如何解决Haskell SBV中的状态序列不满足约束条件

我有如下符号枚举:

data State = Start | Dot
mkSymbolicEnumeration ''State

定义了用于评估状态在序列中相对于先前状态是否有效的函数,使得sDot仅应以sstart开头,而sstart应仅在sDot之前-从理论上讲,这意味着我们不应在序列中连续两个sstartsDot

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 !! ii /= 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)

版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。