Skip to content

Commit db3bbef

Browse files
fontainepfontainep
committed
Fixing various aspects, sync with virtual
1 parent 5bb5dc8 commit db3bbef

14 files changed

+2045
-157
lines changed

‎Theories/FixedSizeBitVectors.smt2

+20
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,12 @@
107107
108108
bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ⋯ + b(0)*2^0
109109
110+
o bv2int, which takes a bitvector b: [0, m) → {0, 1}
111+
with 0 < m, and returns an integer in the range [- 2^(m - 1), 2^(m - 1)),
112+
and is defined as follows:
113+
114+
bv2int(b) := if b(m-1) = 0 then bv2nat(b) else bv2nat(b) - 2^m
115+
110116
o nat2bv[m], with 0 < m, which takes a non-negative integer
111117
n and returns the (unique) bitvector b: [0, m) → {0, 1}
112118
such that
@@ -181,6 +187,20 @@
181187
then [[s]]
182188
else nat2bv[m](bv2nat([[s]]) rem bv2nat([[t]]))
183189
190+
We also define the following predicates
191+
192+
[[(bvnego s)]] := bv2int([[s]]) >= 2^(m - 1)
193+
194+
[[(bvuaddo s t)]] := (bv2nat([[s]]) + bv2nat([[t]])) >= 2^m
195+
196+
[[(bvsaddo s t)]] := (bv2int([[s]]) + bv2int([[t]])) >= 2^(m - 1) or
197+
(bv2int([[s]]) + bv2int([[t]])) < -2^(m - 1)
198+
199+
[[(bvumulo s t)]] := (bv2nat([[s]]) * bv2nat([[t]])) >= 2^m
200+
201+
[[(bvsmulo s t)]] := (bv2int([[s]]) * bv2int([[t]])) >= 2^(m - 1) or
202+
(bv2int([[s]]) * bv2int([[t]])) < -2^(m - 1)
203+
184204
- Shift operations
185205
186206
Suppose s and t are both terms of sort (_ BitVec m), m > 0. We make use of

‎about.shtml

+37-1
Original file line numberDiff line numberDiff line change
@@ -97,8 +97,44 @@ Released for free under a Creative Commons Attribution 3.0 License
9797

9898
</div>
9999
</div>
100-
100+
101+
101102
<div class="clr"></div>
103+
<div class="fbg">
104+
<div class="fbg_resize">
105+
<div class="col c1">
106+
<h3>Latest News</h3>
107+
<small>April 2, 2024</small>
108+
<p>
109+
Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
110+
Official yearly releases of the library will be available
111+
<a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
112+
</p>
113+
</div>
114+
<div class="col c2">
115+
<h3>Previous News</h3>
116+
<small>Feb 13, 2024</small>
117+
<p>
118+
The latest release (2023) of the SMT-LIB benchmark library is now
119+
available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
120+
</p>
121+
</div>
122+
<div class="col c3">
123+
<h3>Older News</h3>
124+
<small>May 12, 2021</small>
125+
<p>
126+
A new release of the the SMT-LIB 2.6 reference document
127+
is now available. This is a minor release addressing a
128+
minor error in the 2021-04-02 release.
129+
</p>
130+
<a href="news.shtml#2021-04-02">[More]</a>
131+
</p>
132+
</div>
133+
</div>
134+
</div>
135+
136+
137+
<div class="clr"></div>
102138
<div class="footer">
103139
<div class="footer_resize">
104140

‎benchmarks.shtml

+37-1
Original file line numberDiff line numberDiff line change
@@ -35,13 +35,15 @@ Released for free under a Creative Commons Attribution 3.0 License
3535
</ul>
3636
</div>
3737

38+
3839
<div class="clr"></div>
3940
<div class="logo">
4041
<h1><a href="index.shtml">SMT-LIB <br/>
4142
<small>The Satisfiability Modulo Theories Library</small></a>
4243
</h1>
4344
</div>
4445

46+
4547
</div>
4648
</div>
4749
<div class="content">
@@ -94,9 +96,43 @@ Released for free under a Creative Commons Attribution 3.0 License
9496

9597
</div>
9698
</div>
99+
100+
101+
<div class="clr"></div>
102+
<div class="fbg">
103+
<div class="fbg_resize">
104+
<div class="col c1">
105+
<h3>Latest News</h3>
106+
<small>April 2, 2024</small>
107+
<p>
108+
Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
109+
Official yearly releases of the library will be available
110+
<a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
111+
</p>
112+
</div>
113+
<div class="col c2">
114+
<h3>Previous News</h3>
115+
<small>Feb 13, 2024</small>
116+
<p>
117+
The latest release (2023) of the SMT-LIB benchmark library is now
118+
available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
119+
</p>
120+
</div>
121+
<div class="col c3">
122+
<h3>Older News</h3>
123+
<small>May 12, 2021</small>
124+
<p>
125+
A new release of the the SMT-LIB 2.6 reference document
126+
is now available. This is a minor release addressing a
127+
minor error in the 2021-04-02 release.
128+
</p>
129+
<a href="news.shtml#2021-04-02">[More]</a>
130+
</p>
131+
</div>
132+
</div>
133+
</div>
97134

