From 45496c70d7b90d4da5cda0aa21b862de01f4929a Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 29 Apr 2016 09:39:05 +0200
Subject: [PATCH] Attempt at reducing native-z3 parallelism during tests
---
.larabot.conf | 1 +
build.sbt | 12 ++++++++++--
.../purescala/PureScalaVerificationSuite.scala | 15 ++++++++-------
3 files changed, 19 insertions(+), 9 deletions(-)
diff --git a/.larabot.conf b/.larabot.conf
index 099fbc1f0..0458c9d97 100644
--- a/.larabot.conf
+++ b/.larabot.conf
@@ -2,6 +2,7 @@ commands = [
"sbt -batch -Dparallel=10 test"
"sbt -batch -Dparallel=10 integration:test"
"sbt -batch -Dparallel=10 regression:test"
+ "sbt -batch -Dparallel=10 native:test"
"sbt -batch -Dparallel=10 genc:test"
"sbt -batch -Dparallel=10 isabelle:test"
]
diff --git a/build.sbt b/build.sbt
index 5d7cdbeb5..e5dd61402 100644
--- a/build.sbt
+++ b/build.sbt
@@ -148,12 +148,19 @@ lazy val IntegrTest = config("integration") extend(Test)
testOptions in IntegrTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.integration."))
+def regressionFilter(name: String, native: Boolean = false): Boolean = name.startsWith("leon.regression") && (name.endsWith("NativeZ3") == native)
// Regression Tests
lazy val RegressionTest = config("regression") extend(Test)
-testOptions in RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.regression."))
+testOptions in RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(regressionFilter(_)))
+// Regression Tests that heavily depend on native Z3
+lazy val NativeZ3RegressionTest = config("native") extend(Test)
+
+testOptions in NativeZ3RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(regressionFilter(_, native = true)))
+
+parallelExecution in NativeZ3RegressionTest := false
// Isabelle Tests
@@ -179,9 +186,10 @@ lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "10ea
lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "57834acfe2e3bc36862be52e4d99829bb8ff0ca7")
lazy val root = (project in file(".")).
- configs(RegressionTest, IsabelleTest, GenCTest, IntegrTest).
+ configs(RegressionTest, NativeZ3RegressionTest, IsabelleTest, GenCTest, IntegrTest).
dependsOn(bonsai).
dependsOn(scalaSmtlib).
+ settings(inConfig(NativeZ3RegressionTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(RegressionTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(IntegrTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(IsabelleTest)(Defaults.testTasks ++ testSettings): _*).
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
index ff1fcd53b..d2a1215f9 100644
--- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -32,13 +32,13 @@ trait PureScalaValidSuite extends PureScalaVerificationSuite {
override def testAll() = testValid()
}
-class PureScalaValidSuite1 extends PureScalaValidSuite {
+class PureScalaValidSuiteLuckyNativeZ3 extends PureScalaValidSuite {
val optionVariants = List(opts(0))
}
-class PureScalaValidSuite2 extends PureScalaValidSuite {
+class PureScalaValidSuiteCodeGenNativeZ3 extends PureScalaValidSuite {
val optionVariants = List(opts(1))
}
-class PureScalaValidSuite3 extends PureScalaValidSuite { // tests verification with --codegen parameter
+class PureScalaValidSuiteEnumNativeZ3 extends PureScalaValidSuite {
val optionVariants = List(opts(2))
override val ignored = Seq("valid/Predicate.scala","valid/TraceInductTacticTest.scala")
}
@@ -53,10 +53,14 @@ trait PureScalaInvalidSuite extends PureScalaVerificationSuite {
override def testAll() = testInvalid()
}
-class PureScalaInvalidSuiteFairZ3 extends PureScalaInvalidSuite {
+class PureScalaInvalidSuiteNativeZ3 extends PureScalaInvalidSuite {
val optionVariants = opts.take(3)
}
+class PureScalaInvalidSuiteZ3 extends PureScalaInvalidSuite {
+ val optionVariants = isZ3Available.option(opts(3)).toList
+}
+
class PureScalaInvalidSuiteCVC4 extends PureScalaInvalidSuite {
val optionVariants = isCVC4Available.option(opts.last).toList
override val ignored = List(
@@ -66,6 +70,3 @@ class PureScalaInvalidSuiteCVC4 extends PureScalaInvalidSuite {
)
}
-class PureScalaInvalidSuiteZ3 extends PureScalaInvalidSuite {
- val optionVariants = isZ3Available.option(opts(3)).toList
-}
--
GitLab