This paper describes two syntactic extensions to Smt-Lib scripts: lambda-expressions and polymorphism. After extending the syntax to allow these expressions, we show how to update the typing rules of the Smt-Lib to check the validity of these new terms and commands. Since most Smt-solvers only deal with many-sorted rst-order formulas, we detail a monomorphization mechanism to allow to use polymorphism in Smt-Lib syntax while retaining a monomorphic solver core. Dissemination of Smt-solvers requires they are powerful, trustable and open (i.e. easy to interface). The Smt-Lib format [BST10] is an initiative from the Smt community to address the last aspect, by o ering both a common language to describe problems and a command language to interact with the solver. The Smt-Lib format has evolved in the recent years from version 1.2 to version 2.0 to simplify the de nition of the syntax for the part of the language that is responsible for problem descriptions (i.e. declaration of the signature and assertion of logic expressions) on the one hand, and to enrich the commands that allow third-party tools to interact with complying SMT solvers. veriT is an open-source solver jointly developed at INRIA and UFRN. Early versions of the veriT solver implemented several extensions to version 1.2 of the Smt-Lib format: macrode nitions, -expressions and -reduction. A later extension included polymorphic sorts, signatures and assertions. A successful application of these extensions has been to apply SMT solving to verify proof obligations stemming from set-based formalisms (namely, B and Event-B) using standard Smt-Lib logics (AUFLIA) [De10, DFGV12, De13]. The rationale of this application is essentially the following: A set is encoded as its characteristic predicate. For instance, fx 0 as: Set operations are encoded as higher-order functions. For instance, set intersection is encoded as a (polymorphic) macro called inter de ned as: (define fun (par (X) (inter (lambda ((f (X Bool)) (g (X Bool)) (x X)) (and (f x) (g x ))))) , and set membership by the macro named member and de ned as: (define fun (par (X) (member (lambda ((x X) (f (X Bool))) (f x ))))) , in both de nitions, X denotes a type variable, its scope being the de nition itself.
To handle such expressions, veriT implements a processor that performs macro-expansion and -reduction steps as well as type inference. For instance, the formula 0 2 (fx x 0g\fx x 0g) would be encoded as (member 0 (union (lambda (x Int) (>= x 0)) (lambda (x Int) (<= x 0)))), and the result of processing this expression is (and (>= 0 0) (<= 0 0)). In addition, this processor rewrites equalities between lambda expressions as universal quanti cations. Once all steps have been applied, if the goal is not rst-order logic, then veriT emits an error message and halts.
Some of these extensions were included in the Smt-Lib format: polymorphic sorts , though restricted to theory les, and macro-de nition (named function de nitions). In this paper, we thus discuss modi cations to the Smt-Lib format 2.0 corresponding to the extensions to Smt-Lib format 1.2 that were implemented in the solver veriT. It is noteworthy that these modi cations maintain backward compatibility with the existing de nition of the Smt-Lib format. Also we discuss how to rewrite a problem expressed with the proposed extensions to plain Smt-Lib 2.0.
This paper is organized as follows. Sec. 2 presents the extensions made to Smt-Lib, introducing polymorphism at the Smt-Lib script level. This leads to an updated set of typing rules, mainly for Smt-Lib terms, which is discussed in Sec. 3. Using these rules, we detail a strategy to generate a monomorphic version of our target problem in Sec. 4. Finally, we discuss the pros and cons of our solution in the context of related work in Sec. 5 and detail ongoing and further work in Sec. 6. 2
anonymous functions (i.e., -abstractions) and their applications; parametric polymorphism for assertions and function types.
The Smt-Lib already features two avors of polymorphism: parametric polymorphism for sorts and function signatures, but only for background theories; ad-hoc polymorphism because functions can be overloaded.
The extension adds parametric polymorphism to assertions and function de nitions and declarations. The additional introduction of gives a very functional, higher-order, avor to this extended Smt-Lib. The typing rules presented in Sec. 3.1 even allow let-polymorphism inside the Smt-Lib.
However, -abstractions as we envision them will not add much expressiveness as we want to be able to get a rst-order problem only through the application of -reduction. Thus, we will not handle a reduced problem with residual higher-order or partial applications. We see the addition of -abstractions as a convenient mechanism to encode certain problems.
Also, the introduction of polymorphism at the syntactic level does not fundamentally change the expressive power available for Smt-Lib scripts. Indeed, the combination of type schemes to express background theories and overloading of functions permitted by the Smt-Lib standard already covers most functionalities which ML-style let-polymorphism permits. Nonetheless, we argue that polymorphism in scripts is syntactically more convenient than writing every ground instances of the expressions we are interested in.
The next section presents the concrete syntax for the two extensions mentioned above. 2.1
Anonymous functions are terms introduced using lambda, which becomes a keyword. Polymorphic terms reuse the same par keyword as the polymorphic elements of the Smt-Lib theories. The syntactic extensions are summarized in the BNF extract of Fig. 1.
h p a r f u n c t i o n a r g s i : : = par ( hsymboli+ ) hpar commandi : : = ( define fun ( h p a r f u n c t i o n a r g s i ( hsymboli
( h s o r t e d v a r i ) h s o r t i htermi ) ) ) j ( declare fun ( h p a r f u n c t i o n a r g s i ( hsymboli ( h s o r t i ) h s o r t i ) ) ) j ( assert ( h p a r f u n c t i o n a r g s i htermi ) )
Function types are allowed as the return type of functions, due to the inclusion of -term. The choice made is to declare a function type as a list of types. For example the function declaration (declare fun f (Int Int ) Int ) is not the same as the function declaration (declare fun f ((Int Int )) Int ). The former is a function which expects two integers and returns an integer, the latter expects only one argument | a function from integer to integer | and returns an integer. Now, the only possible problem is to distinguish in a sort expression (X Y) between a sort meant to express a function type and a sort which is the application of a sort of arity 1 to its argument, like (Array Int ). This is not a practical problem as sort arity is explicitly stated. Therefore, if the arity of X is greater than 1, we say it is a sort application, otherwise it is a function type. 3
This section details the rules for typing extended Smt-Lib scripts. These rules extend the current set of rules for Smt-Lib1.
Typing polymorphic terms is a necessary step towards uncovering monomorphic ground instances of polymorphic terms. Various type instantiations of the same polymorphic functions will lead in Sec. 4 to the generation of multiple monomorphic versions of the same function. Fortunately, ad-hoc polymorphism through overloading is permitted by the Smt-Lib standard. 3.1
The type of polymorphism we introduce in the extended Smt-Lib is ML-style prenex polymorphism [Pie02]. The typing rules of the system are described in Fig. 3. They can be seen as an adaptation of a Damas-Hindley-Milner [Mil78, Hin69] type system to the Smt-Lib syntax. These rules manipulates Smt-Lib sorts, type variables, tuple types and function types: De nition 1 (Types). Let S be a set of sorts, V be a set of (type) variables. The set of well-formed types T is de ned inductively as follows: 1. if s 2 S, then s 2 T 1Detailed in Section 4.2.2 of the Smt-Lib Standard [BST10] ( set logic AUFLIA ) ( define fun ( par (X) ( empty ( ( e X ) ) Bool f a l s e ) ) ) ( define fun ( par (Y) ( i n s e r t ( ( e Y) ( s (Y Bool ) ) ) (Y Bool )
( lambda ( ( e1 Y ) ) ( or (= e e1 ) ( s e1 ) ) ) ) ) ) ( declare fun ( par ( Z ) ( f l a t ( ( ( Z Bool ) Bool ) ) ( Z Bool ) ) ) ) ( assert (= ( f l a t empty ) empty ) ) ( assert ( par (X) ( f o r a l l ( ( ss ( ( X Bool ) Bool ) ) ) (= ( f l a t ( i n s e r t empty ss ) ) ( f l a t ss ) ) ) ) ) ( assert ( par (X) ( f o r a l l ( ( e X) ( s (X Bool ) ) ( ss ( ( X Bool ) Bool ) ) ) (= ( f l a t ( i n s e r t ( i n s e r t e s ) ss ) )
( i n s e r t e ( f l a t ( i n s e r t s ss ) ) ) ) ) ) ) ( assert ( f o r a l l ( ( s ( I n t Bool ) ) ) (= ( f l a t ( i n s e r t s empty ) ) s ) ) ) ( check sat ) 2. if v 2 V, then v 2 T Notations. Type variables will be denoted by . represent a set of type variables (possibly empty). A type is said to be ground if it has no type variables. A type substitution is a mapping from type variables to types (ground or not). The application of a type substitution is denoted using := and extended to variable sets. Hence T [ := T 0] substitutes in T every member of by a corresponding type in T . A typing environment is a mapping from identi ers to types. Universal quanti cation over type variables is denoted 8T, in order to separate this quanti cation from the universal quanti er ranging over term variable. For terms, x or xi will stand for variables, t or ti will stand for any term.
Typing rules. The rules of Fig. 3 use two additional functions: a function to compute the set of free type variables of a type, denoted fvT ; a generalization function Gen, which helps compute the most general type possible for a let-bound variable. This function is de ned as follows:
Gen(T; ) = 8T(fvT (T )nfvT ( )):T
The rules distinguish between curried functions (! type), where partial application is allowed, and uncurried functions, where the arguments are treated as a tuple, thus disallowing partial application. Curried functions come from explicit -abstractions whereas the Smt-Lib's define fun de ne functions which can only be totally applied.
(x) = 8T :T ` x : T [ := T 0]
Ax8 ; x1 : T1; : : : ; xn : Tn ` t : bool
Q 2 f8; 9g Qua ` Q x1 : : : xnt : bool ` x1 : T1 : : :
` xn : Tn ` x1 : : : xn:t : T1 ! : : : ! Tn ! T ` t : T
Lam ` t1 : T1 : : : ` tn : Tn ` f t1 : : : tn : T ` f : T1 ! : : : Tn ! T
App ` t1 : T1 : : : ` tn : Tn
; x1 : Gen(T1; ); : : : ; xn : Gen(Tn; ) ` t : T ` let ((x1 t1) : : : (xn tn)) t : T
Let ` x as T : T
Axas : : : Tn ! T g; fassert 8T ((8x1 : T1 : : : xn : Tn f x1 : : : xn) = t)g [ Ci fundef h [ ff : 8T :T1 h ; fdeclare-fun 8T (f (T1 : : : Tn) T )g [ Ci fundec : : :
Tn ! T g; Ci h ; fassert 8T tg [ Ci
` t : bool h ; Ci
Assert
The typing system is used in particular to nd monomorphic occurrences of polymorphic terms. In the next section, we will use it in a monomorphization procedure. 4
Once we have checked that a set of commands is well-typed, we need to generate a Smt-Libcompatible version of it, since we do not want to have to change the core of the solver. It means rst that -terms must be eliminated and second, that the problem must be monomorphized. The elimination of -terms has been discussed in Sec. 1 and uses -reduction. Only if the problem is still rst-order after this elimination can we then try to compute a monomorphic version of it. Otherwise we will simply discard it.
Bobot and Paskevich [BP11] have shown the undecidability of computing a minimal monomorphic set formulas equivalent to an original set of polymorphic formulas. However, we still aim to present here a monomorphization method for polymorphic formulas. If needed, it should compute an over-approximation of the minimal monomorphic set. Our implied goal is that we hope monomorphization will be good enough in practice for most of our problems. The proposed monomorphization is expected to be sound with respect to the original polymorphic types. Hence, the unsatis ability of the newly generated problem implies the unsatis ability of the original problem but its satis ability does not in general imply the satis ability of the original problem.
Monomorphization example. Let us detail the example of Fig. 2 to show what we would like to achieve on this speci c case. On this example, monomorphization is expected to fail, so that we can also explain how the procedure works and how we deal with failure. In the example, three function signatures are de ned, where type variables are implicitly universally quanti ed: emptyset: e!B insert: (( i ( i!B))! i!B) flat :( f !B!B! f !B)
The rst step identi es polymorphic and monomorphic instances of terms through typing. In the example, we have three polymorphic formulas. These formulas are detailed below. For the sake of readability, we write type annotations only for co-domains, according to the initial function signatures, and hide annotations for term variables.
ath !Bi(emptyseth !B!Bi) = emptyseth !Bi 8ss : !B!B 8e : ; s : !B; ss : !B!B ( ath !Bi(inserth !B!Bi(inserth !Bi(e; s); ss)) = inserth !Bi(e; ath !Bi(inserth !B!Bi(s; ss)))) ( ath !Bi(inserth !B!Bi(emptyseth !Bi; ss)) = ath !Bi(ss)) (4.1a) (4.1b) (4.1c)
8s : Z!B ( athZ!Bi(inserthZ!B!Bi(s; emptysethZ!B!Bi)) = s) Such monomorphic assertions drive the procedure. Basically, they provide the set of ground types that forms the basis for the generation of monomorphic instances of polymorphic functions.
The second step consists in computing the set of new terms derived from the injection of monomorphic elements. Using type substitutions, we can generate monomorphic specializations F = femptyset[ e:=Z!B]; insert[ i:=Z!B]; at[ f :=Z]g of the polymorphic functions. We try to substitute the polymorphic occurrences of the three terms emptyset, insert, flat by their monomorphic counterpart whenever we can in the polymorphic terms 4.1a, 4.1b and 4.1c, using a leftmost-innermost strategy. This generates the following new set of monomorphic assertions: athZ!Bi(emptysethZ!B!Bi) = emptysethZ!Bi
[ e:=Z] 8ss : Z!B!B 8e : Z; s : Z!B; ss : Z!B!B ( athZ!Bi(inserthZ!B!Bi(insert[hZ!i:=BiZ](e; s); ss)) = insert[hZ!i=BZi](e; athZ!Bi(inserthZ!B!Bi(s; ss)))) ( athZ!Bi(inserthZ!B!Bi(emptyset[hZ!e:=BiZ]; ss)) = athZ!Bi(ss)) (4.2a) (4.2b) (4.2c)
The procedure uses all monomorphic terms, and thus generates a number of new monomorphic assertions. At this point, one full pass of the procedure has been executed. This is repeated while new monomorphic type instances are created. For example, the problem after the rst full pass now has uncovered new possible monomorphizations: emptyset[Z= e] (in 4.2a and 4.2b) and insert[Z= i] (in 4.2c).
The procedure thus stops on a nal problem if it does not uncover any more monomorphic instances. There, only two things can happen: if polymorphic terms are only found in their original place (i.e. as subterms of the original problem) then we have found a monomorphic expression of the original polymorphic problem, if we remove the original polymorphic assertions and functions from the nal problem. if polymorphic terms are still present, then we declare that we have failed to monomorphic expression of the original problem and halt there. nd a
On the example, the procedural steps we have applied will never terminate because in the term (flat emptyset) = emptyset, a new monomorphic type can be inferred for the leftmost emptyset at any instantiation of the rightmost emptyset , which will be fed to the rightmost one, thus looping forever.
Monomorphization xpoint. The proposed monomorphization procedure is now summarized. Let T represent the set of term occurrences of the original problem. Initially, the sets of monomorphic and polymorphic term occurrences are empty.
1. Apply type inference and divide the terms in T into two sets M and P of monomorphic and polymorphic term occurrences. If they are the same as the previous M and P , we have reached a xpoint and can stop. Otherwise, go to step 2. 2. Let M = fm1; m2; : : : mng and P = fp1; p2; : : : pmg. For each (mi; pj ), such that mi 2 M , pj 2 P and mi = pj (i.e. mi and pj are two occurrences of the same term), substitute the polymorphic pj by its monomorphic mi in the term t where pj occurs as subterm, thus deriving a new term tij = t[pj := mi].
At the end of this step, we will have a new set of terms from the various possible pairings between monomorphic and polymorphic occurrences of the same term, generating a new set of term occurrences T 0. Let the new problem be represented by T [ T 0.
Non-termination. The fact that our procedure is possibly non-terminating is mitigated by the fact that, in practice, we impose restrictions on time or in this case, on the number of full passes. However, we would like to be able to guess possibly in nite expansions because we know we will not be able to guarantee a sound and complete monomorphization. To this e ect, we have conjectured the following criterion, which depends on uni cation [Rob65]: Conjecture 1 (Non-termination criterion). Let t and s be terms and s1 and s2 be two occurrences of s in the term t. Let T1 be the type inferred for s1 and T2 the one of s2. If T1 and T2 cannot be uni ed because of a failing occur check then the monomorphization procedure will not terminate. 5
The use of polymorphic logics on top of many-sorted or mono-sorted logics has received speci c attention in the last few years.
In the context of the Caduceus and Why [FM07, BFMP11], Couchot and Lescuyer [CL07] describe how to translate ML-style polymorphic formulas into untyped and multi-sorted versions of the original problem.
This method is re ned by Bobot and Paskevich [BP11] who show a 3-staged treatment of polymorphic formulas to translate them into many-sorted versions, including various possibilities for the last translating step. Their proposals particularly take care of protecting data types which are known to be handled by decision procedures by the targeted Smt-solvers. This work is further detailed in Bobot's thesis [Bob11].
Leino and Rummer [LR10] consider the higher-order polymorphic speci cation language of the Boogie2 tool [Lei08] that has to be translated to Smt-solvers which in general do not handle polymorphism. They present two translations, one using type guards, the other adding types as further function arguments.
These two last approaches already present various advanced techniques to translate polymorphism formulas for many-sorted Smt-solvers, each one coming from their experience and needs, but do not tackle monomorphization. In the case of Bobot and Paskevich, their proof of the undecidability of the monomorphization makes clear the reason why, while Leino and Rummer leave it as a possible further optimization.
Bobot et al. [BCCL08] have added built-in support for polymorphism inside the Alt-Ergo prover [BCC+08]. Supporting polymorphic types at the solver level would indeed simplify the addition of polymorphism at the speci cation level. We chose to keep things separated (for now).
There is also a large body of work on the translation of typed higher-order-logic into untyped rst-order logic. In the context of using automation to help discharge proofs Hurd [Hur03] or Meng and Paulson [MP08] can however rely on the type-checking capabilities of higherorder provers to verify automated but untyped rst-order proofs. Therefore they can even use unsound translations and leave to the higher-order prover the task of checking the soundness of the proof. In order to use Smt-solvers inside Isabelle/HOL [Pau94], the monomorphization step of Blanchette et al. [BBP11] bears a strong similarity to our proposal. 6
We have presented a summary of two backward compatible syntactic extensions made to the Smt-Lib standard: -terms and polymorphism. We have shown how to deal with -terms through -reduction. We also have presented how we attempt to generate a monomorphic version of our polymorphic problem using a xpoint-like procedure. This procedure heavily uses a Damas-Hindley-Milner like type inference algorithm to discover relevant monomorphic instances of polymorphic terms.
The support for the proposed syntactic extensions is currently being implemented in the development version of veriT. -terms are already supported and there is preliminary support for polymorphic Smt-Lib scripts. We are currently testing the monomorphization process to see how it behaves in practice.
The preservation of satis ability means that, even in the case of a non-terminating monomorphization, we could devise a strategy to correctly use an unsatis able result at any step of the monomorphization process. Indeed, this would mean that we have found an unsatis able subset of the initial problem.
This strategy would be similar to depth- rst iterative deepening [Kor85], which has been heavily used in provers based on the tableau method [Smu95, DGHP99]. In tableaux, this is used to generate possible term instantiations for universally quanti ed variables in order to nd a model refuting the original formula. In our case, after each deeper monomorphization step, the Smt-solver would get to try a partial and new monomorphic problem containing only a subset of possible type instantiations. If it can prove the unsatis ability of this new problem, we can stop. If not, we can | and should to preserve completeness | continue. In practice, this iterative procedure will be bounded either by a time limit or by a given number of steps.
We believe this work is a step towards a more generalized use of polymorphism in the context of Smt-solvers. These e orts might converge into an Alt-Ergo-like solution for provers supporting Smt-Lib, indeed building polymorphism support in the prover and not only at the syntactic level.
Acknowledgments. We warmly thank the anonymous reviewers for their helpful feedback and constructive criticism, which already show promises of future fruitful discussions about the subject of this paper. [BBP11]