Z3Py 코드의 오류

Question

다음 스크립트의 내용이 잘못되었습니다 http://rise4fun.com/Z3Py/Cbl? 마지막 두 줄을 추가하는 것은 나에게 다음과 같은 오류 'instancemethod' object is not #subscriptable

x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next') 
location,location_next=Bools('location location_next') 
x=0 
location=BoolVal(False) 
k=20 
for i in range(k): 
s=Solver() 
s.add(Or(And(x_next-x>=2*t,x_next-x<=3*t,x_next<=12,t>0,Not(location)), 
     And(x_next-x>=-2*t,x_next-x<=-t,x_next>=0,t>0,location)),location_next==If(And(Not(location),x_next>=12),True,If(And(location,x_next<=0),False,location))) 

print s.check() 
print s.model() 
m=s.model 
#x=m[x_next] 
#location=m[location_next] 

Answer 1

m=s.model을 제공 m에 함수를 지정합니다.

m=s.model()