diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala index c5bcb8d9c49ddaccf6ad845a4cc32155ea4ca722..40ecbc08b5dd1e3b6db38bfd35f3fba62a1db66d 100644 --- a/src/funcheck/FunCheckPlugin.scala +++ b/src/funcheck/FunCheckPlugin.scala @@ -36,7 +36,8 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog " -P:funcheck:BV Use bit-vectors for integers" + "\n" + " -P:funcheck:prune Use additional SMT queries to rule out some unrollings" + "\n" + " -P:funcheck:cores Use UNSAT cores in the unrolling/refinement step" + "\n" + - " -P:funcheck:quickcheck Use QuickCheck-like random search in parrallel with Z3" + "\n" + + " -P:funcheck:quickcheck Use QuickCheck-like random search" + "\n" + + " -P:funcheck:parallel Run all solvers in parallel" + "\n" + " -P:funcheck:noLuckyTests Do not perform additional tests to potentially find models early" ) @@ -58,6 +59,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog case "prune" => purescala.Settings.pruneBranches = true case "cores" => purescala.Settings.useCores = true case "quickcheck" => purescala.Settings.useQuickCheck = true + case "parallel" => purescala.Settings.useParallel = true case "noLuckyTests" => purescala.Settings.luckyTest = false case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 } case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*) diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala index 3f5371e220e6c11d6864194df71637b90c937a50..5fe5ce718ef64544664a8fb09bb03f3e3488f8f7 100644 --- a/src/purescala/Analysis.scala +++ b/src/purescala/Analysis.scala @@ -14,14 +14,7 @@ class Analysis(val program: Program, val reporter: Reporter = Settings.reporter) val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D - val solverExtensions0: Seq[Solver] = trivialSolver +: loadedSolverExtensions - val solverExtensions = - if(Settings.solverTimeout == None) { - solverExtensions0 - } else { - val t = Settings.solverTimeout.get - solverExtensions0.map(s => new TimeoutSolver(s, t)) - } + val solverExtensions: Seq[Solver] = trivialSolver +: loadedSolverExtensions solverExtensions.foreach(_.setProgram(program)) diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala index f8f35df8a7ff684747a4fb74959ea23426fd4e49..a5618f64b06c0680292b0bd5363054cc5dedcb8f 100644 --- a/src/purescala/Extensions.scala +++ b/src/purescala/Extensions.scala @@ -88,20 +88,26 @@ object Extensions { } else { (new Z3Solver(extensionsReporter)) }) - - val qcs : Solver = (if(Settings.useQuickCheck) { - new ParallelSolver(extensionsReporter, new RandomSolver(extensionsReporter), z3s) - } else { - z3s - }) - - qcs :: Nil + z3s :: Nil } else { Nil } + + allLoaded = defaultExtensions ++ loaded analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser]) - solverExtensions = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver]) + + val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver]) + val solverExtensions1 = if(Settings.useQuickCheck) new RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0 + val solverExtensions2 = if(Settings.useParallel) new ParallelSolver(solverExtensions1: _*) +: solverExtensions1 else solverExtensions1 + val solverExtensions3 = + if(Settings.solverTimeout == None) { + solverExtensions2 + } else { + val t = Settings.solverTimeout.get + solverExtensions2.map(s => new TimeoutSolver(s, t)) + } + solverExtensions = solverExtensions3 loaded } diff --git a/src/purescala/ParallelSolver.scala b/src/purescala/ParallelSolver.scala index 2e43ab41db7cc0a7b8a7f4a2b928e9729b00d133..15f89756607dfdd5dc7dbbbf4fefeeede0d9c13d 100644 --- a/src/purescala/ParallelSolver.scala +++ b/src/purescala/ParallelSolver.scala @@ -16,7 +16,7 @@ import scala.actors.Actor._ import scala.concurrent.Lock -class ParallelSolver(reporter: Reporter, solvers: Solver*) extends Solver(reporter) { +class ParallelSolver(solvers: Solver*) extends Solver(solvers(0).reporter) { private val nbSolvers = solvers.size require(nbSolvers >= 2) diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala index 651a13c269cd0277c952cdd27cd6bcdf8995252e..900e9062b33102794278345e832e1fc7d23aec80 100644 --- a/src/purescala/Settings.scala +++ b/src/purescala/Settings.scala @@ -23,6 +23,7 @@ object Settings { var solverTimeout : Option[Int] = None var luckyTest : Boolean = true var useQuickCheck : Boolean = false + var useParallel : Boolean = false // When this is None, use real integers var bitvectorBitwidth : Option[Int] = None }