Testing rouding mode intanciation

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}))))

src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2

+(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

src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2 → src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2

 (set-logic ALL)
-(declare-fun x () (_ FloatingPoint 11 53))
+(declare-fun x () (_ FloatingPoint 8 24))
 (declare-fun y () (_ FloatingPoint 8 24))
-(assert (= x y))
+(assert (forall ((m RoundingMode)) (= (fp.add m x y) x)))
 (check-sat)
\ No newline at end of file

src_colibri2/tests/solve/smt_fp/unsat/dune

+(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))

src_colibri2/tests/solve/smt_fp/unsat/dune.inc

+(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)))

src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2

+(set-logic ALL)
+(assert (fp.eq (_ +oo 8 24) (_ -oo 8 24)))
+(check-sat)
\ No newline at end of file