haskell - 使用 Haskell 给定一些数据生成 SBV 公式的简单方法是什么？

Question

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

1. 每个节点都有一个 bool 变量(表示它是否存在)，
2. 根(如果空闲)(可能存在也可能不存在)，并且
3. 只有当其父节点存在时，节点才能存在(子节点意味着父节点)。

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

data Tree
    = Leaf
    | Tree [ Tree ]
    deriving Show

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

翻译该树应该为每个节点引入 bool 值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的公式？

另一种解决方案是构造如下操作:

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 ，这是相关的。这个想法是构建一个类似于上面替代解决方案的操作，但在树的折叠过程中。这是可能的，因为 Symbolic 是一个 monad。

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 列表。

以下代码遍历树并生成一个公式。首先，我们简化Tree类型

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

然后我们递归地遍历树并为每个节点生成一个谓词。根很特殊:因为它没有父项，所以没有什么可暗示的。

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将被消除。