Fixing various aspects, sync with virtual

SMT-LIB · Sep 24, 2024 · db3bbef · db3bbef
1 parent 5bb5dc8
commit db3bbef
Show file tree

Hide file tree

Showing 14 changed files with 2,045 additions and 157 deletions.
diff --git a/Theories/FixedSizeBitVectors.smt2 b/Theories/FixedSizeBitVectors.smt2
@@ -107,6 +107,12 @@
 
        bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ⋯ + b(0)*2^0
 
+   o bv2int, which takes a bitvector b: [0, m) → {0, 1}
+     with 0 < m, and returns an integer in the range [- 2^(m - 1), 2^(m - 1)),
+     and is defined as follows:
+
+       bv2int(b) := if b(m-1) = 0 then bv2nat(b) else bv2nat(b) - 2^m
+
    o nat2bv[m], with 0 < m, which takes a non-negative integer
      n and returns the (unique) bitvector b: [0, m) → {0, 1}
      such that
@@ -181,6 +187,20 @@
                        then [[s]]
                        else nat2bv[m](bv2nat([[s]]) rem bv2nat([[t]]))
 
+   We also define the following predicates
+
+   [[(bvnego s)]] := bv2int([[s]]) >= 2^(m - 1)
+
+   [[(bvuaddo s t)]] := (bv2nat([[s]]) + bv2nat([[t]])) >= 2^m
+
+   [[(bvsaddo s t)]] := (bv2int([[s]]) + bv2int([[t]])) >= 2^(m - 1) or
+                        (bv2int([[s]]) + bv2int([[t]])) < -2^(m - 1)
+
+   [[(bvumulo s t)]] := (bv2nat([[s]]) * bv2nat([[t]])) >= 2^m
+
+   [[(bvsmulo s t)]] := (bv2int([[s]]) * bv2int([[t]])) >= 2^(m - 1) or
+                        (bv2int([[s]]) * bv2int([[t]])) < -2^(m - 1)
+
    - Shift operations
 
    Suppose s and t are both terms of sort (_ BitVec m), m > 0.  We make use of

diff --git a/about.shtml b/about.shtml
@@ -97,8 +97,44 @@ Released for free under a Creative Commons Attribution 3.0 License
 
     </div>
    </div>
-
+
+
 <div class="clr"></div>
+<div class="fbg">
+ <div class="fbg_resize">
+  <div class="col c1">
+    <h3>Latest News</h3>
+       <small>April 2, 2024</small>
+       <p>
+        Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
+        Official yearly releases of the library will be available
+        <a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
+       </p>
+  </div>
+  <div class="col c2">
+   <h3>Previous News</h3>
+       <small>Feb 13, 2024</small>
+       <p>
+        The latest release (2023) of the SMT-LIB benchmark library is now
+        available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
+       </p>
+  </div>
+  <div class="col c3">
+   <h3>Older News</h3>
+       <small>May 12, 2021</small>
+       <p>
+        A new release of the the SMT-LIB 2.6 reference document
+        is now available. This is a minor release addressing a
+        minor error in the 2021-04-02 release.
+       </p>
+    <a href="news.shtml#2021-04-02">[More]</a>
+   </p>
+  </div>
+ </div>
+</div>
+
+
+   <div class="clr"></div>
    <div class="footer">
     <div class="footer_resize">
 

diff --git a/benchmarks.shtml b/benchmarks.shtml
@@ -35,13 +35,15 @@ Released for free under a Creative Commons Attribution 3.0 License
       </ul>
      </div>
 
+
 <div class="clr"></div>
 <div class="logo">
  <h1><a href="index.shtml">SMT-LIB <br/>
    <small>The Satisfiability Modulo Theories Library</small></a>
  </h1>
 </div>
 
+
     </div>
    </div>
    <div class="content">
@@ -94,9 +96,43 @@ Released for free under a Creative Commons Attribution 3.0 License
 
     </div>
    </div>
+
+
+<div class="clr"></div>
+<div class="fbg">
+ <div class="fbg_resize">
+  <div class="col c1">
+    <h3>Latest News</h3>
+       <small>April 2, 2024</small>
+       <p>
+        Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
+        Official yearly releases of the library will be available
+        <a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
+       </p>
+  </div>
+  <div class="col c2">
+   <h3>Previous News</h3>
+       <small>Feb 13, 2024</small>
+       <p>
+        The latest release (2023) of the SMT-LIB benchmark library is now
+        available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
+       </p>
+  </div>
+  <div class="col c3">
+   <h3>Older News</h3>
+       <small>May 12, 2021</small>
+       <p>
+        A new release of the the SMT-LIB 2.6 reference document
+        is now available. This is a minor release addressing a
+        minor error in the 2021-04-02 release.
+       </p>
+    <a href="news.shtml#2021-04-02">[More]</a>
+   </p>
+  </div>
+ </div>
+</div>
 
 
-
    <div class="clr"></div>
    <div class="footer">
     <div class="footer_resize">

