diff --git a/version3-draft.shtml b/version3-draft.shtml deleted file mode 100644 index 22aa88e..0000000 --- a/version3-draft.shtml +++ /dev/null @@ -1,1656 +0,0 @@ - - - - - SMT-LIB The Satisfiability Modulo Theories Library - - - - - - - - - - - - - - -
-
-
-
- -
- -
- -
-
-
-
-
- -

SMT-LIB Version 3.0 - Preliminary Proposal

- -Last updated: 2021-12-31 - -

Overview

- -

This page contains a preliminary high-level proposal for SMT-LIB Version 3. -The proposal is still being worked out, and this document is an incomplete 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

- -The great majority of the changes described below will affect the way theories and logics are defined. -It will not affect scripts that rely on (the equivalent of) SMT-LIB 2.6 logics. -This means that most of the features of the Version 3 will not have to be supported by current SMT solvers. -Support for some of new features of SMT-LIB 3 can be introduced gradually over time in a solver as a consequence of deciding to support new theories and logics that rely on those features. - - -

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.6. -This is achieved in two ways: -

    -
  1. Giving new meaning to old syntax as needed.
    2. -
  2. Defining the formal semantics so that it is essentially the same as the old one over the old syntax.
    3. -
-For example, now sorts from SMT-LIB 2.6 are interpreted as simple types, -with parametric sorts interpreted as polymorphic types. -Sorted constant and function symbols are interpreted as typed constants, -with function symbols of arity > 1 becoming higher-order constants, Curry-style. -Index symbols, as in (_ extract i j) or (_ BitVec 4), are now seen as syntactic sugar for symbols with a dependent type/kind. -As in SMT-LIB 2, a number of additional syntactic restrictions on scripts are imposed to obtain various fragments of interests or logics, in SMT-LIB 2 terminology. -

- -

The underlying logic of SMT-LIB 3 has many elements of the Calculus of Inductive Constructions (CIC) used by proof assistants like Coq and Lean, with the main restriction of allowing only rank-1 polymorphism (actually, let-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 similar to the logic of the PVS proof assistant or proof assistants of the HOL family. -Differently from those provers, types can depend both on other types (i.e., be polymorphic) and on values. -Consistently with CIC, polymorphism is achieved by allowing functions to take as arguments not just values but also types, with the restriction, however, that all type arguments must come before value arguments which, in turn, cannot have a polymorphic type (to satisfy the restriction to rank-1 polymorphism). -

- - -

Motivation

- -

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

    -
  1. First, using a more powerful logic as the 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.6. -
    2. -
  2. Second, it allows the definition of a single language to define theories, logics, and benchmarks. -
    3. -
  3. Third, it opens the possibility for SMT solvers to provide support for some level of 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 logic of SMT-LIB 2.6. -Moving to a higher-order logic will 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. -
  4. Fourth, it opens the way to 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. -
    5. -
-

- -

We stress that the move to the new logic maintains backward compatibility with SMT-LIB 2.6 to a very large extent. -In particular, it will affect SMT-LIB 2.6-compliant solvers in a minimal way if their developers choose not to support the new features. -

- -

The core language

- -

- -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), (-> Type Type).
    • -
- -The symbol -> will denote the function type constructor. -We will write it as → in this document from now on, for readability. -

- -

-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 constructor of kind (→ Type Type);
    • -
  • BitVec is a type constructor of kind (→ Int Type).
    • -
- -Note that → is both a type and a kind constructor. -The syntax (→ α β) can be understood as an abbreviation of the CIC type or kind Π x:α β. - -The constructor -→ -can be used as a multiarity right-associative symbol. -This allows one, for example, to write the type -(→ A (→ B C)) -as -(→ A B C), -and the kind -(→ Type (→ Int Type)) -as -(→ Type Int Type). - -Function symbols of rank (σ₁ ⋅⋅⋅ σᵢ) in Version 2.6 become constants of type (→ σ₁ ⋅⋅⋅ σᵢ) in Version 3. -This means that function symbols with more than one argument become higher-order functions in Version 3. -For instance, the integer addition operator + now has type (→ Int Int Int), that is, (→ Int (→ Int Int)). -

- - -

Dependent Types

-

