Z3Py基本材料

Z3isahighperformancetheoremproverdevelopedatMicrosoftResearch.Z3isusedinmanyapplicationssuchas:software/hardwareverificationandtesting,constraintsolving,analysisofhybridsystems,security,biology(insilicoanalysis),andgeometricalproblems.ThistutorialdemonstratesthemaincapabilitiesofZ3Py:theZ3APIinPython.NoPythonbackgroundisneededtoreadthistutorial.However,itisusefultolearnPython(afunlanguage!)atsomepoint,andtherearemanyexcellentfreeresourcesfordoingso(PythonTutorial).TheZ3distributionalsocontainstheC,.NetandOCamlAPIs.ThesourcecodeofZ3PyisavailableintheZ3distribution,feelfreetomodifyittomeetyourneeds.ThesourcecodealsodemonstrateshowtousenewfeaturesinZ34.0.Othercoolfront-endsforZ3includeScala^Z3andSBV.Besuretofollowalongwiththeexamplesbyclickingtheloadineditorlinkinthecorner.SeewhatZ3Pysays,tryyourownscripts,andexperiment!Pleasesendfeedback,commentsand/[e-mail]withthefollowingsimpleexample:loadineditorx=Int('x')y=Int('y')solve(x2,y10,x+2*y==7)ThefunctionInt('x')createsanintegervariableinZ3namedx.Thesolvefunctionsolvesasystemofconstraints.Theexampleaboveusestwovariablesxandy,andthreeconstraints.Z3PylikePythonuses=forassignment.Theoperators,=,,=,==and!=forcomparison.Intheexampleabove,theexpressionx+2*y==7isaZ3constraint.Z3cansolveandcrunchformulas.ThenextexamplesshowhowtousetheZ3formula/expressionsimplifier.loadineditorx=Int('x')y=Int('y')printsimplify(x+y+2*x+3)printsimplify(xy+x+2)printsimplify(And(x+1=3,x**2+x**2+y**2+2=5))Bydefault,Z3Py(fortheweb)displaysformulasandexpressionsusingmathematicalnotation.Asusual,∧isthelogicaland,∨isthelogicalor,andsoon.Thecommandset_option(html_mode=False)makesallformulasandexpressionstobedisplayedinZ3Pynotation.ThisisalsothedefaultmodefortheofflineversionofZ3PythatcomeswiththeZ3distribution.loadineditorx=Int('x')y=Int('y')printx**2+y**2=1set_option(html_mode=False)printx**2+y**2=1Z3providesfunctionsfortraversingexpressions.loadineditorx=Int('x')y=Int('y')n=x+y=3printnumargs:,n.num_args()printchildren:,n.children()print1stchild:,n.arg(0)print2ndchild:,n.arg(1)printoperator:,n.decl()printopname:,n.decl().name()Z3providesallbasicmathematicaloperations.Z3PyusesthesameoperatorprecedenceofthePythonlanguage.LikePython,**isthepoweroperator.Z3cansolvenonlinearpolynomialconstraints.loadineditorx=Real('x')y=Real('y')solve(x**2+y**23,x**3+y5)TheprocedureReal('x')createstherealvariablex.Z3Pycanrepresentarbitrarilylargeintegers,rationalnumbers(likeintheexampleabove),andirrationalalgebraicnumbers.Anirrationalalgebraicnumberisarootofapolynomialwithintegercoefficients.Internally,Z3representsallthesenumbersprecisely.Theirrationalnumbersaredisplayedindecimalnotationformakingiteasytoreadtheresults.loadineditorx=Real('x')y=Real('y')solve(x**2+y**2==3,x**3==2)set_option(precision=30)printSolving,anddisplayingresultwith30decimalplacessolve(x**2+y**2==3,x**3==2)Theprocedureset_optionisusedtoconfiguretheZ3environment.Itisusedtosetglobalconfigurationoptionssuchashowtheresultisdisplayed.Theoptionset_option(precision=30)setsthenumberofdecimalplacesusedwhendisplayingresults.The?markin1.2599210498?indicatestheoutputistruncated.Thefollowingexampledemonstratesacommonmistake.Theexpression3/2isaPythonintegerandnotaZ3rationalnumber.TheexamplealsoshowsdifferentwaystocreaterationalnumbersinZ3Py.TheprocedureQ(num,den)createsaZ3rationalwherenumisthenumeratoranddenisthedenominator.TheRealVal(1)createsaZ3realnumberrepresentingthenumber1.loadineditorprint1/3printRealVal(1)/3printQ(1,3)x=Real('x')printx+1/3printx+Q(1,3)printx+1/3printx+0.25Rationalnumberscanalsobedisplayedindecimalnotation.loadineditorx=Real('x')solve(3*x==1)set_option(rational_to_decimal=True)solve(3*x==1)set_option(precision=30)solve(3*x==1)Asystemofconstraintsmaynothaveasolution.Inthiscase,wesaythesystemisunsatisfiable.loadineditorx=Real('x')solve(x4,x0)LikeinPython,commentsbeginwiththehashcharacter#andareterminatedbytheendofline.Z3Pydoesnotsupportcommentsthatspanmorethanoneline.loadineditor#Thisisacommentx=Real('x')#comment:creatingxprintx**2+2*x+2#comment:printingpolynomialBooleanLogicZ3supportsBooleanoperators:And,Or,Not,Implies(implication),If(if-then-else).Bi-implicationsarerepresentedusingequality==.ThefollowingexampleshowshowtosolveasimplesetofBooleanconstraints.loadineditorp=Bool('p')q=Bool('q')r=Bool('r')solve(Implies(p,q),r==Not(q),Or(Not(p),r))ThePythonBooleanconstantsTrueandFalsecanbeusedtobuildZ3Booleanexpressions.loadineditorp=Bool('p')q=Bool('q')printAnd(p,q,True)printsimplify(And(p,q,True))printsimplify(And(p,False))ThefollowingexampleusesacombinationofpolynomialandBooleanconstraints.loadineditorp=Bool('p')x=Real('x')solve(Or(x5,x10),Or(p,x**2==2),Not(p))SolversZ3providesdifferentsolvers.Thecommandsolve,usedinthepreviousexamples,isimplementedusingtheZ3solverAPI.Theimplementationcanbefoundinthefilez3.pyintheZ3distribution.ThefollowingexampledemonstratesthebasicSolverAPI.loadineditorx=Int('x')y=Int('y')s=Solver()printss.add(x10,y==x+2)pri