부동 소수점 리터럴

Question

Z3의 FPA의 논리에 의해 허용으로 나는, IEEE 부동 소수점 상수를 작성에 관한 두 가지 질문을했습니다 : 난

((_ asFloat 11 53) roundTowardZero 0.5 0)) 

: 먼저, this question에, 크리스토프는 예를 사용

최종 0이 무엇을 의미하는지 궁금하십니까? 나는 시도했다 :

((_ asFloat 11 53) roundTowardZero 0.5)) 

그리고 그것은 잘 작동하는 것처럼 보인다. Rummer의 paper은 마지막 0을 필요로하지 않습니다. 그래서 저는 그것이 어떤 역할을하는지 궁금합니다.

(as +1.0000000000000002220446049250313080847263336181640625p1 (_ FP 11 53)) 

가 어떻게이 p1 접미사를 해석합니까 : 나는 Z3로부터 모델을 얻을 때

둘째, 그것은과 같이 부동 소수점 리터럴을 인쇄? 가능한 다른 접미사는 무엇입니까?

감사합니다.

Answer 1

감사합니다. 둘 다 입력 또는 출력에서 ​​아직 부동 소수점 리터럴에 대한 합의 된 표준이 없기 때문입니다.

이 예의 최종 0은 (이원) 지수, 즉 (... 0.5 1) == 1.0을 나타냅니다. 지수를 별도로 지정할 수없는 경우 숫자에 때로는 많은 공간이 필요하기 때문에 간단히 추가했습니다. 이렇게하면 우리는 종종 간결하게 지정할 수 있습니다.

출력에서 ​​p1 접미사는 이진 지수가 e810^8 수단 곳, 즉, 접미사가 p82^8를 의미를 나타낸다. Z3은 현재 이진 지수 만 사용하므로 여기에 항상 p 접미사가 있지만 앞으로 변경 될 수 있습니다. 나머지 숫자에는 정확한 결과를 나타 내기에 충분한 십진수가 지정됩니다.

출력 형식은 아직 SMT 커뮤니티에서 합의하지 않았습니다. 이것은 미래에 바뀔 수 있습니다. 예를 들어, 이것이 IEEE 비트 벡터 형식으로 수행되어야하는지 아니면 실수 비트와 비 IEEE 비트 벡터 사이에 놓이는 중간 형식인지에 대한 논의가 있습니다.