diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index a8c8dcc59e119dc38423a5529e229b23c13d8238..3e716313b9a171542bf3540eef7b41c4359cb03a 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -72,6 +72,12 @@ object DefOps {
toRet.values.toSet
}
+ def visibleFunDefsFrom(df: Definition): Set[FunDef] = {
+ visibleDefsFrom(df).collect {
+ case fd: FunDef => fd
+ }
+ }
+
/** Returns true for strict superpackage */
def isSuperPackageOf(p1:PackageRef, p2 : PackageRef) =
(p2.length > p1.length) &&
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index f0dd2d242c212ce3aeb58b3d59645413dc9d8da8..bfba3388ce06d6d22834d1124c5729dbfecdf62b 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -17,7 +17,7 @@ case class ChooseInfo(ctx: LeonContext,
options: SynthesisOptions) {
val problem = Problem.fromChoose(ch, pc)
- val synthesizer = new Synthesizer(ctx, Some(fd), prog, problem, options)
+ val synthesizer = new Synthesizer(ctx, fd, prog, problem, options)
}
object ChooseInfo {
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 6aa67da6b09184fa86df2e6f477d9ce7ffc8be00..63ed6da246ea56551e9dc76d7a806dc70b2d220f 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -16,7 +16,7 @@ import java.util.concurrent.atomic.AtomicBoolean
case class SynthesisContext(
context: LeonContext,
options: SynthesisOptions,
- functionContext: Option[FunDef],
+ functionContext: FunDef,
program: Program,
reporter: Reporter
) {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 938960f506c1ceb8d50a0ee3fa69c41afdb12786..5ac84fa238f247b9d1da5f6db064fc3fde7dc26e 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -18,7 +18,7 @@ import java.io.File
import synthesis.search._
class Synthesizer(val context : LeonContext,
- val functionContext: Option[FunDef],
+ val functionContext: FunDef,
val program: Program,
val problem: Problem,
val options: SynthesisOptions) {
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 7ebe6c9cb05ee004ac62092b8b947b5c55acb067..6109038c7aa401569816da9afd37acefc8806a69 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -12,6 +12,7 @@ import purescala.Common._
import purescala.Definitions._
import purescala.TypeTrees._
import purescala.TreeOps._
+import purescala.DefOps._
import purescala.TypeTreeOps._
import purescala.Extractors._
import purescala.ScalaPrinter
@@ -114,13 +115,9 @@ case object CEGIS extends Rule("CEGIS") {
if (useFunGenerators) {
def isCandidate(fd: FunDef): Option[TypedFunDef] = {
// Prevents recursive calls
- val isRecursiveCall = sctx.functionContext match {
- case Some(cfd) =>
- (sctx.program.callGraph.transitiveCallers(cfd) + cfd) contains fd
- case None =>
- false
- }
+ val cfd = sctx.functionContext
+ val isRecursiveCall = (sctx.program.callGraph.transitiveCallers(cfd) + cfd) contains fd
val isNotSynthesizable = fd.body match {
case Some(b) =>
@@ -148,7 +145,7 @@ case object CEGIS extends Rule("CEGIS") {
case Some(alts) =>
alts
case None =>
- val alts = sctx.program.definedFunctions.flatMap(isCandidate)
+ val alts = visibleFunDefsFrom(sctx.functionContext).toSeq.flatMap(isCandidate)
funcCache += t -> alts
alts
}
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index a556097db125dcf73ca67ca3e1efbd2790d6ed09..ca97ed85933ee396bc40d3797c6b714323848e24 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -89,13 +89,10 @@ case object TEGIS extends Rule("TEGIS") {
def getFcallGenerators(t: TypeTree): Seq[Generator[TypeTree, Expr]] = {
def isCandidate(fd: FunDef): Option[TypedFunDef] = {
// Prevents recursive calls
- val isRecursiveCall = sctx.functionContext match {
- case Some(cfd) =>
- (sctx.program.callGraph.transitiveCallers(cfd) + cfd) contains fd
- case None =>
- false
- }
+ val cfd = sctx.functionContext
+
+ val isRecursiveCall = (sctx.program.callGraph.transitiveCallers(cfd) + cfd) contains fd
val isNotSynthesizable = fd.body match {
case Some(b) =>
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3d535a9bac8dcd7ee6dfd8e6eb039ca012ea3e8a
--- /dev/null
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -0,0 +1,34 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+package utils
+
+import purescala.Definitions._
+import purescala.TypeTrees._
+import purescala.TypeTreeOps._
+import purescala.Trees._
+
+object Helpers {
+ def functionsReturning(fds: Set[FunDef], tpe: TypeTree): Set[TypedFunDef] = {
+ fds.flatMap { fd =>
+ val free = fd.tparams.map(_.tp)
+ canBeSubtypeOf(fd.returnType, free, tpe) match {
+ case Some(tpsMap) =>
+ Some(fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp))))
+ case None =>
+ None
+ }
+ }
+ }
+
+ def definitionsAvailable(p: Program, from: Definition): Set[Definition] = {
+ Set()
+ }
+
+ def functionsAvailable(p: Program, from: Definition): Set[FunDef] = {
+ definitionsAvailable(p, from).collect {
+ case fd: FunDef => fd
+ }
+ }
+}
diff --git a/src/test/scala/leon/test/codegen/CodeGenTests.scala b/src/test/scala/leon/test/codegen/CodeGenTests.scala
index ca1a56f97eb773ea2322dc65453bad67764b20da..d4221906bb84c9d0c4dafdfac81e7c16d972a752 100644
--- a/src/test/scala/leon/test/codegen/CodeGenTests.scala
+++ b/src/test/scala/leon/test/codegen/CodeGenTests.scala
@@ -56,11 +56,9 @@ class CodeGenTests extends test.LeonTestSuite {
private def testCodeGen(prog : TestCase, requireMonitor : Boolean, doInstrument : Boolean) { test(prog.name) {
import prog._
- val settings = testContext.settings.copy(injectLibrary = false)
val ctx = testContext.copy(
// We want a reporter that actually prints some output
- reporter = new DefaultReporter(settings),
- settings = settings
+ reporter = new DefaultReporter(testContext.settings)
)
val ast = pipeline.run(ctx)( (content, List()) )
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 2673b0ab4abe997897cde2b790d6fc6ec1bcd825..bc203c2b817a738baa20e41056ed85d3e0132621 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -11,6 +11,7 @@ import leon.frontends.scalac.ExtractionPhase
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
+import leon.purescala.DefOps._
import leon.purescala.TypeTrees._
class EvaluatorsTests extends leon.test.LeonTestSuite {
@@ -37,16 +38,27 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
private def mkCall(name : String, args : Expr*)(implicit p : Program) = {
- val fDef = p.definedFunctions.find(_.id.name == name) getOrElse {
- throw new AssertionError("No function named '%s' defined in program.".format(name))
+ p.definedFunctions.foreach { fd =>
+ println(fullName(fd))
}
- FunctionInvocation(fDef.typed, args.toSeq)
+ val fn = s"<empty>.Program.$name"
+
+ searchByFullName(fn, p) match {
+ case Some(fd: FunDef) =>
+ FunctionInvocation(fd.typed, args.toSeq)
+ case _ =>
+ throw new AssertionError("No function named '%s' defined in program.".format(fn))
+ }
}
private def mkCaseClass(name : String, args : Expr*)(implicit p : Program) = {
- val ccDef = p.caseClassDef(name)
- CaseClass(CaseClassType(ccDef, Nil), args.toSeq)
+ searchByFullName("Program."+name, p) match {
+ case Some(ccd: CaseClassDef) =>
+ CaseClass(CaseClassType(ccd, Nil), args.toSeq)
+ case _ =>
+ throw new AssertionError("No case class named '%s' defined in program.".format(name))
+ }
}
private def checkCompSuccess(evaluator : Evaluator, in : Expr) : Expr = {
diff --git a/src/test/scala/leon/test/frontends/FrontEndsTest.scala b/src/test/scala/leon/test/frontends/FrontEndsTest.scala
index b974f7880a4324ca0311247e5befa04ee8529dc7..553dbf1b7581c0563e1c70ff9260326966b320a7 100644
--- a/src/test/scala/leon/test/frontends/FrontEndsTest.scala
+++ b/src/test/scala/leon/test/frontends/FrontEndsTest.scala
@@ -45,20 +45,19 @@ class FrontEndsTest extends leon.test.LeonTestSuite {
// Compile original file
val timeOut = 2
val settings = testContext.settings.copy(
- debugSections = Set(),
- injectLibrary = false //true
+ debugSections = Set()
)
val ctx1 = testContext.copy(
// We want a reporter that actually prints some output
//reporter = new DefaultReporter(settings),
settings = settings,
- options = testContext.options :+ LeonValueOption("o", outFileName1) //:+ LeonFlagOption("library", true)
+ options = testContext.options :+ LeonValueOption("o", outFileName1)
)
val ctx2 = ctx1.copy(
//reporter = new DefaultReporter(settings),
settings = settings,
- options = testContext.options :+ LeonValueOption("o", outFileName2 ) //:+ LeonFlagOption("library", true)
+ options = testContext.options :+ LeonValueOption("o", outFileName2 )
)
pipeline1.run(ctx1)(List(f.getAbsolutePath()))
diff --git a/src/test/scala/leon/test/frontends/Imports.scala b/src/test/scala/leon/test/frontends/Imports.scala
index 1475a7cd8da99f51717a901ee1b744d73cdcd778..01645c5a99f8352eb448429286109e5ebe8e2bc2 100644
--- a/src/test/scala/leon/test/frontends/Imports.scala
+++ b/src/test/scala/leon/test/frontends/Imports.scala
@@ -13,8 +13,7 @@ import utils._
class ImportsTests extends LeonTestSuite {
private def parseStrings(strs : List[String]) : Program = {
val settings : Settings = Settings(
- verify = false,
- injectLibrary = false
+ verify = false
)
val reporter = new DefaultReporter(settings)
val context : LeonContext = LeonContext(
diff --git a/src/test/scala/leon/test/purescala/DefOpsTests.scala b/src/test/scala/leon/test/purescala/DefOpsTests.scala
index ce19061f9e9b0602de72caaedacc22c522da40f6..605e5012b7bf8eecdd27bfe8473c0001efd36c25 100644
--- a/src/test/scala/leon/test/purescala/DefOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/DefOpsTests.scala
@@ -13,8 +13,7 @@ import leon.test.LeonTestSuite
private [purescala] object DefOpsHelper {
private def parseStrings(strs : List[String]) : Program = {
val settings : Settings = Settings(
- verify = false,
- injectLibrary = false
+ verify = false
)
val reporter = new DefaultReporter(settings)
val context : LeonContext = LeonContext(
@@ -122,4 +121,4 @@ class DefOpsTests extends LeonTestSuite {
mustFail("!!!", "Don't find definition that is root of a wildcard import")
mustFail("m.x", "Don't find imported definition shadowed by local definition")
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 7531e24ccb99e3879139a30b11db8f3983026bcb..e79a022db1348b9956c3d2c623e80fe358fd33b8 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -28,7 +28,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
var chooses = List[ChooseInfo]()
test(cat+": "+f.getName()+" Compilation") {
- val ctx = createLeonContext("--synthesis", "--library")
+ val ctx = createLeonContext("--synthesis")
val opts = SynthesisOptions(searchBound = Some(bound), allSeeing = true)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index cbcc3f2305e5f624174d9c7edce6c997d12d417f..3d5efd0bb06dcbcb93c6d1d501eff0022f5e4bc3 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -41,7 +41,7 @@ class SynthesisSuite extends LeonTestSuite {
val sctx = SynthesisContext(ctx,
opts,
- Some(f),
+ f,
program,
ctx.reporter)
diff --git a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
index faf107ebb18d05480c93dcccbc21c35c37ef515c..700c1b193d77e15ab531ea0dde04d86a8069d5cd 100644
--- a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
@@ -18,7 +18,7 @@ class LibraryVerificationRegression extends LeonTestSuite {
PreprocessingPhase andThen
AnalysisPhase
- val ctx = Main.processOptions(Seq("--library", "--functions=_")).copy(reporter = new TestSilentReporter())
+ val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
val report = pipeline.run(ctx)(Nil)
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index a5212585405a27b0a61840e576a6a888517eaa98..71148aa5df64c13fd3e2cc05140d45409f69093a 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -80,14 +80,14 @@ class PureScalaVerificationRegression extends LeonTestSuite {
}
for(f <- fs) {
- mkTest(f, List("--feelinglucky", "--library=no"), forError)(block)
- mkTest(f, List("--codegen", "--evalground", "--feelinglucky", "--library=no"), forError)(block)
- mkTest(f, List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky", "--library=no"), forError)(block)
+ mkTest(f, List("--feelinglucky"), forError)(block)
+ mkTest(f, List("--codegen", "--evalground", "--feelinglucky"), forError)(block)
+ mkTest(f, List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky"), forError)(block)
if (isZ3Available) {
- mkTest(f, List("--solvers=smt-z3", "--feelinglucky", "--library=no"), forError)(block)
+ mkTest(f, List("--solvers=smt-z3", "--feelinglucky"), forError)(block)
}
if (isCVC4Available) {
- mkTest(f, List("--solvers=smt-cvc4", "--feelinglucky", "--library=no"), forError)(block)
+ mkTest(f, List("--solvers=smt-cvc4", "--feelinglucky"), forError)(block)
}
}
}