diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 69641b8b25d3078a87418e850ed7a56eb54182c4..1ad827129aeaa1951219f66f004e68306ba39a47 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -70,7 +70,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
}
}
- if (synth.options.generateDerivationTrees) {
+ if (synth.settings.generateDerivationTrees) {
val dot = new DotGenerator(search.g)
dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
}
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 2f31d5129d02c0174ec21887b980999cf7622141..1cf50638d2f5bef46ab384370f0fad7d521b1333 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -16,14 +16,14 @@ case class ChooseInfo(ctx: LeonContext,
pc: Expr,
source: Expr,
ch: Choose,
- options: SynthesisOptions) {
+ settings: SynthesisSettings) {
val problem = Problem.fromChoose(ch, pc)
- val synthesizer = new Synthesizer(ctx, fd, prog, problem, options)
+ val synthesizer = new Synthesizer(ctx, fd, prog, problem, settings)
}
object ChooseInfo {
- def extractFromProgram(ctx: LeonContext, prog: Program, options: SynthesisOptions): List[ChooseInfo] = {
+ def extractFromProgram(ctx: LeonContext, prog: Program, options: SynthesisSettings): List[ChooseInfo] = {
// Look for choose()
val results = for (f <- prog.definedFunctions if f.body.isDefined;
@@ -34,7 +34,7 @@ object ChooseInfo {
results.sortBy(_.source.getPos)
}
- def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef, options: SynthesisOptions): Seq[ChooseInfo] = {
+ def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef, options: SynthesisSettings): Seq[ChooseInfo] = {
val fterm = prog.library.terminating.getOrElse(ctx.reporter.fatalError("No library ?!?"))
val actualBody = and(fd.precondition.getOrElse(BooleanLiteral(true)), fd.body.get)
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 63ed6da246ea56551e9dc76d7a806dc70b2d220f..c18153ccfdb1c359250d7e35cc68cdfc7f36147b 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -15,20 +15,20 @@ import java.util.concurrent.atomic.AtomicBoolean
case class SynthesisContext(
context: LeonContext,
- options: SynthesisOptions,
+ settings: SynthesisSettings,
functionContext: FunDef,
program: Program,
reporter: Reporter
) {
- val rules = options.rules
+ val rules = settings.rules
val allSolvers: Map[String, SolverFactory[SynthesisContext.SynthesisSolver]] = Map(
"fairz3" -> SolverFactory(() => new FairZ3Solver(context, program) with TimeoutAssumptionSolver),
"enum" -> SolverFactory(() => new EnumerationSolver(context, program) with TimeoutAssumptionSolver)
)
- val solversToUse = allSolvers.filterKeys(options.selectedSolvers)
+ val solversToUse = allSolvers.filterKeys(settings.selectedSolvers)
val solverFactory: SolverFactory[SynthesisContext.SynthesisSolver] = if (solversToUse.isEmpty) {
reporter.fatalError("No solver selected. Aborting")
@@ -56,7 +56,7 @@ object SynthesisContext {
def fromSynthesizer(synth: Synthesizer) = {
SynthesisContext(
synth.context,
- synth.options,
+ synth.settings,
synth.functionContext,
synth.program,
synth.reporter)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index d7ff62406ef077d197969afa6078f89a3d4e7421..17abfd860da1e0ab48ee1f9bac0afbe0b08b1092 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -37,8 +37,8 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
LeonFlagOptionDef( "holes:discrete", "--holes:discrete", "Oracles get split", false)
)
- def processOptions(ctx: LeonContext): SynthesisOptions = {
- var options = SynthesisOptions()
+ def processOptions(ctx: LeonContext): SynthesisSettings = {
+ var options = SynthesisSettings()
for(opt <- ctx.options) opt match {
case LeonFlagOption("manual", v) =>
@@ -141,7 +141,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
val fd = ci.fd
- if (ci.synthesizer.options.generateDerivationTrees) {
+ if (ci.synthesizer.settings.generateDerivationTrees) {
val dot = new DotGenerator(search.g)
dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
}
diff --git a/src/main/scala/leon/synthesis/SynthesisOptions.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
similarity index 97%
rename from src/main/scala/leon/synthesis/SynthesisOptions.scala
rename to src/main/scala/leon/synthesis/SynthesisSettings.scala
index 24a878c8ab71a2baebc9cb472d378c2bd5ec2bf6..c6a1fb1b697cc7feedf06b2a72d74f4fd0366ef2 100644
--- a/src/main/scala/leon/synthesis/SynthesisOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala
@@ -6,7 +6,7 @@ package synthesis
import scala.language.existentials
import leon.purescala.Definitions.FunDef
-case class SynthesisOptions(
+case class SynthesisSettings(
inPlace: Boolean = false,
allSeeing: Boolean = false,
generateDerivationTrees: Boolean = false,
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 0a0a2f3186fb65d7ca7c7e72ebaa65a94ba05db8..cd98f703b0af4fb1e4e849792486586b25ebd021 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -22,18 +22,18 @@ class Synthesizer(val context : LeonContext,
val functionContext: FunDef,
val program: Program,
val problem: Problem,
- val options: SynthesisOptions) {
+ val settings: SynthesisSettings) {
val reporter = context.reporter
def getSearch(): Search = {
- if (options.manualSearch) {
- new ManualSearch(context, problem, options.costModel)
- } else if (options.searchWorkers > 1) {
+ if (settings.manualSearch) {
+ new ManualSearch(context, problem, settings.costModel)
+ } else if (settings.searchWorkers > 1) {
???
//new ParallelSearch(this, problem, options.searchWorkers)
} else {
- new SimpleSearch(context, problem, options.costModel, options.searchBound)
+ new SimpleSearch(context, problem, settings.costModel, settings.searchBound)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index da431e8c0c14bca7346be58d523395f6dbb30fde..d95ac13a3212a9f5e5ed579d15aa70f81a009b0f 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -42,16 +42,16 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
// CEGIS Flags to actiave or de-activate features
- val useUninterpretedProbe = sctx.options.cegisUseUninterpretedProbe
- val useUnsatCores = sctx.options.cegisUseUnsatCores
- val useOptTimeout = sctx.options.cegisUseOptTimeout
- val useVanuatoo = sctx.options.cegisUseVanuatoo
- val useCETests = sctx.options.cegisUseCETests
- val useCEPruning = sctx.options.cegisUseCEPruning
+ val useUninterpretedProbe = sctx.settings.cegisUseUninterpretedProbe
+ val useUnsatCores = sctx.settings.cegisUseUnsatCores
+ val useOptTimeout = sctx.settings.cegisUseOptTimeout
+ val useVanuatoo = sctx.settings.cegisUseVanuatoo
+ val useCETests = sctx.settings.cegisUseCETests
+ val useCEPruning = sctx.settings.cegisUseCEPruning
// Limits the number of programs CEGIS will specifically test for instead of reasonning symbolically
val testUpTo = 5
- val useBssFiltering = sctx.options.cegisUseBssFiltering
+ val useBssFiltering = sctx.settings.cegisUseBssFiltering
val filterThreshold = 1.0/2
val evalParams = CodeGenParams(maxFunctionInvocations = 2000)
lazy val evaluator = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
index b0f8d711aeb5c7a58291f98b3ec3787c99ecc68a..97b10158a33363e8757b7e0e7abfdc4a5728ae2e 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -23,7 +23,7 @@ case object InlineHoles extends Rule("Inline-Holes") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
// When true: withOracle gets converted into a big choose() on result.
- val discreteHoles = sctx.options.distreteHoles
+ val discreteHoles = sctx.settings.distreteHoles
if (!discreteHoles) {
return Nil;
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 1c9fc66c9e575abe6ffc814e1b0456e695fb8ed4..9e4ea49adf2a7006ddee93ce506ed2125d25cc45 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -169,7 +169,7 @@ object ExpressionGrammars {
case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[Label[String]] {
- val excludeFCalls = sctx.options.functionsToIgnore
+ val excludeFCalls = sctx.settings.functionsToIgnore
val normalGrammar = EmbeddedGrammar(
BaseGrammar ||
@@ -392,6 +392,6 @@ object ExpressionGrammars {
}
def default(sctx: SynthesisContext, p: Problem): ExpressionGrammar[TypeTree] = {
- default(sctx.program, p.as.map(_.toVariable), sctx.functionContext, sctx.options.functionsToIgnore, p.ws, p.pc)
+ default(sctx.program, p.as.map(_.toVariable), sctx.functionContext, sctx.settings.functionsToIgnore, p.ws, p.pc)
}
}
diff --git a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
index 625f1fa947d6885d6ed8b9bb43a15b040a8d0ac3..7c53eb560e299311ad30c6eb7f86c140e4f2f80f 100644
--- a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
@@ -35,7 +35,7 @@ class StablePrintingSuite extends LeonTestSuite {
private def testIterativeSynthesis(cat: String, f: File, depth: Int) {
def getChooses(ctx: LeonContext, content: String): (Program, Seq[ChooseInfo]) = {
- val opts = SynthesisOptions()
+ val opts = SynthesisSettings()
val pipeline = leon.utils.TemporaryInputPhase andThen
frontends.scalac.ExtractionPhase andThen
leon.utils.PreprocessingPhase andThen
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 89fe46ea027307e4be12f42e1022e5c79011e256..1e6ed1bd758b2580b044edbde73dabf5c784fffd 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -30,7 +30,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
test(cat+": "+f.getName()+" Compilation") {
val ctx = createLeonContext("--synthesis")
- val opts = SynthesisOptions(searchBound = Some(bound), allSeeing = true)
+ val opts = SynthesisSettings(searchBound = Some(bound), allSeeing = true)
val pipeline = leon.frontends.scalac.ExtractionPhase andThen leon.utils.PreprocessingPhase
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index a21d3e7c1b58cbd6ff7931f147f8fc27d37edafb..9ba2f98f71bbf864ac6a0e5ee477458010317d7a 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -23,7 +23,7 @@ class SynthesisSuite extends LeonTestSuite {
counter
}
- def forProgram(title: String, opts: SynthesisOptions = SynthesisOptions())(content: String)(block: (SynthesisContext, FunDef, Problem) => Unit) {
+ def forProgram(title: String, opts: SynthesisSettings = SynthesisSettings())(content: String)(block: (SynthesisContext, FunDef, Problem) => Unit) {
test("Synthesizing %3d: [%s]".format(nextInt(), title)) {
val ctx = testContext.copy(settings = Settings(
@@ -114,7 +114,7 @@ class SynthesisSuite extends LeonTestSuite {
}
}
- forProgram("Ground Enum", SynthesisOptions(selectedSolvers = Set("enum")))(
+ forProgram("Ground Enum", SynthesisSettings(selectedSolvers = Set("enum")))(
"""
import leon.annotation._
import leon.lang._