98135

99-
100136
<div class="clr"></div>
101137
<div class="footer">
102138
<div class="footer_resize">

‎index.shtml

+18-16
Original file line numberDiff line numberDiff line change
@@ -110,28 +110,30 @@
110110
<div class="fbg_resize">
111111
<div class="col c1">
112112
<h3>Latest News</h3>
113-
<small>April 2, 2024</small>
114-
<p>
115-
Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
116-
Official yearly releases of the library will be available
117-
<a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
118-
</p>
113+
<small>April 2, 2024</small>
114+
<p>
115+
Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
116+
Official yearly releases of the library will be available
117+
<a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
118+
</p>
119119
</div>
120120
<div class="col c2">
121121
<h3>Previous News</h3>
122-
<small>Feb 13, 2024</small>
123-
<p>
124-
The latest release (2023) of the SMT-LIB benchmark library is now
125-
available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
126-
</p>
122+
<small>Feb 13, 2024</small>
123+
<p>
124+
The latest release (2023) of the SMT-LIB benchmark library is now
125+
available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
126+
</p>
127127
</div>
128128
<div class="col c3">
129129
<h3>Older News</h3>
130-
<small>May 12, 2021</small>
131-
<p>
132-
A new release of the the SMT-LIB 2.6 reference document
133-
is now available. This is a minor release addressing a
134-
minor error in the 2021-04-02 release.
130+
<small>May 12, 2021</small>
131+
<p>
132+
A new release of the the SMT-LIB 2.6 reference document
133+
is now available. This is a minor release addressing a
134+
minor error in the 2021-04-02 release.
135+
</p>
136+
<a href="news.shtml#2021-04-02">[More]</a>
135137
</p>
136138
</div>
137139
</div>

‎language.shtml

+2-1
Original file line numberDiff line numberDiff line change
@@ -55,9 +55,10 @@ Released for free under a Creative Commons Attribution 3.0 License
5555
by Clark Barrett, Pascal Fontaine, and Cesare Tinelli.
5656
</dt>
5757
<dd>Latest official release of Version 2.6 of the SMT-LIB standard.
58-
[ <a href="papers/smt-lib-reference-v2.6-r2021-05-12.pdf">pdf</a> | <a href="biblio/BarFT-RR-17.bib">bib</a> ]
58+
[ <a href="papers/smt-lib-reference-v2.6-r2024-09-20.pdf">pdf</a> | <a href="biblio/BarFT-RR-17.bib">bib</a> ]
5959
</dd>
6060
<dd>Previous releases:
61+
<a href="papers/smt-lib-reference-v2.6-r2021-05-12.pdf">2021-05-12</a>;
6162
<a href="papers/smt-lib-reference-v2.6-r2021-04-02.pdf">2021-04-02</a>;
6263
<a href="papers/smt-lib-reference-v2.6-r2017-07-18.pdf">2017-07-18</a>
6364
</dd>

‎theories-FixedSizeBitVectors.shtml

+20
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,12 @@ Released for free under a Creative Commons Attribution 3.0 License
160160

161161
bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ⋯ + b(0)*2^0
162162

163+
o bv2int, which takes a bitvector b: [0, m) → {0, 1}
164+
with 0 < m, and returns an integer in the range [- 2^(m - 1), 2^(m - 1)),
165+
and is defined as follows:
166+
167+
bv2int(b) := if b(m-1) = 0 then bv2nat(b) else bv2nat(b) - 2^m
168+
163169
o nat2bv[m], with 0 < m, which takes a non-negative integer
164170
n and returns the (unique) bitvector b: [0, m) → {0, 1}
165171
such that
@@ -234,6 +240,20 @@ Released for free under a Creative Commons Attribution 3.0 License
234240
then [[s]]
235241
else nat2bv[m](bv2nat([[s]]) rem bv2nat([[t]]))
236242

243+
We also define the following predicates
244+
245+
[[(bvnego s)]] := bv2int([[s]]) >= 2^(m - 1)
246+
247+
[[(bvuaddo s t)]] := (bv2nat([[s]]) + bv2nat([[t]])) >= 2^m
248+
249+
[[(bvsaddo s t)]] := (bv2int([[s]]) + bv2int([[t]])) >= 2^(m - 1) or
250+
(bv2int([[s]]) + bv2int([[t]])) < -2^(m - 1)
251+
252+
[[(bvumulo s t)]] := (bv2nat([[s]]) * bv2nat([[t]])) >= 2^m
253+
254+
[[(bvsmulo s t)]] := (bv2int([[s]]) * bv2int([[t]])) >= 2^(m - 1) or
255+
(bv2int([[s]]) * bv2int([[t]])) < -2^(m - 1)
256+
237257
- Shift operations
238258

239259
Suppose s and t are both terms of sort (_ BitVec m), m > 0. We make use of

0 commit comments

Comments
 (0)