From b64d0d368634693748b267263d825af024e69a28 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Wed, 9 Jun 2021 11:24:15 +0200
Subject: [PATCH] Testing rouding mode intanciation
---
src_colibri2/tests/solve/smt_fp/sat/dune.inc | 4 ++++
.../tests/solve/smt_fp/sat/rm_instanciation.smt2 | 7 +++++++
.../tests/solve/smt_fp/sat/rm_universal.smt2 | 5 +++++
src_colibri2/tests/solve/smt_fp/unsat/dune | 13 +++++++++++++
src_colibri2/tests/solve/smt_fp/unsat/dune.inc | 3 +++
.../solve/smt_fp/unsat/f32_f64_incompatible.smt2 | 5 -----
.../tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2 | 3 +++
7 files changed, 35 insertions(+), 5 deletions(-)
create mode 100644 src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
create mode 100644 src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2
create mode 100644 src_colibri2/tests/solve/smt_fp/unsat/dune
create mode 100644 src_colibri2/tests/solve/smt_fp/unsat/dune.inc
delete mode 100644 src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2
create mode 100644 src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2
diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index 06de62e82..ec4f35a99 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -13,6 +13,10 @@
(rule (alias runtest) (action (diff oracle recognize_float64.smt2.res)))
(rule (action (with-stdout-to recognize_rounding_mode.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:recognize_rounding_mode.smt2}))))
(rule (alias runtest) (action (diff oracle recognize_rounding_mode.smt2.res)))
+(rule (action (with-stdout-to rm_instanciation.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:rm_instanciation.smt2}))))
+(rule (alias runtest) (action (diff oracle rm_instanciation.smt2.res)))
+(rule (action (with-stdout-to rm_universal.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:rm_universal.smt2}))))
+(rule (alias runtest) (action (diff oracle rm_universal.smt2.res)))
(rule (action (with-stdout-to simple_add_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_add_float32.smt2}))))
(rule (alias runtest) (action (diff oracle simple_add_float32.smt2.res)))
(rule (action (with-stdout-to simple_eq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_eq_float32.smt2}))))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2 b/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
new file mode 100644
index 000000000..f88199943
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(declare-fun m () RoundingMode)
+(assert (not (= RNE m)))
+(assert (= (fp.add m x y) x))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2 b/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2
new file mode 100644
index 000000000..78a5beced
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(assert (forall ((m RoundingMode)) (= (fp.add m x y) x)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune b/src_colibri2/tests/solve/smt_fp/unsat/dune
new file mode 100644
index 000000000..6d9fe5883
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune
@@ -0,0 +1,13 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2)
+ (glob_files *.psmt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
new file mode 100644
index 000000000..21f859489
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
@@ -0,0 +1,3 @@
+(rule (action (with-stdout-to oracle (echo "unsat\n"))))
+(rule (action (with-stdout-to inf_pos_neg_neq.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:inf_pos_neg_neq.smt2}))))
+(rule (alias runtest) (action (diff oracle inf_pos_neg_neq.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2
deleted file mode 100644
index fdc81481a..000000000
--- a/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-(set-logic ALL)
-(declare-fun x () (_ FloatingPoint 11 53))
-(declare-fun y () (_ FloatingPoint 8 24))
-(assert (= x y))
-(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2
new file mode 100644
index 000000000..3e7669912
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ +oo 8 24) (_ -oo 8 24)))
+(check-sat)
\ No newline at end of file
--
GitLab