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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
; Centaur Bitops Library
; Copyright (C) 2010-2011 Centaur Technology
;
; Contact:
; Centaur Technology Formal Verification Group
; 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
; http://www.centtech.com/
;
; License: (An MIT/X11-style license)
;
; Permission is hereby granted, free of charge, to any person obtaining a
; copy of this software and associated documentation files (the "Software"),
; to deal in the Software without restriction, including without limitation
; the rights to use, copy, modify, merge, publish, distribute, sublicense,
; and/or sell copies of the Software, and to permit persons to whom the
; Software is furnished to do so, subject to the following conditions:
;
; The above copyright notice and this permission notice shall be included in
; all copies or substantial portions of the Software.
;
; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
; DEALINGS IN THE SOFTWARE.
;
; Original author: Jared Davis <jared@centtech.com>
(in-package "BITSETS")
(include-book "bitsets")
(include-book "sbitsets")
(defxdoc std/bitsets
:parents (std)
:short "Optimized libraries for representing finite sets of natural numbers
using bit masks, featuring a strong connection to the @(see std/osets) library."
:long "<h3>Introduction</h3>
<p>The @('std/bitsets') library offers two ways to represent sets of natural
numbers.</p>
<ul>
<li>@(see bitsets)—<i>plain bitsets</i>—each set is encoded as a
single bit-mask, i.e., using a single natural number. This representation is
particularly efficient for sets of very small numbers but cannot cope well with
large elements.</li>
<li>@(see sbitsets)—<i>sparse bitsets</i>—each set is encoded as an
ordered list of offset/block pairs, each block being a bit-mask for
@(`*sbitset-block-size*`) elements. This representation is more forgiving; it
can handle larger sets, perhaps with very large elements, and still achieves
bitset-like efficiencies in many cases.</li>
</ul>
<p>Either representation provides a nice set-level abstraction that should
shield you from reasoning about the underlying bitwise arithmetic operations;
see @(see reasoning).</p>
<h3>Loading the Library</h3>
<p>To load everything (except for optimizations that require trust tags):</p>
@({
(include-book \"std/bitsets/top\" :dir :system)
})
<p>Alternately, for just the plain bitset library:</p>
@({
(include-book \"std/bitsets/bitsets\" :dir :system)
})
<p>Or for just the sparse bitsets library:</p>
@({
(include-book \"std/bitsets/sbitsets\" :dir :system)
})
<h5>Optional Optimizations</h5>
<p>You may be able to substantially speed up the @(see bitset-members)
operation for large sets, perhaps especially on CCL, by loading an optimized,
raw Lisp definition:</p>
@({
(include-book \"std/bitsets/bitsets-opt\" :dir :system)
})
<p>See @(see ttag-bitset-members) and @(see bignum-extract) for details.</p>")
(defxdoc utilities
:parents (bitsets)
:short "Utility functions.")
(defsection reasoning
:parents (std/bitsets)
:short "How to reason about bitsets."
:long "<box><p>Note: for now this discussion is only about plain @(see
bitsets). In the future, we intend this discussion to apply equally well to
@(see sbitsets).</p></box>
<p>A general goal of the bitsets library is to let you take advantage of
efficient operations like @('logand') and @('logior') without having to do any
arithmetic reasoning. Instead, ideally, you should be able to carry out all of
your reasoning on the level of sets.</p>
<h4>Basic Approach</h4>
<p>To achieve this, we try to cast everything in terms of @(see
bitset-members). If you want to reason about some bitset-producing function
@('foo'), then you should typically try to write your theorems about:</p>
@({
(bitset-members (foo ...))
})
<p>instead of directly proving something about:</p>
@({
(foo ...)
})
<p>For example, to reason about @(see bitset-union) we prove:</p>
@(thm bitset-members-of-bitset-union)
<p>In most cases, this theorem is sufficient for reasoning about the behavior
of @('bitset-union').</p>
<h4>Equivalence Proofs</h4>
<p>The @('bitset-members') approach is good most of the time, but in some cases
you may wish to show that two bitset-producing functions literally create the
same bitset. That is, instead of showing:</p>
@({
(bitset-members (foo ...)) = (bitset-members (bar ...))
})
<p>it is perhaps better to prove:</p>
@({
(foo ...) = (bar ...)
})
<p>It should be automatic to prove this stronger form (after first proving the
weaker form) by using the theorem:</p>
@(def equal-bitsets-by-membership)")
|
