约束SBV中某种类型元素的计数的符号列表

Question

使用SBV库，我试图满足一个符号状态列表的条件：

data State = Intro | Start | Content | Comma | Dot
mkSymbolicEnumeration ''State

-- examples of such lists
[Intro, Start, Content, Comma, Start, Comma, Content, Dot]
[Intro, Comma, Start, Content, Comma, Content, Start, Dot]

所有操作都很好，但我需要最终的列表才能确切地包含任何一个n元素的[Intro, Start, Content]。目前，我使用的是一个有界的过滤器：

answer :: Int -> Symbolic [State]
answer n = do
    seq <- sList "seq"

    let maxl = n+6
    let minl = n+2
    constrain $ L.length seq .<= fromIntegral maxl
    constrain $ L.length seq .>= fromIntegral minl

    -- some additional constraints hidden for brevity purposes

    let etypes e = e `sElem` [sIntro, sStart, sContent]
    constrain $ L.length (L.bfilter maxl etypes seq) .== fromIntegral n

正如您所看到的，列表可以是n+2和n+6之间的任意长度，重要的一点是它有正确的[sIntro, sStart, sContent]元素计数。

这一切都很好，但它的非常慢。就像，对于n=4，它需要几秒钟，但是对于n>=6，它要花费很长时间(超过30分钟，而且还在计数)。如果我删除有界过滤器约束，结果是即时的，n高达25左右。

最后，我并不特别关心使用L.bfilter。我所需要的只是一种方法来声明最终的符号列表应该包含某些给定类型的、、n元素。

count(sIntro || sStart || sContent)**?** -> 有更快的方法可以满足的要求吗？

-经讨论后编辑评论：

下面的代码应该确保所有有效的元素都在elts列表的前面。例如，如果我们从valids中计数8个elts元素，那么我们就可以在这个子列表中计算validTaken有效元素。如果结果是8，则意味着所有8个valids元素都在elts中处于领先地位。可悲的是，这会导致系统的Unsat结果，即使在删除所有其他约束之后也是如此。不过，当对一些虚拟元素列表进行测试时，该函数工作得很好。

-- | test that all valid elements are upfront in the list of elements
validUpFront :: SInteger -> [Elem] -> SBool
validUpFront valids elts =
    let takeValids = flip take elts <$> (fromInteger <$> unliteral valids)
        validTaken = sum $ map (oneIf . included) $ fromMaybe [] takeValids
    in valids .== validTaken

-- ...

answer n = runSMT $ do

    -- ...

    let valids = sum $ map (oneIf . included) elts :: SInteger
    constrain $ validUpFront valids elts

Answer 1

序列逻辑的求解器虽然用途广泛，但速度却很慢。对于这个特殊的问题，我建议使用规则布尔逻辑，它的性能要好得多。下面是我给你的问题编码的方法：

{-# LANGUAGE TemplateHaskell    #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE StandaloneDeriving #-}

import Data.SBV
import Data.SBV.Control
import Data.Maybe
import Control.Monad

data State = Intro | Start | Content | Comma | Dot
mkSymbolicEnumeration ''State

data Elem = Elem { included :: SBool
                 , element  :: SState
                 }

new :: Symbolic Elem
new = do i <- free_
         e <- free_
         pure Elem {included = i, element = e}

get :: Elem -> Query (Maybe State)
get e = do isIn <- getValue (included e)
           if isIn
               then Just <$> getValue (element e)
               else pure Nothing

answer :: Int -> IO [State]
answer n = runSMT $ do
    let maxl = n+6
    let minl = n+2

    -- allocate upto maxl elements
    elts <- replicateM maxl new

    -- ask for at least minl of them to be valid
    let valids :: SInteger
        valids = sum $ map (oneIf . included) elts
    constrain $ valids .>= fromIntegral minl

    -- count the interesting ones
    let isEtype e  = included e .&& element e `sElem` [sIntro, sStart, sContent]
        eTypeCount :: SInteger
        eTypeCount = sum $ map (oneIf . isEtype) elts

    constrain $ eTypeCount .== fromIntegral n

    query $ do cs <- checkSat
               case cs of
                 Sat -> catMaybes <$> mapM get elts
                 _   -> error $ "Query is " ++ show cs

示例运行：

*Main> answer 5
[Intro,Comma,Comma,Intro,Intro,Intro,Start]

我已经能够跑到answer 500，它在我相对老旧的机器上返回了大约5秒。

确保所有的阀门都在开始的时候

使所有有效元素位于列表开头的最简单方法是计数所包含的值中的变化，并确保只允许一个这样的转换：

-- make sure there's at most one-flip in the sequence.
-- This'll ensure all the selected elements are up-front.
let atMostOneFlip []     = sTrue
    atMostOneFlip (x:xs) = ite x (atMostOneFlip xs) (sAll sNot xs)

constrain $ atMostOneFlip (map included elts)

这将确保包含无效条目的列表后缀前面的所有valids。编写其他属性时，必须检查当前元素和下一个元素是否有效。模板形式：

foo (x:y:rest) = ((included x .&& included y) .=> (element y .== sStart .=> element x .== sDot))
                .&& foo (y:rest)

通过象征性地查看included x和included y的值，您可以确定它们是包含在一起的，还是x是最后一个元素，还是两者都是外部元素；并在每种情况下都将相应的约束写成含义。上面的例子显示了当您处于序列中间的某个位置时的情况，其中包括x和y。