z3 Python API를 사용하여 bv-redand를 어떻게 인코딩합니까?

Question

내가 Z3 파이썬 API를 사용하여 다음과 같은 표현 같은 것을 인코딩 할 가정 :

(bv-redand 
    (bv-or 
     (bv-xnor symbolic_bit_0 
      (bv-concat src_ip dst_ip src_port dst_port)) 
     symbolic_dc_0))))) 

어떻게 이런 짓을 했을까?

내가 좋아하는 뭔가를해야 나타납니다

And(~(symbolic_bit_0^Concat(src_ip dst_ip src_port dst_port)) | symbolic_dc_0) 

그러나 바깥 쪽 그리고 작동하지 않습니다. 내가 생각할 수있는 한 가지 해킹은 And를 피하고 모든 1과 비교하는 것이지만 더 좋은 방법이 있습니까?

사이드 노트에서 ~ (a^b) 대신 Xnor b를 직접 지정하는 방법이 있습니까?

Answer 1

감소 및 줄이기 - 또는 아직 Python API에 추가되지 않았습니다. Reduction-And는 'normal and'와는 상당히 다릅니다. 이제 불안정한 지점에 추가했습니다. 참고 및 향후 사용을 위해 C-API에는 있지만 파이썬 API에는없는 함수를 추가 할 수 있습니다. 예를 들어,이 경우에 정의 할 수 있습니다.

다른 부울 연산자는 파이썬과 동등하지만 XNor는 이에 해당하지 않습니다. 따라서 해당 기능이 추가되지 않았습니다. 그러나 원하는 경우 다시 정의 할 수 있습니다.

def BVXNor(a, b): 
    return BitVecRef(Z3_mk_bvxnor(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 

성능 차이는 무시해도 좋습니다.