adding new arguments --quickcheck to run quicheck random solver and --parallel...

adding new arguments --quickcheck to run quicheck random solver and --parallel to run all solvers in parallel

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)): _*)

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

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
   }
 

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)
 

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
 }