-In Version 3, functions that have a dependent type τ take as extra arguments also the types or value that τ depends on. -For instance, bit vector functions 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)))
- -This expression denotes the type of a function that takes as input an integer n and returns a function that takes a bit vector of size n, and returns a bit vector of size n + 1. -Note that (! Int :var n) uses the same term annotation syntax as in Version 2 but now applied to types. -The new predefined :var attribute annotating Int in this case provides a name (n) for the first input. -The general syntax for dependent types is -
-  (→ (! A :var x) B)
-where x is a bound variable whose scope is B. -An alternative syntax, more reminiscent of that of dependent type logics might have been: - -
(Pi (x A) B)
-or -
(Forall (x A) B)
- -which perhaps makes it clearer that x is a variable bound by the binder Pi/Forall in the scope B. -However, the annotation based syntax is possibly more legible and, more importantly, more flexible because it allows the annotation of function inputs with further attributes. -In particular, it allows one to declare an input argument as implicit. -This is done with the new valueless attribute :implicit -that can be associated to a function argument. -For example, : - -
-  (→ (! Int :var n :implicit) (BitVec n) (BitVec n))
- -makes the first argument implicit — in the sense that it is not needed in applications of functions of that type. -This is sensible since the value of the first argument can be inferred from the type of the second argument. -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))
- -the implicit argument n is required to be a positive integer. -In PVS syntax, this would be the dependent type -
-  [n: {m : Int | m > 0} → BitVec(n) → BitVec(n)]
-
-This notation can also express relational constraints on the input and output types, as for instance, in - -
-  (→ (! Int :var m :implicit :restrict (> m 0)) 
-     (! Int :var n :implicit :restrict (> n m)) 
-     (BitVec m) (BitVec n) (BitVec (- n m)))
- -Yet another attribute, :syntax, allows the introduction of syntactic restrictions on input terms: - -
-  (→ (! Int :var n :implicit :restrict (> n 0) :syntax <numeral>) 
-     (BitVec n) (BitVec n))
-
- -The additional restriction :syntax <numeral> specifies that the only permitted applications of functions of the type above are those where n is a concrete constant (1, 2, ...) and not a symbolic term (x, (+ x 1), ...). -This is convenient, for instance, when defining the current SMT-LIB 2 logics with bit vectors, where bit vector sizes cannot be symbolic. -The language includes constructs to define syntactic categories like <numeral> (see later). -

- - -

Polymorphic Types

- -

-Polymorphic functions are now expressed as having input types that depend on types provided as input, -eliminating the need of the par binder from Version 2.6. -For example, the array select function now has type: - -

-  (→ (! Type :var I :implicit) (! Type :var E :implicit) (Array I E) I E) 
-
- -where the first two, implicit arguments I and E are types. -(Type is the kind of all types.) -This style applies to user-defined polymorphic algebraic datatypes as well. -For instance, the empty list constant nil and the list constructor constant cons would now have type - -
-  (→ (! Type :var X) (List X))   ; type of nil
-
-and -
-  (→ (! Type :var X :implicit) X (List X) (List X))   ; type of cons
-
- -respectively. -Note that the type parameter for nil is not implicit in this case, -which requires one to write (nil Int) for the empty list of integers, for instance. -This solution eliminates the ambiguity problem for polymorphic symbols in Version 2.6 where nil would be an overloaded nullary symbol, making the application of the ascription operator as (i.e., (as nil (List Int))), which is mandatory in SMT-LIB 2.6, unnecessary in this case. -

- -

Terms

- -

-A new core binder in terms is now the -lambda -binder whose general form is -

-  (lambda ((x T)) t)
-
-where t is a value term and x is a bound variable of type or kind T with scope t. -This allows the construction of lambda abstractions such as -
-  (lambda ((A Type)) (lambda ((x A)) (lambda ((y A)) (not (= x y)))))
-
-or, more concisely, - - (lambda ((A Type) (x A) (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.6 although it is now seen as an abbreviation of -( ⋅⋅⋅ ((f t₁) t₂) ⋅⋅⋅ tᵢ). -

- -

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

    -
  • the Boolean constants - true and - false; -
    • -
  • the equality operator - =, - now a polymorphic constant of type - (→ (! Type :var A :implicit) A A Bool))); -
    • -
  • the - ite - operator, now with type - (→ (! Type :var A :implicit) Bool A A A))). -
    • -
- - -

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

