metaSMT: Focus On Your Application Not On Solver Integration Finn Haedicke Stefan Frehse Görschwin Fey Daniel Große Rolf Drechsler Institute of Computer Science University of Bremen, 28359 Bremen, Germany {finn,sfrehse,fey,grosse,drechsle}@informatik.uni-bremen.de Abstract—Decision procedures are used as core tech- check for satisfiability. Furthermore, advanced features nique in many applications today. In this context, auto- are available, e.g., computing interpolants which are mated reasoning based on Satisfiability Modulo Theories utilized in SAT-based Model Checking [2]. Moreover (SMT) is very effective. However, developers have to decidelearnt information generated while reasoning can be which concrete engine to use and how to integrate the reused very efficiently in consecutive reasoning processes engine into the application. Even if file formats like SMT- LIB standardize the input of many engines, advanced to prune the search space [12]. Usually this can only be features remain unused and the integration of the engine done by calling native functions which access the learnt is left to the programmer. information. This work presents metaSMT, a framework that inte- This work presents metaSMT a publicly available, easy grates advanced reasoning engines into the program code to use and powerful tool1 which provides an integration of the respective application. metaSMT provides an easy to of the native Application Programming Interface (API) of use language that allows engine independent programming modern reasoning engines into C++ code. The advantages while gaining from high performance reasoning engines. of metaSMT are: (1) engine independence through effi- State-of-the-art solvers for satisfiability and other theo- ries are available for the user via metaSMT with minimal cient abstraction layers (2) simple use of various decision programming effort. For two examples we show how procedures (3) extensibility in terms of input language metaSMT is used in current research projects. and reasoning engines (4) customizability in terms of optimization and infrastructure (5) translation of the input I. I NTRODUCTION language into native engine calls at compile time. In recent years, formal methods have become attractive The remaining work is structured as follows: Section II to solve complex computational hard problems. Decision gives a basic introduction into SMT and the programming procedures are applied in many applications, like e.g., methods used in metaSMT. Afterwards an example Model Checking [1], [2], Synthesis [3], [4] and, Automatic of a metaSMT-based application is given before in Test Pattern Generation (ATPG) [5]. Section IV the architecture of metaSMT is described. Despite the successful research and application of Section V describes how this architecture is implemented decision procedures, the increasing complexity of soft- in metaSMT and Section VI gives an empirical evaluation ware and hardware systems demands for more effective of metaSMT including its use in current research projects. reasoning engines to overcome complexity issues. In The work closes with conclusions. the last years, solvers for Satisfiability Modulo Theo- II. P RELIMINARIES ries (SMT) have been developed. Different theories are combined to formulate the problem. Various works gave This section provides background information. How- empirical evidence that SMT reasoning engines increase ever, basic knowledge of C++ is assumed. the efficiency of formal methods [6], [7], [8]. A. Satisfiability Modulo Theories The performance of SMT reasoning engines remains an active research topic. Annual SMT competitions [9], [10] Boolean satisfiability is a decision problem, also known show their advances. However, SMT reasoning engines as the SAT problem. The problem asks whether there have different strengths on different problem instances. exists an assignment of Boolean variables such that the Therefore, evaluating different engines with respect to a Boolean function evaluates to true. The problem has given problem instance allows to find the best performing been proven NP-complete [13]. In spite of the huge engine. complexity of the problem, sophisticated algorithms When using SMT in a concrete algorithm, the most and clever heuristics help to solve instances with many common way is to generate a problem instance in thousands variables and clauses very efficiently. Usually, SMT-LIB format [11]. Taking a user created SMT- SAT solvers work on a Conjunctive Normal Form (CNF) LIB file as input, an SMT solver decides whether the of a Boolean function that is a disjunction of conjunctions instance is satisfiable or unsatisfiable. However, many of literals, where each literal is variable or its negation. solvers additionally have custom native interfaces. These Satisfiability Modulo Theories is also a decision interfaces are used to pass the instance to the engine and problem but with more complex theories rather than only propositional logic. A detailed introduction is given This work was supported in part by the German Federal Ministry 1 of Education and Research (BMBF) within the project SANITAS Available online at http://www.informatik.uni-bremen.de/agra/eng/ under contract no. 01M3088. metasmt.php Listing 1. SMT instance for a · b = 21466342967 B. Boost.Proto (benchmark factorization.smt The Boost project [16] is a collection of libraries that :logic QF_BV :extrafuns ((a BitVec[32])) cover many features not included in the C++ standard :extrafuns ((b BitVec[32])) library. In particular, Boost.Proto [17] provides tools to integrate Domain Specific Embedded Languages (DSEL) :assumption (not (= a bv1[32])) into C++. Given a programming language, a DSEL in :assumption (not (= b bv1[32])) that language is dedicated to a domain, e.g., parsing [18] :formula (= or vector arithmetic [19]. The DSEL provides a syntax bv21466342967[64] designed for this domain and, therefore, is easier to handle (bvmul (zero_extend[32] a) than the original language. Due to space constraints an (zero_extend[32] b) in-depth description of Boost.Proto is omitted, the reader )) is referred to the Boost documentation. ) Technically, this work uses Boost.Proto to implement a domain specific language for SMT logics in metaSMT. in [14]. Already available SMT-solvers handle complex formulas. In addition to the logics the SMT-LIB standard III. M OTIVATING E XAMPLE also specifies a textual format that is commonly used for Before the subsequent sections give a complete descrip- input files of the solvers. Listing 1 shows an example of tion of metaSMT this section demonstrates how metaSMT such an SMT file: Two variables, a, b are declared as bit- is used in a complete example application. vectors and constrained to be the two factors of a product The usual integration of reasoning engines iteratively resulting in the 64 bit number 21, 466, 342, 967. When calls API functions to construct the problem instance. called with this input, an SMT-QF BV solver outputs However, this reduces the readability of the source code satisfiable and e.g., the assignment a = 740, 218, 723 and and makes it difficult to understand the program. A typical b = 29. example can be constructed using the Boolector API for Moreover, in addition to the SMT-LIB format many the C programming language. Figure 1 (a) shows the solvers provide an Application Programming Inter- code to construct the simple constraint c = a · b using the face (API) that exposes features like incremental solving, Boolector C API (not including memory management). where the SMT instance can be changed after the The same expression, written quite concise in the SMT- satisfiability check. Learnt information about the instance LIB format is shown in Figure 1 (b). The goal of metaSMT is kept and reused. Consequently, using the API may is to allow this compact syntax to be used in C++ increase the overall performance. programs. Due to the limitations of C++ this requires adaptions. Most notably, the expressions cannot easily be An SMT solver can be utilized within an application in written in a symbolic expression (S-expression) syntax as different ways. Each of the following options has certain in the SMT-LIB format, where each function is enclosed advantages and disadvantages: in parenthesis. The syntax for calling functions is used 1) Generate an instance file according to SMT-LIB spec- instead. Moreover, the solver is passed into the expression ification and call the solver. Different SMT solvers using the context e.g., as btor_ctx in Figure 1 (c). can easily be evaluated. However, the instance In order to illustrate the programming interface of generation and result retrieval requires handling of metaSMT an example written in C++ code is presented files and text within the application. in Listing 2. The listing shows the factorization of an 2) Use the solver specific API to call an SMT solver’s integer into two integers. More precisely, given an integer functions directly. In particular, incremental satis- in bit-vector representation ~c ∈ B2n , compute two integers fiability can be exploited. But the application is ~a, ~b ∈ Bn , such that ~a · ~b = ~c. To enforce non-trivial restricted to a specific solver. factorization, both integers a and b may not be 1. As 3) Introduce an abstraction layer specific to the appli- the bit-vectors ~a and ~b are zero-extended, no overflows cation. This technique combines high performance are possible and as a result a valid assignment to the using incremental satisfiability with the ability to constraint either gives a valid factorization of ~c or proves evaluate different solvers. However a custom layer that it is prime. The integer value of ~c is randomly is not portable to different applications. chosen and changed in each iteration of a loop for 10,000 iterations. A similar example is reconsidered in This work separates the programming model from the empirical evaluation. the reasoning engine. With metaSMT the application The first line in Listing 2 defines the solver context, specifies the instance in a simple, common notation. Many which is not explained here but described later in this reasoning engines are available without modifications of work. The context specifies which reasoning engine to use the algorithm. and how the input is handled by metaSMT. The next line The Java package jSMTLIB [15] provides an interface is a user parameter, which defines the bit-vector width of for the usage of different SMT solvers. The package reads, the operands. The algorithm is therefore scalable to an checks and generates SMT-LIB files and executes the abitrary bit-width. In lines 4-6 the bit-vectors a, b and respective SMT-solver executables. However, jSMTLIB c are declared and initialized. currently does not provide an embedded language for Lines 8 and 9 constrain the operands to be different instance generation directly from the application. from 1 in bit-vector representation. In line 11 the boolector_assume( btor, :assumption assumption( btor_ctx, boolector_eq(btor, c, (= c (bvmul a b)) equal(c, bvmul(a, b)) ) boolector_mult(btor, a, b) )) (a) Boolector API calls (b) SMT-Lib format (c) metaSMT C++ Code Fig. 1. Examples for c = a · b Listing 2. metaSMT factorization and prime test F RONTEND (C++) 1 Context ctx; QF BV Core Array 2 const unsigned width = ; 3 4 bitvector a = new_bitvector(width); 5 bitvector b = new_bitvector(width); 6 bitvector c = new_bitvector(width); M IDDLE - END 7 8 assertion(ctx, nequal(a, bvuint(1,width)) ); 9 assertion(ctx, nequal(b, bvuint(1,width)) ); DirectSolver BitBlast GraphSolver 10 11 assertion( ctx, equal( zero_extend(width, c) SAT Clause SAT Aiger Groups , bvmul( zero_extend(width, a), zero_extend(width, b)) )); 12 13 for (unsigned i=0; i < 10000; ++i) { 14 unsigned r = random_number ( 2, 2ˆwidth - BACKEND 1 ); 15 assumption( ctx, equal(c, bvuint(r, 2* SWORD Z3 MiniSAT CUDD width)) ); 16 17 if( solve( ctx ) ) { Boolector PicoSAT AIGER 18 unsigned a_value = read_value( ctx, a ); 19 unsigned b_value = read_value( ctx, b ); 20 21 printf("factorized %d into %d * %d\n", r Solver API , a_value, b_value); 22 } else { 23 printf("%d is prime.", r); Fig. 2. metaSMT layer Architecture 24 } 25 } the input languages, defined in the SMT-LIB format (e.g., Core Boolean logic, QF BV). The middle-end multiplication ~a · ~b = ~c is constrained. However the layer provides translations, intermediate representation multiplication is done in double width to avoid overflows. and optimizations of the input expressions. Optionally, These constraints are identical for each iteration of expressions can directly be passed to the the backend the loop starting in line 13, therefore they are declared layer where the solvers are integrated via their native API. outside the loop as an assertion, which is permanent. Various configurations of middle-ends with backends are Inside the loop, in lines 14-15 c is set equal to a random possible. The frontends allow to combine each translation number from 2 to 2width − 1 using an assumption, middle-end with any compatible backend. However, not which is only valid for the next satisfiability check of the every backend supports every logic. Therefore, some solver, i.e., for one loop iteration. middle-ends supply emulation or translations to other After setting up the SMT instance, the satisfiability logics, e.g, a bit-vector expression can be translated into check is performed in line 17. If the instance is sat- a set of Boolean expressions. isfiable, the values of a and b are determined using The frontends are independent from the underlying read_value. Both operands are printed out in line 21. two layers and have no semantics attached. To evaluate Otherwise the instance is unsatisfiable, the else branch frontend expressions, a context is used that defines their is executed, which outputs c is prime. meaning. The context is the combination of at least one middle-end and one backend, where the middle-end IV. A RCHITECTURE defines how the input language is mapped to function In the following sections the architecture of metaSMT calls of the backend. is described. At first the basic layers are introduced. Then B. Frontends each layer is described in detail. The terms frontend for the input languages, middle-end for the intermediate layer The frontends define the input languages for metaSMT. and backend for the solvers are taken from compiler This includes Core Boolean logic and SMT QF BV as design to denote the metaSMT layers. well as a version of Array logic over bit-vectors. Each frontend defines its own set of available functions as well A. metaSMT Layers as public datatypes. metaSMT consists of three basic layers depicted in The Core Boolean logic defines the public datatype Figure 2. The frontend layer provides primitives of predicate which describes propositional variables. Furthermore, Boolean constants are available, i.e., true 4) BitBlast: This emulation of a QF BV bit-vector and false. This logic also defines primitive Boolean backend uses only Core Boolean logic operations to allow functions, e.g., Or, And. The frontend creates a static the transparent use of SAT or BDD solvers with bit-vector syntax tree for the expression described in the code. This expressions. The translation is performed in a standard syntax tree is passed to the middle-end. way: Given only the Core Boolean logic, each bit-vector C. Middle-ends is transformed into a vector of Boolean variables. The bitwise operations can be applied easily, e.g., an exclusive- The core of metaSMT are basic optimizations and or over two bit-vectors is a bitwise exclusive-or for translations from the frontend to the backend. While the each pair of Boolean variables. The bit-vector predicates frontends provide languages and the backends provide (equal, less-than, etc.) are mapped to a sequence solver integrations, the middle-ends allow the user to of Boolean predicates, e.g., a conjunction of exclusive- customize metaSMT, i.e., on how the input language is nors for equal. Arithmetic operations are reduced to an mapped to the backend. Even in the middle-end itself, equivalent Boolean expression. several modules can be combined. 1) DirectSolver: To enable a low-overhead translation D. Backends from a frontend to a backend the DirectSolver The respective solvers and other constraint solving is provided. All the elements of the input expression techniques are integrated as backends. For each reasoning are directly evaluated in the backend. Variables are engine a dedicated backend is created that maps from the guaranteed to be constructed only once and are stored internal metaSMT API to the API of the engine. Backends in a lookup table. For example, given a multiplication do not have an explicit interface to inherit from. They operation in QF BV logic directly corresponds to a implement the required methods for the languages they multiplication operation in the SMT solver Boolector. support using C++ template mechanisms to integrate The direct middle-end is very lightweight and allows them into a context. This allows the compiler to optimize the compiler to inline all function calls. For a modern the code and, in the case of DirectSolver, produces compiler the resulting executable should perform equally code that is close to a hand-coded implementation using well to a hand-written application using the same backend. the same API. 2) GraphSolver: Instead of adding the frontend ex- This section gives an overview of the backends inte- pressions directly to the solver, they are first inserted grated into metaSMT. They are grouped by the input into a directed graph. The graph models the explicit language they support. The compatibility of the solvers syntax tree of the expression as a Directed Acyclic is also summarized in Table I. Graph (DAG). Formally a node in the graph is a tuple 1) Core Boolean logic backends: Several core logic (Operation, Static Arguments) where the SMT command backends as well as higher level backends are available. and its static arguments are captured (e.g. extract and Core logic is directly supported by backends that accept the range to extract). The edges point from an operation all common Boolean operations. For example, the Binary to the SMT expressions used in this command. A label Decision Diagram (BDD) package CUDD [20] supports on the edges stores the position of the subexpression in all Boolean operations and is integrated in metaSMT. the command. Each time a new expression is evaluated Furthermore, with some minor transformations based on it is first searched in a lookup table before a new node is De-Morgan And-Inverter-Graphs (AIGs) are also able to created, when the node is not found. When the instance handle Boolean operations. Those AIGs are internally is checked for satisfiability, the graph is traversed and represented by the AIGER package [21]. SAT solvers evaluated in the backend. can receive Boolean logic expressions either via the The graph-based translation provides a way to auto- SAT Clause adapter that creates one or more clauses matically detect common subexpressions and efficiently per logic operation or via the SAT Aiger adapter, that handle them to create smaller SMT instances which po- builds an AIG for the expression using the AIGER tentially increases performance of the reasoning process. backend. Afterwards, the AIG is translated into a set This is especially useful if the user wants to automate this of clauses. This infrastructure allow the usage of any process, but either does not want to manually optimize the SAT solver supporting CNF as input language either by SMT instance or does not know the instance in advance an API or externally through files. PicoSAT [22] as well because it is created dynamically inside the program. as MiniSAT [23] are directly supported as Core logic 3) Groups: This middle-end provides an interface and backends via their APIs. Other solvers are supported by implementation of constraint groups for solvers that do generating CNF files and calling the executable of the not have native support for groups. A group is a set SAT solvers. of constraints that belong together. The user can create Furthermore, all SMT QF BV backends natively sup- groups, add expressions to them and delete them at any port Core logic as a subset of the language. time. The solver will then disable all expressions in 2) SMT QF BV backends: Native SMT bit-vector the group. Groups are emulated using guard variables solvers like Boolector [24], SWORD [25] and Z3 [26] and temporary assumptions, e.g., the expression x ∧ y are directly connected through their API for QF BV in group 1 is transformed to g1 → (x ∧ y) using the support. Furthermore, the BitBlast middle-end provides an guard variable g1 and an implication. Depending on the emulation for QF BV using only basic logic operations. solver deleting a group can either lead to the removal This emulation permits using QF BV expressions in of the constraints or to the constraint just being disabled solvers that do not support them natively but support permanently. Core Boolean logic e.g., CUDD or SAT-solvers. TABLE I BACKEND COMPATIBILITY DirectSolver Boolector BACKEND C ORE QF BV A RRAY (BV) SAT AIGER [21] yes emulated no no Boolector [24] yes yes yes no CUDD [20] yes emulated no no MiniSAT [23] emulated emulated no yes GraphSolver Boolector PicoSAT [22] emulated emulated no yes SWORD [25] yes yes no no Z3 [26] yes yes yes no BitBlast yes yes no no SAT Aiger yes emulated no no SAT Clause yes emulated no no DirectSolver BitBlast SAT Clause MiniSAT equal qf_bv_var& GraphSolver BitBlast SAT Aiger MiniSAT {c,width} bvmul qf_bv_var& qf_bv_var& {a,width} {b,width} Fig. 4. Data flow in different contexts Fig. 3. Syntax Tree for equal(c, bvmul(a, b)). Listing 3. metaSMT command grammar 3) SMT QF ABV backends: In addition to Core command ::= assert_cmd | assume_cmd Boolean logic and bit-vector logic the Boolector and | eval_cmd Z3 backends also support arrays in the form of QF QBV | solve_cmd | result_cmd assert_cmd ::= ’assertion(’ context ’,’ logic. Therefore metaSMT supports declaring and work- expression ’);’ ing with arrays over bit-vectors. assume_cmd ::= ’assumption(’ context ’,’ expression ’);’ eval_cmd ::= ’evaluate(’ context ’,’ V. I MPLEMENTATION expression ’);’ solve_cmd ::= ’solve(’ context ’);’ This section describes how the architecture is imple- result_cmd ::= ’read_value(’ context ’,’ mented in metaSMT and how metaSMT is integrated in variable ’);’ C++ programs. variable ::= boolean_variable | bitvector_variable expression ::= A. Syntax and Semantics For the evaluation of metaSMT expressions a context Figure 4 gives some example contexts and visualizes is used which defines syntax and semantics. The context the data flow inside. This illustrates how different concept and different kinds of contexts are described in contexts can change the evaluation of a constraint. The this section. first context defines a solver using Boolector without The syntax component is provided by Boost.Proto. An intermediate representation (DirectSolver). The context expression like equal(c, bvmul(a, b)) is created directly supports Core Boolean logic and QF BV. In from the custom Boost.Proto functions equal and contrast, in the last example, MiniSAT is used. QF BV bvmul as well as the variables a, b and c. From the as well as Core Boolean logic are emulated for this clause expression the syntax tree in Figure 3 is created. The based backend. Furthermore this context uses a graph nodes are labeled with the C++ type and strings inside and an AIG as intermediate representations. the curly braces denote the content of the respective The GraphSolver-based and AIGER-based context first nodes. For metaSMT the tree is used as static type of the create an internal representation and pass the complete ex- expression. The expression and the syntax tree are data, pression directly before solving. When using approaches i.e., they neither have semantics attached nor trigger any without intermediate representation, the requests are actions. forwarded to the next layer until they reach the backend. The semantics for the expression is introduced by Only explicit transformations are applied before passing the metaSMT context, that defines how the syntax tree the expression (e.g., BitBlast, SAT Clause). is evaluated and transformed for a specific solver. The evaluation of Boost.Proto-based expressions is performed B. Usage and API in the metaSMT translation middle-end (e.g., GraphSolver or DirectSolver) so that the backends do not need to The example from Listing 2 contains most of the handle Boost.Proto expressions directly. This reduces the core commands of metaSMT. These are summarized in overhead to implement new backends. Listing 3. Listing 4. Programmatic constraint construction using temporary Listing 5. Using a shared graph for different contexts Variables 1 GraphSolver_Context sword; 1 bitvector x = new_bitvector(8); 2 GraphSolver_Context btor(sword); 2 for( ... ) { 3 3 bitvector tmp = x; 4 GraphSolver_Context::result_type x = 4 x = new_bitvector(8); evaluate(sword, bvuint(0, 8)); 5 assertion(ctx, equal( x, bvmul(tmp, ...))); 5 6 } 6 for( ... ) { 7 ... 7 x = evaluate(sword, equal( x, bvmul(x, 8 solve(ctx) ...))); 8 } 9 assertion(sword, x); The first three functions accept frontend expressions, 10 assertion(btor, x); however they have different effects. The functions 11 solve(sword) == solve(btor); assertion and assumption create the constraint instance where the first adds a constraint permanently to When a GraphSolver is constructed using the copy the (incremental) solver context while the latter adds the constructor, a shared graph is internally used by the constraint for the next call of the solver only. In both contexts. The newly created solver also copies all cases the expression needs to have a Boolean result. The assertions and assumptions, so that both solvers have third function evaluate does not change the instance the same internal state. In this setup the results of but returns a context specific representation of the input evaluate can be shared among the solvers. Each expression only. backend will only evaluate the parts of the graph that To query a context for satisfiability, the solve are required as parts of assertions or assumptions. The function is provided. The result is a Boolean value directly application of evaluate is demonstrated in Listing 5. representing SAT (true) or UNSAT (false). After a call to This can be used for example when building multiple solve the assumptions are discarded while the assertions instances from the same base. At a specific point the are still valid for the subsequent calls. context can be copied and from there both contexts can Getting a SAT result for solve(ctx), i.e., the diverge into seperate instances. instance is satisfiable, a model is generated. The model can be retrieved with the read_value function. The VI. E MPERICAL E VALUATION function takes a context and a variable and returns the This section presents two different applications of assignment of this variable in the given context. The metaSMT. Furthermore, a comparison of metaSMT with result of read_value is automatically convertible to the native API of an SMT solver is presented. The many C++ datatypes, including strings, bit-vectors (vector experiments have been performed on a system with AMD of bool, tribool, bitset) or integers. Opteron 2222 SE processor, 32 GB RAM and a Linux In addition to these core commands, custom middle- operating system. In the following, the run times are ends may provide additional extensions. The Group always given in CPU seconds. middle-end for example provides functions to add groups, change the active group and delete groups. These func- A. Exact Synthesis tions cannot be used in any other context. This section presents examples from exact synthesis of reversible circuits [28], [29]. A reversible circuit computes C. Expression Creation a bijective function, i.e., there is a unique input and output Typically it is necessary to create the metaSMT ex- mapping. Those circuits purely consist of reversible gates pression at run time, e.g., in a loop. As metaSMT syntax – here, the universal Toffoli gate and basic quantum gates trees are statically typed, an extension of the syntax tree are considered. The synthesis problem searches for a is not possible. To work around this limitation, metaSMT reversible circuit consisting of reversible gates which provides two options. The first option is to create a partial computes the function specified by a truth table. There expression and constrain equality to a temporary variable are several exact approaches to synthesize those circuits. that is later reused to create the complete expression. We considered the approach from [28], which translates This would allow strict grammar checking but introduces the problem into a decision problem and asks for a circuit a temporary variable and a constraint, see Listing 4. realization for a given number of gates. The size of the The second option is the use of the evaluate(Ctx, problem instances grows exponentially with number of Expr) function and the context’s result_type. The input variables, because the entire truth table has to be function takes a context and a frontend expression taken into account. This usually results in hard problem and returns the context specific representation of the instances even for small truth tables. expression. The result of the evaluation is of the backend The underlying problem formulation has been encoded specific type Ctx::result_type. This expression in QF BV and an incremental algorithm searches for can be stored and later be used in other expressions. a valid circuit implementation. Using metaSMT six- Note however that the return value is solver specific and teen different configurations have been evaluated. The therefore not portable or reusable in other contexts, not configurations consist of four internal API backend even contexts of the same type. solvers, i.e. Boolector, Z3, MiniSAT, and PicoSAT. A powerful exception to this rule is the Additionally, metaSMT is used to generated CNF files result_type of a GraphSolver-based context, to run the external solvers PicoSAT, MiniSAT, Pre- where the result is a node in the internal graph. coSAT, and Plingeling [30]. All eight backends are used Direct Direct Graph 10000 Graph Dir Dir Graph 1000 Graph Direct Graph Direct time [s] 100 Graph Direct Graph Direct Graph 10 1 0.1 dec per tof 4m gra fre alu gra mi tof hw od es_ fol od yco dk -v0 yco lle fol b4 24 c om i_co 5-v de6 in_ _in de6 r_c i_d _co -v0 ple mp 0_ _co com com _co om ou mp _in let inc ple ple ble le com te_ e_1 om mp te_ ple mp te_ _co te_ ple 4 ple let 3 te_ let 5 mp 20 te_ e_1 10 e_1 let te_ 8 9 9 e_2 15 Fig. 5. Run times of reversible circuit synthesis for hard instances using a metaSMT-based version of RevKit [27] TABLE II with the DirectSolver middle-end as well as the R ESULT FOR MUTATION TESTING USING DIFFERENT CONTEXTS GraphSolver middle-end. Name Time [s] For the synthesis 11 specifications were used which are Direct Graph Direct Graph publicly available from [31]. A timeout of 3,600 seconds Boolector Boolector MiniSAT MiniSAT was applied. The results are presented in Figure 5. On isl 0.05 0.22 0.34 0.47 the x-axis the respective benchmark is shown, whereas min 0.34 0.48 0.82 0.65 the y-axis denotes the run time in seconds for each mid 4.73 5.07 7.87 4.36 fmin3 5.02 5.85 4.45 2.55 configuration in logarithmic scale. Externally called fmin5 21.08 25.96 14.92 9.56 solvers are marked with ∗. fmin10 310.52 260.38 997.65 550.94 From Figure 5 it is clear that no single solver tri 207.69 193.99 1596.99 652.64 dominates the benchmarks. For example, for the benchmarks from decode24-v0_incomple_5 to Boolector contexts and the graph-based MiniSAT perform graycode6_complete_19 Boolector performs much better. However, for difficult instances with a run time better than any other solver. But for the benchmarks from over 1 minute, the graph-based Boolector context is miller_complete_5, Boolector is outperformed by fastest while MiniSAT-based contexts require significantly the SAT solvers. MiniSAT as well as PicoSAT are evalu- more time. For these harder instances the GraphSolver ated as internal and external versions. The accumulated middle-end outperforms the direct variant of the same run times of the solvers MiniSAT and PicoSAT over all backend. This effect is most likely due to the removal benchmarks are 18,790 seconds for the internal version of redundancies in the graph. For MiniSAT this amounts and 8,989 seconds for the external version. Surprisingly, to run time reductions of around 50%. With metaSMT the externally called solvers are much better here than the as abstraction layer it is easy to evaluate the effects of internal called solvers, though the internal solvers may different contexts or optimizations. When changes are benefit from learnt information. Overall, the externally only in the abstraction layer no application code needs called PrecoSAT solver needs 326.24 seconds over all to be changed and only little effort is required. benchmarks and Boolector needs 3,285.05 seconds. To summarize, all the presented results can be achieved C. Comparison with direct API very easily by using metaSMT. Only one parameter needs For the factorization algorithm from Listing 2 a hand to be switched to run a different solver. coded implementation using the Boolector C API is com- pared to a metaSMT DirectSolver-based implementation B. Mutation Testing with the Boolector backend. The resulting application is Given a program, by mutation several faulty variants available as part of the metaSMT package. of the program are created and combined into a single The experiment has the following setup: The algorithm program called meta-mutant. Using metaSMT the meta- from Listing 2 was changed to work on sequences instead mutant is encoded into a set of constraints. Each satisfying of generating random numbers. A sequence of 10,000 assignment yields a test case that discovers at least one random 64 bit numbers is generated and the algorithm it fault. Experiments of [32] where executed on a set of applied to it 10 times. The same sequence is used for both metaSMT contexts. The results are shown in Table II. the hand coded and the metaSMT-based implementation Comparing the Boolector backend with the MiniSAT of the algorithm. The complete experiment was repeated 5 backend using DirectSolver as well as GraphSolver times with Boolector being executed first and 5 times with middle-ends. metaSMT being executed first. Altogether each solver was The results significantly vary with the difficulty of forced to solve 1,000,000 constraints of 64 bit numbers the instance. For easy instances the directly connected factorized into two 32 bit numbers. The results showed no significant difference caused by [11] S. Ranise and C. Tinelli, “The Satisfiability Modulo Theories the metaSMT abstraction layer: 1, 736s for plain Boolec- Library (SMT-LIB),” http://www.smtlib.org, 2006. [12] O. Shtrichman, “Pruning techniques for the SAT-based bounded tor compared to 1, 729s for metaSMT with Boolector, model checking problem,” in CHARME, ser. LNCS, vol. 2144, i.e., 1.7 seconds for 10,000 factorizations. 2001, pp. 58–70. D. Other applications [13] S. Cook, “The complexity of theorem proving procedures,” in 3. ACM Symposium on Theory of Computing, 1971, pp. 151–158. In addition to the aforementioned projects metaSMT is [14] C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, Satisfia- also used in a Constraint Random Stimuli generation Li- bility Modulo Theories, ser. Frontiers in Artificial Intelligence and Applications. IOS Press, February 2009, vol. 185, ch. 26, brary. In the library elements of the SystemC Verification pp. 825–885. Library [33] and techniques from [34] are combined. [15] D. R. Cok, “jSMTLIB: Tutorial, validation and adapter tools for smt-libv2,” in NASA Formal Methods, ser. LNCS, 2011, vol. VII. C ONCLUSIONS 6617, pp. 480–486. [16] “Boost C++ libraries,” http://www.boost.org/. metaSMT is a library that abstracts details of reasoning [17] E. Niebler, “Proto: A compiler construction toolkit for DSELs,” engines. Based on metaSMT very little programming in Proceedings of the 2007 Symposium on Library-Centric Software Design, ser. LCSD ’07. New York, NY, USA: ACM, effort is required to integrate formal methods into a user‘s 2007, pp. 42–51. application. Once this has been done, a wide range of [18] J. de Guzman and D. Nuffer, “The Spirit library: Inline parsing solvers as well as optimization techniques can be selected. in C++,” C/C++ User Journal, vol. 21, no. 9, 2003. Various research projects already integrate metaSMT. [19] T. L. Veldhuizen, “Arrays in Blitz++,” in Proceedings of the Second International Symposium on Computing in Object- Future work on metaSMT includes the development Oriented Parallel Environments, 1998, pp. 223–230. of the following features: New frontend logics will [20] F. Somenzi, CUDD: CU Decision Diagram Package Release complete the support for SMT logics (e.g. uninterpreted 2.4.1. University of Colorado at Boulder, 2009. functions, integer arithmetic), while new middle-ends [21] “Aiger,” http://fmv.jku.at/aiger/. [22] A. Biere, “Picosat essentials,” JSAT, vol. 4, no. 2-4, pp. 75–97, will increase solving performance (e.g. portfolio or multi- 2008. threaded contexts) and new backends will provide access [23] N. Eén and N. Sörensson, “An extensible sat-solver,” in SAT, to additional SMT solvers. ser. LNCS, E. Giunchiglia and A. Tacchella, Eds., vol. 2919. Springer, 2003, pp. 502–518. [24] R. Brummayer and A. Biere, “Boolector: An efficient SMT VIII. ACKNOWLEDGMENTS solver for bit-vectors and arrays,” in Tools and Algorithms for We would like to thank Hoang M. Le, Heinz Riener the Construction and Analysis of Systems, 2009, pp. 174–177. [25] R. Wille, G. Fey, D. Große, S. Eggersglüß, and R. Drechsler, and Fereshta Yazdani for the helpful discussions, their “Sword: A SAT like prover using word level information,” in proposals for improvements, testing and contributions to VLSI of System-on-Chip, 2007, pp. 88–93. metaSMT. [26] L. M. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in TACAS, ser. LNCS, C. R. Ramakrishnan and J. Rehof, Eds., vol. 4963. Springer, 2008, pp. 337–340. R EFERENCES [27] M. Soeken, S. Frehse, R. Wille, and R. Drechsler, “RevKit: A [1] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model toolkit for reversible circuit design,” in Workshop on Reversible checking without BDDs,” in Tools and Algorithms for the Computation, 2010, pp. 69 – 72. Construction and Analysis of Systems, ser. LNCS, vol. 1579. [28] D. Große, R. Wille, G. Dueck, and R. Drechsler, “Exact Springer Verlag, 1999, pp. 193–207. multiple-control toffoli network synthesis with SAT techniques,” [2] K. McMillan, “Interpolation and SAT-based model checking,” Computer-Aided Design of Integrated Circuits and Systems, IEEE in Computer Aided Verification, ser. LNCS. Springer Berlin / Transactions on, vol. 28, no. 5, pp. 703 –715, May 2009. Heidelberg, 2003, vol. 2725, pp. 1–13. [29] R. Wille, D. Große, M. Soeken, and R. Drechler, “Using higher [3] E. Arbel, O. Rokhlenko, and K. Yorav, “SAT-based synthesis levels of abstraction for solving optimization problems by of clock gating functions using 3-valued abstraction,” in Formal boolean satisfiability,” in Symposium on VLSI, 2008. ISVLSI Methods in Computer-Aided Design, 2009, 2009, pp. 198 –204. ’08. IEEE Computer Society Annual, 2008, pp. 411 –416. [4] F. Haedicke, B. Alizadeh, G. Fey, M. Fujita, and R. Drechsler, [30] A. Biere, “Lingeling, plingeling, picosat and precosat at “Polynomial datapath optimization using constraint solving and SAT race 2010,” Tech. Rep., 2010. [Online]. Available: formal modelling,” in Computer-Aided Design (ICCAD), 2010 http://fmv.jku.at/papers/Biere-FMV-TR-10-1.pdf IEEE/ACM International Conference on, 2010, pp. 756 –761. [31] R. Wille, D. Große, L. Teuber, G. W. Dueck, and R. Drech- [5] R. Drechsler, S. Eggersgluss, G. Fey, A. Glowatz, F. Hapke, sler, “RevLib: An online resource for reversible functions and J. Schloeffel, and D. Tille, “On acceleration of SAT-based ATPG reversible circuits,” in Int’l Symp. on Multi-Valued Logic, 2008, for industrial designs,” Computer-Aided Design of Integrated pp. 220–225, RevLib is available at http://www.revlib.org. Circuits and Systems, IEEE Transactions on, vol. 27, no. 7, pp. [32] H. Riener, R. Bloem, and G. Fey, “Test case generation from 1329 –1333, 2008. mutants using model checking techniques,” in International [6] M. K. Ganai and A. Gupta, “Accelerating high-level bounded Conference on Software Testing, Verification and Validation model checking,” in International Conference on Computer- Workshops, 2011, pp. 388 – 397. aided design. New York, NY, USA: ACM, 2006, pp. 794–801. [33] SystemC Verification Standard Specification Version 1.0e, Sys- [7] P. Bjesse, “A practical approach to word level model checking temC Verification Working Group. of industrial netlists,” in International Conference on Computer [34] R. Wille, D. Große, F. Haedicke, and R. Drechsler, “SMT- Aided Verification, 2008, pp. 446–458. based stimuli generation in the SystemC verification library,” [8] A. Armando, J. Mantovani, and L. Platania, “Bounded model in Advances in Design Methods from Modeling Languages checking of software using SMT solvers instead of SAT solvers,” for Embedded Systems and SoC’s: Selected Contributions on Int. J. Softw. Tools Technol. Transf., vol. 11, pp. 69–83, 2009. Specification, Design, and Verification from FDL 2009, ser. [9] “SMT-COMP 2009,” http://www.smtcomp.org/2009, 2009. Lecture Notes in Electrical Engineering, D. Borrione, Ed. [10] “SMT-COMP 2010,” http://www.smtcomp.org/2010, 2010. Springer Netherlands, 2010, vol. 63, pp. 227–244.