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 <andrewvaughanj@gmail.com>

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 83d240b6bc5e57bd692261da13f2fd27a71668ae..2706dee8af176df543322a3f9c108942d35cf9bd 100644 (file)
--- 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 (file)
index 0000000..4b5af67
--- /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 (file)
index 0000000..472ec24
--- /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 (file)
index 0000000..38da256
--- /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 (file)
index 0000000..444d5f8
--- /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 (file)
index 0000000..4f55732
--- /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 (file)
index 0000000..729c5cd
--- /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)