0

假设以下定义：

type Index = Int

data BExp = Prim Bool | IdRef Index | Not BExp | And BExp BExp | Or BExp BExp
           deriving (Eq, Ord, Show)

type NodeId = Int

type BDDNode =  (NodeId, (Index, NodeId, NodeId))

type BDD = (NodeId, [BDDNode])

我想从一个布尔表达式构建一个 ROBDD。到目前为止，我已经能够构建一个不满足无冗余或共享属性的 BDD。

buildBDD :: BExp -> [Index] -> BDD
buildBDD e idxs
 = buildBDD' e 2 idxs

buildBDD' :: BExp -> NodeId -> [Index] -> BDD
buildBDD' (Prim bool) _ []
  | bool       = (1, [])
  | otherwise  = (0, [])
buildBDD' e nodeId (idx : idxs)
 = (nodeId, [newNode] ++ tl ++ tr)
 where
   newNode = (nodeId, (idx, il, ir))
   (il, tl) = buildBDD' (restrict e idx False) (2 * nodeId) idxs
   (ir, tr) = buildBDD' (restrict e idx True) (2 * nodeId + 1) idxs

命名和风格可能不是最好的，因为这仍在进行中。

节点在内部由唯一的 id 表示。它从 2 开始。左子树的根节点将标记为2n，右子树的根节点将标记为2n + 1。

该函数将布尔表达式和表达式中出现的变量的索引列表作为输入。

例如，对于以下表达式：

And (IdRef 7) (Or (IdRef 2) (Not (IdRef 3)))

电话buildBDD bexp [2,3,7]将返回

(2,[(2,(2,4,5)),(4,(3,8,9)),(8,(7,0,1)),(9,(7,0,0)),(5,(3,10,11)),(10,(7,0,1)),
(11,(7,0,1))])

我已经进行了以下更改以说明无冗余属性（这尚未经过彻底测试，但似乎可以正常工作）

checkEqual (_, l, r)
  | l == r    = True
  | otherwise = False

getElemFromTuple (_, _, e)
  = e

getTuple = snd . head

buildROBDD' e nodeId (idx : idxs)
     = (nodeId, [newNode] ++ left ++ right)
 where
   newNode   = (nodeId, (idx, lId, rId))
   (il, tl)  = buildROBDD' (restrict e idx False) (2 * nodeId) idxs
   (ir, tr)  = buildROBDD' (restrict e idx True) (2 * nodeId + 1) idxs
   lId       = if (not . null) tl && (checkEqual . getTuple) tl then (getElemFromTuple . getTuple) tl else il
   rId       = if (not . null) tr && (checkEqual . getTuple) tr then (getElemFromTuple . getTuple) tr else ir
   left      = if (not . null) tl && (checkEqual . getTuple) tl then [] else tl
   right     = if (not . null) tr && (checkEqual . getTuple) tr then [] else tr

（请原谅上面的笨拙表达）

但是，我不知道如何处理共享属性，尤其是因为共享节点可能位于图中的任何位置，并且我没有存储当前树。如果需要，可以更改唯一节点 ID 的公式。

注意：这是一个练习，因此所涉及的类型和风格可能不是最佳的。我也不应该更改它们（尽管我可以自由更改功能）。

4

0 回答 0