SMT-LIB
The Satisfiability Modulo Theories Library

SMT-LIB Version 3.0 - Preliminary Proposal

by C. Barrett, P. Fontaine, and C. Tinelli

Overview

This page contains a high-level proposal for SMT-LIB Version 3. While some aspects of the language are still being worked out, this document is a fairly accurate description of the new format. A reference document is under construction and will contain a description of the proposal in full detail. This page focuses on the most salient aspects of the proposal, for a quicker overview. More content will be added with time as needed.

Preamble

New underlying logic

The main new aspect of the proposed new version is the move from (an extension of) many-sorted first-order logic as the underlying logic of SMT-LIB to a higher-order logic with polymorphism and dependent types but classical semantics. An important aspect of this change is that the new language for SMT-LIB scripts strives to be as backward-compatible as possible to that of Version 2.7. This is achieved in two ways:

1. Giving new meaning to old syntax as needed.
2. Defining the formal semantics so that it is essentially the same as the old one over the old syntax.

The underlying logic of SMT-LIB 3 has many elements of the Calculus of Inductive Constructions (CIC), which are at the basis of the formal foundation of proof assistants like Rocq and Lean. The main restriction is allowing only rank-1 (prenex) polymorphism and not having a Prop-like kind for (constructive) propositions. So, contrary to CIC, formulas are not types and instead continue to be expressed as terms of a two-element Bool type; this is more similar to the logic of the PVS proof assistant or proof assistants of the HOL family. However, as in SMT-LIB 2.7, type polymorphism is approximated by having global (i.e., top-level) type variables, as opposed to actual quantification over types, and so making polymorphic constants actually families of overloaded symbols. In addition to being polymorphic, and contrary to Version 2.7, types can now depend on values as in dependently-typed logics.

Motivation

The main motivation for the move to a CIC-like logic is manyfold.

1. Having a more expressive underlying logic considerably simplifies the design and the formal foundations of the SMT-LIB standard. It obviates the need for most of the ad-hoc extensions to many-sorted first-order logic we had to introduce in Version 2 while also providing enough expressive power to define most theories formally, as opposed to textually as is done in SMT-LIB 2. That includes theories that are not easily definable in Version 2 such as the theory of parametric bit vectors.
2. It facilitates the definition of a single language to define theories, logics, and benchmarks.
3. It extends the possibility for SMT solvers to provide support for higher-order reasoning, facilitating their integration as automated reasoning back ends into higher-order theorem provers and into proof assistants, which are also based on a higher-order logic. Current integrations rely on complex encodings from the higher-order logics supported by these tools to the many-sorted logic of SMT-LIB 2. Moving to a higher-order logic should dramatically simplify these encodings, improving the trustworthiness of the integration. Natively reasoning with higher-order constructs (e.g., via higher-order equational reasoning) by the SMT solver could also considerably improve solving times on goals coming from these tools.
4. It enables the introduction of a number of new SMT-LIB theories (for sets, relations, database tables, sequences) which benefit from the availability of second-order functions such as as fold, map, filter and so on, both to define common operations and to reason about them.

The move to the new logic maintains backward compatibility with SMT-LIB 2.7 to a very large extent. In particular, it should minimally affect SMT-LIB 2.7-compliant solvers whose developers choose not to support the new features.

The core language

Technically, the core language of SMT-LIB 3 is a higher-order logic with dependent types and rank-1 polymorphism. Terms in this logic are built out of variables, constants, applications, Π-abstractions, and λ-abstractions, as in the CIC calculus. There are three classes of (well-formed) terms in the language:

• terms denoting values, such as 3, (+ x 3), (lambda ((x Int)) (+ x 3));
• terms denoting types, such as Bool, Int, (-.> Int Real), (Array Int Bool), (List Int), (BitVec 3);
• terms denoting kinds, such as Type, (-> Int Type).

Well-formed value terms have an associated type term (or, simply, type). Well-formed type terms have an associated kind term (or, simply, kind). For instance,

• 3 is a constant of type Int, which has kind Type;
• not is a constant of type (→ Bool Bool), which has kind Type;
• List is a type constant of kind (→ Type Type);
• BitVec is a type constant of kind (→ Int Type).

With the shift to seeing funtion symbols as constants of → type, the command declare-const becomes primitive, and declare-fun and define-fun are now derived from it. For example, following commands

  (declare-fun h (Int Real) Real)
  (define-fun avg ((x Real) (y Real)) Real (/ (+ x y) 2))

  (declare-const h (→ Int Real Real))
  (define-const avg (→ Real Real Real)
    (lambda ((x Real) (y Real)) (/ (+ x y) 2)))

Name Space and Shadowing

There is a single name space for identifiers, regardless of whether they are used as value constants, type constants, or variables. Within this name space, bound variables, that is, variables local to a specific binder, can shadow any identifier with the same name, including other variables, in accordance with the standard lexical scoping discipline. Note that this policy is more flexible than in Version 2, where bound variables cannot have the same name as, and so cannot shadow, theory symbols.

Dependent Types

In Version 3, constants that have a type τ dependent on a value take as extra argument also the value that τ depends on. For instance, bit vector function symbols take as argument also the size of the bit vector. For conciseness and backward compatibility, however, such arguments are declared as implicit any time they can be inferred from later arguments.

Concretely, dependent function types are expressed with the syntax illustrated in this example:

  (→ (! Int :var n) (BitVec n) (BitVec (+ n 1)))

  (→ (! τ₁ :var x) τ₂) 

(Pi (x τ₁) τ₂) or (Forall (x τ₁) τ₂)

  (→ (! Int :var n :implicit) (BitVec n) (BitVec n))

