From c6f86de8077f667ab2b2e9aac53d60d93ea2da93 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 4 Feb 2010 21:01:04 +0000 Subject: [PATCH] Moved regressions into various levels based on running time. --- test/regress/logops.cvc | 14 -------------- test/regress/{ => regress0}/boolean.cvc | 0 test/regress/{ => regress0}/bug1.cvc | 0 test/regress/{ => regress0}/hole6.cvc | 0 test/regress/regress0/logops.cvc | 14 ++++++++++++++ test/regress/regress0/queries0.cvc | 11 +++++++++++ test/regress/{ => regress0}/simple-uf.smt | 0 test/regress/{ => regress0}/simple.cvc | 0 test/regress/{ => regress0}/simple.smt | 0 test/regress/{ => regress0}/simple2.smt | 0 test/regress/regress0/smallcnf.cvc | 9 +++++++++ test/regress/{ => regress0}/test11.cvc | 0 test/regress/{ => regress0}/test12.cvc | 0 test/regress/{ => regress0}/test9.cvc | 0 test/regress/{ => regress0}/uf20-03.cvc | 0 test/regress/{ => regress0}/wiki.cvc | 0 test/regress/{ => regress1}/friedman_n4_i5.smt | 0 test/regress/{ => regress1}/hole7.cvc | 0 test/regress/{ => regress1}/hole8.cvc | 0 test/regress/{ => regress1}/instance_1444.smt | 0 test/regress/{ => regress2}/bmc-galileo-8.smt | 0 test/regress/{ => regress2}/bmc-galileo-9.smt | 0 test/regress/{ => regress2}/bmc-ibm-1.smt | 0 test/regress/{ => regress2}/bmc-ibm-10.smt | 0 test/regress/{ => regress2}/bmc-ibm-11.smt | 0 test/regress/{ => regress2}/bmc-ibm-12.smt | 0 test/regress/{ => regress2}/bmc-ibm-13.smt | 0 test/regress/{ => regress2}/bmc-ibm-2.smt | 0 test/regress/{ => regress2}/bmc-ibm-3.smt | 0 test/regress/{ => regress2}/bmc-ibm-4.smt | 0 test/regress/{ => regress2}/bmc-ibm-5.smt | 0 test/regress/{ => regress2}/bmc-ibm-6.smt | 0 test/regress/{ => regress2}/bmc-ibm-7.smt | 0 test/regress/{ => regress2}/friedman_n6_i4.smt | 0 test/regress/{ => regress2}/hole9.cvc | 0 .../qwh.35.405.shuffled-as.sat03-1651.smt | 0 .../C880mul.miter.shuffled-as.sat03-348.smt | 0 .../{ => regress3}/comb2.shuffled-as.sat03-420.smt | 0 test/regress/{ => regress3}/hole10.cvc | 0 test/regress/{ => regress3}/instance_1151.smt | 0 40 files changed, 34 insertions(+), 14 deletions(-) delete mode 100644 test/regress/logops.cvc rename test/regress/{ => regress0}/boolean.cvc (100%) rename test/regress/{ => regress0}/bug1.cvc (100%) rename test/regress/{ => regress0}/hole6.cvc (100%) create mode 100644 test/regress/regress0/logops.cvc create mode 100644 test/regress/regress0/queries0.cvc rename test/regress/{ => regress0}/simple-uf.smt (100%) rename test/regress/{ => regress0}/simple.cvc (100%) rename test/regress/{ => regress0}/simple.smt (100%) rename test/regress/{ => regress0}/simple2.smt (100%) create mode 100644 test/regress/regress0/smallcnf.cvc rename test/regress/{ => regress0}/test11.cvc (100%) rename test/regress/{ => regress0}/test12.cvc (100%) rename test/regress/{ => regress0}/test9.cvc (100%) rename test/regress/{ => regress0}/uf20-03.cvc (100%) rename test/regress/{ => regress0}/wiki.cvc (100%) rename test/regress/{ => regress1}/friedman_n4_i5.smt (100%) rename test/regress/{ => regress1}/hole7.cvc (100%) rename test/regress/{ => regress1}/hole8.cvc (100%) rename test/regress/{ => regress1}/instance_1444.smt (100%) rename test/regress/{ => regress2}/bmc-galileo-8.smt (100%) rename test/regress/{ => regress2}/bmc-galileo-9.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-1.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-10.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-11.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-12.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-13.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-2.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-3.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-4.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-5.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-6.smt (100%) rename test/regress/{ => regress2}/bmc-ibm-7.smt (100%) rename test/regress/{ => regress2}/friedman_n6_i4.smt (100%) rename test/regress/{ => regress2}/hole9.cvc (100%) rename test/regress/{ => regress2}/qwh.35.405.shuffled-as.sat03-1651.smt (100%) rename test/regress/{ => regress3}/C880mul.miter.shuffled-as.sat03-348.smt (100%) rename test/regress/{ => regress3}/comb2.shuffled-as.sat03-420.smt (100%) rename test/regress/{ => regress3}/hole10.cvc (100%) rename test/regress/{ => regress3}/instance_1151.smt (100%) diff --git a/test/regress/logops.cvc b/test/regress/logops.cvc deleted file mode 100644 index 35e080992..000000000 --- a/test/regress/logops.cvc +++ /dev/null @@ -1,14 +0,0 @@ - - -a, b, c: BOOLEAN; - -%% QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); - -%% QUERY NOT c AND b; - -QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); - -%% QUERY (a => b) <=> (NOT a OR b); - -%% QUERY TRUE XOR FALSE; - diff --git a/test/regress/boolean.cvc b/test/regress/regress0/boolean.cvc similarity index 100% rename from test/regress/boolean.cvc rename to test/regress/regress0/boolean.cvc diff --git a/test/regress/bug1.cvc b/test/regress/regress0/bug1.cvc similarity index 100% rename from test/regress/bug1.cvc rename to test/regress/regress0/bug1.cvc diff --git a/test/regress/hole6.cvc b/test/regress/regress0/hole6.cvc similarity index 100% rename from test/regress/hole6.cvc rename to test/regress/regress0/hole6.cvc diff --git a/test/regress/regress0/logops.cvc b/test/regress/regress0/logops.cvc new file mode 100644 index 000000000..0cb00599d --- /dev/null +++ b/test/regress/regress0/logops.cvc @@ -0,0 +1,14 @@ + + +a, b, c: BOOLEAN; + +QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); + +QUERY NOT c AND b; + +QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); + +QUERY (a => b) <=> (NOT a OR b); + +QUERY TRUE XOR FALSE; + diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc new file mode 100644 index 000000000..8f7ceedd5 --- /dev/null +++ b/test/regress/regress0/queries0.cvc @@ -0,0 +1,11 @@ + +% Tests the invariants for multiple queries. + +a, b: BOOLEAN; + +%Valid query +QUERY (a AND b) OR NOT (a AND b); + +%Invalid query +QUERY (a OR b); + diff --git a/test/regress/simple-uf.smt b/test/regress/regress0/simple-uf.smt similarity index 100% rename from test/regress/simple-uf.smt rename to test/regress/regress0/simple-uf.smt diff --git a/test/regress/simple.cvc b/test/regress/regress0/simple.cvc similarity index 100% rename from test/regress/simple.cvc rename to test/regress/regress0/simple.cvc diff --git a/test/regress/simple.smt b/test/regress/regress0/simple.smt similarity index 100% rename from test/regress/simple.smt rename to test/regress/regress0/simple.smt diff --git a/test/regress/simple2.smt b/test/regress/regress0/simple2.smt similarity index 100% rename from test/regress/simple2.smt rename to test/regress/regress0/simple2.smt diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc new file mode 100644 index 000000000..3ad6f124a --- /dev/null +++ b/test/regress/regress0/smallcnf.cvc @@ -0,0 +1,9 @@ + +a, b, c : BOOLEAN; + +ASSERT NOT a OR NOT b; +ASSERT c OR b OR a; +ASSERT b OR NOT a; +ASSERT a OR NOT b OR c; +QUERY FALSE; + diff --git a/test/regress/test11.cvc b/test/regress/regress0/test11.cvc similarity index 100% rename from test/regress/test11.cvc rename to test/regress/regress0/test11.cvc diff --git a/test/regress/test12.cvc b/test/regress/regress0/test12.cvc similarity index 100% rename from test/regress/test12.cvc rename to test/regress/regress0/test12.cvc diff --git a/test/regress/test9.cvc b/test/regress/regress0/test9.cvc similarity index 100% rename from test/regress/test9.cvc rename to test/regress/regress0/test9.cvc diff --git a/test/regress/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc similarity index 100% rename from test/regress/uf20-03.cvc rename to test/regress/regress0/uf20-03.cvc diff --git a/test/regress/wiki.cvc b/test/regress/regress0/wiki.cvc similarity index 100% rename from test/regress/wiki.cvc rename to test/regress/regress0/wiki.cvc diff --git a/test/regress/friedman_n4_i5.smt b/test/regress/regress1/friedman_n4_i5.smt similarity index 100% rename from test/regress/friedman_n4_i5.smt rename to test/regress/regress1/friedman_n4_i5.smt diff --git a/test/regress/hole7.cvc b/test/regress/regress1/hole7.cvc similarity index 100% rename from test/regress/hole7.cvc rename to test/regress/regress1/hole7.cvc diff --git a/test/regress/hole8.cvc b/test/regress/regress1/hole8.cvc similarity index 100% rename from test/regress/hole8.cvc rename to test/regress/regress1/hole8.cvc diff --git a/test/regress/instance_1444.smt b/test/regress/regress1/instance_1444.smt similarity index 100% rename from test/regress/instance_1444.smt rename to test/regress/regress1/instance_1444.smt diff --git a/test/regress/bmc-galileo-8.smt b/test/regress/regress2/bmc-galileo-8.smt similarity index 100% rename from test/regress/bmc-galileo-8.smt rename to test/regress/regress2/bmc-galileo-8.smt diff --git a/test/regress/bmc-galileo-9.smt b/test/regress/regress2/bmc-galileo-9.smt similarity index 100% rename from test/regress/bmc-galileo-9.smt rename to test/regress/regress2/bmc-galileo-9.smt diff --git a/test/regress/bmc-ibm-1.smt b/test/regress/regress2/bmc-ibm-1.smt similarity index 100% rename from test/regress/bmc-ibm-1.smt rename to test/regress/regress2/bmc-ibm-1.smt diff --git a/test/regress/bmc-ibm-10.smt b/test/regress/regress2/bmc-ibm-10.smt similarity index 100% rename from test/regress/bmc-ibm-10.smt rename to test/regress/regress2/bmc-ibm-10.smt diff --git a/test/regress/bmc-ibm-11.smt b/test/regress/regress2/bmc-ibm-11.smt similarity index 100% rename from test/regress/bmc-ibm-11.smt rename to test/regress/regress2/bmc-ibm-11.smt diff --git a/test/regress/bmc-ibm-12.smt b/test/regress/regress2/bmc-ibm-12.smt similarity index 100% rename from test/regress/bmc-ibm-12.smt rename to test/regress/regress2/bmc-ibm-12.smt diff --git a/test/regress/bmc-ibm-13.smt b/test/regress/regress2/bmc-ibm-13.smt similarity index 100% rename from test/regress/bmc-ibm-13.smt rename to test/regress/regress2/bmc-ibm-13.smt diff --git a/test/regress/bmc-ibm-2.smt b/test/regress/regress2/bmc-ibm-2.smt similarity index 100% rename from test/regress/bmc-ibm-2.smt rename to test/regress/regress2/bmc-ibm-2.smt diff --git a/test/regress/bmc-ibm-3.smt b/test/regress/regress2/bmc-ibm-3.smt similarity index 100% rename from test/regress/bmc-ibm-3.smt rename to test/regress/regress2/bmc-ibm-3.smt diff --git a/test/regress/bmc-ibm-4.smt b/test/regress/regress2/bmc-ibm-4.smt similarity index 100% rename from test/regress/bmc-ibm-4.smt rename to test/regress/regress2/bmc-ibm-4.smt diff --git a/test/regress/bmc-ibm-5.smt b/test/regress/regress2/bmc-ibm-5.smt similarity index 100% rename from test/regress/bmc-ibm-5.smt rename to test/regress/regress2/bmc-ibm-5.smt diff --git a/test/regress/bmc-ibm-6.smt b/test/regress/regress2/bmc-ibm-6.smt similarity index 100% rename from test/regress/bmc-ibm-6.smt rename to test/regress/regress2/bmc-ibm-6.smt diff --git a/test/regress/bmc-ibm-7.smt b/test/regress/regress2/bmc-ibm-7.smt similarity index 100% rename from test/regress/bmc-ibm-7.smt rename to test/regress/regress2/bmc-ibm-7.smt diff --git a/test/regress/friedman_n6_i4.smt b/test/regress/regress2/friedman_n6_i4.smt similarity index 100% rename from test/regress/friedman_n6_i4.smt rename to test/regress/regress2/friedman_n6_i4.smt diff --git a/test/regress/hole9.cvc b/test/regress/regress2/hole9.cvc similarity index 100% rename from test/regress/hole9.cvc rename to test/regress/regress2/hole9.cvc diff --git a/test/regress/qwh.35.405.shuffled-as.sat03-1651.smt b/test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt similarity index 100% rename from test/regress/qwh.35.405.shuffled-as.sat03-1651.smt rename to test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt diff --git a/test/regress/C880mul.miter.shuffled-as.sat03-348.smt b/test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt similarity index 100% rename from test/regress/C880mul.miter.shuffled-as.sat03-348.smt rename to test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt diff --git a/test/regress/comb2.shuffled-as.sat03-420.smt b/test/regress/regress3/comb2.shuffled-as.sat03-420.smt similarity index 100% rename from test/regress/comb2.shuffled-as.sat03-420.smt rename to test/regress/regress3/comb2.shuffled-as.sat03-420.smt diff --git a/test/regress/hole10.cvc b/test/regress/regress3/hole10.cvc similarity index 100% rename from test/regress/hole10.cvc rename to test/regress/regress3/hole10.cvc diff --git a/test/regress/instance_1151.smt b/test/regress/regress3/instance_1151.smt similarity index 100% rename from test/regress/instance_1151.smt rename to test/regress/regress3/instance_1151.smt -- 2.30.2