에 은밀 INT 분류 : 변수 X는Z3 : bitvector
bitvector 정렬로 X를 변환하는 임의의 방법이 있는가 하여 INT 정렬 정의 (선언 const가 지능 X)인가? 가끔 x가 &과 같은 비트 연산을 포함하기 때문에 int 이론은 처리 할 수 없습니다.
비트 연산을 제외하고 int 이론이 지원하는 연산 (예 : +, -, *, /)이 지원되는 연산보다 훨씬 빠르기 때문에 변수 x를 처음에는 비트 벡터로 정의하고 싶지 않습니다. bitvectors.
그래서 사실 int 정렬을 bitvector sort 또는 vise vesa로 변환하고 싶습니다.
감사합니다.
팅 첸
예, bv2int 및 int2bv 같은 것들을 사용할 수 있습니다. 비트 벡터 길이가 중요하며 int2bv는 파라 메트릭 (비트 벡터 길이가 필요함)에 유의하십시오.
(declare-fun x() (_ BitVec 32))
(declare-fun y() Int)
(declare-fun z() (_ BitVec 16))
(assert (= y 129))
(assert (= (bv2int x) y))
; (assert (= ((_ int2bv 32) y) x)) ; try with this uncommented
(assert (= ((_ int2bv 16) y) z))
(check-sat)
(get-model)
(get-value (x y z)) ; gives ((x #x00000000) (y 129) (z #x0081))
또 다른 예는 여기에 있습니다 : : 현재이 기능을 몇 가지 문제가있을 수 있습니다처럼
것 같습니다 여기
는 (: http://rise4fun.com/Z3/wxcp rise4fun 링크) 최소한의 예입니다 : Check overflow with Z3다른 해결사에서 다른 이름으로 호출 할 수도 있습니다 (bv2nat 및 nat2bv) : http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2