-; Example
-(declare-type A ())   ; declares a new simple type (a nullary type constructor) 
-(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))
-(assert (= b (f a))) 
-(assert (= f g))                                   ; higher-order assertion
-(assert (= p (lambda ((x A) (y B)) (= (g x) y))))  ; higher-order assertion
-
-

- -

Constructors for polymorphic/dependent types can be declared -as in the examples below: -

-  (declare-type Collection (Type))
-  (declare-type Pair (Type Type)) 
-  (declare-type BitVec (Int)) 
-  (declare-type Vector (Type Int)) 
-
- -Type constructor Collection -has kind (→ Type Type). -As an example, the type 
-  (→ (! Type :var X) (Collection X))
-
-built using this constructor is polymorphic; -more precisely, it is a dependent type with one type parameter: -X . -
- -Type constructor Pair has kind (→ Type Type Type). -The type 
-  (→ (! Type :var A) (! Type :var B) (Pair A B))
-
-is a dependent type with two type parameters: -A and -B. -
- -Type constructor BitVec -has kind (→ Int Type). -The type 
-  (→ (! Int :var n) (BitVec n))
-
-is a dependent type with one value parameter: -X. -
- -Type constructor Vector -has kind (→ Type Int Type). -The type 
-  (→ (! Type :var X) (! Int :var n) (Vector X n))
-
-is a dependent type with one type parameter and one value parameter: -X and -n, respectively. -

- -

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

- -

Restrictions on parameters in a type

- -

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 constructor 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) 
-
-A solver could use the knowledge of the official restriction above for instance to issue a warning when it returns a model that gives value 0 to a term that occurs as the second argument of a div application in an assertion. -Alternatively, it could try to determine statically, before solving an input problem, if all applications of partial functions in the problem are provably to values within the function's domain, and issue a warning otherwise. -

- -

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)))
-
-Since the parameter m expresses the size of the vector, the added restriction limits the value of m to the positive integers. -(One could argue that the type constructor is well defined also for m = 0 but this is a discussion for another time). -

- -

Note that 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 positive numeral, as opposed to an arbitrary Int term, as follows: - -

