From 080f0de4379c4e1fe5a016e40c7852a3abb52760 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 7 May 2021 16:30:48 -0700 Subject: [PATCH] Move slow regressions and update guidelines. (#6508) This moves regression test that exceed the time limit of their respective level to the appropriate level. It further updates the guidelines in the README with information on how to properly categorize regression tests into levels (with time limits). Note: Test regress3/issue4717.smt2 was previously unsolved (unknown) and is now sat (Z3 agrees). --- test/regress/CMakeLists.txt | 25 ++++++++++--------- test/regress/README.md | 22 ++++++++++++---- ...le_startup_9nodes.abstract.base.smtv1.smt2 | 0 .../nl/ufnia-factor-open-proof.smt2 | 0 .../quantifiers/issue3481-unsat1.smt2 | 0 .../arith/abz5_1400.smtv1.smt2 | 0 .../{regress2 => regress3}/error0.smt2 | 0 .../{regress2 => regress3}/ho/SYO362^5.p | 0 test/regress/regress3/issue4714.smt2 | 2 +- .../nl/iand-native-1.smt2 | 0 .../quantifiers/ForElimination-scala-9.smt2 | 0 .../quantifiers/javafe.ast.ArrayInit.35.smt2 | 0 .../siegel-nl-bases.smt2 | 0 13 files changed, 31 insertions(+), 18 deletions(-) rename test/regress/{regress1 => regress2}/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 (100%) rename test/regress/{regress1 => regress2}/nl/ufnia-factor-open-proof.smt2 (100%) rename test/regress/{regress1 => regress2}/quantifiers/issue3481-unsat1.smt2 (100%) rename test/regress/{regress2 => regress3}/arith/abz5_1400.smtv1.smt2 (100%) rename test/regress/{regress2 => regress3}/error0.smt2 (100%) rename test/regress/{regress2 => regress3}/ho/SYO362^5.p (100%) rename test/regress/{regress1 => regress3}/nl/iand-native-1.smt2 (100%) rename test/regress/{regress2 => regress3}/quantifiers/ForElimination-scala-9.smt2 (100%) rename test/regress/{regress2 => regress3}/quantifiers/javafe.ast.ArrayInit.35.smt2 (100%) rename test/regress/{regress3 => regress4}/siegel-nl-bases.smt2 (100%) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a64a1eb1e..9bda5cff1 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1576,7 +1576,6 @@ set(regress_1_tests regress1/issue5739-rtf-processed.smt2 regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2 regress1/lemmas/pursuit-safety-8.smtv1.smt2 - regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 regress1/model-blocker-simple.smt2 regress1/model-blocker-values.smt2 regress1/nl/approx-sqrt.smt2 @@ -1599,7 +1598,6 @@ set(regress_1_tests regress1/nl/exp_monotone.smt2 regress1/nl/ext-rew-aggr-test.smt2 regress1/nl/factor_agg_s.smt2 - regress1/nl/iand-native-1.smt2 regress1/nl/iand-native-2.smt2 regress1/nl/iand-native-granularities.smt2 regress1/nl/issue3300-approx-sqrt-witness.smt2 @@ -1647,7 +1645,6 @@ set(regress_1_tests regress1/nl/sugar-ident-3.smt2 regress1/nl/sugar-ident.smt2 regress1/nl/tan-rewrite2.smt2 - regress1/nl/ufnia-factor-open-proof.smt2 regress1/nl/zero-subset.smt2 regress1/non-fatal-errors.smt2 regress1/parsing_ringer.cvc @@ -1763,7 +1760,6 @@ set(regress_1_tests regress1/quantifiers/issue3316.smt2 regress1/quantifiers/issue3317.smt2 regress1/quantifiers/issue3481.smt2 - regress1/quantifiers/issue3481-unsat1.smt2 regress1/quantifiers/issue3537.smt2 regress1/quantifiers/issue3628.smt2 regress1/quantifiers/issue3664.smt2 @@ -2337,7 +2333,6 @@ set(regress_2_tests regress2/DTP_k2_n35_c175_s15.smt2 regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 regress2/GEO123+1.minimized.smt2 - regress2/arith/abz5_1400.smtv1.smt2 regress2/arith/arith-int-098.cvc regress2/arith/pursuit-safety-11.smtv1.smt2 regress2/arith/pursuit-safety-12.smtv1.smt2 @@ -2365,7 +2360,6 @@ set(regress_2_tests regress2/bv_to_int_mask_array_2.smt2 regress2/bv_to_int_mask_array_3.smt2 regress2/bv_to_int_shifts.smt2 - regress2/error0.smt2 regress2/error1.smtv1.smt2 regress2/fuzz_2.smtv1.smt2 regress2/hash_sat_06_19.smt2 @@ -2377,24 +2371,24 @@ set(regress_2_tests regress2/ho/fta0409.smt2 regress2/ho/involved_parsing_ALG248^3.p regress2/ho/partial_app_interpreted_SWW474^2.p - regress2/ho/SYO362^5.p regress2/hole7.cvc regress2/hole8.cvc regress2/instance_1444.smtv1.smt2 regress2/issue3687-check-models.smt2 regress2/issue4707-bv-to-bool-large.smt2 regress2/issue6495-dup-pat-term.smt2 + regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 regress2/javafe.ast.WhileStmt.447_no_forall.smt2 regress2/nl/nt-lemmas-bad.smt2 + regress2/nl/ufnia-factor-open-proof.smt2 regress2/ooo.rf6.smt2 regress2/ooo.tag10.smt2 regress2/piVC_5581bd.smt2 regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 - regress2/quantifiers/ForElimination-scala-9.smt2 regress2/quantifiers/gn-wrong-091018.smt2 - regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 + regress2/quantifiers/issue3481-unsat1.smt2 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 @@ -2452,6 +2446,7 @@ set(regress_2_tests # Regression level 3 tests set(regress_3_tests + regress3/arith/abz5_1400.smtv1.smt2 regress3/arith_prp-13-24.smt2 regress3/aufbv-wchains010ue.smtv1.smt2 regress3/auflia-fuzz06.smtv1.smt2 @@ -2477,24 +2472,27 @@ set(regress_3_tests regress3/decision-wchains010ue.smtv1.smt2 regress3/DRAGON_1.lus.sy regress3/eq_diamond14.smtv1.smt2 + regress3/error0.smt2 regress3/friedman_n4_i5.smtv1.smt2 regress3/friedman_n6_i4.smtv1.smt2 + regress3/ho/SYO362^5.p regress3/hole9.cvc regress3/hole10.cvc regress3/incorrect1.smtv1.smt2 regress3/interpol2.smt2 regress3/inv_gen_n_c11.sy regress3/issue4170.smt2 - regress3/issue4476-ext-rew.smt2 regress3/issue4714.smt2 regress3/lpsat-goal-9.smt2 regress3/nia-max-square.sy + regress3/nl/iand-native-1.smt2 regress3/PEQ018_size4.smtv1.smt2 regress3/policyM.sy + regress3/quantifiers/ForElimination-scala-9.smt2 + regress3/quantifiers/javafe.ast.ArrayInit.35.smt2 regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2 regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2 regress3/regex-rrv.sy - regress3/siegel-nl-bases.smt2 regress3/sixfuncs.sy regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2 regress3/strings-any-term.sy @@ -2502,7 +2500,6 @@ set(regress_3_tests regress3/strings/norn-dis-0707-3.smt2 regress3/strings/replace_re_all.smt2 regress3/unbdd_inv_gen_ex7.sy - regress3/unifpi-solve-car_1.lus.sy regress3/vcb.sy ) @@ -2523,6 +2520,7 @@ set(regress_4_tests regress4/NEQ016_size5.smtv1.smt2 regress4/pp-regfile.smtv1.smt2 regress4/sets-card-neg-mem-union-2.smt2 + regress4/siegel-nl-bases.smt2 regress4/unsat-circ-reduce.smt2 regress4/xs-11-20-5-2-5-3.smt2 regress4/xs-11-20-5-2-5-3.smtv1.smt2 @@ -2616,6 +2614,9 @@ set(regression_disabled_tests regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 regress2/nl/dumortier-050317.smt2 + # time out + regress3/unifpi-solve-car_1.lus.sy + regress3/issue4476-ext-rew.smt2 ) #-----------------------------------------------------------------------------# diff --git a/test/regress/README.md b/test/regress/README.md index f7fb2b6d3..efd79472b 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -1,12 +1,24 @@ # Regression -## Regression Levels and Running Regression Tests +## Regression Levels -cvc5's regression tests are divided into 5 levels (level 0 to 4). Higher -regression levels are reserved for longer running regressions. +cvc5's regression tests are divided into 5 levels (level 0 to 4), based on +their run time (`production` build with `--assertions`). +Higher regression levels are reserved for longer running regressions. -For running regressions tests, -see the [INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) file. +The time limits for each level are: + +* **Level 0:** <= 1s +* **Level 1:** <= 5s +* **Level 2:** <= 10s +* **Level 3:** <= 100s +* **Level 4:** > 100s + +## Running Regression Tests + +For running regressions tests, see the +[INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) +file. By default, each invocation of cvc5 is done with a 10 minute timeout. To use a different timeout, set the `TEST_TIMEOUT` environment variable: diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 b/test/regress/regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 similarity index 100% rename from test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 rename to test/regress/regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 diff --git a/test/regress/regress1/nl/ufnia-factor-open-proof.smt2 b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 similarity index 100% rename from test/regress/regress1/nl/ufnia-factor-open-proof.smt2 rename to test/regress/regress2/nl/ufnia-factor-open-proof.smt2 diff --git a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 b/test/regress/regress2/quantifiers/issue3481-unsat1.smt2 similarity index 100% rename from test/regress/regress1/quantifiers/issue3481-unsat1.smt2 rename to test/regress/regress2/quantifiers/issue3481-unsat1.smt2 diff --git a/test/regress/regress2/arith/abz5_1400.smtv1.smt2 b/test/regress/regress3/arith/abz5_1400.smtv1.smt2 similarity index 100% rename from test/regress/regress2/arith/abz5_1400.smtv1.smt2 rename to test/regress/regress3/arith/abz5_1400.smtv1.smt2 diff --git a/test/regress/regress2/error0.smt2 b/test/regress/regress3/error0.smt2 similarity index 100% rename from test/regress/regress2/error0.smt2 rename to test/regress/regress3/error0.smt2 diff --git a/test/regress/regress2/ho/SYO362^5.p b/test/regress/regress3/ho/SYO362^5.p similarity index 100% rename from test/regress/regress2/ho/SYO362^5.p rename to test/regress/regress3/ho/SYO362^5.p diff --git a/test/regress/regress3/issue4714.smt2 b/test/regress/regress3/issue4714.smt2 index ee3e59a32..ac8914044 100644 --- a/test/regress/regress3/issue4714.smt2 +++ b/test/regress/regress3/issue4714.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --check-models -; EXPECT: unknown +; EXPECT: sat (set-logic UFNIRA) (declare-fun c (Int) Int) (define-fun d ((k Int)) Int (- (c k) 10)) diff --git a/test/regress/regress1/nl/iand-native-1.smt2 b/test/regress/regress3/nl/iand-native-1.smt2 similarity index 100% rename from test/regress/regress1/nl/iand-native-1.smt2 rename to test/regress/regress3/nl/iand-native-1.smt2 diff --git a/test/regress/regress2/quantifiers/ForElimination-scala-9.smt2 b/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2 similarity index 100% rename from test/regress/regress2/quantifiers/ForElimination-scala-9.smt2 rename to test/regress/regress3/quantifiers/ForElimination-scala-9.smt2 diff --git a/test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 b/test/regress/regress3/quantifiers/javafe.ast.ArrayInit.35.smt2 similarity index 100% rename from test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 rename to test/regress/regress3/quantifiers/javafe.ast.ArrayInit.35.smt2 diff --git a/test/regress/regress3/siegel-nl-bases.smt2 b/test/regress/regress4/siegel-nl-bases.smt2 similarity index 100% rename from test/regress/regress3/siegel-nl-bases.smt2 rename to test/regress/regress4/siegel-nl-bases.smt2 -- 2.30.2