使用Haskell生成SBV公式的简单方法是什么？

Question

假设树中的节点可能存在，也可能不存在，我想生成一个公式，其中：

1. 每个节点都有一个布尔变量(用于表示它是否存在)，
2. 根如果是自由的(可能存在也可能不存在)，以及
3. 节点只有在其父节点存在时才能出现(子节点意味着父节点)。

我的目标是使用allSat生成给定形状的所有可能的子树。例如，考虑数据类型和一个示例tree

data Tree
    = Leaf
    | Tree [ Tree ]
    deriving Show

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

转换该树应该为每个节点引入布尔值，T1, T2, L1, L2, L3和一组约束：

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

以下代码生成正确的解决方案(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

那么，如何生成给allSat的公式，给出一些具体的tree

另一种解决方案是构建这样的操作：

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

编辑:我发现了一个answer to another SO question，它是相关的。其想法是构建一个类似于上面的替代解决方案的操作，但是在树的折叠过程中。这是可能的，因为象征性是一个单一的。

Answer 1

为了弄清楚递归应该如何工作，从问题中重写替代解决方案以匹配树的形状是有指导意义的：

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 

正如我们所看到的，我们首先为节点创建一个SBool变量，然后处理它的子节点，然后返回一个连接。这意味着我们可以映射到子程序上，首先生成他们的Predicate，然后用true作为初始值折叠Predicate的列表。

下面的代码遍历树并生成公式。首先，我们简化了树类型

{-# 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" []
            ]
        ]

然后递归遍历树并为每个节点生成一个Predicate。根是特殊的:因为它没有父级，所以没有什么可暗示的。

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

最后，我使用bAnd来创建谓词的连接(如注释中所指出的)。

因为bAnd内部使用foldr，所以我们得到了一个公式

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

代替c1和c2，我们得到

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

代替c3和c4，我们得到

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

如评论中所述，SBV将在内部简化公式，在可能的情况下对其进行部分评价。因此，true将被淘汰。