A further attribute, :restrict, permits the imposition of semantic restrictions on input and output values of a function, something that, in its full generality, effectively allows the definition of PVS-style predicate subtypes (aka, refinement types). For instance, in type

  (→ (! Int :var n :implicit :restrict (> n 0)) (BitVec n) (BitVec n))

  [n: {m : Int | m > 0} → BitVec(n) → BitVec(n)]

  (→ (! Int :var m :implicit :restrict (> m 0)) 
     (! Int :var n :implicit :restrict (> n m)) 
     (BitVec m) (BitVec n) (BitVec (- n m)))

  (→ (! Int :var n :implicit :restrict (> n 0) :syntax <.numeral.>) 
     (BitVec n) (BitVec n))

Polymorphic Types

Polymorphic types reproduce the polymorphic sorts of Version 2.7 through the introduction of globally-declared type variables. A polymorphic type is either a type variable, a nullary type constant, or the application of a non-nullary type constant to value terms and/or polymorphic types. For instance, if X and Y are type variables, and Int and Array are type constants, then (Array Int Int), (Array Int Y), (Array X Int), and (Array X Y) are all polymorphic types. A monomorphic type is a polymorphic type with no occurrences of type variables. For example, (Array Int Int) is a polymorphic type that is also monomorphic.

Note that this version of polymorphism is (intentionally) not equivalent to polymorphism in logics like CIC, where polymorphic functions take types as input. For example, the array select function in does not have type:

  (→ (! Type :var I :implicit) (! Type :var E :implicit) (Array I E) I E) 

  (→ (Array I E) I E) 

Terms

A consequence of identifying functions and maps from Version 2.7 is that the lambda binder of Version 2.7 can now be used to construct the lamba abstractions for all types, not just map types. Its general form is now

  (lambda ((x τ₁)) t)

  (lambda ((x A)) (lambda ((y A)) (not (= x y))))

Since a constant f of type (→ σ₁ ⋅⋅⋅ σᵢ) is a higher-order function when i > 2, partial applications of such constants, e.g., (f t), are meaningful and legal. The syntax (f t₁ ⋅⋅⋅ tᵢ) for the full application of f remains the same as in Version 2.7 although it is now seen as an abbreviation of ( ⋅⋅⋅ ((f t₁) t₂) ⋅⋅⋅ tᵢ).

Version 2.7 allows the application of maps via the apply operator @, as in (@ f a). This syntax is maintained but is now extended to all functions, because of identification of maps with functions.

Formulas

As in Version 2, formulas are terms of type Bool. Predefined constants include

• the constants true and false of type Bool,
• the equality operator =, now a polymorphic constant of type (→ α α Bool),
• the ite operator, now a polymorphic constant of type (→ Bool α α α),

A core language of commands allows one to declare new type variables, type constants, and value constants, and to assert formulas.

  (declare-type-var X)  ; declares a new type variable 
  (declare-type A ())   ; declares a new simple type (a nullary type constant) 
  (declare-type B ()) 
  (declare-const a A)        ; declares a constant of type A
  (declare-const f (→ A B))  ; declares a constant of type (→ A B)
  (declare-const g (→ A B))
  (declare-const p (→ A B Bool))
  (declare-const id (→ X X)) ; a polymorphic function 

  (assert (= b (f a))) 
  (assert (= f g))                                   ; higher-order assertion
  (assert (= p (lambda ((x A) (y B)) (= (g x) y))))  ; higher-order assertion
  (assert (forall ((x X)) (= x (id x))))             ; polymorphic assertion

  (declare-type Collection (Type))
  (declare-type Pair (Type Type)) 
  (declare-type BitVec (Int)) 
  (declare-type Vector (Type Int)) 

Note that since declare-type is essentially a constant declaration but the at level of kinds, the command (declare-type Vector (Type Int)), say, could be understood as an abbreviation of (declare-const Vector (→ Type Int Type)), although the latter syntax is not actually allowed.

Semantic restrictions on types

