z3py에서 Extract 노드의 경계를 검색하십시오.

Question

z3py를 사용하고 있습니다. 내 질문은, 어떻게 Extract 노드의 경계를 검색합니까? 내가 Extract이 인수에 대응 세와 함수가 될 것이라고 생각하지만, 그렇지 않은 :

>>> x = BitVecVal(3, 32) 
>>> e = Extract(15, 0, x) 
>>> e.decl() 
Extract 
>>> e.decl().arity() 
1 
>>> e2 = Extract(7, 0, x) 
>>> e2.decl() 
Extract 
>>> e.decl() == e2.decl() 
False 

각 Extract 작업은 처음 두 개의 인수로 (분명히) 입력 된합니다 (decls 동일하지 않기 때문에 나는이 추론).

Extract 조작 인 BitVecRef이 주어진다면, 조작의 한계를 어떻게 알 수 있습니까? 그래서 Extract(i, j, x)에 대해 나는 i과 j을 돌려주는 함수를 원한다.

Answer 1

경계는 용어와 함께 "매개 변수"로 인코딩됩니다. 이 매개 변수는 일반 인수로 전달되지 않습니다. 파이썬 API는 매개 변수에 대한 액세스를 노출하지 않지만 C API는 파이썬에서 이러한 함수를 호출 할 수 있습니다.

필요한 기능은 Z3_get_decl_int_parameter입니다.

다음은 함수를 사용하여 샘플입니다 : http://rise4fun.com/Z3Py/Rsl8

x = BitVec('x',32) 
t = Extract(10,5,x) 

f = t.decl() 
print Z3_get_decl_int_parameter(t.ctx.ref(), f.ast, 0) 
print Z3_get_decl_int_parameter(t.ctx.ref(), f.ast, 1)