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