2
SMTLIB2에서 BitVector와 FP간에 변환 할 수있는 방법이 있습니까? int2bv 및 bv2int 함수와 비슷합니다.Z3 : FP와 BitVector간에 변환 하시겠습니까?
명확히하기 위해 BitVec 형식의 반올림 된 정수가 아닌 비트의 원시 표현을 찾고 있습니다.
A
답변
5
정확하게 말하자면, SMTLIB에서 부동 소수점 연산에 대한 표준은 아직 없습니다. 이것에 대한 초안이 나중에 확정 될 것입니다; 이 초안은 현재 그러한 기능을 포함하지 않습니다. 그러나 Z3은 QF_FPABV 로직이 활성화 된 경우 이러한 변환 기능을 지원합니다. 부동 소수점에 대한 SMT 이론이 완료되었습니다 : http://smtlib.cs.uiowa.edu/theories
이 기능은
asIEEEBV (takes a float and returns a BV in IEEE764 format of appropriate size)
이 하나에
fromIEEEBV (takes a BV in IEEE764 format and returns a float of appropriate size)
관련 문제
- 1. IR을 Z3 공식으로 변환 하시겠습니까?
- 2. Z3 : Z3py 표현식을 SMT-LIB2로 변환 하시겠습니까?
- 3. Z3 : BoolRef를 BitVecVal로 변환
- 4. C# 문을 z3 형식으로 변환
- 5. Z3 : Z3 소개 int2bv?
- 6. Z3
- 7. Z3
- 8. Z3
- 9. Microsoft Z3 : 표현식을 특정 변수로 변환
- 10. Z3py : picosat에서 사용 조항에 Z3 공식을 변환
- 11. Z3/파이썬 실수 Z3/파이썬 웹 인터페이스와
- 12. Z3 : Z3 API를 지원 명명 된
- 13. Z3 -smt2 -in : Z3 버전 가져 오기
- 14. z3 바이너리와 z3 api 간의 결과가 다릅니다
- 15. Z3 : Z3 C API에서 알 수없는 결과
- 16. Z3 : 일정 수에서 추출하는 방법()? 다음과 같은 Z3 파이썬에서
- 17. 는 Z3
- 18. Z3 : bitvector
- 19. z3 C++ API ast (또는 solver) 객체를 SMTLIB 문자열로 변환
- 20. 비트 벡터 (SMTLIB2, Z3)에 값을 할당 하시겠습니까?
- 21. Z3 타이밍 변형
- 22. Z3 3.2에서 통계를 얻는 방법? Z3 2.x를 가진
- 23. Z3 Java API : 표현식/Z3 객체를 언제 처리할까요?
- 24. Z3 : Z3 파이썬에서 If-the-else를 인코딩하는 방법?
- 25. Z3 파일 읽기
- 26. Python의 Z3 코드
- 27. Z3 이론 플러그인 오류
- 28. Z3 솔버 복사
- 29. Z3 : 모델이 고유한지 확인하십시오.
- 30. Z3 대체 (Java)
업데이트라고합니다 /FloatingPoint.smt2 Z3은 표준에서 이러한 기능을 정확하게 지원하며 모든 이전 연산자가 제거되었습니다. –