From 48f388c88a81ea9369f585656cda31f25ae7cff7 Mon Sep 17 00:00:00 2001
From: Ivan Kuraj <ivan.kuraj@epfl.ch>
Date: Mon, 10 Jun 2013 03:50:29 +0200
Subject: [PATCH] Changed the verification condition generation, mofidified
filtered of candidates, implemented verifier timeout as evidence of validity
---
.../insynth/leon/loader/HoleExtractor.scala | 3 -
.../scala/insynth/leon/loader/PreLoader.scala | 2 +-
src/main/scala/lesynth/Globals.scala | 22 -
.../scala/lesynth/SynthesizerExamples.scala | 639 ++++++++----------
src/main/scala/lesynth/Verifier.scala | 136 ++++
.../evaluation/CodeGenExampleRunner.scala | 13 +-
.../evaluation/DefaultExampleRunner.scala | 12 +-
.../evaluation/EvaluationStrategy.scala | 49 +-
.../lesynth/evaluation/ExampleRunner.scala | 1 +
.../scala/lesynth/ranking/Evaluation.scala | 9 +-
src/main/scala/lesynth/ranking/Ranker.scala | 6 +-
.../scala/lesynth/refinement/Refiner.scala | 30 +-
.../ConditionAbductionSynthesisTwoPhase.scala | 10 +-
13 files changed, 503 insertions(+), 429 deletions(-)
delete mode 100644 src/main/scala/lesynth/Globals.scala
create mode 100644 src/main/scala/lesynth/Verifier.scala
diff --git a/src/main/scala/insynth/leon/loader/HoleExtractor.scala b/src/main/scala/insynth/leon/loader/HoleExtractor.scala
index 10ee46b04..2a917c338 100644
--- a/src/main/scala/insynth/leon/loader/HoleExtractor.scala
+++ b/src/main/scala/insynth/leon/loader/HoleExtractor.scala
@@ -25,9 +25,6 @@ class HoleExtractor(program: Program, hole: Hole) {
if foundHole;
val argDeclarations = funDef.args map { makeArgumentDeclaration(_) }
) {
- // hack
- //Globals.holeFunDef = funDef
-
foundHoleCount+=1
return Some((funDef, argDeclarations.toList ++ declarations))
diff --git a/src/main/scala/insynth/leon/loader/PreLoader.scala b/src/main/scala/insynth/leon/loader/PreLoader.scala
index b362af6be..3f5f2d1ac 100644
--- a/src/main/scala/insynth/leon/loader/PreLoader.scala
+++ b/src/main/scala/insynth/leon/loader/PreLoader.scala
@@ -121,7 +121,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
def getGreaterThan =
// case GreaterThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
makeDeclaration(
- makeNAE( ">", { case List(left, right) => LessThan( left, right ) } ),
+ makeNAE( ">", { case List(left, right) => GreaterThan( left, right ) } ),
FunctionType( List(Int32Type, Int32Type), BooleanType )
)
diff --git a/src/main/scala/lesynth/Globals.scala b/src/main/scala/lesynth/Globals.scala
deleted file mode 100644
index a42136a79..000000000
--- a/src/main/scala/lesynth/Globals.scala
+++ /dev/null
@@ -1,22 +0,0 @@
-package lesynth
-
-import leon.purescala.Common.Identifier
-import leon.purescala.Definitions.{ Program, FunDef }
-import leon.purescala.Trees.{ Expr, Error, Hole }
-
-object Globals {
-
- //var bodyAndPostPlug: (Expr => Expr) = _
-
- //var timeout = 2
-
- var allSolved: Option[Boolean] = None
-
-// var program: Option[Program] = None
-//
- var hole: Hole = _
-//
- var asMap: Map[Identifier, Expr] = _
-//
-// var holeFunDef: FunDef = _
-}
diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/lesynth/SynthesizerExamples.scala
index 1a3037f86..08b9977b9 100755
--- a/src/main/scala/lesynth/SynthesizerExamples.scala
+++ b/src/main/scala/lesynth/SynthesizerExamples.scala
@@ -1,15 +1,14 @@
package lesynth
-import scala.collection.mutable.{ Map => MutableMap }
-import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{ ArrayBuffer, PriorityQueue }
+import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
+import scala.collection.mutable.{ PriorityQueue, ArrayBuffer, HashSet }
+import scala.util.control.Breaks._
import leon.{ Reporter, DefaultReporter, SilentReporter, LeonContext }
import leon.Main.processOptions
-import leon.solvers.{ Solver, TimeoutSolver }
-import leon.solvers.z3.{ FairZ3Solver }
-import leon.verification.AnalysisPhase
+import leon.solvers._
+import leon.solvers.z3._
import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
import leon.purescala.Trees.{ Variable => LeonVariable, _ }
@@ -29,9 +28,6 @@ import insynth.engine._
import insynth.reconstruction.Output
import insynth.util.logging.HasLogger
-import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
-import scala.util.control.Breaks._
-
import lesynth.examples._
import lesynth.evaluation._
import lesynth.ranking._
@@ -42,18 +38,18 @@ import SynthesisInfo.Action._
class SynthesizerForRuleExamples(
// some synthesis instance information
- val solver: Solver,
+ val mainSolver: Solver,
+ var solver: IncrementalSolver,
val program: Program,
val desiredType: LeonType,
val holeFunDef: FunDef,
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 = 1, // seconds
+// leonTimeout: Int = 1, // seconds
analyzeSynthesizedFunctionOnly: Boolean = false,
showLeonOutput: Boolean = false,
reporter: Reporter = new DefaultReporter,
@@ -67,220 +63,55 @@ class SynthesizerForRuleExamples(
numberOfCheckInIteration: Int = 5,
exampleRunnerSteps: Int = 4000) extends HasLogger {
- val fileName: String = "noFileName"
-
info("Synthesizer:")
- info("fileName: %s".format(fileName))
info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
- info("leonTimeout: %d".format(leonTimeout))
- //info("examples: " + examples.mkString(", "))
+// info("leonTimeout: %d".format(leonTimeout))
info("holeFunDef: %s".format(holeFunDef))
info("problem: %s".format(problem.toString))
-
- private var hole: Hole = _
- // initial declarations
- private var allDeclarations: List[Declaration] = _
+
+ // 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 = _
- private var refiner: Filter = _
- //private var solver: Solver = _
- private var ctx: LeonContext = _
- private var initialPrecondition: Expr = _
+ private var hole: Hole = _
+ // initial declarations
+ private var allDeclarations: List[Declaration] = _
- 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
- private var found = false
+ // heuristics that guide the search
+ private var variableRefiner: VariableRefiner = _
+ private var refiner: Filter = _
+ type FilterSet = HashSet[Expr]
+ private var seenBranchExpressions: FilterSet = new FilterSet()
+ // 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 accumulatingPrecondition: Expr = _
// accumulate the final expression of the hole
private var accumulatingExpression: Expr => Expr = _
- //private var accumulatingExpressionMatch: Expr => Expr = _
// information about the synthesis
private val synthInfo = new SynthesisInfo
-
- // filtering/ranking with examples support
- var exampleRunner: ExampleRunner = _
- var gatheredExamples: ArrayBuffer[Example] = _
-
- def analyzeProgram = {
-
- synthInfo.start(Verification)
- 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) {
- bodyAndPost
- } else {
- Implies(matchToIfThenElse(holeFunDef.precondition.get), bodyAndPost)
- }
-
- withPrec
- }
-
- val reporter = //new DefaultReporter
- new SilentReporter
- val args =
- if (analyzeSynthesizedFunctionOnly)
- Array(fileName, "--timeout=" + leonTimeout, "--functions=" + holeFunDef.id.name)
- else
- Array(fileName, "--timeout=" + leonTimeout)
- finest("Leon context array: " + args.mkString(","))
- ctx = processOptions(reporter, args.toList)
- 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)
- finest("Solver said " + Globals.allSolved + " for " + theExpr)
- //interactivePause
-
- // measure time
- synthInfo.end
- fine("Analysis took of theExpr: " + synthInfo.last)
- }
-
- // TODO return boolean (do not do unecessary analyze)
- def generateCounterexamples(program: Program, funDef: FunDef, number: Int): (Seq[Map[Identifier, Expr]], Expr) = {
-
- 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
- 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
- analyzeProgram
-
- // check if solver could solved this instance
- if (Globals.allSolved == Some(false) && !Globals.asMap.isEmpty) {
-
- info("Found counterexample: " + Globals.asMap)
- // add current counterexample
- maps :+= Globals.asMap
-
- // prevent this counterexample to re-occur
- val precAddition = Not(And(Globals.asMap map { case (id, value) => Equals(LeonVariable(id), value) } toSeq))
- precondition = And(Seq(precondition, precAddition))
- // update precondition
- funDef.precondition = Some(precondition)
- } else
- changed = false
-
- ind += 1
- }
-
- // val temptime = System.currentTimeMillis - temp
- // fine("Generation of counter-examples took: " + temptime)
- // verTime += temptime
-
- // 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) }
- }
-
- def synthesizeBooleanExpressions = {
- info("Invoking synthesis for condition expressions")
- synthInfo.start(Generation)
- 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
- }
-
- 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 = {
-
- hole = Hole(desiredType)
-
- // TODO lose this - globals are bad
- Globals.allSolved = None
-
- // create new insynth object
- loader = new LeonLoader(program, hole, problem.as, false)
- inSynth = new InSynth(loader, true)
- // save all declarations seen
- allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
- // make conditions synthesizer
- inSynthBoolean = new InSynth(allDeclarations, BooleanType, true)
-
- // funDef of the hole
- fine("postcondition is: " + holeFunDef.getPostcondition)
- fine("declarations we see: " + allDeclarations.map(_.toString).mkString("\n"))
- // interactivePause
-
- // accumulate precondition for the remaining branch to synthesize
- accumulatingPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
- // save initial precondition
- initialPrecondition = accumulatingPrecondition
- // accumulate the final expression of the hole
- accumulatingExpression = (finalExp: Expr) => finalExp
- //accumulatingExpressionMatch = accumulatingExpression
-
- // each variable of super type can actually have a subtype
- // get sine declaration maps to be able to refine them
- variableRefiner = new VariableRefiner(loader.directSubclassesMap,
- loader.variableDeclarations, loader.classMap, reporter)
-
- // calculate cases that should not happen
- refiner = new Filter(program, holeFunDef, variableRefiner)
-
- gatheredExamples = ArrayBuffer(introduceExamples().map(Example(_)): _*)
- info("Introduced examples: " + gatheredExamples.mkString("\t"))
- }
+
+ val verifier = new Verifier(solver, problem, holeFunDef, synthInfo)
+ import verifier._
def synthesize: Report = {
- reporter.info("Synthesis called on file: " + fileName)
+ reporter.info("Synthesis called on files: " + synthesisContext.context.files)
// profile
synthInfo start Synthesis
@@ -288,18 +119,16 @@ class SynthesizerForRuleExamples(
reporter.info("Initializing synthesizer: ")
reporter.info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
reporter.info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
- reporter.info("leonTimeout: %d".format(leonTimeout))
+// reporter.info("leonTimeout: %d".format(leonTimeout))
initialize
reporter.info("Synthesizer initialized")
// keeps status of validity
- var keepGoing = Globals.allSolved match {
- case Some(true) => false
- case _ => true
- }
+ var keepGoing = true
// update flag in case of time limit overdue
def checkTimeout =
if (synthesisContext.shouldStop.get) {
+ reporter.info("Timeout occured, stopping this synthesis rules")
keepGoing = false
true
} else
@@ -351,16 +180,14 @@ class SynthesizerForRuleExamples(
out => {
val snip = out.getSnippet
fine("enumerated: " + snip)
- (seenBranchExpressions contains snip.toString) || refiner.isAvoidable(snip, problem.as)
+ (seenBranchExpressions contains snip) ||
+ 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
@@ -373,7 +200,7 @@ class SynthesizerForRuleExamples(
info("Ranking candidates...")
synthInfo.start(Action.Evaluation)
- val maxCandidate = ranker.getMax
+ val (maxCandidate, maxCandidateInd) = ranker.getMax
synthInfo.end
// restore original precondition and body
@@ -387,26 +214,34 @@ class SynthesizerForRuleExamples(
// 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)) {
+ // 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 failedExamples = (gatheredExamples zip evalArray).filterNot {
+ case (ex, result) =>
+ result
+ }.map(_._1)
+ fine("Failed examples for the maximum candidate: " + failedExamples.mkString(", "))
+// interactivePause
+
+ val currentCandidateExpr = maxCandidate.getExpr
+ if (tryToSynthesizeBranch(currentCandidateExpr, failedExamples)) {
noBranchFoundIteration = 0
+
+ // after a branch is synthesized it makes sense to consider candidates that previously failed
+ seenBranchExpressions = new FilterSet()
+
break
+ } else {
+ // add to seen if branch was not found for it
+ seenBranchExpressions += currentCandidateExpr
}
- // interactivePause
+// interactivePause
totalExpressionsTested += numberOfTested
noBranchFoundIteration += 1
@@ -414,9 +249,6 @@ class SynthesizerForRuleExamples(
} // 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
@@ -453,7 +285,116 @@ class SynthesizerForRuleExamples(
EmptyReport
}
- def tryToSynthesizeBranch(snippetTree: Expr): Boolean = {
+ 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) = analyzeProgram
+
+ // 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) }
+ }
+
+ def synthesizeBooleanExpressions = {
+ info("Invoking synthesis for condition expressions")
+ synthInfo.start(Generation)
+ 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
+ }
+
+ 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
+ hole = Hole(desiredType)
+ loader = new LeonLoader(program, hole, problem.as, false)
+ inSynth = new InSynth(loader, true)
+ // save all declarations seen
+ allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+ // make conditions synthesizer
+ inSynthBoolean = new InSynth(allDeclarations, BooleanType, true)
+
+ // funDef of the hole
+ fine("postcondition is: " + holeFunDef.getPostcondition)
+ fine("declarations we see: " + allDeclarations.map(_.toString).mkString("\n"))
+ // interactivePause
+
+ // accumulate precondition for the remaining branch to synthesize
+ accumulatingPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+ // save initial precondition
+ initialPrecondition = accumulatingPrecondition
+ // accumulate the final expression of the hole
+ accumulatingExpression = (finalExp: Expr) => finalExp
+ //accumulatingExpressionMatch = accumulatingExpression
+
+ // each variable of super type can actually have a subtype
+ // get sine declaration maps to be able to refine them
+ variableRefiner = new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap, reporter)
+
+ // calculate cases that should not happen
+ refiner = new Filter(program, holeFunDef, variableRefiner)
+
+ gatheredExamples = ArrayBuffer(introduceExamples().map(Example(_)): _*)
+ info("Introduced examples: " + gatheredExamples.mkString("\t"))
+ }
+
+ def tryToSynthesizeBranch(snippetTree: Expr, failedExamples: Seq[Example]): Boolean = {
// replace hole in the body with the whole if-then-else structure, with current snippet tree
val oldBody = holeFunDef.getBody
val newBody = accumulatingExpression(snippetTree)
@@ -465,27 +406,28 @@ class SynthesizerForRuleExamples(
snippetTree.setType(hole.desiredType)
//holeFunDef.getBody.setType(hole.desiredType)
-
- // TODO spare one analyzing step
- // analyze the 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
- found = true
-
- reporter.info("Wooooooow we have a winner!")
- reporter.info("************************************")
- reporter.info("*********And the winner is**********")
- reporter.info(accumulatingExpression(snippetTree).toString)
- reporter.info("************************************")
-
- return true
+
+ if (failedExamples.isEmpty) {
+ // check if solver could solved this instance
+ fine("Analyzing program for funDef:" + holeFunDef)
+ val (result, map) = analyzeProgram
+ info("Solver returned: " + result)
+
+ if (result) {
+ // mark the branch found
+ found = true
+
+ reporter.info("Wooooooow we have a winner!")
+ reporter.info("************************************")
+ reporter.info("*********And the winner is**********")
+ reporter.info(accumulatingExpression(snippetTree).toString)
+ reporter.info("************************************")
+
+ return true
+ } else {
+ gatheredExamples += Example(map)
+ }
}
// store appropriate values here, will be update in a finally branch
@@ -503,34 +445,9 @@ class SynthesizerForRuleExamples(
if (collectCounterExamplesFromLeon)
gatheredExamples ++= maps.map(Example(_))
- // this should not be possible
- // val keepGoing = Globals.allSolved match {
- // case Some(true) => false
- // case _ => true
- // }
- //
- // // if no counterexamples and all are solved, we are done
- // if (maps.isEmpty && !keepGoing) {
- // // mark the branch found
- // found = true
- //
- // println("Wooooooow we have a winner!")
- // println("************************************")
- // println("*********And the winner is**********")
- // println(accumulatingExpression(snippetTree))
- // println("************************************")
- //
- // return true
- // }
-
- //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)
-
+ {
// reconstruct (only defined number of boolean expressions)
val innerSnippets = synthesizeBooleanExpressions
// just printing of expressions
@@ -539,10 +456,11 @@ class SynthesizerForRuleExamples(
case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet
}).mkString("\n"))
+ // 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
@@ -550,8 +468,11 @@ class SynthesizerForRuleExamples(
) {
fine("boolean snippet is: " + innerSnippetTree)
info("Trying: " + innerSnippetTree + " as a condition.")
-
- val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, maps)
+ val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(
+ snippetTree, innerSnippetTree,
+ // counter examples represent those for which candidate fails
+ (failedExamples.map(_.map) ++ maps)
+ )
// if precondition found
if (innerFound) {
@@ -565,7 +486,6 @@ class SynthesizerForRuleExamples(
}
return true
}
-
} // iterating over all boolean solutions
reporter.info("No precondition found for branch expression: " + snippetTree)
@@ -584,90 +504,91 @@ class SynthesizerForRuleExamples(
}
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))
// new expression should not be false
- val notFalseEquivalence = Not(newCondition)
- val notFalseSolveReturn = solver.solve(notFalseEquivalence)
- fine("solve for not false returned: " + notFalseSolveReturn)
-
- notFalseSolveReturn match {
- case Some(true) =>
- (false, None)
- case None =>
- (false, None)
- // nothing here
- // here, our expression is not contradictory, continue
- case Some(false) =>
- // 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
- }
-
- // found a boolean snippet, break
- (true, preconditionToRestore)
- } else {
- // reset funDef and continue with next boolean snippet
- val preconditionToRestore = Some(accumulatingPrecondition)
- (false, preconditionToRestore)
+// val notFalseEquivalence = Not(newCondition)
+ val isSatisfiable =
+ checkSatisfiabilityNoMod(newCondition)
+ fine("Is " + newCondition + " satisfiable: " + isSatisfiable)
+
+ // continue if our expression is not contradictory
+ if (isSatisfiable) {
+ // 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
+ val (valid, map) = analyzeProgram
+ // program is valid, we have a branch
+ if (valid) {
+ // 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
}
- } else {
- fine("solver filtered out the precondition (does not imply counterexamples)")
- (false, None)
+
+ // found a boolean snippet, break
+ (true, preconditionToRestore)
+ } else {
+ // collect (add) counterexamples from leon
+ if (collectCounterExamplesFromLeon && !map.isEmpty)
+ gatheredExamples ++= (map :: Nil).map(Example(_))
+
+ // reset funDef and continue with next boolean snippet
+ val preconditionToRestore = Some(accumulatingPrecondition)
+ (false, preconditionToRestore)
}
- //solveReturn match { (for implying counterexamples)
- } // notFalseSolveReturn match {
+ } else {
+ fine("Solver filtered out the precondition (does not imply counterexamples)")
+ (false, None)
+ }
+ } else {// if (!isItAContradiction)
+ fine("Solver filtered out the precondition (is not sound)")
+ (false, None)
+ }
}
}
+
\ No newline at end of file
diff --git a/src/main/scala/lesynth/Verifier.scala b/src/main/scala/lesynth/Verifier.scala
new file mode 100644
index 000000000..fdf4217d8
--- /dev/null
+++ b/src/main/scala/lesynth/Verifier.scala
@@ -0,0 +1,136 @@
+package lesynth
+
+import leon.solvers._
+import leon.purescala.Common._
+import leon.purescala.Trees._
+import leon.purescala.Extractors._
+import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees._
+import leon.purescala.Definitions._
+import leon.synthesis._
+
+import insynth.util.logging._
+
+class Verifier(solver: IncrementalSolver, p: Problem, funDef: FunDef, synthInfo: SynthesisInfo)
+ extends HasLogger {
+
+ import SynthesisInfo.Action._
+
+ def analyzeProgram = {
+ synthInfo.start(Verification)
+
+ // create an expression to verify
+ val theExpr = generateVerificationCondition(funDef.getBody)
+
+ solver.push
+ val valid = checkValidity(theExpr)
+ val map = solver.getModel
+ solver.pop()
+
+ // measure time
+ synthInfo.end
+ fine("Analysis took of theExpr: " + synthInfo.last)
+ (valid, map)
+ }
+
+ def generateVerificationCondition(body: Expr) = {
+
+ // replace recursive calls with fresh variables
+ case class Replacement(id: Identifier, exprReplaced: FunctionInvocation) {
+ def getMapping: Map[Expr, Expr] = {
+ val funDef = exprReplaced.funDef
+ val pairList = (ResultVariable(), id.toVariable) ::
+ (funDef.args.map(_.toVariable).toList zip exprReplaced.args)
+ pairList.toMap
+ }
+ }
+
+ var isThereARecursiveCall = false
+ var replacements = List[Replacement]()
+
+ // traverse the expression and check for recursive calls
+ def replaceRecursiveCalls(expr: Expr) = expr match {
+ case funInv@FunctionInvocation(`funDef`, args) => {
+ isThereARecursiveCall = true
+ val inductId = FreshIdentifier("induct", true).setType(funDef.returnType)
+ replacements :+= Replacement(inductId, funInv)
+ Some(inductId.toVariable)
+ }
+ case _ => None
+ }
+
+ val newBody = searchAndReplace(replaceRecursiveCalls)(body)
+
+ val resFresh = FreshIdentifier("result", true).setType(newBody.getType)
+ val bodyAndPost =
+ Let(
+ resFresh, newBody,
+ replace(Map(ResultVariable() -> resFresh.toVariable), matchToIfThenElse(funDef.getPostcondition))
+ )
+
+ val precondition = if( isThereARecursiveCall ) {
+ And( funDef.getPrecondition :: replacements.map( r => replace(r.getMapping, funDef.getPostcondition)) )
+ } else
+ funDef.getPrecondition
+
+ val withPrec =
+ Implies(matchToIfThenElse(precondition), bodyAndPost)
+
+ fine("Generated verification condition: " + withPrec)
+ withPrec
+ }
+
+ 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 validity.")
+ true
+ }
+ }
+
+ 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 validity.")
+ true
+ }
+ }
+
+ 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
+ }
+ }
+
+// private def checkSatisfiability = {
+//
+// }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
index 3da1dc0bc..72f42392b 100644
--- a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
+++ b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
@@ -86,7 +86,7 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
try {
evalClosure(args) match {
case Successful(BooleanLiteral(true)) =>
- fine("Eval succeded: EvaluationSuccessful(true)")
+ fine("EvaluationSuccessful(true) for " + args)
true
case m =>
fine("Eval failed: " + m)
@@ -106,9 +106,14 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
val closure = compile(prec, funDef.args.map(_.id))
- _examples = _examples filter {
- evaluate(closure, _)
- }
+ val (newTransformed, newExamples) = ((_examples zip examples) filter {
+ case ((transformedExample, _)) =>
+ evaluate(closure, transformedExample)
+ }).unzip
+
+ _examples = newTransformed
+ examples = newExamples
+
fine("New counterExamples.size: " + examples.size)
}
diff --git a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala b/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
index c11570107..c9b13a866 100644
--- a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
+++ b/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
@@ -62,9 +62,15 @@ case class DefaultExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
def filter(prec: Expr) = {
entering("filter(" + prec + ")")
finest("Old counterExamples.size: " + examples.size)
- _examples = _examples filter {
- evaluate(prec, _)
- }
+
+ val (newTransformed, newExamples) = ((_examples zip examples) filter {
+ case ((exMap, _)) =>
+ evaluate(prec, exMap)
+ }).unzip
+
+ _examples = newTransformed
+ examples = newExamples
+
finest("New counterExamples.size: " + examples.size)
}
diff --git a/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala b/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
index 55780f628..36ed41c3c 100644
--- a/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
+++ b/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
@@ -16,10 +16,28 @@ import insynth.util.logging._
import lesynth.ranking._
import lesynth.examples._
-trait EvaluationStrategy {
+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, funDef: FunDef, ctx: LeonContext,
@@ -27,12 +45,16 @@ case class DefaultEvaluationStrategy(program: Program, funDef: FunDef, ctx: Leon
var exampleRunner: ExampleRunner = _
+ var evaluation: Evaluation = _
+
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)
+ logCounts(candidates, inputExamples)
+
// printing candidates and pass counts
fine("Ranking with examples: " + inputExamples.mkString(", "))
fine( {
@@ -46,12 +68,14 @@ case class DefaultEvaluationStrategy(program: Program, funDef: FunDef, ctx: Leon
logString
})
- val evaluation = Evaluation(exampleRunner)
+ evaluation = Evaluation(exampleRunner)
new Ranker(candidates, evaluation)
}
override def getExampleRunner = exampleRunner
+
+ override def getEvaluation = evaluation
}
case class CodeGenEvaluationStrategy(program: Program, funDef: FunDef, ctx: LeonContext,
@@ -59,6 +83,8 @@ case class CodeGenEvaluationStrategy(program: Program, funDef: FunDef, ctx: Leon
var exampleRunner: ExampleRunner = _
+ var evaluation: Evaluation = _
+
override def getRanker(candidatePairs: IndexedSeq[Output], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]) = {
val candidates = Candidate.makeCodeGenCandidates(candidatePairs, bodyBuilder, funDef)
@@ -71,24 +97,15 @@ case class CodeGenEvaluationStrategy(program: Program, funDef: FunDef, ctx: Leon
val params = CodeGenEvalParams(maxFunctionInvocations = maxSteps, checkContracts = true)
exampleRunner = CodeGenExampleRunner(newProgram, funDef, ctx, candidates, inputExamples, params)
+
+ 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
- })
-
- val evaluation = Evaluation(exampleRunner)
+ evaluation = Evaluation(exampleRunner)
new Ranker(candidates, evaluation)
}
override def getExampleRunner = exampleRunner
+
+ override def getEvaluation = evaluation
}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/evaluation/ExampleRunner.scala b/src/main/scala/lesynth/evaluation/ExampleRunner.scala
index bb78d02ca..c93a8fa99 100644
--- a/src/main/scala/lesynth/evaluation/ExampleRunner.scala
+++ b/src/main/scala/lesynth/evaluation/ExampleRunner.scala
@@ -15,6 +15,7 @@ import lesynth.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 = {
diff --git a/src/main/scala/lesynth/ranking/Evaluation.scala b/src/main/scala/lesynth/ranking/Evaluation.scala
index fb044ab9c..7186b689d 100644
--- a/src/main/scala/lesynth/ranking/Evaluation.scala
+++ b/src/main/scala/lesynth/ranking/Evaluation.scala
@@ -6,18 +6,23 @@ import lesynth.evaluation._
case class Evaluation(exampleRunner: ExampleRunner) {
// keep track of which examples to evaluate next
- var nextExamples: Map[Int, Int] = Map()
+ 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.getOrElse(exprInd, 0)
+ val nextExample = nextExamples(exprInd)//OrElse(exprInd, 0)
if (nextExample >= numberOfExamples) throw new RuntimeException("Exhausted examples for " + exprInd)
nextExamples += (exprInd -> (nextExample + 1))
diff --git a/src/main/scala/lesynth/ranking/Ranker.scala b/src/main/scala/lesynth/ranking/Ranker.scala
index 5f8e969f7..0137c6a98 100644
--- a/src/main/scala/lesynth/ranking/Ranker.scala
+++ b/src/main/scala/lesynth/ranking/Ranker.scala
@@ -17,10 +17,6 @@ class Ranker(candidates: IndexedSeq[Candidate], evaluation: Evaluation, checkTim
(for (i <- 0 until candidatesSize)
yield (i, (0, evaluation.numberOfExamples))) toMap
- def getKMax(k: Int) = {
-
- }
-
def evaluate(ind: Int) {
val tuple = tuples(ind)
val expr = ind
@@ -84,7 +80,7 @@ class Ranker(candidates: IndexedSeq[Candidate], evaluation: Evaluation, checkTim
println("***: " + numberLeft)
}
- candidates(rankings(0))
+ (candidates(rankings(0)), rankings(0))
}
// def getVerifiedMax = {
diff --git a/src/main/scala/lesynth/refinement/Refiner.scala b/src/main/scala/lesynth/refinement/Refiner.scala
index 3c385858b..4ccc2f274 100755
--- a/src/main/scala/lesynth/refinement/Refiner.scala
+++ b/src/main/scala/lesynth/refinement/Refiner.scala
@@ -1,6 +1,8 @@
package lesynth
package refinement
+import scala.collection.mutable._
+
import leon.purescala.Trees._
import leon.purescala.TypeTrees._
import leon.purescala.Definitions._
@@ -9,25 +11,35 @@ import leon.purescala.TreeOps
import leon.plugin.ExtractionPhase
import insynth.leon.loader.LeonLoader
-
import insynth.util.logging.HasLogger
class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) extends HasLogger {
- import Globals._
+
+ // caching of previously filtered expressions
+ type FilterSet = HashSet[Expr]
+ private var seenBranchExpressions: FilterSet = new FilterSet()
def isAvoidable(expr: Expr, funDefArgs: List[Identifier]) = {
- fine(
+ finest(
"Results for refining " + expr + ", are: " +
" ,isCallAvoidableBySize(expr) " + isCallAvoidableBySize(expr, funDefArgs) +
" ,hasDoubleRecursion(expr) " + hasDoubleRecursion(expr) +
" ,isOperatorAvoidable(expr) " + isOperatorAvoidable(expr) +
" ,isUnecessaryInstanceOf(expr) " + isUnecessaryInstanceOf(expr)
)
- isCallAvoidableBySize(expr, funDefArgs) || hasDoubleRecursion(expr) ||
- isOperatorAvoidable(expr) || isUnecessaryInstanceOf(expr)
+ if (seenBranchExpressions contains expr) {
+ true
+ } else {
+ val result = isCallAvoidableBySize(expr, funDefArgs) || hasDoubleRecursion(expr) ||
+ isOperatorAvoidable(expr) || isUnecessaryInstanceOf(expr)
+
+ // cache results
+ if (result) {
+ seenBranchExpressions += expr
+ }
+ result
+ }
}
-
- //val holeFunDef = Globals.holeFunDef
val pureRecurentExpression: Expr =
if (holeFunDef.hasBody) {
@@ -38,7 +50,7 @@ class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) ext
def isBadInvocation(expr2: Expr) = expr2 match {
case `pureRecurentExpression` =>
- fine("pure recurrent expression detected")
+ fine("Pure recurrent expression detected: " + pureRecurentExpression)
true
case FunctionInvocation(`holeFunDef`, args) =>
(0 /: (args zip holeFunDef.args.map(_.id))) {
@@ -71,7 +83,7 @@ class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) ext
case CaseClass(caseClassDef, head :: tail :: Nil) => getSize(tail, size + 1)
case CaseClass(caseClassDef, Nil) => 1
case v: Variable => if (v.id == variable) size else {
- fine("variable IDs do not match: " + v.id.uniqueName + " and " + variable.uniqueName )
+// finest("Refiner: Variable IDs do not match: " + v.id.uniqueName + " and " + variable.uniqueName )
1
}
case _ => //throw new RuntimeException("Could not match " + arg + " in getSize")
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
index f69216abe..a0fd751bb 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -24,7 +24,7 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
List(new RuleInstantiation(p, this, SolutionBuilder.none, "Condition abduction") {
def apply(sctx: SynthesisContext): RuleApplicationResult = {
try {
- val solver = new TimeoutSolver(sctx.solver, 1000L)
+ val solver = new TimeoutSolver(sctx.solver, 500L)
val program = sctx.program
val reporter = sctx.reporter
@@ -42,19 +42,19 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
def getInputExamples = {
() => getDataGenInputExamples(codeGenEval, p,
- 20, 2000, Some(p.as)
+ 50, 2000, Some(p.as)
)
}
- val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 500)
+ val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 1000)
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, evaluationStrategy,
- 20, 1, 1,
+ solver, solver.getNewSolver, program, desiredType, holeFunDef, p, sctx, evaluationStrategy,
+ 20, 1,
reporter = reporter,
introduceExamples = getInputExamples,
numberOfTestsInIteration = 25,
--
GitLab