Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Simols, Daniel
Binary Decision Diagrams
Commits
0cbdeb65
Commit
0cbdeb65
authored
Jan 08, 2021
by
daniel
Browse files
part I done
parents
Changes
1
Hide whitespace changes
Inline
Side-by-side
BDD.hs
0 → 100644
View file @
0cbdeb65
import
Data.List
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
x
=
snd
.
head
.
filter
(
\
(
u
,
_
)
->
x
==
u
)
checkSat
::
BDD
->
Env
->
Bool
checkSat
(
x
,
xs
)
l
|
lookUp
i
l
=
if
r
==
1
||
r
==
0
then
intToBool
r
else
checkSat
(
r
,
xs
)
l
|
otherwise
=
if
q
==
1
||
q
==
0
then
intToBool
q
else
checkSat
(
q
,
xs
)
l
where
(
i
,
q
,
r
)
=
lookUp
x
xs
intToBool
0
=
False
intToBool
_
=
True
sat
::
BDD
->
[[(
Index
,
Bool
)]]
sat
bdd
@
(
rootId
,
nodes
)
=
filter
(
checkSat
bdd
)
allEnvs
where
indexes
=
reverse
.
nub
.
map
(
\
(
_
,
(
i
,
_
,
_
))
->
i
)
$
nodes
boolPerms
0
=
[]
boolPerms
1
=
[[
False
],[
True
]]
boolPerms
n
=
foldr
(
\
x
acc
->
(
True
:
x
)
:
((
False
:
x
)
:
acc
))
[]
(
boolPerms
(
n
-
1
))
allEnvs
=
map
(
zip
indexes
)
(
boolPerms
(
length
indexes
))
{-
sat' :: BDD -> [[(Index, Bool)]]
sat' bdd@(rootId, nodes)
| q == 1 = [[]]
| q == 0 = []
| r == 1 = [[]]
| r == 0 = []
| otherwise = sat' (q, nodes) ++ sat' (r, nodes)
where
(i,q,r) = lookUp rootId nodes
-}
------------------------------------------------------
-- PART II
simplify
::
BExp
->
BExp
simplify
=
undefined
restrict
::
BExp
->
Index
->
Bool
->
BExp
restrict
=
undefined
------------------------------------------------------
-- 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
-- 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
------------------------------------------------------
-- 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
=
undefined
------------------------------------------------------
-- 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
))])
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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