From: Andrew V. Jones <andrewvaughanj@gmail.com>
Date: Mon, 9 Aug 2021 18:01:37 +0000 (+0100)
Subject: Create grouping of tests that exercise '--use-approx' (#6958)
X-Git-Tag: cvc5-1.0.0~1391
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d1343b65765ffdcebfe856d11a6339337f862a3;p=cvc5.git

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