From d0a9a8fea3f39ee5606e9cb390ad06484291c90e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 19 Dec 2022 10:52:52 +0100
Subject: [PATCH] [Tests] Tests for ceil and floor
---
colibri2/tests/solve/all/both/ceil1.smt2 | 13 ++++++
colibri2/tests/solve/all/both/ceil2.smt2 | 13 ++++++
colibri2/tests/solve/all/both/dune | 13 ++++++
colibri2/tests/solve/all/both/dune.inc | 18 +++++++++
colibri2/tests/solve/all/both/floor1.smt2 | 13 ++++++
colibri2/tests/solve/all/unsat/dune.inc | 3 ++
colibri2/tests/solve/smt_nra/both/dune | 12 ++++++
colibri2/tests/solve/smt_nra/both/dune.inc | 6 +++
colibri2/tests/solve/smt_nra/both/propa1.smt2 | 40 +++++++++++++++++++
9 files changed, 131 insertions(+)
create mode 100644 colibri2/tests/solve/all/both/ceil1.smt2
create mode 100644 colibri2/tests/solve/all/both/ceil2.smt2
create mode 100644 colibri2/tests/solve/all/both/dune
create mode 100644 colibri2/tests/solve/all/both/dune.inc
create mode 100644 colibri2/tests/solve/all/both/floor1.smt2
create mode 100644 colibri2/tests/solve/smt_nra/both/dune
create mode 100644 colibri2/tests/solve/smt_nra/both/dune.inc
create mode 100644 colibri2/tests/solve/smt_nra/both/propa1.smt2
diff --git a/colibri2/tests/solve/all/both/ceil1.smt2 b/colibri2/tests/solve/all/both/ceil1.smt2
new file mode 100644
index 000000000..ca23f5937
--- /dev/null
+++ b/colibri2/tests/solve/all/both/ceil1.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+
+(assert (= x1 (colibri_ceil x2)))
+
+(assert (<= 2.5 x2 3.5))
+
+(assert (! (<= 3 x1 4) :colibri2 goal))
+
+
+(check-sat)
diff --git a/colibri2/tests/solve/all/both/ceil2.smt2 b/colibri2/tests/solve/all/both/ceil2.smt2
new file mode 100644
index 000000000..8e173e5b5
--- /dev/null
+++ b/colibri2/tests/solve/all/both/ceil2.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+
+(assert (= x1 (colibri_ceil x2)))
+
+(assert (<= (- 3.5) x2 (- 2.5)))
+
+(assert (! (<= (- 3) x1 (- 2)) :colibri2 goal))
+
+
+(check-sat)
diff --git a/colibri2/tests/solve/all/both/dune b/colibri2/tests/solve/all/both/dune
new file mode 100644
index 000000000..b1c6bc252
--- /dev/null
+++ b/colibri2/tests/solve/all/both/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} . both)))
+ (mode promote))
diff --git a/colibri2/tests/solve/all/both/dune.inc b/colibri2/tests/solve/all/both/dune.inc
new file mode 100644
index 000000000..0a6481640
--- /dev/null
+++ b/colibri2/tests/solve/all/both/dune.inc
@@ -0,0 +1,18 @@
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal
+--dont-print-result %{dep:ceil1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal --learning --dont-print-result %{dep:ceil1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:ceil1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ceil1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal
+--dont-print-result %{dep:ceil2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal --learning --dont-print-result %{dep:ceil2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:ceil2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ceil2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal
+--dont-print-result %{dep:floor1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal --learning --dont-print-result %{dep:floor1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:floor1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:floor1.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/all/both/floor1.smt2 b/colibri2/tests/solve/all/both/floor1.smt2
new file mode 100644
index 000000000..e6c3904ae
--- /dev/null
+++ b/colibri2/tests/solve/all/both/floor1.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+
+(assert (= x1 (colibri_floor x2)))
+
+(assert (<= 2.5 x2 3.5))
+
+(assert (! (<= 2 x1 3) :colibri2 goal))
+
+
+(check-sat)
diff --git a/colibri2/tests/solve/all/unsat/dune.inc b/colibri2/tests/solve/all/unsat/dune.inc
index c84d1e6c6..584dd91c3 100644
--- a/colibri2/tests/solve/all/unsat/dune.inc
+++ b/colibri2/tests/solve/all/unsat/dune.inc
@@ -55,3 +55,6 @@
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:work_with_fourier_not_simplex2.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:work_with_fourier_not_simplex2.psmt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_nra/both/dune b/colibri2/tests/solve/smt_nra/both/dune
new file mode 100644
index 000000000..0807a2205
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/both/dune
@@ -0,0 +1,12 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . both)))
+ (mode promote))
diff --git a/colibri2/tests/solve/smt_nra/both/dune.inc b/colibri2/tests/solve/smt_nra/both/dune.inc
new file mode 100644
index 000000000..bfd9904d2
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/both/dune.inc
@@ -0,0 +1,6 @@
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal
+--dont-print-result %{dep:propa1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal --learning --dont-print-result %{dep:propa1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:propa1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:propa1.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_nra/both/propa1.smt2 b/colibri2/tests/solve/smt_nra/both/propa1.smt2
new file mode 100644
index 000000000..c9b3bc02c
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/both/propa1.smt2
@@ -0,0 +1,40 @@
+(set-logic ALL)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+
+(assert (< 1 x 10))
+(assert (and (< 1 y) (<= y 10)))
+
+(define-fun f ((a Real)(b Real)) Real (+ (/ (/ (- (* x y) y) (+ y 1)) 12.0) 1))
+
+(define-fun z1_1 () Real (f x y))
+(define-fun z2_1 () Real (f y x))
+
+(define-fun z1_2 () Real (f z1_1 z2_1))
+(define-fun z2_2 () Real (f z2_1 z1_1))
+
+(define-fun z1_3 () Real (f z1_2 z2_2))
+(define-fun z2_3 () Real (f z2_2 z1_2))
+
+(define-fun z1_4 () Real (f z1_3 z2_3))
+(define-fun z2_4 () Real (f z2_3 z1_3))
+
+(define-fun z1_5 () Real (f z1_4 z2_4))
+(define-fun z2_5 () Real (f z2_4 z1_4))
+
+(define-fun z1_6 () Real (f z1_5 z2_5))
+(define-fun z2_6 () Real (f z2_5 z1_5))
+
+(define-fun z1_7 () Real (f z1_6 z2_6))
+(define-fun z2_7 () Real (f z2_6 z1_6))
+
+(define-fun z1_8 () Real (f z1_7 z2_7))
+(define-fun z2_8 () Real (f z2_7 z1_8))
+
+(define-fun z1_9 () Real (f z1_8 z2_8))
+(define-fun z2_9 () Real (f z2_8 z1_8))
+
+
+(assert (! (and (< 0.0 z1_9 10.0) (< 0.0 z2_9 10.0)) :colibri2 goal))
+(check-sat)
--
GitLab