Commit b9c23d59 authored by Karol Ciszek's avatar Karol Ciszek
Browse files

parts I,II only

parent 6e2a4644
module Bdds where
import Data.List
import Data.Maybe
type Index = Int
data BExp = Prim Bool | IdRef Index | Not BExp | And BExp BExp | Or BExp BExp
deriving (Eq, Ord, Show)
type Env = [(Index, Bool)]
type NodeId = Int
type BDDNode = (NodeId, (Index, NodeId, NodeId))
type BDD = (NodeId, [BDDNode])
------------------------------------------------------
-- PART I
-- Pre: The item is in the given table
lookUp :: Eq a => a -> [(a, b)] -> b
lookUp item ((key, value):dict)
| item == key = value
| otherwise = lookUp item dict
checkSat :: BDD -> Env -> Bool
checkSat (start, nodes) env
= checkSat' start nodes env
where
checkSat' id ns vars
| id == 0 = False
| id == 1 = True
| otherwise = if var then checkSat' trueId ns vars
else checkSat' falseId ns vars
where
(varIndex, falseId, trueId) = lookUp id ns
var = lookUp varIndex vars
sat :: BDD -> [[(Index, Bool)]]
sat (start, nodes)
= sat' start nodes [] []
where
sat' id ns env foundEnvs
| id == 0 = []
| id == 1 = [env]
| otherwise = sat' trueId ns ((varIndex, True):env) foundEnvs
++ sat' falseId ns ((varIndex, False):env) foundEnvs
where
(varIndex, falseId, trueId) = lookUp id ns
------------------------------------------------------
-- PART II
simplify :: BExp -> BExp
simplify (Not (Prim bool))
= Prim (not bool)
simplify (And (Prim b1) (Prim b2))
= Prim (b1 && b2)
simplify (Or (Prim b1) (Prim b2))
= Prim (b1 || b2)
simplify other
= other
restrict :: BExp -> Index -> Bool -> BExp
restrict expr i val
= simplify (restrict' expr)
where
restr e = restrict e i val
restrict' expr@(IdRef index)
| index == i = Prim val
| otherwise = expr
restrict' (Not expr)
= Not (restr expr)
restrict' (And l r)
= And (restr l) (restr r)
restrict' (Or l r)
= Or (restr l) (restr r)
restrict' any
= any
-- Alternative approach. Tbh the one with the helper is much neater.
-- restrict :: BExp -> Index -> Bool -> BExp
-- restrict expr@(IdRef index) i val
-- | index == i = Prim val
-- | otherwise = expr
-- restrict (Not expr) i val
-- = simplify (Not (restrict expr i val))
-- restrict (And left right) i val
-- = simplify (And (restrict left i val) (restrict right i val))
-- restrict (Or left right) i val
-- = simplify (Or (restrict left i val) (restrict right i val))
-- restrict bool _ _
-- = bool
------------------------------------------------------
-- PART III
-- Pre: Each variable index in the BExp appears exactly once
-- in the Index list; there are no other elements
-- The question suggests the following definition (in terms of buildBDD')
-- but you are free to implement the function differently if you wish.
buildBDD :: BExp -> [Index] -> BDD
buildBDD e xs
= buildBDD' e 2 xs
-- Potential helper function for buildBDD which you are free
-- to define/modify/ignore/delete/embed as you see fit.
buildBDD' :: BExp -> NodeId -> [Index] -> BDD
buildBDD' (Prim b) id []
= ((if b then 1 else 0), [])
buildBDD' e id (x:xs)
= (id, node:(leftNodes ++ rightNodes))
where
restrict' = restrict e x
(leftId, leftNodes) = buildBDD' (restrict' False) (id * 2) xs
(rightId, rightNodes) = buildBDD' (restrict' True) (id * 2 + 1) xs
node = (id, (x, leftId, rightId))
------------------------------------------------------
-- PART IV
-- Done only half of Part IV
-- Pre: Each variable index in the BExp appears exactly once
-- in the Index list; there are no other elements
buildROBDD :: BExp -> [Index] -> BDD
buildROBDD e xs
= buildROBDD' e 2 xs
-- first optimisation from spec
-- wrong?
eqSubTrees :: BDDNode -> Bool
eqSubTrees (_, (_, l, r))
= l == r
buildROBDD' :: BExp -> NodeId -> [Index] -> BDD
buildROBDD' (Prim b) _ []
= ((if b then 1 else 0), [])
buildROBDD' e id (x:xs)
| eqSubTrees node = (leftId, nodes)
| otherwise = (id, node:nodes)
where
restrict' = restrict e x
(leftId, leftNodes) = buildROBDD' (restrict' False) (id * 2) xs
(rightId, rightNodes) = buildROBDD' (restrict' True) (id * 2 + 1) xs
node = (id, (x, leftId, rightId))
nodes = leftNodes ++ rightNodes
------------------------------------------------------
-- Examples for testing...
b1, b2, b3, b4, b5, b6, b7, b8 :: BExp
b1 = Prim False
b2 = Not (And (IdRef 1) (Or (Prim False) (IdRef 2)))
b3 = And (IdRef 1) (Prim True)
b4 = And (IdRef 7) (Or (IdRef 2) (Not (IdRef 3)))
b5 = Not (And (IdRef 7) (Or (IdRef 2) (Not (IdRef 3))))
b6 = Or (And (IdRef 1) (IdRef 2)) (And (IdRef 3) (IdRef 4))
b7 = Or (Not (IdRef 3)) (Or (IdRef 2) (Not (IdRef 9)))
b8 = Or (IdRef 1) (Not (IdRef 1))
bdd1, bdd2, bdd3, bdd4, bdd5, bdd6, bdd7, bdd8 :: BDD
bdd1 = (0,[])
bdd2 = (2,[(4,(2,1,1)),(5,(2,1,0)),(2,(1,4,5))])
bdd3 = (5,[(5,(1,0,1))])
bdd4 = (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))])
bdd5 = (3,[(4,(3,8,9)),(3,(2,4,5)),(8,(7,1,0)),(9,(7,1,1)),
(5,(3,10,11)),(10,(7,1,0)),(11,(7,1,0))])
bdd6 = (2,[(2,(1,4,5)),(4,(2,8,9)),(8,(3,16,17)),(16,(4,0,0)),
(17,(4,0,1)),(9,(3,18,19)),(18,(4,0,0)),(19,(4,0,1)),
(5,(2,10,11)),(10,(3,20,21)),(20,(4,0,0)),(21,(4,0,1)),
(11,(3,22,23)),(22,(4,1,1)),(23,(4,1,1))])
bdd7 = (6,[(6,(2,4,5)),(4,(3,8,9)),(8,(9,1,1)),(9,(9,1,0)),
(5,(3,10,11)),(10,(9,1,1)),(11,(9,1,1))])
bdd8 = (2,[(2,(1,1,1))])
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment