Create grouping of tests that exercise '--use-approx' (#6958)
authorAndrew V. Jones <andrewvaughanj@gmail.com>
Mon, 9 Aug 2021 18:01:37 +0000 (19:01 +0100)
committerGitHub <noreply@github.com>
Mon, 9 Aug 2021 18:01:37 +0000 (11:01 -0700)
commit2d1343b65765ffdcebfe856d11a6339337f862a3
treef533b2f6760df20816e88efd42288581330218aa
parent4e61cff7eb7fa26323f36e2784b252a869c210d9
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>
test/regress/CMakeLists.txt
test/regress/regress0/use_approx/bug812_approx.smt2 [new file with mode: 0644]
test/regress/regress0/use_approx/error0_approx.smt2 [new file with mode: 0644]
test/regress/regress0/use_approx/issue2429_approx.smt2 [new file with mode: 0644]
test/regress/regress0/use_approx/issue4714_approx.smt2 [new file with mode: 0644]
test/regress/regress0/use_approx/siegel-nl-bases_approx.smt2 [new file with mode: 0644]
test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 [new file with mode: 0644]