Add --parallel option, default=false since it crashes like crazy

src/main/scala/leon/synthesis/SynthesisPhase.scala

@@ -14,11 +14,12 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
   val description = "Synthesis"
 
   override def definedOptions = Set(
-    LeonFlagOptionDef( "inplace", "--inplace",           "Debug level"),
-    LeonFlagOptionDef( "derivtrees", "--derivtrees",     "Generate derivation trees"),
-    LeonFlagOptionDef( "firstonly", "--firstonly",       "Stop as soon as one synthesis solution is found"),
-    LeonValueOptionDef("timeout",   "--timeout=T",       "Timeout after T seconds when searching for synthesis solutions .."),
-    LeonValueOptionDef("functions", "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,..")
+    LeonFlagOptionDef( "inplace",    "--inplace",         "Debug level"),
+    LeonFlagOptionDef( "parallel",   "--parallel",        "Parallel synthesis search"),
+    LeonFlagOptionDef( "derivtrees", "--derivtrees",      "Generate derivation trees"),
+    LeonFlagOptionDef( "firstonly",  "--firstonly",       "Stop as soon as one synthesis solution is found"),
+    LeonValueOptionDef("timeout",    "--timeout=T",       "Timeout after T seconds when searching for synthesis solutions .."),
+    LeonValueOptionDef("functions",  "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,..")
   )
 
   def run(ctx: LeonContext)(p: Program): Program = {
@@ -33,6 +34,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
     var inPlace                        = false
     var genTrees                       = false
     var firstOnly                      = false
+    var parallel                       = false
     var filterFun: Option[Seq[String]] = None 
     var timeoutMs: Option[Long]        = None
 
@@ -49,6 +51,8 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
         }
       case LeonFlagOption("firstonly") =>
         firstOnly = true
+      case LeonFlagOption("parallel") =>
+        parallel = true
       case LeonFlagOption("derivtrees") =>
         genTrees = true
       case _ =>
@@ -62,7 +66,16 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
         case ch @ Choose(vars, pred) =>
           val problem = Problem.fromChoose(ch)
-          val synth = new Synthesizer(ctx.reporter, mainSolver, p, problem, Rules.all ++ Heuristics.all, genTrees, filterFun.map(_.toSet), firstOnly, timeoutMs)
+          val synth = new Synthesizer(ctx.reporter,
+                                      mainSolver,
+                                      p,
+                                      problem,
+                                      Rules.all ++ Heuristics.all,
+                                      genTrees,
+                                      filterFun.map(_.toSet),
+                                      parallel,
+                                      firstOnly,
+                                      timeoutMs)
           val sol = synth.synthesize()
 
           solutions += ch -> sol

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -22,6 +22,7 @@ class Synthesizer(val reporter: Reporter,
                   val rules: Set[Rule],
                   generateDerivationTrees: Boolean = false,
                   filterFuns: Option[Set[String]]  = None,
+                  parallel: Boolean                = false,
                   firstOnly: Boolean               = false,
                   timeoutMs: Option[Long]          = None) {
   import reporter.{error,warning,info,fatalError}
@@ -30,7 +31,11 @@ class Synthesizer(val reporter: Reporter,
 
   def synthesize(): Solution = {
 
-    val search = new ParallelSearch(this, problem, rules)
+    val search = if (parallel) {
+      new ParallelSearch(this, problem, rules)
+    } else {
+      new SimpleSearch(this, problem, rules)
+    }
 
     val sigINT = new Signal("INT")
     var oldHandler: SignalHandler = null

src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala

@@ -62,6 +62,8 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
     continue = false
   }
 
+  def search(): Option[S]
+
   def onExpansion(al: g.AndLeaf, res: ExpandResult[OT]) {
     res match {
       case Expanded(ls) =>