>>> n = x + y >=3>>>"num args: ", n.num_args()('num args: ',2)>>>"children: ", n.children()('children: ', [x + y,3])>>>"1st child:", n.arg(0)('1st child:', x + y)>>>"2nd child:", n.arg(1)('2nd child:',3)>>>"operator: ", n.decl()('operator: ',>=)>>>"op name: ", n.decl().name()('op name: ','>=')
set_param() 函数用于对 Z3 的全局变量进行配置,如运算精度,输出格式等等:
>>> x =Real('x')>>> y =Real('y')>>>solve(x**2+ y**2==3, x**3==2)[x = 1.2599210498?, y = -1.1885280594?]>>>>>>set_param(precision=30)>>>solve(x**2+ y**2==3, x**3==2)[x = 1.259921049894873164767210607278?, y = -1.188528059421316533710369365015?]
>>> p =Bool('p')>>> q =Bool('q')>>> r =Bool('r')>>>solve(Implies(p, q), r ==Not(q), Or(Not(p), r))[q = False, p = False, r = True]>>>>>> x =Real('x')>>>solve(Or(x <5, x >10), Or(p, x**2==2), Not(p))[x = -1.4142135623?, p = False]
>>>1/30.3333333333333333>>>RealVal(1)/31/3>>>Q(1, 3)# Q(a, b) 返回有理数 a/b1/3>>>>>> x =Real('x')>>> x +1/3x +3333333333333333/10000000000000000>>> x +Q(1, 3)x +1/3>>> x +"1/3"x +1/3>>> x +0.25x +1/4>>>solve(3*x ==1)[x = 1/3]>>>set_param(rational_to_decimal=True)# 以十进制形式表示有理数>>>solve(3*x ==1)[x = 0.3333333333?]
在混合使用实数和整数变量时,Z3Py 会自动添加强制类型转换将整数表达式转换成实数表达式。
>>> x =Real('x')>>> y =Int('y')>>> a, b, c =Reals('a b c')# 返回一个实数常量元组>>> s, r =Ints('s r')# 返回一个整数常量元组>>> x + y +1+ a + sx +ToReal(y)+1+ a +ToReal(s)# ToReal() 将整数表达式转换成实数表达式>>>ToReal(y)+ cToReal(y)+ c
import sysprint ("Please enter a valid serial number from your RoboCorpIntergalactic purchase")iflen(sys.argv)<2:print ("Usage: %s [serial number]"%sys.argv[0])exit()print ("#>"+ sys.argv[1] +"<#")defcheck_serial(serial):if (notset(serial).issubset(set(map(str,range(10))))):print ("only numbers allowed")returnFalseiflen(serial)!=20:returnFalseifint(serial[15])+int(serial[4])!=10:returnFalseifint(serial[1])*int(serial[18])!=2:returnFalseifint(serial[15])/int(serial[9])!=1:returnFalseifint(serial[17])-int(serial[0])!=4:returnFalseifint(serial[5])-int(serial[17])!=-1:returnFalseifint(serial[15])-int(serial[1])!=5:returnFalseifint(serial[1])*int(serial[10])!=18:returnFalseifint(serial[8])+int(serial[13])!=14:returnFalseifint(serial[18])*int(serial[8])!=5:returnFalseifint(serial[4])*int(serial[11])!=0:returnFalseifint(serial[8])+int(serial[9])!=12:returnFalseifint(serial[12])-int(serial[19])!=1:returnFalseifint(serial[9])%int(serial[17])!=7:returnFalseifint(serial[14])*int(serial[16])!=40:returnFalseifint(serial[7])-int(serial[4])!=1:returnFalseifint(serial[6])+int(serial[0])!=6:returnFalseifint(serial[2])-int(serial[16])!=0:returnFalseifint(serial[4])-int(serial[6])!=1:returnFalseifint(serial[0])%int(serial[5])!=4:returnFalseifint(serial[5])*int(serial[11])!=0:returnFalseifint(serial[10])%int(serial[15])!=2:returnFalseifint(serial[11])/int(serial[3])!=0:returnFalseifint(serial[14])-int(serial[13])!=-4:returnFalseifint(serial[18])+int(serial[19])!=3:returnFalsereturnTrueifcheck_serial(sys.argv[1]):print ("Thank you! Your product has been verified!")else:print ("I'm sorry that is incorrect. Please use a valid RoboCorpIntergalactic serial number")