diff --git a/Theories/FixedSizeBitVectors.smt2 b/Theories/FixedSizeBitVectors.smt2 index 6f5a10b..f60e2fd 100644 --- 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 index 9940d0d..aea44f9 100755 --- a/about.shtml +++ b/about.shtml @@ -97,8 +97,44 @@ Released for free under a Creative Commons Attribution 3.0 License - + +
+
+
+
+

Latest News

+ April 2, 2024 +

+ 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 + Zenodo. +

+
+
+

Previous News

+ Feb 13, 2024 +

+ The latest release (2023) of the SMT-LIB benchmark library is now + available on Zenodo in the form of compressed archives. +

+
+
+

Older News

+ May 12, 2021 +

+ 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. +

+ [More] +

+
+
+
+ + +
diff --git a/benchmarks.shtml b/benchmarks.shtml index 0358d54..0ad3578 100644 --- a/benchmarks.shtml +++ b/benchmarks.shtml @@ -35,6 +35,7 @@ Released for free under a Creative Commons Attribution 3.0 License
+
+
@@ -94,9 +96,43 @@ Released for free under a Creative Commons Attribution 3.0 License
+ + +
+
+
+
+

Latest News

+ April 2, 2024 +

+ 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 + Zenodo. +

+
+
+

Previous News

+ Feb 13, 2024 +

+ The latest release (2023) of the SMT-LIB benchmark library is now + available on Zenodo in the form of compressed archives. +

+
+
+

Older News

+ May 12, 2021 +

+ 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. +

+ [More] +

+
+
+
-
diff --git a/index.shtml b/index.shtml index 5e16730..faaf9e3 100755 --- a/index.shtml +++ b/index.shtml @@ -110,28 +110,30 @@

Latest News

- April 2, 2024 -

- 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 - Zenodo. -

+ April 2, 2024 +

+ 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 + Zenodo. +

Previous News

- Feb 13, 2024 -

- The latest release (2023) of the SMT-LIB benchmark library is now - available on Zenodo in the form of compressed archives. -

+ Feb 13, 2024 +

+ The latest release (2023) of the SMT-LIB benchmark library is now + available on Zenodo in the form of compressed archives. +

Older News

- May 12, 2021 -

- 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. + May 12, 2021 +

+ 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. +

+ [More]

