=Paper=
{{Paper
|id=None
|storemode=property
|title=metaSMT: Focus on Your Application not on Solver Integration
|pdfUrl=https://ceur-ws.org/Vol-832/paper_5.pdf
|volume=Vol-832
|dblpUrl=https://dblp.org/rec/conf/fmcad/HaedickeFFGD11
}}
==metaSMT: Focus on Your Application not on Solver Integration==
https://ceur-ws.org/Vol-832/paper_5.pdf
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.