diff --git a/index.shtml b/index.shtml
@@ -110,28 +110,30 @@
  <div class="fbg_resize">
   <div class="col c1">
     <h3>Latest News</h3>
-    <small>April 2, 2024</small>
-    <p>
-     Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
-     Official yearly releases of the library will be available
-     <a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
-    </p>
+       <small>April 2, 2024</small>
+       <p>
+        Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
+        Official yearly releases of the library will be available
+        <a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
+       </p>
   </div>
   <div class="col c2">
    <h3>Previous News</h3>
-   <small>Feb 13, 2024</small>
-   <p>
-    The latest release (2023) of the SMT-LIB benchmark library is now
-    available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
-   </p>
+       <small>Feb 13, 2024</small>
+       <p>
+        The latest release (2023) of the SMT-LIB benchmark library is now
+        available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
+       </p>
   </div>
   <div class="col c3">
    <h3>Older News</h3>
-   <small>May 12, 2021</small>
-   <p>
-    A new release of the the SMT-LIB 2.6 reference document
-    is now available. This is a minor release addressing a
-    minor error in the 2021-04-02 release.
+       <small>May 12, 2021</small>
+       <p>
+        A new release of the the SMT-LIB 2.6 reference document
+        is now available. This is a minor release addressing a
+        minor error in the 2021-04-02 release.
+       </p>
+    <a href="news.shtml#2021-04-02">[More]</a>
    </p>
   </div>
  </div>

diff --git a/language.shtml b/language.shtml
@@ -55,9 +55,10 @@ Released for free under a Creative Commons Attribution 3.0 License
          by Clark Barrett, Pascal Fontaine, and Cesare Tinelli.
         </dt>
         <dd>Latest official release of Version 2.6 of the SMT-LIB standard.
-         [ <a href="papers/smt-lib-reference-v2.6-r2021-05-12.pdf">pdf</a> | <a href="biblio/BarFT-RR-17.bib">bib</a> ]
+         [ <a href="papers/smt-lib-reference-v2.6-r2024-09-20.pdf">pdf</a> | <a href="biblio/BarFT-RR-17.bib">bib</a> ]
         </dd>
         <dd>Previous releases:
+	   <a href="papers/smt-lib-reference-v2.6-r2021-05-12.pdf">2021-05-12</a>;
 	   <a href="papers/smt-lib-reference-v2.6-r2021-04-02.pdf">2021-04-02</a>;
            <a href="papers/smt-lib-reference-v2.6-r2017-07-18.pdf">2017-07-18</a>
         </dd>

diff --git a/theories-FixedSizeBitVectors.shtml b/theories-FixedSizeBitVectors.shtml
@@ -160,6 +160,12 @@ Released for free under a Creative Commons Attribution 3.0 License
 
        bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ⋯ + b(0)*2^0
 
+   o bv2int, which takes a bitvector b: [0, m) → {0, 1}
+     with 0 < m, and returns an integer in the range [- 2^(m - 1), 2^(m - 1)),
+     and is defined as follows:
+
+       bv2int(b) := if b(m-1) = 0 then bv2nat(b) else bv2nat(b) - 2^m
+
    o nat2bv[m], with 0 < m, which takes a non-negative integer
      n and returns the (unique) bitvector b: [0, m) → {0, 1}
      such that
@@ -234,6 +240,20 @@ Released for free under a Creative Commons Attribution 3.0 License
                        then [[s]]
                        else nat2bv[m](bv2nat([[s]]) rem bv2nat([[t]]))
 
+   We also define the following predicates
+
+   [[(bvnego s)]] := bv2int([[s]]) >= 2^(m - 1)
+
+   [[(bvuaddo s t)]] := (bv2nat([[s]]) + bv2nat([[t]])) >= 2^m
+
+   [[(bvsaddo s t)]] := (bv2int([[s]]) + bv2int([[t]])) >= 2^(m - 1) or
+                        (bv2int([[s]]) + bv2int([[t]])) < -2^(m - 1)
+
+   [[(bvumulo s t)]] := (bv2nat([[s]]) * bv2nat([[t]])) >= 2^m
+
+   [[(bvsmulo s t)]] := (bv2int([[s]]) * bv2int([[t]])) >= 2^(m - 1) or
+                        (bv2int([[s]]) * bv2int([[t]])) < -2^(m - 1)
+
    - Shift operations
 
    Suppose s and t are both terms of sort (_ BitVec m), m > 0.  We make use of