ChooseInfo.extractFromProgram respects --functions and @library

src/main/scala/leon/synthesis/ChooseInfo.scala

@@ -20,9 +20,19 @@ case class ChooseInfo(fd: FunDef,
 
 object ChooseInfo {
   def extractFromProgram(ctx: LeonContext, prog: Program): List[ChooseInfo] = {
+    val functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet }
+
+    def excludeByDefault(fd: FunDef): Boolean = {
+      fd.annotations contains "library"
+    }
+
+    val fdFilter = {
+      import OptionsHelpers._
+      filterInclusive(functions.map(fdMatcher(prog)), Some(excludeByDefault _))
+    }
 
     // Look for choose()
-    val results = for (f <- prog.definedFunctions if f.body.isDefined;
+    val results = for (f <- prog.definedFunctions if f.body.isDefined && fdFilter(f);
                        ci <- extractFromFunction(ctx, prog, f)) yield {
       ci
     }

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

@@ -65,14 +65,8 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
   def run(ctx: LeonContext)(program: Program): Program = {
     val options = processOptions(ctx)
 
-    def excludeByDefault(fd: FunDef): Boolean = { fd.annotations contains "library" }
 
-    val fdFilter = {
-      import OptionsHelpers._
-      filterInclusive(options.functions.map(fdMatcher(program)), Some(excludeByDefault _))
-    }
-
-    val chooses = program.definedFunctions.filter(fdFilter).flatMap(ChooseInfo.extractFromFunction(ctx, program, _))
+    val chooses = ChooseInfo.extractFromProgram(ctx, program)
 
     var functions = Set[FunDef]()
 

src/regression/scala/leon/regression/synthesis/SynthesisSuite.scala

@@ -86,7 +86,10 @@ class SynthesisSuite extends regression.LeonTestSuite {
       test(f"Synthesizing ${nextInt()}%3d: [$title]") {
         val ctx = testContext.copy(options = opts ++ testContext.options)
 
-        val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen PreprocessingPhase andThen SynthesisProblemExtractionPhase
+        val pipeline = leon.utils.TemporaryInputPhase andThen
+                       leon.frontends.scalac.ExtractionPhase andThen
+                       PreprocessingPhase andThen
+                       SynthesisProblemExtractionPhase
 
         val (program, results) = pipeline.run(ctx)((List(content), Nil))