Z3py에서 왜 분단을 해석되지 않은 함수로 단순화합니까?

Question

TL : simplify을 사용할 때 비트 벡터 분할 노드가 Z3_OP_BSDIV에서 Z3_OP_UNINTERPRETED으로 변경됩니다. 어떻게 해석 할 수없는 작전에서 부서 작전을 말할 수 있습니까?

설명 :

다음 세션이 그 비트 벡터 부문은 해석 보여 주지만, simplify() 사용 후,이 해석되지 않습니다. 아래의 변수 d을 어떻게 사용하는지 확인하십시오.

>>> x, y = BitVecs('x y', 32) 
>>> n = x/y 
>>> n.decl().kind() 
1031L 
>>> d = simplify(x/y) 
>>> d.decl().kind() 
2051L 

우리는 수동으로 선언 된 해석의 기능과 UDiv뿐만 아니라 같은 종류를 볼 수 있습니다.

>>> foo = Function('foo', BitVecSort(32), BitVecSort(32), BitVecSort(32)) 
>>> u = foo(x, y) 
>>> u.decl().kind() 
2051L 
>>> d1 = simplify(UDiv(x,y)) 
>>> d1.decl().kind() 
2051L 

그러나 해결에 영향을 미치지 않는 것처럼 보입니다. 해석자는 여전히 작업을 실제 나누기로 해석하는 것 같습니다. 그 kind이 Z3_OP_UNINTERPRETED하더라도, 그것은 정말 해석 있다는 알 수있는 방법이 -

>>> prove(d != 400) 
counterexample 
[y = 1, x = 400] 

나는 그 종류로 노드를 처리하기 위해 노력하고 있지만,이 사람은 그 종류에 대해 "거짓말"에 보인다? 이거 버그 야?

Answer 1

이것은 반드시 버그 일 필요는 없습니다. bvudiv/bvsdiv 연산자의 결과는 분모가 0 일 때 정의되지 않습니다 (QF_BV logic definition 참조). 따라서 "x/y"의 결과는 정의되지 않은 것으로 간주 될 수 있으며 다른 제약 조건이 없으면 해석되지 않은 함수로 대체됩니다. 결과적으로 비트 벡터 수식의 단순화는 해석되지 않은 함수가 단순화 된 용어로 나타날 수 있다는 점을 고려해야합니다.