Constrain a symbolic list on count of elements of a certain type in SBV

Question

Using the SBV library, I'm trying to satisfy conditions on a symbolic list of states:

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]

All works fine except that I need the final list to contain exactly n elements of either [Intro, Start, Content] in total. Currently I do it using a bounded filter:

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

As you can see, the list can be of any length between n+2 and n+6, the important bit is that it has the right count of [sIntro, sStart, sContent] elements within it.

It works all fine, except it's extremely slow. Like, for n=4 it takes a few seconds, but for n>=6 it takes forever (more than 30 minutes and still counting). If I remove the bounded filter constraint, the result is instant with n up to 25 or so.

In the end, I don't particularly care about using L.bfilter. All I need is a way to declare that the final symbolic list should contain exactly n elements of some given types.

-> Is there a faster way to be able to satisfy for count(sIntro || sStart || sContent)?

-- EDIT after discussion in comments:

The code below is supposed to make sure that all valid elements are up-front in the elts list. For example, if we count 8 valids elements from elts, then we take 8 elts and we count the validTaken valid elements in this sub-list. If the result is 8, it means that all the 8 valids elements are up-front in elts. Sadly, this results in a systematic Unsat outcome, even after removing all other constraints. The function works well when tested against some dummy lists of elements, though.

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

Solvers for the sequence logic, while quite versatile, are notoriously slow. For this particular problem, I'd recommend using regular boolean logic, which will perform much better. Here's how I'd code your problem:

{-# 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

Example run:

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

I've been able to run upto answer 500 which returned in about 5 seconds on my relatively old machine.

Making sure all valids are at the beginning

The easiest way to make all the valid elements are at the beginning of the list is to count the alternations in the included value, and make sure you allow only one such transition:

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

This'll make sure all the valids precede the suffix of the list that contain the invalid entries. When you write your other properties, you'd have to check that both the current element and the next element is valid. In template form:

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

By symbolically looking at the values of included x and included y, you can determine if they are both included, or if x is the last element, or if they're both out; and write the corresponding constraints as implications in each case. The above shows the case for when you're in the middle of the sequence somewhere, with both x and y included.