-  (declare-type BitVec ((! Int :var m :restrict (> m 0) :syntax <pos_numeral>))
-
- -This means that, in those logics, the BitVec constructor can be applied only to positive numerals. -The same mechanism is applied in logics of linear integer arithmetic to restrict applications of the multiplication operator to linear multiplications. -

- -

Commands

- -

The SMT-LIB 3 language contains almost all commands in Version 2 -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, none of which change semantics in practice in Version 3. -Most of them become syntactic sugar of core Version 3 commands and -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.6 expression -

-  (declare-fun f (τ₁ ⋅⋅⋅ τᵢ) τ)
-
-with i > 0 is now an abbreviation of -
-  (declare-const f (→ τ₁ ⋅⋅⋅ τᵢ τ))
-
-Similarly, -
-  (define-fun f ((x₁ τ₁) ⋅⋅⋅ ((xᵢ τᵢ)) τ t)
-  (define-fun-rec f ((x₁ τ₁) ⋅⋅⋅ ((xᵢ τᵢ)) τ t)
-
-are now respective abbreviations of -
-  (define-const f (→ τ₁ ⋅⋅⋅ τᵢ τ) (lambda ((x₁ τ₁) ⋅⋅⋅ ((xᵢ τᵢ)) t))
-  (define-const-rec f (→ τ₁ ⋅⋅⋅ τᵢ τ) (lambda ((x₁ τ₁) ⋅⋅⋅ ((xᵢ τᵢ)) t))
-
-where define-const and define-const-rec are new commands. -

- -

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)
-
-with n ≥ 0 now becomes an alternative syntax for -
-  (declare-type S (Type ⋅⋅⋅ Type))
-
-with n occurrences of Type. -Similarly, -
-  (define-sort S (u₁ ⋅⋅⋅ uᵢ) σ)
-
-now becomes an alternative syntax for -
-  (define-type S ((u₁ Type) ⋅⋅⋅ (uᵢ Type)) σ)
-
- -Note that declare-type and define-type are more general than their Version 2 counterparts because they can introduce (value) dependent types as well, as in - -
-  (declare-type Vector (Type (! Int :var m :restrict (>= m 0)))
-  (define-type RVector ((n Int :restrict (> n 0))) (Vector Real n))
-  (define-type RV8 () (RVector 8))
-
- -

- -

Binders

- -

The primitive binders in Version 3 are -

    -
  • let, the parallel version of local definitions - ((let ((x1 t1) ⋅⋅⋅ (xn tn)) t)), as in Version 2.6;
    • -
  • lambda, for function (λ) abstraction - ((lambda ((x1 τ1) ⋅⋅⋅ (xn τn)) t)), a new binder;
    • -
  • forall, for universal quantification of types in formulas ((forall ((τ1 Type) ⋅⋅⋅ (τn Type)) φ)), a new binder;.
    • - -
-Another new binder is choose, for the Hilbert choice operator ε, although technically it is a second-order function that can be used with binder syntax. -The let binder is the same as in Version 2 with the addition that now it can be used to define higher-order variables. -The other binders above are new. -The -match binder for algebraic data types is defined in terms of -let as before. -The -forall and -exists quantifiers from Version 2, however, -are not primitive anymore and are instead defined as higher-order functions. -The syntax that uses them as binders becomes syntactic sugar for terms based on lambda. -For instance, -forall -is now defined as the function -
-  (lambda ((A Type) (P (→ A bool))) (= P (lambda ((x A)) true)))))
-
-of type -(→ (! Type :var A :implicit) (→ A Bool) Bool)). -The old syntax, with expressions of the form -
-  (forall ((x₁ τ₁) ⋅⋅⋅ (xᵢ τᵢ)) φ) 
-
-is maintained but it is understood as an abbreviation of -
-  (forall (lambda ((x₁ τ₁) ⋅⋅⋅ (xᵢ τᵢ)) φ)) 
-
-Similarly, the new binder syntax -
-  (choose (x τ) φ)
-
-abbreviates -
-  (choose (lambda ((x τ)) φ))
-

- - -

Polymorphic definitions and assertions

- -[To do. Polymorphic functions can be introduced in declarations and in constant and let definitions, but they cannot be passed as arguments in function applications (let-polymorphism). More generally, the input type of each function symbol has to be a monotype. -Asserted formulas have to be in prenex form with respect to universal type quantifiers. - ] - -

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

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

- - -

- Within a module, overloading of constant symbols is fully allowed. - -The same constant can be declared multiple times as long as it has a different type every time. -More precisely, since we have polymorphic constants, a constant -c -can be given a new type -τ -(with a declare or define command) only if -τ -has no instances in common with any of the current types of -c. -For instance, if -c -has type -(→ (! Type :var X) (Array Int X)), -it cannot be re-declared later to have any of these types: -

-(→ (! Type :var Y) (Array Int Int))
-(→ (! Type :var Y) (Array Y Int))
-(→ (! Type :var X) (Array Int (Array Int X)))
-
-because all of them have instances in common with -(→ (! Type :var X) (Array Int X)). -In contrast, it would be fine to re-declare c with type Int, say. -In the latter case, c would become an overloaded symbol with two (principal) types: -(→ (! Type :var X) (Array Int X)) -and -Int. -(In fact, it would be fine even to redeclare c with type (Array Int Int), say, since the second c would have arity 0 instead of 1, making its type not an instance of the function (→ (! Type :var X) (Array Int X))). -It is an error to have multiple declarations of the same constant that violate the policy above. -

- -

Note that (permitted) overloading of a constant -c -can make the constant or some of its applications ambiguous, -in the sense of SMT-LIB 2.6 that the type of -c -or terms of the form -(c t₁ ⋅⋅⋅ tᵢ) -cannot be uniquely determined by bottom-up type inference. -In those cases, the ascription operator -as -must be used to disambiguate the constant, as in Version 2.6. -The main difference is that function types are first-class in Version 3 and so ascription now specifies the whole type for a function symbol (e.g., (as f (→ Int Bool)) instead of just its return type (e.g., (as f Bool)). -

- -

Consider for instance the following module: -

-(define-module M (
-  (declare-type A ())
-  (declare-type B ()) 
-  (declare-const a A)
-  (declare-const a B)
-  (declare-const b B)
-  (declare-const f (→ B A))
-  (declare-const f (→ A A)) 
-  (declare-const g (→ B A))
-  (declare-const g (→ B B))
-  )
-)
-
-

- -

The constants a, f, and g, for being overloaded, are ambiguous when used as an argument in an application, e.g., (= a b), or (= f g). -Also ambiguous are applications of g (e.g., (g b)). -However, applications of f (e.g., (f b)) are not. -As a consequence, the uses of as in the assertions below are all necessary. - -

- (assert (= (as a A) (f b))) 
- (assert (= (as a B) b)) 
- (assert (= b ((as g (→ B B)) b))) 
- (assert (= (as f (→ B A)) (as g (→ B A))))
-
- -The different use of as in Version 3 represents one of the few changes that are not backward compatible with Version 2.6. -However, this is not a serious concern since as has been used mostly for 0-arity constants where difference between the new and the old use disappears. -

- -

Module Interfaces

- -

-By default, all the symbols (i.e., constants and type constructors) 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: -

    -
  • :types whose value is the list of exported type constructors with their associated kind, and
    • -
  • :consts whose value is the list of exported constants with their associated type.
    • -
-(The type/kind constructor → does not need to be exported because it a primitive symbol of the underlying logic.) -

- -
-  ; Example
-  (define-module M
-   (
-    (declare-type A ())    (declare-type B ())     (declare-type C ()) 
-    (declare-const a A)    (declare-const b B)
-    (declare-const f (→ A B))
-    (declare-const g (→ B A)) 
-    (define-const  h (→ A A) (lambda ((x A)) (g (f x))))
-    (declare-const c (→ A C))
-   )
-   :types ( (A Type) (B Type) )
-   :consts ( (a A) (f (→ A B)) (h (→ A A)) )
-  )
-
- -

In the example above, only two of the type constructors and three of the constants are exported. -Note that the types of the exported constants must be constructible from the exported type constructors for the interface to be well formed. -Also note that any relationship among the exported constants established in the module through non-exported constants (or through assertions) is maintained when the module is imported. -For example, the formula -

-  (forall ((x1 A) (x2 A)) (=> (= (f x1) (f x2)) (= (h x1) (h x2)))
-)
-is valid not just in the module M above but also in any module that imports M. -Concretely, this means that importing a module has always the effect of declaring and asserting everything in the module. -The only effect of the interface is to prohibit in the importing module any direct reference to non-exported symbols. -

- -

The :types attribute is optional. -Its absence causes all type constructors in the module to be exported. -In contrast, giving it value () causes no type constructors to be exported. -The same policy applies to :consts. -

- -

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 -

-  (→ (! Type :var I :implicit) (! Type :var E :implicit) (Array I E) I E) 
-
-in the module declaring it, could be exported as follows: -
-  :types ( (Bool Type) (Int Type) (Array (→ Type Type Type)) ... ) 
-  :consts ( (select (→ (! Type :implicit) (! Type :var E :implicit) (Array Int E) Int E))
-            (select (→ (! Type :var I :implicit) (! Type :implicit) (Array I Bool) I Bool))
-            ... ; constants other than select 
-          )
-
-This would limit the application of select only to values of the listed types. -Note that the interface above is not exporting two select functions; -it is exporting the same polymorphic function but with two (disjunctive) restrictions on its instances. -

- -

The exported type constructors 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 constructor 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 Type)
-    ... 
-  )
-
-which (cumulatively) restricts the application of Seq only to positive even numerals. -The general rule is that the restrictions imposed on an exported symbol in a module interface are in addition to any restrictions already imposed on the symbol within the module. -The meaning of multiple syntactic restrictions is the intersection of the languages denoted by the individual restrictions. -The meaning of multiple semantic restrictions is the conjunction of the individual restrictions. -

- -

For polymorphic types, additional restrictions are expressible by instantiating type parameters. -This can be done indirectly in module interfaces by defining a new type constructor as an instance of some polymorphic type, and then exporting the new constructor. -

-(define-module M (
-  ...
-  (define-type IntArray ((A Type)) (Array Int A))
-  ...
-  )
- :types ( (IntArray (→ Type Type)) )
- :consts ( ... )
-)
-
-disallow any array other than two dimensional arrays with integer indices. - - -

- -

A natural question is why add restrictions on an exported symbol (type constructor 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 -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. -Because two modules can import the same module, it is possible to effectively import a module directly and indirectly several times. -The effect of multiple imports is cumulative for symbols and disjunctive for their restrictions: -if the same symbol is first imported with a restriction R₁ and then with a restriction R₂ then the disjunction of R₁ and R₂ is considered. - -

-  ; Example
-  [To do]
-
-

- -

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::n where M is the module's name and n is the name of a symbol declared in M and exported by M. -Note that using :: as a separator in qualified names does not break backward compatibility because :: is not allowed in Version 2.6 identifiers. - -

-  ; Example
-  (import (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))
-
- - -

- -

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

-  ; Example 1
-  (import (Ints Reals))
-  (open Ints)
-  (open 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
-
- -Note how opening two modules creates the possibility of overloading of at the level of the importing module, as is the case with open in the example above. - - -
-  ; Example 2
-  (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 (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 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 the example above, (open 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)
-
- -

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

- -
-  ; Example
-  [To do]
-
- - - -

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 constructor 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 us 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.) -

- -
-  ; Example
-  [To do]
-
- -

Inductive Data Types

- -Algebraic data types of SMT 2.6 are generalized to inductive data types and their definition gets a new syntax. -The old syntax is accepted but deprecated and will be eventually phases out. -
- -The new syntax is best explained with a few examples. -The old syntax: -
-  (declare-datatypes ((Size 0) (BinTree 0) (Option 1) (List 1) (Pair 2))
-    ( ; Size
-      ((small) (medium) (large))
-      ; BinTree
-      ((empty) (node (left BinTree) (right BinTree)))
-      ; 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))))
-    )
-  )
-
-stands for new syntax: -
-  (define-inductive-types 
-    ((Size ()) (BinTree ()) (Option (Type)) (List (Type)) (Pair (Type Type)))
-    ( ; Size
-      ( (small Size)
-        (medium Size)
-        (large Size)
-      )
-      ; BinTree
-      ( (empty BinTree)
-        (node (-> (! BinTree :selector left) (! BinTree :selector right) BinTree))
-      )
-      ; Option
-      ( (none (→ (! Type :var A)   ; Type input is explicit for this constructor
-                 (Option A)))    
-        (some (→ (! Type :var A :implicit) 
-                 (! A :selector val) (Option A)))
-      )
-      ; List
-      ( (nil (→ (! Type :var E)    ; Type input is explicit
-                (List E))) 
-        (cons (→ (! Type :var E :implicit) 
-                   (! E :selector head) (! (List E) :selector tail)) (List E))
-      )
-      ; Pair
-      ( (pair (→ (! Type :var A :implicit) (! Type :var B :implicit) 
-                 (A :selector first) (B :selector second) (Pair A B))))
-      )
-    )
-  )
-
- - -

