-We generalize the lemmas on demand de- proposed [10], which uses l -terms similarly to UCLID. cBiosioolnectporrotcoedhuarnedlfeornoanr-rraeycurlosgiviec aansd imnopnle-emxetenntesidonianl This extension provides support for modeling memset, lambda terms. We focus on the implementation aspects memcpy and loop summarizations. However, it does of our new approach and discuss the involved algorithms not make use of native support of l -terms provided aarnrdayosp,tiamrrizaaytioonpseriantimonosreadnedtaSilM.FTu- LrtIhBerv,2wemsahcorwoshaorwe by an SMT solver. Instead, it reduces instances in the represented as lambda terms and lazily handled with theory of arrays with l -terms to a theory combination lemmas on demand. We provide experimental results that supported by solvers such as Boolector [3] (without demonstrate the effect of native lambda support within an SMT solver and give an outlook on future work. native support for l -terms), CVC4, STP [12], and Z3 [6]. In this paper, we generalize the decision procedure I. INTRODUCTION for the theory of arrays with bit vectors as introduced in [3] to lazily handle non-recursive and nonextensional l -terms. We show how arrays, array operations and SMT-LIB v2 macros are represented in Boolector as l -terms and introduce a lemmas on demand procedure for lazily handling l -terms in Boolector in detail. We summarize an experimental evaluation and compare our results to solvers with SMT-LIB v2 macro support (CVC4, MathSAT [5], SONOLAR [13] and Z3) and finally, give an outlook on future work.
The theory of arrays as axiomatized by
McCarthy [
In 2002, Seshia et al. [
This work was funded by the Austrian Science Fund (FWF) under NFN Grant S11408-N23 (RiSE).
We assume the usual notions and terminology of first order logic and are mainly interested in many-sorted languages, where bit vectors of different bit width correspond to different sorts and array sorts correspond to a mapping (ti ) te) from index sort ti to element sort te.
Our approach is focused primarily on the quantifier-free first order theories of fixed size bit vectors, arrays and equality with uninterpreted functions, but not restricted to the above.
We call 0-arity function symbols constant symbols and a, b, i, j, and e denote constants, where a and b are used for array constants, i and j for array indices, and e for an array value. For each bit vector of size n, the equality =n is interpreted as the identity relation over bit vectors of size n. We further interpret the if-then-else bit vector term iten as ite(>;t; e) =n t and ite(?;t; e) =n e.
As a notational convention, the subscript might be
omitted in the following. We identify read and write
as basic operations on array elements, where read(a; i)
denotes the value of array a at index i, and write(a; i; e)
denotes the modified array a overwritten at position i III. l -TERMS IN BOOLECTOR
with value e. The theory of arrays (without
extensionality) is axiomatized by the following axioms, originally In contrast to l -term handling in other SMT solvers
introduced by McCarthy in [
From the theory of equality with uninterpreted func- exactly one bound variable (parameter) and define its tions we primarily focus on the following axiom: representation as l j : t( j). Given an array of sort (ti ) 8x¯; y¯: ^n xi = yi ! f (x¯) = f (y¯) (EUF) te) and its l -term representation l j : t( j), we require i=1 that bound variable j is of sort index ti and term t( j) is The function congruence axiom (EUF) asserts that a of sort element te. Term t( j) is not required to contain function evaluates to the same value for the same j and if it does not contain j, it represents a constant l argument values. term (e.g. l j : 0). In contrast to SMT-LIB v2 macros,
We only consider a non-recursive l -calculus, as- it is not required to represent arrays with curried l
suming the usual notation and terminology, includ- chains, as arrays are accessed at one single index at a
ing the notion of function application, currying and time (cf. read and write operations on arrays).
b -reduction. In general, we denote a l -term lx as We treat array variables as UF with exactly one
l x:t(x), where x is a variable bound by lx and t(x) argument and represent them as fa for array variable a.
is a term in which x may or might not occur. We We interpret read operations as function
applicainterpret t(x) as defining the scope of bound variable tions on either UF or l -terms with read index i as
x. Without loss of generality, the number of bound argument and represent them as read(a; i) fa(i) and
variables per l -term is restricted to exactly one. Func- read(l j : t( j); i) (l j : t( j))(i), respectively.
tions with more than one parameter are transformed We interpret write operations as l -terms
modelinto a chain of nested l -terms by means of currying ing the result of the write operation on array a
(e.g. f (x; y) := x + y is rewritten as l x : l y : x + y). As at index i with value e, and represent them as
a notational convention, we will use lx¯ as a shorthand write(a; i; e) l j : ite(i = j; e; fa( j)). A function
applifor l x0 : : : l xk : t(x0; : : : ; xk) for k 0. We identify the cation on a l -term lw representing a write operation
function application as an explicit operation on l -terms yields value e if j is equal to the modified index
and interpret it as instantiating a bound variable (all i, and the unmodified value fa( j), otherwise. Note
bound variables) of a l -term (a curried l -chain). We that applying b -reduction to a l -term lw yields the
interpret b -reduction as a form of function application, same behaviour described by array axioms A2 and
where all formal parameter variables (bound variables) A3. Consider a function application on lw(k), where
are substituted with their actual parameter terms. We k represents the position to be read from. If k = i
will use lx¯[x0na0; : : : ; xnnan] to indicate b -reduction of (A2), b -reduction yields the written value e, whereas if
a l -term lx¯, where the formal parameters x0; : : : ; xn are k 6= i (A3), b -reduction returns the unmodified value of
substituted with the actual argument terms a0; : : : ; an. array a at position k represented by fa(k). Hence, these
axioms do not need to be explicitly checked during
consistency checking. This is in essence the approach
to handle arrays taken by UCLID [
We interpret if-then-else operations on arrays a and b as l -terms, and represent them as ite(c; a; b) l j : ite(c; fa( j); fb( j)). Condition c yields either function application fa( j) or fb( j), which represent the values of arrays a and b at index j, respectively.
In addition to the base array operations introduced above, l -terms enable us to succinctly model array operations like e.g. memcpy and memset from the standard C library, which we previously were not able to efficiently express by means of read, write and ite operations on arrays. In particular, both memcpy and memset could only be represented by a fixed sequence of read and write operations within a constant index range, such as copying exactly 5 words etc. It was not possible to express a variable range, e.g. copying n words, where n is a symbolic (bit vector) variable.
With l -terms however, we do not require a sequence of array operations as it usually suffices to model a parallel array operation by means of exactly one l -term.
Further, the index range does not have to be fixed and
can therefore be within a variable range. This type of
high level modeling turned out to be useful for
applications in software model checking [
Introducing l -terms does not only enable us to model arrays and array operations, but further provides support for arbitrary functions (macros) by means of currying, with the following restrictions: (1) functions may not be recursive and (2) arguments to functions may not be functions. The first restriction enables keeping the implementation of l -term handling in Boolector as simple as possible, whereas the second restriction limits l -term handling in Boolector to non-higher order functions.
Relaxing these restrictions will turn the considered l calculus to be Turing-complete and in general render the decision problem to be undecidable. As future work it might be interesting to consider some relaxations. lambda 1 2 paryam apply 1 2 args
args vajr
In contrast to treating SMT-LIB v2 macros as C-style macros, i.e., substituting every function application with the instantiated function body, in Boolector, we directly translate SMT-LIB v2 macros into l -terms, which are then handled lazily via lemmas on demand. Formulas are represented as directed acyclic graphs (DAG) of bit vector and array expressions. Further, in this paper, we propose to treat arrays and array operations as l terms and operations on l -terms, which results in an expression graph with no expressions of sort array (ti ) te). Instead, we introduce the following four additional expression types of sort bit vector: a param expression serves as a placeholder variable for a variable bound by a l -term a lambda expression binds exactly one param expression, which may occur in a bit vector expression that represents the body of the l -term an args expression is a list of function arguments an apply expression represents a function application that applies arguments args to a lambda expression
Example 1: Consider y1 f (i) = f ( j) ^ i 6= j with functions f (x) := ite(x < 0; g(x); x), g(y) := y as depicted in Fig. 1. Both functions are represented as l terms, where function g(y) returns the negation of y and is used in function f (x), which computes the absolute value of x. Dotted nodes indicate parameterized expressions, i.e., expressions that depend on param expressions, and serve as templates that are instantiated as soon as b -reduction is applied.
In order to lazily evaluate l -terms in Boolector we implemented two b -reduction approaches, which we will discuss in the next section in more detail.
2 apply 1 2 lambda apply 1 1 2 args vear our SMT solver Boolector. We focus on reduction algorithms for the non-recursive l -calculus, which is rather atypical for the (vast) literature on l -calculus. In the context of Boolector, we distinguish between full and partial b -reduction. They mainly differ in their application and the depth up to which l -terms are expanded. In essence, given a function application lx¯(a0; : : : ; an) partial b -reduction reduces only the topmost l -term lx¯, whereas full b -reduction reduces lx¯ and every l -term in the scope of lx¯.
Full b -reduction of a function application on l -term lx¯ consists of a series of b -reductions, where l -term lx¯ and every l -term ly¯ within the scope of lx¯ are instantiated, substituting all formal parameters with actual parameter terms. Since we do not allow partial function applications, full b -reduction guarantees to yield a term which is free of l -terms. Given a formula with l -terms, we usually employ full b -reduction in order to eliminate all l -terms by substituting every function application with the term obtained by applying full b -reduction on that function application. In the worst case, full b reduction results in an exponential blow-up. However, in practice, it is often beneficial to employ full b reduction, since it usually leads to significant simplifications through rewriting. In Boolector, we incorporate this method as an optional rewriting step. We will use lx¯[x0na0; : : : ; xnnan]f as a shorthand for applying full b -reduction to lx¯ with arguments a0; : : : ; an.
Partial b -reduction of a l -term lx¯, on the other hand, essentially works in the same way as what is referred to as b -reduction in the l -calculus. Given a function application lx¯(a0; : : : ; an), partial b -reduction substitutes formal parameters x0; : : : ; xn with the actual argument terms a0; : : : ; an without applying b -reduction to other l -terms within the scope of lx¯. This has the effect that l -terms are expanded function-wise, which we require for consistency checking. In the following, we use lx¯[x0na0; : : : ; xnnan]p to denote the application of partial b -reduction to lx¯ with arguments a0; : : : ; an.
Given a function application lx¯(a0; : : : ; an) and a DAG representation of lx¯. Full b -reduction of lx¯ consecutively substitutes formal parameters with actual argument terms while traversing and rebuilding the DAG in depth-first-search (DFS) post-order as follows. 1) Initially, we instantiate lx¯ by assigning arguments a0; : : : ; an to the formal parameters x0; : : : ; xn. 2) While traversing down, for any l -term ly¯ in the scope of lx¯, we need special handling for each function application ly¯(b0; : : : ; bm) as follows. args 1 2 var k valr args 1 2
vajr eq 1 2 vair 1 a2nd eq 2 1 1 2 1 mul 2 1 ult eq mul 1 eq 2 mul
2 2 1 2 1 vajr vair const valr vkar (b) Formula y20 after full b -reduction of y2.
vear Fig. 2: Full b -reduction of formula y2. a) Visit arguments b0; : : : ; bm first, and obtain rebuilt arguments b00; : : : ; b0m. b) Assign rebuilt arguments b00; : : : ; b0m to ly¯ and apply b -reduction to ly¯(b00; : : : ; b0m).
This ensures a bottom-up construction of the b reduced DAG (see step 3.), since all arguments b00; : : : ; b0m passed to a l -term ly¯ are b -reduced and rebuilt prior to applying b -reduction to ly¯. 3) During up-traversal of the DAG we rebuild all visited expressions bottom-up and require special handling for the following expressions: param: substitute param expression yi with current instantiation b0
i apply: substitute expression ly¯(b0; : : : ; bm) with ly¯[y0nb00; : : : ; ymnb0m]f We further employ following optimizations to improve the performance of the full b -reduction algorithm.
Given an expression e within the scope of a l -term lx¯. If e is not parameterized and does not contain any l -term, e is not dependent on arguments passed to lx¯ and may therefore be skipped. l -scope caching We cache rebuilt expressions in a l -scope to prevent rebuilding parameterized expressions several times.
Example 2: Given a formula y2 f (i; j) = f (k; l) and two functions g(x) := ite(x = i; e; 2 x) and f (x; y) := ite(y < x; g(x); g(y)) as depicted in Fig. 2a. Applying full b -reduction to formula y2 yields formula y 20 as illustrated in Fig. 2b. Function application f (i; j) has been reduced to ite( j i ^ i 6= j; 2 j; e) and f (k; l) to ite(l < k; ite(k = i; e; 2 k); ite(l = i; e; 2 l)).
Given a function application lx¯(a0; : : : ; an) and a DAG representation of lx¯. The scope of a partial b reduction bp(lx¯) is defined as the sub-DAG obtained by cutting off all l -terms in the scope of lx¯. Assume that we have an assignment for arguments a0; : : : ; an, and for all non-parameterized expressions in the scope of bp(lx¯). The partial b -reduction algorithm substitutes param expressions x0; : : : ; xn with a0; : : : ; an and rebuilds lx¯. Similar to full b -reduction, we perform a DFS post-order traversal of the DAG as follows. 1) Initially, we instantiate lx¯ by assigning arguments a0; : : : ; an to the formal parameters x0; : : : ; xn. 2) While traversing down the DAG, we require special handling for the following expressions: function applications ly¯(b0; : : : ; bm) a) Visit arguments b0; : : : ; bm, obtain rebuilt arguments b00; : : : ; b0m. b) Do not assign rebuilt arguments b00; : : : ; b0m to ly¯ and stop down-traversal at ly¯. ite(c; t1; t2) Since we have an assignment for all nonparameterized expressions within the scope of bp(lx¯), we are able to evaluate condition c. Based on that we either select t1 or t2 to further traverse down (the other branch is omitted). 3) During up-traversal of the DAG we rebuild all visited expressions bottom-up and require special handling for the following expressions: param: substitute param expression yi with current instantiation b0i args valr
apply 2
1 if-then-else: substitute expression ite(c; t1; t2) with t1 if c = >, and t2 otherwise
For partial b -reduction, we have to modify the first of the two optimizations introduced for full b -reduction.
Given an expression e in the scope of partial b reduction bp(lx¯). If e is not parameterized, in the context of partial b -reduction, e is not dependent on arguments passed to lx¯ and may be skipped.
Example 3: Consider y2 from Ex. 2. Applying partial b -reduction to y2 yields the formula depicted in Fig. 3, where function application f (i; j) has been reduced to ite( j < i; e; g( j)) and f (k; l) to ite(l < k; g(k); g(l)).
The idea of lemmas on demand goes back to [
In this section, we introduce lemmas on demand for
non-recursive l -terms based on the algorithm
introduced in [
Example 4: Consider formula y1 from Ex. 1, which has two roots. The abstraction function al performs a consecutive down-traversal of the DAG from both roots.
The resulting abstraction is a mapping of all bit vector terms encountered during traversal, according to the rules 1-3 above. For function applications (e.g. applyi) fresh bit vector variables (e.g. al (applyi)) are introduced, where the remaining sub-DAGs are therefore cut off. The resulting abstraction al (y1) is given in Fig. 5. its satisfiability by means of a SAT solver. As G is an over-approximation of f , we immediately conclude with unsatisfiable if G is unsatisfiable. If G is satisfiable, we have to check if the current satisfying assignment s (as provided by procedure DPB) is consistent w.r.t. preprocessed formula p. If s is consistent, i.e., if it can be extended to a valid satisfying assignment for the preprocessed formula p, we immediately conclude with satisfiable. Otherwise, assignment s is spurious, consistentl (p; s ) identifies a violation of the function congruence axiom EUF, and we generate a symbolic lemma lemmal (p; s ) which is added to formula refinement x in its abstracted form al (lemmal (p; s )).
Note that in f , in contrast to the decision procedure
introduced in [
In this section, we introduce a consistency checking
algorithm consistentl as a generalization of the
consistency checking approach presented in [
VI. FORMULA ABSTRACTION function application in p, we have to check both if
In this section, we introduce a partial formula ab- the assignment of the corresponding abstraction
varistraction function al as a generalization of the ab- able is consistent with the value obtained by applying
straction approach presented in [
to a fresh bit vector variable. In order to check axiom EUF, for each l -term and UF 3) Each bit vector term t(y0; : : : ; ym) is mapped to symbol we maintain a hash table r, which maps l t(al (y0); : : : ; al (ym)). terms and UF symbols to function applications. We Note that by introducing fresh variables for function check consistency w.r.t. p by applying the following applications, we essentially cut off l -terms and UF rules. and therefore yield a pure bit vector skeleton, which I: For each f (a¯), if a¯ is not parameterized, is subsequently eagerly encoded to SAT. add f (a¯) to r( f ) C: For any pair s := g(a¯); t := h(b¯) 2 r( f ) check n ^ s (al (ai)) = s (al (bi)) ! s (al (s)) = s (al (t)) i=0 B: For any s := ly¯(a0; : : : ; an) 2 r(lx¯) with t := lx¯[x0na0; : : : ; xnnan]p, check rule P, if P fails, check eval(t) = s (al (s)) P: For any s := ly¯(a0; : : : ; an) 2 r(lx¯) with t := g(b0; : : : ; bm) = lx¯[x0na0; : : : ; xnnan]p,
n if n = m ^ ^ ai = bi, propagate s to r(g)
i=0
Given a l -term (UF symbol) f and a corresponding hash table r( f ). Rule I, the initialization rule, initializes r( f ) with all non-parameterized function applications on f . Rule C corresponds to the function congruence axiom and is applied whenever we add a function application g(a0; : : : ; an) to r( f ). Rule B is a consistency check w.r.t. the current assignment s , i.e., for every function application s in r( f ), we check if the assignment of s (al (s)) corresponds to the assignment evaluated by the partially b -reduced term lx¯[x0na0; : : : ; xnnan]p. Finally, rule P represents a crucial optimization of consistentl , as it avoids unnecessary conflicts while checking B. If P applies, both function applications s and t have the same arguments.
As function application s 2 r(lx¯), rule C implies that s = lx¯(a0; : : : ; an). Therefore, function applications s and t must produce the same function value as t := lx¯[x0na0; : : : ; xnnan]p = ly¯[x0na0; : : : ; xnnan]p, i.e., function application t must be equal to the result of applying partial b -reduction to function application s.
Assume we encode t and add it to the formula. If DPB guesses an assignment s.t. s (al (t)) 6= s (al (s)) holds, we have a conflict and need to add a lemma. However, this conflict is unnecessary, as we know from the start that both function applications must map to the same function value in order to be consistent. We avoid this conflict by propagating s to r(g).
Figure 6 illustrates our consistency checking algorithm consistentl , which takes the preprocessed input formula p and a current assignment s as arguments, and proceeds as follows. First, we initialize stack S with all non-parameterized function applications in formula p (cf. nonparam_apps(p)) and order them top-down, according to their appearance in the DAG representation of p. The top-most function application then represents the top of stack S, which consists of tuples (g; f (a0; : : : ; an)), where f and g are initially equal and f (a0; : : : ; an) denotes the function application propagated to function g. In the main consistency checking procedure consistentl (p; s )
S nonparam_apps ( p ) w h i l(eg;Sf6 =(a00/; : : : ; an)) pop ( S ) encode ( f (a0; : : : ; an) ) / c h e c k r u l e C / i f not congruent ( g; f (a0; : : : ; an) )
r e t u r n ? add ( f (a0; : : : ; an); r(g) ) i f is_UF ( g ) c o n t i n u e encode ( g ) / c h e c k r u l e B / t g[x0na0; : : : ; xnnan]p i f assigned ( t )
i f s (t) 6= s (al ( f (a0; : : : ; an))) e l i f t = hr(ae0t;u: :r:n; an?) / c h e c k r u l e P / push ( S; (h; f (a0; : : : ; an)) ) c o n t i n u e e l s e apps f resh apps(t) f o r a 2 apps
encode ( a ) i f eval ( t ) 6= s (al ( f (a0; : : : ; an)))
r e t u r n ? f o r h(b0; : : : ; bm) 2 apps
push ( S; (h; h(b0; : : : ; bm)) ) r e t u r n >
Fig. 6: Procedure consistentl in pseudo-code. loop, we check rules C and B for each tuple as follows.
First we check if f (a0; : : : ; an) violates the function congruence axiom EUF w.r.t. function g and return ? if this is the case. Note that for checking rule C, we require an assignment for arguments a0; : : : ; an, hence we encode them on-the-fly. If rule C is not violated and function f is an uninterpreted function, we continue to check the next tuple on stack S. However, if f is a l -term we still need to check rule B, i.e., we need to check if the assignment s (al ( f (a0; : : : ; an))) is consistent with the value produced by g[x0na0; : : : ; xnnan]p. Therefore, we first encode all non-parameterized expressions in the scope of partial b -reduction bp(g) (cf. encode(g)) before applying partial b -reduction with arguments a0; : : : ; an, which yields term t. If term t has an assignment, we can immediately check if it differs from assignment s (al ( f (a0; : : : ; an))) and return ? if this is the case. However, if term t does not have an assignment, which is the case when t has been instantiated from a parameterized expression, we have to compute the value for term t. Note that we could also encode term t to get an assignment s (t), but this might add a considerable amount of superfluous clauses to the SAT solver. Before computing a value for t we check if rule P applies and propagate f (a0; : : : ; an) to h if applicable.
Otherwise, we need to compute a value for t and check if t contains any function applications that were instantiated and not yet encoded (cf. fresh_apps(t)) and encode them if necessary. Finally, we compute the value for t (cf. eval(t)) and compare it to the we run DPB on al (y1) and it returns a satisfying assignment of al ( f (a0; : : : ; an)). If the values differ, assignment s such that s (i) 6= s ( j), s (ai) = s (a j), we found an inconsistency and return ?. Otherwise, s (i) < 0 and s (ai) 6= s ( i). First, we check conwe continue consistency checking the newly encoded sistency for lx(i) and check rule C, which is not function applications apps. We conclude with >, if all rvuiolelaBte.dWase sap(pi)ly6=psar(tija)l, ban-rdedcuocnttiionnueanwditohbtcahinectkeirnmg function applications have been checked successfully t := lx[x=i]p = ly(i) (since s (i) < 0) for which rule P and no inconsistencies have been found. is applicable. We propagate lx(i) to ly, check if lx(i) is consistent w.r.t. ly, apply partial b -reduction, obtain A. Lemma generation t := ly[y=i]p = i and find an inconsistency according
Following [
path ps (pt ) that were ? under given assignment s .
We generate the following (in general symbolic) lemma: j k ^ cis ^ ^ i=0 i=0
l m :cis ^ ^ cti ^ ^ i=0 i=0
n :cti ^ ^ ai = bi ! s = t
i=0
Assume that rule B was violated by a function application s := ly¯(a0; : : : ; an) 2 r(lx¯). We obtained t := lx¯[x0na0; : : : ; xnnan]p and collect all conditions that lead to the conflict as follows. 1) Collect ite conditions cs0; : : : ; csj and cs0; : : : ; csk for s
as in steps 1-3 above. 2) Collect all ite conditions ct0; : : : ; ctl that evaluated to > under current assignment s when partially b reducing lx¯ to obtain t. 3) Collect all ite conditions ct0; : : : ; ctm that evaluated to ? under current assignment s when partially b reducing lx¯ to obtain t.
We generate the following (in general symbolic) lemma: j
k ^ cis ^ ^ i=0 i=0
l m :cis ^ ^ cti ^ ^ :cti ! s = t
i=0 i=0
Example 5: Consider formula y1 and its preprocessed formula abstraction al (y1) from Ex. 1. For the sake of better readability, we will use lx and ly to denote functions f and g, and further use ai and a j as a shorthand for al (applyi) and al (applyj). Assume
We applied our lemmas on demand approach for l -terms on three different benchmark categories: (1) crafted, (2) SMT’12, and (3) application. For the crafted category, we generated benchmarks using SMT-LIB v2 macros, where the instances of the first benchmark set (macro blow-up) tend to blow up in formula size if SMT-LIB v2 macros are treated as C-style macros.
UNSAT encode an incorrect and correct but naive
implementation of the Fisher-Yates shuffle algorithm [
We performed all experiments on 2.83GHz Intel Core
2 Quad machines with 8GB of memory running Ubuntu
12.04.2 setting a memory limit of 7GB and a time limit
for the crafted and the SMT’12 benchmarks of 1200
seconds. For the application benchmarks, as in [
1http://llbmc.org/files/downloads/vstte-2013.tgz ’12 BBoooolleeccttoorrnop T Boolectorb SM Boolectorsc12 l-bopuw CBBBoooVoooCllleee4ccctttooorrrnbop rcao SMOaNthOSALTAR m Z3
Boolector tse BBoooolleeccttoorrnbop -raeyh STA CVC4 sfi SMOaNthOSALTAR
Z3
Boolector s Boolectornop t-eay STA BCoVoCle4ctorb r seh UN SMOaNthOSALTAR fi
Z3
mark set is SONOLAR. However, it is not clear how SONOLAR handles SMT-LIB v2 macros. Surprisingly, on these benchmarks Boolectornop performs better than Boolector with optimization rule P, which needs further investigation. On the fisher-yates SAT benchmarks Boolector not only solves the most instances, but requires 107 seconds for the first 6 instances, for which Boolectorb , MathSAT and Z3 need more than 300 seconds each. Boolectornop does not perform as well as Boolector due to the fact that on these benchmarks optimization rule P is heavily applied. In fact, on these benchmarks, rule P applies to approx. 90% of all propagated function applications on average. On the fisheryates UNSAT benchmarks Z3 and Boolectorb solve the most instances, whereas Boolector and Boolectornop do not perform so well. This is mostly due to the fact that these benchmarks can be simplified significantly when macros are eagerly eliminated, whereas partial b -reduction does not yield as much simplifications.
We measured overhead of b -reduction in Boolector on these benchmarks and it turned out that for the macro blow-up and fisher-yates UNSAT instances the overhead is negligible (max. 3% of total run time), whereas for the fisher-yates SAT instances b -reduction requires over 50% of total run time. we used a time limit of 60 seconds. We evaluated four different versions of Boolector: (1) our lemmas on demand for l -terms approach DPl (Boolector), (2) DPl without optimization rule P (Boolectornop), (3) DPl with full b -reduction (Boolectorb ), and (4) the version submitted to the SMT competition 2012 (Boolectorsc12). For comparison we used the following SMT solvers: CVC4 1.2, MathSAT 5.2.6, SONOLAR 2013-05-15, STP 1673 (svn revision), and Z3 4.3.1.
Note that we limited the set of solvers to those which currently support SMT-LIB v2 macros and the theory of fixed-size bit vectors. As a consequence, we did not compare our approach to UCLID (no bit vector support) and Yices, which both have native l -term support, but Table II summarizes the results of running all lack support for the SMT-LIB v2 standard. four Boolector versions on the SMT’12 benchmark
As indicated in Tables I, II and III, we measured the set. We compared our three approaches Boolector, number of solved instances (Solved), timeouts (TO), Boolectornop, and Boolectorb to Boolectorsc12, which memory outs (MO), total CPU time (Time), and total won the QF AUFBV track in the SMT competition memory consumption (Space) required by each solver 2012. In comparison to Boolectorb , Boolector solves 5 for solving an instance. If a solver ran into a timeout, unique instances, whereas Boolectorb solves 3 unique 1200 seconds (60 seconds for category application) instances. In comparison to Boolectorsc12, both solvers were added to the total time as a penalty. In case of a combined solve 2 unique instances. Overall, on the memory out, 1200 seconds (60 seconds for application) SMT’12 benchmarks Boolectorsc12 still outperforms and 7GB were added to the total CPU time and total the other approaches. However, our results still look memory consumption, respectively. promising since none of the approaches Boolector,
Table I summarizes the results of the crafted bench- Boolectornop and Boolectorb are heavily optimized yet.
mark category. On the macro blow-up benchmarks, On these benchmarks, the overhead of b -reduction in
Boolector and Boolectornop benefit from lazy l -term Boolector is around 7% of the total run time.
handling and thus, outperform all those solvers which Finally, Table III summarizes the results of the
applitry to eagerly eliminate SMT-LIB v2 macros with a cation category. We used the benchmarks obtained from
very high memory consumption as a result. The only the instantiation-based reduction approach presented
solver not having memory problems on this bench- in [
Boolector a Boolectornop bd Boolectorb am Boolectorsc12 l
STP
new approaches to STP, the same version of the solver
that outperformed all other solvers on these benchmarks
in the experimental evaluation of [
Boolectorsc12 and STP do not support l -terms as arrays and therefore were not able to participate on this benchmark set. By exploiting the native l -term support for arrays in Boolectorb , in comparison to the instantiation benchmarks we achieve even better results. Note that on the lambda (instantiation) benchmarks, the overhead in Boolectorb for applying full b -reduction was around 15% (less than 2%) of the total run time.
Benchmarks, binaries of Boolector and all log files of our experiments can be found at: http://fmv.jku.at/
In this paper, we introduced a new decision procedure
for handling non-recursive and non-extensional l -terms
as a generalization of the array decision procedure
presented in [
In future work we will address the performance bottleneck of the b -reduction implementation and will further add l -term specific rewriting rules. We will analyze the impact of various b -reduction strategies on our lemmas on demand procedure and will further add support for extensionality over l -terms. Finally, with the recent and ongoing discussion within the SMT-LIB community to add support for recursive functions, we consider extending our approach to recursive l -terms.
We would like to thank Stephan Falke, Florian Merz Duterte for explaining the implementation and limits of lambdas in SMT solvers, and more specifically in