From ff8c29a47e070e0247f79a54ea6386736a5a3044 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 8 Apr 2014 01:04:05 +0200
Subject: [PATCH] Move condition abduction to a feature branch
---
.../scala/leon/synthesis/SynthesisPhase.scala | 1 -
.../scala/leon/synthesis/condabd/Report.scala | 68 --
.../synthesis/condabd/SynthesisInfo.scala | 78 --
.../condabd/SynthesizerExamples.scala | 780 ------------------
.../evaluation/CodeGenExampleRunner.scala | 138 ----
.../evaluation/DefaultExampleRunner.scala | 90 --
.../evaluation/EvaluationStrategy.scala | 113 ---
.../condabd/evaluation/ExampleRunner.scala | 43 -
.../synthesis/condabd/examples/Example.scala | 15 -
.../condabd/examples/InputExamples.scala | 186 -----
.../synthesis/condabd/insynth/InSynth.scala | 77 --
.../condabd/insynth/leon/CommonTypes.scala | 16 -
.../insynth/leon/DomainTypeTransformer.scala | 55 --
.../insynth/leon/LeonDeclaration.scala | 53 --
.../leon/ReconstructionExpression.scala | 75 --
.../insynth/leon/TypeTransformer.scala | 55 --
.../leon/loader/DeclarationFactory.scala | 86 --
.../insynth/leon/loader/LoadSpec.scala | 8 -
.../condabd/insynth/leon/loader/Loader.scala | 251 ------
.../insynth/leon/loader/PreLoader.scala | 274 ------
.../insynth/leon/query/LeonQuery.scala | 23 -
.../insynth/leon/query/LeonQueryBuilder.scala | 28 -
.../insynth/reconstruction/Output.scala | 19 -
.../reconstruction/Reconstructor.scala | 37 -
.../codegen/CodeGenerator.scala | 118 ---
.../synthesis/condabd/ranking/Candidate.scala | 119 ---
.../condabd/ranking/Evaluation.scala | 69 --
.../synthesis/condabd/ranking/Ranker.scala | 150 ----
.../synthesis/condabd/refinement/Filter.scala | 160 ----
.../condabd/refinement/VariableRefiner.scala | 69 --
.../refinement/VariableRefinerCompose.scala | 50 --
.../refinement/VariableRefinerExecution.scala | 106 ---
.../refinement/VariableRefinerStructure.scala | 64 --
.../refinement/VariableSolverRefiner.scala | 113 ---
.../ConditionAbductionSynthesisTwoPhase.scala | 92 ---
.../verification/AbstractVerifier.scala | 125 ---
.../verification/RelaxedVerifier.scala | 80 --
.../condabd/verification/Verifier.scala | 73 --
.../leon/test/condabd/EvaluationTest.scala | 331 --------
.../leon/test/condabd/VerifierTest.scala | 159 ----
.../condabd/enumeration/EnumeratorTest.scala | 417 ----------
.../test/condabd/insynth/InSynthTest.scala | 299 -------
.../condabd/insynth/loader/LoaderTest.scala | 133 ---
.../reconstruction/CodeGeneratorTest.scala | 62 --
.../reconstruction/ReconstructorTest.scala | 106 ---
.../insynth/testutil/CommonDeclarations.scala | 118 ---
.../insynth/testutil/CommonLambda.scala | 189 -----
.../testutil/CommonLeonExpressions.scala | 26 -
.../insynth/testutil/CommonProofTrees.scala | 220 -----
.../insynth/testutil/CommonUtils.scala | 22 -
.../test/condabd/refinement/FilterTest.scala | 240 ------
.../refinement/RefinementExamples.scala | 77 --
.../VariableRefinerComposeTest.scala | 152 ----
.../VariableRefinerExecutionTest.scala | 300 -------
.../VariableRefinerStructureTest.scala | 72 --
.../VariableSolverRefinerTest.scala | 213 -----
.../leon/test/condabd/util/Scaffold.scala | 98 ---
.../scala/leon/test/condabd/util/Utils.scala | 35 -
58 files changed, 7226 deletions(-)
delete mode 100644 src/main/scala/leon/synthesis/condabd/Report.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/examples/Example.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerCompose.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerExecution.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerStructure.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
delete mode 100644 src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
delete mode 100644 src/test/scala/leon/test/condabd/EvaluationTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/VerifierTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
delete mode 100644 src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
delete mode 100644 src/test/scala/leon/test/condabd/refinement/FilterTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/refinement/RefinementExamples.scala
delete mode 100644 src/test/scala/leon/test/condabd/refinement/VariableRefinerComposeTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/refinement/VariableRefinerExecutionTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/refinement/VariableRefinerStructureTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/refinement/VariableSolverRefinerTest.scala
delete mode 100644 src/test/scala/leon/test/condabd/util/Scaffold.scala
delete mode 100644 src/test/scala/leon/test/condabd/util/Utils.scala
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index d8756d3c8..98e8a8d6e 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -112,7 +112,6 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
if (options.manualSearch) {
options = options.copy(
rules = rules.AsChoose +:
- condabd.rules.ConditionAbductionSynthesisTwoPhase +:
options.rules
)
}
diff --git a/src/main/scala/leon/synthesis/condabd/Report.scala b/src/main/scala/leon/synthesis/condabd/Report.scala
deleted file mode 100644
index 9efbdf379..000000000
--- a/src/main/scala/leon/synthesis/condabd/Report.scala
+++ /dev/null
@@ -1,68 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-
-import leon.purescala.Definitions.{ TypedFunDef, ValDef, Program, ModuleDef }
-
-trait Report {
- def summaryString: String
-
- def isSuccess: Boolean
-}
-
-case object EmptyReport extends Report {
- import Report._
-
- implicit val width = 70
-
- override def summaryString =
- infoHeader +
- ("║ %-" + width + "s ║\n").format("No solution found for this synthesis problem.") +
- infoFooter
-
- override def isSuccess = false
-}
-
-case class FullReport(val function: TypedFunDef, val synthInfo: SynthesisInfo) extends Report {
-
- import SynthesisInfo.Action._
- import Report._
-
- val totalTime = synthInfo.getTime(Synthesis)
-
- implicit val width = 70
-
- override def summaryString : String = {
- infoHeader +
- function.toString.split("\n").map {
- ("║ %-" + (width - 2) + "s ║\n").format(_)
- }.mkString +
- infoSep +
- ("║ Generation: %" + (width - 15) + ".2fs ║\n").format(synthInfo.getTime(Generation).toDouble/1000) +
- ("║ Evaluation: %" + (width - 15) + ".2fs ║\n").format(synthInfo.getTime(Evaluation).toDouble/1000) +
- ("║ Verification: %" + (width - 15) + ".2fs ║\n").format(synthInfo.getTime(Verification).toDouble/1000) +
- ("║ Total time: %" + (width - 15) + ".2fs ║\n").format(totalTime.toDouble/1000) +
- infoFooter
- }
-
- override def isSuccess = true
-}
-
-object Report {
- //def emptyReport : Report = new Report(Nil)
-
- def fit(str : String, maxLength : Int) : String = {
- if(str.length <= maxLength) {
- str
- } else {
- str.substring(0, maxLength - 1) + "…"
- }
- }
-
- def infoSep(implicit width: Int) : String = "╟" + ("┄" * width) + "╢\n"
- def infoFooter(implicit width: Int) : String = "╚" + ("═" * width) + "╝"
- def infoHeader(implicit width: Int) : String = ". ┌─────────┐\n" +
- "╔═╡ Summary ╞" + ("═" * (width - 12)) + "╗\n" +
- "║ └─────────┘" + (" " * (width - 12)) + "║\n"
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala b/src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
deleted file mode 100644
index e50b0a72c..000000000
--- a/src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
+++ /dev/null
@@ -1,78 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-
-import leon.StopwatchCollections
-
-/**
- * Contains information about the synthesis process
- */
-class SynthesisInfo {
-
- import SynthesisInfo.Action
-
- // synthesis information
- private var _numberOfEnumeratedExpressions: Long = 0
- def numberOfEnumeratedExpressions = _numberOfEnumeratedExpressions
- def numberOfEnumeratedExpressions_=(numberOfEnumeratedExpressionsIn: Long) =
- _numberOfEnumeratedExpressions = numberOfEnumeratedExpressionsIn
-
- private var _iterations: Int = 0
- def iterations = _iterations
- def iterations_=(iterationsIn: Int) =
- _iterations = iterationsIn
-
- // times
- private var times = new Array[Long](Action.values.size)
- private var startTimes = new Array[Long](Action.values.size)
- private var lastTimes = new Array[Long](Action.values.size)
-
- private var lastAction: Action.Action = Action.Evaluation
-
- def getTime(a: Action.Action) = times(a.id)
-
- def start(a: Action.Action) = {
- lastAction = a
- startTimes(a.id) = System.currentTimeMillis()
- }
-
- def end: Unit = end(lastAction)
-
- def end(a: Action.Action) = {
- lastAction = a
- lastTimes(a.id) = System.currentTimeMillis() - startTimes(a.id)
- times(a.id) += lastTimes(a.id)
- }
-
- def end[T](returnValue: => T): T = {
- val result = returnValue
- end
- result
- }
-
- def last(a: Action.Action) = lastTimes(a.id)
-
- def last: Long = last(lastAction)
-
- def profile[T](a: Action.Action)(block: => T): T = {
- lastAction = a
- startTimes(a.id) = System.currentTimeMillis()
- val result = block // call-by-name
- lastTimes(a.id) = System.currentTimeMillis() - startTimes(a.id)
- times(a.id) += lastTimes(a.id)
- result
- }
-
-}
-
-object SynthesisInfo {
- object Action extends Enumeration {
- type Action = Value
- val Synthesis,
- Verification, Generation, Evaluation = Value
-// VerificationBranch, VerificationCondition,
-// EvaluationGeneration, EvaluationBranch, EvaluationCondition,
-// VerificationCounterExampleGen
-// = Value
- }
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
deleted file mode 100644
index 92e5bfb59..000000000
--- a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
+++ /dev/null
@@ -1,780 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-
-import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
-import scala.collection.mutable.{ PriorityQueue, ArrayBuffer, HashSet }
-import scala.util.control.Breaks._
-
-import leon.{ Reporter, DefaultReporter, LeonContext }
-import leon.Main.processOptions
-
-import leon.solvers._
-import leon.solvers.z3._
-
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Trees.{ Variable => LeonVariable, _ }
-import leon.purescala.Definitions.{ TypedFunDef, FunDef, Program, ModuleDef}
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.TreeOps
-
-import leon.evaluators.EvaluationResults
-import leon.evaluators._
-import leon.synthesis.{ Problem, SynthesisContext }
-
-import insynth._
-import insynth.leon.loader._
-import insynth.leon.{ LeonDeclaration => Declaration, _ }
-import insynth.reconstruction.Output
-
-import _root_.insynth.{ Solver => _, _ }
-import _root_.insynth.engine._
-import _root_.insynth.util.logging.HasLogger
-
-import examples._
-import evaluation._
-import ranking._
-import refinement._
-import verification._
-
-import SynthesisInfo._
-import SynthesisInfo.Action._
-import SynthesisContext.SynthesisSolver
-
-// enable postfix operations
-import scala.language.postfixOps
-
-class SynthesizerForRuleExamples(
- // some synthesis instance information
- val mainSolver: SolverFactory[SynthesisSolver],
- val program: Program,
- val desiredType: LeonType,
- val tfd: TypedFunDef,
- val problem: Problem,
- val synthesisContext: SynthesisContext,
- val evaluationStrategy: EvaluationStrategy, // = DefaultEvaluationStrategy(program, tfd, synthesisContext.context),
- // number of condition expressions to try before giving up on that branch expression
- numberOfBooleanSnippets: Int = 5,
- numberOfCounterExamplesToGenerate: Int = 5,
-// leonTimeout: Int = 1, // seconds
- analyzeSynthesizedFunctionOnly: Boolean = false,
- showLeonOutput: Boolean = false,
- reporter: Reporter,
- //examples: List[Map[Identifier, Expr]] = Nil,
- // we need the holeDef to know the right ids
- introduceExamples: (() => List[Map[Identifier, Expr]]) = { () => Nil },
- collectCounterExamplesFromLeon: Boolean = false,
- filterOutAlreadySeenBranchExpressions: Boolean = true,
- useStringSetForFilterOutAlreadySeenBranchExpressions: Boolean = true,
- numberOfTestsInIteration: Int = 25,
- numberOfCheckInIteration: Int = 5,
- exampleRunnerSteps: Int = 4000) extends HasLogger {
-
- def info(message: String) = {
- reporter.info(message)
- super.info(message)
- }
-
- info("Synthesizer:")
- info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
- info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
-// info("leonTimeout: %d".format(leonTimeout))
-
- info("holeFunDef: %s".format(tfd))
- info("problem: %s".format(problem.toString))
-
- // flag denoting if a correct body has been synthesized
- private var found = false
-
- // objects used in the synthesis
- private var loader: LeonLoader = _
- private var inSynth: InSynth = _
- private var inSynthBoolean: InSynth = _
- // initial declarations
- private var allDeclarations: List[Declaration] = _
-
- // can be used to unnecessary syntheses
- private var variableRefinedBranch = false
- private var variableRefinedCondition = true // assure initial synthesis
- private var booleanExpressionsSaved: Stream[Output] = _
-
- // heuristics that guide the search
- private var variableRefiner: VariableRefiner = _
- private var refiner: Filter = _
- type FilterSet = HashSet[Expr]
- private var seenBranchExpressions: FilterSet = new FilterSet()
- private var successfulCandidates = IndexedSeq[Output]()
-
- // filtering/ranking with examples support
- var exampleRunner: ExampleRunner = _
- var gatheredExamples: ArrayBuffer[Example] = _
-
- // store initial precondition since it will be overwritten
- private var initialPrecondition: Expr = _
- // accumulate precondition for the remaining branch to synthesize
- private var accumulatingCondition: Expr = _
- // accumulate the final expression of the hole
- private var accumulatingExpression: Expr => Expr = _
-
- // information about the synthesis
- private val synthInfo = new SynthesisInfo
-
- val verifier = new RelaxedVerifier(mainSolver, problem, synthInfo)
- import verifier._
-
- def synthesize: Report = {
- info("Synthesis called on files: " + synthesisContext.context.files)
-
- // profile
- synthInfo start Synthesis
-
- info("Initializing synthesizer: ")
- info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
- info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
-// info("leonTimeout: %d".format(leonTimeout))
- initialize
- info("Synthesizer initialized")
-
- // keeps status of validity
- var keepGoing = true
- // update flag in case of time limit overdue
- def checkTimeout =
- if (synthesisContext.context.interruptManager.isInterrupted()) {
- info("Timeout occured, stopping this synthesis rules")
- keepGoing = false
- true
- } else
- false
-
- // initial snippets (will update in the loop)
- var snippets = synthesizeBranchExpressions
- var snippetsIterator = snippets.iterator
-
- // ordering of expressions according to passed examples
- var pq = getNewExampleQueue
-
- // iterate while the program is not valid
- import scala.util.control.Breaks._
- var totalExpressionsTested = 0
- var iteration = 0
- var noBranchFoundIteration = 0
- breakable {
- while (keepGoing) {
- if (checkTimeout) break
- // next iteration
- iteration += 1
- noBranchFoundIteration += 1
- info("####################################")
- info("######Iteration #" + iteration + " ###############")
- info("####################################")
- info("# precondition is: " + tfd.precondition.getOrElse(BooleanLiteral(true)))
- info("# accumulatingCondition is: " + accumulatingCondition)
- info("# accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral()))
- info("####################################")
- interactivePause
-
- var numberOfTested = 0
-
- info("Going into a enumeration/testing phase.")
- fine("evaluating examples: " + gatheredExamples.mkString("\n"))
-
- breakable {
- while (true) {
- if (checkTimeout) break
- val batchSize = numberOfTestsInIteration * (1 << noBranchFoundIteration)
-
- info("numberOfTested: " + numberOfTested)
- // ranking of candidates
- val candidates = {
- val (it1, it2) = snippetsIterator.duplicate
- snippetsIterator = it2.drop(batchSize)
- it1.take(batchSize).
- filterNot(
- out => {
- val snip = out.getSnippet
- fine("enumerated: " + snip)
- (seenBranchExpressions contains snip) ||
- refiner.isAvoidable(snip, problem.as)
- }).toIndexedSeq ++
- // adding previous candidates because they may not be enumerated
- successfulCandidates
- }
-
-// info("Got candidates of size: " + candidates.size +
-// " , first 10 of them are: " + candidates.take(10).map(_.getSnippet.toString).mkString(",\t"))
- info("Got candidates of size: " + candidates.size)
- fine("Got candidates: " + candidates.map(_.getSnippet.toString).mkString(",\n"))
- interactivePause
-
- if (candidates.size > 0) {
- // save current precondition and the old body since it will can be mutated during evaluation
- val oldPreconditionSaved = tfd.precondition
- val oldBodySaved = tfd.body
- // set initial precondition
- tfd.fd.precondition = Some(initialPrecondition)
-
- val ranker = evaluationStrategy.getRanker(candidates, accumulatingExpression, gatheredExamples)
- exampleRunner = evaluationStrategy.getExampleRunner
-
- info("Ranking candidates...")
- synthInfo.start(Action.Evaluation)
- val (maxCandidate, maxCandidateInd) = ranker.getMax
- val (passed, failedModulo) = ranker.fullyEvaluate(maxCandidateInd)
- synthInfo.end
-
- // get all examples that failed evaluation to filter potential conditions
- val evaluation = evaluationStrategy.getEvaluation
- // evaluate all remaining examples
- for (_ <- exampleRunner.examples.size until
- evaluation.getNumberOfEvaluations(maxCandidateInd) by -1)
- evaluation.evaluate(maxCandidateInd)
- val (evalArray, size) = evaluation.getEvaluationVector(maxCandidateInd)
- assert(size == gatheredExamples.size)
- val (passedExamplesPairs, failedExamplesPairs) = (gatheredExamples zip evalArray).partition {
- case (ex, result) =>
- result
- }
- val examplesPartition =
- (passedExamplesPairs.map(_._1), failedExamplesPairs.map(_._1))
-
- fine("Failed examples for the maximum candidate: " + examplesPartition)
-
- // restore original precondition and body
- tfd.fd.precondition = oldPreconditionSaved
- tfd.fd.body = oldBodySaved
-
- // check for timeouts
- if (!keepGoing) break
-
- info("candidate with the most successfull evaluations is: " + maxCandidate.getExpr +
- " with pass count " + passed + " out of " + gatheredExamples.size)
- interactivePause
- numberOfTested += batchSize
-// interactivePause
-
- val currentCandidateExpr = maxCandidate.getExpr
- if (tryToSynthesizeBranch(currentCandidateExpr, examplesPartition)) {
- //noBranchFoundIteration = 0
-
- // after a branch is synthesized it makes sense to consider candidates that previously failed
- seenBranchExpressions = new FilterSet()
- successfulCandidates +:= candidates(maxCandidateInd)
-
-// interactivePause
- break
- } else {
- // add to seen if branch was not found for it
- seenBranchExpressions += currentCandidateExpr
- }
- interactivePause
-
- totalExpressionsTested += numberOfTested
- noBranchFoundIteration += 1
- }
- } // while(true)
- } // breakable
-
- if (!keepGoing) break
-
- // if did not found for any of the branch expressions
- if (found) {
- synthInfo end Synthesis
- synthInfo.iterations = iteration
- synthInfo.numberOfEnumeratedExpressions = numberOfTested
- info("We are done, in time: " + synthInfo.last)
- return new FullReport(tfd, synthInfo)
- }
-
- if (variableRefinedBranch) {
- info("Variable refined, doing branch synthesis again")
- // get new snippets
- snippets = synthesizeBranchExpressions
- snippetsIterator = snippets.iterator
- pq = getNewExampleQueue
-
- // reset flag
- variableRefinedBranch = false
- } else
- // reseting iterator needed because we may have some expressions that previously did not work
- snippetsIterator = snippets.iterator
-
- info("Filtering based on precondition: " + And(initialPrecondition, accumulatingCondition))
- fine("counterexamples before filter: " + gatheredExamples.size)
- exampleRunner.filter(And(initialPrecondition, accumulatingCondition))
- gatheredExamples = exampleRunner.examples
- fine("counterexamples after filter: " + gatheredExamples.size)
- fine("counterexamples after filter: " + gatheredExamples.mkString("\n"))
- }
- } //breakable { while (!keepGoing) {
-
- EmptyReport
- }
-
- def generateCounterexamples(program: Program, funDef: FunDef, number: Int): (Seq[Map[Identifier, Expr]], Expr) = {
- info("Generate counter examples with precondition " + funDef.precondition.getOrElse(BooleanLiteral(true)))
-
- // save current precondition
- var precondition = funDef.precondition.getOrElse(BooleanLiteral(true))
- val preconditionToRestore = funDef.precondition
- // accumulate counterexamples as sequence of maps
- var maps: Seq[Map[Identifier, Expr]] = Seq.empty
-
- // iterate specific number of times or until no further counterexample can be generated
- var changed = true
- var ind = 0
- while (ind < number && changed) {
- // analyze the program
- val (solved, map) = analyzeFunction(tfd)
-
- // check if solver could solved this instance
- if (solved == false && !map.isEmpty) {
- info("Found counterexample: " + map)
- // add current counterexample
- maps :+= map
-
- // prevent this counterexample to re-occur
- val precAddition = Not(
- And(map map { case (id, value) => Equals(LeonVariable(id), value) } toSeq)
- )
- precondition = And(Seq(precondition, precAddition))
- // update precondition
- funDef.precondition = Some(precondition)
- } else
- changed = false
-
- // add new constraint
- ind += 1
- }
-
- funDef.precondition = preconditionToRestore
- // return found counterexamples and the formed precondition
- (maps, precondition)
- }
-
- def getCurrentBuilder = new InitialEnvironmentBuilder(allDeclarations)
-
- def synthesizeBranchExpressions = {
- info("Invoking synthesis for branch expressions")
- synthInfo.profile(Generation) { inSynth.getExpressions(getCurrentBuilder).distinct }
- }
-
- def synthesizeBooleanExpressions = {
- info("Invoking synthesis for condition expressions")
- synthInfo.start(Generation)
- if (variableRefinedCondition) {
- // store for later fetch (will memoize values)
- fine("Going into boolean synthesis")
- val stream = inSynthBoolean.getExpressions(getCurrentBuilder)
- fine("Out of boolean synthesis")
- println("stream is here!")
- booleanExpressionsSaved =
- stream.distinct.take(numberOfBooleanSnippets).
- filterNot(expr => refiner.isAvoidable(expr.getSnippet, problem.as))
- // reset flag
- variableRefinedCondition = false
- }
-
- synthInfo end booleanExpressionsSaved
- }
-
- def interactivePause = {
-// System.out.println("Press Any Key To Continue...");
-// new java.util.Scanner(System.in).nextLine();
- }
-
- def getNewExampleQueue = PriorityQueue[(Expr, Int)]()(
- new Ordering[(Expr, Int)] {
- def compare(pair1: (Expr, Int), pair2: (Expr, Int)) =
- pair1._2.compare(pair2._2)
- })
-
- def initialize = {
- // create new insynth object
- loader = new LeonLoader(program, problem.as, false)
- inSynth = new InSynth(loader, desiredType, true)
- // save all declarations seen
- allDeclarations = inSynth.declarations
- // make conditions synthesizer
- inSynthBoolean = new InSynth(allDeclarations, BooleanType, true)
-
- // funDef of the hole
- fine("postcondition is: " + tfd.postcondition.get)
- fine("declarations we see: " + allDeclarations.map(_.toString).mkString("\n"))
- // interactivePause
-
- // accumulate precondition for the remaining branch to synthesize
- accumulatingCondition = BooleanLiteral(true)
- // save initial precondition
- initialPrecondition = tfd.precondition.getOrElse(BooleanLiteral(true))
- val holeFunDefBody = tfd.body.get
- // accumulate the final expression of the hole
- accumulatingExpression = (finalExp: Expr) => {
- def replaceChoose(expr: Expr) = expr match {
- case _: Choose => Some(finalExp)
- case _ => None
- }
-
- //import TreeOps._
- //matchToIfThenElse(searchAndReplace(replaceChoose)(holeFunDefBody))
- TreeOps.postMap(replaceChoose)(TreeOps.matchToIfThenElse(holeFunDefBody))
- }
- //accumulatingExpressionMatch = accumulatingExpression
-
- // each variable of super type can actually have a subtype
- // get sine declaration maps to be able to refine them
- variableRefiner = new VariableRefinerCompose add
- // refiner on structure
- new VariableRefinerStructure(loader.directSubclassesMap,
- loader.variableDeclarations, loader.classMap, reporter) add
- // refiner that uses execution
- new VariableRefinerExecution(loader.variableDeclarations, loader.classMap)
-// new VariableSolverRefiner(loader.directSubclassesMap,
-// loader.variableDeclarations, loader.classMap, mainSolver, reporter)
-
- // calculate cases that should not happen
- refiner = new Filter(program, tfd, variableRefiner)
-
- gatheredExamples = ArrayBuffer(introduceExamples().map(Example(_)): _*)
- fine("Introduced examples: " + gatheredExamples.mkString("\t"))
- }
-
- def tryToSynthesizeBranch(snippetTree: Expr, examplesPartition: (Seq[Example], Seq[Example])): Boolean = {
- val (succeededExamples, failedExamples) = examplesPartition
- // replace hole in the body with the whole if-then-else structure, with current snippet tree
- val oldBody = tfd.body.get
- val newBody = accumulatingExpression(snippetTree)
- tfd.fd.body = Some(newBody)
-
- // precondition
- val oldPrecondition = tfd.precondition.getOrElse(BooleanLiteral(true))
- tfd.fd.precondition = Some(initialPrecondition)
-
- snippetTree.setType(desiredType)
- //holeFunDef.getBody.setType(hole.desiredType)
- info("Current candidate solution is:\n" + tfd)
-
- if (failedExamples.isEmpty) {
- // check if solver could solved this instance
- fine("Analyzing program for funDef:" + tfd)
- val (result, map) = analyzeFunction(tfd)
- info("Solver returned: " + result + " with CE " + map)
-
- if (result) {
- // mark the branch found
- found = true
-
- info("Wooooooow we have a winner!")
- info("************************************")
- info("*********And the winner is**********")
- info(accumulatingExpression(snippetTree).toString)
- info("************************************")
-
- return true
- } else {
- gatheredExamples += Example(map)
- }
- }
-
- // store appropriate values here, will be update in a finally branch
- var bodyToRestore = oldBody
- var preconditionToRestore = Some(oldPrecondition)
-
- // because first initial test
- tfd.fd.precondition = preconditionToRestore
-
- // get counterexamples
-// info("Going to generating counterexamples: " + holeFunDef)
-// val (maps, precondition) = generateCounterexamples(program, holeFunDef, numberOfCounterExamplesToGenerate)
-//
-// // collect (add) counterexamples from leon
-// if (collectCounterExamplesFromLeon)
-// gatheredExamples ++= maps.map(Example(_))
- val maps = Seq[Map[Identifier, Expr]]()
-
- // will modify funDef body and precondition, restore it later
- try {
- {
- // reconstruct (only defined number of boolean expressions)
- val innerSnippets = synthesizeBooleanExpressions
- // just printing of expressions
- fine(
- (innerSnippets.zipWithIndex map {
- case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet
- }).mkString("\n"))
- interactivePause
-
- // enumerate synthesized boolean expressions and filter out avoidable ones
- for (
- innerSnippetTree <- innerSnippets map { _.getSnippet };
- if (
- {
- val flag = !refiner.isAvoidable(innerSnippetTree, problem.as)
- if (!flag) fine("Refiner filtered this snippet: " + innerSnippetTree)
- flag
- })
- ) {
- fine("boolean snippet is: " + innerSnippetTree)
- info("Trying: " + innerSnippetTree + " as a condition.")
- val innerPrecFound = tryToSynthesizeBooleanCondition(
- snippetTree, innerSnippetTree,
- // counter examples represent those for which candidate fails
- (failedExamples.map(_.map) ++ maps), succeededExamples.map(_.map)
- )
-
- info("tryToSynthesizeBooleanCondition returned " + innerPrecFound + " for " + snippetTree)
- if ( innerPrecFound ) {
- // update accumulating expression
- val oldAccumulatingExpression = accumulatingExpression
- val newAccumulatingExpression =
- (finalExpr: Expr) =>
- oldAccumulatingExpression({
- val innerIf = IfExpr(innerSnippetTree, snippetTree, finalExpr)
- innerIf.setType(snippetTree.getType)
- innerIf
- })
-
- accumulatingExpression = newAccumulatingExpression
-
- // update accumulating precondition
- fine("updating accumulatingPrecondition")
- accumulatingCondition = And(Seq(accumulatingCondition, Not(innerSnippetTree)))
- fine("updating hole fun precondition and body (to be hole)")
- // new precondition (restore in finally)
- preconditionToRestore = Some(accumulatingCondition)
-
- val currentBranchCondition = And(Seq(accumulatingCondition, innerSnippetTree))
- val variableRefinementResult = variableRefiner.refine(innerSnippetTree,
- currentBranchCondition, allDeclarations, exampleRunner.getEvaluator)
-
- if (variableRefinementResult._1) {
- info("Variable is refined.")
- allDeclarations = variableRefinementResult._2
-
- // the reason for two flags is for easier management of re-syntheses only if needed
- variableRefinedBranch = true
- variableRefinedCondition = true
- }
-
- return true
- }
-
- } // iterating over all boolean solutions
-
- info("No precondition found for branch expression: " + snippetTree)
- return false
-
- } // if ( !maps.isEmpty ) {
- // no counter examples, we just say that we cannot do anything
- false
- } // try
- finally {
- // set these to the FunDef
- tfd.fd.precondition = preconditionToRestore
- // restore old body (we accumulate expression)
- tfd.fd.body = Some(oldBody)
- }
- }
-
- /**
- * tries to abduce a new branch
- * @param snippetTree expression candidate
- * @param innerSnippetTree condition candidate
- * @param counterExamples failed examples
- * @param succExamples successful examples
- * @return whether branch condition is found
- */
- def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr,
- counterExamples: Seq[Map[Identifier, Expr]], succExamples: Seq[Map[Identifier, Expr]]):
- Boolean = {
- // new condition together with existing precondition
- val newPrecondition = And(Seq(initialPrecondition, accumulatingCondition, innerSnippetTree))
- val newPathCondition = And(Seq(problem.pc, accumulatingCondition, innerSnippetTree))
-
- // new expression should not be false
-// val notFalseEquivalence = Not(newCondition)
- val isSatisfiable =
- checkSatisfiabilityNoMod(newPathCondition)
- fine("Is " + newPathCondition + " satisfiable: " + isSatisfiable)
-
- // continue if our expression is not contradictory
- if (isSatisfiable) {
- // check if synthesized boolean expression implies precondition (counterexamples)
- var hadRuntimeError = false
- val implyCounterExamplesPre = (false /: counterExamples) {
- case (false, exMapping) =>
- exampleRunner.evaluateToResult(newPrecondition, exMapping) match {
- case EvaluationResults.Successful(BooleanLiteral(false)) => false
- case r =>
-// throw new RuntimeException("should not go here")
-
- // TODO take care of this mess
- val newFunId = FreshIdentifier("tempIntroducedFunction22")
- val newFun = new FunDef(newFunId, tfd.fd.tparams, tfd.fd.returnType, tfd.fd.params)
-// newFun.precondition = Some(newCondition)
- newFun.precondition = Some(initialPrecondition)
- newFun.postcondition = tfd.fd.postcondition
-
- def replaceFunDef(expr: Expr) = expr match {
- case FunctionInvocation(`tfd`, args) =>
- Some(FunctionInvocation(newFun.typed(tfd.tps), args))
- case _ => None
- }
-
- val error = Error("Condition flow hit unknown path.")
- error.setType(snippetTree.getType)
- val ifInInnermostElse =
- IfExpr(innerSnippetTree, snippetTree, error)
-
- import TreeOps._
-// println("ifInInnermostElse " + ifInInnermostElse)
-// println("acc expr before replace: " + accumulatingExpression(ifInInnermostElse))
- val newBody = postMap(replaceFunDef)(accumulatingExpression(ifInInnermostElse))
-
- newFun.body = Some(newBody)
-
- assert(newBody.getType != Untyped)
- val resFresh2 = FreshIdentifier("result22", true).setType(newBody.getType)
-
- val (id, post) = newFun.postcondition.get
-
- val newCandidate =
- Let(resFresh2, newBody,
-// matchToIfThenElse(replace(Map(LeonVariable(id) -> LeonVariable(resFresh2)),
-// post)))
- replace(Map(LeonVariable(id) -> LeonVariable(resFresh2)),
- matchToIfThenElse(post)))
- finest("New fun for Error evaluation: " + newFun)
-// println("new candidate: " + newBody)
-
- val newProgram = program.copy(modules = ModuleDef(FreshIdentifier("result"), List(newFun)) :: program.modules)
-// println("new program: " + newProgram)
-
- val _evaluator = new CodeGenEvaluator(synthesisContext.context, newProgram
- , _root_.leon.codegen.CodeGenParams(maxFunctionInvocations = 500, checkContracts = true))
-
- val res = _evaluator.eval(newCandidate, exMapping)
-// if (newCandidate.toString contains "tree.value < value")
-// interactivePause
-
-// interactivePause
- res match {
- case EvaluationResults.RuntimeError("Condition flow hit unknown path.") =>
- hadRuntimeError = true
- false
- case EvaluationResults.Successful(BooleanLiteral(innerRes)) => !innerRes
- case _ =>
- // TODO think about this
- // I put condition into precondition so some examples will be violated?
- println("new evalution got: " + res + " for " + newCandidate + " and " + exMapping + " newFun is " + newFun)
- true
- }
-
-// fine("Evaluation result for " + newCondition + " on " + exMapping + " is " + r)
-// true
- }
- case _ => true
- }
-
- fine("implyCounterExamplesPre: " + implyCounterExamplesPre)
-
- val implyCounterExamples = if (!implyCounterExamplesPre && hadRuntimeError) {
- ! succExamples.exists( exMapping => {
-// throw new RuntimeException("should not go here")
- // TODO take care of this mess
- val newFunId = FreshIdentifier("tempIntroducedFunction22")
- val newFun = new FunDef(newFunId, tfd.fd.tparams, tfd.fd.returnType, tfd.fd.params)
-// newFun.precondition = Some(newCondition)
- newFun.precondition = Some(initialPrecondition)
- newFun.postcondition = tfd.fd.postcondition
-
- def replaceFunDef(expr: Expr) = expr match {
- case FunctionInvocation(`tfd`, args) =>
- Some(FunctionInvocation(newFun.typed(tfd.tps), args))
- case _ => None
- }
-
- val error = Error("Condition flow hit unknown path.")
- error.setType(snippetTree.getType)
- val ifInInnermostElse =
- IfExpr(innerSnippetTree, snippetTree, error)
-
- import TreeOps._
- val newBody = postMap(replaceFunDef)(accumulatingExpression(ifInInnermostElse))
-
- newFun.body = Some(newBody)
-
- assert(newBody.getType != Untyped)
- val resFresh2 = FreshIdentifier("result22", true).setType(newBody.getType)
-
- val (id, post) = newFun.postcondition.get
-
- val newCandidate =
- Let(resFresh2, newBody,
-// matchToIfThenElse(replace(Map(LeonVariable(id) -> LeonVariable(resFresh2)),
-// post)))
- replace(Map(LeonVariable(id) -> LeonVariable(resFresh2)),
- matchToIfThenElse(post)))
- finest("New fun for Error evaluation: " + newFun)
-// println("new candidate: " + newBody)
-
- val newProgram = program.copy(modules = ModuleDef(FreshIdentifier("result"), List(newFun)) :: program.modules)
-// println("new program: " + newProgram)
-
- val _evaluator = new CodeGenEvaluator(synthesisContext.context, newProgram,
- _root_.leon.codegen.CodeGenParams(maxFunctionInvocations = 500, checkContracts = true))
-
- val res = _evaluator.eval(newCandidate, exMapping)
- println("for mapping: " + exMapping + "res is: " + res)
-// if (newCandidate.toString contains "tree.value < value")
-// interactivePause
-
- interactivePause
- res match {
- case EvaluationResults.RuntimeError("Condition flow hit unknown path.") =>
- false
- case EvaluationResults.Successful(BooleanLiteral(innerRes)) => innerRes
- case _ =>
- println("new evalution got: " + res + " for " + newCandidate + " and " + exMapping)
- false
- }
- })
- } else
- implyCounterExamplesPre
-
-
- fine("implyCounterExamples: " + implyCounterExamples)
-// interactivePause
-
- if (!implyCounterExamples) {
- // if expression implies counterexamples add it to the precondition and try to validate program
- tfd.fd.precondition = Some(newPathCondition)
-
- // do analysis
- val (valid, map) = analyzeFunction(tfd)
- // program is valid, we have a branch
- if (valid) {
- // we found a branch
- info("We found a branch, for expression %s, with condition %s.".format(snippetTree, innerSnippetTree))
-
- // found a boolean snippet, break
- true
- } else {
- // collect (add) counterexamples from leon
- if (collectCounterExamplesFromLeon && !map.isEmpty)
- gatheredExamples ++= (map :: Nil).map(Example(_))
-
- // reset funDef and continue with next boolean snippet
- false
- }
- } else {
- fine("Solver filtered out the precondition (does not imply counterexamples)")
- false
- }
- } else {// if (!isItAContradiction)
- fine("Solver filtered out the precondition (is not sound)")
- false
- }
- }
-
-}
-
diff --git a/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
deleted file mode 100644
index 31fb734dc..000000000
--- a/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
+++ /dev/null
@@ -1,138 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package evaluation
-
-import scala.collection.mutable.ArrayBuffer
-
-import leon._
-import leon.evaluators._
-import leon.evaluators.EvaluationResults._
-import leon.purescala.Trees._
-import leon.purescala.Definitions.{ TypedFunDef, FunDef, ValDef, Program, ModuleDef }
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.TreeOps
-import leon.codegen.CodeGenParams
-
-import examples._
-import ranking._
-
-import _root_.insynth.util.logging.HasLogger
-
-case class CodeGenExampleRunner(program: Program, tfd: TypedFunDef, ctx: LeonContext,
- candidates: Seq[Candidate], inputExamples: Seq[Example],
- params: CodeGenParams = CodeGenParams(maxFunctionInvocations = 200, checkContracts = true)) extends ExampleRunner(inputExamples) with HasLogger {
-
- private var _examples = ArrayBuffer(transformExamples(inputExamples): _*)
-
- val evaluationContext = ctx
-
- fine("building codegen evaluator with params " + params + " and program: " + program)
- lazy val _evaluator = new CodeGenEvaluator(evaluationContext, program, params)
- override def getEvaluator = _evaluator
-
- def transformExamples(examples: Seq[Example]) =
- examples.map(
- ex => {
- val map = ex.map
- for(id <- tfd.params.map(_.id)) yield
- map(id)
- }
- )
-
- def compile(expr: Expr, ids: Seq[Identifier]) = {
- finest("Compiling expr: " + expr + " for ids: " + ids)
- // this get is dubious
- StopwatchCollections.get("Compilation").newStopwatch profile getEvaluator.compile(expr, ids).get
- }
-
- val candidateClosures = candidates.map(cand => compile(cand.prepareExpression, tfd.params.map(_.id)))
-
- override def evaluate(candidateInd: Int, exampleInd: Int) = {
- val closure = candidateClosures(candidateInd)
-
- finer("Index evaluate candidate [%d]%s, for [%d]%s.".format(
- candidateInd, candidates(candidateInd).prepareExpression, exampleInd, examples(exampleInd)
- ))
-
- evaluate(closure, _examples(exampleInd))
- }
-
- override def addExamples(newExamples: Seq[Example]) = {
- super.addExamples(newExamples)
- _examples ++= transformExamples(examples)
- }
-
- def evaluate(expr: Expr, args: Seq[Expr]) {
- fine("to evaluate: " + expr + " for: " + args)
-
- val closure = compile(expr, tfd.params.map(_.id))
- evaluate(closure, args)
- }
-
- override def evaluate(expr: Expr, mapping: Map[Identifier, Expr]) = {
- fine("to evaluate: " + expr + " for mapping: " + mapping)
-
- val closure = compile(expr, tfd.params.map(_.id))
-
- evaluate(closure, tfd.params.map(arg => mapping(arg.id)))
- }
-
- override def evaluateToResult(expr: Expr, mapping: Map[Identifier, Expr]): Result = {
- fine("to evaluate: " + expr + " for mapping: " + mapping)
-
- val closure = compile(expr, tfd.params.map(_.id))
-
- closure(tfd.params.map(arg => mapping(arg.id)))
- }
-
- def evaluate(evalClosure: Seq[Expr] => Result, args: Seq[Expr]) = {
- try {
- evalClosure(args) match {
- case Successful(BooleanLiteral(true)) =>
- fine("EvaluationSuccessful(true) for " + args)
- true
- case m =>
- fine("Eval failed: " + m)
- false
- }
- } catch {
- case e: StackOverflowError =>
- fine("Eval failed: " + e)
- false
- }
- }
-
- /** filter counterexamples according to an expression (precondition) */
- override def filter(prec: Expr) = {
- entering("filter(" + prec + ")")
- fine("Old counterExamples.size: " + examples.size)
-
- val closure = compile(prec, tfd.params.map(_.id))
-
- val (newTransformed, newExamples) = ((_examples zip examples) filter {
- case ((transformedExample, _)) =>
- evaluate(closure, transformedExample)
- }).unzip
-
- _examples = newTransformed
- examples = newExamples
-
- fine("New counterExamples.size: " + examples.size)
- }
-
- /** count how many examples pass */
- override def countPassed(expressionToCheck: Expr) = {
- fine("expressionToCheck: " + expressionToCheck)
-
- val closure = compile(expressionToCheck, tfd.params.map(_.id))
-
- val (passed, failed) = (_examples zip examples).partition(
- pair => evaluate(closure, pair._1)
- )
-
- fine("(passed.size, failed.size): " + (passed.size, failed.size))
- (passed.size, passed map (_._2))
- }
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
deleted file mode 100644
index 8c0838da0..000000000
--- a/src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
+++ /dev/null
@@ -1,90 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package evaluation
-
-import scala.collection.mutable.ArrayBuffer
-
-import leon._
-import leon.evaluators._
-import leon.evaluators.EvaluationResults._
-import leon.purescala.Trees._
-import leon.purescala.Definitions.{ TypedFunDef, ValDef, Program, ModuleDef }
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.TreeOps
-
-import examples._
-import ranking._
-
-import _root_.insynth.util.logging.HasLogger
-
-case class DefaultExampleRunner(program: Program, tfd: TypedFunDef, ctx: LeonContext,
- candidates: Seq[Candidate], inputExamples: Seq[Example],
- maxSteps: Int = 2000) extends ExampleRunner(inputExamples) with HasLogger {
-
- private var _examples = ArrayBuffer(inputExamples.map(_.map): _*)
-
- override def addExamples(newExamples: Seq[Example]) = {
- super.addExamples(newExamples)
- _examples ++= newExamples.map(_.map)
- }
-
- val evaluationContext = ctx
-
- lazy val _evaluator = new DefaultEvaluator(evaluationContext, program)
- override def getEvaluator = _evaluator
-
- override def evaluate(expr: Expr, mapping: Map[Identifier, Expr]): Boolean = {
- finest("to evaluate: " + expr + " for mapping: " + mapping)
- getEvaluator.eval(expr, mapping) match {
- case Successful(BooleanLiteral(true)) =>
- finest("Eval succeded: EvaluationSuccessful(true)")
- true
- case m =>
- finest("Eval failed: " + m)
- false
- }
- }
-
- def evaluate(expr: Expr, args: Seq[Expr]): Boolean = {
- evaluate(expr, tfd.params.map(_.id).zip(args).toMap)
- }
-
- override def evaluateToResult(expr: Expr, mapping: Map[Identifier, Expr]) = {
- finest("to evaluate: " + expr + " for mapping: " + mapping)
- getEvaluator.eval(expr, mapping)
- }
-
-
- /** if the example runner knows about candidates and input examples, run by their indexes */
- def evaluate(candidateInd: Int, exampleInd: Int) =
- evaluate(candidates(candidateInd).prepareExpression, _examples(exampleInd))
-
- /** filter counterexamples according to an expression (precondition) */
- def filter(prec: Expr) = {
- entering("filter(" + prec + ")")
- finest("Old counterExamples.size: " + examples.size)
-
- val (newTransformed, newExamples) = ((_examples zip examples) filter {
- case ((exMap, _)) =>
- evaluate(prec, exMap)
- }).unzip
-
- _examples = newTransformed
- examples = newExamples
-
- finest("New counterExamples.size: " + examples.size)
- }
-
- /** count how many examples pass */
- def countPassed(expressionToCheck: Expr) = {
- finest("count passed for expression to check: " + expressionToCheck)
-
- val (passed, failed) = examples.partition(
- ex => evaluate(expressionToCheck, ex.map)
- )
-
- (passed.size, passed)
- }
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala b/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
deleted file mode 100644
index f799f8f56..000000000
--- a/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
+++ /dev/null
@@ -1,113 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package evaluation
-
-import leon._
-import leon.evaluators._
-import leon.evaluators.EvaluationResults._
-import leon.purescala.Trees._
-import leon.purescala.Definitions.{ TypedFunDef, ValDef, Program, ModuleDef }
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.TreeOps
-import leon.codegen.CodeGenParams
-
-import insynth.reconstruction.Output
-import _root_.insynth.util.logging._
-
-import ranking._
-import examples._
-
-trait EvaluationStrategy extends HasLogger {
- def getRanker(candidatePairs: IndexedSeq[(Output)], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]): Ranker
-
- def getExampleRunner: ExampleRunner
-
- def getEvaluation: Evaluation
-
- protected def logCounts(candidates: IndexedSeq[Candidate], inputExamples: Seq[Example]) {
- // printing candidates and pass counts
- fine("Ranking with examples: " + inputExamples.mkString(", "))
- fine( {
- val logString = ((candidates.zipWithIndex) map {
- case (cand: Candidate, ind: Int) => {
- val result = getExampleRunner.countPassed(cand.prepareExpression)
- ind + ": snippet is " + cand.getExpr +
- " pass count is " + result._1 +"/" + inputExamples.size + " (" + result._2.mkString(", ") + ")"
- }
- }).mkString("\n")
- logString
- })
- }
-
-}
-
-case class DefaultEvaluationStrategy(program: Program, tfd: TypedFunDef, ctx: LeonContext,
- maxSteps: Int = 2000) extends EvaluationStrategy with HasLogger {
-
- var exampleRunner: ExampleRunner = _
-
- var evaluation: Evaluation = _
-
- override def getRanker(candidatePairs: IndexedSeq[Output], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]) = {
-
- val candidates = Candidate.makeDefaultCandidates(candidatePairs, bodyBuilder, tfd)
-
- exampleRunner = DefaultExampleRunner(program, tfd, ctx, candidates, inputExamples)
-
- logCounts(candidates, inputExamples)
-
- // printing candidates and pass counts
- fine("Ranking with examples: " + inputExamples.mkString(", "))
- fine( {
- val logString = ((candidates.zipWithIndex) map {
- case (cand: Candidate, ind: Int) => {
- val result = exampleRunner.countPassed(cand.prepareExpression)
- ind + ": snippet is " + cand.expr +
- " pass count is " + result._1 + " (" + result._2.mkString(", ") + ")"
- }
- }).mkString("\n")
- logString
- })
-
- evaluation = Evaluation(exampleRunner)
-
- new Ranker(candidates, evaluation)
- }
-
- override def getExampleRunner = exampleRunner
-
- override def getEvaluation = evaluation
-}
-
-case class CodeGenEvaluationStrategy(program: Program, tfd: TypedFunDef, ctx: LeonContext,
- maxSteps: Int = 200) extends EvaluationStrategy with HasLogger {
-
- var exampleRunner: ExampleRunner = _
-
- var evaluation: Evaluation = _
-
- override def getRanker(candidatePairs: IndexedSeq[Output], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]) = {
-
- val candidates = Candidate.makeCodeGenCandidates(candidatePairs, bodyBuilder, tfd)
-
- val newProgram = program.copy(modules = ModuleDef(FreshIdentifier("result"), candidates.map(_.newFunDef)) :: program.modules)
-
- finest("New program looks like: " + newProgram)
- finest("Candidates look like: " + candidates.map(_.prepareExpression).mkString("\n"))
-
- val params = CodeGenParams(maxFunctionInvocations = maxSteps, checkContracts = true)
-
- exampleRunner = CodeGenExampleRunner(newProgram, tfd, ctx, candidates, inputExamples, params)
-
- logCounts(candidates, inputExamples)
-
- evaluation = Evaluation(exampleRunner)
-
- new Ranker(candidates, evaluation)
- }
-
- override def getExampleRunner = exampleRunner
-
- override def getEvaluation = evaluation
-}
diff --git a/src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
deleted file mode 100644
index d67e3d995..000000000
--- a/src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
+++ /dev/null
@@ -1,43 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package evaluation
-
-import scala.collection.mutable.ArrayBuffer
-
-import leon.purescala.Trees._
-import leon.purescala.Common.Identifier
-import leon.evaluators._
-import leon.evaluators.EvaluationResults.Result
-
-import _root_.insynth.util.logging.HasLogger
-
-import examples.Example
-
-abstract class ExampleRunner(inputExamples: Seq[Example]) extends HasLogger {
-
- private var _examples = ArrayBuffer(inputExamples: _*)
- protected def examples_=(newExamples: ArrayBuffer[Example]) = _examples = newExamples
- def examples = _examples
-
- def addExamples(newExamples: Seq[Example]): Unit = {
- _examples ++= newExamples
- }
-
- def getEvaluator: Evaluator
-
- /** evaluate given expression */
- def evaluate(expr: Expr, mapping: Map[Identifier, Expr]): Boolean
-
- def evaluateToResult(expr: Expr, mapping: Map[Identifier, Expr]): Result
-
- /** if the example runner knows about candidates and input examples, run by their indexes */
- def evaluate(candidateInd: Int, exampleInd: Int): Boolean
-
- /** filter counterexamples according to an expression (precondition) */
- def filter(prec: Expr): Unit
-
- /** count how many examples pass */
- def countPassed(expressionToCheck: Expr): (Int, Seq[Example])
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/examples/Example.scala b/src/main/scala/leon/synthesis/condabd/examples/Example.scala
deleted file mode 100644
index 86be74f69..000000000
--- a/src/main/scala/leon/synthesis/condabd/examples/Example.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package examples
-
-import leon.purescala.Trees._
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-
-case class Example(map: Map[Identifier, Expr]) {
-
- override def toString = {
- map.toString
- }
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala b/src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
deleted file mode 100644
index dbda0fe80..000000000
--- a/src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
+++ /dev/null
@@ -1,186 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package examples
-
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps
-import leon.purescala.Common.Identifier
-import leon.purescala.Definitions.Program
-import leon.evaluators.Evaluator
-import leon.synthesis.Problem
-import leon.LeonContext
-
-import insynth.leon.loader.LeonLoader
-import leon.datagen._
-
-object InputExamples {
-
- val rnd = new scala.util.Random(System.currentTimeMillis)
- val MAX_INT = 1000
-
- def getDataGenInputExamples(ctx: LeonContext, program: Program, evaluator: Evaluator, p: Problem,
- numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]]) = {
-
- val ins = _forcedFreeVars.getOrElse(TreeOps.variablesOf(p.pc).toSeq)
-
- val models = new NaiveDataGen(ctx, program, evaluator).generateFor(ins, p.pc, numOfModels, numOfTries)
-
- models.toList.map(m => (ins zip m).toMap)
- }
-
- def getDataGenInputExamplesRandomIntegers(ctx: LeonContext, program: Program, evaluator: Evaluator, p: Problem,
- numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]],
- bound: Int = MAX_INT) = {
- import TreeOps._
-
- val ins = _forcedFreeVars.getOrElse(TreeOps.variablesOf(p.pc).toSeq)
-
- val models = new NaiveDataGen(ctx, program, evaluator).generateFor(ins, p.pc, numOfModels, numOfTries)
-
- def foundInteger(x: Expr) = x match {
- case _:IntLiteral => Some(IntLiteral(rnd.nextInt(bound)))
- case _ => None
- }
-
- models.toList.map(m => (ins zip m).toMap).map( innerMap =>
- innerMap.map( innerEl => innerEl match {
- case (id, expr) => (id, postMap(foundInteger)(expr))
- })
- )
- }
-
- def getFixedInputExamples(argumentIds: Seq[Identifier], loader: LeonLoader, goalType: TypeTree) = {
- argumentIds match {
- case singleArgument :: Nil if isList(singleArgument) =>
- introduceOneListArgumentExamples(argumentIds, loader)
- case first :: second :: Nil if isList(first) && isList(second) =>
- introduceTwoListArgumentsExamples(argumentIds, loader, goalType)
- case first :: second :: Nil if isInt(first) && isList(second) =>
- introduceExamplesIntList(argumentIds, loader)
- case _ => null
- }
- }
-
- def introduceExamplesIntList(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = {
-
- // list type
- val ct = argumentIds(1).getType.asInstanceOf[ClassType]
-
- val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType])
-
- val (nilClassSet, consClassSet) = setSubclasses.partition(_.fields.size == 0)
-
- val nilClass = nilClassSet.head
- val consClass = consClassSet.head
-
- var counter = 10
- def getIntLiteral = { counter += 1; IntLiteral(counter) }
- val intLiteral = IntLiteral(5)
-
- val list0 = CaseClass(nilClass, Nil)
- val list1 = CaseClass(consClass, IntLiteral(10) :: list0 :: Nil)
- val list32 = CaseClass(consClass, IntLiteral(5) :: CaseClass(consClass, IntLiteral(7) :: list1 :: Nil) :: Nil)
-
- Map(argumentIds(0) -> IntLiteral(3), argumentIds(1) -> list32) ::
- Map(argumentIds(0) -> IntLiteral(2), argumentIds(1) -> list32) ::
- Map(argumentIds(0) -> IntLiteral(3), argumentIds(1) -> list0) ::
- Map(argumentIds(0) -> IntLiteral(2), argumentIds(1) -> list0) ::
- Map(argumentIds(0) -> IntLiteral(6), argumentIds(1) -> list32) ::
- Map(argumentIds(0) -> IntLiteral(9), argumentIds(1) -> list32) ::
- Nil
- }
-
- def introduceOneListArgumentExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = {
-
- // list type
- val ct = argumentIds(0).getType.asInstanceOf[ClassType]
-
- val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType])
-
- val (nilClassSet, consClassSet) = setSubclasses.partition(_.fields.size == 0)
-
- val nilClass = nilClassSet.head
- val consClass = consClassSet.head
-
- var counter = 10
- def getIntLiteral = { counter += 1; IntLiteral(counter) }
- val intLiteral = IntLiteral(5)
-
- val list0 = CaseClass(nilClass, Nil)
- val list1 = CaseClass(consClass, IntLiteral(10) :: list0 :: Nil)
- val list2s = CaseClass(consClass, IntLiteral(5) :: list1 :: Nil)
- val list2u = CaseClass(consClass, IntLiteral(5) :: list1 :: Nil)
- val list3s = CaseClass(consClass, IntLiteral(5) :: list2s :: Nil)
- val list3u1 = CaseClass(consClass, IntLiteral(5) :: list2u :: Nil)
- val list3u2 = CaseClass(consClass, IntLiteral(15) :: list2s :: Nil)
- val list3u3 = CaseClass(consClass, IntLiteral(15) :: list2u :: Nil)
-
- for (list <- List(list0, list1, list2s, list2u, list3s, list3u1, list3u2, list3u3))
- yield Map(argumentIds(0) -> list)
- }
-
- def introduceTwoListArgumentsExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader,
- goalType: TypeTree) = {
-
- goalType match {
- case ct: ClassType =>
- val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType])
-
- val (nilClassSet, consClassSet) = setSubclasses.partition(_.fields.size == 0)
-
- val nilClass = nilClassSet.head
- val consClass = consClassSet.head
-
- var counter = 0
- def getIntLiteral = { counter += 1; IntLiteral(counter) }
-
- val list0 = () => CaseClass(nilClass, Nil)
- val list1 = () => CaseClass(consClass, getIntLiteral :: list0() :: Nil)
- val list2 = () => CaseClass(consClass, getIntLiteral :: list1() :: Nil)
- val list3 = () => CaseClass(consClass, getIntLiteral :: list2() :: Nil)
- val list4 = () => CaseClass(consClass, getIntLiteral :: list3() :: Nil)
-
- val lists = List(list0, list1, list2, list3 /*, list4*/ )
-
- for (l1 <- lists; l2 <- lists)
- yield Map(argumentIds(0) -> l1(), argumentIds(1) -> l2())
-
- case _ =>
- null
- }
- }
-
- def isList(id: Identifier) = id.getType.toString == "List"
- def isInt(id: Identifier) = id.getType == Int32Type
-
- // def introduceOneListArgumentExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = {
- //
- // // list type
- // val ct = argumentIds(0).getType.asInstanceOf[ClassType]
- //
- // val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
- //
- // val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
- //
- // val nilClass = nilClassSet.head
- // val consClass = consClassSet.head
- //
- // var counter = 10
- // def getIntLiteral = { counter+=1; IntLiteral(counter) }
- // val intLiteral = IntLiteral(5)
- //
- // val list0 = CaseClass(nilClass, Nil)
- // val list1 = CaseClass(consClass, IntLiteral(5) :: list0 :: Nil)
- // val list2 = CaseClass(consClass, IntLiteral(3) :: list1 :: Nil)
- // val list3 = CaseClass(consClass, IntLiteral(1) :: list2 :: Nil)
- // val list32 = CaseClass(consClass, IntLiteral(10) :: CaseClass(consClass, IntLiteral(7) :: list1 :: Nil) :: Nil)
- //
- // val lists = List(list0, list1, list2, list3, list32)
- //
- // for(l1 <- lists)
- // yield Map(argumentIds(0) -> l1)
- //
- // }
-}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala b/src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
deleted file mode 100644
index 8e27e2628..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
+++ /dev/null
@@ -1,77 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth
-
-import reconstruction.codegen.CodeGenerator
-import reconstruction.Reconstructor
-
-import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFactory }
-import insynth.Solver
-import insynth.engine.InitialEnvironmentBuilder
-
-import leon.{ LeonDeclaration => Declaration }
-import leon.loader.LeonLoader
-import leon.query.LeonQueryBuilder
-
-import _root_.leon.purescala.Definitions.Program
-import _root_.leon.purescala.TypeTrees.{ TypeTree => Type }
-
-import insynth.util.logging.HasLogger
-
-/**
- * Main class for the synthesis process invocation
- * @param program Leon program object that contains the hole
- * @param hole hole in the program on which the synthesis is called
- */
-class InSynth(_declarations: List[Declaration], goalType: Type, ordered: Boolean = true) extends HasLogger {
-
- def declarations = _declarations
-
-// def this(program: Program, hole: Hole, ordered: Boolean) =
-// this(new LeonLoader(program, hole).load, hole.getType, ordered)
-
- def this(loader: LeonLoader, goalType: Type, ordered: Boolean) =
- this(loader.load, goalType, ordered)
-
- lazy val solver = new Solver(declarations, new LeonQueryBuilder(goalType))
-
- def getExpressions = {
- info("InSynth synthesizing type + " + goalType + " with declarations " + solver.allDeclarations.mkString("\n"))
- val proofTree = solver.getProofTree
-
- assert(proofTree != null, "Proof tree is null" )
- assert(1 == proofTree.getNodes.size)
-
- val codegen = new CodeGenerator
-
- Reconstructor(proofTree.getNodes.head, codegen, ordered)
- }
-
- def getExpressions(builder: InitialEnvironmentBuilder) = {
- info("InSynth synthesizing type + " + goalType + " with declarations " + builder.getAllDeclarations.mkString("\n"))
- val proofTree = solver.getProofTree(builder)
- info("Proof tree is acquired")
-
- assert(proofTree != null, "Proof tree is null" )
- assert(1 == proofTree.getNodes.size)
-
- val codegen = new CodeGenerator
-
- Reconstructor(proofTree.getNodes.head, codegen, ordered)
- }
-
- def getCurrentBuilder = solver.currentBuilder
-
- def getAllDeclarations = _declarations
-
-}
-
-object InSynth {
-
- def apply(declarations: List[Declaration], goalType: Type, ordered: Boolean) =
- new InSynth(declarations, goalType, ordered)
-
- def apply(loader: LeonLoader, goalType: Type, ordered: Boolean) =
- new InSynth(loader.load, goalType, ordered)
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
deleted file mode 100644
index 7d144e04a..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon
-
-import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
-
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Common.FreshIdentifier
-import leon.purescala.Definitions.AbstractClassDef
-
-object CommonTypes {
-
- val LeonBottomType = AbstractClassType(new AbstractClassDef(FreshIdentifier("$IDontCare$"), Nil, None), Nil)
- val InSynthBottomType = Const("$IDontCare$")
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
deleted file mode 100644
index bf353c58a..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
+++ /dev/null
@@ -1,55 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon
-
-import insynth.structures._
-
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Common.FreshIdentifier
-import leon.purescala.Definitions._
-
-import scala.language.implicitConversions
-
-object DomainTypeTransformer extends ( LeonType => DomainType ) {
-
- val InSynthTypeTransformer = TypeTransformer
-
- def apply(typeDef: ClassDef): DomainType = {
- implicit def singletonList(x: DomainType) = List(x)
-
- typeDef match {
- case abs: AbstractClassDef => Atom(Const(abs.id.name))
- case caseClassDef: CaseClassDef => Atom(Const(caseClassDef.id.name))
- }
- }
-
- def apply(leonType: LeonType): DomainType = {
- implicit def singletonList(x: DomainType) = List(x)
-
- leonType match {
- case Untyped => throw new RuntimeException("Should not happen at this point")
- case BooleanType => Atom(Const("Boolean"))
- case UnitType => Atom(Const("Unit"))
- case Int32Type => Atom(Const("Int"))
- case TypeParameter(id) => Atom(Const(id.name))
- case ListType(baseType) => Atom(InSynthTypeTransformer(leonType))
- case ArrayType(baseType) => Atom(InSynthTypeTransformer(leonType))
- case TupleType(baseTypes) => Atom(InSynthTypeTransformer(leonType))
- case SetType(baseType) => Atom(InSynthTypeTransformer(leonType))
- case MultisetType(baseType) => Atom(InSynthTypeTransformer(leonType))
- case MapType(from, to) => Atom(InSynthTypeTransformer(leonType))
- case FunctionType(froms, to) => transformFunction(to, froms)
- case c: ClassType => Atom(Const(c.id.name))
- }
- }
-
- private def transformFunction(fun: LeonType, params: List[LeonType]): DomainType = fun match {
- case FunctionType(froms, to) =>
- transformFunction(to, params ++ froms)
- case Untyped => throw new RuntimeException("Should not happen at this point")
- // query will have this
- case t =>
- Function( params map this, this(t) )
- }
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
deleted file mode 100644
index c8ad8f4ec..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
+++ /dev/null
@@ -1,53 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon
-
-import insynth.structures.SuccinctType
-import insynth.structures.Weight._
-import insynth.load.Declaration
-
-import leon.purescala.TypeTrees.{ TypeTree => LeonType }
-import leon.purescala.Trees.Expr
-
-case class LeonDeclaration(
- override val inSynthType: SuccinctType, override val weight: Weight,
- val leonType: LeonType, val expression: ReconstructionExpression
-)
-extends Declaration(inSynthType, weight) {
-
- def this(expression: ReconstructionExpression, inSynthType: SuccinctType,
- leonType: LeonType, commutative: Boolean, weight: Weight
- ) = {
- this(inSynthType, weight, leonType, expression)
- isCommunitative = commutative
- }
-
- def this(expression: ReconstructionExpression, inSynthType: SuccinctType, leonType: LeonType)
- = this(inSynthType, 1.0f, leonType, expression)
-
- var isCommunitative = false
-
- private var query = false
-
- def getDomainType = DomainTypeTransformer(leonType)
-
- def getSimpleName = expression.getSimpleName
-
- override def toString = getSimpleName + " : " + inSynthType + " : " + leonType + " [" + expression + "]"
-
-}
-
-object LeonDeclaration {
-
- def apply(expression: ReconstructionExpression, inSynthType: SuccinctType, leonType: LeonType)
- = new LeonDeclaration(expression, inSynthType, leonType)
-
- def apply(expression: ReconstructionExpression, inSynthType: SuccinctType,
- leonType: LeonType, weight: Weight
- ) = new LeonDeclaration(inSynthType, weight, leonType, expression)
-
- def apply(expression: ReconstructionExpression, inSynthType: SuccinctType,
- leonType: LeonType, commutative: Boolean, weight: Weight
- ) = new LeonDeclaration(expression, inSynthType, leonType, commutative, weight)
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
deleted file mode 100644
index ae62251a9..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
+++ /dev/null
@@ -1,75 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon
-
-import leon.purescala.TypeTrees.{ TypeTree => LeonType }
-import leon.purescala.Trees.Expr
-import leon.purescala.Common.Identifier
-
-trait ReconstructionExpression {
-
- def getSimpleName: String
-
- override def toString = getSimpleName
-
-}
-
-case object QueryExpression extends ReconstructionExpression {
-
- def getSimpleName = "query"
-
-}
-
-case object ErrorExpression extends ReconstructionExpression {
-
- def getSimpleName = "error"
-
-}
-
-object ImmediateExpression {
-
- def apply(id: Identifier, expr: Expr): ImmediateExpression = ImmediateExpression(id.name, expr)
-
-}
-
-case class ImmediateExpression( name: String, expr: Expr ) extends ReconstructionExpression {
-
- def this(id: Identifier, expr: Expr) = this(id.toString, expr)
-
- def apply( ) = expr
-
- def getSimpleName: String = name
-
-}
-
-object UnaryReconstructionExpression {
-
- def apply(id: Identifier, funToExpr: Expr => Expr): UnaryReconstructionExpression = UnaryReconstructionExpression(id.name, funToExpr)
-
-}
-
-case class UnaryReconstructionExpression( name: String, funToExpr: Expr => Expr ) extends ReconstructionExpression {
-
- def this(id: Identifier, funToExpr: Expr => Expr) = this(id.toString, funToExpr)
-
- def apply( op: Expr ) = funToExpr(op)
-
- def getSimpleName: String = name
-
-}
-
-object NaryReconstructionExpression {
-
- def apply(id: Identifier, funToExpr: List[Expr] => Expr): NaryReconstructionExpression = NaryReconstructionExpression(id.name, funToExpr)
-
-}
-
-case class NaryReconstructionExpression( name: String, funToExpr: List[Expr] => Expr ) extends ReconstructionExpression {
-
- def this(id: Identifier, funToExpr: List[Expr] => Expr) = this(id.toString, funToExpr)
-
- def apply( op: List[Expr] ) = funToExpr(op)
-
- def getSimpleName: String = name
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
deleted file mode 100644
index afc51eb5e..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
+++ /dev/null
@@ -1,55 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon
-
-import insynth.structures._
-
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Common.FreshIdentifier
-import leon.purescala.Definitions._
-
-// enable postfix operations and implicit conversions
-import scala.language.postfixOps
-import scala.language.implicitConversions
-
-object TypeTransformer extends ( LeonType => SuccinctType ) {
-
- def apply(typeDef: ClassDef): SuccinctType = {
- implicit def singletonList(x: SuccinctType) = List(x)
-
- typeDef match {
- case abs: AbstractClassDef => Const(abs.id.name)
- case caseClassDef: CaseClassDef => Const(caseClassDef.id.name)
- }
- }
-
- def apply(leonType: LeonType): SuccinctType = {
- implicit def singletonList(x: SuccinctType) = List(x)
-
- leonType match {
- case Untyped => throw new RuntimeException("Should not happen at this point")
- case BooleanType => Const("Boolean")
- case UnitType => Const("Unit")
- case TypeParameter(id) => Const(id.name)
- case Int32Type => Const("Int")
- case ListType(baseType) => Instance("List", this(baseType) )
- case ArrayType(baseType) => Instance("Array", this(baseType) )
- case TupleType(baseTypes) => Instance("Tuple", baseTypes map { this(_) } toList )
- case SetType(baseType) => Instance("Set", this(baseType) )
- case MultisetType(baseType) => Instance("MultiSet", this(baseType) )
- case MapType(from, to) => Instance("Map", List( this(from), this(to) ))
- case FunctionType(froms, to) => transformFunction(to, froms)
- case c: ClassType => Const(c.id.name)
- }
- }
-
- private def transformFunction(fun: LeonType, params: List[LeonType]): SuccinctType = fun match {
- case FunctionType(froms, to) =>
- transformFunction(to, params ++ froms)
- case Untyped => throw new RuntimeException("Should not happen at this point")
- // query will have this
- case t =>
- Arrow( TSet(params map this distinct), this(t) )
- }
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
deleted file mode 100644
index dc83ac1ff..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
+++ /dev/null
@@ -1,86 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon.loader
-
-import leon.synthesis.condabd.insynth.leon.{ LeonDeclaration => Declaration, _ }
-import leon.synthesis.condabd.insynth.leon.TypeTransformer
-
-import insynth.engine.InitialEnvironmentBuilder
-import insynth.structures.{ SuccinctType => InSynthType, Variable => InSynthVariable, _ }
-
-import leon.purescala.Definitions._
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.Trees._
-
-object DeclarationFactory {
-
- val WEIGHT_FOR_LITERALS = 5f
-
- val listOfInstanceTypes = List(BooleanType, Int32Type)
-
- def makeDeclaration(expression: ReconstructionExpression, leonType: LeonType) = {
- val inSynthType = TypeTransformer(leonType)
- Declaration(expression, inSynthType, leonType)
- }
-
- def makeLiteral(expression: ReconstructionExpression, leonType: LeonType) = {
- val inSynthType = TypeTransformer(leonType)
- Declaration(expression, inSynthType, leonType, WEIGHT_FOR_LITERALS)
- }
-
- def makeDeclaration(expression: ReconstructionExpression, leonType: LeonType, commutative: Boolean) = {
- val inSynthType = TypeTransformer(leonType)
- Declaration(expression, inSynthType, leonType)
- }
-
- def makeArgumentDeclaration(id: Identifier) = {
- val leonType = id.getType
- val inSynthType = TypeTransformer(leonType)
- Declaration(ImmediateExpression(id, Variable(id)), inSynthType, leonType)
- }
-
- def makeArgumentDeclaration(varDecl: ValDef) = {
- val leonType = varDecl.getType
- val inSynthType = TypeTransformer(leonType)
- Declaration(ImmediateExpression(varDecl.id, Variable(varDecl.id)), inSynthType, leonType)
- }
-
- def makeInheritance(from: ClassDef, to: ClassDef) = {
- val expr = UnaryReconstructionExpression("[" +
- from.id.name + "=>" + to.id.name + "]", identity[Expr] _)
- val inSynthType = Arrow(TSet(TypeTransformer(from)), TypeTransformer(to))
- Declaration(expr, inSynthType, Untyped)
- }
-
- def makeInheritance(from: ClassType, to: ClassType) = {
- val expr = UnaryReconstructionExpression("[" +
- from.classDef.id.name + "=>" + to.classDef.id.name + "]", identity[Expr] _)
- val inSynthType = Arrow(TSet(TypeTransformer(from)), TypeTransformer(to))
- Declaration(expr, inSynthType, FunctionType(List(from), to))
- }
-
- def makeDeclarationForTypes(types: List[LeonType])(makeFunction: LeonType => _) =
- for (tpe <- types)
- makeFunction(tpe)
-
- def yieldDeclarationForTypes(types: List[LeonType])(makeFunction: LeonType => Declaration) =
- for (tpe <- types)
- yield makeFunction(tpe)
-
- def makeAbstractDeclaration(inSynthType: InSynthType) = {
- throw new RuntimeException
- Declaration(getAbsExpression(inSynthType), inSynthType, null)
- }
-
-// def makeFieldDeclaration(id: Identifier, caseClassDef: CaseClassType) = {
-// makeDeclaration(
-// NaryReconstructionExpression( id.name , { CaseClass(caseClassDef, _: List[Expr]) } ),
-// FunctionType(caseClassDef.fields map { _.id.getType } toList, classMap(id))
-// )
-// }
-
- // define this for abstract declarations
- def getAbsExpression(inSynthType: InSynthType) =
- ErrorExpression
-}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
deleted file mode 100644
index 53f8c9b5e..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon.loader
-
-/** defines what to load in the PreLoader */
-class LoadSpec {
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
deleted file mode 100644
index 65c207cef..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
+++ /dev/null
@@ -1,251 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon.loader
-
-import leon.synthesis.condabd.insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression, ImmediateExpression, UnaryReconstructionExpression }
-import insynth.structures.{ SuccinctType => InSynthType }
-import insynth.load.Loader
-import insynth.util.logging.HasLogger
-
-import leon.purescala.Definitions.{ Program, FunDef }
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Trees.{ Expr, FunctionInvocation, _ }
-import leon.purescala.Common.{ Identifier }
-import leon.purescala.Definitions.{ AbstractClassDef, CaseClassDef, ClassDef }
-
-// enable postfix operations
-import scala.language.postfixOps
-
-case class LeonLoader(program: Program, variables: List[Identifier], loadArithmeticOps: Boolean = true)
- extends Loader with HasLogger {
- //var temporaryDesiredType: LeonType = Int32Type
-
- lazy val classMap: Map[Identifier, ClassType] = extractClasses
-
- lazy val directSubclassesMap: Map[ClassType, Set[ClassType]] = initializeSubclassesMap(program)
-
- // arguments + all found variables in the hole function
- lazy val variableDeclarations: Seq[Declaration] = variables.map(DeclarationFactory.makeArgumentDeclaration(_))
-
- //lazy val holeDef = initResults._3
-
- lazy val initResults = init
-
- import DeclarationFactory._
-
- def load: List[Declaration] = initResults
-
- private def init = {
-
- // the list of declarations to be returned
- var list = scala.collection.mutable.MutableList[Declaration]()
-
- /* add declarations to builder */
-
- // add function declarations
- for( funDef <- program.definedFunctions ) {
- val tfd = funDef.typed(funDef.tparams.map(_.tp))
-
- val leonFunctionType = tfd.functionType
-
- val newDeclaration = makeDeclaration(
- NaryReconstructionExpression(tfd.fd.id, { args: List[Expr] => FunctionInvocation(tfd, args) } ),
- leonFunctionType
- )
-
- list += newDeclaration
- fine("Leon loader added declaration: " + newDeclaration)
- }
-
- // add predefs and literals
- list ++= PreLoader(loadArithmeticOps)
-
- list ++= extractInheritances
-
- list ++= extractCaseClasses
-
- list ++= extractFields
-
- list ++= extractClassDependentDeclarations
-
- list ++= variableDeclarations
-
- for (variable <- variables; variableType = variable.getType) variableType match {
- case variableClassType: CaseClassType => variableClassType.classDef match {
- case cas @ CaseClassDef(id, tparams, parent, isObj) =>
- fine("adding fields of variable " + variable)
- for (field <- cas.fields)
- list += makeDeclaration(
- ImmediateExpression( field.id.name ,
- CaseClassSelector(CaseClassType(cas, tparams.map(_.tp)), variable.toVariable, field.id) ),
- field.id.getType
- )
- case _ =>
- }
- case _ =>
- }
-
- list.toList
- }
-
- def initializeSubclassesMap(program: Program) = {
- val seqOfPairs = for (classDef <- program.definedClasses)
- yield classDef match {
- case caseClassDef: CaseClassDef =>
- val caseClassType = classMap(classDef.id)
- ( caseClassType, Set[ClassType]( /*caseClassType*/ ) )
- case absClassDef: AbstractClassDef =>
- val childrenTypes = for (child <- absClassDef.knownChildren)
- yield classMap(child.id)
- ( classMap(absClassDef.id), childrenTypes.toSet )
- }
-
- seqOfPairs.toMap
- }
-
- def extractClasses: Map[Identifier, ClassType] = {
- (
- for (classDef <- program.definedClasses)
- yield classDef match {
- case ccd: CaseClassDef => ( ccd.id, CaseClassType(ccd, ccd.tparams.map(_.tp)) )
- case acd: AbstractClassDef => ( acd.id, AbstractClassType(acd, acd.tparams.map(_.tp)) )
- }
- ) toMap
- }
-
- // TODO add anyref to all and all to bottom ???
- def extractInheritances: Seq[Declaration] = {
-
- def extractInheritancesRec(classDef: ClassDef): List[Declaration] =
- classDef match {
- case abs: AbstractClassDef =>
- Nil ++
- (
- for (child <- abs.knownChildren)
- yield makeInheritance(
- classMap(child.id), classMap(abs.id)
- )
- ) ++ (
- for (child <-abs.knownChildren)
- yield extractInheritancesRec(child)
- ).flatten
- case _ =>
- Nil
- }
-
-// (for (classHierarchyRoot <- program.classHierarchyRoots)
-// yield extractInheritancesRec(classHierarchyRoot)).flatten.toList
-
- for (classHierarchyRoot <- program.classHierarchyRoots;
- inheritance <- extractInheritancesRec(classHierarchyRoot))
- yield inheritance
- }
-
- def extractFields(classDef: ClassDef) = classDef match {
- case abs: AbstractClassDef =>
- // this case does not seem to work
- //abs.fields
- Seq.empty
- case cas: CaseClassDef =>
- val cct = CaseClassType(cas, cas.tparams.map(_.tp))
- for (field <- cas.fields)
- yield makeDeclaration(
- UnaryReconstructionExpression(field.id.name, { CaseClassSelector(cct, _: Expr, field.id) }),
- FunctionType(List(classMap(cas.id)), field.id.getType))
- }
-
- def extractFields: Seq[Declaration] = {
- for (classDef <- program.definedClasses;
- decl <- extractFields(classDef))
- yield decl
- }
-
- def extractCaseClasses: Seq[Declaration] = {
- for (caseClassDef @ CaseClassDef(id, tparams, parent, isObj) <- program.definedClasses)
- yield caseClassDef.fields match {
- case Nil => makeDeclaration(
- ImmediateExpression( id.name, { CaseClass(CaseClassType(caseClassDef, caseClassDef.tparams.map(_.tp)), Nil) } ),
- classMap(id)
- )
- case fields => makeDeclaration(
- NaryReconstructionExpression( id.name , { CaseClass(CaseClassType(caseClassDef, caseClassDef.tparams.map(_.tp)), _: List[Expr]) } ),
- FunctionType(fields map { _.id.getType } toList, classMap(id))
- )
- }
- }
-
- def extractClassDependentDeclarations: Seq[Declaration] = {
-// def getClassDef(id: Identifier): CaseClassDef = {
-// program.caseClassDef(id.name)
-// program.definedClasses.find( _.id == `id` ) match {
-// case Some(classDef) => classDef
-// case _ => throw new RuntimeException
-// }
-// }
-
-for ( classDef <- program.definedClasses collect { case ccd: CaseClassDef => ccd };
- if classDef.hasParent)
- yield makeDeclaration(
- UnaryReconstructionExpression( "isInstance[" + classDef.id + "]", { CaseClassInstanceOf(CaseClassType(classDef, classDef.tparams.map(_.tp)), _: Expr)
- } ),
- FunctionType(List(classMap(classDef.parent.get.id)), BooleanType)
- )
- }
-
- // XXX does not care about hiding, does not see function arguments
-
-// def loadLocals(functionBody: Expr, hole: Expr): Set[Declaration] = {
-// scanMethod(functionBody, hole)._2
-// }
-
-}
-
-// old load function
-// def load(program: Program, hole: Hole): List[Declaration] = {
-// initializeClassMap(program)
-//
-// var list: scala.collection.mutable.LinkedList[Declaration] = scala.collection.mutable.LinkedList()
-//
-// /* add declarations to builder */
-//
-// // add function declarations
-// for( funDef@FunDef(id, returnType, args, _, _, _) <- program.definedFunctions ) {
-// val leonFunctionType = FunctionType(args map { _.tpe } toList, returnType)
-//
-// val newDeclaration = makeDeclaration(
-// NaryReconstructionExpression( id, { args: List[Expr] => FunctionInvocation(funDef, args) } ),
-// leonFunctionType
-// )
-//
-// list :+= newDeclaration
-// }
-//
-// // add predefs and literals
-// list ++= PreLoader()
-//
-// list ++= extractInheritances(program)
-//
-// list ++= extractCaseClasses(program)
-////
-//// builder.addDeclarations( extractClassDependentDeclarations(program) )
-//
-// // XXX we currently go through all functions, not efficient!
-// var foundHoleCount = 0
-// for (
-// funDef <-program.definedFunctions;
-// if funDef.hasBody;
-// val (foundHole, declarations) = scanMethod(funDef.getBody, hole);
-// if foundHole;
-// val argDeclarations = funDef.params map { makeArgumentDeclaration(_) }
-// ) {
-// // hack
-// Globals.holeFunDef = funDef
-// foundHoleCount+=1
-//
-// list ++= declarations.toList
-// list ++= argDeclarations
-// }
-// assert(foundHoleCount <= 1)
-//
-// list toList
-// }
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
deleted file mode 100644
index e3abe2f00..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
+++ /dev/null
@@ -1,274 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon.loader
-
-import leon.synthesis.condabd.insynth.leon.{
- LeonDeclaration => Declaration, NaryReconstructionExpression => NAE, ImmediateExpression => IE
-}
-import insynth.structures.{ SuccinctType => InSynthType }
-import insynth.engine.InitialEnvironmentBuilder
-
-import leon.purescala.Definitions.{ Program, FunDef }
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Common.{ Identifier }
-import leon.purescala.Trees._
-
-// enable postfix operations
-import scala.language.postfixOps
-
-object PreLoader extends ( (Boolean) => List[Declaration] ) {
-
- import DeclarationFactory._
-
- def apply(loadArithmeticOps: Boolean = true): List[Declaration] = {
-
- val supportedBaseTypes = List(BooleanType, Int32Type)
- var list = scala.collection.mutable.MutableList[Declaration]()
-
- list += getAnd
- list += getNot
-
- list += getLessEquals
- list += getLessThan
- list += getGreaterThan
- list ++= getEquals(supportedBaseTypes)
-
- if (loadArithmeticOps)
- list ++= getArithmeticOps
-
- list toList
- }
-
- def getAnd =
- // case And(args) if args.isEmpty => BooleanLiteral(true)
- makeDeclaration(
- makeNAE("And", (args: List[Expr]) => And( args )),
- FunctionType( List(BooleanType, BooleanType), BooleanType )
- )
-
- def getNot =
- // case Not(arg) => rec(ctx, arg) match {
- makeDeclaration(
- makeNAE( "Not", (args: List[Expr]) => Not( args.head ) ),
- FunctionType( List(BooleanType), BooleanType )
- )
-
- def getOr =
- // case Or(args) if args.isEmpty => BooleanLiteral(false)
- makeDeclaration(
- makeNAE( "Or", (args: List[Expr]) => Or( args ) ),
- FunctionType( List(BooleanType, BooleanType), BooleanType )
- )
-
- def getImplies =
- // case Implies(l, r) => (rec(ctx, l), rec(ctx, r)) match {
- makeDeclaration(
- makeNAE( "=>", (args: List[Expr]) => Implies( args(0), args(1) ) ),
- FunctionType( List(BooleanType, BooleanType), BooleanType )
- )
-
- def getIff =
- //case Iff(le, re) => (rec(ctx, le), rec(ctx, re)) match {
- makeDeclaration(
- makeNAE( "<=>", (args: List[Expr]) => Iff( args(0), args(1) ) ),
- FunctionType( List(BooleanType, BooleanType), BooleanType )
- )
-
- def getEquals(listOfInstanceTypes: List[LeonType]) =
- // case Equals(le, re) => {
- yieldDeclarationForTypes(listOfInstanceTypes) {
- x: LeonType =>
- makeDeclaration(
- makeNAE( "=", (args: List[Expr]) => Equals( args(0), args(1) ) ),
- FunctionType( List(x, x), BooleanType ),
- true
- )
- }
-
- def getArithmeticOps = {
- // case Plus(l, r) => (rec(ctx, l), rec(ctx, r)) match {
- makeDeclaration(
- makeNAE( "+", (args: List[Expr]) => Plus( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), Int32Type )
- ) ::
- // case Minus(l, r) => (rec(ctx, l), rec(ctx, r)) match {
- makeDeclaration(
- makeNAE( "-", (args: List[Expr]) => Minus( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), Int32Type )
- ) ::
- // case UMinus(e) => rec(ctx, e) match {
- makeDeclaration(
- makeNAE( "UMinus", (args: List[Expr]) => UMinus( args.head ) ),
- FunctionType( List(Int32Type), Int32Type )
- ) ::
- //case Times(l, r) => (rec(ctx, l), rec(ctx, r)) match {
- makeDeclaration(
- makeNAE( "*", (args: List[Expr]) => Times( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), Int32Type )
- ) ::
- // case Division(l, r) => (rec(ctx, l), rec(ctx, r)) match {
- makeDeclaration(
- makeNAE( "/", (args: List[Expr]) => Division( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), Int32Type )
- ) ::
- // case Modulo(l,r) => (rec(ctx,l), rec(ctx,r)) match {
- makeDeclaration(
- makeNAE( "%", (args: List[Expr]) => Modulo( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), Int32Type )
- ) :: Nil
- }
-
- def getLessThan =
- // case LessThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
- makeDeclaration(
- makeNAE( "<", (args: List[Expr]) => LessThan( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), BooleanType )
- )
-
- def getGreaterThan =
- // case GreaterThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
- makeDeclaration(
- makeNAE( ">", (args: List[Expr]) => GreaterThan( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), BooleanType )
- )
-
- def getLessEquals =
- // case LessEquals(l,r) => (rec(ctx,l), rec(ctx,r)) match {
- makeDeclaration(
- makeNAE( "<=", (args: List[Expr]) => LessEquals( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), BooleanType )
- )
-
- def getGreaterEquals =
- // case GreaterEquals(l,r) => (rec(ctx,l), rec(ctx,r)) match {
- makeDeclaration(
- makeNAE( ">=", (args: List[Expr]) => GreaterEquals( args(0), args(1) ) ),
- FunctionType( List(Int32Type, Int32Type), BooleanType )
- )
-
- // currently Leon has some troubles with sets
- def getSetOperations(listOfInstanceTypes: List[LeonType]) = {
-
- // case SetUnion(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
- yieldDeclarationForTypes(listOfInstanceTypes) {
- x: LeonType =>
- makeDeclaration(
- makeNAE( "SetUnion", (args: List[Expr]) => SetUnion( args(0), args(1) ) ),
- FunctionType( List(SetType(x), SetType(x)), SetType(x) )
- )
- } ++
- //case SetIntersection(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
- yieldDeclarationForTypes(listOfInstanceTypes) {
- x: LeonType =>
- makeDeclaration(
- makeNAE( "SetIntersection", (args: List[Expr]) => SetIntersection( args(0), args(1) ) ),
- FunctionType( List(SetType(x), SetType(x)), SetType(x) )
- )
- } ++
- //case SetDifference(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
- yieldDeclarationForTypes(listOfInstanceTypes) {
- x: LeonType =>
- makeDeclaration(
- makeNAE( "SetDifference", (args: List[Expr]) => SetDifference( args(0), args(1) ) ),
- FunctionType( List(SetType(x), SetType(x)), SetType(x) )
- )
- } ++
- //case ElementOfSet(el,s) => (rec(ctx,el), rec(ctx,s)) match {
- yieldDeclarationForTypes(listOfInstanceTypes) {
- x: LeonType =>
- makeDeclaration(
- makeNAE( "ElementOfSet", (args: List[Expr]) => ElementOfSet( args(0), args(1) ) ),
- FunctionType( List(x, SetType(x)), BooleanType )
- )
- } ++
- // case SetCardinality(s) => {
- yieldDeclarationForTypes(listOfInstanceTypes) {
- x: LeonType =>
- makeDeclaration(
- makeNAE( "SetCardinality", (args: List[Expr]) => SetCardinality( args(0) ) ),
- FunctionType( List(SetType(x)), Int32Type )
- )
- }
-
- }
-
- // not covered atm
-// case CaseClass(cd, args) => CaseClass(cd, args.map(rec(ctx, _)))
-// case CaseClassInstanceOf(cd, expr) => {
-// case CaseClassSelector(cd, expr, sel) => {
-
- // we do not synthesize ifs explicitly
- //case IfExpr(cond, then, elze) => {
- def getIfExpr(listOfInstanceTypes: List[LeonType]) = {
- yieldDeclarationForTypes(listOfInstanceTypes) {
- x: LeonType =>
- makeDeclaration(
- makeNAE( "If", (args: List[Expr]) => args match {
- case List(cond, then_, elze) => IfExpr(cond, then_, elze)
- case _ => throw new RuntimeException
- }),
- FunctionType( List(BooleanType, x, x), x )
- )
- }
- }
-
-// no arrays atm
-// case f @ ArrayFill(length, default) => {
-// case ArrayLength(a) =>
-// case ArrayUpdated(a, i, v) =>
-// case ArraySelect(a, i) =>
-// case FiniteArray(exprs) =>
-
- // no maps atm
-// case g @ MapGet(m,k) => (rec(ctx,m), rec(ctx,k)) match {
-// case u @ MapUnion(m1,m2) => (rec(ctx,m1), rec(ctx,m2)) match {
-// case i @ MapIsDefinedAt(m,k) => (rec(ctx,m), rec(ctx,k)) match {
-
- // needed?
-// case Distinct(args) => {
-
- // not covered atm
- // case Tuple(ts) => {
- // case TupleSelect(t, i) => {
- // should produce all declarations with tupleselect
-
- // needed?
- //case Waypoint(_, arg) => rec(ctx, arg)
- //case FunctionInvocation(fd, args) => {
-
- def getLiteralDeclarations = {
-
- var list = scala.collection.mutable.MutableList[Declaration]()
-
-// case i @ IntLiteral(_) => i
- list += makeLiteral(
- IE( "IntLit", IntLiteral(0) ),
- Int32Type
- )
-// case b @ BooleanLiteral(_) => b
- list += makeLiteral(
- IE( "BoolLit", BooleanLiteral(false) ),
- BooleanType
- )
-// case u @ UnitLiteral => u
- list += makeLiteral(
- IE( "UnitLit", UnitLiteral() ),
- UnitType
- )
-
-// case e @ EmptySet(_) => e
- // NOTE sets are removed in Leon
-// yieldDeclarationForTypes(listOfInstanceTypes) {
-// x: LeonType =>
-// list += makeDeclaration(
-// IE( "SetLit", EmptySet(x) ),
-// SetType(x)
-// )
-// }
-
- list toList
- }
-
- def makeNAE( name: String, fun: List[Expr]=>Expr ): NAE = NAE( name, fun )
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
deleted file mode 100644
index 63833f57f..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon
-package query
-
-import loader.DeclarationFactory
-import insynth.engine.InitialSender
-import insynth.structures.SuccinctType
-import insynth.query.Query
-
-import leon.purescala.TypeTrees._
-import leon.purescala.Common.FreshIdentifier
-
-case class LeonQuery(override val inSynthRetType: SuccinctType, decl: LeonDeclaration, sender: InitialSender)
-extends Query(inSynthRetType) {
-
- def getSolution = sender.getAnswers
-
- def getDeclaration = decl
-
- def getSender = sender
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
deleted file mode 100644
index 1105f354d..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.leon
-package query
-
-import insynth.query._
-import insynth.engine.InitialSender
-import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
-
-import loader.DeclarationFactory
-
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Common.FreshIdentifier
-import leon.purescala.Definitions.AbstractClassDef
-
-import CommonTypes._
-
-class LeonQueryBuilder(leonGoalType: LeonType) extends QueryBuilder(TypeTransformer(leonGoalType)) {
-
- val leonRetType = LeonBottomType
- val leonType = FunctionType(List(leonGoalType), leonRetType)
-
- val inSynthRetType = InSynthBottomType
- val inSynthType = Arrow(TSet(tpe), inSynthRetType)
-
- def getQuery = LeonQuery(inSynthRetType, new LeonDeclaration(QueryExpression, inSynthType, leonType), new InitialSender())
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
deleted file mode 100644
index 9c688c255..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.reconstruction
-
-import insynth.structures.Weight._
-import leon.purescala.Trees.Expr
-
-/**
- * Encapsulation of the result output from the reconstruction phase, non UI dependent
- */
-case class Output(snippet: Expr, weight: Weight){
- def getSnippet = snippet
- def getWeight = weight
-
- override def equals(obj:Any) = {
- obj.isInstanceOf[Output] && obj.asInstanceOf[Output].snippet == this.snippet
- }
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
deleted file mode 100644
index 67058cd93..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
+++ /dev/null
@@ -1,37 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd.insynth.reconstruction
-
-import insynth.structures.{ SimpleNode, Weight }
-import insynth.reconstruction.stream.{ Node => LambdaNode, _ }
-import insynth.reconstruction._
-
-import codegen.CodeGenerator
-
-import insynth.util.format.{ FormatSuccinctNode, FormatStreamUtils }
-import insynth.util.logging.HasLogger
-import insynth.util._
-
-/**
- * Object for reconstruction of proof trees into output(s)
- */
-object Reconstructor extends ( (SimpleNode, CodeGenerator, Boolean) => Stream[Output]) with HasLogger {
-
- def apply(tree: SimpleNode, codeGenerator: CodeGenerator, streamOrdered: Boolean = false) = {
-
- // transform the trees (first two steps of the code generation phase)
- val stream = Streamer(tree, streamOrdered)
-
- info("streamer done, stream computed")
-
- // for each tree, generate the code for it
- val generatedCode = stream map {
- resPair => Output(codeGenerator(resPair._1), resPair._2)
- }
-
- info("stream of solutions is generated")
-
- generatedCode
- }
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
deleted file mode 100644
index 3b2b67036..000000000
--- a/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
+++ /dev/null
@@ -1,118 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon
-package synthesis.condabd.insynth
-package reconstruction.codegen
-
-import scala.text.Document
-import scala.text.Document.empty
-
-import leon._
-import insynth.reconstruction.stream._
-import insynth.structures.Function
-import insynth.util.logging.HasLogger
-
-import purescala.Trees.{ Expr }
-import purescala.TypeTrees.{ TypeTree => DomainType, FunctionType }
-import purescala.{ TypeTrees => domain }
-import purescala.Trees.{ Expr => CodeGenOutput }
-
-/**
- * class that converts an intermediate tree into a list of output elements (elements
- * capable of Scala code generation)
- * should be extended to provide syntax-style variants
- */
-class CodeGenerator extends (Node => CodeGenOutput) with HasLogger {
-
- /**
- * takes the tree and calls the recursive function and maps documents to Output elements
- * @param tree root of intermediate (sub)tree to transform
- * @return list of output (code snippet) elements
- */
- def apply(tree: Node) = {
- // match the starting tree to an application that produces query type
- tree match {
- case Application(Function(_, _ /* BottomType */), queryDec :: List(innerApp)) =>
- transform(innerApp)
- case _ => throw new RuntimeException
- }
- }
-
- /** transform context determines the place of the element to transform */
- object TransformContext extends Enumeration {
- type TransformContext = Value
- // expression, application, parameter, argument (in a function), single parameter
- val Expr, App, Par, Arg, SinglePar = Value
- }
- // import all transform context values
- import TransformContext._
-
- /**
- * main method (recursive) for transforming a intermediate (sub)tree
- * @param tree root node of the (sub)tree to transform
- * @return list of documents containing all combinations of available expression for
- * the given (sub)tree
- */
- def transform(tree: Node): CodeGenOutput = {
- tree match {
- // variable (declared previously as arguments)
- case Variable(tpe, name) =>
- // what to do here
- throw new RuntimeException
- // identifier from the scope
- case Identifier(tpe, LeonDeclaration(_, _, _, im: ImmediateExpression)) =>
- im()
- // apply parameters in the tail of params according to the head of params
- case app@Application(tpe, params) => {
- // match the application definition term
- params.head match {
- case Identifier(_, decl: LeonDeclaration) => {
- info("Generating application: " + decl + " with params: " + params + " params.size = " + params.size)
-
- // for an expression of each parameters yield the appropriate transformed expression
- val paramsExpr: List[CodeGenOutput] = params.tail.map(transform _)
-
- decl.expression match {
- // identifier is a function
- case NaryReconstructionExpression(_, fun) =>
- info("NaryReconstructionExpression with params: " + paramsExpr + " paramsExpr.size = " + paramsExpr.size)
- assert(paramsExpr.size >= 1)
-
- // return application of transformed parameters to fun
- fun(paramsExpr)
-
- // identifier is an immediate expression
- case ImmediateExpression(_, expr) =>
- assert(paramsExpr.isEmpty)
- expr
-
- // identifier is an unary operator
- case UnaryReconstructionExpression(_, fun) =>
- assert(paramsExpr.size == 1)
- fun(paramsExpr.head)
-
- // this should not happen
- case _ => throw new Exception("Unsupported reconstruction: " + decl.expression)
- }
- } // case Identifier
-
- case innerApp@Application(appType: Function, params) =>
- warning("Cannot have app head: " + innerApp + " in application " + app)
- throw new Exception("Cannot have app head: " + innerApp + " in application " + app)
-
- // function that is created as an argument or anything else
- case /*Identifier(_, _:AbsDeclaration) | */_:Variable | _ =>
- throw new Exception("Unsupported combination for application head " + params.head)
-
- } // params.head match
- }
-
- // abstraction first creates all of its arguments
- case Abstraction(tpe, vars, subtrees) =>
- assert(vars.size > 0)
- throw new RuntimeException
-
- } // tree match
- }
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala b/src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
deleted file mode 100644
index 1339717ca..000000000
--- a/src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
+++ /dev/null
@@ -1,119 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package ranking
-
-import leon.purescala.Trees._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps
-
-import insynth.reconstruction.Output
-import _root_.insynth.structures.Weight._
-import _root_.insynth.util.logging.HasLogger
-
-object Candidate {
- private var _freshResultVariable: Identifier = _
- def freshResultVariable = _freshResultVariable
-
- def getFreshResultVariable(tpe: TypeTree) = _freshResultVariable = FreshIdentifier("result", true).setType(tpe)
-
- def makeDefaultCandidates(candidatePairs: IndexedSeq[Output], bodyBuilder: Expr => Expr, tfd: TypedFunDef) = {
- getFreshResultVariable(tfd.returnType)
- candidatePairs map {
- pair =>
- DefaultCandidate(pair.getSnippet, bodyBuilder(pair.getSnippet), pair.getWeight, tfd)
- }
- }
-
- def makeCodeGenCandidates(candidatePairs: IndexedSeq[Output], bodyBuilder: Expr => Expr, tfd: TypedFunDef) = {
- getFreshResultVariable(tfd.returnType)
- candidatePairs map {
- pair =>
- CodeGenCandidate(pair.getSnippet, bodyBuilder(pair.getSnippet), pair.getWeight, tfd)
- }
- }
-}
-
-abstract class Candidate(weight: Weight) {
- def getExpr: Expr
-
- def prepareExpression: Expr
-
- def getWeight = weight
-}
-
-case class DefaultCandidate(expr: Expr, bodyExpr: Expr, weight: Weight, tfd: TypedFunDef)
- extends Candidate(weight) with HasLogger {
- import Candidate._
-
- override def getExpr = expr
-
- lazy val expressionToEvaluate = {
- import TreeOps._
-
- assert(bodyExpr.getType != Untyped)
- val resFresh = freshResultVariable//.setType(expr.getType)
-
- val (id, post) = tfd.postcondition.get
-
- // body can contain (self-)recursive calls
- Let(resFresh, bodyExpr,
- replace(Map(Variable(id) -> Variable(resFresh)),
- matchToIfThenElse(post)))
- }
-
- override def prepareExpression = {
- // set appropriate body to the function for the correct evaluation due to recursive calls
- tfd.fd.body = Some(bodyExpr)
-
-// finest("going to evaluate candidate for: " + tfd)
-// finest("going to evaluate candidate for: " + expressionToEvaluate)
- expressionToEvaluate
- }
-}
-
-case class CodeGenCandidate(expr: Expr, bodyExpr: Expr, weight: Weight, tfd: TypedFunDef)
- extends Candidate(weight) with HasLogger {
- import Candidate._
-
- override def getExpr = expr
-
- lazy val (expressionToEvaluate, newFunDef) = {
- import TreeOps._
- val fd = tfd.fd
-
- val newFunId = FreshIdentifier("tempIntroducedFunction")
- val newFun = new FunDef(newFunId, fd.tparams, fd.returnType, fd.params)
- newFun.precondition = fd.precondition
- newFun.postcondition = fd.postcondition
-
- def replaceFunDef(expr: Expr) = expr match {
- case FunctionInvocation(`tfd`, args) =>
- Some(FunctionInvocation(newFun.typed(tfd.tps), args))
- case _ => None
- }
- val newBody = postMap(replaceFunDef)(bodyExpr)
-
- newFun.body = Some(newBody)
-
- assert(bodyExpr.getType != Untyped)
- val resFresh = freshResultVariable//.setType(expr.getType)
-
- val (id, post) = newFun.postcondition.get
-
- // body can contain (self-)recursive calls
- (Let(resFresh, newBody,
- replace(Map(Variable(id) -> Variable(resFresh)),
- matchToIfThenElse(post)))
- ,
- newFun)
- }
-
- override def prepareExpression = {
-// finest("going to evaluate candidate for: " + tfd)
-// finest("going to evaluate candidate for: " + expressionToEvaluate)
- expressionToEvaluate
- }
-}
diff --git a/src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala b/src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
deleted file mode 100644
index 1c9d53e67..000000000
--- a/src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
+++ /dev/null
@@ -1,69 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package ranking
-
-import evaluation._
-
-case class Evaluation(exampleRunner: ExampleRunner) {
-
- // keep track of which examples to evaluate next
- var nextExamples: Map[Int, Int] = Map().withDefaultValue(0)
-
- def getNumberOfEvaluations(ind: Int) = nextExamples(ind)
-
- // keep track of evaluation results
- var evaluations = Map[Int, Array[Boolean]]()
-
- def getEvaluationVector(ind: Int) =
- (evaluations(ind), nextExamples(ind))
-
- def numberOfExamples = exampleRunner.examples.size
-
- def evaluate(exprInd: Int) = {
- numberOfEvaluationCalls += 1
-
- // get next example index and update
- val nextExample = nextExamples(exprInd)//OrElse(exprInd, 0)
- if (nextExample >= numberOfExamples) throw new RuntimeException("Exhausted examples for " + exprInd)
- nextExamples += (exprInd -> (nextExample + 1))
-
- val result = exampleRunner.evaluate(exprInd, nextExample)
-
- // update evaluation results
- val evalArray = evaluations.getOrElse(exprInd, Array.ofDim[Boolean](numberOfExamples))
- evalArray(nextExample) = result
- evaluations += (exprInd -> evalArray)
-
- result
- }
-
- // for measurements
- var numberOfEvaluationCalls = 0
- def getEfficiencyRatio = numberOfEvaluationCalls.toFloat / (numberOfExamples * evaluations.size)
-
-// def evaluate(expr: Int, exampleInd: Int) = {
-// val nextExample = nextExamples.getOrElse(expr, 0)
-// assert(exampleInd <= nextExample)
-//
-// if (exampleInd >= nextExample) {
-// nextExamples += (expr -> (nextExample + 1))
-// val example = examples(nextExample)
-// val result = example(expr)
-// val evalArray = evaluations.getOrElse(expr, Array.ofDim[Boolean](examples.size))
-// evalArray(nextExample) = result
-// evaluations += (expr -> evalArray)
-// result
-// } else {
-// assert(evaluations.contains(expr))
-// evaluations.get(expr).get(exampleInd)
-// }
-// }
-
-// def evalAvailable(expr: Int) = {
-// val nextExample = nextExamples.getOrElse(expr, 0)
-// if (nextExample >= examples.size) false
-// else true
-// }
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala b/src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
deleted file mode 100644
index 030aabae8..000000000
--- a/src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
+++ /dev/null
@@ -1,150 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package ranking
-
-import scala.util.control.Breaks._
-import scala.collection._
-
-import leon.purescala.Trees.{ Variable => LeonVariable, _ }
-
-// enable postfix
-import scala.language.postfixOps
-
-class Ranker(candidates: IndexedSeq[Candidate], evaluation: Evaluation, checkTimeout: (() => Boolean) = { () => false }, printStep: Boolean = false) {
-
- val candidatesSize = candidates.size
-
- var rankings: Array[Int] = (0 until candidatesSize).toArray
-
- // keep track of intervals
- var tuples: Map[Int, (Int, Int)] =
- (for (i <- 0 until candidatesSize)
- yield (i, (0, evaluation.numberOfExamples))) toMap
-
- def evaluate(ind: Int) {
- val tuple = tuples(ind)
- val expr = ind
-
- tuples += ( ind ->
- {
- if (evaluation.evaluate(expr)) {
- (tuple._1 + 1, tuple._2)
- } else {
- (tuple._1, tuple._2 - 1)
- }
- }
- )
-
- }
-
- def swap(ind1: Int, ind2: Int) = {
- val temp = rankings(ind1)
- rankings(ind1) = rankings(ind2)
- rankings(ind2) = temp
- }
-
- def bubbleDown(ind: Int): Unit = {
- if (compare(rankings(ind), rankings(ind + 1))) {
- swap(ind, ind + 1)
- if (ind < candidatesSize-2)
- bubbleDown(ind + 1)
- }
- }
-
- var numberLeft = candidatesSize
-
- def getMax = {
-
- numberLeft = candidatesSize
-
- while (numberLeft > 1 && !checkTimeout()) {
-
- evaluate(rankings(0))
-
- if (printStep) {
- println(printTuples)
- println("*** left: " + numberLeft)
- }
-
- bubbleDown(0)
-
- val topRank = rankings(0)
- var secondRank = rankings(1)
-
- while (strictCompare(secondRank, topRank) && numberLeft > 1) {
- numberLeft -= 1
- swap(1, numberLeft)
- secondRank = rankings(1)
- }
-
- }
-
- if (printStep) {
- println(printTuples)
- println("***: " + numberLeft)
- }
-
- (candidates(rankings(0)), rankings(0))
- }
-
- def fullyEvaluate(ind: Int) = {
- val tuple = tuples(ind)
- for (_ <- 0 until (tuple._2 - tuple._1))
- evaluate(ind)
-
- tuples(ind)
- }
-
-// def getVerifiedMax = {
-// val results = (for (candidate <- 0 until candidates.size)
-// yield (candidate,
-// (0 /: (0 until evaluation.getNumberOfExamples)) {
-// (res, exampleInd) =>
-// if (evaluation.evaluate(candidate, exampleInd)) {
-// res + 1
-// } else {
-// res
-// }
-// }))
-//
-// val maxPassed = results.sortWith((r1, r2) => r1._2 < r2._2)(candidates.size - 1)._2
-//
-// (results.filter(_._2 == maxPassed).map(x => candidates(x._1)), results)//.map(x => candidates(x._1))
-// }
-
- def strictCompare(x: Int, y: Int) = {
- val tuple1 = tuples(x)
- val tuple2 = tuples(y)
-
- tuple1._2 <= tuple2._1
- }
-
- // candidate x <= candidate y heuristically (compare their sizes)
- def heurCompare(x: Int, y: Int) = candidates(x).getWeight >= candidates(y).getWeight
-
- def compare(x: Int, y: Int) = {
- val tuple1 = tuples(x)
- val tuple2 = tuples(y)
-
- val median1 = (tuple1._1 + tuple1._2).toFloat/2
- val median2 = (tuple2._1 + tuple2._2).toFloat/2
-
- /*median1 < median2 || median1 == median2 && */
- tuple1._2 < tuple2._2 || tuple1._2 == tuple2._2 &&
- (heurCompare(x, y) || median1 < median2)
- }
-
- def rankOf(expr: Int) =
- rankings.indexOf(expr)
-
- def printTuples =
- (for ((tuple, ind) <-
- tuples.toList.sortWith((tp1, tp2) => rankOf(tp1._1) <= rankOf(tp2._1)).zipWithIndex)
- yield (if (tuple._1 == rankings(0)) "->" else if (ind >= numberLeft) "/\\" else " ") + tuple._1 +
- ": " +
- ((0 until evaluation.numberOfExamples) map {
- x => if (x < tuple._2._1) '+' else if (x >= tuple._2._2) '-' else '_'
- }).mkString).mkString("\n")
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala b/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
deleted file mode 100644
index d7034b062..000000000
--- a/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
+++ /dev/null
@@ -1,160 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis
-package condabd.refinement
-
-import scala.collection.mutable.{Seq => _, _}
-
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.TreeOps
-
-import condabd.insynth.leon.loader.LeonLoader
-import insynth.util.logging.HasLogger
-
-/**
- * Class used for filtering out unnecessary candidates during the search
- */
-class Filter(program: Program, holeFunDef: TypedFunDef, refiner: VariableRefiner) extends HasLogger {
-
- // caching of previously filtered expressions
- type FilterSet = HashSet[Expr]
- private var seenBranchExpressions: FilterSet = new FilterSet()
-
- /**
- * expr - expression to check
- * funDefArgs - list of identifiers according to which well ordering is checked
- */
- def isAvoidable(expr: Expr, funDefArgs: List[Identifier]) = {
- finest(
- "Results for refining " + expr + ", are: " +
- " ,isCallAvoidableBySize(expr) " + isCallAvoidableBySize(expr, funDefArgs) +
- " ,hasDoubleRecursion(expr) " + hasDoubleRecursion(expr) +
- " ,isOperatorAvoidable(expr) " + isOperatorAvoidable(expr) +
- " ,isUnecessaryInstanceOf(expr) " + isUnecessaryInstanceOf(expr) +
- ", isUnecessaryStructuring(expr) " + isUnecessaryStructuring(expr)
- )
- if (seenBranchExpressions contains expr) {
- true
- } else {
- val result = isCallAvoidableBySize(expr, funDefArgs) || hasDoubleRecursion(expr) ||
- isOperatorAvoidable(expr) || isUnecessaryInstanceOf(expr) ||
- isUnecessaryStructuring(expr)
-
- // cache results
- if (result) {
- seenBranchExpressions += expr
- }
- result
- }
- }
-
- val pureRecurentExpression: Expr =
- if (holeFunDef.hasBody) {
- FunctionInvocation(holeFunDef, holeFunDef.params map { _.toVariable })
- } else
- Error("Hole FunDef should have a body")
- fine("Refiner initialized. Recursive call: " + pureRecurentExpression)
-
- def isBadInvocation(expr2: Expr) = expr2 match {
- case `pureRecurentExpression` =>
- fine("Pure recurrent expression detected: " + pureRecurentExpression)
- true
- case FunctionInvocation(`holeFunDef`, args) =>
- (0 /: (args zip holeFunDef.params.map(_.id))) {
- case (res, (arg, par)) if res == 0 => isLess(arg, par)
- case (res, _) => res
- } >= 0
- case _ => false
- }
-
- // check according to size
- // true - YES, false - NO or don't know
- // basically a lexicographic (well-founded) ordering
- def isCallAvoidableBySize(expr: Expr, funDefArgs: List[Identifier]) = {
- TreeOps.exists(isBadInvocation)(expr)
- }
-
- def isLess(arg: Expr, variable: Identifier): Int = {
- def getSize(arg: Expr, size: Int): Int = arg match {
- //case FunctionInvocation(_, args) => -1 // if some random calls are involved
- case CaseClassSelector(cas, expr, fieldId) if fieldId.name == "tail" => getSize(expr, size - 1)
- case CaseClassSelector(cas, expr, fieldId) if fieldId.name == "head" => size + 1
- case CaseClass(caseClassDef, head :: tail :: Nil) => getSize(tail, size + 1)
- case CaseClass(caseClassDef, Nil) => 1
- case v: Variable => if (v.id == variable) size else {
-// finest("Refiner: Variable IDs do not match: " + v.id.uniqueName + " and " + variable.uniqueName )
- 1
- }
- case _ => //throw new RuntimeException("Could not match " + arg + " in getSize")
- -1
- }
-
- getSize(arg, 0)
- }
-
- def hasDoubleRecursion(expr: Expr) = {
- def recursionLevel(expr: Expr, rec: Seq[Int]) = expr match {
- case FunctionInvocation(`holeFunDef`, args) => (0 +: rec).max + 1
- case _ => (0 +: rec).max
- }
-
- TreeOps.foldRight(recursionLevel)(expr) >= 2
- }
-
- // removing checking instance of fields (e.g. x.field.isInstanceOf[..]) - this is deemed unecessary
- def isUnecessaryStructuring(expr: Expr) = {
- var found = false
-
- def isCaseClassSelector(expr: Expr) = expr match {
- case CaseClassInstanceOf(_, _: CaseClassSelector) =>
- found = true
- None
- case _ => None
- }
-
- TreeOps.postMap(isCaseClassSelector)(expr)
-
- found
- }
-
- def isOperatorAvoidable(expr: Expr) = expr match {
- case And(expr1 :: expr2) if expr1 == expr2 => true
- case Or(expr1 :: expr2) if expr1 == expr2 => true
- case LessThan(expr1, expr2) if expr1 == expr2 => true
- case LessEquals(expr1, expr2) if expr1 == expr2 => true
- case GreaterThan(expr1, expr2) if expr1 == expr2 => true
- case GreaterEquals(expr1, expr2) if expr1 == expr2 => true
- case Equals(expr1, expr2) if expr1 == expr2 => true
- case _ => false
- }
-
- def isUnecessaryInstanceOf(expr: Expr) = {
- def isOfClassType(exp: Expr, classDef: ClassDef) =
- expr.getType match {
- case tpe: ClassType => tpe.classDef == classDef
- case _ => false
- }
- expr match {
- // if we check instance of an constructor we know that it is a constant
-// case CaseClassInstanceOf(_, _: CaseClass) =>
-// true
- case CaseClassInstanceOf(classDef, _: FunctionInvocation) =>
- true
- case CaseClassInstanceOf(cct, innerExpr)
- if isOfClassType(innerExpr, cct.classDef) =>
- true
- case CaseClassInstanceOf(cct, v@Variable(id)) => {
- val possibleTypes = refiner.getPossibleTypes(id)
- if (possibleTypes.size == 1)
- possibleTypes.head.classDef == cct.classDef
- else
- false
- }
- case _ => false
- }
- }
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
deleted file mode 100644
index 87b4d30b8..000000000
--- a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
+++ /dev/null
@@ -1,69 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package refinement
-
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.evaluators._
-
-import insynth.leon.{ LeonDeclaration => Declaration, _ }
-
-import _root_.insynth.util.logging.HasLogger
-
-// TODO a *provider* for maps from id to possible types (so that not all classes need to maintain a map)
-trait VariableRefiner extends HasLogger {
-
- type Type = ClassType
-
- def getPossibleTypes(id: Identifier): Set[Type]
-
- def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])])
-
- /**
- * refine given declarations according to given expression and current partition condition
- * @param expr
- * @param condition
- * @param declarations
- * @return new declarations with refined ones
- */
- def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null): List[(Identifier, Set[ClassType])]
-
- def refine(expr: Expr, condition: Expr, declarations: List[Declaration], evaluator: Evaluator = null) = {
- checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator) match {
- case Nil => (false, declarations)
- case list =>
- ((false, declarations) /: list) {
- case ((flag, refined), (id, newTypes)) =>
- fine(((flag, refined), (id, newTypes)).toString)
- if (newTypes.size == 1)
- (true, refineDeclarations(id, newTypes.head, refined))
- else
- (flag, refined)
- }
- }
- }
-
- def refineDeclarations(id: Identifier, newType: ClassType, allDeclarations: List[Declaration]) =
- (for (dec <- allDeclarations)
- yield dec match {
- case Declaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, Variable(`id`))) =>
- ((
- newType match {
- case cct: CaseClassType =>
- fine("matched case class def for refinement " + cct)
- for (field <- cct.fields)
- yield Declaration(
- ImmediateExpression(id.name + "." + field.id.name,
- CaseClassSelector(cct, imex.expr, field.id)),
- TypeTransformer(field.tpe), field.tpe)
- case _ =>
- Seq.empty
- }): Seq[Declaration]) :+ Declaration(imex, TypeTransformer(newType), newType)
- case _ =>
- Seq(dec)
- }).flatten
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerCompose.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerCompose.scala
deleted file mode 100644
index 0f02aedd1..000000000
--- a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerCompose.scala
+++ /dev/null
@@ -1,50 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package refinement
-
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.evaluators._
-
-import insynth.leon.{ LeonDeclaration => Declaration, _ }
-
-// TODO update other refiners with results of this one
-class VariableRefinerCompose extends VariableRefiner {
-
- private var refiners = Array[VariableRefiner]()
-
- def add(refiner: VariableRefiner) = {
- refiners :+= refiner
- // refiner.refinePossibleTypes(id, types)
- this
- }
-
- override def getPossibleTypes(id: Identifier) =
- refiners.head.getPossibleTypes(id)
-
- override def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])]) =
- for (refiner <- refiners)
- refiner.refinePossibleTypes(refinements)
-
- override def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null) = {
- val refineMap =
- ((Map[Identifier, Set[ClassType]]()) /: refiners) {
- case (refineMap, refiner) =>
- ( refineMap /: refiner.checkRefinements(expr, condition)(evaluator) ) {
- case (map, (id, newTypes)) =>
- if (map contains id)
- map + (id -> map(id).intersect(newTypes))
- else
- map + (id -> newTypes)
- }
- }
-
- for (refiner <- refiners)
- refiner.refinePossibleTypes(refineMap.toList)
-
- refineMap.toList
- }
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerExecution.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerExecution.scala
deleted file mode 100644
index d41f1428c..000000000
--- a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerExecution.scala
+++ /dev/null
@@ -1,106 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon
-package synthesis.condabd
-package refinement
-
-import scala.collection.mutable.{ Map => MutableMap }
-import scala.collection.mutable.{ Set => MutableSet }
-
-import leon.purescala.Extractors._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.evaluators._
-import EvaluationResults._
-
-import insynth.leon.loader._
-import insynth.leon.{ LeonDeclaration => Declaration, _ }
-
-import _root_.insynth.util.logging.HasLogger
-
-class VariableRefinerExecution(variableDeclarations: Seq[Declaration],
- classMap: Map[Identifier, ClassType]) extends VariableRefiner with HasLogger {
-
- // map from identifier into a set of possible subclasses
- // currently only classes with no fields
- protected var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = MutableMap.empty
-
- // TODO use cd.knownDescendents?
- for (varDec <- variableDeclarations) {
- varDec match {
- case Declaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, IsTyped(Variable(id), AbstractClassType(cd, tps)))) =>
- variableRefinements += (id -> MutableSet(cd.knownDescendents.map(classDefToClassType(_, tps)): _*))
- case _ =>
- }
- }
-
- override def getPossibleTypes(id: Identifier) = variableRefinements(id).toSet
-
- override def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null) = {
- val variables = variablesOf(expr)
-
- // TODO can be extended with more variables (fix SOME values for other ones)
- if (variables.size == 1) {
- val variable = variables.head
- variable match {
- case oldId @ IsTyped(id, AbstractClassType(cd, tps)) // do not try to refine if we already know a single type is possible
- if variableRefinements(id).size > 1 =>
-
- assert(variableRefinements(id).map(_.classDef) subsetOf cd.knownDescendents.toSet)
-
- val optCases =
- for (cct <- variableRefinements(id)) yield cct match {
- case cct: CaseClassType if cct.fields.isEmpty =>
-
- val testValue = CaseClass(cct, Nil)
- val conditionToEvaluate = And(Not(expr), condition)
- fine("Execute condition " + conditionToEvaluate + " on variable " + id + " as " + testValue)
-
- evaluator.eval(conditionToEvaluate, Map(id -> testValue)) match {
- case Successful(BooleanLiteral(false)) =>
- fine("EvaluationSuccessful(false)")
- fine("Refining variableRefinements(id): " + variableRefinements(id))
- variableRefinements(id) -= cct
- fine("Refined variableRefinements(id): " + variableRefinements(id))
- Some(cct)
- case Successful(BooleanLiteral(true)) =>
- fine("EvaluationSuccessful(true)")
- None
- case m =>
- warning("Eval failed: " + m)
- None
- }
-
- case _ =>
- None
- }
-
- if (optCases.flatten.isEmpty)
- Nil
- else {
- finest("Returning: " + List((id, variableRefinements(id).toSet)))
- List((id, variableRefinements(id).toSet))
- }
- case _ =>
- fine("did not match for refinement " + variable)
- Nil
- }
- } else Nil
- }
-
- // inspect the expression if some refinements can be done
- def getIdAndClassDef(expr: Expr) = expr match {
- case CaseClassInstanceOf(classDef, Variable(id)) =>
- Some((id, classDef))
- case _ =>
- None
- }
-
- override def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])]) =
- for ((id, types) <- refinements)
- variableRefinements(id) &~= types
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerStructure.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerStructure.scala
deleted file mode 100644
index 22ab471e6..000000000
--- a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerStructure.scala
+++ /dev/null
@@ -1,64 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package refinement
-
-import scala.collection.mutable.{Map => MutableMap}
-import scala.collection.mutable.{Set => MutableSet}
-
-import leon._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.evaluators._
-
-import insynth.leon.loader._
-import insynth.leon.{ LeonDeclaration => Declaration, _ }
-
-import _root_.insynth.util.logging.HasLogger
-
-// each variable of super type can actually have a subtype
-// get sine declaration maps to be able to refine them
-class VariableRefinerStructure(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[Declaration],
- classMap: Map[Identifier, ClassType], reporter: Reporter) extends VariableRefiner with HasLogger {
-
- // map from identifier into a set of possible subclasses
- protected var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = MutableMap.empty
- for (varDec <- variableDeclarations) {
- varDec match {
- case Declaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, Variable(id))) =>
- variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
- case _ =>
- }
- }
-
- override def getPossibleTypes(id: Identifier) = variableRefinements(id).toSet
-
- override def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null) =
- // check for refinements
- getIdAndClassDef(expr) match {
- case Some(refinementPair @ (id, classType)) if variableRefinements(id).size > 1 =>
- fine("And now we have refinement type: " + refinementPair)
- fine("variableRefinements(id) before" + variableRefinements(id))
- variableRefinements(id) -= classMap(classType.id)
- fine("variableRefinements(id) after" + variableRefinements(id))
-
- List((id, variableRefinements(id).toSet))
- case _ =>
- Nil
- }
-
- // inspect the expression if some refinements can be done
- def getIdAndClassDef(expr: Expr) = expr match {
- case CaseClassInstanceOf(classDef, Variable(id)) =>
- Some((id, classDef))
- case _ =>
- None
- }
-
- override def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])]) =
- for ((id, types) <- refinements)
- variableRefinements(id) &~= types
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
deleted file mode 100644
index a32264395..000000000
--- a/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
+++ /dev/null
@@ -1,113 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon
-package synthesis.condabd
-package refinement
-
-import scala.collection.mutable.{ Map => MutableMap }
-import scala.collection.mutable.{ Set => MutableSet }
-
-import purescala.Extractors._
-import purescala.TypeTrees._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Definitions._
-import purescala.Common.{ Identifier, FreshIdentifier }
-import solvers._
-import synthesis.Problem
-import leon.evaluators._
-
-import insynth.leon.loader._
-import insynth.leon._
-
-import _root_.insynth.util.logging.HasLogger
-
-class VariableSolverRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[LeonDeclaration],
- classMap: Map[Identifier, ClassType], solverf: SolverFactory[Solver], reporter: Reporter)
- extends VariableRefinerStructure(directSubclassMap, variableDeclarations, classMap, reporter) with HasLogger {
-
- val solver = SimpleSolverAPI(solverf)
-
- override def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null) = {
- val variables = variablesOf(expr)
- if (variables.size == 1) {
- val variable = variables.head
- variable match {
- case oldId@IsTyped(id, AbstractClassType(cd, tps)) if variableRefinements(id).size > 1 =>
- assert(variableRefinements(id).map(_.classDef) subsetOf cd.knownDescendents.toSet)
- //val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
- val optCases = for (cct <- variableRefinements(id)) yield cct match {
- case cct : CaseClassType =>
- fine("testing variable " + id + " with condition " + condition)
- val toSat = And(condition, CaseClassInstanceOf(cct, Variable(id)))
-
- fine("checking satisfiability of: " + toSat)
- solver.solveSAT(toSat) match {
- case (Some(false), _) =>
- fine("variable cannot be of type " + cct)
- None
- case _ =>
- fine("variable can be of type " + cct)
- Some(cct)
- }
- case _ =>
- None
- }
-
- val cases = optCases.flatten
- variableRefinements(id) = variableRefinements(id) & cases.toSet
- assert(variableRefinements(id).size == cases.size)
-
- List((id, variableRefinements(id).toSet))
-
- case id =>
- fine("no id found for refinement that has potential refinements > 1")
- Nil
- }
- } else {
- fine("VariableSolverRefiner will not refine: more than one variable")
- Nil
- }
- }
-
- def refineProblem(p: Problem) = {
-
- val newAs = p.as.map {
- case oldId @ IsTyped(id, act : AbstractClassType) =>
-
- val optCases = for (cct <- act.knownCCDescendents) yield {
- val toSat = And(p.pc, CaseClassInstanceOf(cct, Variable(id)))
-
- val isImplied = solver.solveSAT(toSat) match {
- case (Some(false), _) => true
- case _ => false
- }
-
- println(isImplied)
-
- if (!isImplied) {
- Some(cct)
- } else {
- None
- }
- }
-
- val cases = optCases.flatten
-
- println(id)
- println(cases)
-
- if (cases.size == 1) {
- // id.setType(CaseClassType(cases.head))
- FreshIdentifier(oldId.name).setType(cases.head)
- } else oldId
-
- case id => id
- }
-
- p.copy(as = newAs)
- }
-
- override def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])]) = Unit
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
deleted file mode 100644
index 534b99d74..000000000
--- a/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ /dev/null
@@ -1,92 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.synthesis.condabd
-package rules
-
-import leon.purescala.Trees._
-import leon.purescala.Common._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps._
-import leon.purescala.Extractors._
-import leon.purescala.Definitions._
-import leon.synthesis._
-import leon.solvers._
-import leon.evaluators.CodeGenEvaluator
-
-import examples.InputExamples._
-import evaluation._
-
-import leon.StopwatchCollections
-
-case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abduction synthesis (two phase).") {
- def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
-
- p.xs match {
- case givenVariable :: Nil =>
- List(new RuleInstantiation(p, this, SolutionBuilder.none, "Condition abduction") {
- def apply(sctx: SynthesisContext): RuleApplicationResult = {
- try {
- val solver = SolverFactory(() => sctx.newSolver.setTimeout(500L))
- val program = sctx.program
- val reporter = sctx.reporter
-
- val desiredType = givenVariable.getType
- val fd = sctx.functionContext.get
- val tfd = fd.typed(fd.tparams.map(_.tp))
-
- // temporary hack, should not mutate FunDef
- val oldPostcondition = fd.postcondition
-
- try {
- val freshResID = FreshIdentifier("result").setType(tfd.returnType)
- val freshResVar = Variable(freshResID)
-
- val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
- def getInputExamples = {
- () =>
- //getDataGenInputExamples(sctx.context, sctx.program, codeGenEval, p,
- // 100, 6000, Some(p.as)) ++
- getDataGenInputExamplesRandomIntegers(sctx.context, sctx.program, codeGenEval, p,
- 100, 6000, Some(p.as)
- // bound the random geenerator
- ,10)
- }
-
- val evaluationStrategy = new CodeGenEvaluationStrategy(program, tfd, sctx.context, 5000)
- fd.postcondition = Some((givenVariable, p.phi))
-
- val synthesizer = new SynthesizerForRuleExamples(
- solver, program, desiredType, tfd, p, sctx, evaluationStrategy,
- 20, 1,
- reporter = reporter,
- introduceExamples = getInputExamples,
- numberOfTestsInIteration = 25,
- numberOfCheckInIteration = 2
- )
-
- synthesizer.synthesize match {
- case EmptyReport => RuleApplicationImpossible
- case fr@FullReport(resFunDef, _) =>
- println(fr.summaryString)
- println("Compilation time: " + StopwatchCollections.get("Compilation").getMillis)
- RuleSuccess(
- Solution(BooleanLiteral(true), Set.empty, Tuple(Seq(resFunDef.body.get))),
- isTrusted = !synthesizer.verifier.isTimeoutUsed
- )
- }
- } catch {
- case e: Throwable =>
- sctx.reporter.warning("Condition abduction crashed: " + e.getMessage)
- e.printStackTrace
- RuleApplicationImpossible
- } finally {
- fd.postcondition = oldPostcondition
- }
- }
- }
- })
- case _ =>
- Nil
- }
- }
-}
diff --git a/src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala b/src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
deleted file mode 100644
index ffcfe66c5..000000000
--- a/src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
+++ /dev/null
@@ -1,125 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon
-package synthesis
-package condabd
-package verification
-
-import solvers._
-import purescala.Common._
-import purescala.Trees._
-import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
-
-import _root_.insynth.util.logging._
-
-abstract class AbstractVerifier(solverf: SolverFactory[Solver with IncrementalSolver with TimeoutSolver], p: Problem, synthInfo: SynthesisInfo)
- extends HasLogger {
-
- val solver = solverf.getNewSolver
-
- import SynthesisInfo.Action._
-
- def analyzeFunction(tfd: TypedFunDef) = {
- synthInfo.start(Verification)
- fine("Analyzing function: " + tfd)
-
- // create an expression to verify
- val theExpr = generateInductiveVerificationCondition(tfd, tfd.body.get)
-
- solver.push
- val valid = checkValidity(theExpr)
- val map = solver.getModel
- solver.pop()
-
- // measure time
- synthInfo.end
- fine("Analysis of " + theExpr + ",took :" + synthInfo.last)
- (valid, map)
- }
-
- def analyzeFunction(tfd: TypedFunDef, body: Expr) = {
- synthInfo.start(Verification)
-
- // create an expression to verify
- val theExpr = generateInductiveVerificationCondition(tfd, body)
-
- solver.push
- val valid = checkValidity(theExpr)
- val map = solver.getModel
- solver.pop()
-
- // measure time
- synthInfo.end
- fine("Analysis of " + theExpr + ",took :" + synthInfo.last)
- (valid, map)
- }
-
- protected def generateInductiveVerificationCondition(tfd: TypedFunDef, body: Expr) = {
-
- // replace recursive calls with fresh variables
- case class Replacement(id: Identifier, exprReplaced: FunctionInvocation) {
- def getMapping: Map[Expr, Expr] = {
- val tfd = exprReplaced.tfd
- val pairList = (Variable(tfd.postcondition.get._1), id.toVariable) ::
- (tfd.params.map(_.toVariable).toList zip exprReplaced.args)
- pairList.toMap
- }
- }
-
- // traverse the expression and check (and replace) recursive calls
- var isThereARecursiveCall = false
- var replacements = List[Replacement]()
-
- def replaceRecursiveCalls(expr: Expr) = expr match {
- case funInv@FunctionInvocation(`tfd`, args) => {
- isThereARecursiveCall = true
- val inductId = FreshIdentifier("induct", true).setType(tfd.returnType)
- replacements :+= Replacement(inductId, funInv)
- Some(inductId.toVariable)
- }
- case _ => None
- }
-
- val newBody = postMap(replaceRecursiveCalls)(body)
-
- // build the verification condition
- val resFresh = FreshIdentifier("result", true).setType(newBody.getType)
- val (id, post) = tfd.postcondition.get
- val bodyAndPost =
- Let(
- resFresh, newBody,
- replace(Map(Variable(id) -> resFresh.toVariable), matchToIfThenElse(post))
- )
-
- val precondition = if( isThereARecursiveCall ) {
- And( tfd.precondition.get :: replacements.map( r => replace(r.getMapping, post)) )
- } else
- tfd.precondition.get
-// val bodyAndPost =
-// Let(
-// resFresh, newBody,
-// replace(Map(p.xs.head.toVariable -> resFresh.toVariable), matchToIfThenElse(p.phi))
-// )
-//
-// val precondition = if( isThereARecursiveCall ) {
-// And( p.pc :: replacements.map( r => replace(r.getMapping, p.phi)) )
-// } else
-// p.pc
-
- val withPrec =
- Implies(matchToIfThenElse(precondition), bodyAndPost)
-
- info("Generated verification condition: " + withPrec)
- withPrec
- }
-
- def checkValidity(expression: Expr): Boolean
-
- def checkValidityNoMod(expression: Expr): Boolean
-
- def checkSatisfiabilityNoMod(expression: Expr): Boolean
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala b/src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
deleted file mode 100644
index d8be887b4..000000000
--- a/src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
+++ /dev/null
@@ -1,80 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon
-package synthesis
-package condabd
-package verification
-
-import solvers._
-import purescala.Common._
-import purescala.Trees._
-import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
-import SynthesisContext.SynthesisSolver
-
-import _root_.insynth.util.logging._
-
-class RelaxedVerifier(solverf: SolverFactory[SynthesisSolver], p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
- extends AbstractVerifier(solverf, p, synthInfo) with HasLogger {
-
- var _isTimeoutUsed = false
-
- def isTimeoutUsed = _isTimeoutUsed
-
- override def checkValidity(expression: Expr) = {
- fine("Checking validity - assertCnstr: " + Not(expression))
- solver.assertCnstr(Not(expression))
- val solverCheckResult = solver.check
- fine("Solver said " + solverCheckResult + " for " + expression)
- solverCheckResult match {
- case Some(true) =>
- false
- case Some(false) =>
- true
- case None =>
- _isTimeoutUsed = true
- warning("Interpreting None (timeout) as evidence for validity.")
- true
- }
- }
-
- override def checkValidityNoMod(expression: Expr) = {
- solver.push
- fine("Checking validityNoMod - assertCnstr: " + Not(expression))
- solver.assertCnstr(Not(expression))
- val solverCheckResult = solver.check
- fine("Solver said " + solverCheckResult + " for " + expression)
- solver.pop()
- solverCheckResult match {
- case Some(true) =>
- fine("And the model is " + solver.getModel)
- false
- case Some(false) =>
- true
- case None =>
- _isTimeoutUsed = true
- warning("Interpreting None (timeout) as evidence for validity.")
- true
- }
- }
-
- override def checkSatisfiabilityNoMod(expression: Expr) = {
- solver.push
- fine("Checking checkSatisfiabilityNoMod - assertCnstr: " + expression)
- solver.assertCnstr(expression)
- val solverCheckResult = solver.check
- fine("Solver said " + solverCheckResult + " for " + expression)
- solver.pop()
- solverCheckResult match {
- case Some(true) =>
- true
- case Some(false) =>
- false
- case None =>
- false
- }
- }
-
-}
diff --git a/src/main/scala/leon/synthesis/condabd/verification/Verifier.scala b/src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
deleted file mode 100644
index f3bde5039..000000000
--- a/src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
+++ /dev/null
@@ -1,73 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon
-package synthesis
-package condabd
-package verification
-
-import solvers._
-import purescala.Common._
-import purescala.Trees._
-import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
-import SynthesisContext.SynthesisSolver
-
-import _root_.insynth.util.logging._
-
-class Verifier(solverf: SolverFactory[SynthesisSolver], p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
- extends AbstractVerifier(solverf, p, synthInfo) with HasLogger {
-
- import SynthesisInfo.Action._
-
- override def checkValidity(expression: Expr) = {
- solver.assertCnstr(Not(expression))
- val solverCheckResult = solver.check
- fine("Solver said " + solverCheckResult + " for " + expression)
- solverCheckResult match {
- case Some(true) =>
- false
- case Some(false) =>
- true
- case None =>
- warning("Interpreting None (timeout) as evidence for invalidity.")
- false
- }
- }
-
- override def checkValidityNoMod(expression: Expr) = {
- solver.push
- solver.assertCnstr(Not(expression))
- val solverCheckResult = solver.check
- fine("Solver said " + solverCheckResult + " for " + expression)
- solver.pop()
- solverCheckResult match {
- case Some(true) =>
- fine("And the model is " + solver.getModel)
- false
- case Some(false) =>
- true
- case None =>
- warning("Interpreting None (timeout) as evidence for invalidity.")
- false
- }
- }
-
- override def checkSatisfiabilityNoMod(expression: Expr) = {
- solver.push
- solver.assertCnstr(expression)
- val solverCheckResult = solver.check
- fine("Solver said " + solverCheckResult + " for " + expression)
- solver.pop()
- solverCheckResult match {
- case Some(true) =>
- true
- case Some(false) =>
- false
- case None =>
- false
- }
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/EvaluationTest.scala b/src/test/scala/leon/test/condabd/EvaluationTest.scala
deleted file mode 100644
index 0f3fd9dd9..000000000
--- a/src/test/scala/leon/test/condabd/EvaluationTest.scala
+++ /dev/null
@@ -1,331 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-
-import org.scalatest.FunSuite
-import org.scalatest.matchers.ShouldMatchers._
-
-import leon._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import java.io.{ BufferedWriter, FileWriter, File }
-import leon.evaluators.CodeGenEvaluator
-import leon.purescala.TreeOps
-import leon.purescala.Common._
-import leon.codegen.CodeGenParams
-import leon.purescala.TypeTrees._
-import leon.evaluators.EvaluationResults._
-
-import leon.synthesis.condabd.examples._
-import leon.synthesis.condabd.evaluation.CodeGenEvaluationStrategy
-import leon.synthesis.condabd.ranking.Candidate
-import leon.synthesis.condabd.insynth.reconstruction.Output
-
-import util.Scaffold
-
-// TODO codegen evaluator params should be used but not yet in master
-class EvaluationTest extends FunSuite {
-
- import Scaffold._
-
- val mergeSortWithTwoExamples = """
- import leon.lang._
-
- object MergeSort {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class PairAbs
- case class Pair(fst: List, snd: List) extends PairAbs
-
- def contents(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x, xs) => contents(xs) ++ Set(x)
- }
-
- def isSorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x, xs) => xs match {
- case Nil() => true
- case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
- }
- }
-
- def size(list: List): Int = list match {
- case Nil() => 0
- case Cons(x, xs) => 1 + size(xs)
- }
-
- def splithelper(aList: List, bList: List, n: Int): Pair = {
- if (n <= 0) Pair(aList, bList)
- else
- bList match {
- case Nil() => Pair(aList, bList)
- case Cons(x, xs) => splithelper(Cons(x, aList), xs, n - 1)
- }
- } ensuring (res =>
- contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd)
- &&
- size(aList) + size(bList) == size(res.fst) + size(res.snd)
- )
-
- def split(list: List): Pair = {
- splithelper(Nil(), list, 2)
- } ensuring (res =>
- contents(list) == contents(res.fst) ++ contents(res.snd)
- &&
- size(list) == size(res.fst) + size(res.snd)
- )
-
- def merge(aList: List, bList: List): List = {
- require(isSorted(aList) && isSorted(bList))
- bList match {
- case Nil() => aList
- case Cons(x, xs) =>
- aList match {
- case Nil() => bList
- case Cons(y, ys) =>
- if (y < x)
- Cons(y, merge(ys, bList))
- else
-
- Cons(x, merge(aList, xs))
- }
- }
- } ensuring (res => contents(res) ==
- contents(aList) ++ contents(bList) && isSorted(res) &&
- size(res) == size(aList) + size(bList)
- )
-
- def isEmpty(list: List): Boolean = list match {
- case Nil() => true
- case Cons(x, xs) => false
- }
-
- def sort(list: List): List = choose {
- (res: List) =>
- contents(res) == contents(list) && isSorted(res) && size(res) == size(list)
- } ensuring ( res => contents(res) == contents(list) && isSorted(res) && size(res) == size(list))
-
- def testFun1(list: List) = {
- if (isEmpty(list))
- list
- else
- if (isSorted(list))
- list
- else
- splithelper(Nil(), list, size(list)).fst
- }
-
- def testFun2(list: List) = {
- if (isEmpty(list))
- list
- else
- if (isSorted(list))
- list
- else
- merge(sort(split(list).fst), sort(split(list).snd))
- }
- }
- """
-
- test("codegen strategy") {
-
- for ((sctx, funDef, problem) <- forProgram(mergeSortWithTwoExamples)) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- expectResult(1) { problem.xs.size }
- val resultVariable = problem.xs.head
-
- val codeGenEval = new CodeGenEvaluator(sctx.context, program)
- def inputExamples =
- InputExamples.getDataGenInputExamples(sctx.context, program, codeGenEval, problem,
- 20, 2000, Some(arguments)).map(Example(_))
-
- import TreeOps._
- def replaceFun(expr: Expr) = expr match {
- case Variable(id) if id.name == "list" =>
- Some(Variable(arguments.head))
- // case FunctionInvocation(`funDef`, args) =>
- // FunctionInvocation(funDef, )
- case _ => None
- }
-
- val body1 =
- postMap(replaceFun)(
- program.definedFunctions.find(_.id.name == "testFun1").get.body.get)
-
- val body2 =
- postMap(replaceFun)(
- program.definedFunctions.find(_.id.name == "testFun2").get.body.get)
-
- val evaluationStrategy = new CodeGenEvaluationStrategy(program, funDef.typed, sctx.context, 500)
-
- val candidates = IndexedSeq(body1, body2) map (b => Output(b, 0))
-
- val ranker = evaluationStrategy.getRanker(candidates, identity, inputExamples)
- val exampleRunner = evaluationStrategy.exampleRunner
-
- val eval1 = (for (ind <- 0 until inputExamples.size) yield {
- val res = exampleRunner.evaluate(0, ind)
- (res, exampleRunner.examples(ind))
- })
-
- val eval2 = (for (ind <- 0 until inputExamples.size) yield {
- val res = exampleRunner.evaluate(1, ind)
- (res, exampleRunner.examples(ind))
- })
-
- val message = "Examples: " + inputExamples.mkString(", ")
- val eval1message = "Evaluation of " + body1 + " yielded: " + eval1.mkString("\n")
- val eval2message = "Evaluation of " + body2 + " yielded: " + eval2.mkString("\n")
- assert(inputExamples.size == eval2.count(_._1), message + " " + eval2message)
- assert(inputExamples.size > eval1.count(_._1), message + " " + eval1message)
- }
- }
-
- test("codegen evaluator") {
-
- for ((sctx, funDef, problem) <- forProgram(mergeSortWithTwoExamples)) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- expectResult(1) { problem.xs.size }
- val resultVariable = problem.xs.head
-
- val codeGenEval = new CodeGenEvaluator(sctx.context, program)
- def inputExamples =
- InputExamples.getDataGenInputExamples(sctx.context, program, codeGenEval, problem,
- 20, 2000, Some(arguments)).map(Example(_))
-
- import TreeOps._
- def replaceFun(expr: Expr) = expr match {
- case Variable(id) if id.name == "list" =>
- Some(Variable(arguments.head))
- case _ => None
- }
-
- val body1 =
- postMap(replaceFun)(
- program.definedFunctions.find(_.id.name == "testFun1").get.body.get)
- val body2 =
- postMap(replaceFun)(
- program.definedFunctions.find(_.id.name == "testFun2").get.body.get)
-
- // evaluate expressions with let
- {
- def formExecutable(expr: Expr) = {
-
- import TreeOps._
-
- val newFunId = FreshIdentifier("tempIntroducedFunction")
- val newFun = new FunDef(newFunId, Nil, funDef.returnType, funDef.params)
- newFun.precondition = funDef.precondition
- newFun.postcondition = funDef.postcondition
-
- def replaceFunDef(expr: Expr) = expr match {
- case FunctionInvocation(`funDef`, args) =>
- Some(FunctionInvocation(newFun.typed, args))
- case _ => None
- }
- val newBody = postMap(replaceFunDef)(expr)
-
- newFun.body = Some(newBody)
-
- assert(expr.getType != Untyped)
- val resFresh = FreshIdentifier("result") //.setType(expr.getType)
- resFresh.setType(newBody.getType)
-
- val (id, post) = newFun.postcondition.get
- // body can contain (self-)recursive calls
- (
- Let(resFresh, newBody,
- replace(Map(Variable(id) -> Variable(resFresh)),
- matchToIfThenElse(post))),
- newFun)
- }
-
- val pairs = List(body1, body2) map (formExecutable(_))
- val candidates = pairs map (_._1)
-
- val params = CodeGenParams(maxFunctionInvocations = 500, checkContracts = true)
-
- val evaluator = new CodeGenEvaluator(sctx.context,
- program.copy(modules = ModuleDef(FreshIdentifier("new"), pairs.map(_._2)) :: program.modules)
- , params)
-
- val eval1 = (for (ind <- 0 until inputExamples.size) yield {
- val res = evaluator.eval(candidates(0), inputExamples(ind).map)
- (res, inputExamples(ind))
- })
-
- val eval2 = (for (ind <- 0 until inputExamples.size) yield {
- val res = evaluator.eval(candidates(1), inputExamples(ind).map)
- (res, inputExamples(ind))
- })
-
- val message = "Examples: " + inputExamples.mkString(", ")
- val eval1message = "Evaluation of " + body1 + " yielded: " + eval1.mkString("\n")
- val eval2message = "Evaluation of " + body2 + " yielded: " + eval2.mkString("\n")
- assert(inputExamples.size == eval2.count(_._1 == Successful(BooleanLiteral(true))), message + " " + eval2message)
- assert(inputExamples.size > eval1.count(_._1 == Successful(BooleanLiteral(true))), message + " " + eval1message)
- }
-
- // evaluate expressions without let
- {
- def formExecutable(expr: Expr) = {
-
- import TreeOps._
-
- val newFunId = FreshIdentifier("tempIntroducedFunction")
- val newFun = new FunDef(newFunId, Nil, funDef.returnType, funDef.params)
- newFun.precondition = funDef.precondition
- newFun.postcondition = funDef.postcondition
-
- def replaceFunDef(expr: Expr) = expr match {
- case FunctionInvocation(`funDef`, args) =>
- Some(FunctionInvocation(newFun.typed, args))
- case _ => None
- }
- val newBody = postMap(replaceFunDef)(expr)
-
- newFun.body = Some(newBody)
-
- assert(expr.getType != Untyped)
- val resFresh = FreshIdentifier("result") //.setType(expr.getType)
- resFresh.setType(newBody.getType)
-
- // body can contain (self-)recursive calls
- (newBody, newFun)
- }
-
- val pairs = List(body1, body2) map (formExecutable(_))
- val candidates = pairs map (_._1)
-
- val params = CodeGenParams(maxFunctionInvocations = 500, checkContracts = true)
-
- val evaluator = new CodeGenEvaluator(sctx.context,
- program.copy(modules = ModuleDef(FreshIdentifier("new"), pairs.map(_._2)) :: program.modules)
- , params)
-
- val eval1 = (for (ind <- 0 until inputExamples.size) yield {
- val res = evaluator.eval(candidates(0), inputExamples(ind).map)
- (res, inputExamples(ind))
- })
-
- val eval2 = (for (ind <- 0 until inputExamples.size) yield {
- val res = evaluator.eval(candidates(1), inputExamples(ind).map)
- (res, inputExamples(ind))
- })
-
- val message = "Examples: " + inputExamples.mkString(", ")
- val eval1message = "Evaluation of " + body1 + " yielded: " + eval1.mkString("\n")
- val eval2message = "Evaluation of " + body2 + " yielded: " + eval2.mkString("\n")
-// assert(inputExamples.size == eval2.count(_._1 == Successful(BooleanLiteral(true))), message + " " + eval2message)
-// assert(inputExamples.size > eval1.count(_._1 == Successful(BooleanLiteral(true))), message + " " + eval1message)
- }
- }
- }
-}
diff --git a/src/test/scala/leon/test/condabd/VerifierTest.scala b/src/test/scala/leon/test/condabd/VerifierTest.scala
deleted file mode 100644
index 395417e15..000000000
--- a/src/test/scala/leon/test/condabd/VerifierTest.scala
+++ /dev/null
@@ -1,159 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-
-import org.junit.Assert._
-import org.junit._
-import org.scalatest._
-import org.scalatest.matchers._
-
-import leon.synthesis.condabd.insynth.leon.loader.LeonLoader
-import leon.synthesis.condabd.verification._
-
-import leon.purescala._
-import leon.evaluators._
-import leon.solvers._
-import leon.purescala.Trees._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.synthesis.Problem
-
-import util._
-
-class VerifierTest extends FunSpec {
-
- import Utils._
- import Scaffold._
-
- val lesynthTestDir = "testcases/condabd/test/lesynth"
-
- def getPostconditionFunction(problem: Problem) = {
- (list: Iterable[Identifier]) => {
- (problem.phi /: list) {
- case ((res, newId)) =>
- (res /: problem.as.find(_.name == newId.name)) {
- case ((res, oldId)) =>
- TreeOps.replace(Map(Variable(oldId) -> Variable(newId)), res)
- }
- }
- }
- }
-
- describe("Concrete verifier: ") {
- val testCaseFileName = lesynthTestDir + "/ListConcatVerifierTest.scala"
-
- val problems = forFile(testCaseFileName)
- assert(problems.size == 1)
-
- for ((sctx, funDef, problem) <- problems) {
-
- val timeoutSolver = SolverFactory(() => sctx.newSolver.setTimeout(2000L))
-
-
- val getNewPostcondition = getPostconditionFunction(problem)
-
- describe("A Verifier") {
- it("should verify first correct concat body") {
- val newFunDef = getFunDefByName(sctx.program, "goodConcat1")
- funDef.body = newFunDef.body
-
- expectResult(1) { problem.xs.size }
- funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.params.map(_.id))))
- funDef.precondition = Some(BooleanLiteral(true))
-
- val verifier = new Verifier(timeoutSolver, problem)
-
- assert( verifier.analyzeFunction(funDef.typed)._1 )
- verifier.solver.free()
- }
-
- it("should verify 2nd correct concat body") {
- val newFunDef = getFunDefByName(sctx.program, "goodConcat2")
- funDef.body = newFunDef.body
-
- expectResult(1) { problem.xs.size }
- funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.params.map(_.id))))
- funDef.precondition = Some(BooleanLiteral(true))
-
- val verifier = new Verifier(timeoutSolver, problem)
-
- assert( verifier.analyzeFunction(funDef.typed)._1 )
- verifier.solver.free()
- }
-
- it("should not verify an incorrect concat body") {
- val newFunDef = getFunDefByName(sctx.program, "badConcat1")
- funDef.body = newFunDef.body
-
- expectResult(1) { problem.xs.size }
- funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.params.map(_.id))))
- funDef.precondition = Some(BooleanLiteral(true))
-
- val verifier = new Verifier(timeoutSolver, problem)
-
- assert( ! verifier.analyzeFunction(funDef.typed)._1 )
- verifier.solver.free()
- }
- }
- }
- }
-
- def getPreconditionFunction(problem: Problem) = {
- (list: Iterable[Identifier]) => {
- (problem.pc /: list) {
- case ((res, newId)) =>
- (res /: problem.as.find(_.name == newId.name)) {
- case ((res, oldId)) =>
- TreeOps.replace(Map(Variable(oldId) -> Variable(newId)), res)
- }
- }
- }
- }
-
- describe("Relaxed verifier: ") {
- val testCaseFileName = lesynthTestDir + "/BinarySearchTree.scala"
-
- val problems = forFile(testCaseFileName)
- assert(problems.size == 1)
-
- for ((sctx, funDef, problem) <- problems) {
-
- val timeoutSolver = SolverFactory(() => sctx.newSolver.setTimeout(1000L))
-
- val getNewPostcondition = getPostconditionFunction(problem)
- val getNewPrecondition = getPreconditionFunction(problem)
-
- describe("A RelaxedVerifier on BST") {
- it("should verify a correct member body") {
- val newFunDef = getFunDefByName(sctx.program, "goodMember")
- funDef.body = newFunDef.body
-
- expectResult(1) { problem.xs.size }
- funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.params.map(_.id))))
- funDef.precondition = Some(getNewPrecondition(newFunDef.params.map(_.id)))
-
- val verifier = new RelaxedVerifier(timeoutSolver, problem)
-
- assert( verifier.analyzeFunction(funDef.typed)._1 )
- verifier.solver.free()
- }
-
- it("should not verify an incorrect member body") {
- val newFunDef = getFunDefByName(sctx.program, "badMember")
- funDef.body = newFunDef.body
-
- expectResult(1) { problem.xs.size }
- funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.params.map(_.id))))
- funDef.precondition = Some(getNewPrecondition(newFunDef.params.map(_.id)))
-
- val verifier = new Verifier(timeoutSolver, problem)
-
- assert( verifier.analyzeFunction(funDef.typed)._1 )
- verifier.solver.free()
- }
- }
- }
-
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala b/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
deleted file mode 100644
index 6a629eb26..000000000
--- a/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
+++ /dev/null
@@ -1,417 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-
-import leon.synthesis.condabd.insynth.InSynth
-import leon.synthesis.condabd.insynth.leon._
-import leon.synthesis.condabd.insynth.leon.loader._
-import leon.synthesis.condabd.insynth.reconstruction.codegen._
-import leon.synthesis.condabd.insynth.reconstruction.Output
-
-import _root_.insynth.engine._
-import _root_.insynth.reconstruction._
-import _root_.insynth.reconstruction.{ stream => lambda }
-import _root_.insynth.reconstruction.stream.{ OrderedStreamFactory }
-
-import _root_.leon._
-import _root_.leon.purescala._
-import _root_.leon.purescala.Definitions._
-import _root_.leon.purescala.Common._
-import _root_.leon.purescala.TypeTrees._
-import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
-import _root_.insynth.util.format._
-import _root_.insynth.util._
-
-import leon.synthesis.condabd.refinement._
-
-import org.junit.{ Test, Ignore }
-import org.junit.Assert._
-import org.scalatest.junit.JUnitSuite
-
-import util._
-
-import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
-
-// this suggests we should refactor an enumerator class
-class EnumeratorTest extends JUnitSuite {
-
- import CommonDeclarations._
- import CommonProofTrees._
- import CommonLambda._
- import DeclarationFactory._
-
- import Scaffold._
-
- import ProofTreeOperations.StringNode
-
- val lesynthTestDir = "testcases/condabd/test/lesynth/"
-
- val transformer = Streamer.apply _
- val codegen = (new CodeGenerator).apply _
-
- def assertWeight(pair: Output) =
- assertEquals("Node " + pair.getSnippet + " does not have size " + pair.getWeight,
- TreeOps.formulaSize(pair.getSnippet).toFloat, pair.getWeight, 0f)
-
- def assertTake(insynth: InSynth, num: Int) = {
- val result = insynth.getExpressions take num
-
- // TODO this should be applied
-// def message(pos: Int) = "Part of the resulting stream: " + result.slice(pos - 10, pos + 10).mkString("\n")
-//
-// for (ind <- 0 until result.size)
-// assertWeight(result(ind))
-// for (ind <- 0 until result.size - 1)
-// assertTrue("Weights are not in non-decreasing order.\n" + "At position " + ind + "\n" + message(ind),
-// result(ind).getWeight <= result(ind + 1).getWeight)
-
- result.map(_.getSnippet)
- }
-
- def assertNoDuplicity(extractorResults: Stream[(lambda.Node, Float)]) = {
- // note that duplicates may exist in generated code (e.g. because coercions), but should not before that
- val duplicityMap = (Map[lambda.Node, Set[(lambda.Node, Float)]]() /: extractorResults) {
- (resMap, pair) =>
- val snippet = pair._1
- resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
- }
-
- lazy val duplicityMessage =
- for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) yield
- ("Key: " + key) + ("\nValues: " + value.mkString("\n"))
-
- assertTrue(
- "There are some duplications in generated code:\n" + duplicityMessage,
- duplicityMap.filter(_._2.size > 1).isEmpty
- )
- }
-
- // note, refines first argument
- def refineListVariable(program: Program, funDef: FunDef,
- loader: LeonLoader, allDeclarations: List[LeonDeclaration], reporter: Reporter) = {
- val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
- get.asInstanceOf[CaseClassDef]
- val listVal = funDef.params.head.toVariable
-
- val variableRefiner =
- new VariableRefinerStructure(loader.directSubclassesMap,
- loader.variableDeclarations, loader.classMap, reporter)
-
- val (refined, newDeclarations) =
- variableRefiner.refine(
- CaseClassInstanceOf(CaseClassType(nilAbstractClassDef, Nil), listVal), BooleanLiteral(true), allDeclarations)
- assertTrue(refined)
- assert(allDeclarations.size + 2 == newDeclarations.size)
-
- val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
- newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
- assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "tail"))
- assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "a"))
-
- newDeclarations
- }
-
- @Test
- def testAddressesWithRefinementProofTree {
-
- for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val inSynth = new InSynth(loader, resultVariable.getType, true)
- val allDeclarations = inSynth.getAllDeclarations
-
- val newDeclarations = refineListVariable(program, funDef, loader, allDeclarations, sctx.reporter)
-
- val builder = new InitialEnvironmentBuilder(newDeclarations)
- val solver = inSynth.solver
- val solution = solver.getProofTree(builder)
-
- assertTrue(
- ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
- ProofTreeOperations.checkInhabitants(solution,
- StringNode("AddressBook", Set(
- StringNode("[Cons=>List]", Set(StringNode("Cons")))
- ,
- StringNode("pers", Set(StringNode("makeAddressBook")))
- ))
- ))
- assertTrue(
- ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
- ProofTreeOperations.checkInhabitants(solution,
- StringNode("addToPers", Set(
- StringNode("makeAddressBook", Set(
- StringNode("l.tail", Set())
- ))
- ,
- StringNode("a", Set( ))
- ))
- ))
- assertTrue(
- ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
- ProofTreeOperations.checkInhabitants(solution,
- StringNode("addToBusiness", Set(
- StringNode("makeAddressBook", Set(
- StringNode("l.tail", Set())
- ))
- ,
- StringNode("a", Set( ))
- ))
- ))
- assertTrue(
- ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
- ProofTreeOperations.checkInhabitants(solution,
- StringNode("addToBusiness", Set(
- StringNode("makeAddressBook", Set(
- StringNode("l.tail", Set())
- ))
- ,
- StringNode("l.a", Set( ))
- ))
- ))
- }
- }
-
- @Test
- def testAddressesWithRefinementSnippets {
-
- for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
- val reporter = sctx.reporter
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val newDeclarations = refineListVariable(program, funDef, loader, loader.load, reporter)
- val inSynth = new InSynth(newDeclarations, resultVariable.getType, true)
-
- val extractedSnipptes = assertTake(inSynth, 1000)
-
- val message = "Extracted: " + extractedSnipptes.size + "\n" +
- (for (output <- extractedSnipptes)
- yield "%20s" format output).mkString("\n")
-
- val expectedSnipptes = List(
- "AddressBook(Nil, l)",
- "makeAddressBook(l)",
- "addToPers(AddressBook(l, l), l.a)",
- "addToBusiness(makeAddressBook(l), l.a)"
- )
-
- for (snippet <- expectedSnipptes)
- assertTrue(snippet + " not found in extracted. results:\n" + message,
- extractedSnipptes.exists(_.toString == snippet.toString)
- )
- }
- }
-
- @Test
- def testAddressesMergeWithRefinementSnippets {
-
- for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "AddressesMergeAddressBooks.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
- val reporter = sctx.reporter
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val inSynth = new InSynth(loader.load, resultVariable.getType, true)
-
- val extractedSnipptes = assertTake(inSynth, 15000)
-
- val message = "Extracted: " + extractedSnipptes.size + "\n" +
- (for (output <- extractedSnipptes)
- yield "%20s" format output).mkString("\n")
-
- val expectedSnipptes = List(
- "AddressBook(ab1.pers, ab2.business)",
- "makeAddressBook(ab1.pers)",
- "AddressBook(merge(ab1.business, ab2.business), merge(ab2.pers, ab1.pers))"
- )
-
- for (snippet <- expectedSnipptes)
- assertTrue(snippet + " not found in extracted. results:\n" + message,
- extractedSnipptes.exists(_.toString == snippet.toString)
- )
- }
- }
-
- @Test
- def testListConcatWithRefinementSnippets {
-
- for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "ListConcat.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
- val reporter = sctx.reporter
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val newDeclarations = refineListVariable(program, funDef, loader, loader.load, reporter)
-
- val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
- newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
- assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l1.tail"))
- assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l1.head"))
-
- val inSynth = new InSynth(newDeclarations, resultVariable.getType, true)
-
- val extractedSnipptes = assertTake(inSynth, 1000)
-
- val message = "Extracted: " + extractedSnipptes.size + "\n" +
- (for (output <- extractedSnipptes)
- yield "%20s" format output).mkString("\n")
-
- val expectedSnipptes = List(
- "concat(Nil(), l1)",
- "Cons(l1.head, Nil())",
- "Cons(l1.head, concat(l1.tail, l2))"
- )
-
- for (snippet <- expectedSnipptes)
- assertTrue(snippet + " not found in extracted. results:\n" + message,
- extractedSnipptes.exists(_.toString == snippet.toString)
- )
-
- }
- }
-
- @Test
- def testAddressesWithRefinementBooleanSnippets {
-
- for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
- val reporter = sctx.reporter
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val newDeclarations = refineListVariable(program, funDef, loader, loader.load, reporter)
-
- val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
- newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
- assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
- assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
- assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName == "l"))
-
- val inSynth = new InSynth(newDeclarations, BooleanType, true)
-
- val extractedSnipptes = assertTake(inSynth, 5000)
-
- val message = "Extracted: " + extractedSnipptes.size + "\n" +
- (for (output <- extractedSnipptes)
- yield "%20s" format output).mkString("\n")
-
- val expectedSnipptes = List(
- // FIXME!
- // this one is harder to get since it has coercion for l
-// "allBusiness(AddressBook(Nil, l).pers)",
-// "allBusiness(AddressBook(Nil, l.tail).pers)",
- "allBusiness(makeAddressBook(l).business)",
- "allBusiness(l.tail)",
- "allPrivate(addToBusiness(makeAddressBook(l), l.a).pers)"
- )
-
- for (snippet <- expectedSnipptes)
- assertTrue(snippet + " not found in extracted. results:\n" + message,
- extractedSnipptes.exists(_.toString == snippet.toString)
- )
- }
- }
-
- @Test
- def testAddressesWithRefinementBooleanProofTree {
-
- for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val inSynth = new InSynth(loader, BooleanType, true)
- val allDeclarations = inSynth.getAllDeclarations
-
- val newDeclarations = refineListVariable(program, funDef, loader, allDeclarations, sctx.reporter)
-
- val builder = new InitialEnvironmentBuilder(newDeclarations)
- val solver = inSynth.solver
- val solution = solver.getProofTree(builder)
-
- assertTrue(
- ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
- ProofTreeOperations.checkInhabitants(solution,
- StringNode("allBusiness", Set(
- StringNode("pers", Set(
- StringNode("AddressBook", Set(
- StringNode("[Nil=>List]", Set(StringNode("Nil", Set())))
- ,
- StringNode("[Cons=>List]", Set(StringNode("l", Set())))
- ,
- StringNode("l.tail", Set())
- ))
- ))
- ))
- ))
-
- }
- }
-
- val CANDIDATES_TO_ENUMERATE = 50 :: 100 :: 1000 :: 10000 :: Nil
-
- val files = List("InsertionSortInsert.scala", "ListConcat.scala", "MergeSortSort.scala",
- "RedBlackTreeInsert.scala") map { lesynthTestDir + _ }
-
- @Ignore
- @Test
- def candidateEnumerationDuplicatesTest {
-
- for (candidatesToEnumerate <- CANDIDATES_TO_ENUMERATE;
- file <- files;
- (sctx, funDef, problem) <- forFile(file)) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
- val reporter = sctx.reporter
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val inSynth = new InSynth(loader.load, resultVariable.getType, true)
-
- val outputs = inSynth.getExpressions
-
- val taken = outputs.take(candidatesToEnumerate).map(_.getSnippet).toList
- val takenDistinct = taken.distinct
- val takenRepeated = taken.filter(snip => taken.count(_ == snip) > 1)
-
- assert(taken.size == takenDistinct.size, "First " + candidatesToEnumerate +
- " are not distinct." +
- "Repeated #" + takenRepeated.size
- + ": " + takenRepeated.map(snip => snip.toString +
- " repeats " + taken.count(_ == snip)).mkString("\n")
- )
- assert(takenRepeated.isEmpty)
- }
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/insynth/InSynthTest.scala b/src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
deleted file mode 100644
index bdc588de1..000000000
--- a/src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
+++ /dev/null
@@ -1,299 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package insynth
-
-import leon.synthesis.condabd.insynth.InSynth
-import leon.synthesis.condabd.insynth.leon._
-import leon.synthesis.condabd.insynth.leon.loader._
-import leon.synthesis.condabd.insynth.reconstruction.codegen._
-import leon.synthesis.condabd.insynth.reconstruction.Output
-
-import _root_.insynth.engine._
-import _root_.insynth.reconstruction._
-import _root_.insynth.reconstruction.{ stream => lambda }
-import _root_.insynth.reconstruction.stream.{ OrderedStreamFactory }
-import _root_.insynth.util.format._
-import _root_.insynth.util._
-
-import _root_.leon.purescala.Definitions._
-import _root_.leon.purescala.Common._
-import _root_.leon.purescala.TypeTrees._
-import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
-
-import org.junit.{ Test, Ignore }
-import org.junit.Assert._
-import org.scalatest.junit.JUnitSuite
-
-import util._
-import testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
-
-// TODO test abstractions (vals)
-class InSynthTest extends JUnitSuite {
-
- import CommonDeclarations._
- import CommonProofTrees._
- import CommonLambda._
- import DeclarationFactory._
-
- import Scaffold._
-
- import ProofTreeOperations.StringNode
-
- val insynthTestDir = "testcases/condabd/test/insynth/"
-
- val transformer = Streamer.apply _
- val codegen = (new CodeGenerator).apply _
-
- val maxElToOutput = 20
-
- import lambda.Node._
-
- def assertWeight(lambdaNode: lambda.Node, weight: Float) =
- assertEquals(size(lambdaNode), weight, 0f)
-
- def assertWeight(expected: Int, weight: Float) =
- assertEquals(expected.toFloat, weight, 0f)
-
- def assertWeight(pair: (lambda.Node, Float)) =
- assertEquals("Node " + pair._1, size(pair._1), pair._2, 0f)
-
- def assertTake(stream: Stream[(lambda.Node, Float)], num: Int) = {
- val result = stream take num
- def message(pos: Int) = "Part of the resulting stream: " + result.slice(pos - 10, pos + 10).mkString("\n")
-
- for (ind <- 0 until result.size)
- assertWeight(result(ind))
- for (ind <- 0 until result.size - 1)
- assertTrue("Weights are not in non-decreasing order.\n" + "At position " + ind + "\n" + message(ind), stream(ind)._2 <= stream(ind + 1)._2)
- result
- }
-
- def assertNoDuplicity(extractorResults: Stream[(lambda.Node, Float)]) = {
- // note that duplicates may exist in generated code (e.g. because coercions), but should not before that
- val duplicityMap = (Map[lambda.Node, Set[(lambda.Node, Float)]]() /: extractorResults) {
- (resMap, pair) =>
- val snippet = pair._1
- resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
- }
-
- lazy val duplicityMessage =
- for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) yield
- ("Key: " + key) + ("\nValues: " + value.mkString("\n"))
-
- assertTrue(
- "There are some duplications in generated code:\n" + duplicityMessage,
- duplicityMap.filter(_._2.size > 1).isEmpty
- )
- }
-
- def interactivePause = {
- System.out.println("Press Any Key To Continue...");
- new java.util.Scanner(System.in).nextLine();
- }
-
- @Test
- def testAddressesProofTree {
-
- for ((sctx, funDef, problem) <- forFile(insynthTestDir + "Addresses.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val inSynth = new InSynth(loader, resultVariable.getType, true)
- val solver = inSynth.solver
- val solution = solver.getProofTree
-
- assertTrue(
- ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
- ProofTreeOperations.checkInhabitants(solution,
- StringNode("AddressBook", Set(
- StringNode("[Cons=>List]", Set(StringNode("Cons")))
- ,
- StringNode("pers", Set(StringNode("makeAddressBook")))
- ))
- ))
- assertTrue(
- ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
- ProofTreeOperations.checkInhabitants(solution,
- StringNode("addToPers", Set(
- StringNode("makeAddressBook", Set())
- ,
- StringNode("Address", Set( ))
- ))
- ))
- assertTrue(
- ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
- ProofTreeOperations.checkInhabitants(solution,
- StringNode("addToBusiness", Set(
- StringNode("makeAddressBook", Set())
- ,
- StringNode("Address", Set( ))
- ))
- ))
- }
- }
-
- @Test
- def testAddressesExpressionsTypeAddress {
-
- for ((sctx, funDef, problem) <- forFile(insynthTestDir + "Addresses.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val inSynth = new InSynth(loader, resultVariable.getType, true)
- val solver = inSynth.solver
- val solution = solver.getProofTree
-
- val extractorResults = assertTake(transformer(solution.getNodes.head, true), 1000)
- assertNoDuplicity(extractorResults)
-
- val extractedSnipptes = extractorResults map { pair => codegen(pair._1) }
-
- val message = "Extracted: " + extractedSnipptes.size + "\n" +
- (for (output <- extractedSnipptes)
- yield "%20s" format output).mkString("\n")
-
- val expectedSnipptes = List(
- "AddressBook(Nil, l)",
- "makeAddressBook(l)"
- )
-
- for (snippet <- expectedSnipptes)
- assertTrue(snippet + " not found in extracted. results:\n" + message,
- extractedSnipptes.exists(_.toString == snippet.toString)
- )
-
- assertTrue(
- extractedSnipptes.exists(_.toString contains "addToPers")
- )
- assertTrue(
- extractedSnipptes.exists(_.toString contains "addToBusiness")
- )
-
- }
- }
-
- @Ignore("See this weight bug in InSynth")
- @Test
- def testAddressesExpressionsTypeBoolean {
-
- for ((sctx, funDef, problem) <- forFile(insynthTestDir + "Addresses.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
- val inSynth = new InSynth(loader, BooleanType, true)
- val solver = inSynth.solver
- val solution = solver.getProofTree
-
- val extractorResults = assertTake(transformer(solution.getNodes.head, true), 1000)
- assertNoDuplicity(extractorResults)
-
- val extractedSnipptes = extractorResults map { pair => codegen(pair._1) }
-
- val message = "Extracted: " + extractedSnipptes.size + "\n" +
- (for (output <- extractedSnipptes)
- yield "%20s" format output).mkString("\n")
-
- val expectedSnipptes = List(
- "allPrivate(AddressBook(Nil, l))",
- "allBusiness(makeAddressBook(l))",
- "allBusiness(makeAddressBook(l)) && allPrivate(AddressBook(Nil, l))"
- )
-
- for (snippet <- expectedSnipptes)
- assertTrue(snippet + " not found in extracted. results:\n" + message,
- extractedSnipptes.exists(_.toString == snippet.toString)
- )
- }
- }
-
- @Test
- def testAddressesExpressionsTypeAddressWithAddition {
-
- for ((sctx, funDef, problem) <- forFile(insynthTestDir + "AddressesWithAddition.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- // note problem.as does not contain function arguments, thus we use funDef.params
- //val varsInScope = problem.as
-
- val loader = new LeonLoader(program, arguments.toList, false)
- val inSynth = new InSynth(loader.load, resultVariable.getType, true)
- val solver = inSynth.solver
- val solution = solver.getProofTree
-
- val extractedSnipptes = inSynth.getExpressions.map(_.getSnippet) take 1000
-
- val message = "Extracted: " + extractedSnipptes.size + "\n" +
- (for (output <- extractedSnipptes)
- yield "%20s" format output).mkString("\n")
-
- val expectedSnipptes = List(
- "AddressBook(Nil, l)",
- "makeAddressBook(l, x, y)",
- "addToPers(AddressBook(l, l), Address(x, x, y))",
- "addToBusiness(AddressBook(l, l), Address(x, x, y))"
- )
-
- for (snippet <- expectedSnipptes)
- assertTrue(snippet + " not found in extracted. results:\n" + message,
- extractedSnipptes.exists(_.toString == snippet.toString)
- )
-
- }
- }
-
- @Test
- def testDeclarations {
-
- for ((sctx, funDef, problem) <- forFile(insynthTestDir + "AddressesWithAddition.scala")) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- // note problem.as does not contain function arguments, thus we use funDef.params
- //val varsInScope = problem.as
-
- val loader = new LeonLoader(program, arguments.toList, false)
- val inSynth = new InSynth(loader.load, resultVariable.getType, true)
-
- val allDeclarations = inSynth.getAllDeclarations.map(d => (d.getSimpleName, d.leonType.toString)).toSet
-
- val expectedDeclarations = Set(
- ("AddressBook", "(List, List) => AddressBook"),
- ("[Cons=>List]", "Cons => List"),
- ("pers", "AddressBook => List"),
- ("addToPers", "(AddressBook, Address) => AddressBook"),
- ("addToBusiness", "(AddressBook, Address) => AddressBook"),
- ("l", "List"),
- ("tail", "Cons => List"),
- ("a", "Cons => Address"),
- ("x", "Int"),
- ("y", "Boolean")
- )
-
- assertTrue(
- "Expected:\n" + expectedDeclarations.mkString("\n") + "\nFound:\n" + allDeclarations.mkString("\n"),
- expectedDeclarations.subsetOf(allDeclarations)
- )
- }
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala b/src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
deleted file mode 100644
index 2b06d18cc..000000000
--- a/src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
+++ /dev/null
@@ -1,133 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package insynth
-package loader
-
-import util._
-
-import leon.synthesis.condabd.insynth.leon._
-import leon.synthesis.condabd.insynth.leon.loader._
-
-import _root_.leon.purescala.Definitions._
-import _root_.leon.purescala.Common._
-import _root_.leon.purescala.TypeTrees._
-import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
-
-import org.junit.{ Test, Ignore }
-import org.junit.Assert._
-import org.scalatest.junit.JUnitSuite
-
-class LoaderTest extends JUnitSuite {
-
- import Scaffold._
-
- val insynthTestDir = "testcases/condabd/test"
- val testDir = insynthTestDir + "/insynth/"
-
- @Test
- def testAddresses {
- val fileName = testDir + "Addresses.scala"
-
- for ((sctx, funDef, problem) <- forFile(fileName)) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
-
- val allDeclarations = loader.load.map(d => (d.getSimpleName, d.leonType.toString)).toSet
-
- val expectedDeclarations = Set(
- ("AddressBook", "(List, List) => AddressBook"),
- ("[Cons=>List]", "Cons => List"),
- ("pers", "AddressBook => List"),
- ("makeAddressBook", "List => AddressBook"),
- ("addToPers", "(AddressBook, Address) => AddressBook"),
- ("addToBusiness", "(AddressBook, Address) => AddressBook"),
- ("l", "List"),
- ("tail", "Cons => List"),
- ("a", "Cons => Address")
- )
-
- assertTrue(
- "Expected:\n" + expectedDeclarations.mkString("\n") + "\nFound:\n" + allDeclarations.mkString("\n"),
- expectedDeclarations.subsetOf(allDeclarations)
- )
- }
- }
-
- @Test
- def testListConcat {
- val fileName = testDir + "ListConcat.scala"
-
- for ((sctx, funDef, problem) <- forFile(fileName)) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = problem.as
-
- val loader = new LeonLoader(program, varsInScope, false)
-
- val allDeclarations = loader.load.map(d => (d.getSimpleName, d.leonType.toString)).toSet
-
- val expectedDeclarations = Set(
- ("[Nil=>List]", "Nil => List"),
- ("[Cons=>List]", "Cons => List"),
- ("concat", "(List, List) => List"),
- ("l1", "List"),
- ("l2", "List"),
- ("tail", "Cons => List"),
- ("head", "Cons => Int")
- )
-
- assertTrue(
- "Expected:\n" + expectedDeclarations.mkString("\n") + "\nFound:\n" + allDeclarations.mkString("\n"),
- expectedDeclarations.subsetOf(allDeclarations)
- )
- }
- }
-
- @Test
- def testAddressesWithAddition {
- val fileName = testDir + "AddressesWithAddition.scala"
-
- for ((sctx, funDef, problem) <- forFile(fileName)) {
- val program = sctx.program
- val arguments = funDef.params.map(_.id)
-
- assertEquals(1, problem.xs.size)
- val resultVariable = problem.xs.head
- val varsInScope = funDef.params.map(_.id).toList //problem.as)
- assertTrue(varsInScope.size >= 3)
-
- val loader = new LeonLoader(program, varsInScope, false)
-
- val allDeclarations = loader.load.map(d => (d.getSimpleName, d.leonType.toString)).toSet
-
- val expectedDeclarations = Set(
- ("AddressBook", "(List, List) => AddressBook"),
- ("[Cons=>List]", "Cons => List"),
- ("pers", "AddressBook => List"),
- ("addToPers", "(AddressBook, Address) => AddressBook"),
- ("addToBusiness", "(AddressBook, Address) => AddressBook"),
- ("l", "List"),
- ("tail", "Cons => List"),
- ("a", "Cons => Address"),
- ("x", "Int"),
- ("y", "Boolean")
- )
-
- assertTrue(
- "Expected:\n" + expectedDeclarations.mkString("\n") + "\nFound:\n" + allDeclarations.mkString("\n"),
- expectedDeclarations.subsetOf(allDeclarations)
- )
- }
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala b/src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
deleted file mode 100644
index 0db1d7161..000000000
--- a/src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
+++ /dev/null
@@ -1,62 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd.insynth
-package reconstruction
-
-import org.junit.Assert._
-import org.junit.{ Test, Ignore }
-import org.scalatest.junit.JUnitSuite
-
-import leon.synthesis.condabd.insynth.reconstruction.codegen.CodeGenerator
-
-import _root_.leon.purescala.Trees._
-
-import testutil.{ CommonLambda, CommonDeclarations }
-
-// NOTE function cannot return function in Leon, no need to test that
-
-class CodeGeneratorTest extends JUnitSuite {
-
- import CommonLambda._
- import CommonDeclarations._
-
- val codeGenerator = new CodeGenerator
-
- @Test
- def testBooleanToIntIntermediateLambda {
- val codeGenResult = codeGenerator(constructBooleanToIntIntermediateLambda.head)
-
- assertEquals(
- FunctionInvocation(functionBoolToIntFunDef.typed, List(BooleanLiteral(false))),
- codeGenResult
- )
- }
-
- @Test
- def testThreeParFunction {
-
- val generated =
- for (intermediateTree <- constructThreeParFunctionIntermediateLambda(4))
- yield codeGenerator(intermediateTree)
-
- val baseCase = FunctionInvocation(threeParFunctionDef.typed, List(IntLiteral(0), IntLiteral(0), BooleanLiteral(false)))
-
- val message = "Generated:\n" + generated.mkString("\n")
-
- assertTrue(baseCase + " not found. " + message, generated contains baseCase)
-
- val oneLevCase1 = FunctionInvocation(threeParFunctionDef.typed, List(baseCase, IntLiteral(0), BooleanLiteral(false)))
- val oneLevCase2 = FunctionInvocation(threeParFunctionDef.typed, List(baseCase, baseCase, BooleanLiteral(false)))
-
- assertTrue(oneLevCase1 + " not found. " + message, generated contains oneLevCase1)
- assertTrue(oneLevCase2 + " not found. " + message, generated contains oneLevCase2)
-
- val twoLevCase1 = FunctionInvocation(threeParFunctionDef.typed, List(oneLevCase1, IntLiteral(0), BooleanLiteral(false)))
- val twoLevCase2 = FunctionInvocation(threeParFunctionDef.typed, List(baseCase, oneLevCase2, BooleanLiteral(false)))
-
- assertTrue(twoLevCase1 + " not found. " + message, generated contains twoLevCase1)
- assertTrue(twoLevCase2 + " not found. " + message, generated contains twoLevCase2)
-
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala b/src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
deleted file mode 100644
index dc37adb2b..000000000
--- a/src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
+++ /dev/null
@@ -1,106 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd.insynth
-package reconstruction
-
-import org.junit.{ Test, Ignore, BeforeClass, AfterClass }
-import org.junit.Assert._
-import org.scalatest.junit.JUnitSuite
-
-import leon.synthesis.condabd.insynth.reconstruction.codegen.CodeGenerator
-import leon.synthesis.condabd.insynth.reconstruction._
-
-import leon.purescala.Definitions.{ FunDef, ValDef, Program, ModuleDef }
-import leon.purescala.Common.{ FreshIdentifier }
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees.{ Variable => LeonVariable, _ }
-
-import testutil.{ CommonProofTrees, CommonDeclarations, CommonLeonExpressions, CommonUtils }
-
-class ReconstructorTest extends JUnitSuite {
-
- import CommonDeclarations._
- import CommonProofTrees._
- import CommonLeonExpressions._
- import CommonUtils._
-
- val codegen = new CodeGenerator
-
- @Test
- def treeBoolToInt {
- val (queryNode, query) = exampleBoolToInt
-
- val expStream = Reconstructor(queryNode, codegen)
-
- assertEquals(1, expStream.size)
-
- val codeGenResult = expStream.head
-
- assertEquals(FunctionInvocation(functionBoolToIntFunDef.typed, List(BooleanLiteral(false))), codeGenResult.snippet)
- assertEquals(0f, codeGenResult.weight, 0f)
- }
-
- @Test
- def treeIntToIntBoth {
- val queryNode = exampleIntToIntBoth
-
- val expStream = Reconstructor(queryNode, codegen)
-
- val expressions = expStream.map(_.snippet).take(20).toSet
-
- assertTrue(expressions contains inv1boolInv)
- assertTrue(expressions contains inv2WithBoolInv)
- assertTrue(expressions contains inv1WithInt)
- assertTrue(expressions contains inv2WithInt)
- assertTrue(expressions contains inv3WithInt)
- assertTrue(expressions contains inv3WithBoolInv)
- assertTrue(expressions contains inv4WithBoolInv)
- assertTrue(expressions contains inv4WithInt)
- }
-
- @Test
- def treeIntToIntBothOrdered {
- val queryNode = exampleIntToIntBoth
-
- val expStream = Reconstructor(queryNode, codegen, true)
-
- val expressions = assertTake(expStream, 20).map(_.snippet)
-
- val listOfExpressions = List(inv1boolInv, inv1WithInt, inv2WithBoolInv, inv2WithInt,
- inv3WithInt, inv3WithBoolInv, inv4WithBoolInv, inv4WithInt)
-
- for (exp <- listOfExpressions)
- assertTrue(expressions.toSet contains exp)
-
- val listOfExpressionsOrder = List(
- List(inv1boolInv, inv1WithInt),
- List(inv2WithBoolInv, inv2WithInt),
- List(inv3WithInt, inv3WithBoolInv),
- List(inv4WithBoolInv, inv4WithInt)
- )
-
- for (ind <- 0 until listOfExpressionsOrder.size - 1) {
- for( previousEl <- listOfExpressionsOrder(ind); nextEl <- listOfExpressionsOrder(ind + 1) )
- assertTrue("Expression " + previousEl + " (position " + expressions.indexOf(previousEl) +
- ") should occur before expression " + nextEl + " (position " + expressions.indexOf(nextEl) + ")",
- expressions.indexOf(previousEl) < expressions.indexOf(nextEl))
- }
-
- }
-
-}
-
-//object ReconstructorTest {
-//
-// var useEnumerationOrdering: Boolean = _
-//
-// @BeforeClass
-// def saveFlag = {
-// useEnumerationOrdering = Config.useEnumerationOrdering
-// Config.useEnumerationOrdering = false
-// }
-//
-// @AfterClass
-// def restoreFlag = Config.useEnumerationOrdering = useEnumerationOrdering
-//
-//}
diff --git a/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
deleted file mode 100644
index 3991240a6..000000000
--- a/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
+++ /dev/null
@@ -1,118 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd.insynth.testutil
-
-import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
-
-import org.junit.Assert._
-import org.junit.Test
-import org.junit.Ignore
-
-import leon.synthesis.condabd.insynth.leon.loader.DeclarationFactory._
-import leon.synthesis.condabd.insynth.leon._
-
-import leon.purescala.Definitions.{ FunDef, ValDef, Program, ModuleDef }
-import leon.purescala.Common.{ FreshIdentifier }
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-
-object CommonDeclarations {
-
- val booleanLiteral = BooleanLiteral(false)
-
- val booleanDeclaration = makeDeclaration(
- ImmediateExpression("false", booleanLiteral),
- BooleanType
- )
-
- val intLiteral = IntLiteral(0)
-
- val intDeclaration = makeDeclaration(
- ImmediateExpression("0", intLiteral),
- Int32Type
- )
-
- val unit = UnitLiteral()
-
- val unitDeclaration = makeDeclaration(
- ImmediateExpression("unit", unit),
- UnitType
- )
-
- val functionBoolToIntFunDef =
- new FunDef(
- FreshIdentifier("function1"),
- Nil,
- Int32Type,
- List( ValDef(FreshIdentifier("var"), BooleanType))
- )
-
- val functionBoolToIntType =
- FunctionType(List(BooleanType), Int32Type)
-
- val functionBoolToIntDeclaration = makeDeclaration(
- NaryReconstructionExpression("function1", { args: List[Expr] => FunctionInvocation(functionBoolToIntFunDef.typed, args) }),
- functionBoolToIntType
- )
-
- val functionFun1ToUnitFunDef =
- new FunDef(
- FreshIdentifier("function2"),
- Nil,
- UnitType,
- List( ValDef(FreshIdentifier("var"), functionBoolToIntType))
- )
-
- val functionFun1ToUnitType =
- FunctionType(List(UnitType), functionBoolToIntType)
-
- val functionFun1ToUnitDeclaration = makeDeclaration(
- NaryReconstructionExpression("function2", { args: List[Expr] => FunctionInvocation(functionFun1ToUnitFunDef.typed, args) }),
- functionFun1ToUnitType
- )
-
- val functionIntToIntType =
- FunctionType(List(Int32Type), Int32Type)
-
- val functionIntToIntFunDef= {
- val varId = FreshIdentifier("var")
- val varDec = ValDef(varId, Int32Type)
-
- val funDef = new FunDef(
- FreshIdentifier("functionRec"),
- Nil,
- Int32Type,
- List( varDec )
- )
-
- funDef.body = Some(Variable(varId))
-
- funDef
- }
-
- val functionIntToIntDeclaration = makeDeclaration(
- NaryReconstructionExpression("functionRec", { args: List[Expr] => FunctionInvocation(functionIntToIntFunDef.typed, args) }),
- functionIntToIntType
- )
-
- val threeParFunctionType =
- FunctionType(List(Int32Type, Int32Type, BooleanType), Int32Type)
-
- val threeParFunctionDef =
- new FunDef(
- FreshIdentifier("function3"),
- Nil,
- Int32Type,
- List(
- ValDef(FreshIdentifier("var_1"), Int32Type),
- ValDef(FreshIdentifier("var_2"), Int32Type),
- ValDef(FreshIdentifier("var_3"), BooleanType)
- )
- )
-
- val threeParFunctionDeclaration = makeDeclaration(
- NaryReconstructionExpression("function3", { args: List[Expr] => FunctionInvocation(threeParFunctionDef.typed, args) }),
- threeParFunctionType
- )
-
-}
diff --git a/src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
deleted file mode 100644
index 04593e929..000000000
--- a/src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
+++ /dev/null
@@ -1,189 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd.insynth.testutil
-
-import leon.synthesis.condabd.insynth.leon.query.{ LeonQueryBuilder => QueryBuilder, _ }
-import leon.synthesis.condabd.insynth.leon._
-import insynth.reconstruction.stream._
-
-import leon.purescala.Definitions.{ FunDef, ValDef, Program, ModuleDef }
-import leon.purescala.Common.{ FreshIdentifier }
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees.{ Variable => _, _ }
-
-object CommonLambda {
-
- implicit val leonToDomainType = DomainTypeTransformer(_: TypeTree)
-
- import CommonDeclarations._
- import CommonProofTrees._
-
- val booleanIdentifier = Identifier(BooleanType, booleanDeclaration)
-
- def constructBooleanToIntIntermediateLambda = {
- val query = new QueryBuilder(Int32Type)
-
- val functionApplication =
- Application(
- functionIntToIntType,
- List(
- Identifier(functionBoolToIntType, functionBoolToIntDeclaration),
- booleanIdentifier))
-
- val intermediateTree =
- Application(
- query.leonType,
- List(
- Identifier(query.leonType, query.getQuery.getDeclaration),
- functionApplication))
-
- List(intermediateTree)
- }
-
- def constructIntToIntIntermediateFirstLambda(x: Int) = {
- val query = new QueryBuilder(Int32Type)
-
- val functionApplication =
- Application(
- functionIntToIntType,
- List(
- Identifier(functionIntToIntType, functionIntToIntDeclaration),
- Identifier(Int32Type, intDeclaration)))
-
- val (_, listOfApplication) =
- (((Identifier(Int32Type, intDeclaration), Nil): (Node, List[Node])) /: (1 to x)) {
- case ((nextArg, list), _) =>
- val app = Application(
- functionIntToIntType,
- List(Identifier(functionIntToIntType, functionIntToIntDeclaration),
- nextArg))
-
- (app, list :+ app)
- }
-
- for (app <- listOfApplication) yield
- Application(
- query.leonType,
- List(
- Identifier(query.leonType, query.getQuery.getDeclaration),
- app))
- }
-
- def constructIntAndBoolToIntIntermediateLambda(x: Int) = {
- val query = new QueryBuilder(Int32Type)
-
- val functionApplicationBoolean =
- Application(
- functionBoolToIntType,
- List(
- Identifier(functionBoolToIntType, functionBoolToIntDeclaration),
- booleanIdentifier))
-
- val functionApplication =
- Application(
- functionIntToIntType,
- List(
- Identifier(functionIntToIntType, functionIntToIntDeclaration),
- Identifier(Int32Type, intDeclaration)))
-
- val (listOfApplication, _) =
- (((Nil, List(Identifier(Int32Type, intDeclaration), functionApplicationBoolean)): (List[Node], List[Node])) /: (1 to x)) {
- case ((list, args), _) =>
- val listAddition =
- for (arg <- args) yield
- Application(functionIntToIntType,
- List(Identifier(functionIntToIntType, functionIntToIntDeclaration), arg))
-
- (list ++ listAddition, listAddition)
- }
-
- for (app <- listOfApplication) yield
- Application(
- query.leonType,
- List(
- Identifier(query.leonType, query.getQuery.getDeclaration),
- app))
- }
-
- def constructThreeParFunctionIntermediateLambda(x: Int) = {
- val query = new QueryBuilder(Int32Type)
-
- val listOfApplication =
- ((List(Identifier(Int32Type, intDeclaration), Identifier(Int32Type, intDeclaration)): List[Node]) /: (1 to x)) {
- case (list, _) =>
- val listAddition =
- (for (arg <- list.combinations(2)) yield
- Application(
- threeParFunctionType,
- List(
- Identifier(threeParFunctionType, threeParFunctionDeclaration),
- arg(0),
- arg(1),
- booleanIdentifier
- )
- )) ++
- (for (arg <- list.combinations(2)) yield
- Application(
- threeParFunctionType,
- List(
- Identifier(threeParFunctionType, threeParFunctionDeclaration),
- arg(1),
- arg(0),
- booleanIdentifier
- )
- )) ++
- (for (arg <- list) yield
- Application(
- threeParFunctionType,
- List(
- Identifier(threeParFunctionType, threeParFunctionDeclaration),
- arg, arg,
- booleanIdentifier
- )
- ))
-
- (list ++ listAddition).distinct
- }
-
- for (app <- listOfApplication.distinct) yield
- Application(
- query.leonType,
- List(
- Identifier(query.leonType, query.getQuery.getDeclaration),
- app))
- }
-
- // TODO do if we need abstraction (high-order functions)
-// def constructFunctionIntToIntIntermediateLambda = {
-// val query = new QueryBuilder(FunctionType(List(Int32Type), Int32Type))
-//
-// val functionApplicationBoolean =
-// Application(
-// functionBoolToIntType,
-// List(
-// Set(Identifier(functionIntToIntType, functionBoolToIntDeclaration)),
-// Set(booleanIdentifier)))
-//
-// val functionApplication =
-// Application(
-// functionIntToIntType,
-// List(
-// Set(Identifier(functionIntToIntType, functionIntToIntDeclaration)),
-// Set(Variable(Int32Type, "freshInt"), functionApplicationBoolean)))
-//
-// functionApplication.recursiveParams = List(Set(functionApplication))
-//
-// val abstraction = Abstraction(functionIntToIntType,
-// List(Variable(Int32Type, "var_1")), Set(functionApplicationBoolean, functionApplication))
-//
-// val intermediateTree =
-// Application(
-// query.leonType,
-// List(
-// Set(Identifier(query.leonType, query.getQuery.getDeclaration)),
-// Set(abstraction)))
-//
-// intermediateTree
-// }
-
-}
diff --git a/src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
deleted file mode 100644
index dacfe93cd..000000000
--- a/src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
+++ /dev/null
@@ -1,26 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd.insynth.testutil
-
-import leon.purescala.Definitions.{ FunDef, ValDef, Program, ModuleDef }
-import leon.purescala.Common.{ FreshIdentifier }
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees.{ Variable => _, _ }
-
-object CommonLeonExpressions {
-
- import CommonDeclarations._
-
- val boolToInt = functionBoolToIntFunDef.typed
- val intToInt = functionIntToIntFunDef.typed
-
- val inv1boolInv = FunctionInvocation(boolToInt, List(booleanLiteral))
- val inv2WithBoolInv = FunctionInvocation(intToInt, List(inv1boolInv))
- val inv1WithInt = FunctionInvocation(intToInt, List(intLiteral))
- val inv2WithInt = FunctionInvocation(intToInt, List(inv1WithInt))
- val inv3WithInt = FunctionInvocation(intToInt, List(inv2WithInt))
- val inv3WithBoolInv = FunctionInvocation(intToInt, List(inv2WithBoolInv))
- val inv4WithBoolInv = FunctionInvocation(intToInt, List(inv3WithBoolInv))
- val inv4WithInt = FunctionInvocation(intToInt, List(inv3WithInt))
-
-}
diff --git a/src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
deleted file mode 100644
index 0cfdfe301..000000000
--- a/src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
+++ /dev/null
@@ -1,220 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd.insynth.testutil
-
-import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
-
-import org.junit.Assert._
-import org.junit.Test
-import org.junit.Ignore
-
-import leon.synthesis.condabd.insynth.leon.query.{ LeonQueryBuilder => QueryBuilder, _ }
-import insynth.structures._
-
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-
-object CommonProofTrees {
-
- import CommonDeclarations._
-
- def exampleBoolToInt = {
- val queryBuilder = new QueryBuilder(Int32Type)
-
- val query = queryBuilder.getQuery
-
- val queryDeclaration = query.getDeclaration
-
- val getBooleanNode =
- new SimpleNode(
- List(booleanDeclaration),
- MutableMap.empty)
-
- val getIntNode =
- new SimpleNode(
- List(functionBoolToIntDeclaration),
- MutableMap( // for each parameter type - how can we resolve it
- Const("Boolean") ->
- new ContainerNode(
- MutableSet(getBooleanNode))))
-
- val queryNode =
- new SimpleNode(
- List(queryDeclaration),
- MutableMap( // for each parameter type - how can we resolve it
- Const("Int") ->
- new ContainerNode(
- MutableSet(getIntNode))))
-
- (queryNode, query)
- }
-
- def exampleIntToInt = {
- val queryBuilder = new QueryBuilder(Int32Type)
-
- val query = queryBuilder.getQuery
-
- val queryDeclaration = query.getDeclaration
-
- val intNode =
- new SimpleNode(
- List(intDeclaration),
- MutableMap.empty)
-
- val getIntNode =
- new SimpleNode(
- List(functionIntToIntDeclaration),
- MutableMap())
-
- getIntNode.getParams +=
- (
- Const("Int") ->
- new ContainerNode(
- MutableSet(intNode, getIntNode)))
-
- val queryNode =
- new SimpleNode(
- List(queryDeclaration),
- MutableMap( // for each parameter type - how can we resolve it
- Const("Int") ->
- new ContainerNode(
- MutableSet(getIntNode))))
-
- queryNode
- }
-
-
- def exampleIntToIntBool = {
- val queryBuilder = new QueryBuilder(Int32Type)
-
- val query = queryBuilder.getQuery
-
- val queryDeclaration = query.getDeclaration
-
- val getBooleanNode =
- new SimpleNode(
- List(booleanDeclaration),
- MutableMap.empty)
-
- val getIntNodeFromBoolean =
- new SimpleNode(
- List(functionBoolToIntDeclaration),
- MutableMap( // for each parameter type - how can we resolve it
- Const("Boolean") ->
- new ContainerNode(
- MutableSet(getBooleanNode))))
-
- val getIntNodeFromIntToInt =
- new SimpleNode(
- List(functionIntToIntDeclaration),
- MutableMap())
-
- getIntNodeFromIntToInt.getParams +=
- (
- Const("Int") ->
- new ContainerNode(
- MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt)))
-
- val queryNode =
- new SimpleNode(
- List(queryDeclaration),
- MutableMap( // for each parameter type - how can we resolve it
- Const("Int") ->
- new ContainerNode(
- MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt))))
-
- queryNode
- }
-
-
- def exampleIntToIntBoth = {
- val queryBuilder = new QueryBuilder(Int32Type)
-
- val query = queryBuilder.getQuery
-
- val queryDeclaration = query.getDeclaration
-
- val intNode =
- new SimpleNode(
- List(intDeclaration),
- MutableMap.empty)
-
- val getBooleanNode =
- new SimpleNode(
- List(booleanDeclaration),
- MutableMap.empty)
-
- val getIntNodeFromBoolean =
- new SimpleNode(
- List(functionBoolToIntDeclaration),
- MutableMap( // for each parameter type - how can we resolve it
- Const("Boolean") ->
- new ContainerNode(
- MutableSet(getBooleanNode))))
-
- val getIntNodeFromIntToInt =
- new SimpleNode(
- List(functionIntToIntDeclaration),
- MutableMap())
-
- getIntNodeFromIntToInt.getParams +=
- (
- Const("Int") ->
- new ContainerNode(
- MutableSet(intNode, getIntNodeFromBoolean, getIntNodeFromIntToInt)))
-
- val queryNode =
- new SimpleNode(
- List(queryDeclaration),
- MutableMap( // for each parameter type - how can we resolve it
- Const("Int") ->
- new ContainerNode(
- MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt))))
-
- queryNode
- }
-
- // TODO do if we need abstraction (high-order functions)
-// def exampleFunctionIntToInt = {
-// val queryBuilder = new QueryBuilder(FunctionType(List(Int32Type), Int32Type))
-//
-// val query = queryBuilder.getQuery
-//
-// val queryDeclaration = query.getDeclaration
-//
-// val getBooleanNode =
-// new SimpleNode(
-// List(booleanDeclaration),
-// MutableMap.empty)
-//
-// val getIntNodeFromBoolean =
-// new SimpleNode(
-// List(functionBoolToIntDeclaration),
-// MutableMap( // for each parameter type - how can we resolve it
-// Const("Boolean") ->
-// new ContainerNode(
-// MutableSet(getBooleanNode))))
-//
-// val getIntNodeFromIntToInt =
-// new SimpleNode(
-// List(functionIntToIntDeclaration),
-// MutableMap())
-//
-// getIntNodeFromIntToInt.getParams +=
-// (
-// Const("Int") ->
-// new ContainerNode(
-// MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt)))
-//
-// val queryNode =
-// new SimpleNode(
-// List(queryDeclaration),
-// MutableMap( // for each parameter type - how can we resolve it
-// Const("Int") ->
-// new ContainerNode(
-// MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt))))
-//
-// queryNode
-// }
-
-}
\ No newline at end of file
diff --git a/src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
deleted file mode 100644
index 7c273e245..000000000
--- a/src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
+++ /dev/null
@@ -1,22 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd.insynth.testutil
-
-import org.junit.Assert._
-
-import leon.synthesis.condabd.insynth.reconstruction.Output
-
-object CommonUtils {
-
- val maxElToOutput = 20
-
- def assertTake(stream: Stream[Output], num: Int) = {
- val result = stream take num
- val message = "Part of the resulting stream: " + result.take(maxElToOutput).mkString("\n")
-
- for (ind <- 0 until result.size - 1)
- assertTrue("Weight are not in non-decreasing order.\n" + "At position " + ind + "\n" + message, stream(ind).getWeight <= stream(ind + 1).getWeight)
- result
- }
-
-}
\ No newline at end of file
diff --git a/src/test/scala/leon/test/condabd/refinement/FilterTest.scala b/src/test/scala/leon/test/condabd/refinement/FilterTest.scala
deleted file mode 100644
index 30cd50d2f..000000000
--- a/src/test/scala/leon/test/condabd/refinement/FilterTest.scala
+++ /dev/null
@@ -1,240 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package refinement
-
-import scala.util.Random
-
-import org.junit.Assert._
-import org.junit.{ Test, Ignore, Before }
-import org.scalatest.junit.JUnitSuite
-
-import leon.synthesis.condabd.insynth.leon.loader.LeonLoader
-import leon.synthesis.condabd.insynth.leon._
-
-import _root_.leon.purescala.Trees._
-import _root_.leon.purescala.TypeTrees._
-import _root_.leon.purescala._
-import _root_.leon.purescala.Definitions._
-
-import leon.synthesis.condabd.refinement._
-
-import util._
-
-class FilterTest extends JUnitSuite {
-
- import TreeOps._
- import Scaffold._
-
- val lesynthTestDir = "testcases/condabd/test/lesynth/"
-
- val rnd = new Random(System.currentTimeMillis())
-
- var filter: Filter = _
-
- var prog: Program = _
- var funDef: FunDef = _
- var tfunDef: TypedFunDef = _
- var variableRefiner: VariableRefiner = _
-
- var tail: UnaryReconstructionExpression = _
- var head: UnaryReconstructionExpression = _
- var nil: Expr = _
- var cons: NaryReconstructionExpression = _
-
- @Before
- def extract = {
-
- val problems = forFile(lesynthTestDir + "/ListConcat.scala")
- assertEquals(1, problems.size)
-
- val (sctx, funDef, problem) = problems.head
-
- prog = sctx.program
- this.funDef = funDef
- this.tfunDef = funDef.typed
-
- val loader = new LeonLoader(prog, problem.as, true)
-
- variableRefiner = new VariableRefinerStructure(loader.directSubclassesMap, loader.variableDeclarations,
- loader.classMap, sctx.reporter)
-
- tail =
- loader.extractFields.find {
- _.expression match {
- case ure: UnaryReconstructionExpression => ure(UnitLiteral()).toString.contains(".tail")
- case _ => false
- }
- } match {
- case Some(found) => found.expression.asInstanceOf[UnaryReconstructionExpression]
- case _ => fail("could not extract tail"); null
- }
-
- head =
- loader.extractFields.find {
- _.expression match {
- case ure: UnaryReconstructionExpression => ure(UnitLiteral()).toString.contains(".head")
- case _ => false
- }
- } match {
- case Some(found) => found.expression.asInstanceOf[UnaryReconstructionExpression]
- case _ => fail("could not extract head"); null
- }
-
- cons =
- loader.extractCaseClasses.find {
- _.expression match {
- case nre: NaryReconstructionExpression => nre(List(UnitLiteral(), UnitLiteral())).toString.contains("Cons")
- case _ => false
- }
- } match {
- case Some(found) => found.expression.asInstanceOf[NaryReconstructionExpression]
- case _ => fail("could not extract cons"); null
- }
-
- nil =
- loader.extractCaseClasses.find {
- _.expression match {
- case im: ImmediateExpression => im().toString.contains("Nil")
- case _ => false
- }
- } match {
- case Some(found) => found.expression.asInstanceOf[ImmediateExpression]()
- case _ => fail("could not extract cons"); null
- }
-
- filter = new Filter(prog, tfunDef, variableRefiner)
- }
-
- @Test
- def testIsLess = {
- val filter = this.filter
- import filter.isLess
-
- assertEquals(2, tfunDef.params.size)
-
- val variable1 = tfunDef.params.head
- val variable2 = tfunDef.params(1)
-
- assertEquals(+1, isLess(cons(List(UnitLiteral(), variable1.toVariable)), variable1.id))
- assertEquals(+1, isLess(cons(List(UnitLiteral(), variable1.toVariable)), variable2.id))
- assertEquals(-1, isLess(tail(variable1.toVariable), variable1.id))
- assertEquals(+1, isLess(head(variable1.toVariable), variable1.id))
- assertEquals(0, isLess(variable1.toVariable, variable1.id))
- assertEquals(1, isLess(variable1.toVariable, variable2.id))
- assertEquals(1, isLess(tail(variable1.toVariable), variable2.id))
- assertEquals(1, isLess(head(variable1.toVariable), variable2.id))
- assertEquals(1, isLess(nil, variable2.id))
-
- }
-
- @Test
- def testIsCallLessBySize = {
-
- val filter = this.filter
- import filter.isCallAvoidableBySize
-
- assertEquals(2, tfunDef.params.size)
-
- val arg1 = tfunDef.params.head.toVariable
- val arg2 = tfunDef.params(1).toVariable
-
- def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(tfunDef, Seq(arg1, arg2))
-
- val arguments = tfunDef.params.map(_.id).toList
-
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(nil, nil), arguments))
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg1, arg2), arguments))
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg2, arg1), arguments))
- assertEquals(false, isCallAvoidableBySize(makeFunctionCall(arg1, tail(arg2)), arguments))
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg1, tail(arg1)), arguments))
- assertEquals(false, isCallAvoidableBySize(makeFunctionCall(tail(arg1), tail(arg2)), arguments))
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(cons(List(nil, tail(arg1))), arg2), arguments))
- assertEquals(false, isCallAvoidableBySize(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2)), arguments))
- assertEquals(false, isCallAvoidableBySize(nil, arguments))
-
- }
-
- @Test
- def testHasDoubleRecursion = {
-
- val filter = this.filter
- import filter.hasDoubleRecursion
-
- assertEquals(2, tfunDef.params.size)
-
- val arg1 = tfunDef.params.head.toVariable
- val arg2 = tfunDef.params(1).toVariable
-
- def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(tfunDef, Seq(arg1, arg2))
-
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(nil, nil)))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, arg2)))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg2, arg1)))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, tail(arg2))))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, tail(arg1))))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(tail(arg1), tail(arg2))))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(cons(List(nil, tail(arg1))), arg2)))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2))))
- assertEquals(false, hasDoubleRecursion(nil))
-
- assertEquals(false, hasDoubleRecursion(And(makeFunctionCall(arg1, arg2), makeFunctionCall(arg1, arg2))))
- assertEquals(true, hasDoubleRecursion(makeFunctionCall(makeFunctionCall(arg1, arg2), tail(arg2))))
-
- }
-
- @Test
- def testIsAvoidable = {
-
- val filter = this.filter
- import filter.isAvoidable
-
- assertEquals(2, tfunDef.params.size)
-
- val arg1 = tfunDef.params.head.toVariable
- val arg2 = tfunDef.params(1).toVariable
-
- def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(tfunDef, Seq(arg1, arg2))
-
- val arguments = tfunDef.params.map(_.id).toList
-
- assertEquals(true, isAvoidable(makeFunctionCall(nil, nil), arguments))
- assertEquals(true, isAvoidable(makeFunctionCall(arg1, arg2), arguments))
- assertEquals(true, isAvoidable(makeFunctionCall(arg2, arg1), arguments))
- assertEquals(false, isAvoidable(makeFunctionCall(arg1, tail(arg2)), arguments))
- assertEquals(true, isAvoidable(makeFunctionCall(arg1, tail(arg1)), arguments))
- assertEquals(false, isAvoidable(makeFunctionCall(tail(arg1), tail(arg2)), arguments))
- assertEquals(true, isAvoidable(makeFunctionCall(cons(List(nil, tail(arg1))), arg2), arguments))
- assertEquals(false, isAvoidable(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2)), arguments))
- assertEquals(false, isAvoidable(nil, arguments))
-
- assertEquals(true, isAvoidable(makeFunctionCall(makeFunctionCall(arg1, arg2), tail(arg2)), arguments))
-
- }
-
- @Test
- def testIsAvoidableUneccessaryStructure {
-
- val filter = this.filter
- import filter.isAvoidable
-
- val arg1 = funDef.params.head.toVariable
- val arg2 = tfunDef.params(1).toVariable
- val arguments = tfunDef.params.map(_.id).toList
-
- val tpe = cons(List(Error("temp"))).getType match {
- case cct: CaseClassType => cct
- case _ =>
- fail(arg1 + " should have a class type")
- null
- }
-
- assertEquals(false, isAvoidable(CaseClassInstanceOf(tpe, arg1), arguments))
- assertEquals(false, isAvoidable(CaseClassInstanceOf(tpe, arg2), arguments))
- assertEquals(false, isAvoidable(CaseClassInstanceOf(tpe, cons(List(arg1, nil))), arguments))
- assertEquals(true, isAvoidable(CaseClassInstanceOf(tpe, tail(arg1)), arguments))
- assertEquals(true, isAvoidable(CaseClassInstanceOf(tpe, tail(tail(arg1))), arguments))
- assertEquals(true, isAvoidable(CaseClassInstanceOf(tpe, tail(tail(tail(tail(arg1))))), arguments))
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/refinement/RefinementExamples.scala b/src/test/scala/leon/test/condabd/refinement/RefinementExamples.scala
deleted file mode 100644
index 347d8ecf3..000000000
--- a/src/test/scala/leon/test/condabd/refinement/RefinementExamples.scala
+++ /dev/null
@@ -1,77 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd.refinement
-
-import scala.util.Random
-
-import org.scalatest.FunSpec
-import org.scalatest.GivenWhenThen
-
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-
-import leon.synthesis.condabd.insynth.leon._
-import leon.synthesis.condabd.refinement._
-
-object RefinementExamples {
-
- val listClassId = FreshIdentifier("List")
- val listAbstractClassDef = new AbstractClassDef(listClassId, Nil, None)
- val listAbstractClass = new AbstractClassType(listAbstractClassDef, Nil)
-
- val nilClassId = FreshIdentifier("Nil")
- val nilAbstractClassDef = new CaseClassDef(nilClassId, Nil, None, false)
- val nilAbstractClass = new CaseClassType(nilAbstractClassDef, Nil)
-
- val consClassId = FreshIdentifier("Cons")
- val consAbstractClassDef = new CaseClassDef(consClassId, Nil, None, false)
- val headId = FreshIdentifier("head").setType(Int32Type)
- consAbstractClassDef.setFields(Seq(ValDef(headId, Int32Type)))
- val consAbstractClass = new CaseClassType(consAbstractClassDef, Nil)
-
- val directSubclassMap: Map[ClassType, Set[ClassType]] = Map(
- listAbstractClass -> Set(nilAbstractClass, consAbstractClass)
- )
-
- val listVal = Variable(FreshIdentifier("tempVar"))
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- val classMap: Map[Identifier, ClassType] = Map(
- listClassId -> listAbstractClass,
- nilClassId -> nilAbstractClass,
- consClassId -> consAbstractClass
- )
-
- def buildClassMap(program: Program) = {
- val listAbstractClassDef = program.definedClasses.find(_.id.name == "List").
- get.asInstanceOf[AbstractClassDef]
- val listAbstractClass = AbstractClassType(listAbstractClassDef, Nil)
-
- val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
- get.asInstanceOf[CaseClassDef]
- val nilAbstractClass = CaseClassType(nilAbstractClassDef, Nil)
-
- val consAbstractClassDef = program.definedClasses.find(_.id.name == "Cons").
- get.asInstanceOf[CaseClassDef]
- val consAbstractClass = CaseClassType(consAbstractClassDef, Nil)
-
- val directSubclassMap: Map[ClassType, Set[ClassType]] = Map(
- listAbstractClass ->
- Set(nilAbstractClass, consAbstractClass)
- )
-
- val classMap: Map[Identifier, ClassType] = Map(
- listAbstractClassDef.id -> listAbstractClass,
- nilAbstractClassDef.id -> nilAbstractClass,
- consAbstractClassDef.id -> consAbstractClass
- )
-
- (directSubclassMap, listAbstractClass, classMap)
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/refinement/VariableRefinerComposeTest.scala b/src/test/scala/leon/test/condabd/refinement/VariableRefinerComposeTest.scala
deleted file mode 100644
index 8e281fa29..000000000
--- a/src/test/scala/leon/test/condabd/refinement/VariableRefinerComposeTest.scala
+++ /dev/null
@@ -1,152 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package refinement
-
-import scala.util.Random
-
-import org.scalatest.FunSpec
-import org.scalatest.GivenWhenThen
-
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.evaluators._
-
-import leon.synthesis.condabd.insynth.leon._
-import leon.synthesis.condabd.insynth.leon.loader._
-import leon.synthesis.condabd.refinement._
-
-import util.Scaffold
-
-class VariableRefinerComposeTest extends FunSpec with GivenWhenThen {
-
- import Scaffold._
- import RefinementExamples._
-
- val lesynthTestDir = "testcases/condabd/test/lesynth/"
-
- describe("A variable compose(structure, exec) refiner with list ADT") {
-
- it("should refine if condition is isSorted()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/InsertionSortInsert.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
- val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val isSorted =
- program.definedFunctions.find {
- _.id.name == "isSorted"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isSorted"); null
- }
-
- val listVal = funDef.params.find(_.id.name == "l").get.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableRefinerCompose")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableRefinerCompose add
- new VariableRefinerStructure(
- directSubclassMap, Seq(listLeonDeclaration), classMap, reporter
- ) add
- new VariableRefinerExecution(
- declarations, classMap
- )
-
- val res = variableRefiner.refine(
- isSorted(listVal),
- BooleanLiteral(true),
- declarations,
- codeGenEval
- )
-
- Then("declarations should be updated accordingly")
- expectResult((true, declarations.size + 2)) {
- (res._1, res._2.size)
- }
-
- withClue(declarations.toString) {
- assert {
- res._2.exists(_.leonType.toString contains "Cons")
- }
- }
-
- And("after 2nd consequtive call, nothing should happen")
- expectResult((false, res._2)) {
- val res2 = variableRefiner.refine(
- isSorted(listVal),
- BooleanLiteral(true),
- res._2,
- codeGenEval
- )
- (res2._1, res2._2)
- }
- }
- }
-
- }
-
- describe("A variable compose(structure) refiner with list ADT") {
-
- it("should not refine if condition is isSorted()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/InsertionSortInsert.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
- val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val isSorted =
- program.definedFunctions.find {
- _.id.name == "isSorted"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isSorted"); null
- }
-
- val listVal = funDef.params.find(_.id.name == "l").get.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableRefinerCompose")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableRefinerCompose add
- new VariableRefinerStructure(
- directSubclassMap, Seq(listLeonDeclaration), classMap, reporter
- )
-
- val res = variableRefiner.refine(
- isSorted(listVal),
- BooleanLiteral(true),
- declarations,
- codeGenEval
- )
-
- Then("declarations should stay the same")
- expectResult((false, declarations.size)) {
- (res._1, res._2.size)
- }
- }
- }
-
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/refinement/VariableRefinerExecutionTest.scala b/src/test/scala/leon/test/condabd/refinement/VariableRefinerExecutionTest.scala
deleted file mode 100644
index 770e5734a..000000000
--- a/src/test/scala/leon/test/condabd/refinement/VariableRefinerExecutionTest.scala
+++ /dev/null
@@ -1,300 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package refinement
-
-import scala.util.Random
-
-import org.scalatest.FunSpec
-import org.scalatest.GivenWhenThen
-
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.evaluators._
-
-import leon.synthesis.condabd.insynth.leon._
-import leon.synthesis.condabd.insynth.leon.loader._
-import leon.synthesis.condabd.refinement._
-
-import util.Scaffold
-
-class VariableRefinerExecutionTest extends FunSpec with GivenWhenThen {
-
- import Scaffold._
- import RefinementExamples._
-
- val lesynthTestDir = "testcases/condabd/test/lesynth/"
-
- describe("A variable execution refiner with list ADT on insertion sort") {
-
- it("should refine if condition is isSorted()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/InsertionSortInsert.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
- val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val isSorted =
- program.definedFunctions.find {
- _.id.name == "isSorted"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isSorted"); null
- }
-
- val listVal = funDef.params.find(_.id.name == "l").get.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableRefinerExecution")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableRefinerExecution(
- declarations, classMap
- )
-
- val res = variableRefiner.refine(
- isSorted(listVal),
- BooleanLiteral(true),
- declarations,
- codeGenEval
- )
-
- Then("declarations should be updated accordingly")
- expectResult((true, declarations.size + 2)) {
- (res._1, res._2.size)
- }
-
- withClue(declarations.toString) {
- assert {
- res._2.exists(_.leonType.toString contains "Cons")
- }
- }
-
- And("after 2nd consequtive call, nothing should happen")
- expectResult((false, res._2)) {
- val res2 = variableRefiner.refine(
- isSorted(listVal),
- BooleanLiteral(true),
- res._2,
- codeGenEval
- )
- (res2._1, res2._2)
- }
- }
- }
- }
-
- describe("A variable execution refiner with list ADT on lists") {
-
- it("should refine if condition is isEmpty()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
- val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val isEmpty =
- program.definedFunctions.find {
- _.id.name == "isEmpty"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isEmpty"); null
- }
-
- val isEmptyBad =
- program.definedFunctions.find {
- _.id.name == "isEmptyBad"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isEmpty"); null
- }
-
- val listVal = funDef.params.head.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableRefinerExecution")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableRefinerExecution(
- declarations, classMap
- )
-
- val res = variableRefiner.refine(
- isEmpty(listVal),
- BooleanLiteral(true),
- declarations,
- codeGenEval
- )
-
- Then("declarations should be updated accordingly")
- expectResult((true, declarations.size + 2)) {
- (res._1, res._2.size)
- }
-
- withClue(declarations.toString) {
- assert {
- res._2.exists(_.leonType.toString contains "Cons")
- }
- }
-
- And("after 2nd consequtive call, nothing should happen")
- expectResult((false, res._2)) {
- val res2 = variableRefiner.refine(
- isEmpty(listVal),
- BooleanLiteral(true),
- res._2,
- codeGenEval
- )
- (res2._1, res2._2)
- }
- }
- }
-
- it("should refine list to Cons if condition is hasContent()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
- val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
-// val inSynth = new InSynth(loader, true)
-// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val hasContent =
- program.definedFunctions.find {
- _.id.name == "hasContent"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract hasContent"); null
- }
-
- val listVal = funDef.params.head.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableRefinerExecution")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableRefinerExecution(
- declarations, classMap
- )
-
- val condition = Not(hasContent(listVal))
-
- val res = variableRefiner.refine(
- condition,
- BooleanLiteral(true),
- declarations,
- codeGenEval
- )
-
- Then("declarations should be updated accordingly")
- expectResult((true, declarations.size + 2)) {
- (res._1, res._2.size)
- }
-
- withClue(declarations.toString) {
- assert {
- res._2.exists(_.leonType.toString contains "Cons")
- }
- }
-
- And("after 2nd consequtive call, nothing should happen")
- expectResult((false, res._2)) {
- val res2 = variableRefiner.refine(
- condition,
- BooleanLiteral(true),
- res._2,
- codeGenEval
- )
- (res2._1, res2._2)
- }
- }
- }
-
- it("should not refine if condition is isEmptyBad()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
- val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
-// val inSynth = new InSynth(loader, true)
-// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val isEmpty =
- program.definedFunctions.find {
- _.id.name == "isEmpty"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isEmpty"); null
- }
-
- val isEmptyBad =
- program.definedFunctions.find {
- _.id.name == "isEmptyBad"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isEmpty"); null
- }
-
- val listVal = funDef.params.head.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableRefinerExecution")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableRefinerExecution(
- declarations, classMap
- )
-
- val res = variableRefiner.refine(
- isEmptyBad(listVal),
- BooleanLiteral(true),
- declarations,
- codeGenEval
- )
-
- Then("declarations should not be updated")
- expectResult((false, res._2)) {
- val res2 = variableRefiner.refine(
- isEmptyBad(listVal),
- BooleanLiteral(true),
- res._2,
- codeGenEval
- )
- (res2._1, res2._2)
- }
- }
- }
-
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/refinement/VariableRefinerStructureTest.scala b/src/test/scala/leon/test/condabd/refinement/VariableRefinerStructureTest.scala
deleted file mode 100644
index f0f385719..000000000
--- a/src/test/scala/leon/test/condabd/refinement/VariableRefinerStructureTest.scala
+++ /dev/null
@@ -1,72 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package refinement
-
-import scala.util.Random
-
-import org.scalatest.FunSpec
-import org.scalatest.GivenWhenThen
-
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-
-import leon.synthesis.condabd.insynth.leon._
-import leon.synthesis.condabd.refinement._
-
-import util.Scaffold._
-
-class VariableRefinerTest extends FunSpec with GivenWhenThen {
-
- import RefinementExamples._
-
- describe("A variable refiner with list ADT") {
-
- it("should refine if variable is not Nil") {
-
- Given("a VariableRefiner based on structure")
- val variableRefiner = new VariableRefinerStructure(
- directSubclassMap, Seq(listLeonDeclaration), classMap, reporter
- )
-
- Then("it should return appropriate id And class def")
- expectResult(Some((listVal.id, nilAbstractClass))) {
- variableRefiner.getIdAndClassDef(CaseClassInstanceOf(nilAbstractClass, listVal))
- }
- And("return None for some unknown expression")
- expectResult(None) {
- variableRefiner.getIdAndClassDef(listVal)
- }
-
-
- Then("declarations should be updated accordingly")
- val allDeclarations = List(listLeonDeclaration)
- expectResult((true,
- LeonDeclaration(
- ImmediateExpression( listVal + "." + headId,
- CaseClassSelector(consAbstractClass, listVal, headId) ),
- TypeTransformer(Int32Type), Int32Type
- ) ::
- LeonDeclaration(
- listLeonDeclaration.expression, TypeTransformer(consAbstractClass), consAbstractClass
- ) :: Nil
- )) {
- variableRefiner.refine(CaseClassInstanceOf(nilAbstractClass, listVal),
- BooleanLiteral(true),
- allDeclarations
- )
- }
-
- And("after 2nd consequtive call, nothing should happen")
- expectResult((false, allDeclarations)) {
- variableRefiner.refine(CaseClassInstanceOf(nilAbstractClass, listVal),
- BooleanLiteral(true),
- allDeclarations)
- }
- }
-
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/refinement/VariableSolverRefinerTest.scala b/src/test/scala/leon/test/condabd/refinement/VariableSolverRefinerTest.scala
deleted file mode 100644
index 444ca30ad..000000000
--- a/src/test/scala/leon/test/condabd/refinement/VariableSolverRefinerTest.scala
+++ /dev/null
@@ -1,213 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package refinement
-
-import scala.util.Random
-
-import org.scalatest.FunSpec
-import org.scalatest.GivenWhenThen
-
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-
-import insynth._
-import leon.synthesis.condabd.insynth.leon._
-import leon.synthesis.condabd.insynth.leon.loader._
-import leon.synthesis.condabd.refinement._
-
-import util._
-
-class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
-
- import Scaffold._
- import RefinementExamples._
-
- val lesynthTestDir = "testcases/condabd/test/lesynth/"
-
- describe("A variable solver refiner with list ADT") {
-
- it("should refine if condition is isEmpty()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
-// val inSynth = new InSynth(loader, true)
-// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val isEmpty =
- program.definedFunctions.find {
- _.id.name == "isEmpty"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isEmpty"); null
- }
-
- val isEmptyBad =
- program.definedFunctions.find {
- _.id.name == "isEmptyBad"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isEmpty"); null
- }
-
- val listVal = funDef.params.head.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableSolverRefiner")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableSolverRefiner(
- directSubclassMap, declarations, classMap, solver, reporter
- )
-
- val res = variableRefiner.refine(
- isEmpty(listVal),
- isEmpty(listVal),
- declarations
- )
-
- Then("declarations should be updated accordingly")
- expectResult((true, declarations.size)) {
- (res._1, res._2.size)
- }
-
- And("after 2nd consequtive call, nothing should happen")
- expectResult((false, res._2)) {
- val res2 = variableRefiner.refine(
- isEmpty(listVal),
- isEmpty(listVal),
- res._2
- )
- (res2._1, res2._2)
- }
- }
- }
-
- it("should refine list to Cons if condition is hasContent()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
-// val inSynth = new InSynth(loader, true)
-// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val hasContent =
- program.definedFunctions.find {
- _.id.name == "hasContent"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract hasContent"); null
- }
-
- val listVal = funDef.params.head.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableSolverRefiner")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableSolverRefiner(
- directSubclassMap, declarations, classMap, solver, reporter
- )
-
- val res = variableRefiner.refine(
- hasContent(listVal),
- hasContent(listVal),
- declarations
- )
-
- Then("declarations should be updated accordingly")
- expectResult((true, declarations.size + 2)) {
- (res._1, res._2.size)
- }
-
- And("after 2nd consequtive call, nothing should happen")
- expectResult((false, res._2)) {
- val res2 = variableRefiner.refine(
- hasContent(listVal),
- hasContent(listVal),
- res._2
- )
- (res2._1, res2._2)
- }
- }
- }
-
- it("should not refine if condition is isEmptyBad()") {
-
- for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
- val program = sctx.program
- val solver = sctx.solverFactory
- val reporter = sctx.reporter
-
- val loader = new LeonLoader(program, problem.as, false)
- val allDeclarations = loader.load
-// val inSynth = new InSynth(loader, true)
-// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
- val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
-
- val isEmpty =
- program.definedFunctions.find {
- _.id.name == "isEmpty"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isEmpty"); null
- }
-
- val isEmptyBad =
- program.definedFunctions.find {
- _.id.name == "isEmptyBad"
- } match {
- case Some(found) => (x: Expr) => FunctionInvocation(found.typed, Seq(x))
- case _ => fail("could not extract isEmpty"); null
- }
-
- val listVal = funDef.params.head.toVariable
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- Given("a VariableSolverRefiner")
- val declarations = List(listLeonDeclaration)
- val variableRefiner = new VariableSolverRefiner(
- directSubclassMap, declarations, classMap, solver, reporter
- )
-
- val res = variableRefiner.refine(
- isEmptyBad(listVal),
- isEmptyBad(listVal),
- declarations
- )
-
- Then("declarations should not be updated")
- expectResult((false, res._2)) {
- val res2 = variableRefiner.refine(
- isEmptyBad(listVal),
- isEmptyBad(listVal),
- res._2
- )
- (res2._1, res2._2)
- }
- }
- }
-
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/util/Scaffold.scala b/src/test/scala/leon/test/condabd/util/Scaffold.scala
deleted file mode 100644
index 3b30dca9b..000000000
--- a/src/test/scala/leon/test/condabd/util/Scaffold.scala
+++ /dev/null
@@ -1,98 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package util
-
-import org.scalatest.FunSuite
-import org.scalatest.matchers.ShouldMatchers._
-
-import java.io.{BufferedWriter, FileWriter, File}
-
-import leon._
-import leon.test._
-import leon.frontends._
-import leon.utils._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.solvers.z3._
-import leon.solvers.Solver
-import leon.synthesis._
-import leon.synthesis.utils._
-
-object Scaffold {
-
- val reporter = new TestSilentReporter
-
- def forProgram(content: String): Iterable[(SynthesisContext, FunDef, Problem)] = {
-
- val forProgramReporter = new TestSilentReporter
- val ctx = LeonContext(
- settings = Settings(
- synthesis = true,
- xlang = false,
- verify = false
- ),
- files = List(),
- reporter = forProgramReporter,
- interruptManager = new InterruptManager(forProgramReporter)
- )
-// Settings.showIDs = true
-
- val pipeline = TemporaryInputPhase andThen scalac.ExtractionPhase andThen SynthesisProblemExtractionPhase
-
- val (program, results) = try {
- pipeline.run(ctx)((content, Nil))
- } catch {
- case _: Throwable =>
- fail("Error while processing")
- }
-
- extractProblems(ctx, program, results)
- }
-
- def forFile(file: String): Iterable[(SynthesisContext, FunDef, Problem)] = {
- val programFile = new File(file)
-
- val forProgramReporter = new TestSilentReporter
- val ctx = LeonContext(
- settings = Settings(
- synthesis = true,
- xlang = false,
- verify = false
- ),
- files = List(programFile),
- reporter = forProgramReporter,
- interruptManager = new InterruptManager(forProgramReporter)
- )
-
- val pipeline = scalac.ExtractionPhase andThen SynthesisProblemExtractionPhase
-
- val (program, results) = try {
- pipeline.run(ctx)(file :: Nil)
- } catch {
- case _: Throwable =>
- fail("Error while processing " + file)
- }
-
- extractProblems(ctx, program, results)
- }
-
- private def extractProblems(ctx: LeonContext, program: Program,
- problemMap: Map[leon.purescala.Definitions.FunDef,Seq[leon.synthesis.Problem]]) = {
-
- val opts = SynthesisOptions()
-
- for ((f, ps) <- problemMap; p <- ps)
- yield {
- val sctx = SynthesisContext(ctx,
- opts,
- Some(f),
- program,
- new TestSilentReporter)
-
- (sctx, f, p)
- }
- }
-
-}
diff --git a/src/test/scala/leon/test/condabd/util/Utils.scala b/src/test/scala/leon/test/condabd/util/Utils.scala
deleted file mode 100644
index 0bd397000..000000000
--- a/src/test/scala/leon/test/condabd/util/Utils.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon.test.condabd
-package util
-
-import org.scalatest.FunSuite
-import org.scalatest.matchers.ShouldMatchers._
-
-import java.io.{BufferedWriter, FileWriter, File}
-
-import leon._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.solvers.z3._
-import leon.solvers.Solver
-import leon.synthesis._
-import leon.synthesis.utils._
-
-object Utils {
-
- def getFunDefByName(program: Program, name: String) = {
- assert(program.definedFunctions.exists({
- funDef: FunDef => funDef.id.name == name
- }), "Function " + name + " not found. All functions: " + program.definedFunctions.map(_.id.name).mkString(", "))
-
- program.definedFunctions.find({
- funDef: FunDef => funDef.id.name == name
- }) match {
- case Some(res) => res
- case _ => null
- }
- }
-
-}
\ No newline at end of file
--
GitLab