+ def test_fmadd_f8_rne_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RNE,
+ negate_addend=False, negate_product=False)
+
+ def test_fmsub_f8_rne_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RNE,
+ negate_addend=True, negate_product=False)
+
+ def test_fnmadd_f8_rne_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RNE,
+ negate_addend=True, negate_product=True)
+
+ def test_fnmsub_f8_rne_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RNE,
+ negate_addend=False, negate_product=True)
+
+ def test_fmadd_f8_rtz_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTZ,
+ negate_addend=False, negate_product=False)
+
+ def test_fmsub_f8_rtz_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTZ,
+ negate_addend=True, negate_product=False)
+
+ def test_fnmadd_f8_rtz_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTZ,
+ negate_addend=True, negate_product=True)
+
+ def test_fnmsub_f8_rtz_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTZ,
+ negate_addend=False, negate_product=True)
+
+ def test_fmadd_f8_rtp_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTP,
+ negate_addend=False, negate_product=False)
+
+ def test_fmsub_f8_rtp_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTP,
+ negate_addend=True, negate_product=False)
+
+ def test_fnmadd_f8_rtp_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTP,
+ negate_addend=True, negate_product=True)
+
+ def test_fnmsub_f8_rtp_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTP,
+ negate_addend=False, negate_product=True)
+
+ def test_fmadd_f8_rtn_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTN,
+ negate_addend=False, negate_product=False)
+
+ def test_fmsub_f8_rtn_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTN,
+ negate_addend=True, negate_product=False)
+
+ def test_fnmadd_f8_rtn_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTN,
+ negate_addend=True, negate_product=True)
+
+ def test_fnmsub_f8_rtn_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTN,
+ negate_addend=False, negate_product=True)
+
+ def test_fmadd_f8_rna_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RNA,
+ negate_addend=False, negate_product=False)
+
+ def test_fmsub_f8_rna_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RNA,
+ negate_addend=True, negate_product=False)
+
+ def test_fnmadd_f8_rna_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RNA,
+ negate_addend=True, negate_product=True)
+
+ def test_fnmsub_f8_rna_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RNA,
+ negate_addend=False, negate_product=True)
+
+ def test_fmadd_f8_rtop_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTOP,
+ negate_addend=False, negate_product=False)
+
+ def test_fmsub_f8_rtop_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTOP,
+ negate_addend=True, negate_product=False)
+
+ def test_fnmadd_f8_rtop_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTOP,
+ negate_addend=True, negate_product=True)
+
+ def test_fnmsub_f8_rtop_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTOP,
+ negate_addend=False, negate_product=True)
+
+ def test_fmadd_f8_rton_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTON,
+ negate_addend=False, negate_product=False)
+
+ def test_fmsub_f8_rton_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTON,
+ negate_addend=True, negate_product=False)
+
+ def test_fnmadd_f8_rton_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTON,
+ negate_addend=True, negate_product=True)
+
+ def test_fnmsub_f8_rton_formal(self):
+ self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
+ rm=FPRoundingMode.RTON,
+ negate_addend=False, negate_product=True)
+
+ @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
+ "ENABLE_FMA_F16_FORMAL not in environ")