The command define-inductive-types takes two arguments: -

    -
  1. a list of pairs of consisting of a type constructor (the name of the inductive type) and a possibly empty list of the form (Type ... Type) for each type constructor, indicating the number of type parameters it takes; -
    2. -
  2. a corresponding list of value constructors for each inductive type. -
    3. -
-The value constructors for an inductive type are themselves grouped in a list. -Each element of this list is a pair of a constructor and its type. - -The type is given with the same syntax as any other (possibly functional) type. -An optional :selector attribute for one of the arguments of the constructor can be used to name the corresponding selector. -

- -

-Several constraints on the type definition ensure the generality and the well-foundedness of the type. -

    -
  • If a datatype D being defined has n parameters, each constructor of that datatype must return a value whose type has the form (D X₁ ... Xᵢ) where X₁ ... Xᵢ are i distinct type variables. Consequently, the constructor must have those type variables as (implicit or explicit) input parameters. -
  • An inductive type can be parametrized by other types but not values. So it can be polymorphic but not dependent in general. - -
    • -
  • If a datatype D being defined has n parameters, each constructor of that datatype must return a value whose type has the form (D X₁ ... Xᵢ) where X₁ ... Xᵢ are i distinct type variables. Consequently, the constructor must have those type variables as (implicit or explicit) input parameters. -
    • -
  • The constructors of the the same datatype must have distinct names. -However, the same name can be used for two constructors of distinct inductive types. -
    • -
  • An inductive type can be parametrized by other types but not values. So it can be polymorphic but not dependent in general. This is a temporary restriction that may be lifted at a later time. -
    • -
  • No nested types are allowed. - That is, the type of a constructor's argument for an inductive type D cannot be a type term that nests D within another type constructor. - For instance, it is not possible to define a parametric inductive type (Tree A) with a constructor of type - (→ A (List (Tree A)) (Tree A)) or - (→ A (Array Int (Tree A)) (Tree A)) - because (Tree A) occurs nested in List (resp. Array). -
    • -
  • The same well-foundedness constraints as in 2.6 (which enable the type inhabited). -
    • -