While semantic restrictions on types yield the full power of predicate subtyping, their intended use in SMT-LIB 3 is to document precisely the input domain over which a partial function or type constant is defined. So they are meant to be used as formal documentation, not as the definition of a subtype. The type system SMT-LIB 3 remains without subtypes which means that semantic restrictions on types can be completely ignored for type checking purposes. That said, solvers can use type restriction information to provide more informative messages in case of scripts that use partial functions outside of their domain of definition. As an example, the integer division operator in Version 3 is defined as follows

  (declare-const div (→ Int (! Int :var n :restrict (distinct n 0)) Int) 

Semantic restrictions can be introduced in function declarations and definitions, and can apply also to the returned value, as shown in the following example.

  (declare-const f 
    (-> (! Int :var m1 :restrict (> m1 0)) 
        (! Int :var m2 :restrict (> m2 m1)) 
        (! Int :var n :restrict (exists ((x Int)) (= n (* 2 x)))))
  )

  (declare-fun f ((m1 Int :restrict (> m1 0)) (m2 Int :restrict (> m2 m1)))
    (! Int :var n :restrict (exists ((x Int)) (= n (* 2 x))))
  )

As another example, the actual bit vector type in the Version 3 bit vector theory is defined as follows:

  (declare-type BitVec ((! Int :var m :restrict (>= m 0)))

Syntactic restrictions on types

Syntactic restrictions on types are orthogonal to semantic ones and have a different purpose: to restrict the set of expressible terms and formulas in a benchmark so as to achieve decidability of the satisfiability problem or some other computational objective — as done, for instance, in the various BV logics of SMT-LIB 2. Concretely, in modules corresponding to SMT-LIB logics (see later), the parameter m of the bit vector type above is further constrained to be a numeral, as opposed to an arbitrary Int integer term, as follows:

  (declare-type BitVec ((! Int :var m :restrict (>= m 0) :syntax <.numeral.>)))

  (define-fun-rec * ((x Int :syntax <.signed_numeral.>) (y Int)) 
    (ite (= x 0) 0
      (ite (< x 0) (* (- x) y) 
        (+ x (* ((- x 1) y)))))
   :left-assoc)

Contrary to semantic restrictions, syntactic restrictions must be enforced by compliant SMT solvers.

Commands

The SMT-LIB 3 language contains almost all commands in Version 2.7 as well as an additional number of new constructs and commands. A large number of them, however, are defined in terms of the core language above. This includes all the commands from Version 2.7, none of which change semantics in practice in Version 3. Most of them become syntactic sugar of core Version 3 commands. Some of them will be deprecated and eventually phased out. For instance, declare-const is now a core command while declare-fun is not. The SMT-LIB 2.7 expression

  (declare-fun f (τ₁ ⋅⋅⋅ τᵢ) τ)

  (declare-const f (→ τ₁ ⋅⋅⋅ τᵢ τ))

  (define-fun f ((x₁ τ₁) ⋅⋅⋅ ((xᵢ τᵢ)) τ t)

  (define-fun-rec f ((x₁ τ₁) ⋅⋅⋅ ((xᵢ τᵢ)) τ t)

  (define-const f (→ τ₁ ⋅⋅⋅ τᵢ τ) (lambda ((x₁ τ₁) ⋅⋅⋅ ((xᵢ τᵢ)) t))

  (define-const-rec f (→ τ₁ ⋅⋅⋅ τᵢ τ) (lambda ((x₁ τ₁) ⋅⋅⋅ ((xᵢ τᵢ)) t))

In a similar vein, sorts are not primitive anymore and become types. Correspondingly, declare-sort is now a special case of the new core command declare-type. For instance,

  (declare-sort S n)

  (declare-type S (Type ⋅⋅⋅ Type))

  (define-sort S (u₁ ⋅⋅⋅ uᵢ) σ)

  (define-type S ((u₁ Type) ⋅⋅⋅ (uᵢ Type)) σ)

  (declare-type Vector (Type (! Int :var m :restrict (>= m 0)))
  (define-type NonEmptyRealVector ((n Int :restrict (> n 0))) (Vector Real n))
  (define-type RealVector8 () (NonEmptyRealVector 8))

Command attributes

  (declare-type-var A)
  ...
  (declare-const = (-> A A Bool)
   :pairwise 
   :builtin 
   "= denotes the identity function, which returns true iff 
    its two arguments are identical.") 

  (define-fun or ((b1 Bool) (b2 Bool)) Bool
    (ite b1 true b2) 
   :left-assoc)

Binders

The primitive binders in Version 3 are

• let, the parallel version of local definitions ((let ((x₁ t₁) ⋅⋅⋅ (xn tn)) t));
• lambda, for function (λ) abstraction ((lambda ((x₁ τ₁) ⋅⋅⋅ (xn τn)) t)).

The other binders are the following:

• match, for cases analysis of algebraic datatypes;
• forall, the universal quantifier;
• exists, the existential quantifier;
• choose, the choise operator.

  (lambda ((p (→ A bool))) (= p (lambda ((x A)) true)))))

  (forall ((x₁ τ₁) ⋅⋅⋅ (xᵢ τᵢ)) φ) 

  (forall (lambda ((x₁ τ₁) ⋅⋅⋅ (xᵢ τᵢ)) φ)) 

  (choose (x τ) φ)

  (choose (lambda ((x τ)) φ))

Polymorphism in declarations, definitions and assertions

  (declare-type-var α)
  (declare-const f (→ α α))

  (assert (forall ((a α)) (= (f a) a)))

  (define-fun g1 ((a α) (p (→ α Bool))) Bool (h a)) 
  (define-fun g2 ((a α) (p (→ α Bool))) Bool (h 1)) 

  (assert 
    (let ((id (lambda ((x α)) x)))
      (= 1 (id 1))
    )
  )

Function g1 is also polymorphic, with type ∀α.(α → (α → Bool) → Bool). However, its input predicate p is not polymorphic. For each monomorphic instance of g1 of type (τ → (τ → Bool) → Bool), the input function h is of type τ → Bool, not ∀α.(α → Bool). This means, that function g2 has in fact an ill-typed body since its instance of type (String → (String → Bool) → Bool), say, applies its input function to a value whose type is not String.

The last assert is ill-typed in a similar way, since the variable id has type α → α, not ∀α.(α → α). In more technical terms then, Version 3's type system does not allow let-polymorphism. Only globally defined symbols can be polymorphic.

Overloading

Within an SMT-LIB 3 script, some symbols can be overloaded by redeclaring them, others cannot. Specifically, type constants and type variables cannot be overloaded. In particular, they cannot be redeclared as a type constant, type variable, value constant or local variable. In contrast, value constants can always be redeclared. We say that a constant f has a, possibly polymorphic, principal type τ in a script if the script contains a declaration or definition of f with type τ. A constant has more than one principal type in a script if and only if it is overloaded. As in previous versions, Version 3 enforces a type discipline that allows simple bottom-up typing. If a constant f is overloaded, the type of each occurrence of f in a term is determined as follows:

1. If f occurs in a function position, as in (f t₁ ··· tₙ), the type of f is the one in the most recent declaration of f that makes (f t₁ ··· tₙ) well typed;
2. If f occurs as an argument, as in (t₁ ··· f ··· tₙ), its type is the one in the most recent declaration of f.

This disambiguation policy can be overridden by explicitly ascribing to f one of its types using the as operator, in an expression of the form (as f τ) where τ is the intended type of that occurrence, that is, an instance of a principal type of f. Specifically, the f selected by (as f τ) is be the most recently declared f whose type has τ as an instance.

  (declare-type-var X)
  (declare-const f (→ (List X) X))    ; variant 1, polymorphic
  (declare-const f (→ Int Real Int))  ; variant 2
  (declare-const f (→ Int Int))       ; variant 3
  (declare-const f (→ Int Real))      ; variant 4
  (declare-const p (→ X Bool))

  (assert (f 5 4.3))  ; no ambiguity, variant 2 of f inferred here
  (assert (f 8))      ; ambiguity resolved in favor of variant 4, the most recent
  (assert (p f))      ; ambiguity resolved in favor of variant 4, the most recent

Note that as stands now for the standard ascription operator. This is different with the use of as in Version 2, which provides only the return type of the function. This one of the very few cases that breaks backward-compatibility.

In extensions of the script above with later commands, f cannot be reintroduced with type (→ Int Real Int), (→ Int Int), (→ Int Real), or (→ (List τ) τ) for any type τ, since such types would all be instances of a type already assigned to f. The different use of as in SMT-LIB 3 versus Version 2 represents one of the few changes that are not backward compatible with Version 2.7. However, this is not a serious concern since as has been used mostly for 0-arity constants (like the nil list constructor) where the new and the old use coincide.

New language constructs

Some of the new constructs for terms, such as lambda and choose, are specific to the move to higher-order logic. Other novel constructs are orthogonal to that extension and are motivated by a desire to unify in a single language the various sublanguages of SMT-LIB 2.7 for theory definitions, logic definitions, and command scripts. This is done by extending the command language to allow the definition of theory symbols in the same style as user-defined symbols and by introducing a notion of module that can be used to define both theories and logics.

Modules

Modules are a general construct to structure scripts in units with their own name space and provide a basic form of encapsulation and information hiding. For the medium term, modules will not be allowed in user scripts. The hope, however, is that with time they will be supported by SMT solvers and so will eventually be available to regular users. For now, they will be used only to define SMT-LIB theories and logics.

(define-module M (
  (declare-type-var A)
  (declare-type ping ()) 
  (declare-type pong ()) 
  (declare-const a ping)
  (declare-const f (→ A pong))  
  ; The scope (visibility) of the symbols 
  ; A, ping, pong, a, and f is limited to module M
  )
)
; A, ping, pong, a, and f are not directly accessible here

The scope, that is, the visibility, of symbols introduced in a module is limited to the module. Such symbols can be accessed outside the module only if they are exported by the module’s interface and only with a qualified name of the form <.module name.>::<.symbol.> (e.g., M::ping).

Module Interfaces

By default, all the symbols (i.e., constants and type constants) declared and defined in a module M are public, i.e., visible by modules importing M. Optionally, however, it is possible to specify explicitly an interface for the module, which selects the symbols that are exported, that is, made visible. Interfaces are used to construct modules that correspond to logics in the sense of SMT-LIB 2. The interface is specified with two attributes in a module definition:

• :type-vars whose value is the list of exported type variables,
• :types whose value is the list of exported type constants with their associated input kind or type, if any, and
• :consts whose value is the list of exported constants with their associated type.

(define-module M (
  (declare-type-var X)
  (declare-type-var Y)
  (declare-type A ())
  (declare-type B ())
  (declare-type C ()) 
  (declare-type Pair (Type Type))   

  (declare-const a A)
  (declare-const b B)
  (declare-const f (→ A B))
  (declare-const g (→ B A)) 
  (declare-const c (→ A C))
  (declare-const d (→ X Y X))

  (define-const  h (→ A A) (lambda ((x A)) (g (f x))))
  )
 :type-vars ( X )
 :types ( A B (Pair (Type Type)) )
 :consts ( (a A) (f (→ A B)) (h (→ A A)) (d (→ X X X)) )
)

  (forall ((x1 A) (x2 A)) (=> (= (f x1) (f x2)) (= (h x1) (h x2))))

All three interface attributes are optional. The absence of the :types attribute, say, causes all all type constants in the module are exported in their full generality. In contrast, giving it value () causes no type constants to be exported. The same policy applies to :type-vars and :consts. When a datatype constant (e.g., List) is exported, the datatype's recursor and all of its constructors, selectors, and testers are exported by default.

The reason constants are listed in a module's interface with an associated type is that its is possible to assign them a more restricted type than the one they have in the module. For instance, the array select function, which has type

  (→ (Array I E) I E) 

  :type-vars ( I E ) 
  :types ( Bool Int (Array (Type Type)) ... ) 
  :consts ( (select (→ (Array Int E) Int E))
            (select (→ (Array I Bool) I Bool))
            ... ; constants other than select 
          )

The exported type constants can be restricted in similar way, disallowing in the importing modulo any terms whose types does not conform to the restrictions. For example, a module having a type constant Seq (for generic sequences of len n) of kind: (→ (! Int :var n :restrict (>= n 0)) Type Type) could export it as follows:

  :types 
  ( (Seq (! Int :var n :syntax <.numeral.> :restrict (even n)) Type)
    ... 
  )

For polymorphic types, it is possible to impose instantiation restrictions on the type parameters, using a similar syntax using a (limited) language of constraints over types.

(define-module M2 (
  ...
  (declare-type Array (Type Type))
  ...
  )
 :types ( ... (Array (! I Type :restrict (= I Int)) Type) ... )
 :consts ( ... )
)

A natural question is why add restrictions on an exported symbol (type constant or constant) in the interface of a module and not directly inside the module when the symbol is declared. The reason is that a module can import a symbol from another module and export a restricted version of it. This approach is followed in defining modules that correspond to SMT-LIB 2 logics. Such modules import symbols from theory modules in their full generality and then export them with restrictions. For instance, a linear integer arithmetic module would import the arithmetic symbols from the module defining the integers and export the multiplication symbol with the additional restriction that at least one of its arguments is a (concrete) integer value:

  :consts 
  ( (* (→ (! Int :syntax <.int_value.>) Int Int))
    (* (→ Int (! Int :syntax <.int_value.>) Int)
    ... 
  )

Module Imports

Modules can be imported into another module or at the top level in an SMT-LIB 3 script with the new command import-modules which lists all the modules to be imported. At most one import command is allowed in a module. Moreover, the command has to occur before any command that modifies the context (declarations, assertions, ...). At the top level, later import commands are allowed only if interleaved with reset commands.

  (import-modules (M1 M2)) 
  ...
  (reset)
  (import-modules (M3)) 
  ...

Qualified names

Every module automatically defines a name space corresponding to it. The name space is reflected in the generation of qualified names for the symbols exported by a module. Qualified names have the form M::s where M is the module's name and s is a symbol exported by M. Note that using :: as a separator in qualified names does not break backward compatibility because :: is not allowed in Version 2.7 identifiers.

  (import-modules (Ints Reals))

  (declare-const n Ints::Int)
  (declare-const x Reals::Real)
  (define-const i Ints::Int (Ints::+ n Ints::2))
  (define-const y Reals::Real (Reals::+ x Reals::4.3))

The new command open-module can be used to allow unqualified names for the (exported) symbols of an imported module.

;; Example 1
(define-module M1 (
  (declare-type A ())
  (declare-type B ())
  (declare-type C ()) 
  (declare-const a A)
  (declare-const f (→ A B)) 
  (declare-const P (→ A B Bool))
  (assert (P b (f a)))
 )
 :types (A B)
 :consts ((a A) (f (→ A B)))
)

(import-modules (M1))
; all exported symbols of M1 are now visible with their fully qualified name
; all assertions in M1 are now in the assertion context.

(declare-const a1 M1::A) ; declares a1 in the top-level namespace
(assert (= a1 M1::a))    ; adds this equality to the assertion context
(open-module M1) 

; now all symbols of M1 can be used without qualification
(declare-const b2 B) 
(assert (= b2 (f a))) ; B, f and a are from M1

The effect of opening a module M is to create a local alias for each symbol exported by M. In Example 1 above, (open-module M1) can be understood as an abbreviation of

  (define-type A () M1::A)
  (define-type B () M1::B)
  (define-const a A M1::a)
  (define-const f (→ A B) M1::f)

Opening one of more modules creates the possibility of overloading at the level of the importing module, as in the example below. That overloading is resolved with the same policy as for overloading caused by local declarations. Since the policy is based on the order in which two constants with the same name are introduced, the order in which two modules are open is then meaningful.

; Example 2
(import-modules (Ints Reals))
(open-module Ints)
(open-module Reals)
(declare-const n Int)           ; Int is an alias of Ints::Int
(declare-const x Real)          ; Real is an alias of Reals::Real
(define-const i Int (+ n 2))    ; + and 2 are aliases of Ints::+ and Ints::2
(define-const y Real (+ x 4.3)) ; + and 4.3 are aliases of Reals::+ and Reals::4.3

A module M importing a module N can export the symbols exported by N as if they were its own. It has the option, however, to export them with stronger restrictions. The name used in M's interface to export N's symbols can be its fully qualified name (with the prefix N::) or its short version if N is opened in M.

An important point is that all module imports declare their symbols at the top level, which means that qualified names are never nested. Importing a module M at the top level that in turn imports a module N internally has the effect of first importing N at the top level and then M. However, since M is the module being directly imported at the top level, the only symbols of N visible (that is, usable in later commands) are those re-exported by M, if any. If M opens N, the module prefix of the fully qualified names of the re-exported symbols of N is indifferently M:: or N::. Concretely, if s is a type constant or constant exported by N and then re-exported by M, it is accessible at the top level as N::s or as M::s, or simply as s once M has been opened; it is not accessible as M::N::c. (The latter would be the case if N's definition itself was inside M's which is, however, not allowed since all modules are defined at the top level.)

Import Graph

Considering the top level as an implicit (special) module, let's say that a module N is imported directly by a module M if N appears explicitly in an import command in M. We say that N is imported indirectly by M if N is imported, directly or indirectly, by a module imported by M. Circular import dependencies are disallowed, that is, a module cannot import itself, directly or indirectly. In other words, the "directly imports" relation always defines a direct acyclic graph over modules.

Without interleaving calls to the reset command, a module N can be imported directly at most once but can be imported indirectly many times as a result of importing several modules that in turn import N. Another consequence on the import structure is that a module's symbol can be imported in a module multiple times and with different restrictions. The effect of two imports of symbols from the same module is additive: symbols imported with the second import that had not already been imported with the first are added to the top level; however, no already imported symbols are removed.

If the same dependent constant c is imported once with a (restricted) type τ₁ and then with a (restricted) type τ₂ then it can be used with either type. (Note that c is not overloaded in this case because type τ₁ and τ₂ both are restrictions of the same principal type that c has in the module it originally was introduced in.)

(define-module M0 (
  (declare-type-var X)
  (declare-type-var Y)
  (declare-const p (→ X Y Bool))
  )
 ; X, Y and p are exported in full generality
)
(define-module M1 (
  (import-modules (M0))
  (open-module M0)
  (declare-type A ())
  )
 :type-vars (Y)
 :consts (p (→ A Y Bool))
)
(define-module M2 (
  (import-modules (M0))
  (open-module M0)
  (declare-type B ())
  )
 :type-vars (X)
 :consts (p (→ X B Bool))
)
(define-module M3 (
  (import-modules (M1 M2))
  (open-module M1)
  (open-module M2)
  ...
  )
)

Algebraic Data Types

Algebraic data types in SMT-LIB 3 are unchanged from version 2.7, both in syntax and semantics.

  (declare-datatypes ((Size 0) (Option 1) (List 1) (Pair 2)) ()
    ; Size
    ((small) (medium) (large))
    ; Option
    (par (V) ((none) (some (val V)) ))
    ; List
    (par (E) ((nil) (cons (head E) (tail (List E)))))
    ; Pair
    (par (A B) ((pair (first A) (second B))))
    )
  )

  (declare-datatype BinTree (par (X)
    ((leaf) (node (left (BinTree X) (val X) (right (BinTree X)))))
  )

A consequence of maintaining the old syntax from Version 2.7 is that, while algebraic datatypes can be polymorphic, they cannot be dependent (on values). This restriction is intentional but could be lifted in future releases of Version 3. Another restriction is that constructors of arity greater than 1, which are now higher-order functions, can be applied only in full. For example, a term like (node leaf) is not well-formed, whereas one like (node leaf 4 leaf) is.

Testers and recursors

Every inductive type definition induces an implicit definition of testers for each constant as well as general recursor for the type. For example, for the List type defined above there would be the following tester functions

  (is-nil (→ (List E) Bool))
  (is-cons (→ (List E) Bool))

Recursors are a new feature in SMT-LIB 3. Using again as an example the List datatype introduced above, its definition also defines automatically the recursor reduce of type (→ Y (→ X (List X) Y Y) (List X) Y) where X and Y are type variables. The List recursor behaves as if it had been directly defined as follows

  (declare-type-var X)
  (declare-type-var Y)
  (define-fun-rec reduce 
    ( (y0 Y) (comb (→ X (List X) Y Y)) (l (List X)) ) ; input vars
    Y                                                 ; output type
    (match l ( 
      (nil y0)
      ((cons h t) (comb h t (reduce y0 comb t))))))

  (define-fun-rec reduce 
    ( (y0 Y) (comb (→ (BinTree X) X (BinTree X) Y Y Y)) (t (Tree X)) ) Y
    (match t ( 
      (leaf y0)
      ((node t1 v t2) (comb t1 v t2 (reduce y0 comb t1) (reduce y0 comb t2))))))

For each datatype, the recursor can be defined automatically based on the datatype's constructors and their type. The rationale for having recursors supported directly by the SMT solver is that a wealth of functions over a recursive datatype can be defined, non-recursively, by the user in terms of reduce. This in principle should facilitate reasoning about functions over datatypes as the solver can concentrate on reasoning about reduce. For the List datatype, the functions that can be defined with reduce include the following:

  ; Sum over the elements of an Int list
  (define-const sum ((l (List Int))) Int
    (reduce 0 (lambda ((n Int) (t (List Int)) (s Int)) (+ n s)) l) 
  )
  ; Length of a list
  (declare-type-var A)
  (define-fun len ((l (List A))) Int
    (reduce 0 (lambda ((a A) (t (List A)) (n Int)) (+1 n)) l)
  )
  ; List concatenation
  (define-fun append ((l1 (List A))) (l2 (List A)) (List A)
    (reduce l2 (lambda ((a A) (t (List A)) (r (List A))) (cons a r)) l1)
  )
  ; List reverse
  (define-fun reverse ((l (List A))) (List A)
    (reduce (as nil (List A)) 
      (lambda ((a A) (t (List A)) (r (List A)))
        (append r (cons a (as nil (List A))))) l)
  )
  ; List of elements of input list that satisfy input predicate
  (define-fun filter ((p (-> A Bool)) (l (List A))) (List A)
    (reduce (as nil (List A)) 
      (lambda ((a A) (t (List A)) (r (List A))) (ite (p a) (cons a r) r)) l)
  )
  (declare-type-var B)
  ; List map function
  (define-fun map ((f (→ A B)) (l (List A))) (List B)
    (reduce (as nil (List A)) 
      (lambda ((a A) (t (List A)) (r (List B))) (cons (f a) r)) l)
  )

External Symbols

When defining new theories there is sometimes the need for two theories to refer to each other's symbols. This cannot be done with imports because it would create a circular dependency. To address this issue while keeping theories in separate modules the language allows the definition of external types and constants in a module.

More generally, one imports a module A in a module B if B is meant to be an extension of A. If, on the other hand, A and B are conceptually separate modules where, however, one module may need to use a type or a constant in the other, then they can be introduced as external. Types constants and constants in module can be declared as external with an :extern attribute which connects them to symbols exported by another module.

Suppose a module Ints defines the integer theory with its usual operators and a unary operator +1 for the integer successor function. A module for the theory of lists may be defined as follows.

(define-module Lists (
  (declare-datatype List (par (X)
    ((nil) (cons (head X) (tail (List X))))))
  ...
  (declare-type Int () :extern Ints::Int)
  (declare-const 0 Int :extern Ints::0)
  (declare-const +1 (→ Int Int) :extern Ints::+1)
  (define-fun len ((l (List A))) Int
    (reduce 0 (lambda ((a A) (t (List A)) (n Int)) (+1 n)) l))
  ...
  )
  :type-vars ( E )
  :types ( (List Type) )
  :consts ( ... (len (→ (List E) Ints::Int) )
)

In general, symbols declared as :extern in a module M cannot be exported by M. This entails that if M exports a symbol s that depends on external symbols from a module N, a module importing M can use s in a command only if it imports N too. [To do: define precisely what it means for a symbol to depend on external ones.]

In the example above, since Lists exports a function whose type and definition depend on external symbols from module Ints, any module importing Lists must also import Ints so that the reference to the external symbols in Lists can be resolved.

  ; Example 1
  (import-modules (Lists))
  ; Illegal import since Lists::len depends on Ints.
  ...

  ; Example 2
  (import-modules (Ints Lists))
  ; Lists::len can be used here
  ...

Syntactic categories for syntax restrictions

[To do: definition of <.int_value.> <.pos_numeral.> and so on via an attribute grammar. Syntax categories can be defined in modules and should be exported like types and constants.]

SMT-LIB 3 Theories

The standard SMT-LIB 3 theories are now defined just as modules. A first draft of the new definition for some of the standard theories in Version 2.7 is available below. Note that the modules are still at the pre-proposal stage. They are incomplete and subject to change. However, they should offer a pretty good idea of the expressive power of SMT-LIB 3. The theories are defined intentionally to be rather rich. Any restriction on theory signature and language is left to modules that define restricted logics.

In the current formalization, the theories below are essentially conservative extensions of the corresponding SMT-LIB 2.7 theories, that is, they have more symbols and richer types but do not change the semantics 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 "2026-XX-XX")
  (set-info :written-by "Pascal Fontaine and Cesare Tinelli")
  (set-info :date "2026-03-15")
  (set-info :last-updated "2026-03-15")
  (set-info :update-history
   "TODO.")

  (declare-type-var A)
  (declare-type-var B)
  (declare-type-var C)

  ;-----------------
  ; Builtin symbols
  ;----------------- 

  ; Booleans
  (declare-datatype Bool ((true) (false)))

  ; Equality  
  (declare-const = (-> A A Bool)
   :pairwise 
   :builtin 
   "= denotes the identity function, which returns true iff 
    its two arguments are identical.")

  ;-------------------
  ; Defined constants
  ;------------------- 
  ; Apply
  (define-fun @ ((f (-> A B)) (a A)) B
    (f a)
   :left-assoc) ; (@ f a b) = (@ (@ f a) b)
  ; Identity
  (define-const iden ((a A)) A
    a)
  ; if-the-else 
  (define-fun ite ((b Bool) (a1 A) (a2 A)) A
    (match b (true a1) (false a2))) 
  ; not
  (define-fun not ((b Bool)) Bool
    (ite b false true))
  ; !=
  (define-fun != ((a1 A) (a2 A)) Bool 
    (not (= a1 a2)))
  ; distinct
  (define-fun distinct ((a1 A) (a2 A)) Bool 
    (!= a1 a2)
   :pairwise)
  ; or
  (define-fun or ((b1 Bool) (b2 Bool)) Bool
    (ite b1 true b2) 
   :left-assoc)
  ; and
  (define-fun and ((b1 Bool) (b2 Bool)) bool
    (ite b1 b2 false)
   :left-assoc)
  ; implies
  (define-fun => ((b1 Bool) (b2 Bool)) Bool
    (ite b1 b2 true)
   :right-assoc)
  ; iff
  (define-fun <=> ((b1 Bool) (b2 Bool)) Bool
    (= b1 b2)
   :right-assoc)
  ; xor
  (define-fun xor ((b1 Bool) (b2 Bool)) Bool 
    (!= b1 b2)
   :left-assoc)
  ; forall
  (define-fun forall ((p (-> A Bool))) Bool
    (= p (lambda ((x A)) true)))
  ;
  (set-info :notation 
   "(forall ((x τ)) φ) abbreviates 
    (forall (lambda ((x τ)) φ))
  
    (forall ((x₁ τ₁) ⋅⋅⋅ (xᵢ τᵢ)) φ) abbreviates 
    (forall ((x₁ τ₁)) ⋅⋅⋅ (forall ((xᵢ τᵢ)) φ))")
  ; exists
  (define-fun exists ((p (-> A Bool))) Bool
    (!= 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 (-> A Bool) A)
  ; choose is defined axiomatically   
  (assert (forall ((p (-> A Bool))) (<=> (exists p) (p (choose p)))))
  ;
  (set-info :notation 
   "(choose (x τ) φ)  abbreviates  (choose (lambda ((x τ)) φ))")
  ; compose
  (define-fun compose ((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.")

  ;-----------------------
  ; Abstract value syntax
  ;-----------------------
  (define-syntax 
    ; non-terminals
    ( <.abstract_value.> <.bool_value.> )
    ; production rules
    ( (<.bool_value.> (true false))
      (<.abstract_value.> ((! <.symbol.> :restrict "starts with @")))))

  ;-------------
  ; Bool values
  ;-------------
  (define-values <.bool_value.> () Bool)


  ;-------------------
  ; Import Attributes
  ;-------------------

  (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.")
))

(define-module Ints (
  (set-info :smt-lib-version 3.0)
  (set-info :smt-lib-release "2026-XX-XX")
  (set-info :written-by "Pascal Fontaine and Cesare Tinelli")
  (set-info :date "2026-03-15")
  (set-info :last-updated "2026-03-15")
  (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-consts <.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-fun <= ((x Int) (y Int)) Bool
    (or (= x y) (< x y))
   :chainable)
  ; >
  (define-fun > ((x Int) (y Int)) Bool
    (< y x)
   :chainable)
  ; >=
  (define-fun >= ((x Int) (y Int)) Bool
    (or (= x y) (> x y))
   :chainable)
  ; unary -
  (define-fun-rec - ((x Int)) Int
    (ite (< x 0) (+1 (- (+1 x))) 
      (ite (= x 0) 0
        (-1 (- (-1 x))))))
  ; +
  (define-fun-rec + ((x Int) (y Int)) Int
    (ite (< y 0) (-1 (+ x (+1 y))) 
      (ite (= y 0) x 
        (+1 (+ x (-1 y)))))
   :left-assoc)
  ; binary -
  (define-fun - ((x Int) (y Int)) Int
    (+ x (- y))
   :left-assoc
   :no-partial 
   ; this constant cannot be applied partially:
   ; (- t) is not allowed but ((as - (-> Int Int Int)) t) is allowed
   )
  ; * 
  (define-fun-rec * ( (x Int) (y Int) ) Int
    (ite (< y 0) (- (* x (- y))) 
      (ite (= y 0) 0
        (+ x (* x (-1 y)))))
   :left-assoc)
  ; abs
  (define-fun abs ((x Int)) Int
    (ite (>= x 0) x (- x)))

  ; div 
  (declare-const div (-> Int (! Int :var n :restrict (!= n 0)) Int) 
   :left-assoc)
  ; mod
  (declare-fun mod (-> Int Int Int))
  ; div/mod axiom
  (assert (forall ((m Int) (n Int)) (=> (!= 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-fun divisible ( (m Int) (n Int :restrict (> n 0)) ) Bool
    (= (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-fun-rec sum ((a Int) (b Int) (f (-> Int 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 "numeral 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).")
))

(define-module Reals (
  (set-info :smt-lib-version 3.0)
  (set-info :smt-lib-release "2026-XX-XX")
  (set-info :written-by "Pascal Fontaine and Cesare Tinelli")
  (set-info :date "2026-03-15")
  (set-info :last-updated "2026-03-15")
  (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-consts <.decimal.> Real 
   :builtin
   "Each <.decimal.> denotes the corresponding real number as usual.")

  ; negation
  (declare-const - (-> Real Real) :builtin "Unary 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-fun - ((x Real) (y Real)) Real
    (+ x (- y))
   :left-assoc)
  ; division /
  (declare-const / (-> Real Real Real) :left-assoc :restrict (!= y 0.0))
  (assert (forall ((x Real) (y Real)) (=> (distinct y 0.0)
    (= x (* y (/ x y))))))
  ; <
  (define-fun < ((x Real) (y Real)) Bool
    (and (<= x y) (!= x y))
   :chainable)
  ; >
  (define-const > ((x Real) (y Real)) Bool
    (< y x)
   :chainable)
  ; >=
  (define-const >= ((x Real) (y Real)) Bool
    (<= y x)
   :chainable)
  ; Summation 
  ; we use a step different from 1 and provide it as additional input
  (define-fun-rec sum ((a Real) (b Real) (f (-> Real Real))) Real
    (ite (> a b)  0.0 
      (+ (f a) (sum (+ a 1.0) b f))))
  ; rational constants
  (define-const / ((n Int :value) (d Int :value :restrict (> (to_real d) 0.0))) Real
    (/ (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 
                          "as integers, <.m.> and <.n.> have no common factors besides 1")))
     (<.p.> ((! <.decimal.> :syntax "it has the form n.0 except for 0.0")))
     (<.m.> ((! <.numeral.> :syntax "it is not 0")))
     (<.n.> ((! <.numeral.> :syntax "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
      (!= 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
  ")
))

[Coming soon.]

[Coming soon.]

SMT-LIB 3 Logics

One of the goals of SMT-LIB 3 is to get rid of the notion of SMT-LIB logic (such as QF_UF, LIA, and so on) and provide users the ability, in effect, to construct logics on the fly by importing the right modules with the right restrictions at the beginning of an SMT-LIB script.

With some limitations, modules, interfaces and imports provide a suitable mechanism for indicating to an SMT solver a specific fragment in which to reason, allowing the solver to apply the best reasoning techniques at its disposal for that fragment, or recognize it as unsupported.

SMT-LIB logics, however, have been used historically also for another, orthogonal purpose: providing a way to index/structure the SMT-LIB benchmark library. Concurrently, they have also been used by the SMT-COMP competition as a convenient way to structure the competition in divisions. These uses of logics make them still necessary. So the set-logic will not go away. However, in SMT-LIB 3 it becomes an abbreviation of a particular sequence of module declarations and imports.

For example, (set-logic QF_UF) could become an abbreviation of

(define-module QF_UF (
  (import (Core))
  (open Core) 
 )  
 :type-vars (A)
 :types (Bool)
 :consts (
    (true Bool)
    (false Bool)
    (ite (→ Bool A A A))
    (not (→ Bool Bool))
    (= (→ A A Bool) :pairwise)
    (!= (→ A A Bool))
    (distinct (→ (A A Bool)) :pairwise)
    (=> (→ Bool Bool Bool) :right-assoc)
    (and (→ Bool Bool Bool) :left-assoc)
    (or (→ Bool Bool Bool) :left-assoc)
    (xor (→ Bool Bool Bool) :left-assoc)
    (<=> (→ Bool Bool Bool) :left-assoc)
    ; quantifiers and other higher-order constants are not exported
 )
 :FOL ; only FOL syntax allowed
)
(import (QF_UF))
(open QF_UF)
...

Similarly, for the logic LIA (set-logic LIA) would be and abbreviation of

(define-module LIA (
  (import (Core Ints))
  (open Core)
  (open Ints)
 )
 :type-vars (A)
 :types (Bool Int)
 :consts (
    (<.numeral.> Int)
    (+ (→ Int Int Int) :left-assoc)
    (- (→ Int Int Int) :left-assoc)
    (* (→ (! Int :syntax <.int_value.>) (! Int :syntax <.symbol.>) Int)) ; linear mul.
    (* (→ (! Int :syntax <.symbol.>) (! Int :syntax <.int_value.>) Int)) ; linear mul.
    (* (→ (! Int :syntax <.symbol.>) (! Int :syntax <.symbol.>) Int)
      :left-assoc) ; linear mul.
    (> (→ Int Int Bool) :chainable)
    (>= (→ Int Int Bool) :chainable)
    (< (→ Int Int Bool) :chainable)
    (<= (→ Int Int Bool) :chainable)
    (true Bool)
    (false Bool)
    (ite (→ Bool A A A))
    (not (→ Bool Bool))
    (= (→ A A Bool) :pairwise)
    (!= (→ A A Bool))
    (distinct (→ (A A Bool)) :pairwise)
    (=> (→ Bool Bool Bool) :right-assoc)
    (and (→ Bool Bool Bool) :left-assoc)
    (or (→ Bool Bool Bool) :left-assoc)
    (xor (→ Bool Bool Bool) :left-assoc)
    (<=> (→ Bool Bool Bool) :left-assoc)
    (forall (→ (→ A Bool) Bool))
    (exists (→ (→ A Bool) Bool))
 )
 :FOL ; only FOL syntax allowed
)
(import (LIA))
(open LIA)