새로운 FP 로직을 실험하고 있습니다. 아아, FMA와 관련된 가장 간단한 쿼리조차도 z3에 상당한 문제를 일으키는 것 같습니다.
다음은 내가 증명하기 위해 노력 하나의 예이다 x*y+0같다 fma(x,y,0). 그것은 여분의 몇 가지를 확인하기 위해 수행 x하고 y없는 NaN평등은 참으로 개최 할 수 있도록 등이야. 이 벤치 마크가 많은 문제를 일으키는 이유가 z3있습니까?
내 z3버전 :Z3 [version 4.3.2 - 64 bit - build hashcode 728835357594].
(set-option :produce-models true)
(set-logic QF_FPA)
(define-fun s3 () (_ FP 8 24) (as plusInfinity (_ FP 8 24)))
(define-fun s5 () (_ FP 8 24) (as minusInfinity (_ FP 8 24)))
(define-fun s17 () (_ FP 8 24) ((_ asFloat 8 24) roundNearestTiesToEven (/ 0 1)))
(declare-fun s0 () (_ FP 8 24))
(declare-fun s1 () (_ FP 8 24))
(assert
(let ((s2 (== s0 s0)))
(let ((s4 (< s0 s3)))
(let ((s6 (> s0 s5)))
(let ((s7 (and s4 s6)))
(let ((s8 (and s2 s7)))
(let ((s9 (== s1 s1)))
(let ((s10 (< s1 s3)))
(let ((s11 (> s1 s5)))
(let ((s12 (and s10 s11)))
(let ((s13 (and s9 s12)))
(let ((s14 (and s8 s13)))
(let ((s15 (not s14)))
(let ((s16 (* roundNearestTiesToEven s0 s1)))
(let ((s18 (+ roundNearestTiesToEven s16 s17)))
(let ((s19 (fusedMA roundNearestTiesToEven s0 s1 s17)))
(let ((s20 (== s18 s19)))
(let ((s21 (or s15 s20)))
(not s21)))))))))))))))))))
(check-sat)
Z3는 부동 소수점 수식을 비트 벡터 수식 (및 SAT)으로 변환하여 해결합니다. 일부 공식 (예 : ACDCL 기반 또는 일부 근사 개선)에서는 이보다 더 빠른 방법이 있지만이 특정 공식에서는 모두 성능이 저하 될 것으로 예상합니다. 곱셈 (및 유사) 제약 조건은 일반적으로 기본 엔진에 어렵고 곱셈이 일부 속성을 보존한다는 것을 증명하는 것은 훨씬 더 어렵습니다.
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다