-

- -

Note that specifying selectors is not mandatory anymore. -The reason is that thanks to the match binder they can eliminated from any formulas without loss of generality. -

- -

Each inductive type D implicitly creates its own namespace similarly to modules. - The fully qualified name for a constructor or selector f for a inductive type D is D::f. -For instance, for the constructor the Pair type defined above id Pair::pair and the selectors are Pair::first and Pair::second. - -Short names can be used after opening the type, as with modules, with the open command: - -

-  (open Pair)
-
- -The same rule on overloading apply as for modules. -

- -

Two new commands are provided as abbreviation of the define-inductive-types. -The first one, define-inductive-type, can be used to define a single inductive type, as in: - -

-  (define-inductive-type (List (Type)) 
-    ( (nil (→ (! Type :var E) (List E))) 
-      (cons (→ (! Type :var E :implicit) 
-               (! E :sel head) (! (List E) :sel tail)) (List E))
-    )
-  )
-
- -The previous command is understood as an abbreviation of: - -
-  (define-inductive-types ( (List (Type)) ) 
-    ( ( (nil (→ (! Type :var E) (List E))) 
-        (cons (→ (! Type :var E :implicit) 
-                 (! E :sel head) (! (List E) :sel tail)) (List E))
-      )
-    )
-  )
-
- -The second new command, provides a light-weight syntax for datatypes that have only constant constructors, as in: - -
-  (define-enumeration-type Size (small medium large))
-
- -which abbreviates the more verbose - -
-  (define-inductive-types ( (Size ()) )
-    ( ((small Size) (medium Size) (large Size)) )
-  )
-
-

