From 5c083d1b88a35c2659b2d539dcb6487db1a08fcc Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 4 Nov 2015 14:39:19 +0100
Subject: [PATCH] ChooseInfo -> SourceInfo
---
src/main/scala/leon/repair/Repairman.scala | 2 +-
src/main/scala/leon/synthesis/FileInterface.scala | 2 +-
src/main/scala/leon/synthesis/Problem.scala | 2 +-
src/main/scala/leon/synthesis/SearchContext.scala | 2 +-
.../synthesis/{ChooseInfo.scala => SourceInfo.scala} | 12 ++++++------
src/main/scala/leon/synthesis/SynthesisPhase.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 2 +-
src/main/scala/leon/synthesis/graph/Search.scala | 6 +++---
.../utils/SynthesisProblemExtractionPhase.scala | 6 +++---
.../regression/synthesis/StablePrintingSuite.scala | 4 ++--
.../synthesis/SynthesisRegressionSuite.scala | 4 ++--
.../leon/regression/synthesis/SynthesisSuite.scala | 2 +-
12 files changed, 23 insertions(+), 23 deletions(-)
rename src/main/scala/leon/synthesis/{ChooseInfo.scala => SourceInfo.scala} (89%)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index e62ee6658..3dd72ad61 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -133,7 +133,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val guide = Guide(origBody)
val pre = fd.precOrTrue
- val ci = ChooseInfo(
+ val ci = SourceInfo(
fd = fd,
pc = andJoin(Seq(pre, guide, term)),
source = origBody,
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 94bb363c4..25edd338f 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -14,7 +14,7 @@ import leon.utils.RangePosition
import java.io.File
class FileInterface(reporter: Reporter) {
- def updateFile(origFile: File, solutions: Map[ChooseInfo, Expr])(implicit ctx: LeonContext) {
+ def updateFile(origFile: File, solutions: Map[SourceInfo, Expr])(implicit ctx: LeonContext) {
import java.io.{File, BufferedWriter, FileWriter}
val FileExt = """^(.+)\.([^.]+)$""".r
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index a48e3111d..cf3640f70 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -57,7 +57,7 @@ object Problem {
Problem(as, andJoin(wss), andJoin(pcs), phi, xs, eb)
}
- def fromChooseInfo(ci: ChooseInfo): Problem = {
+ def fromSourceInfo(ci: SourceInfo): Problem = {
// Same as fromChoose, but we order the input variables by the arguments of
// the functions, so that tests are compatible
val p = fromSpec(ci.spec, ci.pc, ci.eb)
diff --git a/src/main/scala/leon/synthesis/SearchContext.scala b/src/main/scala/leon/synthesis/SearchContext.scala
index 5fc938b77..1ee7361d5 100644
--- a/src/main/scala/leon/synthesis/SearchContext.scala
+++ b/src/main/scala/leon/synthesis/SearchContext.scala
@@ -11,7 +11,7 @@ import graph._
*/
case class SearchContext (
sctx: SynthesisContext,
- ci: ChooseInfo,
+ ci: SourceInfo,
currentNode: Node,
search: Search
) {
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
similarity index 89%
rename from src/main/scala/leon/synthesis/ChooseInfo.scala
rename to src/main/scala/leon/synthesis/SourceInfo.scala
index 20eeb723f..fc8a9bbd8 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -9,17 +9,17 @@ import purescala.Expressions._
import purescala.ExprOps._
import Witnesses._
-case class ChooseInfo(fd: FunDef,
+case class SourceInfo(fd: FunDef,
pc: Expr,
source: Expr,
spec: Expr,
eb: ExamplesBank) {
- val problem = Problem.fromChooseInfo(this)
+ val problem = Problem.fromSourceInfo(this)
}
-object ChooseInfo {
- def extractFromProgram(ctx: LeonContext, prog: Program): List[ChooseInfo] = {
+object SourceInfo {
+ def extractFromProgram(ctx: LeonContext, prog: Program): List[SourceInfo] = {
val functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet }
def excludeByDefault(fd: FunDef): Boolean = {
@@ -40,7 +40,7 @@ object ChooseInfo {
results.sortBy(_.source.getPos)
}
- def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef): Seq[ChooseInfo] = {
+ def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef): Seq[SourceInfo] = {
val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
@@ -56,7 +56,7 @@ object ChooseInfo {
ExamplesBank.empty
}
- val ci = ChooseInfo(fd, and(path, term), ch, ch.pred, outerEb)
+ val ci = SourceInfo(fd, and(path, term), ch, ch.pred, outerEb)
val pcEb = eFinder.generateForPC(ci.problem.as, path, 20)
val chooseEb = eFinder.extractFromProblem(ci.problem)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index dabd354e0..72cfffec3 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -65,7 +65,7 @@ object SynthesisPhase extends TransformationPhase {
def apply(ctx: LeonContext, program: Program): Program = {
val options = processOptions(ctx)
- val chooses = ChooseInfo.extractFromProgram(ctx, program)
+ val chooses = SourceInfo.extractFromProgram(ctx, program)
var functions = Set[FunDef]()
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 54e305adf..35fdfb845 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -15,7 +15,7 @@ import synthesis.graph._
class Synthesizer(val context : LeonContext,
val program: Program,
- val ci: ChooseInfo,
+ val ci: SourceInfo,
val settings: SynthesisSettings) {
val problem = ci.problem
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index c33a31ceb..98554a5ae 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -10,7 +10,7 @@ import scala.collection.mutable.ArrayBuffer
import leon.utils.Interruptible
import java.util.concurrent.atomic.AtomicBoolean
-abstract class Search(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: CostModel) extends Interruptible {
+abstract class Search(ctx: LeonContext, ci: SourceInfo, p: Problem, costModel: CostModel) extends Interruptible {
val g = new Graph(costModel, p)
def findNodeToExpandFrom(n: Node): Option[Node]
@@ -83,7 +83,7 @@ abstract class Search(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: C
ctx.interruptManager.registerForInterrupts(this)
}
-class SimpleSearch(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: CostModel, bound: Option[Int]) extends Search(ctx, ci, p, costModel) {
+class SimpleSearch(ctx: LeonContext, ci: SourceInfo, p: Problem, costModel: CostModel, bound: Option[Int]) extends Search(ctx, ci, p, costModel) {
val expansionBuffer = ArrayBuffer[Node]()
def findIn(n: Node) {
@@ -124,7 +124,7 @@ class SimpleSearch(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: Cost
}
}
-class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel: CostModel, initCmd: Option[String]) extends Search(ctx, ci, problem, costModel) {
+class ManualSearch(ctx: LeonContext, ci: SourceInfo, problem: Problem, costModel: CostModel, initCmd: Option[String]) extends Search(ctx, ci, problem, costModel) {
import ctx.reporter._
abstract class Command
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index dfd1360d5..c3df2a382 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -7,14 +7,14 @@ package utils
import purescala.DefOps.funDefsFromMain
import purescala.Definitions._
-object SynthesisProblemExtractionPhase extends SimpleLeonPhase[Program, (Program, Map[FunDef, Seq[ChooseInfo]])] {
+object SynthesisProblemExtractionPhase extends SimpleLeonPhase[Program, (Program, Map[FunDef, Seq[SourceInfo]])] {
val name = "Synthesis Problem Extraction"
val description = "Synthesis Problem Extraction"
- def apply(ctx: LeonContext, p: Program): (Program, Map[FunDef, Seq[ChooseInfo]]) = {
+ def apply(ctx: LeonContext, p: Program): (Program, Map[FunDef, Seq[SourceInfo]]) = {
// Look for choose()
val results = for (f <- funDefsFromMain(p).toSeq.sortBy(_.id) if f.body.isDefined) yield {
- f -> ChooseInfo.extractFromFunction(ctx, p, f)
+ f -> SourceInfo.extractFromFunction(ctx, p, f)
}
(p, results.toMap)
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index 2daccc24d..c8bfc2688 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -50,7 +50,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
InnerCaseSplit
)
- def getChooses(ctx: LeonContext, content: String): (Program, SynthesisSettings, Seq[ChooseInfo]) = {
+ def getChooses(ctx: LeonContext, content: String): (Program, SynthesisSettings, Seq[SourceInfo]) = {
val opts = SynthesisSettings()
val pipeline = leon.utils.TemporaryInputPhase andThen
frontends.scalac.ExtractionPhase andThen
@@ -58,7 +58,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
val (ctx2, program) = pipeline.run(ctx, (List(content), Nil))
- (program, opts, ChooseInfo.extractFromProgram(ctx2, program))
+ (program, opts, SourceInfo.extractFromProgram(ctx2, program))
}
case class Job(content: String, choosesToProcess: Set[Int], rules: List[String]) {
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
index b5e4bfe99..9dbb0e36f 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
@@ -21,7 +21,7 @@ class SynthesisRegressionSuite extends LeonRegressionSuite {
private def testSynthesis(cat: String, f: File, bound: Int) {
- var chooses = List[ChooseInfo]()
+ var chooses = List[SourceInfo]()
var program: Program = null
var ctx: LeonContext = null
var opts: SynthesisSettings = null
@@ -37,7 +37,7 @@ class SynthesisRegressionSuite extends LeonRegressionSuite {
program = pgm2
- chooses = ChooseInfo.extractFromProgram(ctx2, program)
+ chooses = SourceInfo.extractFromProgram(ctx2, program)
}
for (ci <- chooses) {
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
index f95d7b964..e7c5fbf2a 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
@@ -24,7 +24,7 @@ class SynthesisSuite extends LeonRegressionSuite {
class TestSearch(ctx: LeonContext,
- ci: ChooseInfo,
+ ci: SourceInfo,
p: Problem,
strat: SynStrat) extends SimpleSearch(ctx, ci, p, CostModels.default, None) {
--
GitLab