z3py의 Z3-LIB에서 (_ map op) 사용 방법

Question

Z3-LIB는 (_ map op)와 같은 확장 배열 이론의 연산자를 지원합니다. 하지만 Z3py에서이 연산자를 어떻게 사용할 수 있습니까?

Answer 1

사용자는 A1, A2 및 B 배열 변수

b = Map(f, a1, a2) 

를 사용할 수있다. 첫 번째 매개 변수 f는 함수 선언이어야합니다. 예를 들어, z3.And는 나를 위해 작동하지 않습니다. 대신, 나는 And와 동등한 커스텀 함수 f와 또 다른 공리를 도입했습니다. 하지만 미리 정의 된 것을 필요로하지 않을 수도 있습니다.