- -
Testers and recursors
- -

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

-  (List::is-nil (→ (! Type :var E :implicit) (List E) Bool))
-  (List::is-cons (→ (! Type :var E :implicit) (List E) Bool))
-
- -as well as the recursor List::reduce defined as if it had been introduced as follows - -
-  (define-fun-rec reduce 
-    ( (A Type :implicit) (B Type :implicit)
-      (b B) (comb (→ A (List A) B B))) (l (List A)) ) B
-    (match l 
-      ( (nil b)
-        ((cons h t) (comb h t (reduce b comb t)))
-      )
-    ) 
-  )
-
-

- -For example, the recursor List::reduce reduces any list l of type (List A) to a value of type B with the aid of a value b of type B for the case where l is empty, and of a function comb that computes the reduction in the non-empty case -from the head h and tail t of l and the (recursively computed) reduction of t. - -A wealth of functions over lists can be defined in terms of List::reduce, including the following: - -
-  (define-const sum ((l (List Int))) Int
-    (List::reduce 0 (lambda ((n Int) (t (List Int)) (s Int)) (+ n s)) l) 
-  )
-  (define-fun len ((A Type :implicit) (l (List A))) Int
-    (List::reduce 0 (lambda ((a A) (t (List A)) (n Int)) (+1 n)) l)
-  )
-  (define-fun append ((A Type :implicit) (l1 (List A))) (l2 (List A)) (List A)
-    (List::reduce l2 (lambda ((a A) (t (List A)) (r (List A))) (cons a r)) l1)
-  )
-  (define-fun reverse ((A Type :implicit) (l (List A))) (List A)
-    (List::reduce (nil A) 
-      (lambda ((a A) (t (List A)) (r (List A))) (append r (cons a (nil A)))) l)
-  )
-  (define-fun filter ((A Type :implicit) (p (-> A Bool)) (l (List A))) (List A)
-    (List::reduce (nil A) 
-      (lambda ((a A) (t (List A)) (r (List A))) (ite (p a) (cons a r) r)) l)
-  )
-  (define-fun map ((A Type :implicit) (B Type :implicit) 
-                   (f (→ A B)) (l (List A))) (List A)
-    (List::reduce (nil A) 
-      (lambda ((a A) (t (List A)) (r (List B))) (ite (p a) (cons a r) r)) l)
-  )
-
-

- - -

External Symbols

- -

When defining new theories there is sometimes the need for two theories -to refer to each other's symbols. -This need cannot be addressed 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 constructors and constants in module can be declared as external with an :extern attribute which connects them to symbols exported by another module. -

