title: What's an easy way to generate an SBV formula given some data using Haskell?
body: <p>Assuming a tree in which the nodes may or may not be present, I would like to generate a formula in which:</p>
  
  <ol>
  <li>there's a boolean variable for each node (to represent whether it's present or not), </li>
  <li>a root if free (may or may not be present), and</li>
  <li>a node can only be present if its parent is present (child implies the parent).</li>
  </ol>
  
  <p>My goal is to generate all possible subtrees of the given shape using <code>allSat</code>. For example, consider the datatype and an example <code>tree</code>:</p>
  
  <pre><code>data Tree
      = Leaf
      | Tree [ Tree ]
      deriving Show
  
  tree :: Tree
  tree
      = Tree            -- T1
          [ Leaf        -- L1
          , Tree        -- T2
              [ Leaf    -- L2
              , Leaf    -- L3
              ]
          ]
  </code></pre>
  
  <p>translating that tree should introduce booleans for each node <code>T1, T2, L1, L2, L3</code> and a set of constraints:</p>
  
  <pre><code>L1 =&gt; T1
  T2 =&gt; T1
  L2 =&gt; T2
  L3 =&gt; T2
  </code></pre>
  
  <p>The following code produces the right solutions (11):</p>
  
  <pre><code>main :: IO ()
  main = do
      res &lt;- allSat . forSome ["T1", "T2", "L1", "L2", "L3"] $
          \ (t1::SBool) t2 l1 l2 l3 -&gt;
              (   (l1 ==&gt; t1)
              &amp;&amp;&amp; (t2 ==&gt; t1)
              &amp;&amp;&amp; (l2 ==&gt; t2)
              &amp;&amp;&amp; (l3 ==&gt; t2)
              )
      putStrLn $ show res
  </code></pre>
  
  <p>So, how can I generate the formula given to <code>allSat</code> given some concrete <code>tree</code>?</p>
  
  <p>An alternative solution would be to construct the action like this:</p>
  
  <pre><code>main :: IO ()
  main = do
      res &lt;- allSat $ makePredicate tree
      putStrLn $ show res
  
  makePredicate :: Tree -&gt; Predicate
  makePredicate    _     = do
          t1 &lt;- exists "T1"
          l1 &lt;- exists "L1"
          constrain $ l1 ==&gt; t1
          t2 &lt;- exists "T2"
          constrain $ t2 ==&gt; t1
          l2 &lt;- exists "L2"
          constrain $ l2 ==&gt; t2
          l3 &lt;- exists "L3"
          constrain $ l3 ==&gt; t2
          return true
  </code></pre>
  
  <p>EDIT: I discovered an <a href="https://stackoverflow.com/a/23234919/3642157">answer to another SO question</a>, 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.</p>