Z3:An Efficient SMT Solver
Leonardo de Moura and Nikolaj Bjørner
Microsoft Rearch,One Microsoft Way,Redmond,WA,98074,USA
{leonardo,nbjorner}@
Abstract.Satisfiability Modulo Theories(SMT)problem is a decision
problem for logicalfirst order formulas with respect to combinations of
background theories such as:arithmetic,bit-vectors,arrays,and unin-
terpreted functions.Z3is a new and efficient SMT Solver freely available
from Microsoft Rearch.It is ud in various software verification and
analysis applications.
1Introduction
Satisfiability modulo theories(SMT)generalizes boolean satisfiability(SAT)by adding equality reasoning,arithmetic,fixed-size bit-vectors,arrays,quantifiers, and other ufulfirst-order theories.An SMT solver is a tool for deciding the satisfiability(or dually the validity)of formulas in the theories.SMT solvers enable applications such as extended static checking,predicate abstraction,test ca generation,and bounded model checking over infinite domains,to mention a few.
Z3is a new SMT solver from Microsoft Rearch.It is targeted at solving problems that ari in software verification and software analysis.Conquently, it integrates support for a variety of theories.A prototype of Z3participated in SMT-COMP’07,where it won4first places,and7cond places.Z3us novel algorithms for quantifier instantiation[4]and theory combination[5].The first external relea of Z3was in September2007.More information,including instructions for downloading and installing the tool,is available at the Z3web page:/projects/z3.
Currently,Z3is ud in Spec#/Boogie[2,7],Pex[13],HAVOC[11],Vigi-lante[3],a verifying C compiler(VCC),and Yogi[10].It is being integrated with other projects,including SLAM/SDV[1].
2Clients
Before describing the inner workings of Z3,two lected us are briefly de-scribed.Front-ends interact with Z3by using either a textual format or a binary API.Three textual input-formats are supported:The SMT-LIB[12]format,the Simplify[8]format,and a low-level native format in the spirit of the DIMACS format for propositional SAT formulas.One can also call Z3procedurally by using either an ANSI C API,an API for the managed common language runtime,or an OCaml API.
Spec#/Boogie generates logical verification conditions from a Spec#pro-gram(an extension of C#).Internally,it us Z3to analyze the verification conditions,to prove the correctness of programs,or tofind errors on them.The formulas produced by Spec#/Boogie contain universal quantifiers,and also u linear integer arithmetic.Spec#replaced the Simplify theorem prover by Z3as the default reasoning engine in May2007,resulting in substantial performance improvements during theorem proving.
Pex(Program EXploration)is an intelligent assistant to the programmer.By automatically generating unit tests,it allows tofind bugs early.In addition,it suggests to the programmer how tofix the bugs.Pex learns the program behavior from the execution traces,and Z3is ud to produce new test cas with different behavior.The result is a minimal test suite with maximal code coverage.The formulas produced by Pex containsfixed-sized bit-vectors,tuples,arrays,and quantifiers.
生物学教学3System Architecture
Z3integrates a modern DPLL-bad SAT solver,a core theory solver that han-dles equalities and uninterpreted functions,satellite solvers(for arithmetic,ar-rays,etc.),and an E-matching abstract machine(for quantifiers).Z3is imple-mented in C++.A schematic overview of Z3is shown in the followingfigure.
Simplifier Input formulas arefirst procesd using an incomplete,but efficient simplification.The simplifier applies standard algebraic reduction rules,such as p∧true→p,but also performs limited contextual simplification,as it identifies equational definitions within a context and reduces the remaining formula using the definition,so for instance x=4∧q(x)→x=4∧q(4).The trivially satisfiable conjunct x=4is not compiled into the core,but kept aside in the ca the client requires a model to evaluate x.
Compiler The simplified abstract syntax tree reprentation of the formula is converted into a different data-structure comprising of a t of claus and congruence-closure nodes.
Congruence Closure Core The congruence closure core receives truth assign-ments to atoms from the SAT solver.Atoms range over equalities and theory specific atomic formulas,such as arithmetical inequalities.Equalities asrted by the SAT solver are propagated by the congruence closure core using a data structure that we will call an E-graph following[8].Nodes in the E-graph may point to one or more theory solvers.When two nodes are merged,the t of theory solver references are merged,and the merge is propagated as an equality to the theory solvers in the interction of the two ts of solver references.The core also propagates the effects of the theory solvers,such as inferred equalities that are produced and atoms assigned to true or fal.The theory solvers may als
票据交易所
o produce fresh atoms in the ca of non-convex theories.The atoms are subquently owned and assigned by the SAT solver.
Theory Combination:Traditional methods for combining theory solvers rely on capabilities of the solvers to produce all implied equalities or a pre-processing step that introduces additional literals into the arch space.Z3us a new theory combination method that incrementally reconciles models maintained by each theory[5].
SAT Solver Boolean ca splits are controlled using a state-of-the art SAT solver.The SAT solver integrates standard arch pruning methods,such as two-watch literals for efficient Boolean constraint propagation,lemma learning using conflict claus,pha caching for guiding ca splits,and performs non-chronological backtracking.
Deleting claus:Quantifier instantiation has a side-effect of producing new claus containing new atoms into the arch space.Z3garbage collects claus, together with their atoms and terms,that were uless in closing branches.Con-flict claus,and literals ud in them,are on the other hand not deleted,so quantifier instantiations that were uful in producing conflicts are retained as a side-effect.
Relevancy propagation:DPLL(T)bad solvers assign a Boolean value to potentially all atoms appearing in a goal.In practice,veral of the atoms are don’t cares.Z3ignores the atoms for expensive theories,such as bit-vectors, and inference rules,such as quantifier instantiation.The algorithm ud for discriminating relevant atoms from don’t cares is described in[6].
Quantifier instantiation using E-matching Z3us a well known approach for quantifier reasoning that works over an E-graph to instantiate quantified vari-
ables.Z3us new algorithms that identify matches on E-graphs incrementally and efficiently.Experimental results show substantial performance improvements over existing state-of-the-art SMT solvers[4].
Theory Solvers Z3us a linear arithmetic solver bad on the algorithm ud in Yices[9].The array theory us lazy instantiation of array axioms.The fixed-sized bit-vectors theory applies bit-blasting to all bit-vector operations,but equality.
Model generation Z3has the ability to produce models as part of the output. Models assign values to the constants in the input and generate partial function graphs for predicates and function symbols.
不擅长的英文4Conclusion电话机简笔画
Z3is being ud in veral projects at Microsoft since February2007.Its main applications are extended static checking,test ca generation,and predicate abstraction.
References
1.T.Ball and S.K.Rajamani.The SLAM project:debugging system software via
三步舞经典老歌
static analysis.SIGPLAN Not.,37(1):1–3,2002.
2.M.Barnett,K.R.M.Leino,and W.Schulte.The Spec#programming system:
什么的像什么An overview.In CASSIS2004,LNCS3362,pages49–69.Springer,2005.
3.M.Costa,J.Crowcroft,M.Castro,A.I.T.Rowstron,L.Zhou,L.Zhang,and
P.Barham.Vigilante:end-to-end containment of internet worms.In A.Herbert and K.P.Birman,editors,SOSP,pages133–147.ACM,2005.
4.L.de Moura and N.Bjørner.Efficient E-matching for SMT Solvers.In CADE’07.
Springer-Verlag,2007.
幸福小城
5.L.de Moura and N.Bjørner.Model-bad Theory Combination.In SMT’07,2007.
6.L.de Moura and N.Bjørner.Relevancy Propagation.Technical Report MSR-TR-
2007-140,Microsoft Rearch,2007.
7.R.DeLine and K.R.M.Leino.BoogiePL:A typed procedural language for check-
ing object-oriented programs.Technical Report2005-70,Microsoft Rearch,2005.
8. D.Detlefs,G.Nelson,and J.B.Saxe.Simplify:a theorem prover for program
checking.J.ACM,52(3):365–473,2005.
9. B.Dutertre and L.de Moura.A Fast Linear-Arithmetic Solver for DPLL(T).In
CAV’06,LNCS4144,pages81–94.Springer-Verlag,2006.
10. B.S.Gulavani,T.A.Henzinger,Y.Kannan,A.V.Nori,and S.K.Rajamani.Syn-
ergy:a new algorithm for property checking.In Michal Young and Premkumar T.
Devanbu,editors,SIGSOFT FSE,pages117–127.ACM,2006.
11.S.K.Lahiri and S.Qadeer.Back to the Future:Revisiting Preci Program Veri-
fication using SMT Solvers.In POPL’2008,2008.
12.S.Rani and C.Tinelli.The Satisfiability Modulo Theories Library(SMT-LIB).
www.SMT-LIB,2006.
13.N.Tillmann and W.Schulte.Unit Tests Reloaded:Parameterized Unit Testing
with Symbolic Execution.IEEE software,23:38–47,2006.
柠檬简笔画
