-Decision procedures are used as core technique in many applications today. In this context, automated reasoning based on Satisfiability Modulo Theories (SMT) is very effective. However, developers have to decide which concrete engine to use and how to integrate the engine into the application. Even if file formats like SMTLIB standardize the input of many engines, advanced features remain unused and the integration of the engine is left to the programmer. This work presents metaSMT, a framework that integrates advanced reasoning engines into the program code of the respective application. metaSMT provides an easy to use language that allows engine independent programming while gaining from high performance reasoning engines. State-of-the-art solvers for satisfiability and other theories are available for the user via metaSMT with minimal programming effort. For two examples we show how metaSMT is used in current research projects.
Despite the successful research and application of
decision procedures, the increasing complexity of
software and hardware systems demands for more effective
reasoning engines to overcome complexity issues. In
the last years, solvers for Satisfiability Modulo
Theories (SMT) have been developed. Different theories are
combined to formulate the problem. Various works gave
empirical evidence that SMT reasoning engines increase
the efficiency of formal methods [
The performance of SMT reasoning engines remains an
active research topic. Annual SMT competitions [
When using SMT in a concrete algorithm, the most
common way is to generate a problem instance in
SMT-LIB format [
This work was supported in part by the German Federal Ministry
of Education and Research (BMBF) within the project SANITAS
under contract no. 01M3088.
check for satisfiability. Furthermore, advanced features
are available, e.g., computing interpolants which are
utilized in SAT-based Model Checking [
This work presents metaSMT a publicly available, easy to use and powerful tool1 which provides an integration of the native Application Programming Interface (API) of modern reasoning engines into C++ code. The advantages of metaSMT are: (1) engine independence through efficient abstraction layers (2) simple use of various decision procedures (3) extensibility in terms of input language and reasoning engines (4) customizability in terms of optimization and infrastructure (5) translation of the input language into native engine calls at compile time.
The remaining work is structured as follows: Section II gives a basic introduction into SMT and the programming methods used in metaSMT. Afterwards an example of a metaSMT-based application is given before in Section IV the architecture of metaSMT is described. Section V describes how this architecture is implemented in metaSMT and Section VI gives an empirical evaluation of metaSMT including its use in current research projects. The work closes with conclusions.
as the SAT problem. The problem asks whether there
exists an assignment of Boolean variables such that the
Boolean function evaluates to true. The problem has
been proven NP-complete [
problem but with more complex theories rather than only propositional logic. A detailed introduction is given
metasmt.php
Listing 1. SMT instance for a b = 21466342967
(benchmark factorization.smt
:logic QF_BV
:extrafuns ((a BitVec[
The Boost project [
Technically, this work uses Boost.Proto to implement
a domain specific language for SMT logics in metaSMT.
in [
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 SMTsatisfiability 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 2 B2n, compute two integers fiability can be exploited. But the application is ~a;~b 2 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 [
Listing 2. metaSMT factorization and prime test 1 Context ctx; 2 const unsigned width = <parameter>; 3 4 bitvector a = new_bitvector(width); 5 bitvector b = new_bitvector(width); 6 bitvector c = new_bitvector(width); 7 8 assertion(ctx, nequal(a, bvuint(1,width)) ); 9 assertion(ctx, nequal(b, bvuint(1,width)) ); 10 11 assertion( ctx, equal( zero_extend(width, c) , 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
1 ); 15 assumption( ctx, equal(c, bvuint(r, 2*
width)) ); if( solve( ctx ) ) { unsigned a_value = read_value( ctx, a ); unsigned b_value = read_value( ctx, b ); printf("factorized %d into %d * %d\n", r
, a_value, b_value); } else { printf("%d is prime.", r);
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. ARCHITECTURE defines how the input language is mapped to function calls of the backend. 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 exclusivecustomize 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 intepressions 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 [
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 [
Boolean logic and bit-vector logic the Boolector and Z3 backends also support arrays in the form of QF QBV logic. Therefore metaSMT supports declaring and working with arrays over bit-vectors.
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 exexpression. 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 5. Using a shared graph for different contexts 1 GraphSolver_Context<SWORD> sword; 2 GraphSolver_Context<Boolector> btor(sword); 3 4 GraphSolver_Context<SWORD>::result_type x =
evaluate(sword, bvuint(0, 8)); 5 6 for( ... ) { 7 x = evaluate(sword, equal( x, bvmul(x, ...))); Listing 4. Programmatic constraint construction using temporary Variables 1 bitvector x = new_bitvector(8); 2 for( ... ) { 3 bitvector tmp = x; 4 x = new_bitvector(8); 5 assertion(ctx, equal( x, bvmul(tmp, ...))); 6 } 7 ... 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. EMPERICAL EVALUATION 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 [
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 [
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 sixNote 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,
Prewhere the result is a node in the internal graph. coSAT, and Plingeling [
lete_15 decod24-v0_incomp eres_complete_4 p toffoli_comp lete_1 4mod5-v0_incomp graycode6_comp fredkin_comp
lete_3 lete_8 lete_19 alu-v0_incomp graycode6_comp lete_10 lete_19 m iller_comp lete_5 toffoli_double_comphwb4_complete_20 lete_2 with the DirectSolver middle-end as well as the GraphSolver middle-end.
For the synthesis 11 specifications were used which are
publicly available from [
From Figure 5 it is clear that no single solver dominates the benchmarks. For example, for the benchmarks from decode24-v0_incomple_5 to graycode6_complete_19 Boolector performs much better than any other solver. But for the benchmarks from miller_complete_5, Boolector is outperformed by the SAT solvers. MiniSAT as well as PicoSAT are evaluated as internal and external versions. The accumulated run times of the solvers MiniSAT and PicoSAT over all benchmarks are 18,790 seconds for the internal version and 8,989 seconds for the external version. Surprisingly, the externally called solvers are much better here than the internal called solvers, though the internal solvers may benefit from learnt information. Overall, the externally called PrecoSAT solver needs 326.24 seconds over all benchmarks and Boolector needs 3,285.05 seconds.
To summarize, all the presented results can be achieved very easily by using metaSMT. Only one parameter needs to be switched to run a different solver. Boolector contexts and the graph-based MiniSAT perform better. However, for difficult instances with a run time over 1 minute, the graph-based Boolector context is fastest while MiniSAT-based contexts require significantly more time. For these harder instances the GraphSolver middle-end outperforms the direct variant of the same backend. This effect is most likely due to the removal of redundancies in the graph. For MiniSAT this amounts to run time reductions of around 50%. With metaSMT as abstraction layer it is easy to evaluate the effects of different contexts or optimizations. When changes are only in the abstraction layer no application code needs to be changed and only little effort is required.
coded implementation using the Boolector C API is compared 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 [
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 metaSMT abstraction layer: 1; 736s for plain Boolector compared to 1; 729s for metaSMT with Boolector, i.e., 1:7 seconds for 10,000 factorizations.
metaSMT is a library that abstracts details of reasoning engines. Based on metaSMT very little programming effort is required to integrate formal methods into a user‘s application. Once this has been done, a wide range of solvers as well as optimization techniques can be selected.
Various research projects already integrate metaSMT. Future work on metaSMT includes the development of the following features: New frontend logics will complete the support for SMT logics (e.g. uninterpreted functions, integer arithmetic), while new middle-ends will increase solving performance (e.g. portfolio or multithreaded contexts) and new backends will provide access to additional SMT solvers.
and Fereshta Yazdani for the helpful discussions, their proposals for improvements, testing and contributions to metaSMT.