- -
-; Example
-(define-module Lists (
-  (declare-datatypes ((List 1))
-    ((nil (→ (! Type :var A) (List A)))
-     (cons (→ (! Type :var A :implicit) 
-              (! A :selector car) (! (List A) :selector cdr)) (List A))
-    )
-  )  
-  ...
- (declare-type Int () :extern Ints::Int)
- (declare-const 0 Int :extern Ints::0)
- (declare-const +1 (→ Int Int) :extern Ints::+1)
- (define-fun len ((A Type :implicit) (l (List A))) Int
-   (List::reduce 0 (lambda ((a A) (t (List A)) (n Int)) (+1 n)) l)
-)
-...
- )
- :types ((→ (! Type E) (List E)))
- :consts ((len (→ (Type :var E :implicit) (List E) Ints::Int)) 
-          ...
-         )
-)
-
- -

Using the :extern attribute, the type Int in the module Lists above is declared to be external and a proxy for Ints::Int. -The constants 0 and +1 are introduced similarly. - -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 (Lists))
-  ; Since Lists::len depends on Ints, it cannot be used here
-  ...
-
- -
-  ; Example 2
-  (import (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.6 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.6 theories, -that is, they have more symbols and richer types but do not change the semantics -of the old ones in any meaningful way. -

- -
- 
-  
-
- (raw file) -
- -
- 

-
- (raw file) -
- -
- 

-
- (raw file) -
- -
- 

-
- (raw file) -
- -
- 

-
- (raw file) -
-
- - -

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 anytime soon. -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) 
- )  
- :types (Bool)
- :consts (
-   (true Bool)
-   (false Bool)
-   (ite (→ (! Type :var A :implicit) Bool A A A))
-   (not (→ Bool Bool))
-   (= (→ (! Type :var A :implicit) A A Bool))
-   (distinct (→ (! Type :var A :implicit) A A Bool))
-   (and (→ Bool Bool Bool))
-   (or (→ Bool Bool Bool))
-   (=> (→ Bool Bool Bool))
-   (xor (→ Bool Bool Bool))
-   ; quantifiers are not exported
- )
- :FOL ; only FOL syntax allowed
-)
-(import (QF_UF))
-(open QF_UF)
-...
-
-The command (set-info :FOL) is a (imperfect) solution of the problem of capturing the Version 2.6 restriction -for terms to be in the applicative fragment -where all function symbols (i.e., non-nullary constants of type (→ τ₁ ⋅⋅⋅ τᵢ)) -are fully applied (i,e., applied to exactly i arguments). - - -

- -Similarly, for the logic LIA (set-logic LIA) would be and abbreviation of -
-(define-module LIA 
- (
-  (import (Core Ints))
-  (open Core)
-  (open Ints)
- )
- :types (Bool Int)
- :consts (
-    (<numeral> Int)
-    (+ (→ Int Int Int))
-    (- (→ Int Int Int))
-    (* (→ (! Int :syntax <int_value>) (! Int :syntax <symbol>) Int)) ; linear mul.
-    (* (→ (! Int :syntax <symbol>) (! Int :syntax <int_value>) Int)) ; linear mul.
-    (> (→ Int Int Bool))
-    (>= (→ Int Int Bool))
-    (< (→ Int Int Bool))
-    (<= (→ Int Int Bool))
-    (true Bool)
-    (false Bool)
-    (ite (→ (! Type :var A :implicit) Bool A A A)) 
-    (not (→ Bool Bool))
-    (= (→ (! Type :var A :implicit) A A Bool))
-    (distinct (→ (! Type :var A :implicit) A A Bool))
-    (and (→ Bool Bool Bool))
-    (or (→ Bool Bool Bool))
-    (=> (→ Bool Bool Bool))
-    (xor (→ Bool Bool Bool))
-    (forall (→ (! Type :var A :implicit) (→ A Bool) Bool))
-    (exists (→ (! Type :var A :implicit) (→ A Bool) Bool))
- )
- :FOL ; only FOL syntax allowed
-) 
-(import (LIA))
-(open LIA)
-
- -Note that the linearity restriction does not need an ad-hoc attribute thanks to the restriction imposed on the type of the multiplication symbol * requiring one of its two arguments to be a concrete integer value. - -

- -
-
- -
-
-
-

- © Copyright The SMT-LIB Initiative
- Based on a design by - Blue Web Templates -

- -
-
-
-
-
- - - -