Z3PY에서 배열 사용

Question

제 연구에 z3을 사용하고 있으며 다음과 같은 문제가 있습니다. 배열을 포함하는 만족스러운 수식의 모델을 분석 중이지만 모델 결과를 이해하지 못합니다. 예를 들어, 두 변수 'pkgcounter'와 'rxlen'과 두 개의 명제 p1과 p2가 있습니다. 제 목표는 두 가지 명제를 모두 만족시키는 모델이 있는지 알아 보는 것입니다.

[! -> 0] = [다른 pkgcounter - -> 0] = [다른 K> 0 0] rxlen = [다른]

pkgcounter = Array('pkgcounter',IntSort(),BitVecSort(8)) 

rxlen = Array('rxlen',IntSort(),BitVecSort(8)) 

s = Solver() 

p1 = (pkgcounter < rxlen) 

p2 = (pkgcounter == rxlen) 


s.add(p1,p2) 

if s.check() == sat: 

    print s.model() 

결과는 다음 모델

누군가이 결과를 해석하는 데 도움이 될 수 있습니까? rxlen과 pkgcounter가 0과 같은 모든 필드를 가지므로 명제 p1에는 모델이 없습니다. ArrayRef 객체가이 없기 때문에

Answer 1

Z3와 파이썬 사용의 버전으로 따라이 문제는 다른 결과를 얻을 수, 그들 모두 파이썬 2.7 (pkgcounter < rxlen)에서

p1 = (pkgcounter < rxlen) 

에 의해 트리거는 False로 단순화 < 연산자와 개체가 다릅니다. 반대로 Python 3.5는 이러한 객체가 주문되지 않는다고 불평합니다 (TypeError: unorderable types: ArrayRef() < ArrayRef()).

Z3의 배열에는 크기가 없습니다. 그것들이 정수에 의해 인덱싱된다면, 그것들은 실제로 무한 크기입니다. 따라서 이러한 배열은 이런 방식으로 비교 될 수 없으므로 (pkgcounter < rxlen)은이 문맥에서 의미가 없습니다. (SMT ArraysEx Theory 참조).

이 테스트 케이스가 만족스러운 이유는 이전 버전의 Z3이 사용 된 것일 수 있습니다. 최신 버전 (GitHub의 마스터 브랜치)에서는 이것이 만족스럽지 않지만 다시 그 이유는 p1이 False이기 때문입니다. 일반적

을 배열 변수 모델은 예를 들어 rxlen = [else -> 0] 함수 rxlen 배열의 요소를 검색하는 것을 의미 항상 0을 반환하는 함수이고, 함수 정의보고된다.

p3 = (rxlen[0] == 1) 

을 추가함으로써 우리는 첫 번째 위치에서 다른 값을 가지도록 rxlen 강제 할 수 있으며이 모델은 다음 rxlen = [0 -> 1, else -> 1]으로보고됩니다; 즉 은 0이고 1은 다른 모든 위치에 있습니다.