Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Lun Ai
Binary_Decision_Diagrams
Commits
d87f4f8c
Commit
d87f4f8c
authored
Jan 02, 2016
by
Lun Ai
Browse files
Part III no instance for show
parent
de9ca28b
Changes
2
Hide whitespace changes
Inline
Side-by-side
template.hs
View file @
d87f4f8c
...
...
@@ -24,7 +24,7 @@ lookUp k ks
checkSat
::
BDD
->
Env
->
Bool
checkSat
(
_
,
[]
)
_
=
f
alse
=
F
alse
checkSat
(
root
,
nodes
)
env
=
checkSat'
nodes
env
(
lookUp
root
nodes
)
where
...
...
@@ -36,42 +36,103 @@ checkSat (root, nodes) env
|
lookUpEnv
=
checkSat'
nodeList
env
(
lookUp
r
nodeList
)
|
otherwise
=
checkSat'
nodeList
env
(
lookU
P
l
nodeList
)
=
checkSat'
nodeList
env
(
lookU
p
l
nodeList
)
where
lookUpEnv
=
lookUp
i
env
sat
::
BDD
->
[[(
Index
,
Bool
)]]
sat
=
undefined
sat
(
_
,
[]
)
=
[]
sat
(
root
,
nodes
)
=
(
sat'
[(
root'
,
False
)]
(
lookUp
root
nodes
))
++
(
sat'
[(
root'
,
True
)]
(
lookUp
root
nodes
))
where
(
root'
,
_
,
_
)
=
lookUp
root
nodes
sat'
env
(
i
,
l
,
r
)
|
(
fOrT
&&
r
==
0
)
||
(
not
(
fOrT
)
&&
l
==
0
)
=
[]
|
(
fOrT
&&
r
==
1
)
||
(
not
(
fOrT
)
&&
l
==
1
)
=
[
env
]
|
fOrT
=
(
sat'
(
env
++
[(
i'
,
False
)])
(
lookUp
r
nodes
))
++
(
sat'
(
env
++
[(
i'
,
True
)])
(
lookUp
r
nodes
))
|
otherwise
-- missing one condition !!!
=
(
sat'
(
env
++
[(
i'
,
False
)])
(
lookUp
l
nodes
))
++
(
sat'
(
env
++
[(
i'
,
True
)])
(
lookUp
l
nodes
))
where
fOrT
=
lookUp
i
env
(
i'
,
_
,
_
)
=
lookUp
r
nodes
------------------------------------------------------
-- PART II
simplify
::
BExp
->
BExp
simplify
=
undefined
simplify
(
Not
(
Prim
a
))
=
Prim
(
not
(
a
))
simplify
(
Not
i
)
=
Not
i
simplify
(
Or
(
Prim
a
)
(
Prim
b
))
=
Prim
(
a
||
b
)
simplify
(
Or
a
b
)
=
Or
a
b
simplify
(
And
(
Prim
a
)
(
Prim
b
))
=
Prim
(
a
&&
b
)
simplify
(
And
a
b
)
=
And
a
b
restrict
::
BExp
->
Index
->
Bool
->
BExp
restrict
=
undefined
restrict
(
Prim
a
)
_
_
=
Prim
a
restrict
(
IdRef
i
)
index
bool
|
i
==
index
=
Prim
bool
|
otherwise
=
IdRef
i
restrict
(
Not
a
)
index
bool
=
simplify
(
Not
(
restrict
a
index
bool
))
restrict
(
Or
a
b
)
index
bool
=
simplify
(
Or
(
restrict
a
index
bool
)
(
restrict
b
index
bool
))
restrict
(
And
a
b
)
index
bool
=
simplify
(
And
(
restrict
a
index
bool
)
(
restrict
b
index
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
=
undefined
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'
=
undefined
buildBDD'
(
Prim
e
)
firstID
[]
|
e
=
(
1
,
[]
)
|
otherwise
=
(
0
,
[]
)
buildBDD'
e
firstID
(
i
:
is
)
=
(
firstID
,
(
buildBDD''
e
firstID
(
i
:
is
)))
where
buildBDD''
::
BExp
->
NodeId
->
[
Index
]
->
[
BDDNode
]
buildBDD''
exp
id
[
lastID
]
=
[(
id
,
(
lastID
,
primToInt
(
restrict
exp
lastID
False
),
primToInt
(
restrict
exp
lastID
True
)))]
buildBDD''
exp
id
(
x
:
xs
)
=
(
buildBDD''
boolValueLeft
nextIndexLeft
xs
)
++
(
buildBDD''
boolValueRight
nextIndexRight
xs
)
++
[(
id
,
(
x
,
nextIndexLeft
,
nextIndexRight
))]
where
boolValueLeft
=
restrict
exp
x
False
boolValueRight
=
restrict
exp
x
True
nextIndexLeft
=
2
*
id
nextIndexRight
=
2
*
id
+
1
primToInt
::
BExp
->
Int
primToInt
(
Prim
bool
)
|
bool
=
1
|
otherwise
=
0
instance
Show
([
Index
]
->
BDD
)
where
showList
=
[
()
]
------------------------------------------------------
-- PART IV
...
...
template.hs~
View file @
d87f4f8c
...
...
@@ -24,7 +24,7 @@ lookUp k ks
checkSat :: BDD -> Env -> Bool
checkSat (_, []) _
=
f
alse
=
F
alse
checkSat (root, nodes) env
= checkSat' nodes env (lookUp root nodes)
where
...
...
@@ -36,42 +36,103 @@ checkSat (root, nodes) env
| lookUpEnv
= checkSat' nodeList env (lookUp r nodeList)
| otherwise
= checkSat' nodeList env (lookU
P
l nodeList)
= checkSat' nodeList env (lookU
p
l nodeList)
where
lookUpEnv = lookUp i env
sat :: BDD -> [[(Index, Bool)]]
sat
= undefined
sat (_, [])
= []
sat (root, nodes)
= (sat' [(root', False)] (lookUp root nodes))
++ (sat' [(root', True)] (lookUp root nodes))
where
(root', _, _) = lookUp root nodes
sat' env (i, l, r)
| (fOrT && r == 0) || (not(fOrT) && l == 0)
= []
| (fOrT && r == 1) || (not(fOrT) && l == 1)
= [env]
| fOrT
= (sat' (env ++ [(i', False)]) (lookUp r nodes))
++ (sat' (env ++ [(i', True)]) (lookUp r nodes))
| otherwise -- missing one condition !!!
= (sat' (env ++ [(i', False)]) (lookUp l nodes))
++ (sat' (env ++ [(i', True)]) (lookUp l nodes))
where
fOrT = lookUp i env
(i', _, _) = lookUp r nodes
------------------------------------------------------
-- PART II
simplify :: BExp -> BExp
simplify
= undefined
simplify (Not (Prim a))
= Prim (not(a))
simplify (Not i)
= Not i
simplify (Or (Prim a) (Prim b))
= Prim (a || b)
simplify (Or a b)
= Or a b
simplify (And (Prim a) (Prim b))
= Prim (a && b)
simplify (And a b)
= And a b
restrict :: BExp -> Index -> Bool -> BExp
restrict
= undefined
restrict (Prim a) _ _
= Prim a
restrict (IdRef i) index bool
| i == index = Prim bool
| otherwise = IdRef i
restrict (Not a) index bool
= simplify (Not (restrict a index bool))
restrict (Or a b) index bool
= simplify (Or (restrict a index bool) (restrict b index bool))
restrict (And a b) index bool
= simplify (And (restrict a index bool) (restrict b index 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
=
undefined
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'
= undefined
buildBDD' (Prim e) firstID []
| e = (1, [])
| otherwise = (0, [])
buildBDD' e firstID (i:is)
= (firstID, (buildBDD'' e firstID (i:is)))
where
buildBDD'' :: BExp -> NodeId -> [Index] -> [BDDNode]
buildBDD'' exp id [lastID]
= [(id, (lastID, primToInt(restrict exp lastID False),
primToInt(restrict exp lastID True)))]
buildBDD'' exp id (x:xs)
= (buildBDD'' boolValueLeft nextIndexLeft xs)
++ (buildBDD'' boolValueRight nextIndexRight xs)
++ [(id, (x, nextIndexLeft, nextIndexRight))]
where
boolValueLeft = restrict exp x False
boolValueRight = restrict exp x True
nextIndexLeft = 2 * id
nextIndexRight = 2 * id + 1
primToInt :: BExp -> Int
primToInt (Prim bool)
| bool = 1
| otherwise = 0
instance Show([Index] -> BDD) where
showList = [()]
------------------------------------------------------
-- PART IV
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment