What's an easy way to generate an SBV formula given some data using Haskell?

Question

Assuming a tree in which the nodes may or may not be present, I would like to generate a formula in which:

1. there's a boolean variable for each node (to represent whether it's present or not),
2. a root if free (may or may not be present), and
3. a node can only be present if its parent is present (child implies the parent).

My goal is to generate all possible subtrees of the given shape using allSat. For example, consider the datatype and an example tree:

data Tree
    = Leaf
    | Tree [ Tree ]
    deriving Show

tree :: Tree
tree
    = Tree            -- T1
        [ Leaf        -- L1
        , Tree        -- T2
            [ Leaf    -- L2
            , Leaf    -- L3
            ]
        ]

translating that tree should introduce booleans for each node T1, T2, L1, L2, L3 and a set of constraints:

L1 => T1
T2 => T1
L2 => T2
L3 => T2

The following code produces the right solutions (11):

main :: IO ()
main = do
    res <- allSat . forSome ["T1", "T2", "L1", "L2", "L3"] $
        \ (t1::SBool) t2 l1 l2 l3 ->
            (   (l1 ==> t1)
            &&& (t2 ==> t1)
            &&& (l2 ==> t2)
            &&& (l3 ==> t2)
            )
    putStrLn $ show res

So, how can I generate the formula given to allSat given some concrete tree?

An alternative solution would be to construct the action like this:

main :: IO ()
main = do
    res <- allSat $ makePredicate tree
    putStrLn $ show res

makePredicate :: Tree -> Predicate
makePredicate    _     = do
        t1 <- exists "T1"
        l1 <- exists "L1"
        constrain $ l1 ==> t1
        t2 <- exists "T2"
        constrain $ t2 ==> t1
        l2 <- exists "L2"
        constrain $ l2 ==> t2
        l3 <- exists "L3"
        constrain $ l3 ==> t2
        return true

EDIT: I discovered an answer to another SO question, which is related. The idea would be to construct an action like in the alternative solution above but during the fold of the tree. That is possible because Symbolic is a monad.

Answer 1

In order to figure out how the recursion should work, it is instructive to rewrite the alternative solution from the question to match the shape of the tree:

makePredicate :: Tree -> Predicate
makePredicate    _     = do
        -- SBool for root
        t1 <- exists "T1"
        -- predicates for children
        c1 <- do
                -- SBool for child
                l1 <- exists "L1"
                -- child implies the parent
                constrain $ l1 ==> t1
                return true
        c2 <- do
                t2 <- exists "T2"
                constrain $ t2 ==> t1
                -- predicates for children
                c3 <- do
                        l2 <- exists "L2"
                        constrain $ l2 ==> t2
                        return true                    
                c4 <- do
                        l3 <- exists "L3"
                        constrain $ l3 ==> t2
                        return true
                return $ c3 &&& c4 &&& true 
        return $ c1 &&& c2 &&& true 

As we can see, we first create an SBool variable for a node, then process it's children, and then return a conjunction. That means we can map over children to produce their Predicates first, then fold the list of the Predicates with true as the initial value.

The following code traverses the tree and produces a formula. First, we simplify the Tree type

{-# LANGUAGE ScopedTypeVariables #-}
import Data.SBV

data Tree
    = Node String [ Tree ]
    deriving Show

tree :: Tree
tree
    = Node "T1"
        [ Node "L1" []
        , Node "T2"
            [ Node "L2" []
            , Node "L3" []
            ]
        ]

Then we recursively traverse the tree and produce a Predicate for each node. The root is special: because it does not have a parent, there's nothing to imply.

main :: IO ()
main = do
    res <- allSat $ makeRootPredicate tree
    putStrLn $ show res

makeRootPredicate :: Tree       -> Predicate
makeRootPredicate    (Node i cs) = do
    x <- exists i
    cps <- mapM (makeNodePredicate x) cs
    return $ bAnd cps

makeNodePredicate :: SBool -> Tree       -> Predicate
makeNodePredicate    parent   (Node i cs) = do
    x <- exists i
    constrain $ x ==> parent
    cps <- mapM (makeNodePredicate x) cs
    return $ bAnd cps

Finally, I am using bAnd to create a conjunction of the predicates (as pointed out in the comment).

Because bAnd internally uses foldr, we get a formula

(c1 &&& (c2 &&& true))

substituting for c1 and c2, we get

(((l1 ==> t1) &&& true) &&& (((t2 ==> t1) &&& c3 &&& c4 &&& true) &&& true))

substituting for c3 and c4, we get

(((l1 ==> t1) &&& true) &&& (((t2 ==> t1) &&& ((l2 ==> t2) &&& true) &&& ((l3 ==> t2) &&& true) &&& true) &&& true))

As indicated in the comment, SBV will internally simplify the formula by partially evaluating it where possible. So, the trues will be eliminated.