nouveaux benchs qf_fp

UnitTests/sat/QF_FP/square_id_fp_sat.smt2

+
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FP)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status sat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+
+(define-fun one () Float64
+  ((_ to_fp 11 53) (_ bv4607182418800017408 64)))
+
+(define-fun two () Float64
+  ((_ to_fp 11 53) (_ bv4611686018427387904 64)))
+
+(define-fun xpy2 () Float64
+  (fp.mul RNE (fp.add RNE dx dy) (fp.add RNE dx dy)))
+
+(define-fun id_xpy2 () Float64
+  (fp.add RNE (fp.add RNE (fp.mul RNE dx dx) (fp.mul RNE dy dy))
+	  (fp.mul RNE two (fp.mul RNE dx dy))))
+
+(define-fun isInsideAbsMax ((xx Float64) (max Float64)) Bool
+  (and
+   (isFinite xx)
+   (fp.leq (fp.neg max) xx max)))
+
+(define-fun diff () Float64
+  (fp.sub RNE xpy2 id_xpy2))
+
+(define-fun max_diff () Float64
+;; 2^-53
+  ((_ to_fp 11 53) (_ bv4368491638549381120 64)))
+ 
+(assert
+ (not
+  (=>
+   (and (isInsideAbsMax dx one)
+	(not (fp.isZero dx))
+	(isInsideAbsMax dy one)
+	(not (fp.isZero dy))
+	(isFinite diff))
+   (isInsideAbsMax diff max_diff))))
+
+(check-sat)
+

UnitTests/sat/QF_FP/square_neg_id_fp_sat.smt2

+
+(set-info :smt-lib-version 2.6)
+(set-logic ALL)
+(set-info :category |Crafted from GATeL POs|)
+;(set-info :status sat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+
+(define-fun one () Float64
+  ((_ to_fp 11 53) (_ bv4607182418800017408 64)))
+
+(define-fun two () Float64
+  (fp #b0 #b10000000000 #b0000000000000000000000000000000000000000000000000000))
+
+(define-fun xmy2 () Float64
+  (fp.mul RNE (fp.sub RNE dx dy) (fp.sub RNE dx dy)))
+
+(define-fun id_xmy2 () Float64
+  (fp.sub RNE (fp.add RNE (fp.mul RNE dx dx) (fp.mul RNE dy dy))
+	  (fp.mul RNE two (fp.mul RNE dx dy))))
+
+(define-fun isInsideAbsMax ((x Float64) (max Float64)) Bool
+  (and
+   (isFinite x)
+   (fp.leq (fp.neg max) x max)))
+
+(define-fun diff () Float64
+  (fp.sub RNE xmy2 id_xmy2))
+
+(define-fun max_diff () Float64
+;; 2^-53
+  ((_ to_fp 11 53) (_ bv4368491638549381120 64)))
+
+(assert
+ (not
+  (=>
+   (and (isInsideAbsMax dx one)
+	(not (fp.isZero dx))
+	(isInsideAbsMax dy one)
+	(not (fp.isZero dy))
+	(isFinite diff))
+   (isInsideAbsMax diff max_diff))))
+
+(check-sat)
+