1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
<html>
<head><title>BDD.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>BDD</h1>ordered binary decision diagrams with rewriting
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
Ordered binary decision diagrams (OBDDs, often simply called BDDs)
are a technique, originally published by Randy Bryant, for the
efficient simplification of Boolean expressions. In ACL2 we combine
this technique with rewriting to handle arbitrary ACL2 terms that
can represent not only Boolean values, but non-Boolean values as
well. In particular, we provide a setting for deciding equality of
bit vectors (lists of Boolean values).
<p>
<ul>
<li><h3><a href="BDD-ALGORITHM.html">BDD-ALGORITHM</a> -- summary of the BDD algorithm in ACL2
</h3>
</li>
<li><h3><a href="BDD-INTRODUCTION.html">BDD-INTRODUCTION</a> -- examples illustrating the use of BDDs in ACL2
</h3>
</li>
<li><h3><a href="IF_star_.html">IF*</a> -- for conditional rewriting with BDDs
</h3>
</li>
<li><h3><a href="SHOW-BDD.html">SHOW-BDD</a> -- inspect failed BDD proof attempts
</h3>
</li>
</ul>
An introduction to BDDs for the automated reasoning community may
be found in ``Introduction to the OBDD Algorithm for the ATP
Community'' by J Moore, <i>Journal of Automated Reasoning</i> (1994),
pp. 33-45. (This paper also appears as Technical Report #84 from
Computational Logic, Inc.)<p>
Further information about BDDs in ACL2 can be found in the
subtopics of this <a href="DOCUMENTATION.html">documentation</a> section. In particular,
see <a href="BDD-INTRODUCTION.html">bdd-introduction</a> for a good starting place that provides a
number of examples.<p>
See <a href="HINTS.html">hints</a> for a description of <code>:bdd</code> hints. For quick
reference, here is an example; but only the <code>:vars</code> part of the
hint is required, as explained in the documentation for <a href="HINTS.html">hints</a>.
The values shown are the defaults.
<pre>
(:vars nil :bdd-constructors (cons) :prove t :literal :all)
</pre>
We suggest that you next visit the documentation topic
<a href="BDD-INTRODUCTION.html">BDD-INTRODUCTION</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
