diff --git a/src/main/scala/lesynth/ExampleRunner.scala b/src/main/scala/lesynth/ExampleRunner.scala
deleted file mode 100644
index 3d82d3c037faa8cc2cfbe1531ffaf83c73d40186..0000000000000000000000000000000000000000
--- a/src/main/scala/lesynth/ExampleRunner.scala
+++ /dev/null
@@ -1,134 +0,0 @@
-package lesynth
-
-import scala.collection.mutable.{ Map => MutableMap }
-import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{ LinkedList => MutableList }
-
-import leon.{ Main => LeonMain, DefaultReporter, Settings, LeonContext }
-import leon.evaluators._
-import leon.evaluators.EvaluationResults._
-import leon.solvers.Solver
-import leon.solvers.z3.{ FairZ3Solver }
-import leon.verification.AnalysisPhase
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Trees._
-import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.TreeOps
-
-import insynth.util.logging.HasLogger
-
-import EvaluationResults._
-
-class ExampleRunner(program: Program, maxSteps: Int = 2000) extends HasLogger {
-
- import TreeOps._
-
- var counterExamples = MutableList[Map[Identifier, Expr]]()
-
- val leonEmptyContext = LeonContext()
-
- // its okay to construct just one, prog is not use in the default evaluator
- lazy val defaultEvaluator = {
- val ev = new DefaultEvaluator(leonEmptyContext, program)
- ev.maxSteps = maxSteps
- ev
- }
-
- def evaluate(expr: Expr, mapping: Map[Identifier, Expr]) = {
- fine("to evaluate: " + expr + " for mapping: " + mapping)
- defaultEvaluator.eval(expr, mapping) match {
- case Successful(BooleanLiteral(true)) =>
- fine("Eval succeded: EvaluationSuccessful(true)")
- true
- case m =>
- fine("Eval failed: " + m)
- false
- }
- }
-
- def evaluateToResult(expr: Expr, mapping: Map[Identifier, Expr]) = {
- fine("to evaluate: " + expr + " for mapping: " + mapping)
- defaultEvaluator.eval(expr, mapping)
- }
-
- /** filter counterexamples according to an expression (precondition) */
- def filter(prec: Expr) = {
- entering("filter(" + prec + ")")
- fine("Old counterExamples.size: " + counterExamples.size)
- counterExamples = counterExamples filter {
- evaluate(prec, _)
- }
- fine("New counterExamples.size: " + counterExamples.size)
- }
-
- /** count how many examples pass */
- def countPassed(expressionToCheck: Expr) = {
- // TODO body dont have set type in synthesizer
-// val expressionToCheck =
-// //Globals.bodyAndPostPlug(exp)
-// {
-// val resFresh = FreshIdentifier("result", true).setType(body.getType)
-// Let(
-// resFresh, body,
-// replace(Map(ResultVariable() -> Variable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition)))
-// }
- fine("expressionToCheck: " + expressionToCheck)
- finest("program: " + program)
-
- (0 /: counterExamples) {
- (res, ce) =>
- {
- if (evaluate(expressionToCheck, ce)) res + 1
- else res
- }
- }
- }
-
-// def countPassedAndTerminating(body: Expr): Int = {
-// // TODO body dont have set type in synthesizer
-// val expressionToCheck =
-// //Globals.bodyAndPostPlug(exp)
-// {
-// val resFresh = FreshIdentifier("result", true).setType(body.getType)
-// Let(
-// resFresh, body,
-// replace(Map(ResultVariable() -> Variable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition)))
-// }
-// fine("expressionToCheck: " + expressionToCheck)
-//
-// (0 /: counterExamples) {
-// (res, ce) =>
-// {
-// evaluateToResult(expressionToCheck, ce) match {
-// case EvaluationSuccessful(BooleanLiteral(true)) =>
-// res + 1
-// case EvaluationError("Stack overflow") =>
-// return -counterExamples.size
-// case m =>
-// res
-// }
-// }
-// }
-// }
-
- // check if this body passes all examples
-// def check(body: Expr): Boolean = {
-// val examplesToCheck = counterExamples
-// val expressionToCheck = Globals.bodyAndPostPlug(body)
-// fine("Expression to check: " + expressionToCheck)
-//
-// var res = true
-// val iterator = counterExamples.iterator
-//
-// while (res && iterator.hasNext) {
-// val currentExample = iterator.next
-// res = evaluate(expressionToCheck, currentExample)
-//
-// if (!res) fine("Failed example: " + currentExample)
-// }
-//
-// return res
-// }
-
-}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/SynthesisInfo.scala b/src/main/scala/lesynth/SynthesisInfo.scala
index 82a5487d8972817338283af882d57c2a5236879d..e438d247173037cb93e6f170b5c54f55bf3bdd55 100644
--- a/src/main/scala/lesynth/SynthesisInfo.scala
+++ b/src/main/scala/lesynth/SynthesisInfo.scala
@@ -1,5 +1,7 @@
package lesynth
+import leon.StopwatchCollections
+
/**
* Contains information about the synthesis process
*/
@@ -7,6 +9,17 @@ 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)
diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/lesynth/SynthesizerExamples.scala
index 7f5cd95ac9c9a3b9f6a14b3e8f740488eedb10d3..1a3037f86d678a8bfd442125b4e208b4318b8d08 100755
--- a/src/main/scala/lesynth/SynthesizerExamples.scala
+++ b/src/main/scala/lesynth/SynthesizerExamples.scala
@@ -2,42 +2,45 @@ package lesynth
import scala.collection.mutable.{ Map => MutableMap }
import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.PriorityQueue
+import scala.collection.mutable.{ ArrayBuffer, PriorityQueue }
+
+import leon.{ Reporter, DefaultReporter, SilentReporter, LeonContext }
+import leon.Main.processOptions
-import leon.{Reporter, DefaultReporter, SilentReporter, LeonContext}
import leon.solvers.{ Solver, TimeoutSolver }
import leon.solvers.z3.{ FairZ3Solver }
import leon.verification.AnalysisPhase
+
import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
import leon.purescala.Trees.{ Variable => LeonVariable, _ }
-import leon.purescala.Definitions.{FunDef, Program}
+import leon.purescala.Definitions.{ FunDef, Program }
import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
-import insynth.util.logging.HasLogger
+import leon.evaluators.EvaluationResults
+import leon.evaluators._
+import leon.synthesis.{ Problem, SynthesisContext }
+
import insynth.interfaces.Declaration
import insynth.InSynth
-import insynth.leon.loader.LeonLoader
-import insynth.leon.LeonDeclaration
-import insynth.leon.ImmediateExpression
-import insynth.engine.InitialEnvironmentBuilder
-import insynth.interfaces.Declaration
-import insynth.engine.InitialEnvironmentBuilder
-import insynth.leon.TypeTransformer
+import insynth.leon.loader._
+import insynth.leon._
+import insynth.engine._
import insynth.reconstruction.Output
-import leon.synthesis.{ Problem, SynthesisContext }
-import leon.Main.processOptions
-import leon.purescala.TypeTrees._
+import insynth.util.logging.HasLogger
+
+import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
+import scala.util.control.Breaks._
-import scala.collection.mutable.{Map => MutableMap}
-import scala.collection.mutable.{Set => MutableSet}
-import scala.util.control.Breaks.break
-import scala.util.control.Breaks.breakable
+import lesynth.examples._
+import lesynth.evaluation._
+import lesynth.ranking._
+import lesynth.refinement._
import SynthesisInfo._
import SynthesisInfo.Action._
-class SynthesizerForRuleExamples(
+class SynthesizerForRuleExamples(
// some synthesis instance information
val solver: Solver,
val program: Program,
@@ -46,23 +49,24 @@ class SynthesizerForRuleExamples(
val problem: Problem,
val synthesisContext: SynthesisContext,
val freshResVar: LeonVariable,
+ val evaluationStrategy: EvaluationStrategy, // = DefaultEvaluationStrategy(program, holeFunDef, synthesisContext.context),
// number of condition expressions to try before giving up on that branch expression
numberOfBooleanSnippets: Int = 5,
numberOfCounterExamplesToGenerate: Int = 5,
- leonTimeout: Int = 2, // seconds
+ leonTimeout: Int = 1, // seconds
analyzeSynthesizedFunctionOnly: Boolean = false,
showLeonOutput: Boolean = false,
reporter: Reporter = new DefaultReporter,
//examples: List[Map[Identifier, Expr]] = Nil,
// we need the holeDef to know the right ids
- introduceExamples: ((Seq[Identifier], LeonLoader) => List[Map[Identifier, Expr]]) = { (_, _) => Nil },
+ introduceExamples: (() => List[Map[Identifier, Expr]]) = { () => Nil },
collectCounterExamplesFromLeon: Boolean = false,
filterOutAlreadySeenBranchExpressions: Boolean = true,
- useStringSetForFilterOutAlreadySeenBranchExpressions: Boolean = true,
- numberOfTestsInIteration: Int = 50,
- numberOfCheckInIteration: Int = 5
-) extends HasLogger {
-
+ useStringSetForFilterOutAlreadySeenBranchExpressions: Boolean = true,
+ numberOfTestsInIteration: Int = 25,
+ numberOfCheckInIteration: Int = 5,
+ exampleRunnerSteps: Int = 4000) extends HasLogger {
+
val fileName: String = "noFileName"
info("Synthesizer:")
@@ -71,7 +75,7 @@ class SynthesizerForRuleExamples(
info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
info("leonTimeout: %d".format(leonTimeout))
//info("examples: " + examples.mkString(", "))
-
+
info("holeFunDef: %s".format(holeFunDef))
info("problem: %s".format(problem.toString))
@@ -82,17 +86,17 @@ class SynthesizerForRuleExamples(
private var loader: LeonLoader = _
private var inSynth: InSynth = _
private var inSynthBoolean: InSynth = _
- private var refiner: Refiner = _
+ private var refiner: Filter = _
//private var solver: Solver = _
private var ctx: LeonContext = _
private var initialPrecondition: Expr = _
-
+
private var variableRefiner: VariableRefiner = _
// can be used to unnecessary syntheses
private var variableRefinedBranch = false
private var variableRefinedCondition = true // assure initial synthesis
private var booleanExpressionsSaved: Stream[Output] = _
-
+
private var seenBranchExpressions: Set[String] = Set.empty
// flag denoting if a correct body has been synthesized
@@ -109,24 +113,24 @@ class SynthesizerForRuleExamples(
// filtering/ranking with examples support
var exampleRunner: ExampleRunner = _
+ var gatheredExamples: ArrayBuffer[Example] = _
def analyzeProgram = {
-
+
synthInfo.start(Verification)
- Globals.allSolved = Some(true)
+ Globals.allSolved = None
import TreeOps._
-
+
val body = holeFunDef.getBody
val theExpr = {
- val resFresh = FreshIdentifier("result", true).setType(body.getType)
- val bodyAndPost =
- Let(
- resFresh, body,
- replace(Map(ResultVariable() -> LeonVariable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition))
- )
-
- val withPrec = if( holeFunDef.precondition.isEmpty) {
+ val resFresh = FreshIdentifier("result", true).setType(body.getType)
+ val bodyAndPost =
+ Let(
+ resFresh, body,
+ replace(Map(ResultVariable() -> LeonVariable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition)))
+
+ val withPrec = if (holeFunDef.precondition.isEmpty) {
bodyAndPost
} else {
Implies(matchToIfThenElse(holeFunDef.precondition.get), bodyAndPost)
@@ -134,7 +138,7 @@ class SynthesizerForRuleExamples(
withPrec
}
-
+
val reporter = //new DefaultReporter
new SilentReporter
val args =
@@ -142,14 +146,15 @@ class SynthesizerForRuleExamples(
Array(fileName, "--timeout=" + leonTimeout, "--functions=" + holeFunDef.id.name)
else
Array(fileName, "--timeout=" + leonTimeout)
- info("Leon context array: " + args.mkString(","))
+ finest("Leon context array: " + args.mkString(","))
ctx = processOptions(reporter, args.toList)
- val solver = new TimeoutSolver(new FairZ3Solver(ctx), 4000L)
- //new TimeoutSolver(synthesisContext.solver.getNewSolver, 2000L)
+ val solver = new TimeoutSolver(new FairZ3Solver(ctx), 1000L * leonTimeout)
+ //new TimeoutSolver(synthesisContext.solver.getNewSolver, 2000L)
solver.setProgram(program)
-
+
+ Globals.asMap = Map.empty
Globals.allSolved = solver.solve(theExpr)
- fine("solver said " + Globals.allSolved + " for " + theExpr)
+ finest("Solver said " + Globals.allSolved + " for " + theExpr)
//interactivePause
// measure time
@@ -160,8 +165,8 @@ class SynthesizerForRuleExamples(
// TODO return boolean (do not do unecessary analyze)
def generateCounterexamples(program: Program, funDef: FunDef, number: Int): (Seq[Map[Identifier, Expr]], Expr) = {
- fine("generate counter examples with funDef.prec= " + funDef.precondition.getOrElse(BooleanLiteral(true)))
-
+ info("Generate counter examples with precondition " + funDef.precondition.getOrElse(BooleanLiteral(true)))
+
// get current precondition
var precondition = funDef.precondition.getOrElse(BooleanLiteral(true))
// where we will accumulate counterexamples as sequence of maps
@@ -178,7 +183,7 @@ class SynthesizerForRuleExamples(
// check if solver could solved this instance
if (Globals.allSolved == Some(false) && !Globals.asMap.isEmpty) {
- fine("found coounterexample: " + Globals.asMap)
+ info("Found counterexample: " + Globals.asMap)
// add current counterexample
maps :+= Globals.asMap
@@ -193,9 +198,9 @@ class SynthesizerForRuleExamples(
ind += 1
}
-// val temptime = System.currentTimeMillis - temp
-// fine("Generation of counter-examples took: " + temptime)
-// verTime += temptime
+ // val temptime = System.currentTimeMillis - temp
+ // fine("Generation of counter-examples took: " + temptime)
+ // verTime += temptime
// return found counterexamples and the formed precondition
(maps, precondition)
@@ -203,21 +208,23 @@ class SynthesizerForRuleExamples(
def getCurrentBuilder = new InitialEnvironmentBuilder(allDeclarations)
- def synthesizeBranchExpressions = {
- synthInfo.profile(Generation) { inSynth.getExpressions(getCurrentBuilder) }
+ def synthesizeBranchExpressions = {
+ info("Invoking synthesis for branch expressions")
+ synthInfo.profile(Generation) { inSynth.getExpressions(getCurrentBuilder) }
}
def synthesizeBooleanExpressions = {
+ info("Invoking synthesis for condition expressions")
synthInfo.start(Generation)
- if ( variableRefinedCondition ) {
+ if (variableRefinedCondition) {
// store for later fetch (will memoize values)
- booleanExpressionsSaved =
- inSynthBoolean.getExpressions(getCurrentBuilder).
- filterNot(expr => refiner.isAvoidable(expr.getSnippet, problem.as)) take numberOfBooleanSnippets
- // reset flag
- variableRefinedCondition = false
+ booleanExpressionsSaved =
+ inSynthBoolean.getExpressions(getCurrentBuilder).
+ filterNot(expr => refiner.isAvoidable(expr.getSnippet, problem.as)) take numberOfBooleanSnippets
+ // reset flag
+ variableRefinedCondition = false
}
-
+
synthInfo end booleanExpressionsSaved
}
@@ -225,7 +232,7 @@ class SynthesizerForRuleExamples(
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)) =
@@ -235,27 +242,10 @@ class SynthesizerForRuleExamples(
def initialize = {
hole = Hole(desiredType)
-
+
// TODO lose this - globals are bad
Globals.allSolved = None
- // context needed for verification
- import leon.Main._
-// val reporter =
-// if (showLeonOutput) new DefaultReporter
-// else new SilentReporter
-//
-// val args =
-// if (analyzeSynthesizedFunctionOnly)
-// Array(fileName, "--timeout=" + leonTimeout, "--functions=" + holeFunDef.id.name)
-// else
-// Array(fileName, "--timeout=" + leonTimeout)
-// info("Leon context array: " + args.mkString(","))
-// ctx = processOptions(reporter, args.toList)
-
- //solver = //new FairZ3Solver(ctx)
- // new TimeoutSolver(new FairZ3Solver(ctx), leonTimeout)
-
// create new insynth object
loader = new LeonLoader(program, hole, problem.as, false)
inSynth = new InSynth(loader, true)
@@ -267,7 +257,7 @@ class SynthesizerForRuleExamples(
// funDef of the hole
fine("postcondition is: " + holeFunDef.getPostcondition)
fine("declarations we see: " + allDeclarations.map(_.toString).mkString("\n"))
- interactivePause
+ // interactivePause
// accumulate precondition for the remaining branch to synthesize
accumulatingPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
@@ -283,92 +273,10 @@ class SynthesizerForRuleExamples(
loader.variableDeclarations, loader.classMap, reporter)
// calculate cases that should not happen
- refiner = new Refiner(program, hole, holeFunDef)
- fine("Refiner initialized. Recursive call: " + refiner.recurentExpression)
-
- exampleRunner = new ExampleRunner(program, 4000)
- exampleRunner.counterExamples ++= //examples
- introduceExamples(holeFunDef.args.map(_.id), loader)
-
- fine("Introduced examples: " + exampleRunner.counterExamples.mkString(", "))
- }
-
- def countPassedExamples(snippet: Expr) = {
- synthInfo.start(Action.Evaluation)
-
- val oldPreconditionSaved = holeFunDef.precondition
- val oldBodySaved = holeFunDef.body
-
- // restore initial precondition
- holeFunDef.precondition = Some(initialPrecondition)
-
- // get the whole body (if else...)
- val accumulatedExpression = accumulatingExpression(snippet)
- // set appropriate body to the function for the correct evaluation
- holeFunDef.body = Some(accumulatedExpression)
-
-
- import TreeOps._
- val expressionToCheck =
- //Globals.bodyAndPostPlug(exp)
- {
- val resFresh = FreshIdentifier("result", true).setType(accumulatedExpression.getType)
- Let(
- resFresh, accumulatedExpression,
- replace(Map(ResultVariable() -> LeonVariable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition)))
- }
-
- finest("going to count passed for: " + holeFunDef)
- finest("going to count passed for: " + expressionToCheck)
-
- val count = exampleRunner.countPassed(expressionToCheck)
-// if (snippet.toString == "Cons(l1.head, concat(l1.tail, l2))")
-// interactivePause
-
- holeFunDef.precondition = oldPreconditionSaved
- holeFunDef.body = oldBodySaved
-
- synthInfo end count
- }
-
-
- def evaluateCandidate(snippet: Expr, mapping: Map[Identifier, Expr]) = {
-
- synthInfo.start(Action.Evaluation)
+ refiner = new Filter(program, holeFunDef, variableRefiner)
- val oldPreconditionSaved = holeFunDef.precondition
- val oldBodySaved = holeFunDef.body
-
- // restore initial precondition
- holeFunDef.precondition = Some(initialPrecondition)
-
- // get the whole body (if else...)
- val accumulatedExpression = accumulatingExpression(snippet)
- // set appropriate body to the function for the correct evaluation
- holeFunDef.body = Some(accumulatedExpression)
-
- import TreeOps._
- val expressionToCheck =
- //Globals.bodyAndPostPlug(exp)
- {
- val resFresh = FreshIdentifier("result", true).setType(accumulatedExpression.getType)
- Let(
- resFresh, accumulatedExpression,
- replace(Map(ResultVariable() -> LeonVariable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition)))
- }
-
- finest("going to evaluate candidate for: " + holeFunDef)
- finest("going to evaluate candidate for: " + expressionToCheck)
-
- val count = exampleRunner.evaluate(expressionToCheck, mapping)
-
- holeFunDef.precondition = oldPreconditionSaved
- holeFunDef.body = oldBodySaved
-
-// if(snippet.toString == "checkf(f2, reverse(r2))")
-// interactivePause
-
- synthInfo end count
+ gatheredExamples = ArrayBuffer(introduceExamples().map(Example(_)): _*)
+ info("Introduced examples: " + gatheredExamples.mkString("\t"))
}
def synthesize: Report = {
@@ -389,23 +297,24 @@ class SynthesizerForRuleExamples(
case Some(true) => false
case _ => true
}
- // update flag in case of time limit overdue
- def checkTimeout =
- if (synthesisContext.shouldStop.get) {
- keepGoing = false
- true
- } else
- false
+ // update flag in case of time limit overdue
+ def checkTimeout =
+ if (synthesisContext.shouldStop.get) {
+ 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 {
@@ -425,101 +334,119 @@ class SynthesizerForRuleExamples(
var numberOfTested = 0
reporter.info("Going into a enumeration/testing phase.")
- fine("evaluating examples: " + exampleRunner.counterExamples.mkString("\n"))
-
+ fine("evaluating examples: " + gatheredExamples.mkString("\n"))
+
breakable {
- while(true) {
+ while (true) {
+ if (checkTimeout) break
val batchSize = numberOfTestsInIteration * (1 << noBranchFoundIteration)
-
- reporter.info("numberOfTested: " + numberOfTested)
- // ranking of candidates
- val candidates = {
- val (it1, it2) = snippetsIterator.duplicate
- snippetsIterator = it2.drop(batchSize)
- it1.take(batchSize).
- map(_.getSnippet).filterNot(
- snip => {
- (seenBranchExpressions contains snip.toString) || refiner.isAvoidable(snip, problem.as)
- }
- ).toSeq
- }
- info("got candidates of size: " + candidates.size)
- //interactivePause
-
- // printing candidates and pass counts
- fine( {
- val logString = ((candidates.zipWithIndex) map {
- case ((snippet: Expr, ind: Int)) => ind + ": snippet is " + snippet.toString +
- " pass count is " + countPassedExamples(snippet)
- }).mkString("\n")
- logString
- })
- //interactivePause
-
- if (candidates.size > 0) {
- val ranker = new Ranker(candidates,
- Evaluation(exampleRunner.counterExamples, this.evaluateCandidate _, candidates, exampleRunner),
- false)
-
- val maxCandidate = ranker.getMax
- info("maxCandidate is: " + maxCandidate)
- numberOfTested += batchSize
-
- if (
- candidates.exists(_.toString contains "checkf(f2, Cons(x, r2))")
- ) {
- println("maxCandidate is: " + maxCandidate)
- println(ranker.printTuples)
- println("AAA2")
- println("Candidates: " + candidates.zipWithIndex.map({
- case (cand, ind) => "[" + ind + "]" + cand.toString
- }).mkString("\n"))
- println("Examples: " + exampleRunner.counterExamples.zipWithIndex.map({
- case (example, ind) => "[" + ind + "]" + example.toString
- }).mkString("\n"))
- interactivePause
- }
-
- interactivePause
- if (tryToSynthesizeBranch(maxCandidate)) {
- noBranchFoundIteration = 0
- break
- }
- interactivePause
-
- noBranchFoundIteration += 1
- }
- }
- }
-
- // add to seen if branch was not found for it
- //seenBranchExpressions += snippetTree.toString
+
+ reporter.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.toString) || refiner.isAvoidable(snip, problem.as)
+ }).toIndexedSeq
+ }
+ info("Got candidates of size: " + candidates.size +
+ " , first 10 of them are: " + candidates.take(10).map(_.getSnippet.toString).mkString(",\t"))
+ //interactivePause
+
+
+ // val count = exampleRunner.evaluate(expressionToCheck, mapping)
+
+ if (candidates.size > 0) {
+ // save current precondition and the old body since it will can be mutated during evaluation
+ val oldPreconditionSaved = holeFunDef.precondition
+ val oldBodySaved = holeFunDef.body
+ // set initial precondition
+ holeFunDef.precondition = Some(initialPrecondition)
+
+ val ranker = evaluationStrategy.getRanker(candidates, accumulatingExpression, gatheredExamples)
+ exampleRunner = evaluationStrategy.getExampleRunner
+
+ info("Ranking candidates...")
+ synthInfo.start(Action.Evaluation)
+ val maxCandidate = ranker.getMax
+ synthInfo.end
+
+ // restore original precondition and body
+ holeFunDef.precondition = oldPreconditionSaved
+ holeFunDef.body = oldBodySaved
+
+ // check for timeouts
+ if (!keepGoing) break
+
+ info("Candidate with the most successfull evaluations is: " + maxCandidate)
+// interactivePause
+ numberOfTested += batchSize
+
+ if (false //candidates.exists(_.toString contains "merge(sort(split(list")
+ ) {
+ println("maxCandidate is: " + maxCandidate)
+ println(ranker.printTuples)
+ println("AAA2")
+ println("Candidates: " + candidates.zipWithIndex.map({
+ case (cand, ind) => "[" + ind + "]" + cand.toString
+ }).mkString("\n"))
+ println("Examples: " + gatheredExamples.zipWithIndex.map({
+ case (example, ind) => "[" + ind + "]" + example.toString
+ }).mkString("\n"))
+ interactivePause
+ }
+
+ // interactivePause
+ if (tryToSynthesizeBranch(maxCandidate.getExpr)) {
+ noBranchFoundIteration = 0
+ break
+ }
+ // interactivePause
+
+ totalExpressionsTested += numberOfTested
+ noBranchFoundIteration += 1
+ }
+ } // while(true)
+ } // breakable
+
+ // add to seen if branch was not found for it
+ //seenBranchExpressions += snippetTree.toString
+
+ if (!keepGoing) break
// if did not found for any of the branch expressions
if (found) {
synthInfo end Synthesis
+ synthInfo.iterations = iteration
+ synthInfo.numberOfEnumeratedExpressions = numberOfTested
reporter.info("We are done, in time: " + synthInfo.last)
return new FullReport(holeFunDef, synthInfo)
}
- if ( variableRefinedBranch ) {
- fine("Variable refined, doing branch synthesis again")
- // get new snippets
- snippets = synthesizeBranchExpressions
- snippetsIterator = snippets.iterator
- pq = getNewExampleQueue
-
+ 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
+ snippetsIterator = snippets.iterator
- fine("filtering based on: " + holeFunDef.precondition.get)
- fine("counterexamples before filter: " + exampleRunner.counterExamples.size)
+ info("Filtering based on precondition: " + holeFunDef.precondition.get)
+ fine("counterexamples before filter: " + gatheredExamples.size)
exampleRunner.filter(holeFunDef.precondition.get)
- fine("counterexamples after filter: " + exampleRunner.counterExamples.size)
- fine("counterexamples after filter: " + exampleRunner.counterExamples.mkString("\n"))
+ gatheredExamples = exampleRunner.examples
+ fine("counterexamples after filter: " + gatheredExamples.size)
+ fine("counterexamples after filter: " + gatheredExamples.mkString("\n"))
}
} //breakable { while (!keepGoing) {
@@ -541,10 +468,12 @@ class SynthesizerForRuleExamples(
// TODO spare one analyzing step
// analyze the program
- fine("analyzing program for funDef:" + holeFunDef)
-// solver.setProgram(program)
+ info("Current candidate solution is:\n" + holeFunDef)
+ fine("Analyzing program for funDef:" + holeFunDef)
+ // solver.setProgram(program)
analyzeProgram
+ info("Solver returned: " + Globals.allSolved)
// check if solver could solved this instance
if (Globals.allSolved == Some(true)) {
// mark the branch found
@@ -572,7 +501,7 @@ class SynthesizerForRuleExamples(
// collect (add) counterexamples from leon
if (collectCounterExamplesFromLeon)
- exampleRunner.counterExamples ++= maps
+ gatheredExamples ++= maps.map(Example(_))
// this should not be possible
// val keepGoing = Globals.allSolved match {
@@ -594,15 +523,13 @@ class SynthesizerForRuleExamples(
// return true
// }
- //if(maps.isEmpty) throw new RuntimeException("asdasdasd")
-
+ //if(maps.isEmpty) throw new RuntimeException("asdasdasd")
-
// will modify funDef body and precondition, restore it later
try {
{ //if (!maps.isEmpty) {
// proceed with synthesizing boolean expressions
- solver.setProgram(program)
+ //solver.setProgram(program)
// reconstruct (only defined number of boolean expressions)
val innerSnippets = synthesizeBooleanExpressions
@@ -613,16 +540,18 @@ class SynthesizerForRuleExamples(
}).mkString("\n"))
for (
- innerSnippetTree <- innerSnippets map { _.getSnippet };
- if (
- { val flag = !refiner.isAvoidable(innerSnippetTree, problem.as)
- if (!flag) fine("Refiner filtered this snippet: " + innerSnippetTree)
- flag }
- )
- ) {
+ 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 (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, precondition)
+ val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, maps)
// if precondition found
if (innerFound) {
@@ -654,8 +583,8 @@ class SynthesizerForRuleExamples(
}
}
- def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: Expr): (Boolean, Option[Expr]) = {
-
+ def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, counterExamples: Seq[Map[Identifier, Expr]]): (Boolean, Option[Expr]) = {
+
// new condition together with existing precondition
val newCondition = And(Seq(accumulatingPrecondition, innerSnippetTree))
@@ -672,69 +601,73 @@ class SynthesizerForRuleExamples(
// nothing here
// here, our expression is not contradictory, continue
case Some(false) =>
- // check if synthesized boolean expression implies precondition (counterexamples)
- val implyExpression = Implies(newCondition, precondition)
- fine("implyExpression is: " + implyExpression)
-
- // check if synthesized condition implies counter-examples
- val solveReturn = solver.solve(implyExpression)
- fine("solve returned: " + solveReturn)
-
- solveReturn match {
- case Some(true) =>
- // if expression implies counterexamples add it to the precondition and try to validate program
- holeFunDef.precondition = Some(newCondition)
- // do analysis
-// solver.setProgram(program)
- analyzeProgram
- // program is valid, we have a branch
- if (Globals.allSolved == Some(true)) {
- // we found a branch
- reporter.info("We found a branch, for expression %s, with condition %s.".format(snippetTree, innerSnippetTree))
-
- // 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")
- accumulatingPrecondition = And(Seq(accumulatingPrecondition, Not(innerSnippetTree)))
- fine("updating hole fun precondition and body (to be hole)")
-
- // set to set new precondition
- val preconditionToRestore = Some(accumulatingPrecondition)
-
- val variableRefinementResult = variableRefiner.checkRefinements(innerSnippetTree, allDeclarations)
- if (variableRefinementResult._1) {
- allDeclarations = variableRefinementResult._2
-
- // the reason for two flags is for easier management of re-syntheses only if needed
- variableRefinedBranch = true
- variableRefinedCondition = true
- }
-
- // found a boolean snippet, break
- (true, preconditionToRestore)
- } else {
- // reset funDef and continue with next boolean snippet
- val preconditionToRestore = Some(accumulatingPrecondition)
- (false, preconditionToRestore)
+ // check if synthesized boolean expression implies precondition (counterexamples)
+ val implyCounterExamples = (false /: counterExamples) {
+ case (false, exMapping) =>
+ exampleRunner.evaluateToResult(newCondition, exMapping) match {
+ case EvaluationResults.Successful(BooleanLiteral(false)) => false
+ case r =>
+ fine("Evaluation result for " + newCondition + " on " + exMapping + " is " + r)
+ true
+ }
+ case _ => true
+ }
+ fine("implyCounterExamples: " + implyCounterExamples)
+
+ if (!implyCounterExamples) {
+ // if expression implies counterexamples add it to the precondition and try to validate program
+ holeFunDef.precondition = Some(newCondition)
+ // do analysis
+ solver.setProgram(program)
+ analyzeProgram
+ // program is valid, we have a branch
+ if (Globals.allSolved == Some(true)) {
+ // we found a branch
+ reporter.info("We found a branch, for expression %s, with condition %s.".format(snippetTree, innerSnippetTree))
+
+ // 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")
+ accumulatingPrecondition = And(Seq(accumulatingPrecondition, Not(innerSnippetTree)))
+ fine("updating hole fun precondition and body (to be hole)")
+
+ // set to set new precondition
+ val preconditionToRestore = Some(accumulatingPrecondition)
+
+ val variableRefinementResult = variableRefiner.checkRefinements(innerSnippetTree, allDeclarations)
+ 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
}
- case _ =>
-
- fine("solver filtered out the precondition (does not imply counterexamples)")
- (false, None)
- } //solveReturn match { (for implying counterexamples)
+ // found a boolean snippet, break
+ (true, preconditionToRestore)
+ } else {
+ // reset funDef and continue with next boolean snippet
+ val preconditionToRestore = Some(accumulatingPrecondition)
+ (false, preconditionToRestore)
+ }
+ } else {
+ fine("solver filtered out the precondition (does not imply counterexamples)")
+ (false, None)
+ }
+ //solveReturn match { (for implying counterexamples)
} // notFalseSolveReturn match {
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3da1dc0bcace4c65996d175bc11c41b0e9597182
--- /dev/null
+++ b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
@@ -0,0 +1,128 @@
+package lesynth
+package evaluation
+
+import scala.collection.mutable.ArrayBuffer
+
+import leon._
+import leon.evaluators._
+import leon.evaluators.EvaluationResults._
+import leon.purescala.Trees._
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.TreeOps
+import leon.codegen.CodeGenEvalParams
+
+import lesynth.examples._
+import lesynth.ranking._
+
+import insynth.util.logging.HasLogger
+
+case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonContext,
+ candidates: Seq[Candidate], inputExamples: Seq[Example],
+ params: CodeGenEvalParams = CodeGenEvalParams(maxFunctionInvocations = 200, checkContracts = true)) extends ExampleRunner(inputExamples) with HasLogger {
+
+ private var _examples = ArrayBuffer(transformExamples(inputExamples): _*)
+
+ val evaluationContext = ctx.copy(reporter = new SilentReporter)
+
+ 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 <- funDef.args.map(_.id)) yield
+ map(id)
+ }
+ )
+
+ def compile(expr: Expr, ids: Seq[Identifier]) = {
+ // this get is dubious
+ StopwatchCollections.get("Compilation").newStopwatch profile getEvaluator.compile(expr, ids).get
+ }
+
+ val candidateClosures = candidates.map(cand => compile(cand.prepareExpression, funDef.args.map(_.id)))
+
+ override def evaluate(candidateInd: Int, exampleInd: Int) = {
+ val closure = candidateClosures(candidateInd)
+
+ fine("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, funDef.args.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, funDef.args.map(_.id))
+
+ evaluate(closure, funDef.args.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, funDef.args.map(_.id))
+
+ closure(funDef.args.map(arg => mapping(arg.id)))
+ }
+
+ def evaluate(evalClosure: Seq[Expr] => Result, args: Seq[Expr]) = {
+ try {
+ evalClosure(args) match {
+ case Successful(BooleanLiteral(true)) =>
+ fine("Eval succeded: EvaluationSuccessful(true)")
+ 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, funDef.args.map(_.id))
+
+ _examples = _examples filter {
+ evaluate(closure, _)
+ }
+ fine("New counterExamples.size: " + examples.size)
+ }
+
+ /** count how many examples pass */
+ override def countPassed(expressionToCheck: Expr) = {
+ fine("expressionToCheck: " + expressionToCheck)
+
+ val closure = compile(expressionToCheck, funDef.args.map(_.id))
+
+ val (passed, failed) = (_examples zip examples).partition(
+ pair => evaluate(closure, pair._1)
+ )
+
+ (passed.size, passed map (_._2))
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala b/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c11570107d4b8910bcd88ca49e6185c0a14a6202
--- /dev/null
+++ b/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
@@ -0,0 +1,82 @@
+package lesynth
+package evaluation
+
+import scala.collection.mutable.ArrayBuffer
+
+import leon._
+import leon.evaluators._
+import leon.evaluators.EvaluationResults._
+import leon.purescala.Trees._
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.TreeOps
+
+import lesynth.examples._
+import lesynth.ranking._
+
+import insynth.util.logging.HasLogger
+
+case class DefaultExampleRunner(program: Program, funDef: FunDef, 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.copy(reporter = new SilentReporter)
+
+ 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, funDef.args.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)
+ _examples = _examples filter {
+ evaluate(prec, _)
+ }
+ 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)
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala b/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
new file mode 100644
index 0000000000000000000000000000000000000000..55780f6283451e8e47fc2dc3839078f6c52d93fd
--- /dev/null
+++ b/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
@@ -0,0 +1,94 @@
+package lesynth
+package evaluation
+
+import leon._
+import leon.evaluators._
+import leon.evaluators.EvaluationResults._
+import leon.purescala.Trees._
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.TreeOps
+import leon.codegen.CodeGenEvalParams
+
+import insynth.reconstruction.Output
+import insynth.util.logging._
+
+import lesynth.ranking._
+import lesynth.examples._
+
+trait EvaluationStrategy {
+ def getRanker(candidatePairs: IndexedSeq[(Output)], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]): Ranker
+
+ def getExampleRunner: ExampleRunner
+}
+
+case class DefaultEvaluationStrategy(program: Program, funDef: FunDef, ctx: LeonContext,
+ maxSteps: Int = 2000) extends EvaluationStrategy with HasLogger {
+
+ var exampleRunner: ExampleRunner = _
+
+ override def getRanker(candidatePairs: IndexedSeq[Output], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]) = {
+
+ val candidates = Candidate.makeDefaultCandidates(candidatePairs, bodyBuilder, funDef)
+
+ exampleRunner = DefaultExampleRunner(program, funDef, ctx, 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
+ })
+
+ val evaluation = Evaluation(exampleRunner)
+
+ new Ranker(candidates, evaluation)
+ }
+
+ override def getExampleRunner = exampleRunner
+}
+
+case class CodeGenEvaluationStrategy(program: Program, funDef: FunDef, ctx: LeonContext,
+ maxSteps: Int = 200) extends EvaluationStrategy with HasLogger {
+
+ var exampleRunner: ExampleRunner = _
+
+ override def getRanker(candidatePairs: IndexedSeq[Output], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]) = {
+
+ val candidates = Candidate.makeCodeGenCandidates(candidatePairs, bodyBuilder, funDef)
+
+ val newProgram = program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ candidates.map(_.newFunDef)))
+
+ finest("New program looks like: " + newProgram)
+ finest("Candidates look like: " + candidates.map(_.prepareExpression).mkString("\n"))
+
+ val params = CodeGenEvalParams(maxFunctionInvocations = maxSteps, checkContracts = true)
+
+ exampleRunner = CodeGenExampleRunner(newProgram, funDef, ctx, candidates, inputExamples, params)
+
+ // 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
+ })
+
+ val evaluation = Evaluation(exampleRunner)
+
+ new Ranker(candidates, evaluation)
+ }
+
+ override def getExampleRunner = exampleRunner
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/evaluation/ExampleRunner.scala b/src/main/scala/lesynth/evaluation/ExampleRunner.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bb78d02ca92398e4ec9d3a56125f59ae5346da3f
--- /dev/null
+++ b/src/main/scala/lesynth/evaluation/ExampleRunner.scala
@@ -0,0 +1,40 @@
+package lesynth
+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 insynth.util.logging.HasLogger
+
+import lesynth.examples.Example
+
+abstract class ExampleRunner(inputExamples: Seq[Example]) extends HasLogger {
+
+ private var _examples = ArrayBuffer(inputExamples: _*)
+ 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/lesynth/examples/Example.scala b/src/main/scala/lesynth/examples/Example.scala
new file mode 100644
index 0000000000000000000000000000000000000000..10a47e48c8b75512acf6ca74105769b0cf112c6d
--- /dev/null
+++ b/src/main/scala/lesynth/examples/Example.scala
@@ -0,0 +1,13 @@
+package lesynth
+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/lesynth/InputExamples.scala b/src/main/scala/lesynth/examples/InputExamples.scala
similarity index 97%
rename from src/main/scala/lesynth/InputExamples.scala
rename to src/main/scala/lesynth/examples/InputExamples.scala
index 71c9db244bb0374c268e2a28c604ebcb0335f1b8..8d0f314ab7c849a20c21161f4b6a67637ef3855f 100755
--- a/src/main/scala/lesynth/InputExamples.scala
+++ b/src/main/scala/lesynth/examples/InputExamples.scala
@@ -1,4 +1,5 @@
package lesynth
+package examples
import leon.{ Main => LeonMain, Reporter, DefaultReporter, SilentReporter, Settings, LeonContext }
import leon.solvers.{ Solver, TimeoutSolver }
@@ -18,14 +19,11 @@ import insynth.leon.loader.{ HoleExtractor, LeonLoader }
object InputExamples {
def getDataGenInputExamples(evaluator: Evaluator, p: Problem,
- numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]])
- (argumentIds: Seq[Identifier], loader: LeonLoader) = {
-
+ numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]]) = {
val models = findModels(p.pc, evaluator, numOfModels, numOfTries,
forcedFreeVars = _forcedFreeVars)
models.toList
-
}
def getFixedInputExamples(argumentIds: Seq[Identifier], loader: LeonLoader) = {
diff --git a/src/main/scala/lesynth/ranking/Candidate.scala b/src/main/scala/lesynth/ranking/Candidate.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3305b1832e2d4ccb9df515a79950d456ad041981
--- /dev/null
+++ b/src/main/scala/lesynth/ranking/Candidate.scala
@@ -0,0 +1,112 @@
+package lesynth
+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 insynth.structures.Weight._
+import 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, funDef: FunDef) = {
+ getFreshResultVariable(funDef.getBody.getType)
+ candidatePairs map {
+ pair =>
+ DefaultCandidate(pair.getSnippet, bodyBuilder(pair.getSnippet), pair.getWeight, funDef)
+ }
+ }
+
+ def makeCodeGenCandidates(candidatePairs: IndexedSeq[Output], bodyBuilder: Expr => Expr, funDef: FunDef) = {
+ getFreshResultVariable(funDef.getBody.getType)
+ candidatePairs map {
+ pair =>
+ CodeGenCandidate(pair.getSnippet, bodyBuilder(pair.getSnippet), pair.getWeight, funDef)
+ }
+ }
+}
+
+abstract class Candidate(weight: Weight) {
+ def getExpr: Expr
+
+ def prepareExpression: Expr
+
+ def getWeight = weight
+}
+
+case class DefaultCandidate(expr: Expr, bodyExpr: Expr, weight: Weight, holeFunDef: FunDef)
+ 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)
+
+ // body can contain (self-)recursive calls
+ Let(resFresh, bodyExpr,
+ replace(Map(ResultVariable() -> Variable(resFresh)),
+ matchToIfThenElse(holeFunDef.getPostcondition)))
+ }
+
+ override def prepareExpression = {
+ // set appropriate body to the function for the correct evaluation due to recursive calls
+ holeFunDef.body = Some(bodyExpr)
+
+// finest("going to evaluate candidate for: " + holeFunDef)
+// finest("going to evaluate candidate for: " + expressionToEvaluate)
+ expressionToEvaluate
+ }
+}
+
+case class CodeGenCandidate(expr: Expr, bodyExpr: Expr, weight: Weight, holeFunDef: FunDef)
+ extends Candidate(weight) with HasLogger {
+ import Candidate._
+
+ override def getExpr = expr
+
+ lazy val (expressionToEvaluate, newFunDef) = {
+ import TreeOps._
+
+ val newFunId = FreshIdentifier("tempIntroducedFunction")
+ val newFun = new FunDef(newFunId, holeFunDef.returnType, holeFunDef.args)
+ newFun.precondition = holeFunDef.precondition
+ newFun.postcondition = holeFunDef.postcondition
+
+ def replaceFunDef(expr: Expr) = expr match {
+ case FunctionInvocation(`holeFunDef`, args) =>
+ Some(FunctionInvocation(newFun, args))
+ case _ => None
+ }
+ val newBody = searchAndReplace(replaceFunDef)(bodyExpr)
+
+ newFun.body = Some(newBody)
+
+ assert(bodyExpr.getType != Untyped)
+ val resFresh = freshResultVariable//.setType(expr.getType)
+
+ // body can contain (self-)recursive calls
+ (Let(resFresh, newBody,
+ replace(Map(ResultVariable() -> Variable(resFresh)),
+ matchToIfThenElse(newFun.getPostcondition)))
+ ,
+ newFun)
+ }
+
+ override def prepareExpression = {
+// finest("going to evaluate candidate for: " + holeFunDef)
+// finest("going to evaluate candidate for: " + expressionToEvaluate)
+ expressionToEvaluate
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/Evaluation.scala b/src/main/scala/lesynth/ranking/Evaluation.scala
similarity index 59%
rename from src/main/scala/lesynth/Evaluation.scala
rename to src/main/scala/lesynth/ranking/Evaluation.scala
index 93093979d158648310f749d733b33c9009862ba6..fb044ab9cf9620ad8b5078c21d899e1be227e75b 100644
--- a/src/main/scala/lesynth/Evaluation.scala
+++ b/src/main/scala/lesynth/ranking/Evaluation.scala
@@ -1,44 +1,40 @@
package lesynth
+package ranking
-import scala.util.Random
+import lesynth.evaluation._
-import leon.purescala.Trees.{ Variable => LeonVariable, _ }
-import leon.purescala.Common.Identifier
-
-case class Evaluation(examples: Seq[Map[Identifier, Expr]], exampleFun: (Expr, Map[Identifier, Expr])=>Boolean, candidates: Seq[Expr],
- exampleRunner: ExampleRunner) {
+case class Evaluation(exampleRunner: ExampleRunner) {
- val random: Random = new Random(System.currentTimeMillis)
-
- // keep track of evaluations
+ // keep track of which examples to evaluate next
var nextExamples: Map[Int, Int] = Map()
+ // keep track of evaluation results
var evaluations = Map[Int, Array[Boolean]]()
-// def evalAvailable(expr: Int) = {
-// val nextExample = nextExamples.getOrElse(expr, 0)
-// if (nextExample >= examples.size) false
-// else true
-// }
-
+ def numberOfExamples = exampleRunner.examples.size
+
def evaluate(exprInd: Int) = {
numberOfEvaluationCalls += 1
+ // get next example index and update
val nextExample = nextExamples.getOrElse(exprInd, 0)
- if (nextExample >= examples.size) throw new RuntimeException("Exhausted examples for " + exprInd)
-
+ if (nextExample >= numberOfExamples) throw new RuntimeException("Exhausted examples for " + exprInd)
nextExamples += (exprInd -> (nextExample + 1))
-
- val example = examples(nextExample)
- val expressionToCheck = candidates(exprInd)
- val result = exampleFun(expressionToCheck, example)
- val evalArray = evaluations.getOrElse(exprInd, Array.ofDim[Boolean](examples.size))
+ 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)
@@ -57,13 +53,10 @@ case class Evaluation(examples: Seq[Map[Identifier, Expr]], exampleFun: (Expr, M
// }
// }
- def evaluate(expression: Int, example: Int => Boolean) = {
- example(expression)
- }
-
- def getNumberOfExamples = examples.size
-
- var numberOfEvaluationCalls = 0
- def getEfficiencyRatio = numberOfEvaluationCalls.toFloat / (examples.size * evaluations.size)
-
+// 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/lesynth/Ranker.scala b/src/main/scala/lesynth/ranking/Ranker.scala
similarity index 76%
rename from src/main/scala/lesynth/Ranker.scala
rename to src/main/scala/lesynth/ranking/Ranker.scala
index 13742f2c2a94c8e800519a0ca7a7cf56e928507e..5f8e969f7fdb8bcb7550c38f449669a90720ae4d 100644
--- a/src/main/scala/lesynth/Ranker.scala
+++ b/src/main/scala/lesynth/ranking/Ranker.scala
@@ -1,18 +1,21 @@
package lesynth
+package ranking
import util.control.Breaks._
import scala.collection._
import leon.purescala.Trees.{ Variable => LeonVariable, _ }
-class Ranker(candidates: Seq[Expr], evaluation: Evaluation, printStep: Boolean = false) {
+class Ranker(candidates: IndexedSeq[Candidate], evaluation: Evaluation, checkTimeout: (() => Boolean) = { () => false }, printStep: Boolean = false) {
- var rankings: Array[Int] = (0 until candidates.size).toArray
+ 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 candidates.size)
- yield (i, (0, evaluation.getNumberOfExamples))) toMap
+ (for (i <- 0 until candidatesSize)
+ yield (i, (0, evaluation.numberOfExamples))) toMap
def getKMax(k: Int) = {
@@ -43,18 +46,18 @@ class Ranker(candidates: Seq[Expr], evaluation: Evaluation, printStep: Boolean =
def bubbleDown(ind: Int): Unit = {
if (compare(rankings(ind), rankings(ind + 1))) {
swap(ind, ind + 1)
- if (ind < candidates.size-2)
+ if (ind < candidatesSize-2)
bubbleDown(ind + 1)
}
}
- var numberLeft = candidates.size
+ var numberLeft = candidatesSize
def getMax = {
- numberLeft = candidates.size
+ numberLeft = candidatesSize
- while (numberLeft > 1) {
+ while (numberLeft > 1 && !checkTimeout()) {
evaluate(rankings(0))
@@ -81,8 +84,7 @@ class Ranker(candidates: Seq[Expr], evaluation: Evaluation, printStep: Boolean =
println("***: " + numberLeft)
}
- candidates(rankings(0))
-
+ candidates(rankings(0))
}
// def getVerifiedMax = {
@@ -109,6 +111,9 @@ class Ranker(candidates: Seq[Expr], evaluation: Evaluation, printStep: Boolean =
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)
@@ -117,7 +122,8 @@ class Ranker(candidates: Seq[Expr], evaluation: Evaluation, printStep: Boolean =
val median2 = (tuple2._1 + tuple2._2).toFloat/2
/*median1 < median2 || median1 == median2 && */
- tuple1._2 < tuple2._2 || tuple1._2 == tuple2._2 && median1 < median2
+ tuple1._2 < tuple2._2 || tuple1._2 == tuple2._2 &&
+ (heurCompare(x, y) || median1 < median2)
}
def rankOf(expr: Int) =
@@ -128,7 +134,7 @@ class Ranker(candidates: Seq[Expr], evaluation: Evaluation, printStep: Boolean =
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.getNumberOfExamples) map {
+ ((0 until evaluation.numberOfExamples) map {
x => if (x < tuple._2._1) '+' else if (x >= tuple._2._2) '-' else '_'
}).mkString).mkString("\n")
diff --git a/src/main/scala/lesynth/Refiner.scala b/src/main/scala/lesynth/refinement/Refiner.scala
similarity index 65%
rename from src/main/scala/lesynth/Refiner.scala
rename to src/main/scala/lesynth/refinement/Refiner.scala
index 2fc2cbd4424546dffeeaa4c61a268897ea150788..3c385858b9dee01ff908dfa0c92c910fdfb69b15 100755
--- a/src/main/scala/lesynth/Refiner.scala
+++ b/src/main/scala/lesynth/refinement/Refiner.scala
@@ -1,7 +1,9 @@
package lesynth
+package refinement
import leon.purescala.Trees._
-import leon.purescala.Definitions.{ Program, VarDecl, FunDef, VarDecls }
+import leon.purescala.TypeTrees._
+import leon.purescala.Definitions._
import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
import leon.plugin.ExtractionPhase
@@ -10,42 +12,47 @@ import insynth.leon.loader.LeonLoader
import insynth.util.logging.HasLogger
-class Refiner(program: Program, hole: Hole, holeFunDef: FunDef) extends HasLogger {
+class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) extends HasLogger {
import Globals._
def isAvoidable(expr: Expr, funDefArgs: List[Identifier]) = {
fine(
"Results for refining " + expr + ", are: " +
- " ,recurentExpression == expr " + (recurentExpression == expr) +
" ,isCallAvoidableBySize(expr) " + isCallAvoidableBySize(expr, funDefArgs) +
" ,hasDoubleRecursion(expr) " + hasDoubleRecursion(expr) +
- " ,isOperatorAvoidable(expr) " + isOperatorAvoidable(expr)
+ " ,isOperatorAvoidable(expr) " + isOperatorAvoidable(expr) +
+ " ,isUnecessaryInstanceOf(expr) " + isUnecessaryInstanceOf(expr)
)
- recurentExpression == expr || isCallAvoidableBySize(expr, funDefArgs) || hasDoubleRecursion(expr) || isOperatorAvoidable(expr)
+ isCallAvoidableBySize(expr, funDefArgs) || hasDoubleRecursion(expr) ||
+ isOperatorAvoidable(expr) || isUnecessaryInstanceOf(expr)
}
//val holeFunDef = Globals.holeFunDef
- val recurentExpression: Expr =
+ val pureRecurentExpression: Expr =
if (holeFunDef.hasBody) {
- FunctionInvocation(holeFunDef, holeFunDef.args map { varDecl => Variable(varDecl.id) })
+ FunctionInvocation(holeFunDef, holeFunDef.args 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")
+ true
+ case FunctionInvocation(`holeFunDef`, args) =>
+ (0 /: (args zip holeFunDef.args.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]) = {
-
- def isBadInvocation(expr2: Expr) = expr2 match {
- case FunctionInvocation(`holeFunDef`, args) =>
- (0 /: (args zip holeFunDef.args.map(_.id))) {
- case (res, (arg, par)) if res == 0 => isLess(arg, par)
- case (res, _) => res
- } >= 0
- case _ => false
- }
-
+
import TreeOps.treeCatamorphism
treeCatamorphism(
@@ -73,7 +80,7 @@ class Refiner(program: Program, hole: Hole, holeFunDef: FunDef) extends HasLogge
getSize(arg, 0)
}
-
+
def hasDoubleRecursion(expr: Expr) = {
var found = false
@@ -107,4 +114,25 @@ class Refiner(program: Program, hole: Hole, holeFunDef: FunDef) extends HasLogge
case _ => false
}
+ def isUnecessaryInstanceOf(expr: Expr) = {
+ def isOfClassType(exp: Expr, classDef: ClassTypeDef) =
+ expr.getType match {
+ case tpe: ClassType => tpe.classDef == classDef
+ case _ => false
+ }
+ expr match {
+ case CaseClassInstanceOf(classDef, innerExpr)
+ if isOfClassType(innerExpr, classDef) =>
+ true
+ case CaseClassInstanceOf(classDef, v@Variable(id)) => {
+ val possibleTypes = refiner.getPossibleTypes(id)
+ if (possibleTypes.size == 1)
+ possibleTypes.head.classDef == classDef
+ else
+ false
+ }
+ case _ => false
+ }
+ }
+
}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/VariableRefiner.scala b/src/main/scala/lesynth/refinement/VariableRefiner.scala
similarity index 97%
rename from src/main/scala/lesynth/VariableRefiner.scala
rename to src/main/scala/lesynth/refinement/VariableRefiner.scala
index cc3b664cdcc55776ba82e799926b2e5901840fc8..42fc251cb60f2e9f63f955786c24f2012cf5922c 100755
--- a/src/main/scala/lesynth/VariableRefiner.scala
+++ b/src/main/scala/lesynth/refinement/VariableRefiner.scala
@@ -1,4 +1,5 @@
package lesynth
+package refinement
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
@@ -30,6 +31,8 @@ class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variabl
}
}
+ def getPossibleTypes(id: Identifier) = variableRefinements(id)
+
def checkRefinements(expr: Expr, allDeclarations: List[Declaration]) =
// check for refinements
getIdAndClassDef(expr) match {
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
index 0b28a99862e21c238eb87eb85ed8166d39944bb0..f69216abe431699b2ee54711722d8477204c26e4 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -7,12 +7,14 @@ import leon.purescala.TypeTrees._
import leon.purescala.TreeOps._
import leon.purescala.Extractors._
import leon.purescala.Definitions._
-import leon.purescala.DataGen.findModels
import leon.synthesis._
import leon.solvers.{ Solver, TimeoutSolver }
import leon.evaluators.CodeGenEvaluator
-import InputExamples._
+import lesynth.examples.InputExamples._
+import lesynth.evaluation._
+
+import leon.StopwatchCollections
case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abduction synthesis (two phase).") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -38,21 +40,24 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
val freshResVar = Variable(freshResID)
val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
- def getInputExamples =
- getDataGenInputExamples(codeGenEval, p,
- 40, 2000, Some(holeFunDef.args.map(_.id))
- ) _
+ def getInputExamples = {
+ () => getDataGenInputExamples(codeGenEval, p,
+ 20, 2000, Some(p.as)
+ )
+ }
+ val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 500)
+
holeFunDef.postcondition = Some(replace(
Map(givenVariable.toVariable -> ResultVariable().setType(holeFunDef.returnType)), p.phi))
holeFunDef.precondition = Some(p.pc)
val synthesizer = new SynthesizerForRuleExamples(
- solver, program, desiredType, holeFunDef, p, sctx, freshResVar,
- 40, 2, 1,
+ solver, program, desiredType, holeFunDef, p, sctx, freshResVar, evaluationStrategy,
+ 20, 1, 1,
reporter = reporter,
introduceExamples = getInputExamples,
- numberOfTestsInIteration = 50,
+ numberOfTestsInIteration = 25,
numberOfCheckInIteration = 2
)
@@ -60,6 +65,7 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
case EmptyReport => RuleApplicationImpossible
case fr@FullReport(resFunDef, _) =>
println(fr.summaryString)
+ println("Compilation time: " + StopwatchCollections.get("Compilation").getMillis)
RuleSuccess(Solution(resFunDef.getPrecondition, Set.empty, resFunDef.body.get))
}
} catch {