From 2d1343b65765ffdcebfe856d11a6339337f862a3 Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Mon, 9 Aug 2021 19:01:37 +0100 Subject: [PATCH] Create grouping of tests that exercise '--use-approx' (#6958) Currently, it seems that `cvc5` has no tests that get anywhere near close to exercising the code in `approx_simplex`, which means that the GLPK integration is effectively untested in CI: * https://cvc4.cs.stanford.edu/downloads/builds/coverage/cvc5-2021-08-02/index.src_theory_arith_approx_simplex.cpp.html (which is at 2.8% at the time of writing!) Indeed, if you run the whole of `ctest`, none of the code near GLPK is exercised; and, worse, there are *no* regression tests that use `--use-approx`! This commit adds a selection of simple tests that have been derived (using `cvc5`'s existing regression suite and ddSMT) to reach code inside of `approx_simplex`; namely: - `solveRelaxation`, and - `solveMIP` This is (hopefully) an initial start that will allow us to grow more regression tests exercising GLPK (e.g., following the same process of reduction, but using the SMTLIB benchmarks vs. only `cvc5`'s regression suite). The folder structure has been named such that I can do `ctest -R "use_approx"` to run only the tests that (should) reach GLPK. Signed-off-by: Andrew V. Jones --- test/regress/CMakeLists.txt | 6 ++++++ .../regress0/use_approx/bug812_approx.smt2 | 17 +++++++++++++++++ .../regress0/use_approx/error0_approx.smt2 | 13 +++++++++++++ .../regress0/use_approx/issue2429_approx.smt2 | 12 ++++++++++++ .../regress0/use_approx/issue4714_approx.smt2 | 11 +++++++++++ .../use_approx/siegel-nl-bases_approx.smt2 | 14 ++++++++++++++ ...rd.15.RTE.Terminate_System.Int32_approx.smt2 | 14 ++++++++++++++ 7 files changed, 87 insertions(+) create mode 100644 test/regress/regress0/use_approx/bug812_approx.smt2 create mode 100644 test/regress/regress0/use_approx/error0_approx.smt2 create mode 100644 test/regress/regress0/use_approx/issue2429_approx.smt2 create mode 100644 test/regress/regress0/use_approx/issue4714_approx.smt2 create mode 100644 test/regress/regress0/use_approx/siegel-nl-bases_approx.smt2 create mode 100644 test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 83d240b6b..2706dee8a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1425,6 +1425,12 @@ set(regress_0_tests regress0/unconstrained/mult1.smt2 regress0/unconstrained/uf1.smt2 regress0/unconstrained/xor.smt2 + regress0/use_approx/bug812_approx.smt2 + regress0/use_approx/error0_approx.smt2 + regress0/use_approx/issue2429_approx.smt2 + regress0/use_approx/issue4714_approx.smt2 + regress0/use_approx/siegel-nl-bases_approx.smt2 + regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 regress0/wiki.01.cvc regress0/wiki.02.cvc regress0/wiki.03.cvc diff --git a/test/regress/regress0/use_approx/bug812_approx.smt2 b/test/regress/regress0/use_approx/bug812_approx.smt2 new file mode 100644 index 000000000..4b5af6710 --- /dev/null +++ b/test/regress/regress0/use_approx/bug812_approx.smt2 @@ -0,0 +1,17 @@ +; REQUIRES: glpk +; COMMAND-LINE: --use-approx +; EXPECT: unknown +(set-logic UFNIA) +(set-info :source "Reduced from regression 'bug812.smt2' using ddSMT to exercise GLPK") +(set-info :smt-lib-version 2.6) +(set-info :category "crafted") +(set-info :status unknown) +(declare-fun s (Int Int) Int) +(declare-fun P (Int Int Int) Int) +(declare-fun p (Int) Int) +(declare-fun H (Int Int) Int) +(declare-fun H (Int Int Int) Int) +(declare-fun R (Int Int) Int) +(assert (and (forall ((? Int)) (! (= (R ? 0) (s 0 0)) :pattern ((P 0 ? 0)))) (forall ((x Int)) (! false :pattern ((s x (s 0 0)) (s x (H 0 0))))) (forall ((? Int)) (! (exists ((k Int)) (= (* ? k) (- 1 (s 0 0)))) :pattern ((R ? 0)))) (forall ((x Int) (? Int) (z Int)) (! (= 0 (s (H 0 0) (P 0 ? (H 0 0)))) :pattern ((H x ? z)))))) +(assert (= 0 (H (s 0 0) 2 (p 0)))) +(check-sat) diff --git a/test/regress/regress0/use_approx/error0_approx.smt2 b/test/regress/regress0/use_approx/error0_approx.smt2 new file mode 100644 index 000000000..472ec24f7 --- /dev/null +++ b/test/regress/regress0/use_approx/error0_approx.smt2 @@ -0,0 +1,13 @@ +; REQUIRES: glpk +; COMMAND-LINE: --use-approx +; EXPECT: sat +(set-logic QF_UFLIA) +(set-info :source "Reduced from regression 'error0.smt2' using ddSMT to exercise GLPK") +(set-info :smt-lib-version 2.6) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun a () Int) +(declare-fun x (Int) Int) +(assert (> 0 (+ a (* 2 (x 0))))) +(assert (< 0 (+ a 1))) +(check-sat) diff --git a/test/regress/regress0/use_approx/issue2429_approx.smt2 b/test/regress/regress0/use_approx/issue2429_approx.smt2 new file mode 100644 index 000000000..38da256ca --- /dev/null +++ b/test/regress/regress0/use_approx/issue2429_approx.smt2 @@ -0,0 +1,12 @@ +; REQUIRES: glpk +; COMMAND-LINE: --use-approx +; EXPECT: sat +(set-logic QF_UFLIA) +(set-info :source "Reduced from regression 'issue2429.smt2' using ddSMT to exercise GLPK") +(set-info :smt-lib-version 2.6) +(set-info :category "crafted") +(set-info :status sat) +(declare-const x5 Int) +(declare-const x Int) +(assert (> (+ x (* 4 x5)) 1)) +(check-sat) diff --git a/test/regress/regress0/use_approx/issue4714_approx.smt2 b/test/regress/regress0/use_approx/issue4714_approx.smt2 new file mode 100644 index 000000000..444d5f851 --- /dev/null +++ b/test/regress/regress0/use_approx/issue4714_approx.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: glpk +; COMMAND-LINE: --use-approx +; EXPECT: sat +(set-logic UFNIRA) +(set-info :source "Reduced from regression 'issue2429.smt2' using ddSMT to exercise GLPK") +(set-info :smt-lib-version 2.6) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun c (Int) Int) +(assert (exists ((l Int) (k Int)) (and (< 0 l) (< l (- (c k) 1)) (distinct 0 (mod (mod 0 (c 0)) (c k)))))) +(check-sat) diff --git a/test/regress/regress0/use_approx/siegel-nl-bases_approx.smt2 b/test/regress/regress0/use_approx/siegel-nl-bases_approx.smt2 new file mode 100644 index 000000000..4f5573258 --- /dev/null +++ b/test/regress/regress0/use_approx/siegel-nl-bases_approx.smt2 @@ -0,0 +1,14 @@ +; REQUIRES: glpk +; COMMAND-LINE: --use-approx +; EXPECT: sat +(set-logic QF_NIA) +(set-info :source "Reduced from regression 'issue4714.smt2' using ddSMT to exercise GLPK") +(set-info :smt-lib-version 2.6) +(set-info :category "crafted") +(set-info :status sat) +(declare-const x Bool) +(declare-const n Int) +(declare-const j Int) +(assert (< j n)) +(assert (or x (= 0 (+ n j)))) +(check-sat) diff --git a/test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 b/test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 new file mode 100644 index 000000000..729c5cdd2 --- /dev/null +++ b/test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 @@ -0,0 +1,14 @@ +; REQUIRES: glpk +; COMMAND-LINE: --use-approx +; EXPECT: unsat +(set-logic UFNIA) +(set-info :source "Reduced from regression 'specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2' using ddSMT to exercise GLPK") +(set-info :smt-lib-version 2.6) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun s (Int Int Int) Int) +(declare-fun x (Int Int) Int) +(declare-fun x_ (Int Int) Int) +(assert (and (forall ((? Int)) (! (= (x_ 0 0) (- ? (x_ 0 0))) :pattern ((x ? 1)) :pattern ((x_ 0 0)))))) +(assert (and (distinct 0 (s 0 0 0)) (= 0 (x (s 0 0 0) 1)))) +(check-sat) -- 2.30.2