diff --git a/language.shtml b/language.shtml index 57411a8..fac4ac2 100644 --- 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.
Latest official release of Version 2.6 of the SMT-LIB standard. - [ pdf | bib ] + [ pdf | bib ]
Previous releases: + 2021-05-12; 2021-04-02; 2017-07-18
diff --git a/theories-FixedSizeBitVectors.shtml b/theories-FixedSizeBitVectors.shtml index 7baf456..22284c2 100644 --- 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 diff --git a/version3-proposal.shtml b/version3-proposal.shtml index 22aa88e..5b39d2b 100644 --- a/version3-proposal.shtml +++ b/version3-proposal.shtml @@ -1434,31 +1434,1893 @@ of the old ones in any meaningful way. 
-  
+; Core SMT-LIB theory
+
+(define-module Core ( 
+  (set-info :smt-lib-version 3.0)
+  (set-info :smt-lib-release "2020-XX-XX")
+  (set-info :written-by "Pascal Fontaine and Cesare Tinelli")
+  (set-info :date "2020-04-24")
+  (set-info :last-updated "2020-04-24")
+  (set-info :update-history
+   "TODO.
+   "
+  )
+
+  ;---------------
+  ; Builtin types
+  ;--------------- 
+  ; Booleans
+  (declare-type Bool () :builtin
+   "The (binary) set {true, false}")
+
+  ; Could be defined as a datatype in alternative
+
+  ;-------------------
+  ; Builtin constants
+  ;------------------- 
+   ; Equality  
+  (declare-const = (-> (! Type :var A :implicit) 
+                       A A Bool)
+   :chainable 
+   :builtin 
+   "= denotes the identity function, which returns true iff 
+    its two arguments are identical.")
+
+  ;-----------------------
+  ; Axiomatized constants
+  ;----------------------- 
+  ; true, false
+  (define-const true Bool)
+  (declare-const false Bool)
+  ; ite
+  (declare-const ite 
+    (-> (! Type :var A :implicit) 
+           Bool A A A))
+  ; ite is if-then-else
+  (assert (forall ((A Type)) (= (ite true) (lambda ((x A) (y A)) x))))
+  (assert (forall ((A Type)) (= (ite false) (lambda ((x A) (y A)) y))))
+  ; true and false are distinct
+  (assert (= (= true false) false))
+
+  ;-------------------
+  ; Defined constants
+  ;------------------- 
+  ; not
+  (define-const not (-> Bool Bool) 
+    (lambda ((b Bool)) (ite b false true)))
+  ; distinct
+  (define-const distinct (-> (! Type :var A :implicit) A A Bool) 
+    (lambda ((A Type :implicit) (x A) (y A)) (not (= x y))) :pairwise)
+  ; or
+  (define-const or (-> Bool Bool Bool) 
+    (lambda ((b1 Bool) (b2 Bool)) (ite b1 true b2)) :left-assoc)
+  ; and
+  (define-const and (-> Bool Bool Bool) 
+    (lambda ((b1 Bool) (b2 Bool)) (ite b1 b2 false)) :left-assoc)
+  ; implies
+  (define-const => (-> Bool Bool Bool) 
+    (lambda ((b1 Bool) (b2 Bool)) (ite b1 b2 true)) :right-assoc)
+  ; xor
+  (define-const xor (-> Bool Bool Bool) 
+    (lambda ((b1 Bool) (b2 Bool)) (distinct b1 b2)) :left-assoc)
+  ; forall
+  (define-const forall 
+    (-> (! Type :var A :implicit)
+        (-> A Bool) Bool)
+    (lambda ((A Type :implicit) (P (-> A Bool)))
+      (= P (lambda ((x A)) true))))
+  ; Note: This forall quantifies only over individuals, not over types.
+  ;       A forall quantifier over types is provided as a primitive binder.
+
+  (set-info :notation 
+   "(forall ((x τ)) φ) abbreviates 
+    (forall (lambda ((x₁ τ₁)) φ))
+  
+    (forall ((x₁ τ₁) ⋅⋅⋅ (xᵢ τᵢ)) φ) abbreviates 
+    (forall ((x₁ τ₁)) ⋅⋅⋅ (forall ((xᵢ τᵢ)) φ))
+
+    (forall ((τ₁ Type) ⋅⋅⋅ (τⱼ Type) (x₁ τ₁) ⋅⋅⋅ (xᵢ τᵢ)) φ) abbreviates 
+    (forall ((τ₁ Type) ⋅⋅⋅ (τⱼ Type))
+      (forall ((x₁ τ₁)) ⋅⋅⋅ (forall ((xᵢ τᵢ)) φ)))
+   ")
+  ; exists
+  (define-const exists 
+    (-> (! Type :var A :implicit) 
+        (-> A Bool) Bool) 
+    (lambda ((A Type :implicit) (P (-> A Bool)))
+      (distinct P (lambda ((x A)) false))))
+  ;
+  (set-info :notation 
+   "(exists ((x τ)) φ) abbreviates 
+    (exists (lambda ((x₁ τ₁)) φ))
+
+    (exists ((x₁ τ₁) ⋅⋅⋅ (xᵢ τᵢ)) φ) abbreviates 
+    (exists ((x₁ τ₁)) ⋅⋅⋅ (exists ((xᵢ τᵢ)) φ))
+   ")
+
+  ; Hilbert's choice (ε)
+  (declare-const choose 
+    (-> (! Type :var A :implicit)
+        (-> A Bool) A))
+  ;
+  ; choose is axiomatically defined  
+  (assert (forall ((A Type) (P (-> A Bool))) 
+    (= (exists P) (P (choose P)))))
+  ;
+  (set-info :notation 
+   "(choose (x τ) φ)  abbreviates  (choose (lambda ((x τ)) φ))
+   ")
+
+  ;-------------
+  ; Bool values
+  ;-------------
+  ; The set of values of type Bool is {true, false}.
+  (define-syntax (⟨bool_value⟩)
+    ; production rules
+    ((⟨bool_value⟩ (true false))))
+
+  (define-values Bool ⟨bool_value⟩)
+
+  ; compose
+  (define-fun compose
+   ((A Type :implicit)
+    (B Type :implicit)
+    (C Type :implicit)
+    (f (-> B C))
+    (g (-> A B))
+   )
+   (-> A C)
+   (lambda ((a A)) (f (g a)))
+   :note 
+    "compose is not declared left-associative on purpose otherwise
+     there would be ambiguity between (compose f g h) where f g and h 
+     are functions to be composed and (compose f g a) where a is 
+     the input of g."
+ )
+
+; ; pipe
+;   (define-const pipe
+;     (-> (! Type :var A :implicit)
+;         (! Type :var B :implicit)
+;         A (-> A B) B)
+;     (lambda ((A Type) (B Type) (a A) (f (-> A B)))
+;       (f a))
+;     :left-assoc  ; this is actually problematic without type inference:
+;     ; (pipe a f g) = (pipe (pipe a f) g)      ((pipe a f) g)
+;     ; (pipe a f g) = (pipe (pipe a f) g) 
+;     )
+
+
+; identity
+  (define-const iden
+    (-> (! Type :var A :implicit) A A)
+    (lambda ((A Type) (a A)) a))
+
+  ;apply
+  (define-const apply
+    (-> (! Type :var A :implicit)
+        (! Type :var B :implicit)
+        (-> A B) A B)
+    (lambda ((A Type) (B Type) (f (-> A B))) f)
+    :left-assoc ; (apply g a b) = (apply (apply g a) b) 
+  )
+
+ 
+
+  ;-----------------------
+  ; Abstract value syntax
+  ;-----------------------
+  (define-syntax 
+    ; non-terminals
+    ( ⟨abstract_value⟩ ⟨bool_value⟩ )
+    ; production rules
+    ( (⟨bool_value⟩ (true false))
+      (⟨abstract_value⟩ ((! ⟨symbol⟩ :restrict "starts with @")))))
+
+  (define-values () Bool ⟨bool_value⟩)
+
+
+  ;-------------------
+  ; Import Attributes
+  ;-------------------
+
+     ; FOL
+  (set-info :FOL
+   "The import attribute :FOL restricts Core
+      to the first-order applicative fragment:
+      - no lambdas
+      - no partial applications: 
+        the first argument of an application can only be a constant
+      - all arguments of an application have a type of order 0
+      - can only declare or define constants whose type has order <= 1
+      - can use forall, exists, and choose only in their
+        abbreviated form.
+   ")
+
+  (set-info :no-new-types 
+   "The import attribute :no-new-types disallows the use  
+    of the declare-type command.")
+
+  (set-info :no-new-functions 
+   "The import attribute :no-new-functions disallows the declaration 
+    of constants of arrow type.")
+))
+
(raw file)
- 

-
+ 
+(define-module Ints (
+  (set-info :smt-lib-version 3.0)
+  (set-info :smt-lib-release "2020-XX-XX")
+  (set-info :written-by "Pascal Fontaine and Cesare Tinelli")
+  (set-info :date "2020-05-01")
+  (set-info :last-updated "2020-05-01")
+  (set-info :update-history
+   "TODO.
+   "
+  )
+  (set-info :notes 
+   "Integer arithmetic")
+ 
+  (import (Core))
+  (open Core)
+
+  ;---------------
+  ; Builtin types
+  ;--------------- 
+  ; Int
+  (declare-type Int () :builtin 
+  "Int denotes the set of all integer numbers.")
+
+  ;-------------------
+  ; Builtin constants
+  ;------------------- 
+  ; 0, 1, 2, ...
+  (declare-const ⟨numeral⟩ Int :builtin 
+   "Each numeral denotes the corresponding integer as usual.") 
+  ; successor
+  (declare-const +1 (-> Int Int) :builtin
+   "+1 denotes the integer successor function")
+  ; predecessor
+  (declare-const -1 (-> Int Int) :builtin
+   "-1 denotes the integer predecessor function")
+  ; <
+  (declare-const < (-> Int Int Bool) :builtin
+   "< denotes the standard strict total ordering over the integers."
+   :chainable)
+  ;
+
+  ;-----------------------------------
+  ; Axiomatized and defined constants
+  ;----------------------------------- 
+
+  ; <=
+  (define-const <= (-> Int Int Bool) (lambda ((x Int) (y Int)) 
+    (or (= x y) (< x y)))
+   :chainable)
+  ; >
+  (define-const > (-> Int Int Bool) (lambda ((x Int) (y Int))
+    (< y x))
+   :chainable)
+  ; >=
+  (define-const >= (-> Int Int Bool) (lambda ((x Int) (y Int))
+    (or (= x y) (> x y)))
+   :chainable)
+  ; unary -
+  (define-const-rec - (-> Int Int) (lambda ((x Int))
+    (ite (= x 0) 0
+      (ite (< x 0) (+1 (- (+1 x))) 
+        (-1 (- (-1 x)))))))
+  ; +
+  (define-const-rec + (-> Int Int Int) (lambda ((x Int) (y Int)) 
+    (ite (= y 0) x 
+      (ite (< y 0) (-1 (+ x (+1 y))) 
+        (+1 (+ x (-1 y))))))
+   :left-assoc)
+  ; binary -
+  (define-const - (-> Int Int Int) (lambda ((x Int) (y Int)) 
+    (+ x (- y)))
+   :left-assoc
+   :no-partial ; this constant cannot be applied partially 
+   )
+  ; * 
+  (define-const-rec * (-> Int Int Int) (lambda ((x Int) (y Int)) 
+    (ite (= y 0) 0
+      (ite (< y 0) (- (* x (- y))) 
+        (+ x (* x (-1 y))))))
+   :left-assoc)
+  ; abs
+  (define-const abs (-> Int Int) (lambda ((x Int))
+    (ite (>= x 0) x (- x))))
+  ; div 
+  (declare-const div (-> Int (! Int :var n :restrict (distinct n 0)) Int) 
+   :left-assoc)
+  ; mod
+  (declare-const mod (-> Int Int Int))
+  ; div/mod axiom
+  (assert (forall ((m Int) (n Int)) (=> (distinct n 0)
+    (let ((q (div m n)) (r (mod m n)))
+      (and (= m (+ (* n q) r))
+           (<= 0 r (-1 (abs n))))))))
+      
+  ; divisible by constant n
+  (define-const divisible (-> Int (! Int :var n :restrict (> n 0)) Bool)
+    (lambda ((m Int) (n Int)) (= (mod m n) 0)))
+
+
+  (set-info :notes
+   "The axiomatization of div and mod is based on [1].
+   
+    Regardless of the sign of m, 
+    - when n is positive, (div m n) is the floor of the rational number m/n;
+    - when n is negative, (div m n) is the ceiling of m/n.
+
+    This contrasts with alternative but less robust definitions of div and mod
+    where (div m n) is 
+    - always the integer part of m/n (rounding towards 0), or 
+    - always the floor of x/y (rounding towards -infinity).
+
+    [1] Boute, Raymond T. (April 1992). 
+        The Euclidean definition of the functions div and mod. 
+        ACM Transactions on Programming Languages and Systems (TOPLAS) 
+        ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
+   ")
+
+  ; summation
+  (define-const-rec sum (-> Int Int (-> Int Int) Int)
+    (lambda ((a Int) (b Int) (f (-> Int Int)))
+      (ite (> a b) 
+        0 
+        (+ (f a) (sum (+1 a) b f)))))
+
+  ;-------- 
+  ; Values
+  ;--------
+  ; The set of values for type Int consists of 
+  ;  - all numerals,
+  ;  - all terms of the form (- n) where n is a numeral other than 0.
+  (define-syntax 
+    ; non-terminals
+    (⟨int_value⟩ ⟨pos_numeral⟩) 
+    ; production rules
+    ((⟨int_value⟩ (⟨numeral⟩
+                   (- ⟨pos_numeral⟩)))
+     (⟨pos_numeral⟩ ((! ⟨numeral⟩ :syntax-restrict "other than 0")))))
+
+  (define-values () Int ⟨int_value⟩)
+
+
+  ;-------------------------------
+  ; External and Bridging symbols
+  ;-------------------------------
+  ; Real
+  (declare-type Real () :extern Reals::Real)
+
+  (declare-const to_int (-> Real Int) :builtin 
+   "to_int denotes the function that maps each real number r 
+    to its integer part, that is, to the largest integer n 
+    that satisfies (<= (to_real n) r).")
+))
+
+
(raw file)
- 

-
+ 
+(define-module Reals (
+  (set-info :smt-lib-version 3.0)
+  (set-info :smt-lib-release "2020-XX-XX")
+  (set-info :written-by "Pascal Fontaine and Cesare Tinelli")
+  (set-info :date "2020-07-01")
+  (set-info :last-updated "2020-07-01")
+  (set-info :update-history
+   "TODO.
+   "
+  )
+  (set-info :notes  "Real arithmetic")
+
+  (import (Core))
+  (open Core)
+
+  ;---------------
+  ; Builtin types
+  ;---------------
+  ; Real
+  (declare-type Real () :builtin
+   "Real denotes the set of all real numbers."
+  )
+
+  ;-------------------------------
+  ; External and Bridging symbols
+  ;-------------------------------
+  ; Int
+  (declare-type Int () :extern Ints::Int)
+
+  (declare-const to_real (-> Int Real) :builtin 
+   "to_real as the standard injection of the integers into the reals.")
+
+  ;-------------------
+  ; Builtin constants
+  ;------------------- 
+  ; Decimals
+  (declare-const ⟨decimal⟩ Real :builtin
+   "Each ⟨decimal⟩ denotes the corresponding real number as usual.")
+
+  ; rational constants defined further down
+
+   ; Unary -
+  (declare-const - (-> Real Real) :builtin "Negation.")
+  ;  
+  ; +
+  (declare-const + (-> Real Real Real) :left-assoc :builtin "Addition.")
+
+  ; *
+  (declare-const * (-> Real Real Real) :left-assoc :builtin "Multiplication.")
+
+  ; <=
+  (declare-const <= (-> Real Real Bool) :chainable :builtin 
+   "Usual non-strict total ordering over the reals.")
+
+   ; is_int
+  (declare-const is_int (-> Real Bool) :builtin
+   "is_int maps whole real numbers to true and all the other reals to false.")
+
+  ;-----------------------
+  ; Axiomatized constants
+  ;----------------------- 
+
+  ; subtraction -
+  (define-const - (-> Real Real Real) (lambda ((x Real) (y Real))
+    (+ x (- y))
+   :left-assoc))
+
+  ; division /
+  (declare-const / (-> Real Real Real) :left-assoc :restrict (distinct y 0.0))
+  (assert (forall ((x Real) (y Real)) (=> (distinct y 0.0)
+    (= x (* y (/ x y))))))
+    
+  ; <
+  (define-const < (-> Real Real Bool) (lambda ((x Real) (y Real))
+    (and (<= x y) (distinct x y)))
+   :chainable)
+
+  ; >
+  (define-const > (-> Real Real Bool) (lambda ((x Real) (y Real))
+    (< y x))
+   :chainable)
+
+  ; >=
+  (define-const >= (-> Real Real Bool) (lambda ((x Real) (y Real))
+    (<= y x))
+   :chainable)
+
+  ; Summation 
+  ; we use a step different from 1 and provide it as additional input
+  (define-const-rec sum (-> Real Real (-> Real Real) Real)
+    (lambda ((a Real) (b Real) (f (-> Real Real)))
+      (ite (> a b) 
+        0.0 
+        (+ (f a) (sum (+ a 1.0) b f)))))
+
+  ; rational constants
+  (define-const / 
+    (-> (! Int :value) 
+        (! Int :var d :value :restrict (> (to_real d) 0.0))
+        Real) 
+    (lambda ((n Int) (d Int)) 
+      (/ (to_real n) (to_real d))))
+
+
+  ;-------------
+  ; Real values
+  ;-------------
+
+  ; The set of values for the sort Real consists of 
+  ;  - an abstract value for each irrational algebraic number
+  ;  - all decimals of the form n.0
+  ;  - all terms of the form (- n.0) where n is a ⟨numeral⟩ other than 0
+  ;  - all terms of the form (/ m n) or (- (/ m n)) where 
+  ;    - m is a ⟨numeral⟩ other than 0,
+  ;    - n is a ⟨numeral⟩ other than 0 and 1,
+  ;    - as integers, m and n have no common factors besides 1.
+  (define-syntax 
+    ; non-terminals
+    (⟨real_value⟩ ⟨p⟩ ⟨f⟩ ⟨m⟩ ⟨n⟩) 
+    ; production rules
+    ((⟨real_value⟩ (⟨abstract⟩ ; for irrational algebraic numbers
+                    0.0
+                    ⟨p⟩
+                    (- ⟨p⟩)
+                    ⟨f⟩
+                    (- ⟨f⟩))
+     (⟨f⟩ ((! (/ ⟨m⟩ ⟨n⟩) :syntax-restrict 
+                          "as integers, ⟨m⟩ and ⟨n⟩ have no common factors besides 1")))
+     (⟨p⟩ ((! ⟨decimal⟩ :syntax-restrict "it has the form n.0 except for 0.0")))
+     (⟨m⟩ ((! ⟨numeral⟩ :syntax-restrict "it is not 0")))
+     (⟨n⟩ ((! ⟨numeral⟩ :syntax-restrict "it is neither 0 nor 1"))))))
+
+  (define-values () Real ⟨real_value⟩)
+
+  (set-info :notes
+   "In Real values decimals are used only for whole numbers, e.g., 42.0. 
+   For all other rational numbers the fractional notation is necessary, e.g., (/ 1 2).
+   This way there is unique value for each rational."
+  )
+
+  (set-info :notes
+   "The restriction of Reals over the signature having just the symbols 
+    (0.0 Real)
+    (1.0 Real)
+    (- Real Real)
+    (+ Real Real Real) 
+    (* Real Real Real)
+    (<= Real Real Bool)
+    (<  Real Real Bool)
+    coincides with the theory of real closed fields, axiomatized by
+    the formulas below: 
+
+    - associativity of +
+      (forall ((x Real) (y Real) (z Real)) (= (+ (+ x y) z) (+ x (+ y z))))
+
+    - commutativity of +
+      (forall ((x Real) (y Real)) (= (* x y) (* y x)))
+
+    - 0.0 is the right (and by commutativity, left) unit of +
+      (forall ((x Real)) (= (+ x 0.0) x))
+
+    - right (and left) inverse wrt +
+      (forall ((x Real)) (= (+ x (- x)) 0.0))
+
+    - associativity of *
+      (forall ((x Real) (y Real) (z Real)) (= (* (* x y) z) (* x (* y z))))
+
+    - commutativity of *
+      (forall ((x Real) (y Real)) (= (* x y) (* y x)))
+
+    - 1.0 is the right (and by commutativity, left) unit of *
+      (forall ((x Real)) (= (* x 1.0) x))
+
+    - existence of right (and left) inverse wrt *
+      (forall ((x Real)) (or (= x 0) (exists (y Real) (= (* x y) 1.0))))
+
+    - left distributivity of * over +
+      (forall ((x Real) (y Real) (z Real)) (= (* x (+ y z)) (+ (* x y) (* x z))))
+
+    - right distributivity of * over +
+     (forall ((x Real) (y Real) (z Real)) (= (* (+ x y) z) (+ (* x z) (* y z))))
+
+    - non-triviality
+      (distinct 0.0 1.0)
+
+    - all positive elements have a square root
+      (forall ((x Real)) (exists ((y Real))
+        (or (= x (* y y)) (= (- x) (* y y)))))
+
+    - axiom schemas for all n > 0
+      (forall ((x_1 Real) ... (x_n Real))
+        (distinct (- 1) (+ (* x_1 x_1) (+ ... (* x_n x_n))))) 
+
+    - axiom schemas for all odd n > 0 where (^ y n) abbreviates
+      the n-fold product of y with itself
+      (forall ((x_1 Real) ... (x_n Real)) (exists ((y Real))
+        (= 0 (+ (^ y n) (+ (* x_1 (^ y n-1)) (+  ... (+ (* x_{n-1} y) x_n)))))))
+
+    - reflexivity of <=
+      (forall ((x Real)) (<= x x))
+
+    - antisymmetry of <=
+      (forall ((x Real) (y Real)) (=> (and (<= x y) (<= y x)) (= x y)))
+
+    - transitivity of <=
+      (forall ((x Real) (y Real) (z Real)) (=> (<= x y z)) (<= x z))
+
+    - totality of <=
+      (forall ((x Real) (y Real)) (or (<= x y) (<= y x)))
+    
+    - monotonicity of <= wrt +
+      (forall ((x Real) (y Real) (z Real)) (=> (<= x y) (<= (+ x z) (+ y z))))
+
+    - monotonicity of <= wrt *
+      (forall (x Real) (y Real) (z Real) 
+        (=> (and (<= x y) (<= 0 z)) (<= (* z x) (* z y))))
+
+    - definition of <
+      (forall ((x Real) (y Real)) 
+        (= (< x y) (and (<= x y) (distinct x y))))
+
+    References:
+    1) W. Hodges. Model theory. Cambridge University Press, 1993.
+    2) PlanetMath, http://planetmath.org/encyclopedia/RealClosedFields.html
+  ")
+
+))
+
+
(raw file)
- 

+  
+;; **Make sure that all operators in QF_BV.smt2 have been added**
+
+(define-module FixedSizeBitVectors (
+  (set-info :smt-lib-version 3.0)
+  (set-info :smt-lib-release "2020-XX-XX")
+  (set-info :written-by "Pascal Fontaine and Cesare Tinelli")
+  (set-info :date "2020-05-01")
+  (set-info :last-updated "2020-07-01")
+  (set-info :update-history
+   "TODO.
+   "
+    )
+  (set-info :notes
+   "This theory declaration defines a core theory for fixed-size bitvectors 
+    where the operations of concatenation and extraction of bitvectors as well 
+    as the usual logical and arithmetic operations are overloaded.
+   ")
+ 
+   (import (Core))
+   (open Core)
+
+  ;------------------
+  ; External symbols
+  ;------------------
+
+  (declare-type Int () :extern Ints::Int)
+
+  (declare-const ⟨numeral⟩ Int :extern Ints::⟨numeral⟩)
+
+  (declare-const 0 Int :extern Ints::0)
+  (declare-const 1 Int :extern Ints::1)
+  (declare-const +1 (-> Int Int) :extern Ints::+1)
+  (declare-const + (-> Int Int Int) :extern Ints::+)
+  (declare-const - (-> Int Int Int) :extern Ints::-)
+  (declare-const * (-> Int Int Int) :extern Ints::*)
+  (declare-const < (-> Int Int Bool) :extern Ints::<)
+  (declare-const > (-> Int Int Bool) :extern Ints::>)
+
+  ;---------------
+  ; Builtin types
+  ;---------------
+
+  ; definition as a dependent type 
+  (declare-type BitVec ((! Int :var m :restrict (<= 0 m)))
+   :builtin 
+   "(BitVec m) denotes the set of all bitvectors of size m >= 0.
+   More precisely, it denotes the set of finite functions
+   whose domain is the initial segment [0, m) of the naturals, starting at
+   0 (included) and ending at m (excluded), and whose co-domain is {0, 1}.")
+
+  (set-info :notes
+   "(BitVec 0) contains just one element, the empty vector, corresponding to
+    the only function in the function space {} -> {0,1}, the empty function.
+   "
+  )
+				   
+  (set-info :notes
+   "To define some of the semantics below, we use the following mathematical
+    functions:
+
+    o _ div _,  which takes an integer x ≥ 0 and an integer y > 0 and returns
+     the integer part of x divided by y (i.e., truncated integer division).
+
+    o _ rem _, which takes an integer x ≥ 0 and y > 0 and returns the
+      remainder when x is divided by y.  Note that we always have the following
+      equivalence for y > 0: (x div y) * y + (x rem y) = x.
+
+    o bv2nat, which takes a bitvector b: [0, m) → {0, 1}
+      with 0 < m, and returns an integer in the range [0, 2ᵐ),
+      and is defined as follows:
+
+        bv2nat(b) := b(m-1) * 2ᵐ⁻¹ + b(m-2) * 2ᵐ⁻² + ⋯ + b(0) * 2⁰
+
+      Note that bv2nat(b) = 0 for the empty bitvector b: [0, 0) → {0, 1}.
+
+    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
+
+        b(m-1) * 2ᵐ⁻¹ + ⋯ + b(0) * 2⁰ = n rem 2ᵐ
+
+      Note that nat2bv[0](n) is the empty vector b: [0, 0) → {0, 1}
+      for every natural n.
+
+    The semantic interpretation of terms of type (BitVec m) is provided
+    by the function ⟦_⟧ used in the definition below for the builtin operators.
+   ")
+
+  (set-info :notes
+   "In builtin definitions below, |exp| is used denote the integer  
+    resulting from the evaluation of the arithmetic expression exp.
+   ")
+
+  ;--------------------
+  ; Bridging functions
+  ;--------------------
+
+  ; to_int
+  (declare-const to_int
+    (-> (! Int :var m :implicit :restrict (>= m 0)) 
+        (BitVec m) Int)
+   :built-in 
+    "Standard (BitVec m) to Int conversion, mapping each vector 
+     to a number in the interval [0,2^m)"
+  )
+
+  ; to_bv from Int
+  (declare-const to_bv 
+    (-> (! Int :var m :restrict (<= 0 m))  ; explicit argument
+        Int (BitVec m))
+   :built-in 
+   "Int to (BitVec m) conversion mapping each integer n 
+    to the 2's complement representation of (n modulo m)." ; to be double-checked
+  )
+
+  ; to_bv from Bool
+  (define-const to_bv (-> Bool (BitVec 1))
+    (lambda ((b Bool)) (ite b #b1 #b0)))
+
+  ;-------------------
+  ; Constant literals
+  ;-------------------
+
+  ; Empty bitvector
+  (declare-const bvempty (BitVec 0))
+
+  ; Bitvector literals in binary form (such as #b10110)
+  (declare-const ⟨binary⟩
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit 
+         :restrict "m is the number of binary digits in the constant") 
+        (BitVec m))
+   :builtin
+   "The constant symbols #b0 and #b1 of sort (BitVec 1) are defined as follows
+
+    ⟦#b0⟧ := λx:[0, 1). 0
+    ⟦#b1⟧ := λx:[0, 1). 1
+
+    More generally, given a string #b followed by a sequence of 0's and 1's,
+    if n is the numeral represented in base 2 by the sequence of 0's and 1's
+    and m is the length of the sequence, then the term represents
+    nat2bv[m](n).
+   ")
+
+  ; Bitvector literals in hexadecimal form (such as #xB93AD)
+  (declare-const ⟨hexadecimal⟩
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit
+         :restrict "m is 4 times the number of hexadecimal digits in the constant") 
+        (BitVec m))
+   :builtin
+   "Let h be the constant. Then h denotes nat2bv[m](n) where n is the numeral 
+    represented in hexadecimal (base 16) by h.
+    For example, #xFF is equivalent to #b11111111.
+   ")
+
+				     
+  ;--------------------
+  ; Sequence operators
+  ;--------------------
+
+  ; concat
+  (declare-const concat 
+    (-> (! Int :var i :syntax ⟨numeral⟩ :implicit :restrict (<= 0 i)) 
+        (! Int :var j :syntax ⟨numeral⟩ :implicit :restrict (<= 0 j)) 
+        (! Int :var k :syntax ⟨numeral⟩ :implicit :restrict (= k (+ i j))) 
+        (BitVec i) (BitVec j)
+        (BitVec k))
+   :builtin
+   "- For all terms s and t of type (BitVec 0) and (BitVec j), respectively,
+      ⟦(concat s t)⟧ := ⟦t⟧
+    - For all terms s and t of type (BitVec i) and (BitVec j) with i > 0,
+      ⟦(concat s t)⟧ := λx:[0, i+j). (if (x < j) then ⟦t⟧(x) else ⟦s⟧(x - j))
+ ")
+
+  ; extract
+  (declare-const extract
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (< 0 m)) 
+        (! Int :var i :syntax ⟨numeral⟩ :restrict (< i m)) 
+        (! Int :var j :syntax ⟨numeral⟩ :restrict (<= 0 j i))
+        (! Int :var k :syntax ⟨numeral⟩ :implicit :restrict (= k (+1 (- i j))))
+        (BitVec m) (BitVec k))
+   :builtin
+   "For all terms t of type (BitVec m),
+    ⟦(extract i j t)⟧ := λx:[0, m). ⟦t⟧(j + x)
+   ")
+
+  (set-info :notes
+   "extract extracts from a _non-empty_ bitvector a sub-bitvector 
+    from position i down to position j.
+    The spec could be refined to have the function return the empty vector 
+    when i is smaller than j.
+   ")
+
+  ; repeat
+  ; (repeat i x) means concatenate i copies of x
+  (define-fun-rec repeat 
+    ((i Int :syntax ⟨numeral⟩ :restrict (<= 0 i)) 
+     (m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+     (n Int :syntax ⟨numeral⟩ :implicit :restrict (= n (* m i))) 
+     (x (BitVec m))
+    ) 
+    (BitVec n)
+    (ite (= i 0) bvempty (concat x (repeat (- i 1) x)))
+  )
+
+  ;-------------------- 
+  ; Bit-wise operators
+  ;-------------------- 
+
+  ; bvnot
+  (declare-const bvnot
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m))
+   :builtin
+   "- For all terms s of type (BitVec 0),
+      ⟦(bvnot s)⟧ := ⟦bvempty⟧
+    - For all terms s of type (BitVec m) with m > 0,
+      ⟦(bvnot s)⟧ := λx:[0, m). if ⟦s⟧(x) = 0 then 1 else 0
+   ")
+
+  ; bvand
+  (declare-const bvand
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m))
+   :left-assoc
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvand s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m) with m > 0,
+      ⟦(bvand s t)⟧ := λx:[0, m). if ⟦s⟧(x) = 0 then 0 else ⟦t⟧(x)
+   ")
+
+  ; bvor
+  (declare-const bvor
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+   :left-assoc
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvor s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m) with m > 0,
+      ⟦(bvor s t)⟧ := λx:[0, m). if ⟦s⟧(x) = 1 then 1 else ⟦t⟧(x)
+   ")
+
+  ; bvnand
+  (define-const bvnand
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+         (BitVec m) (BitVec m) (BitVec m)) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m))
+             (s (BitVec m)) (t (BitVec m))) 
+      (bvnot (bvand s t)))
+  )
+
+  ; bvnor
+  (define-const bvnor
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+             (s (BitVec m)) (t (BitVec m))) 
+      (bvnot (bvor s t)))
+  )
+
+  ; bvxor
+  (define-const bvxor
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+             (s (BitVec m)) (t (BitVec m))) 
+      (bvor (bvand s (bvnot t)) (bvand (bvnot s) t)))
+   :left-assoc
+  )
+
+  ; bvxnor
+  (define-const bvxnor
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+             (s (BitVec m)) (t (BitVec m))) 
+      (bvor (bvand s t) (bvand (bvnot s) (bvnot t))))
+  )
+
+  ;bvcomp
+  (declare-const bvcomp
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec 1))
+    (lambda ((m Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m))
+             (s (BitVec m)) (t (BitVec m)))
+      (to_bv (= s t)))
+  )
+;   :builtin
+;   "For all terms s, t of type (BitVec m),
+;    (bvcomp s t) is equivalent to 
+;     - (bvxnor s t) 
+;       if m = 1
+;     - (bvand (bvxnor ((extract |m-1| |m-1|) s) ((extract |m-1| |m-1|) t))
+;         (bvcomp ((extract |m-2| 0) s) ((extract |m-2| 0) t))) 
+;       otherwise
+;   ")
+
+  ;----------------------
+  ; Arithmetic operators
+  ;----------------------
+
+  ; bvneg
+  (declare-const bvneg
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m))
+   :builtin
+   "- For all terms s of type (BitVec 0),
+      ⟦(bvneg s)⟧ := ⟦bvempty⟧
+    - For all terms s of type (BitVec m),
+      ⟦(bvneg s)⟧ := nat2bv[m](2ᵐ - bv2nat(⟦s⟧))
+   ")
+
+  ; bvadd
+  (declare-const bvadd
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+   :left-assoc
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvadd s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m),
+      ⟦(bvadd s t)⟧ := nat2bv[m](bv2nat(⟦s⟧) + bv2nat(⟦t⟧))
+   ")
+
+  ; bvmul
+  (declare-const bvmul
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+   :left-assoc
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvmul s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m),
+      ⟦(bvmul s t)⟧ := nat2bv[m](bv2nat(⟦s⟧) * bv2nat(⟦t⟧))
+   ")
+
+  ; bvudiv
+  (declare-const bvudiv
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvudiv s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m),
+      ⟦(bvudiv s t)⟧ := if bv2nat(⟦t⟧) = 0
+                        then λx:[0, m). 1
+                        else nat2bv[m](bv2nat(⟦s⟧) div bv2nat(⟦t⟧))
+   ")
+
+  ; bvurem
+  (declare-const bvurem
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvurem s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m),
+      ⟦(bvurem s t)⟧ := if bv2nat(⟦t⟧) = 0 
+                       then ⟦s⟧
+                       else nat2bv[m](bv2nat(⟦s⟧) rem bv2nat(⟦t⟧))
+   ")
+
+  ; bvsub
+  (define-const bvsub
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m))
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+             (s (BitVec m)) (t (BitVec m))) 
+      (bvadd s (bvneg t)))
+   )
+
+  ;----------------------------- 
+  ; Signed arithmetic operators
+  ;----------------------------- 
+
+  ; bvsdiv
+  (declare-const bvsdiv
+      (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+          (BitVec m) (BitVec m) (BitVec m)) 
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvsdiv s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m),
+      (bvsdiv s t) is equivalent to 
+        (let ((?msb_s ((extract |m-1| |m-1|) s))
+              (?msb_t ((extract |m-1| |m-1|) t)))
+         (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
+              (bvudiv s t)
+         (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
+              (bvneg (bvudiv (bvneg s) t))
+         (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
+              (bvneg (bvudiv s (bvneg t)))
+              (bvudiv (bvneg s) (bvneg t))))))
+   ")
+
+  ; bvsrem
+  (declare-const bvsrem
+      (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+          (BitVec m) (BitVec m) (BitVec m)) 
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvsrem s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m),
+      (bvsrem s t) is equivalent to  
+       (let ((?msb_s ((extract |m-1| |m-1|) s))
+             (?msb_t ((extract |m-1| |m-1|) t)))
+         (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
+              (bvurem s t)
+         (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
+              (bvneg (bvurem (bvneg s) t))
+         (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
+              (bvurem s (bvneg t)))
+              (bvneg (bvurem (bvneg s) (bvneg t))))))
+   ")
+
+;;;; REVISE DEFINITION [what is (bv0 m) ?]  TODO
+  ; bvsmod
+  (declare-const bvsmod
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) (BitVec m)) 
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvsmod s t)⟧ := ⟦bvempty⟧
+    - For all terms s, t of type (BitVec m),
+      (bvsmod s t) is equivalent to
+       (let ((?msb_s ((extract |m-1| |m-1|) s))
+             (?msb_t ((extract |m-1| |m-1|) t)))
+         (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
+               (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
+            (let ((u (bvurem abs_s abs_t)))
+             (ite (= u (bv0 m))
+                  u
+             (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
+                  u
+             (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
+                  (bvadd (bvneg u) t)
+             (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
+                   (bvadd u t)
+                  (bvneg u))))))))
+   ")
+
+  ;-------------------------------
+  ; Unsigned Comparison operators
+  ;-------------------------------
+
+  ; bvult
+  (declare-const bvult
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) Bool) 
+   :chainable
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvult s t)⟧ := false
+    - For all terms s, t of type (BitVec m),
+      ⟦(bvult s t)⟧ := true iff bv2nat(⟦s⟧) < bv2nat(⟦t⟧)
+   ")
+ 
+  ; bvule
+  (define-const bvule
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) Bool) 
+    (lambda ((m Int :implicit :restrict (<= 0 m))
+	     (s (BitVec m)) (t (BitVec m))) 
+      (or (bvult s t) (= s t)))
+   )
+
+  ; bvugt
+  (define-const bvugt
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) Bool) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m))
+             (s (BitVec m)) (t (BitVec m))) 
+      (bvult t s))
+   )
+
+  ; bvuge
+  (define-const bvuge
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) Bool) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m))
+             (s (BitVec m)) (t (BitVec m))) 
+      (bvule t s))
+   )
+
+  ;-----------------------------
+  ; Signed Comparison operators
+  ;-----------------------------
+
+  ; bvslt
+  (declare-const bvslt
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) Bool)
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvslt s t)⟧ := false
+    - For all terms s, t of type (BitVec m),
+      (bvslt s t) is equivalent to  
+       (or (and (= ((extract |m-1| |m-1|) s) #b1)
+                (= ((extract |m-1| |m-1|) t) #b0))
+           (and (= ((extract |m-1| |m-1|) s) ((extract |m-1| |m-1|) t))
+                (bvult s t)))
+   ")
+
+  ; bvsle
+  (declare-const bvsle
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) Bool)
+   :builtin
+   "- For all terms s, t of type (BitVec 0),
+      ⟦(bvsle s t)⟧ := false
+    - For all terms s, t of type (BitVec m),
+      (bvsle s t) is equivalent to 
+       (or (and (= ((extract |m-1| |m-1|) s) #b1)
+                (= ((extract |m-1| |m-1|) t) #b0))
+           (and (= ((extract |m-1| |m-1|) s) ((extract |m-1| |m-1|) t))
+                (bvule s t)))
+   ")
+
+  ; bvsgt
+  (define-const bvsgt
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) Bool) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m))
+	     (s (BitVec m)) (t (BitVec m))) 
+      (bvslt t s))
+   )
+  
+  ; bvsge
+  (define-const bvsge
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m) Bool) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m))
+             (s (BitVec m)) (t (BitVec m))) 
+      (bvsle t s))
+   )   
+
+  ;----------------- 
+  ; Shift operators
+  ;----------------- 
+
+  ; bvshl
+  (declare-const bvshl
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (! Int :var n :syntax ⟨numeral⟩ :implicit :restrict (<= 0 n)) 
+        (BitVec m) (BitVec n) (BitVec m))
+   :builtin
+   "For all terms s and t of type (BitVec m) and (BitVec n), respectively,
+    ⟦(bvshl s t)⟧ := nat2bv[m](bv2nat(⟦s⟧) * 2ᵏ)  where k = bv2nat(⟦t⟧)
+   ")
+ 
+  ; bvlshr  
+  (declare-const bvlshr
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (! Int :var n :syntax ⟨numeral⟩ :implicit :restrict (<= 0 n)) 
+    (BitVec m) (BitVec n) (BitVec m))
+   :builtin
+   "For all terms s and t of type (BitVec m) and (BitVec n), respectively,
+    ⟦(bvlshr s t)⟧ := nat2bv[m](bv2nat(⟦s⟧) div 2ᵏ) where k = bv2nat(⟦t⟧)
+   ")
+
+  ;------------------------- 
+  ; Miscellaneous operators
+  ;------------------------- 
+
+  ; zero_extend
+  (declare-const zero_extend
+    (-> (! Int :var i :syntax ⟨numeral⟩ :restrict (<= 0 i)) 
+        (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (! Int :var n :syntax ⟨numeral⟩ :implicit :restrict (= n (+ m i))) 
+        (BitVec m) (BitVec n))
+   :builtin
+   "For all terms t of type (BitVec m),
+    (zero_extend i t) means extend t with zeroes to the (unsigned) bitvector
+    of size m+i that has the same (unsigned) integer value.
+   ")
+
+  ; sign_extend
+  (declare-const sign_extend
+    (-> (! Int :var i :syntax ⟨numeral⟩ :restrict (<= 0 i)) 
+        (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (! Int :var n :syntax ⟨numeral⟩ :implicit :restrict (= n (+ m i))) 
+        (BitVec m) (BitVec n))
+   :builtin
+   "For all terms t of type (BitVec m),
+    (sign_extend i t) means extend to the (signed) bitvector of size m+i
+    that has the same (signed) integer value as t.
+   ")
+
+  ; rotate_left
+  (declare-const rotate_left
+    (-> (! Int :var i :syntax ⟨numeral⟩ :restrict (<= 0 i)) 
+        (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m))
+   :builtin
+   "For all terms t of type (BitVec m),
+    (rotate_left i t) means rotate the bits of t to the left i times.
+   ")
+ 
+  ; rotate_right
+  (declare-const rotate_right
+    (-> (! Int :var i :syntax ⟨numeral⟩ :restrict (<= 0 i)) 
+        (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m))
+   :builtin
+   "For all terms t of type (BitVec m),
+    (rotate_right i t) means rotate the bits of t to the right i times.
+   ")
+ 
+  ; pop_count
+  (declare-const pop_count
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec m))
+  :builtin
+  "For all terms t of type (BitVec m),
+   (pop_count t) is the bitvector whose unsigned integer value is equal 
+   to the number of 1s in t. 
+  ")
+   
+  ; reduce_and
+  (declare-const reduce_and
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec 1))
+  :builtin
+  "For all terms t of type (BitVec m),
+   (reduce_and t) returns the logical conjunction of all the bits in t.
+   Note that the result is #b1 if m is 0. 
+  ")
+
+  ; reduce_or
+  (declare-const reduce_or
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec 1))
+  :builtin
+  "For all terms t of type (BitVec m),
+   (reduce_or t) returns the logical disjunction of all the bits in t.
+   Note that the result is #b0 if m is 0. 
+  ")
+
+  ; reduce_xor
+  (declare-const reduce_xor
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec m) (BitVec 1))
+  :builtin
+  "For all terms t of type (BitVec m),
+   (reduce_xor t) returns the logical xor of all the bits in t.
+   Note that the result is #b0 if m is 0. 
+   ")
+
+  ; bvite
+  (define-const bvite
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+        (BitVec 1) (BitVec m) (BitVec m) (BitVec m)) 
+    (lambda ((m Int :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m))
+             (x (BitVec 1)) (y (BitVec m)) (z (BitVec m))) 
+      (ite (= x #b1) y z))
+   )
+
+; TODO:   A (BV 1) version of all comparison ops
+; PF TODO fix all functions
+  (declare-const bv1ult
+    (-> (! Int :var m :syntax ⟨numeral⟩ :implicit :restrict (<= 0 m)) 
+      (BitVec m) (BitVec m) (BitVec 1))
+    (lambda ((m Int :implicit :restrict (<= 0 m))
+             (s (BitVec m)) (t (BitVec m)))
+      (to_bv (bvult s t)))
+   :notes
+   "This function cannot be chainable like its boolean counterpart
+    since it does not return a boolean
+   ")
+
+  ;------------------
+  ; Bitvector values
+  ;------------------
+
+  (define-syntax 
+    ; non-terminals
+    (⟨bitvector_value⟩) 
+    ; production rules
+    ((⟨bitvector_value⟩ (bvempty ⟨binary⟩))))
+
+  (define-values ((n Int :restrict (<= 0 n)))
+    (BitVec n) 
+    (! ⟨bitvector_value⟩ 
+     :syntax-restrict 
+     "bvemtpy when n = 0 and otherwise only binaries #bX with n digits"))
+				     
+))
+
  

  (raw file)
- 

+  
+(define-module Strings (
+  (set-info :smt-lib-version 3.0)
+  (set-info :smt-lib-release "2020-XX-XX")
+  (set-info :written-by "Pascal Fontaine and Cesare Tinelli")
+  (set-info :date "2020-07-01")
+  (set-info :last-updated "2020-07-01")
+  (set-info :update-history
+   "TODO.
+   "
+    )
+  (set-info :notes
+    "This is a theory of character strings and regular expressions over an
+     alphabet consisting of Unicode characters. It is not meant to be used in
+     isolation but in combination with Ints, the theory of integer numbers.")
+
+  (import (Core))
+  (open Core)
+
+  (set-info :notes
+    "To define some of the semantics below, we use the following mathematical
+     notation:
+
+     - The semantic interpretation of terms of type String and Lan is provided
+       by the function ⟦_⟧ used in the definition below for the builtin
+       operators.
+
+     - UC denotes the set of all integers from 0x000000 to 0xFFFFFF,
+       representing a superset of the set of all code points for Unicode
+       characters at the time of this writing. 
+
+     - UC* is the set of all words, in the sense of universal algebra, 
+       with juxtaposition denoting the concatenation operator here. 
+       Note: Character positions in a word are numbered starting at 0.
+
+     - If w is a word in UC*, |w| denotes the number of characters, i.e., 
+       elements, in w.")
+
+
+  ;------------------
+  ; External symbols
+  ;------------------
+
+  ; Int
+  (declare-type Int () :extern Ints::Int)
+
+  ; (BitVec m)
+  (declare-type BitVec ((! Int :var m :syntax ⟨int_value⟩ :restrict (> m 0)))
+   :extern FixedSizeBitVectors::BitVec)
+
+  (declare-const ⟨hexadecimal⟩
+    (-> (! Int :var m :syntax ⟨int_value⟩ :restrict (> m 0) :implicit
+         :restrict "m is 4 times the number of hexadecimal digits in the constant") 
+        (BitVec m))
+    :extern FixedSizeBitVectors::⟨hexadecimal⟩)
+
+  ;---------------
+  ; Builtin types
+  ;---------------
+
+  (declare-type String () :builtin
+    "Strings denotes the set of unbounded strings of Unicode characters.
+     Formally, ⟦String⟧ = UC* ")
+
+  (declare-type Lan () :builtin
+    "Lan denotes the set of all languages over Unicode strings.
+     Formally, ⟦Lan⟧ is the powerset of ⟦String⟧. 
+     Each element of ⟦Lan⟧ can be seen as a language with alphabet UC. 
+     Each variable-free term of type Lan denotes a regular language in ⟦Lan⟧.")
+
+  (set-info :notes
+    "There was consensus in the community that having a character type is not
+     really necessary and in fact complicates the theory. So the only way to
+     express characters is to use strings of length 1.")
+
+  ; In string fields below (which are double-quote-delimited) we cannot write
+  ; something like "abc" to denote a string constant, we must use ""abc""
+  ; instead.
+
+  (set-info :notes
+    "Because of SMT-LIB's own escaping conventions, string literals are written 
+     in quadruple quotes, as in ""abc"", in textual fields here.")
+
+  ;-----------
+  ; Constants
+  ;-----------
+
+  ; string constants for _singleton_ strings, 
+  ; i.e., strings consisting of exactly one character 
+
+  (declare-const char
+    (-> (! Int :var m :syntax ⟨int_value⟩ :implicit
+               :restrict (or (= m 4) (= m 8) (= m 12) (= m 16) (= m 20) (= m 24)))
+        (! (BitVec m) :value)
+        String)
+    :builtin
+    "For all h, (char h) denotes a string of length 1 whose only character 
+     is the Unicode character with code point n where n is the (unsigned) 
+     integer represented by h. We identify Unicode characters
+     with their code point, but expressed as a hexadecimal.
+     For instance, 
+     - (char #x2B) denotes the string ""+"" whose only character has code
+       point 0x00002B (PLUS SIGN); 
+     - (char #x27E8) denotes the string ""⟨"" whose only character has code
+       point 0x0027E8 (MATHEMATICAL LEFT ANGLE BRACKET).")
+ 
+  (set-info :notes
+    "The argument of char can have at most 6 (hexadecimal) characters
+     Ex:  (char #xA)  (char #x4E)  (char #x123)  (char #x1BC3D)
+          (char #x01BC3D)")
+
+  (set-info :notes
+    "Because of leading zeros, the same one-character string is denoted  
+     in more than one way. 
+     Example: (char #x2B), (char #x02B), (char #x002B), (char #x0002B)
+              and (char #x00002B)")
+
+  (set-info :notes
+    "The singleton string constants represent a superset of all the Unicode
+     code points (from 0x000000 to 0x10FFFF) at the time of this writing.
+
+     References:
+     - https://www.unicode.org/main.html
+     - http://www.utf8-chartable.de/
+     - https://www.compart.com/en/unicode/")
+
+  (set-info :notes
+    "Rationale for the chosen notation for singleton string constants:
+     Because of their large range, Unicode code points are typically given in
+     hexadecimal notation. Using a hexadecimal directly to denote the
+     corresponding character, however, would create an overloading problem in
+     logics that combine this theory with that of bitvectors since hexadecimals
+     denote bitvectors there.
+     Using them as indices instead avoids this problem.")
+
+  ; String constants
+  (declare-const ⟨string⟩ String
+    :restrict
+    "All double-quote-delimited string literals consisting of printable US ASCII
+     characters, i.e., those with Unicode code point from 0x000020 to 0x00007E.
+     Arbitrary Unicode characters can be represented with _escape sequences_ 
+     which can have one of the following forms 
+      \ud₃d₂d₁d₀
+      \u{d₀}
+      \u{d₁d₀}
+      \u{d₂d₁d₀}
+      \u{d₃d₂d₁d₀}
+      \u{d₄d₃d₂d₁d₀}
+      \u{d₅d₄d₃d₂d₁d₀}
+     where each dᵢ is a hexadecimal digit.
+     This is enough to allow characters from all Unicode planes at the time of 
+     this writing.
+     The restriction to printable US ASCII characters in string constants is for
+     simplicity since that set is universally supported."
+    :builtin
+    "1. The empty string constant """" is interpreted as the empty word ε of UC*.
+
+     2. Each string constant containing a single (printable) US ASCII character
+        is interpreted as the word consisting of the corresponding Unicode
+        character code point.
+      
+        Ex: ⟦""m""⟧ = ⟦(char #x6D)⟧ = 0x00006D
+            ⟦"" ""⟧ = ⟦(char #x20)⟧ = 0x000020
+
+     3. Each string constant of the form ""\ud₃d₂d₁d₀"" where each dᵢ is a
+        hexadecimal digit is interpreted as the word consisting of just the 
+        character with code point 0xd₃d₂d₁d₀
+
+        Ex: ⟦""\u003A""⟧ = ⟦(char #x3A)⟧ = 0x00003A
+
+     4. Each literal of the form ""\u{d₀}"" (resp., ""\u{d₁d₀}"", ""\u{d₂d₁d₀}"",
+        ""\u{d₃d₂d₁d₀}"", ""\u{d₄d₃d₂d₁d₀}"" or ""\u{d₅d₄d₃d₂d₁d₀}""), where each 
+        dᵢ is a hexadecimal digit, is interpreted as the word consisting 
+        of just the character with code point 0xd₀ (resp., 0xd₁d₀, 0xd₂d₁d₀, 
+        0xd₃d₂d₁d₀, 0xd₄d₃d₂d₁d₀, or 0xd₅d₄d₃d₂d₁d₀).
+
+        Ex: ⟦""\u{3A}""⟧ = ⟦(char #x3A)⟧ = 0x00003A
+
+     5. ⟦l⟧ = ⟦l₁⟧⟦l₂⟧  if l does not start with an escape sequence and can be 
+        obtained as the concatenation of a one-character string literal l₁ and
+        a non-empty string literal l₂.
+
+        Ex: ⟦""a\u02C1""⟧ = ⟦""a""⟧⟦""\u02C1""⟧ = 0x000061 0x0002C1
+            ⟦""\u2CA""⟧ = 0x00005C ⟦""u2CXA""⟧        (not an escape sequence)
+            ⟦""\u2CXA""⟧ = 0x00005C ⟦""u2CXA""⟧       (not an escape sequence)
+            ⟦""\u{ACG}A""⟧ = 0x00005C ⟦""u{ACG}A""⟧   (not an escape sequence)
+
+     6. ⟦l⟧ = ⟦l₁⟧⟦l₂⟧  if l can be obtained as the concatenation of string
+        literals l₁ and l₂ where l₁ is an escape sequence and l₂ is non-empty.
+
+        Ex: ⟦""\u02C1a""⟧ = ⟦""\u02C1""⟧⟦""a""⟧ = 0x0002C1 ⟦""a""⟧
+            ⟦""\u{2C}1a""⟧ = ⟦""\u{2C}""⟧⟦""1a""⟧ = 0x00002C ⟦""1a""⟧
+
+     Note: Character positions in a string literal are numbered starting at 0, 
+           with escape sequences treated as a single character – consistently
+           with their semantics.
+
+           Ex.: In ""a\u1234T"", character a is at position 0, the character 
+                corresponding to ""\u1234"" is at position 1, and character T is
+                at position 2.")
+
+  (set-info :notes
+    "Observe that the first form, \ud₃d₂d₁d₀, has exactly 4 hexadecimal digit, 
+     following the common use of this form in some programming languages.
+     Unicode characters outside the range covered by \ud₃d₂d₁d₀ can be
+     represented with the long forms \u{d₄d₃d₂d₁d₀} and \u{d₅d₄d₃d₂d₁d₀}.
+  
+     Also observe that programming language-specific escape sequences, such as
+     \n, \b, \r and so on, are _not_ escape sequences in this theory as they
+     are not fully standard across languages.
+
+     SMT-LIB 2.6 has one escape sequence of its own for string literals. Two
+     double quotes ("") are used to represent the double-quote character within 
+     a string literal such as the one containing this very note. That escape 
+     sequence is at the level of the SMT-LIB frontend of a solver, not at the 
+     level of this theory.")
+
+  ;---------------
+  ; String values
+  ;---------------
+  (define-syntax 
+    ; non-terminals
+    (⟨string_value⟩) 
+    ; production rules
+    ((⟨string_value⟩ ((! ⟨string⟩ :syntax-restrict 
+                                   "Same restriction as for string constants")))))
+ 
+  (define-values () String ⟨string_value⟩)
+
+
+  (set-info :notes
+    "The set of values for String and Lan could be restricted further, to remove
+     some redundancies. For instance, we could disallow leading zeros in escape
+     sequences.
+     For Lan, we could insist on some level of normalization for regular
+     expression values. These restrictions are left to future versions.")
+
+  (set-info :notes
+    "All function symbols in this theory denote *total* functions, i.e., they
+     are fully specified by the theory. This is achieved by returning _error_
+     values for inputs where the intended functions are undefined.
+     Error outputs are always outside of the range of the intended function,
+     so there is no confusion with non-error outputs.")
+
+
+  ;----------------
+  ; Core functions
+  ;----------------
+
+ ; String functions
+
+  ; Strings::++
+  ; String concatenation
+  (declare-const ++ (-> String String String) :builtin
+    " ⟦++⟧ is the word concatenation function."
+    :left-assoc)
+
+  ; Lexicographic ordering
+  (declare-const < (-> String String Bool) :builtin
+    "⟦<⟧(w₁, w₂) is true iff w₁ is smaller than w₂ in the lexicographic 
+     extension to UC* of the standard numerical < ordering over UC.
+
+     Note: The order induced by < corresponds to alphabetical order
+     for strings composed of characters from the alphabet of a western language 
+     such as English:
+     ⟦(< ""a"" ""aardvark"" ""aardwolf"" ... ""zygomorphic"" ""zygotic"")⟧ = true"
+    :chainable)
+
+  ; Functions on languages
+
+  ; String to language injection
+  (declare-const to_lan (-> String Lan) :builtin
+    "⟦to_lan⟧(w) = { w } .
+    ")
+
+  (set-info :notes
+    "Function to_lan allows one to write _symbolic regular expressions_, 
+     e.g., Lan terms with subterms like (to_lan x) where x is a variable. 
+     Such terms have more expressive power than regular expressions. This is 
+     intentional, for future developments.
+     The restriction to actual regular expressions will be imposed in a logic
+     where to_lan will be applicable to string constants only.
+    ")
+
+  ; Language membership
+  (declare-const in (-> String Lan Bool) :builtin
+    "⟦in⟧(w)(L) = true iff w ∈ L .")
+
+  ; Constant denoting the empty set of strings
+  (declare-const empty Lan :builtin
+    "⟦empty⟧ = ∅ .")
+
+  ; Constant denoting the set of all strings 
+  (declare-const univ Lan :builtin
+    "⟦univ⟧ = ⟦String⟧ = UC* .")
+
+  ; Constant denoting the set of all strings of length 1
+  (declare-const allchar Lan :builtin
+    "⟦allchar⟧ = { w ∈ UC* | |w| = 1 } .")
+      
+  ; Language concatenation
+  (declare-const ++ (-> Lan Lan Lan) :builtin
+    "⟦++⟧(L₁)(L₂) = { w₁w₂ | w₁ ∈ L₁ and w₂ ∈ L₂ } ."
+    :left-assoc)
+
+  ; Language union
+  (declare-const union (-> Lan Lan Lan) :builtin
+    "⟦union⟧(L₁)(L₂) = { w | w ∈ L₁ or w ∈ L₂ } ."
+    :left-assoc)
+
+  ; Language intersection
+  (declare-const inter (-> Lan Lan Lan) :builtin
+    "⟦inter⟧(L₁)(L₂) = { w | w ∈ L₁ and w ∈ L₂ } ."
+    :left-assoc)
+
+  ; Kleene Closure
+  (declare-const * (-> Lan Lan) :builtin
+    "⟦*⟧(L) is the smallest subset K of UC* such that
+     1. ε ∈ K
+     2. ⟦++⟧(L)(K) ⊆ K
+    ")
+
+  ;--------------------
+  ; Bridging functions
+  ;--------------------
+
+  ; String length
+  (declare-const len (-> String Int) :builtin
+    "⟦len⟧(w) = |w|  (the number of characters, i.e., elements of UC, in w).")
+
+  (set-info :notes
+    "⟦len⟧(w) is **not** the number of bytes used by some Unicode encoding, such
+     as UTF-8 – that number can be greater than the number of characters. 
+
+     ⟦len(""\u1234"")⟧ is 1 since every escape sequence denotes a single
+     character.")
+
+  ;----------------------
+  ; Additional functions
+  ;----------------------
+
+  ; Reflexive closure of lexicographic ordering
+  (define-const <= (-> String String Bool)
+    (lambda ((x String) (y String)) (or (= x y) (< x y)))
+    :chainable)
+
+  ; Substring
+  ; (substr s i n) evaluates to the longest (unscattered) substring
+  ; of s of length at most n starting at position i.
+  ; It evaluates to the empty string if n is negative or i is not in 
+  ; the interval [0,|s|-1].
+  (declare-const substr (-> String Int Int String) :builtin
+    "⟦substr⟧(w)(m)(n) is the unique word w₂ such that
+       for some words w₁ and w₃
+       - w = w₁w₂w₃ 
+         - |w₁| = m
+         - |w₂| = min(n, |w| - m)  if 0 <= m < |w| and 0 < n
+       - ⟦substr⟧(w, m, n) = ε   otherwise")
+
+  (set-info :notes
+    "The second part of this definition makes ⟦substr⟧ a total function.")
+
+  ; Singleton string containing a character at given position 
+  ; or empty string when position is out of range.
+  ; The leftmost position is 0.
+  (define-const at (-> String Int String)
+    (lambda ((x String) (n Int)) (substr x n 1)))
+
+  ; First string is a prefix of second one.
+  ; (prefixof s t) is true iff s is a prefix of t.
+  (define-const prefixof (-> String String Bool)
+    (lambda ((x String) (y String))
+      (exists ((z String)) (= x (++ y z)))))
+
+  ; First string is a suffix of second one.
+  ; (suffixof s t) is true iff s is a suffix of t.
+  (define-const suffixof (-> String String Bool)
+    (lambda ((x String) (y String))
+      (exists ((z String)) (= x (++ z y)))))
+
+  ; First string contains second one
+  ; (contains s t) iff s contains t.
+  (define-const contains (-> String String Bool)
+    (lambda ((x String) (y String))
+      (exists ((z1 String) (z2 String)) (= x (++ z1 y z2)))))
+
+  ; Index of first occurrence of second string in first one starting at 
+  ; the position specified by the third argument.
+  ; (indexof s t i), with 0 <= i <= |s| is the position of the first
+  ; occurrence of t in s at or after position i, if any. 
+  ; Otherwise, it is -1. Note that the result is i whenever i is within
+  ; the range [0, |s|] and t is empty.
+  (declare-const indexof (-> String String Int Int) :builtin 
+    "⟦indexof⟧(w)(w₂)(i) is the smallest n such that for some words w₁, w₃
+     - w = w₁w₂w₃
+     - i <= n = |w₁| if ⟦contains⟧(w)(w₂) = true and i >= 0
+     - ⟦indexof⟧(w,w₂,i) = -1  otherwise")
+
+  ; Replace
+  ; (replace s t t') is the string obtained by replacing the first
+  ; occurrence of t in s, if any, by t'. Note that if t is empty, the
+  ; result is to prepend t' to s; also, if t does not occur in s then
+  ; the result is s.
+  (declare-const replace (-> String String String String) :builtin 
+    "- ⟦replace⟧(w)(w₁)(w₂) = w          if ⟦contains⟧(w, w₁) = false
+     - ⟦replace⟧(w)(w₁)(w₂) = u₁w₂u₂
+       where u₁ is the shortest word such that w = u₁w₁u₂
+                                         if ⟦contains⟧(w, w₁) = true")
+
+  ; (replace_all s t t’) is s if t is the empty string. Otherwise, it
+  ; is the string obtained from s by replacing in one pass 
+  ; all occurrences of t in s by t’, starting with the first occurrence 
+  ; and proceeding in left-to-right order. 
+  (declare-const replace_all (-> String String String String) :builtin 
+    "- ⟦replace_all⟧(w)(w₁)(w₂) = w
+       if ⟦contains⟧(w)(w₁) = false or w₁ = ε
+     - ⟦replace_all⟧(w)(w₁)(w₂) = u₁w₂⟦replace_all⟧(u₂)(w₁)(w₂)
+       otherwise
+       where u₁ is the shortest word such that w = u₁w₁u₂")
+
+  ; (replace_lan s l t) is the string obtained by replacing the
+  ; shortest leftmost match of l in s, if any, by t.
+  ; Note that if l contains the empty string, the result is to prepend t to s.
+  (declare-const replace_lan (-> String Lan String String) :builtin 
+    "- ⟦replace_lan⟧(w)(l)(u) = w₁uw₂
+       where v is the shortest leftmost word from l in w such that w = w₁vw₂
+     - ⟦replace_lan⟧(w)(l)(u) = w
+       if no substring in w belongs to l")
+
+  ; Language difference
+  (declare-const diff (-> Lan Lan Lan) :builtin
+    "⟦diff⟧(L₁)(L₂) = L₁ \ L₂"
+    :left-assoc)
+
+  ; Language complement
+  (define-const comp (-> Lan Lan)  
+    (lambda ((l Lan)) (diff univ l)))
+
+  ; Language Kleene cross
+  ; (+ e) abbreviates ee*.
+  (define-const + (-> Lan Lan)  
+    (lambda ((l Lan)) (++ l (* l))))
+
+  ; Language option
+  ; (opt e) abbreviates e ∪ {ε}
+  (define-const opt (-> Lan Lan)
+    (lambda ((l Lan)) (union l (to_lan ""))))
+
+  ; Language range
+  ; (range s₁ s₂) is the set of all *singleton* strings s such that
+  ; (<= s₁ s s₂) provided s₁ and s₂ are singleton. Otherwise, it 
+  ; is the empty language.
+  (declare-const range (-> String String Lan) :builtin
+    "- ⟦range⟧(w₁)(w₂) = { w ∈ UC | w₁ ⪯ w ⪯ w₂ } where ⪯ = ⟦<=⟧
+       if |w₁| = |w₂| = 1
+     - ⟦range⟧(w₁)(w₂) = ∅
+       otherwise")
+
+  (set-info :notes
+    "⟦range⟧(⟦""ab""⟧, ⟦""c""⟧) = ∅
+     ⟦range⟧(⟦""a""⟧, ⟦""bc""⟧) = ∅
+     ⟦range⟧(⟦""c""⟧, ⟦""a""⟧)  = ∅")
+
+  (set-info :notes
+   "The arguments to range can be symbolic. This is intentional, 
+    as in the case of to_re .")
+
+
+  ; TODO change the order of the arguments of ^?
+
+  ; Function symbol indexed by a numeral n.
+  ; (^ n e) is the nth power of e:
+  ; - (^ 0 e) = (to_re "") 
+  ; - (^ n' e) = (++ e (^ n e))  where n' = n + 1
+  ;   (^ n Lan Lan)
+  (declare-const ^ (-> (! Int :syntax ⟨int_value⟩) Lan Lan) 
+    :builtin
+    "⟦^⟧(n)(L) = Lⁿ  where Lⁿ is defined inductively on n as follows:
+      - L⁰ = { ε } 
+      - Lⁿ⁺¹ = ⟦++⟧(L)(Lⁿ)"
+  )
+
+  ; Function symbol indexed by two numerals i and n.
+  ; - (loop i n e) = empty                        if i > n
+  ; - (loop i n e) = (^ n₁ e)                     if i = n
+  ; - (loop i n e) = (union (^ i e) ... (^ n e))  if i < n
+  (declare-const loop 
+    (-> (! Int :var i :syntax ⟨int_value⟩ :restrict (>= i 0)) 
+        (! Int :var n :syntax ⟨int_value⟩ :restrict (>= n 0))  
+        Lan Lan)
+    :builtin
+    "⟦loop⟧(i)(n)(L) = Lⁱ ∪ ... ∪ Lⁿ   if i <= n       
+     ⟦loop⟧(i)(n)(L) = ∅               otherwise")
+
+  ; (is_digit s) is true iff s consists of a single character which is 
+  ; a decimal digit, that is, a code point in the range 0x000030 ... 0x000039.
+  (define-const is_digit (-> String Bool)
+    (lambda ((s String))
+      (or (= s (char #x000030))
+        (= s (char #x000031))
+        (= s (char #x000032))
+        (= s (char #x000033))
+        (= s (char #x000034))
+        (= s (char #x000035))
+        (= s (char #x000036))
+        (= s (char #x000037))
+        (= s (char #x000038))
+        (= s (char #x000039)))))
+;     ⟦is_digit⟧(w) = true  iff |w| = 1 and 0x000030 <= w <= 0x000039
+
+  ;-----------------------------------------
+  ; Bridging functions to and from integers
+  ;-----------------------------------------
+
+  ; (to_code s) is the code point of the only character of s, 
+  ; if s is a singleton string; otherwise, it is -1. 
+  (declare-const to_code (-> String Int) :builtin
+    "- ⟦to_code⟧(w) = -1 if |w| ≠ 1
+     - ⟦to_code⟧(w) = i  otherwise, where i is such that w = (char i)
+                                    since w consists of a single code point")
+
+  ; (from_code n) is the singleton string whose only character is
+  ; code point n if n is in the range [0, 0xFFFFFF].
+  ; Otherwise, it is the empty string.
+  (declare-const from_code (-> Int String) :builtin
+    "- ⟦from_code⟧(n) = n        if 0x000000 <= n <= 0xFFFFFF 
+     - ⟦from_code⟧(n) = ε        otherwise")
+
+  ; Conversion to integers
+  ; (to_int s) with s consisting of digits (in the sense of is_digit)
+  ; evaluates to the positive integer denoted by s when seen as a number in 
+  ; base 10 (possibly with leading zeros).
+  ; It evaluates to -1 if s is empty or contains non-digits. 
+  (declare-const to_int (-> String Int) :builtin
+    "- ⟦to_int⟧(w) = -1 if w = ⟦l⟧ 
+       where l is the empty string literal or one containing anything other than
+       digits, i.e., characters with code point outside the range
+       0x000030–0x000039
+
+     - ⟦to_int⟧(w) = n if w = ⟦l⟧  
+       where l is a string literal consisting of a single digit denoting
+       number n
+
+     - ⟦to_int⟧(w) = 10*⟦to_int⟧(w₁) + ⟦to_int⟧(w₂) if 
+         - w = w₁w₂
+         - |w₁| > 0
+         - |w₂| = 1
+         - ⟦to_int⟧(w₁) >= 0
+         - ⟦to_int⟧(w₂) >= 0")
+
+  (set-info :notes
+    "to_int is made total by mapping the empty word and words with
+     non-digits to -1.
+
+     The function returns a non-negative number also for words that start
+     with (characters corresponding to) superfluous zeros, such as 
+     ⟦""0023""⟧.")
+
+  ; Conversion from integers.
+  ; (from_int n) with n non-negative is the corresponding string in
+  ; decimal notation, with no leading zeros. If n < 0, it is the empty string. 
+  (declare-const from_int (-> Int String) :builtin
+    "- ⟦from_int⟧(n) = w    if n > 0, where w is the shortest word
+                                      such that ⟦to_int⟧(w) = n
+     - ⟦from_int⟧(n) = ε    otherwise")
+
+  (set-info :notes
+    "from_int is made total by mapping negative integers to the empty word.
+
+     ⟦to_int⟧(⟦from_int⟧(n)) = n iff n is a non-negative integer.
+
+     ⟦from_int⟧(⟦to_int⟧(w)) = w iff w consists only of digits *and*
+                                     has no leading zeros.")
+
+  (set-info :notes
+    "(to_int ""00123"") evaluates to 123.
+     (from_int 123) evaluates to ""123"".
+     (to_int ""-123"") evaluates to -1, an error value, not to -123.
+     (from_int -123) evaluates to """", an error value, not to ""-123"".")
+))
+
  

  (raw file)
diff --git a/virtual/SSI-free.sh b/virtual/SSI-free.sh index 851c012..22e60ab 100755 --- a/virtual/SSI-free.sh +++ b/virtual/SSI-free.sh @@ -15,7 +15,7 @@ replace() { } for FILE in `find . -maxdepth 1 -name '*.shtml'`; do - replace "$FILE" > ../"$FILE" + replace "$FILE" > ../new/"$FILE" done diff --git a/virtual/benchmarks.shtml b/virtual/benchmarks.shtml index c5f9351..4402d51 100644 --- a/virtual/benchmarks.shtml +++ b/virtual/benchmarks.shtml @@ -27,120 +27,18 @@ Released for free under a Creative Commons Attribution 3.0 License

Benchmarks

-

The SMT-LIB benchmark repository is now hosted on the SMT-LIB GitLab server. Read access does not require an account. - The releases are stored in the master branch. The current release is at the head.
-

-

- The following links point to the repositories for individual logics.
- Note: Some of the logics listed below have not been entered in the Logics section yet. - -

Non-incremental benchmarks

- ABVFP, - ALIA, - AUFBVDTLIA, - AUFDTLIA, - AUFLIA, - AUFLIRA, - AUFNIA, - AUFNIRA, - BV, - BVFP, - FP, - LIA, - LRA, - NIA, - NRA, - QF_ABV, - QF_ABVFP, - QF_ALIA, - QF_ANIA, - QF_AUFBV, - QF_AUFLIA, - QF_AUFNIA, - QF_AX, - QF_BV, - QF_BVFP, - QF_BVFPLRA, - QF_DT, - QF_FP, - QF_FPLRA, - QF_IDL, - QF_LIA, - QF_LIRA, - QF_LRA, - QF_NIA, - QF_NIRA, - QF_NRA, - QF_RDL, - QF_S, - QF_SLIA, - QF_UF, - QF_UFBV, - QF_UFIDL, - QF_UFLIA, - QF_UFLRA, - QF_UFNIA, - QF_UFNRA, - UF, - UFBV, - UFDT, - UFDTLIA, - UFDTNIA, - UFIDL, - UFLIA, - UFLRA, - UFNIA -

Incremental benchmarks

- ABVFP, - ALIA, - ANIA, - AUFNIRA, - BV, - BVFP, - LIA, - LRA, - QF_ABV, - QF_ABVFP, - QF_ALIA, - QF_ANIA, - QF_AUFBV, - QF_AUFBVLIA, - QF_AUFBVNIA, - QF_AUFLIA, - QF_BV, - QF_BVFP, - QF_FP, - QF_LIA, - QF_LRA, - QF_NIA, - QF_UF, - QF_UFBV, - QF_UFBVLIA, - QF_UFLIA, - QF_UFLRA, - QF_UFNIA, - UFLRA -

- Instructions on how to clone each repository are available in the - repository's space. You can also - download this bash script, uncomment the - lines relevant to the logic/repositories you want to clone, and run - it. Note: Benchmarks with a size of 10MB+ are stored - via Git LFS. You will need - to install and set up Git LFS before cloning any repositories. -

-

Zip archives

- To decrease maintenance, we decided not to provide zip archives anymore. If you miss this feature, let us know. - + The latest release of the SMT-LIB benchmark library is hosted on Zenodo under the SMT-LIB community. + Also available there are all previous releases starting from 2023.

+

StarExec

-

The latest release of the benchmark library is also available on StarExec. +

Historical releases of the benchmark library, from 2013 to 2023, are available on StarExec.

Submitting Benchmarks

For details on how to submit benchmarks to SMT-LIB, please refer to the README file in - the benchmarks-pending - repository on the SMT-LIB GitLab. + the benchmark-submission + SMT-LIB GitHub repository.

diff --git a/virtual/bottom.shtml b/virtual/bottom.shtml index 7ba940d..46f5f0f 100644 --- a/virtual/bottom.shtml +++ b/virtual/bottom.shtml @@ -3,30 +3,30 @@

Latest News

- May 12, 2021 -

- 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. -

+ April 2, 2024 +

+ 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 + Zenodo. +

Previous News

- April 2, 2021 -

- A new release of the SMT-LIB 2.6 reference document - is now available. This is a minor release addressing a few - errors in the 2017-07-18 release. -

+ Feb 13, 2024 +

+ The latest release (2023) of the SMT-LIB benchmark library is now + available on Zenodo in the form of compressed archives. +

Older News

- Feb 11, 2020 -

- A theory of Unicode character strings and regular expressions has been added - to the set of SMT-LIB theories. -

- [More] + May 12, 2021 +

+ 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. +

+ [More]

diff --git a/virtual/credits.shtml b/virtual/credits.shtml index c25aa53..054e797 100644 --- a/virtual/credits.shtml +++ b/virtual/credits.shtml @@ -422,7 +422,8 @@ Released for free under a Creative Commons Attribution 3.0 License

This site was developed and is currently maintained by Cesare Tinelli, - with contributions from Clark Barrett and Pascal Fontaine. + with contributions from Clark Barrett, Pascal Fontaine, + Matthias Preiner, and Hans-Jörg Schurr.

Any opinions, findings and conclusions or recommendations expressed in this site are those of the authors and do not necessarily reflect the views of the funding institutions or corporations. diff --git a/virtual/language.shtml b/virtual/language.shtml index 111d2e2..9a838d3 100644 --- a/virtual/language.shtml +++ b/virtual/language.shtml @@ -35,10 +35,9 @@ Released for free under a Creative Commons Attribution 3.0 License [ pdf | bib ]

Previous releases: + 2021-05-12; 2021-04-02; - 2017-07-18; - 2021-05-12 - + 2017-07-18
The SMT-LIB Standard: Version 2.5, by Clark Barrett, Pascal Fontaine, and Cesare Tinelli. diff --git a/virtual/news.shtml b/virtual/news.shtml index da4a99b..71ffab7 100644 --- a/virtual/news.shtml +++ b/virtual/news.shtml @@ -25,6 +25,19 @@

News

+ + April 2, 2024 +

+ From today on 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 + Zenodo. +

+ + Feb 13, 2024 +

+ The latest release (2023) of the SMT-LIB benchmark library is now + available on Zenodo in the form of compressed archives. +

May 12, 2021

diff --git a/virtual/version3.shtml b/virtual/version3-proposal.shtml similarity index 100% rename from virtual/version3.shtml rename to virtual/version3-proposal.shtml