From d088c3d10d85dd56e434b1170cf0956e23865678 Mon Sep 17 00:00:00 2001
From: Ivan Kuraj <ivan.kuraj@epfl.ch>
Date: Mon, 24 Jun 2013 23:56:12 -0400
Subject: [PATCH] Refactored verifier into concrete and timeout one, added
generation of input examples with fuzzying, expression filter detects
according to expression structure, added some benchmarks for the paper
---
.../scala/insynth/leon/loader/PreLoader.scala | 49 +-
.../scala/lesynth/SynthesizerExamples.scala | 134 ++-
.../evaluation/CodeGenExampleRunner.scala | 9 +-
.../lesynth/examples/InputExamples.scala | 37 +-
.../{Refiner.scala => Filter.scala} | 34 +-
.../lesynth/refinement/VariableRefiner.scala | 2 +-
...ConditionAbductionSynthesisImmediate.scala | 89 +-
.../ConditionAbductionSynthesisTwoPhase.scala | 12 +-
.../AbstractVerifier.scala} | 90 +-
.../verification/RelaxedVerifier.scala | 66 ++
.../scala/lesynth/verification/Verifier.scala | 68 ++
src/test/scala/lesynth/AnalyzerTest.scala | 49 --
src/test/scala/lesynth/EnumerationTest.scala | 75 ++
src/test/scala/lesynth/EvaluationTest.scala | 328 ++++++++
src/test/scala/lesynth/FilterTest.scala | 235 ++++++
src/test/scala/lesynth/RefinerTest.scala | 209 -----
.../TryOutSynthesizerExamplesTest.scala | 672 ---------------
src/test/scala/lesynth/TryOutTest.scala | 639 ---------------
.../lesynth/TryOutTestWithFiltering.scala | 768 ------------------
.../scala/lesynth/VariableRefinerTest.scala | 2 +
src/test/scala/lesynth/VerifierTest.scala | 90 ++
src/test/scala/lesynth/util/Scaffold.scala | 96 +++
src/test/scala/lesynth/util/TestConfig.scala | 40 +
src/test/scala/lesynth/util/Utils.scala | 33 +
testcases/lesynth/BinarySearchTree.scala | 94 ---
testcases/lesynth/InsertionSortFull.scala | 51 --
.../lesynth/InsertionSortHoleInsert.scala | 54 --
testcases/lesynth/InsertionSortHoleSort.scala | 53 --
testcases/lesynth/ListOperations.scala | 45 -
testcases/lesynth/ListOperationsHole.scala | 24 -
testcases/lesynth/ListOperationsHole2.scala | 24 -
testcases/lesynth/MergeSortHole.scala | 81 --
.../BatchedQueue/BatchedQueueCheckf.scala | 32 +-
.../BatchedQueue/BatchedQueueSnoc.scala | 41 +-
.../BatchedQueue/BatchedQueueTail.scala | 59 +-
.../synthesis/MergeSort/MergeSortSort.scala | 2 +-
.../lesynth/synthesis/Other/Addresses.scala | 85 ++
.../Other/AddressesMakeAddressBook.scala | 21 +-
.../AddressesMakeAddressBookWithHelpers.scala | 16 +-
.../Other/AddressesMergeAddressBooks.scala | 23 +-
40 files changed, 1515 insertions(+), 3016 deletions(-)
rename src/main/scala/lesynth/refinement/{Refiner.scala => Filter.scala} (84%)
rename src/main/scala/lesynth/{Verifier.scala => verification/AbstractVerifier.scala} (51%)
create mode 100644 src/main/scala/lesynth/verification/RelaxedVerifier.scala
create mode 100644 src/main/scala/lesynth/verification/Verifier.scala
delete mode 100644 src/test/scala/lesynth/AnalyzerTest.scala
create mode 100644 src/test/scala/lesynth/EnumerationTest.scala
create mode 100644 src/test/scala/lesynth/EvaluationTest.scala
create mode 100644 src/test/scala/lesynth/FilterTest.scala
delete mode 100644 src/test/scala/lesynth/RefinerTest.scala
delete mode 100755 src/test/scala/lesynth/TryOutSynthesizerExamplesTest.scala
delete mode 100644 src/test/scala/lesynth/TryOutTest.scala
delete mode 100644 src/test/scala/lesynth/TryOutTestWithFiltering.scala
create mode 100644 src/test/scala/lesynth/VerifierTest.scala
create mode 100644 src/test/scala/lesynth/util/Scaffold.scala
create mode 100644 src/test/scala/lesynth/util/TestConfig.scala
create mode 100644 src/test/scala/lesynth/util/Utils.scala
delete mode 100644 testcases/lesynth/BinarySearchTree.scala
delete mode 100644 testcases/lesynth/InsertionSortFull.scala
delete mode 100644 testcases/lesynth/InsertionSortHoleInsert.scala
delete mode 100644 testcases/lesynth/InsertionSortHoleSort.scala
delete mode 100644 testcases/lesynth/ListOperations.scala
delete mode 100644 testcases/lesynth/ListOperationsHole.scala
delete mode 100644 testcases/lesynth/ListOperationsHole2.scala
delete mode 100644 testcases/lesynth/MergeSortHole.scala
create mode 100644 testcases/lesynth/synthesis/Other/Addresses.scala
diff --git a/src/main/scala/insynth/leon/loader/PreLoader.scala b/src/main/scala/insynth/leon/loader/PreLoader.scala
index 3f5f2d1ac..ba25d9468 100644
--- a/src/main/scala/insynth/leon/loader/PreLoader.scala
+++ b/src/main/scala/insynth/leon/loader/PreLoader.scala
@@ -35,35 +35,35 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
def getAnd =
// case And(args) if args.isEmpty => BooleanLiteral(true)
makeDeclaration(
- makeNAE("And", { case List(arg1, arg2) => And( List(arg1, arg2) ) }),
+ makeNAE("And", (args: List[Expr]) => And( args )),
FunctionType( List(BooleanType, BooleanType), BooleanType )
- )
+ )
def getNot =
// case Not(arg) => rec(ctx, arg) match {
makeDeclaration(
- makeNAE( "Not", { case List(arg) => Not( arg ) } ),
+ makeNAE( "Not", (args: List[Expr]) => Not( args.head ) ),
FunctionType( List(BooleanType), BooleanType )
)
def getOr =
// case Or(args) if args.isEmpty => BooleanLiteral(false)
makeDeclaration(
- makeNAE( "Or", { case List(arg1, arg2) => Or( List(arg1, arg2) ) } ),
+ makeNAE( "Or", (args: List[Expr]) => Or( args ) ),
FunctionType( List(BooleanType, BooleanType), BooleanType )
)
def getImplies =
// case Implies(l, r) => (rec(ctx, l), rec(ctx, r)) match {
makeDeclaration(
- makeNAE( "=>", { case List(left, right) => Implies( left, right ) } ),
+ makeNAE( "=>", (args: List[Expr]) => Implies( args(0), args(1) ) ),
FunctionType( List(BooleanType, BooleanType), BooleanType )
)
def getIff =
//case Iff(le, re) => (rec(ctx, le), rec(ctx, re)) match {
makeDeclaration(
- makeNAE( "<=>", { case List(left, right) => Iff( left, right ) } ),
+ makeNAE( "<=>", (args: List[Expr]) => Iff( args(0), args(1) ) ),
FunctionType( List(BooleanType, BooleanType), BooleanType )
)
@@ -72,7 +72,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
yieldDeclarationForTypes(listOfInstanceTypes) {
x: LeonType =>
makeDeclaration(
- makeNAE( "=", { case List(left, right) => Equals( left, right ) } ),
+ makeNAE( "=", (args: List[Expr]) => Equals( args(0), args(1) ) ),
FunctionType( List(x, x), BooleanType ),
true
)
@@ -81,32 +81,32 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
def getArithmeticOps = {
// case Plus(l, r) => (rec(ctx, l), rec(ctx, r)) match {
makeDeclaration(
- makeNAE( "+", { case List(left, right) => Plus( left, right ) } ),
+ makeNAE( "+", (args: List[Expr]) => Plus( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), Int32Type )
) ::
// case Minus(l, r) => (rec(ctx, l), rec(ctx, r)) match {
makeDeclaration(
- makeNAE( "-", { case List(left, right) => Minus( left, right ) } ),
+ makeNAE( "-", (args: List[Expr]) => Minus( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), Int32Type )
) ::
// case UMinus(e) => rec(ctx, e) match {
makeDeclaration(
- makeNAE( "UMinus", { case List(e) => UMinus( e ) } ),
+ makeNAE( "UMinus", (args: List[Expr]) => UMinus( args.head ) ),
FunctionType( List(Int32Type), Int32Type )
) ::
//case Times(l, r) => (rec(ctx, l), rec(ctx, r)) match {
makeDeclaration(
- makeNAE( "*", { case List(left, right) => Times( left, right ) } ),
+ makeNAE( "*", (args: List[Expr]) => Times( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), Int32Type )
) ::
// case Division(l, r) => (rec(ctx, l), rec(ctx, r)) match {
makeDeclaration(
- makeNAE( "/", { case List(left, right) => Division( left, right ) } ),
+ makeNAE( "/", (args: List[Expr]) => Division( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), Int32Type )
) ::
// case Modulo(l,r) => (rec(ctx,l), rec(ctx,r)) match {
makeDeclaration(
- makeNAE( "%", { case List(left, right) => Modulo( left, right ) } ),
+ makeNAE( "%", (args: List[Expr]) => Modulo( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), Int32Type )
) :: Nil
}
@@ -114,28 +114,28 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
def getLessThan =
// case LessThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
makeDeclaration(
- makeNAE( "<", { case List(left, right) => LessThan( left, right ) } ),
+ makeNAE( "<", (args: List[Expr]) => LessThan( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), BooleanType )
)
def getGreaterThan =
// case GreaterThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
makeDeclaration(
- makeNAE( ">", { case List(left, right) => GreaterThan( left, right ) } ),
+ makeNAE( ">", (args: List[Expr]) => GreaterThan( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), BooleanType )
)
def getLessEquals =
// case LessEquals(l,r) => (rec(ctx,l), rec(ctx,r)) match {
makeDeclaration(
- makeNAE( "<=", { case List(left, right) => LessEquals( left, right ) } ),
+ makeNAE( "<=", (args: List[Expr]) => LessEquals( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), BooleanType )
)
def getGreaterEquals =
// case GreaterEquals(l,r) => (rec(ctx,l), rec(ctx,r)) match {
makeDeclaration(
- makeNAE( ">=", { case List(left, right) => GreaterEquals( left, right ) } ),
+ makeNAE( ">=", (args: List[Expr]) => GreaterEquals( args(0), args(1) ) ),
FunctionType( List(Int32Type, Int32Type), BooleanType )
)
@@ -146,7 +146,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
yieldDeclarationForTypes(listOfInstanceTypes) {
x: LeonType =>
makeDeclaration(
- makeNAE( "SetUnion", { case List(left, right) => SetUnion( left, right ) } ),
+ makeNAE( "SetUnion", (args: List[Expr]) => SetUnion( args(0), args(1) ) ),
FunctionType( List(SetType(x), SetType(x)), SetType(x) )
)
} ++
@@ -154,7 +154,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
yieldDeclarationForTypes(listOfInstanceTypes) {
x: LeonType =>
makeDeclaration(
- makeNAE( "SetIntersection", { case List(left, right) => SetIntersection( left, right ) } ),
+ makeNAE( "SetIntersection", (args: List[Expr]) => SetIntersection( args(0), args(1) ) ),
FunctionType( List(SetType(x), SetType(x)), SetType(x) )
)
} ++
@@ -162,7 +162,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
yieldDeclarationForTypes(listOfInstanceTypes) {
x: LeonType =>
makeDeclaration(
- makeNAE( "SetDifference", { case List(left, right) => SetDifference( left, right ) } ),
+ makeNAE( "SetDifference", (args: List[Expr]) => SetDifference( args(0), args(1) ) ),
FunctionType( List(SetType(x), SetType(x)), SetType(x) )
)
} ++
@@ -170,7 +170,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
yieldDeclarationForTypes(listOfInstanceTypes) {
x: LeonType =>
makeDeclaration(
- makeNAE( "ElementOfSet", { case List(left, right) => ElementOfSet( left, right ) } ),
+ makeNAE( "ElementOfSet", (args: List[Expr]) => ElementOfSet( args(0), args(1) ) ),
FunctionType( List(x, SetType(x)), BooleanType )
)
} ++
@@ -178,7 +178,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
yieldDeclarationForTypes(listOfInstanceTypes) {
x: LeonType =>
makeDeclaration(
- makeNAE( "SetCardinality", { case List(set) => SetCardinality( set ) } ),
+ makeNAE( "SetCardinality", (args: List[Expr]) => SetCardinality( args(0) ) ),
FunctionType( List(SetType(x)), Int32Type )
)
}
@@ -196,7 +196,10 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
yieldDeclarationForTypes(listOfInstanceTypes) {
x: LeonType =>
makeDeclaration(
- makeNAE( "If", { case List(cond: Expr, then: Expr, elze: Expr) => IfExpr(cond, then, elze) } ),
+ makeNAE( "If", (args: List[Expr]) => args match {
+ case List(cond, then, elze) => IfExpr(cond, then, elze)
+ case _ => throw new RuntimeException
+ }),
FunctionType( List(BooleanType, x, x), x )
)
}
diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/lesynth/SynthesizerExamples.scala
index 08b9977b9..03d696d12 100755
--- a/src/main/scala/lesynth/SynthesizerExamples.scala
+++ b/src/main/scala/lesynth/SynthesizerExamples.scala
@@ -21,7 +21,7 @@ import leon.evaluators._
import leon.synthesis.{ Problem, SynthesisContext }
import insynth.interfaces.Declaration
-import insynth.InSynth
+import insynth.{ Solver => _, _ }
import insynth.leon.loader._
import insynth.leon._
import insynth.engine._
@@ -76,8 +76,8 @@ class SynthesizerForRuleExamples(
// objects used in the synthesis
private var loader: LeonLoader = _
- private var inSynth: InSynth = _
- private var inSynthBoolean: InSynth = _
+ private var inSynth: InSynthTemp = _
+ private var inSynthBoolean: InSynthTemp = _
private var hole: Hole = _
// initial declarations
private var allDeclarations: List[Declaration] = _
@@ -92,6 +92,7 @@ class SynthesizerForRuleExamples(
private var refiner: Filter = _
type FilterSet = HashSet[Expr]
private var seenBranchExpressions: FilterSet = new FilterSet()
+ private var successfulCandidates = IndexedSeq[Output]()
// filtering/ranking with examples support
var exampleRunner: ExampleRunner = _
@@ -107,7 +108,7 @@ class SynthesizerForRuleExamples(
// information about the synthesis
private val synthInfo = new SynthesisInfo
- val verifier = new Verifier(solver, problem, holeFunDef, synthInfo)
+ val verifier = new RelaxedVerifier(solver, problem, synthInfo)
import verifier._
def synthesize: Report = {
@@ -159,6 +160,7 @@ class SynthesizerForRuleExamples(
reporter.info("# accumulatingPrecondition is: " + accumulatingPrecondition)
reporter.info("# accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
reporter.info("####################################")
+ interactivePause
var numberOfTested = 0
@@ -182,11 +184,16 @@ class SynthesizerForRuleExamples(
fine("enumerated: " + snip)
(seenBranchExpressions contains snip) ||
refiner.isAvoidable(snip, problem.as)
- }).toIndexedSeq
+ }).toIndexedSeq ++
+ // adding previous candidates because they may not be enumerated
+ successfulCandidates
}
- info("Got candidates of size: " + candidates.size +
- " , first 10 of them are: " + candidates.take(10).map(_.getSnippet.toString).mkString(",\t"))
- //interactivePause
+
+// info("Got candidates of size: " + candidates.size +
+// " , first 10 of them are: " + candidates.take(10).map(_.getSnippet.toString).mkString(",\t"))
+ info("Got candidates of size: " + candidates.size)
+ fine("Got candidates: " + candidates.map(_.getSnippet.toString).mkString(",\n"))
+ interactivePause
if (candidates.size > 0) {
// save current precondition and the old body since it will can be mutated during evaluation
@@ -201,6 +208,7 @@ class SynthesizerForRuleExamples(
info("Ranking candidates...")
synthInfo.start(Action.Evaluation)
val (maxCandidate, maxCandidateInd) = ranker.getMax
+ val (passed, failedModulo) = ranker.fullyEvaluate(maxCandidateInd)
synthInfo.end
// restore original precondition and body
@@ -210,8 +218,9 @@ class SynthesizerForRuleExamples(
// check for timeouts
if (!keepGoing) break
- info("Candidate with the most successfull evaluations is: " + maxCandidate)
-// interactivePause
+ info("candidate with the most successfull evaluations is: " + maxCandidate.getExpr +
+ " with pass count " + passed + " out of " + gatheredExamples.size)
+ interactivePause
numberOfTested += batchSize
// get all examples that failed evaluation to filter potential conditions
@@ -231,17 +240,19 @@ class SynthesizerForRuleExamples(
val currentCandidateExpr = maxCandidate.getExpr
if (tryToSynthesizeBranch(currentCandidateExpr, failedExamples)) {
- noBranchFoundIteration = 0
+ //noBranchFoundIteration = 0
// after a branch is synthesized it makes sense to consider candidates that previously failed
seenBranchExpressions = new FilterSet()
+ successfulCandidates +:= candidates(maxCandidateInd)
+// interactivePause
break
} else {
// add to seen if branch was not found for it
seenBranchExpressions += currentCandidateExpr
}
-// interactivePause
+ interactivePause
totalExpressionsTested += numberOfTested
noBranchFoundIteration += 1
@@ -299,7 +310,7 @@ class SynthesizerForRuleExamples(
var ind = 0
while (ind < number && changed) {
// analyze the program
- val (solved, map) = analyzeProgram
+ val (solved, map) = analyzeFunction(holeFunDef)
// check if solver could solved this instance
if (solved == false && !map.isEmpty) {
@@ -330,7 +341,7 @@ class SynthesizerForRuleExamples(
def synthesizeBranchExpressions = {
info("Invoking synthesis for branch expressions")
- synthInfo.profile(Generation) { inSynth.getExpressions(getCurrentBuilder) }
+ synthInfo.profile(Generation) { inSynth.getExpressions(getCurrentBuilder).distinct }
}
def synthesizeBooleanExpressions = {
@@ -338,9 +349,13 @@ class SynthesizerForRuleExamples(
synthInfo.start(Generation)
if (variableRefinedCondition) {
// store for later fetch (will memoize values)
+ fine("Going into boolean synthesis")
+ val stream = inSynthBoolean.getExpressions(getCurrentBuilder)
+ fine("Out of boolean synthesis")
+ println("stream is here!")
booleanExpressionsSaved =
- inSynthBoolean.getExpressions(getCurrentBuilder).
- filterNot(expr => refiner.isAvoidable(expr.getSnippet, problem.as)) take numberOfBooleanSnippets
+ stream.distinct.take(numberOfBooleanSnippets).
+ filterNot(expr => refiner.isAvoidable(expr.getSnippet, problem.as))
// reset flag
variableRefinedCondition = false
}
@@ -363,11 +378,11 @@ class SynthesizerForRuleExamples(
// create new insynth object
hole = Hole(desiredType)
loader = new LeonLoader(program, hole, problem.as, false)
- inSynth = new InSynth(loader, true)
+ inSynth = new InSynthTemp(loader, true)
// save all declarations seen
allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
// make conditions synthesizer
- inSynthBoolean = new InSynth(allDeclarations, BooleanType, true)
+ inSynthBoolean = new InSynthTemp(allDeclarations, BooleanType, true)
// funDef of the hole
fine("postcondition is: " + holeFunDef.getPostcondition)
@@ -384,14 +399,17 @@ class SynthesizerForRuleExamples(
// 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)
+ variableRefiner =
+ new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap, reporter)
+// new VariableSolverRefiner(loader.directSubclassesMap,
+// loader.variableDeclarations, loader.classMap, mainSolver, reporter)
// calculate cases that should not happen
refiner = new Filter(program, holeFunDef, variableRefiner)
gatheredExamples = ArrayBuffer(introduceExamples().map(Example(_)): _*)
- info("Introduced examples: " + gatheredExamples.mkString("\t"))
+ fine("Introduced examples: " + gatheredExamples.mkString("\t"))
}
def tryToSynthesizeBranch(snippetTree: Expr, failedExamples: Seq[Example]): Boolean = {
@@ -411,8 +429,8 @@ class SynthesizerForRuleExamples(
if (failedExamples.isEmpty) {
// check if solver could solved this instance
fine("Analyzing program for funDef:" + holeFunDef)
- val (result, map) = analyzeProgram
- info("Solver returned: " + result)
+ val (result, map) = analyzeFunction(holeFunDef)
+ info("Solver returned: " + result + " with CE " + map)
if (result) {
// mark the branch found
@@ -438,7 +456,7 @@ class SynthesizerForRuleExamples(
holeFunDef.precondition = preconditionToRestore
// get counterexamples
- fine("Going to generating counterexamples: " + holeFunDef)
+ info("Going to generating counterexamples: " + holeFunDef)
val (maps, precondition) = generateCounterexamples(program, holeFunDef, numberOfCounterExamplesToGenerate)
// collect (add) counterexamples from leon
@@ -452,9 +470,10 @@ class SynthesizerForRuleExamples(
val innerSnippets = synthesizeBooleanExpressions
// just printing of expressions
fine(
- ((innerSnippets zip Iterator.range(0, numberOfBooleanSnippets).toStream) map {
+ (innerSnippets.zipWithIndex map {
case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet
}).mkString("\n"))
+ interactivePause
// enumerate synthesized boolean expressions and filter out avoidable ones
for (
@@ -521,19 +540,73 @@ class SynthesizerForRuleExamples(
exampleRunner.evaluateToResult(newCondition, exMapping) match {
case EvaluationResults.Successful(BooleanLiteral(false)) => false
case r =>
- fine("Evaluation result for " + newCondition + " on " + exMapping + " is " + r)
- true
+
+ // TODO take care of this mess
+ val newFunId = FreshIdentifier("tempIntroducedFunction22")
+ val newFun = new FunDef(newFunId, holeFunDef.returnType, holeFunDef.args)
+// newFun.precondition = Some(newCondition)
+ 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 error = Error("Condition flow hit unknown path.")
+ error.setType(snippetTree.getType)
+ val ifInInnermostElse =
+ IfExpr(innerSnippetTree, snippetTree, error)
+
+ import TreeOps._
+ val newBody = searchAndReplace(replaceFunDef)(accumulatingExpression(ifInInnermostElse))
+
+ newFun.body = Some(newBody)
+
+ assert(newBody.getType != Untyped)
+ val resFresh2 = FreshIdentifier("result22", true).setType(newBody.getType)
+
+ val newCandidate =
+ Let(resFresh2, newBody,
+ replace(Map(ResultVariable() -> LeonVariable(resFresh2)),
+ matchToIfThenElse(newFun.getPostcondition)))
+ finest("New fun for Error evaluation: " + newFun)
+// println("new candidate: " + newBody)
+
+ val newProgram = program.copy(mainObject =
+ program.mainObject.copy(defs = newFun +: program.mainObject.defs ))
+// println("new program: " + newProgram)
+
+ val _evaluator = new CodeGenEvaluator(synthesisContext.context, newProgram,
+ _root_.leon.codegen.CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true))
+
+ val res = _evaluator.eval(newCandidate, exMapping)
+ println(res)
+// if (newCandidate.toString contains "tree.value < value")
+// interactivePause
+
+// interactivePause
+ res match {
+ case EvaluationResults.RuntimeError("Condition flow hit unknown path.") => false
+ case EvaluationResults.Successful(BooleanLiteral(innerRes)) => !innerRes
+ case _ => true
+ }
+
+// fine("Evaluation result for " + newCondition + " on " + exMapping + " is " + r)
+// true
}
case _ => true
}
fine("implyCounterExamples: " + implyCounterExamples)
-
+// interactivePause
+
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
+ val (valid, map) = analyzeFunction(holeFunDef)
// program is valid, we have a branch
if (valid) {
// we found a branch
@@ -550,6 +623,7 @@ class SynthesizerForRuleExamples(
})
accumulatingExpression = newAccumulatingExpression
+ val currentBranchCondition = And(Seq(accumulatingPrecondition, innerSnippetTree))
// update accumulating precondition
fine("updating accumulatingPrecondition")
@@ -559,7 +633,7 @@ class SynthesizerForRuleExamples(
// set to set new precondition
val preconditionToRestore = Some(accumulatingPrecondition)
- val variableRefinementResult = variableRefiner.checkRefinements(innerSnippetTree, allDeclarations)
+ val variableRefinementResult = variableRefiner.checkRefinements(innerSnippetTree, currentBranchCondition, allDeclarations)
if (variableRefinementResult._1) {
info("Variable is refined.")
allDeclarations = variableRefinementResult._2
diff --git a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
index 72f42392b..269650e6f 100644
--- a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
+++ b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
@@ -47,7 +47,7 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
override def evaluate(candidateInd: Int, exampleInd: Int) = {
val closure = candidateClosures(candidateInd)
- fine("Index evaluate candidate [%d]%s, for [%d]%s.".format(
+ finest("Index evaluate candidate [%d]%s, for [%d]%s.".format(
candidateInd, candidates(candidateInd).prepareExpression, exampleInd, examples(exampleInd)
))
@@ -86,15 +86,15 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
try {
evalClosure(args) match {
case Successful(BooleanLiteral(true)) =>
- fine("EvaluationSuccessful(true) for " + args)
+ finest("EvaluationSuccessful(true) for " + args)
true
case m =>
- fine("Eval failed: " + m)
+ finest("Eval failed: " + m)
false
}
} catch {
case e: StackOverflowError =>
- fine("Eval failed: " + e)
+ finest("Eval failed: " + e)
false
}
}
@@ -127,6 +127,7 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
pair => evaluate(closure, pair._1)
)
+ fine("(passed.size, failed.size): " + (passed.size, failed.size))
(passed.size, passed map (_._2))
}
diff --git a/src/main/scala/lesynth/examples/InputExamples.scala b/src/main/scala/lesynth/examples/InputExamples.scala
index 8d0f314ab..71a186e42 100755
--- a/src/main/scala/lesynth/examples/InputExamples.scala
+++ b/src/main/scala/lesynth/examples/InputExamples.scala
@@ -1,22 +1,21 @@
package lesynth
package examples
-import leon.{ Main => LeonMain, Reporter, DefaultReporter, SilentReporter, Settings, LeonContext }
-import leon.solvers.{ Solver, TimeoutSolver }
-import leon.solvers.z3.{ FairZ3Solver }
-import leon.verification.AnalysisPhase
-import leon.plugin.ExtractionPhase
-import leon.purescala.TypeTrees.{ ClassType, CaseClassType, Int32Type }
-import leon.purescala.Trees.{ IntLiteral, CaseClass }
-import leon.purescala.Definitions.{ FunDef, VarDecls }
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps
import leon.purescala.Common.Identifier
import leon.evaluators.Evaluator
-import leon.purescala.DataGen.findModels
import leon.synthesis.Problem
+import leon.purescala.DataGen
import insynth.leon.loader.{ HoleExtractor, LeonLoader }
object InputExamples {
+ import DataGen._
+
+ val rnd = new scala.util.Random(System.currentTimeMillis)
+ val MAX_INT = 1000
def getDataGenInputExamples(evaluator: Evaluator, p: Problem,
numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]]) = {
@@ -25,6 +24,26 @@ object InputExamples {
models.toList
}
+
+ def getDataGenInputExamplesRandomIntegers(evaluator: Evaluator, p: Problem,
+ numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]],
+ bound: Int = MAX_INT) = {
+ import TreeOps._
+
+ val models = findModels(p.pc, evaluator, numOfModels, numOfTries,
+ forcedFreeVars = _forcedFreeVars)
+
+ def foundInteger(x: Expr) = x match {
+ case _:IntLiteral => Some(IntLiteral(rnd.nextInt(bound)))
+ case _ => None
+ }
+
+ models.toList.map( innerMap =>
+ innerMap.map( innerEl => innerEl match {
+ case (id, expr) => (id, searchAndReplace(foundInteger)(expr))
+ })
+ )
+ }
def getFixedInputExamples(argumentIds: Seq[Identifier], loader: LeonLoader) = {
argumentIds match {
diff --git a/src/main/scala/lesynth/refinement/Refiner.scala b/src/main/scala/lesynth/refinement/Filter.scala
similarity index 84%
rename from src/main/scala/lesynth/refinement/Refiner.scala
rename to src/main/scala/lesynth/refinement/Filter.scala
index 4ccc2f274..a041a49dc 100755
--- a/src/main/scala/lesynth/refinement/Refiner.scala
+++ b/src/main/scala/lesynth/refinement/Filter.scala
@@ -13,25 +13,34 @@ import leon.plugin.ExtractionPhase
import insynth.leon.loader.LeonLoader
import insynth.util.logging.HasLogger
+/**
+ * Class used for filtering out unnecessary candidates during the search
+ */
class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) extends HasLogger {
-
+
// caching of previously filtered expressions
type FilterSet = HashSet[Expr]
private var seenBranchExpressions: FilterSet = new FilterSet()
+ /**
+ * expr - expression to check
+ * funDefArgs - list of identifiers according to which well ordering is checked
+ */
def isAvoidable(expr: Expr, funDefArgs: List[Identifier]) = {
finest(
"Results for refining " + expr + ", are: " +
" ,isCallAvoidableBySize(expr) " + isCallAvoidableBySize(expr, funDefArgs) +
" ,hasDoubleRecursion(expr) " + hasDoubleRecursion(expr) +
" ,isOperatorAvoidable(expr) " + isOperatorAvoidable(expr) +
- " ,isUnecessaryInstanceOf(expr) " + isUnecessaryInstanceOf(expr)
+ " ,isUnecessaryInstanceOf(expr) " + isUnecessaryInstanceOf(expr) +
+ ", isUnecessaryStructuring(expr) " + isUnecessaryStructuring(expr)
)
if (seenBranchExpressions contains expr) {
true
} else {
val result = isCallAvoidableBySize(expr, funDefArgs) || hasDoubleRecursion(expr) ||
- isOperatorAvoidable(expr) || isUnecessaryInstanceOf(expr)
+ isOperatorAvoidable(expr) || isUnecessaryInstanceOf(expr) ||
+ isUnecessaryStructuring(expr)
// cache results
if (result) {
@@ -115,6 +124,22 @@ class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) ext
found
}
+ // removing checking instance of fields (e.g. x.field.isInstanceOf[..]) - this is deemed unecessary
+ def isUnecessaryStructuring(expr: Expr) = {
+ var found = false
+
+ def isCaseClassSelector(expr: Expr) = expr match {
+ case CaseClassInstanceOf(_, _: CaseClassSelector) =>
+ found = true
+ None
+ case _ => None
+ }
+
+ TreeOps.searchAndReplace(isCaseClassSelector)(expr)
+
+ found
+ }
+
def isOperatorAvoidable(expr: Expr) = expr match {
case And(expr1 :: expr2) if expr1 == expr2 => true
case Or(expr1 :: expr2) if expr1 == expr2 => true
@@ -133,6 +158,9 @@ class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) ext
case _ => false
}
expr match {
+ // if we check instance of an constructor we know that it is a constant
+// case CaseClassInstanceOf(_, _: CaseClass) =>
+// true
case CaseClassInstanceOf(classDef, innerExpr)
if isOfClassType(innerExpr, classDef) =>
true
diff --git a/src/main/scala/lesynth/refinement/VariableRefiner.scala b/src/main/scala/lesynth/refinement/VariableRefiner.scala
index 42fc251cb..910e1fa72 100755
--- a/src/main/scala/lesynth/refinement/VariableRefiner.scala
+++ b/src/main/scala/lesynth/refinement/VariableRefiner.scala
@@ -19,7 +19,7 @@ import insynth.util.logging.HasLogger
// each variable of super type can actually have a subtype
// get sine declaration maps to be able to refine them
class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[LeonDeclaration],
- classMap: Map[Identifier, ClassType], reporter: Reporter = new DefaultReporter) extends HasLogger {
+ classMap: Map[Identifier, ClassType], reporter: Reporter = new SilentReporter) extends HasLogger {
// map from identifier into a set of possible subclasses
private var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = MutableMap.empty
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
index 31acfdbb5..6f7567fd6 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
@@ -7,55 +7,74 @@ import leon.purescala.TypeTrees._
import leon.purescala.TreeOps._
import leon.purescala.Extractors._
import leon.purescala.Definitions._
-import leon.synthesis.{ Rule, RuleInstantiation, SynthesisContext, Problem, Solution }
-import InputExamples._
-import lesynth.SynthesizerForRuleExamples
+import leon.synthesis._
+import leon.solvers.{ Solver, TimeoutSolver }
+import leon.evaluators.CodeGenEvaluator
+
+import lesynth.examples.InputExamples._
+import lesynth.evaluation._
+
+import leon.StopwatchCollections
case object ConditionAbductionSynthesisImmediate extends Rule("Condition abduction synthesis (immediate).") {
- def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
- val solver = sctx.solver
- val program = sctx.program
- val reporter = sctx.reporter
-
- p.xs match {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+
+ p.xs match {
case givenVariable :: Nil =>
+ val solver = new TimeoutSolver(sctx.solver, 500L)
+ val program = sctx.program
+ val reporter = sctx.reporter
+
val desiredType = givenVariable.getType
val holeFunDef = sctx.functionContext.get
-
+
// temporary hack, should not mutate FunDef
val oldPostcondition = holeFunDef.postcondition
val oldPrecondition = holeFunDef.precondition
+
try {
val freshResID = FreshIdentifier("result").setType(holeFunDef.returnType)
val freshResVar = Variable(freshResID)
- 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,
- reporter = reporter,
- introduceExamples = introduceTwoListArgumentsExamples
- )
-
- synthesizer.synthesize match {
- case EmptyReport => None
- case FullReport(resFunDef, _) =>
- List(
- RuleInstantiation.immediateSuccess(p, this,
- Solution(resFunDef.getPrecondition, Set.empty, resFunDef.body.get)
- )
- )
- }
- } finally {
- holeFunDef.postcondition = oldPostcondition
- holeFunDef.precondition = oldPrecondition
+
+ val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
+ def getInputExamples = {
+ () =>
+ getDataGenInputExamples(codeGenEval, p,
+ 200, 6000, Some(p.as)) ++
+ getDataGenInputExamplesRandomIntegers(codeGenEval, p,
+ 200, 6000, Some(p.as) // bound the random geenerator
+ , 5)
+ }
+
+ 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, solver.getNewSolver, program, desiredType, holeFunDef, p, sctx, evaluationStrategy,
+ 20, 1,
+ reporter = reporter,
+ introduceExamples = getInputExamples,
+ numberOfTestsInIteration = 25,
+ numberOfCheckInIteration = 2)
+
+ synthesizer.synthesize match {
+ case EmptyReport => None
+ case FullReport(resFunDef, _) =>
+ List(
+ RuleInstantiation.immediateSuccess(p, this,
+ Solution(resFunDef.getPrecondition, Set.empty, resFunDef.body.get)))
+ }
+ } finally {
+ holeFunDef.postcondition = oldPostcondition
+ holeFunDef.precondition = oldPrecondition
}
case _ =>
- throw new RuntimeException("should not")
+ throw new RuntimeException("Rule is not applicable for more than one output variable.")
Nil
}
-
+
}
}
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
index a0fd751bb..53f557611 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -41,8 +41,13 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
def getInputExamples = {
- () => getDataGenInputExamples(codeGenEval, p,
- 50, 2000, Some(p.as)
+ () =>
+ getDataGenInputExamples(codeGenEval, p,
+ 200, 6000, Some(p.as)) ++
+ getDataGenInputExamplesRandomIntegers(codeGenEval, p,
+ 200, 6000, Some(p.as)
+ // bound the random geenerator
+ ,5
)
}
@@ -81,8 +86,9 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
}
})
case _ =>
- throw new RuntimeException("should not")
+ throw new RuntimeException("Rule is not applicable for more than one output variable.")
Nil
}
+
}
}
diff --git a/src/main/scala/lesynth/Verifier.scala b/src/main/scala/lesynth/verification/AbstractVerifier.scala
similarity index 51%
rename from src/main/scala/lesynth/Verifier.scala
rename to src/main/scala/lesynth/verification/AbstractVerifier.scala
index fdf4217d8..5d14e85b1 100644
--- a/src/main/scala/lesynth/Verifier.scala
+++ b/src/main/scala/lesynth/verification/AbstractVerifier.scala
@@ -11,16 +11,17 @@ import leon.synthesis._
import insynth.util.logging._
-class Verifier(solver: IncrementalSolver, p: Problem, funDef: FunDef, synthInfo: SynthesisInfo)
+abstract class AbstractVerifier(solver: IncrementalSolver, p: Problem,
+ synthInfo: SynthesisInfo)
extends HasLogger {
import SynthesisInfo.Action._
- def analyzeProgram = {
+ def analyzeFunction(funDef: FunDef) = {
synthInfo.start(Verification)
// create an expression to verify
- val theExpr = generateVerificationCondition(funDef.getBody)
+ val theExpr = generateInductiveVerificationCondition(funDef, funDef.getBody)
solver.push
val valid = checkValidity(theExpr)
@@ -29,11 +30,28 @@ class Verifier(solver: IncrementalSolver, p: Problem, funDef: FunDef, synthInfo:
// measure time
synthInfo.end
- fine("Analysis took of theExpr: " + synthInfo.last)
+ fine("Analysis of " + theExpr + ",took :" + synthInfo.last)
(valid, map)
}
+
+ def analyzeFunction(funDef: FunDef, body: Expr) = {
+ synthInfo.start(Verification)
+
+ // create an expression to verify
+ val theExpr = generateInductiveVerificationCondition(funDef, body)
+
+ solver.push
+ val valid = checkValidity(theExpr)
+ val map = solver.getModel
+ solver.pop()
- def generateVerificationCondition(body: Expr) = {
+ // measure time
+ synthInfo.end
+ fine("Analysis of " + theExpr + ",took :" + synthInfo.last)
+ (valid, map)
+ }
+
+ protected def generateInductiveVerificationCondition(funDef: FunDef, body: Expr) = {
// replace recursive calls with fresh variables
case class Replacement(id: Identifier, exprReplaced: FunctionInvocation) {
@@ -45,10 +63,10 @@ class Verifier(solver: IncrementalSolver, p: Problem, funDef: FunDef, synthInfo:
}
}
+ // traverse the expression and check (and replace) recursive calls
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
@@ -61,17 +79,18 @@ class Verifier(solver: IncrementalSolver, p: Problem, funDef: FunDef, synthInfo:
val newBody = searchAndReplace(replaceRecursiveCalls)(body)
+ // build the verification condition
val resFresh = FreshIdentifier("result", true).setType(newBody.getType)
val bodyAndPost =
Let(
resFresh, newBody,
- replace(Map(ResultVariable() -> resFresh.toVariable), matchToIfThenElse(funDef.getPostcondition))
+ replace(Map(ResultVariable() -> resFresh.toVariable), matchToIfThenElse(p.pc))
)
val precondition = if( isThereARecursiveCall ) {
- And( funDef.getPrecondition :: replacements.map( r => replace(r.getMapping, funDef.getPostcondition)) )
+ And( p.phi :: replacements.map( r => replace(r.getMapping, p.pc)) )
} else
- funDef.getPrecondition
+ p.phi
val withPrec =
Implies(matchToIfThenElse(precondition), bodyAndPost)
@@ -80,57 +99,10 @@ class Verifier(solver: IncrementalSolver, p: Problem, funDef: FunDef, synthInfo:
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 checkValidity(expression: Expr): Boolean
- 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
- }
- }
+ def checkValidityNoMod(expression: Expr): Boolean
-// private def checkSatisfiability = {
-//
-// }
+ def checkSatisfiabilityNoMod(expression: Expr): Boolean
}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/verification/RelaxedVerifier.scala b/src/main/scala/lesynth/verification/RelaxedVerifier.scala
new file mode 100644
index 000000000..a1ce8db96
--- /dev/null
+++ b/src/main/scala/lesynth/verification/RelaxedVerifier.scala
@@ -0,0 +1,66 @@
+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 RelaxedVerifier(solver: IncrementalSolver, p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
+ extends AbstractVerifier(solver, p, synthInfo) with HasLogger {
+
+ override def checkValidity(expression: Expr) = {
+ solver.assertCnstr(Not(expression))
+ val solverCheckResult = solver.check
+ fine("Solver said " + solverCheckResult + " for " + expression)
+ solverCheckResult match {
+ case Some(true) =>
+ false
+ case Some(false) =>
+ true
+ case None =>
+ warning("Interpreting None (timeout) as evidence for validity.")
+ true
+ }
+ }
+
+ override def checkValidityNoMod(expression: Expr) = {
+ solver.push
+ solver.assertCnstr(Not(expression))
+ val solverCheckResult = solver.check
+ fine("Solver said " + solverCheckResult + " for " + expression)
+ solver.pop()
+ solverCheckResult match {
+ case Some(true) =>
+ fine("And the model is " + solver.getModel)
+ false
+ case Some(false) =>
+ true
+ case None =>
+ warning("Interpreting None (timeout) as evidence for validity.")
+ true
+ }
+ }
+
+ override def checkSatisfiabilityNoMod(expression: Expr) = {
+ solver.push
+ solver.assertCnstr(expression)
+ val solverCheckResult = solver.check
+ fine("Solver said " + solverCheckResult + " for " + expression)
+ solver.pop()
+ solverCheckResult match {
+ case Some(true) =>
+ true
+ case Some(false) =>
+ false
+ case None =>
+ false
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/verification/Verifier.scala b/src/main/scala/lesynth/verification/Verifier.scala
new file mode 100644
index 000000000..f21277c7c
--- /dev/null
+++ b/src/main/scala/lesynth/verification/Verifier.scala
@@ -0,0 +1,68 @@
+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, synthInfo: SynthesisInfo = new SynthesisInfo)
+ extends AbstractVerifier(solver, p, synthInfo) with HasLogger {
+
+ import SynthesisInfo.Action._
+
+ override def checkValidity(expression: Expr) = {
+ solver.assertCnstr(Not(expression))
+ val solverCheckResult = solver.check
+ fine("Solver said " + solverCheckResult + " for " + expression)
+ solverCheckResult match {
+ case Some(true) =>
+ false
+ case Some(false) =>
+ true
+ case None =>
+ warning("Interpreting None (timeout) as evidence for invalidity.")
+ false
+ }
+ }
+
+ override def checkValidityNoMod(expression: Expr) = {
+ solver.push
+ solver.assertCnstr(Not(expression))
+ val solverCheckResult = solver.check
+ fine("Solver said " + solverCheckResult + " for " + expression)
+ solver.pop()
+ solverCheckResult match {
+ case Some(true) =>
+ fine("And the model is " + solver.getModel)
+ false
+ case Some(false) =>
+ true
+ case None =>
+ warning("Interpreting None (timeout) as evidence for invalidity.")
+ false
+ }
+ }
+
+ override def checkSatisfiabilityNoMod(expression: Expr) = {
+ solver.push
+ solver.assertCnstr(expression)
+ val solverCheckResult = solver.check
+ fine("Solver said " + solverCheckResult + " for " + expression)
+ solver.pop()
+ solverCheckResult match {
+ case Some(true) =>
+ true
+ case Some(false) =>
+ false
+ case None =>
+ false
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/AnalyzerTest.scala b/src/test/scala/lesynth/AnalyzerTest.scala
deleted file mode 100644
index 166da8159..000000000
--- a/src/test/scala/lesynth/AnalyzerTest.scala
+++ /dev/null
@@ -1,49 +0,0 @@
-package lesynth
-
-import scala.util.Random
-
-import org.junit.Assert._
-import org.junit.{ Test, Ignore }
-
-import insynth.leon.HoleFinder
-import insynth.leon.loader.LeonLoader
-
-import _root_.leon.purescala.Trees.{ Hole, IntLiteral }
-import _root_.leon.purescala.TreeOps
-import _root_.leon.evaluators._
-import _root_.leon.{ LeonContext, DefaultReporter, Main }
-import _root_.leon.verification.AnalysisPhase
-
-import insynth.testutil.CommonUtils
-import testutil.TestConfig
-
-class AnalyzerTest {
-
- import TestConfig._
- import CommonUtils._
- import TreeOps._
-
- val rnd = new Random(System.currentTimeMillis())
-
- @Test
- def testModel = {
- val holeFinder = new HoleFinder(lesynthTestDir + "ListOperations.scala")
-
- holeFinder.extract match {
- case Some((prog, hole)) =>
-
- val reporter = new DefaultReporter()
- val args = Array("testcases/insynth/ListOperations.scala", "--timeout=2")
-
- val ctx = Main.processOptions(reporter, args.toList)
-
- val verReport = AnalysisPhase.run(ctx)(prog)
-
- assertTrue(Globals.asMap.size > 0)
-
- case _ =>
- fail("HoleFinder could not extract hole from the program")
- }
- }
-
-}
diff --git a/src/test/scala/lesynth/EnumerationTest.scala b/src/test/scala/lesynth/EnumerationTest.scala
new file mode 100644
index 000000000..3cfd735c5
--- /dev/null
+++ b/src/test/scala/lesynth/EnumerationTest.scala
@@ -0,0 +1,75 @@
+package lesynth
+
+import org.scalatest.FunSuite
+import org.scalatest.matchers.ShouldMatchers._
+
+import leon._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import java.io.{ BufferedWriter, FileWriter, File }
+import leon.evaluators.CodeGenEvaluator
+import leon.purescala.TreeOps
+import leon.purescala.Common._
+import leon.codegen.CodeGenEvalParams
+import leon.purescala.TypeTrees._
+import leon.evaluators.EvaluationResults._
+
+import insynth._
+import insynth.leon._
+import insynth.leon.loader._
+import insynth.engine._
+
+import lesynth.examples.InputExamples
+import lesynth.evaluation.CodeGenEvaluationStrategy
+import lesynth.ranking.Candidate
+import insynth.reconstruction.Output
+import lesynth.examples.Example
+
+import lesynth.util._
+
+class EnumerationTest extends FunSuite {
+
+ import Scaffold._
+ import TestConfig._
+
+ val CANDIDATES_TO_ENUMERATE = 50 :: 100 :: 1000 :: 10000 :: Nil
+
+ val files = List("InsertionSortInsert.scala", "ListConcat.scala", "MergeSortSort.scala",
+ "RedBlackTreeInsert.scala") map { lesynthTestDir + _ }
+
+ ignore("Candidate enumeration duplicates") {
+
+ for (candidatesToEnumerate <- CANDIDATES_TO_ENUMERATE;
+ file <- files;
+ (sctx, funDef, problem) <- forFile(file)) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ expect(1) { problem.xs.size }
+ val resultVariable = problem.xs.head
+ val hole = Hole(resultVariable.getType)
+
+ val loader = new LeonLoader(program, hole, problem.as, false)
+ val inSynth = new InSynth(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ val builder = new InitialEnvironmentBuilder(allDeclarations)
+
+ val outputs = inSynth.getExpressions(builder)
+
+ val taken = outputs.take(candidatesToEnumerate).map(_.getSnippet).toList
+ val takenDistinct = taken.distinct
+ val takenRepeated = taken.filter(snip => taken.count(_ == snip) > 1)
+
+ assert(taken.size == takenDistinct.size, "First " + candidatesToEnumerate +
+ " are not distinct." +
+ "Repeated #" + takenRepeated.size
+ + ": " + takenRepeated.map(snip => snip.toString +
+ " repeats " + taken.count(_ == snip)).mkString("\n")
+ )
+ assert(takenRepeated.isEmpty)
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/EvaluationTest.scala b/src/test/scala/lesynth/EvaluationTest.scala
new file mode 100644
index 000000000..8a60f432b
--- /dev/null
+++ b/src/test/scala/lesynth/EvaluationTest.scala
@@ -0,0 +1,328 @@
+package lesynth
+
+import org.scalatest.FunSuite
+import org.scalatest.matchers.ShouldMatchers._
+
+import leon._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import java.io.{ BufferedWriter, FileWriter, File }
+import leon.evaluators.CodeGenEvaluator
+import leon.purescala.TreeOps
+import leon.purescala.Common._
+import leon.codegen.CodeGenEvalParams
+import leon.purescala.TypeTrees._
+import leon.evaluators.EvaluationResults._
+
+import lesynth.examples.InputExamples
+import lesynth.evaluation.CodeGenEvaluationStrategy
+import lesynth.ranking.Candidate
+import insynth.reconstruction.Output
+import lesynth.examples.Example
+
+import lesynth.util.Scaffold
+
+class EvaluationTest extends FunSuite {
+
+ import Scaffold._
+
+ val mergeSortWithTwoExamples = """
+ import leon.Utils._
+
+ object MergeSort {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst: List, snd: List) extends PairAbs
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x, xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list: List): Int = list match {
+ case Nil() => 0
+ case Cons(x, xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList: List, bList: List, n: Int): Pair = {
+ if (n <= 0) Pair(aList, bList)
+ else
+ bList match {
+ case Nil() => Pair(aList, bList)
+ case Cons(x, xs) => splithelper(Cons(x, aList), xs, n - 1)
+ }
+ } ensuring (res =>
+ contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd)
+ &&
+ size(aList) + size(bList) == size(res.fst) + size(res.snd)
+ )
+
+ def split(list: List): Pair = {
+ splithelper(Nil(), list, 2)
+ } ensuring (res =>
+ contents(list) == contents(res.fst) ++ contents(res.snd)
+ &&
+ size(list) == size(res.fst) + size(res.snd)
+ )
+
+ def merge(aList: List, bList: List): List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x, xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y, ys) =>
+ if (y < x)
+ Cons(y, merge(ys, bList))
+ else
+
+ Cons(x, merge(aList, xs))
+ }
+ }
+ } ensuring (res => contents(res) ==
+ contents(aList) ++ contents(bList) && isSorted(res) &&
+ size(res) == size(aList) + size(bList)
+ )
+
+ def isEmpty(list: List): Boolean = list match {
+ case Nil() => true
+ case Cons(x, xs) => false
+ }
+
+ def sort(list: List): List = choose {
+ (res: List) =>
+ contents(res) == contents(list) && isSorted(res) && size(res) == size(list)
+ } ensuring ( res => contents(res) == contents(list) && isSorted(res) && size(res) == size(list))
+
+ def testFun1(list: List) = {
+ if (isEmpty(list))
+ list
+ else
+ if (isSorted(list))
+ list
+ else
+ splithelper(Nil(), list, size(list)).fst
+ }
+
+ def testFun2(list: List) = {
+ if (isEmpty(list))
+ list
+ else
+ if (isSorted(list))
+ list
+ else
+ merge(sort(split(list).fst), sort(split(list).snd))
+ }
+ }
+ """
+
+ test("codegen strategy") {
+
+ for ((sctx, funDef, problem) <- forProgram(mergeSortWithTwoExamples)) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ expect(1) { problem.xs.size }
+ val resultVariable = problem.xs.head
+ val hole = Hole(resultVariable.getType)
+
+ val codeGenEval = new CodeGenEvaluator(sctx.context, program)
+ def inputExamples =
+ InputExamples.getDataGenInputExamples(codeGenEval, problem,
+ 20, 2000, Some(arguments)).map(Example(_))
+
+ import TreeOps._
+ def replaceFun(expr: Expr) = expr match {
+ case Variable(id) if id.name == "list" =>
+ Some(Variable(arguments.head))
+ // case FunctionInvocation(`funDef`, args) =>
+ // FunctionInvocation(funDef, )
+ case _ => None
+ }
+
+ val body1 =
+ searchAndReplace(replaceFun)(
+ program.definedFunctions.find(_.id.name == "testFun1").get.getBody)
+
+ val body2 =
+ searchAndReplace(replaceFun)(
+ program.definedFunctions.find(_.id.name == "testFun2").get.getBody)
+
+ val evaluationStrategy = new CodeGenEvaluationStrategy(program, funDef, sctx.context, 500)
+
+ val candidates = IndexedSeq(body1, body2) map (b => Output(b, 0))
+
+ val ranker = evaluationStrategy.getRanker(candidates, identity, inputExamples)
+ val exampleRunner = evaluationStrategy.exampleRunner
+
+ val eval1 = (for (ind <- 0 until inputExamples.size) yield {
+ val res = exampleRunner.evaluate(0, ind)
+ (res, exampleRunner.examples(ind))
+ })
+
+ val eval2 = (for (ind <- 0 until inputExamples.size) yield {
+ val res = exampleRunner.evaluate(1, ind)
+ (res, exampleRunner.examples(ind))
+ })
+
+ val message = "Examples: " + inputExamples.mkString(", ")
+ val eval1message = "Evaluation of " + body1 + " yielded: " + eval1.mkString("\n")
+ val eval2message = "Evaluation of " + body2 + " yielded: " + eval2.mkString("\n")
+ assert(inputExamples.size == eval2.count(_._1), message + " " + eval2message)
+ assert(inputExamples.size > eval1.count(_._1), message + " " + eval1message)
+ }
+ }
+
+ test("codegen evaluator") {
+
+ for ((sctx, funDef, problem) <- forProgram(mergeSortWithTwoExamples)) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ expect(1) { problem.xs.size }
+ val resultVariable = problem.xs.head
+ val hole = Hole(resultVariable.getType)
+
+ val codeGenEval = new CodeGenEvaluator(sctx.context, program)
+ def inputExamples =
+ InputExamples.getDataGenInputExamples(codeGenEval, problem,
+ 20, 2000, Some(arguments)).map(Example(_))
+
+ import TreeOps._
+ def replaceFun(expr: Expr) = expr match {
+ case Variable(id) if id.name == "list" =>
+ Some(Variable(arguments.head))
+ case _ => None
+ }
+
+ val body1 =
+ searchAndReplace(replaceFun)(
+ program.definedFunctions.find(_.id.name == "testFun1").get.getBody)
+ val body2 =
+ searchAndReplace(replaceFun)(
+ program.definedFunctions.find(_.id.name == "testFun2").get.getBody)
+
+ // evaluate expressions with let
+ {
+ def formExecutable(expr: Expr) = {
+
+ import TreeOps._
+
+ val newFunId = FreshIdentifier("tempIntroducedFunction")
+ val newFun = new FunDef(newFunId, funDef.returnType, funDef.args)
+ newFun.precondition = funDef.precondition
+ newFun.postcondition = funDef.postcondition
+
+ def replaceFunDef(expr: Expr) = expr match {
+ case FunctionInvocation(`funDef`, args) =>
+ Some(FunctionInvocation(newFun, args))
+ case _ => None
+ }
+ val newBody = searchAndReplace(replaceFunDef)(expr)
+
+ newFun.body = Some(newBody)
+
+ assert(expr.getType != Untyped)
+ val resFresh = FreshIdentifier("result") //.setType(expr.getType)
+ resFresh.setType(newBody.getType)
+
+ // body can contain (self-)recursive calls
+ (
+ Let(resFresh, newBody,
+ replace(Map(ResultVariable() -> Variable(resFresh)),
+ matchToIfThenElse(newFun.getPostcondition))),
+ newFun)
+ }
+
+ val pairs = List(body1, body2) map (formExecutable(_))
+ val candidates = pairs map (_._1)
+
+ val params = CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true)
+
+ val evaluator = new CodeGenEvaluator(sctx.context,
+ program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ pairs.map(_._2))), params)
+
+ val eval1 = (for (ind <- 0 until inputExamples.size) yield {
+ val res = evaluator.eval(candidates(0), inputExamples(ind).map)
+ (res, inputExamples(ind))
+ })
+
+ val eval2 = (for (ind <- 0 until inputExamples.size) yield {
+ val res = evaluator.eval(candidates(1), inputExamples(ind).map)
+ (res, inputExamples(ind))
+ })
+
+ val message = "Examples: " + inputExamples.mkString(", ")
+ val eval1message = "Evaluation of " + body1 + " yielded: " + eval1.mkString("\n")
+ val eval2message = "Evaluation of " + body2 + " yielded: " + eval2.mkString("\n")
+ assert(inputExamples.size == eval2.count(_._1 == Successful(BooleanLiteral(true))), message + " " + eval2message)
+ assert(inputExamples.size > eval1.count(_._1 == Successful(BooleanLiteral(true))), message + " " + eval1message)
+ }
+
+ // evaluate expressions without let
+ {
+ def formExecutable(expr: Expr) = {
+
+ import TreeOps._
+
+ val newFunId = FreshIdentifier("tempIntroducedFunction")
+ val newFun = new FunDef(newFunId, funDef.returnType, funDef.args)
+ newFun.precondition = funDef.precondition
+ newFun.postcondition = funDef.postcondition
+
+ def replaceFunDef(expr: Expr) = expr match {
+ case FunctionInvocation(`funDef`, args) =>
+ Some(FunctionInvocation(newFun, args))
+ case _ => None
+ }
+ val newBody = searchAndReplace(replaceFunDef)(expr)
+
+ newFun.body = Some(newBody)
+
+ assert(expr.getType != Untyped)
+ val resFresh = FreshIdentifier("result") //.setType(expr.getType)
+ resFresh.setType(newBody.getType)
+
+ // body can contain (self-)recursive calls
+ (newBody, newFun)
+ }
+
+ val pairs = List(body1, body2) map (formExecutable(_))
+ val candidates = pairs map (_._1)
+
+ val params = CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true)
+
+ val evaluator = new CodeGenEvaluator(sctx.context,
+ program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ pairs.map(_._2))), params)
+
+ val eval1 = (for (ind <- 0 until inputExamples.size) yield {
+ val res = evaluator.eval(candidates(0), inputExamples(ind).map)
+ (res, inputExamples(ind))
+ })
+
+ val eval2 = (for (ind <- 0 until inputExamples.size) yield {
+ val res = evaluator.eval(candidates(1), inputExamples(ind).map)
+ (res, inputExamples(ind))
+ })
+
+ val message = "Examples: " + inputExamples.mkString(", ")
+ val eval1message = "Evaluation of " + body1 + " yielded: " + eval1.mkString("\n")
+ val eval2message = "Evaluation of " + body2 + " yielded: " + eval2.mkString("\n")
+// assert(inputExamples.size == eval2.count(_._1 == Successful(BooleanLiteral(true))), message + " " + eval2message)
+// assert(inputExamples.size > eval1.count(_._1 == Successful(BooleanLiteral(true))), message + " " + eval1message)
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/FilterTest.scala b/src/test/scala/lesynth/FilterTest.scala
new file mode 100644
index 000000000..e9b6aab17
--- /dev/null
+++ b/src/test/scala/lesynth/FilterTest.scala
@@ -0,0 +1,235 @@
+package lesynth
+
+import scala.util.Random
+
+import org.junit.Assert._
+import org.junit.{ Test, Ignore, Before }
+
+import insynth.leon.loader.{ LeonLoader, HoleExtractor }
+import insynth.leon._
+
+import _root_.leon.purescala.Trees._
+import _root_.leon.purescala.TypeTrees._
+import _root_.leon.purescala._
+import _root_.leon.purescala.Definitions._
+
+import lesynth.refinement._
+
+import util._
+
+class FilterTest {
+
+ import TestConfig._
+ import TreeOps._
+ import Scaffold._
+
+ val rnd = new Random(System.currentTimeMillis())
+
+ var filter: Filter = _
+
+ var prog: Program = _
+ var hole: Hole = _
+ var funDef: FunDef = _
+ var variableRefiner: VariableRefiner = _
+
+ var tail: UnaryReconstructionExpression = _
+ var head: UnaryReconstructionExpression = _
+ var nil: Expr = _
+ var cons: NaryReconstructionExpression = _
+
+ @Before
+ def extract = {
+
+ val problems = forFile(lesynthTestDir + "refinement/ListConcat.scala")
+ assertEquals(1, problems.size)
+
+ val (sctx, funDef, problem) = problems.head
+
+ prog = sctx.program
+ hole = Hole(funDef.getBody.getType)
+ this.funDef = funDef
+
+ val loader = new LeonLoader(prog, hole, problem.as)
+
+ variableRefiner = new VariableRefiner(loader.directSubclassesMap, loader.variableDeclarations,
+ loader.classMap)
+
+ tail =
+ loader.extractFields.find {
+ _.expression match {
+ case ure: UnaryReconstructionExpression => ure(UnitLiteral).toString.contains(".tail")
+ case _ => false
+ }
+ } match {
+ case Some(found) => found.expression.asInstanceOf[UnaryReconstructionExpression]
+ case _ => fail("could not extract tail"); null
+ }
+
+ head =
+ loader.extractFields.find {
+ _.expression match {
+ case ure: UnaryReconstructionExpression => ure(UnitLiteral).toString.contains(".head")
+ case _ => false
+ }
+ } match {
+ case Some(found) => found.expression.asInstanceOf[UnaryReconstructionExpression]
+ case _ => fail("could not extract head"); null
+ }
+
+ cons =
+ loader.extractCaseClasses.find {
+ _.expression match {
+ case nre: NaryReconstructionExpression => nre(List(UnitLiteral, UnitLiteral)).toString.contains("Cons")
+ case _ => false
+ }
+ } match {
+ case Some(found) => found.expression.asInstanceOf[NaryReconstructionExpression]
+ case _ => fail("could not extract cons"); null
+ }
+
+ nil =
+ loader.extractCaseClasses.find {
+ _.expression match {
+ case im: ImmediateExpression => im().toString.contains("Nil")
+ case _ => false
+ }
+ } match {
+ case Some(found) => found.expression.asInstanceOf[ImmediateExpression]()
+ case _ => fail("could not extract cons"); null
+ }
+
+ filter = new Filter(prog, funDef, variableRefiner)
+ }
+
+ @Test
+ def testIsLess = {
+ val filter = this.filter
+ import filter.isLess
+
+ assertEquals(2, funDef.args.size)
+
+ val variable1 = funDef.args.head
+ val variable2 = funDef.args(1)
+
+ assertEquals(+1, isLess(cons(List(UnitLiteral, variable1.toVariable)), variable1.id))
+ assertEquals(+1, isLess(cons(List(UnitLiteral, variable1.toVariable)), variable2.id))
+ assertEquals(-1, isLess(tail(variable1.toVariable), variable1.id))
+ assertEquals(+1, isLess(head(variable1.toVariable), variable1.id))
+ assertEquals(0, isLess(variable1.toVariable, variable1.id))
+ assertEquals(1, isLess(variable1.toVariable, variable2.id))
+ assertEquals(1, isLess(tail(variable1.toVariable), variable2.id))
+ assertEquals(1, isLess(head(variable1.toVariable), variable2.id))
+ assertEquals(1, isLess(nil, variable2.id))
+
+ }
+
+ @Test
+ def testIsCallLessBySize = {
+
+ val filter = this.filter
+ import filter.isCallAvoidableBySize
+
+ assertEquals(2, funDef.args.size)
+
+ val arg1 = funDef.args.head.toVariable
+ val arg2 = funDef.args(1).toVariable
+
+ def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(funDef, Seq(arg1, arg2))
+
+ val arguments = funDef.args.map(_.id).toList
+
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(nil, nil), arguments))
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg1, arg2), arguments))
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg2, arg1), arguments))
+ assertEquals(false, isCallAvoidableBySize(makeFunctionCall(arg1, tail(arg2)), arguments))
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg1, tail(arg1)), arguments))
+ assertEquals(false, isCallAvoidableBySize(makeFunctionCall(tail(arg1), tail(arg2)), arguments))
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(cons(List(nil, tail(arg1))), arg2), arguments))
+ assertEquals(false, isCallAvoidableBySize(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2)), arguments))
+ assertEquals(false, isCallAvoidableBySize(nil, arguments))
+
+ }
+
+ @Test
+ def testHasDoubleRecursion = {
+
+ val filter = this.filter
+ import filter.hasDoubleRecursion
+
+ assertEquals(2, funDef.args.size)
+
+ val arg1 = funDef.args.head.toVariable
+ val arg2 = funDef.args(1).toVariable
+
+ def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(funDef, Seq(arg1, arg2))
+
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(nil, nil)))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, arg2)))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg2, arg1)))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, tail(arg2))))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, tail(arg1))))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(tail(arg1), tail(arg2))))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(cons(List(nil, tail(arg1))), arg2)))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2))))
+ assertEquals(false, hasDoubleRecursion(nil))
+
+ assertEquals(false, hasDoubleRecursion(And(makeFunctionCall(arg1, arg2), makeFunctionCall(arg1, arg2))))
+ assertEquals(true, hasDoubleRecursion(makeFunctionCall(makeFunctionCall(arg1, arg2), tail(arg2))))
+
+ }
+
+ @Test
+ def testIsAvoidable = {
+
+ val filter = this.filter
+ import filter.isAvoidable
+
+ assertEquals(2, funDef.args.size)
+
+ val arg1 = funDef.args.head.toVariable
+ val arg2 = funDef.args(1).toVariable
+
+ def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(funDef, Seq(arg1, arg2))
+
+ val arguments = funDef.args.map(_.id).toList
+
+ assertEquals(true, isAvoidable(makeFunctionCall(nil, nil), arguments))
+ assertEquals(true, isAvoidable(makeFunctionCall(arg1, arg2), arguments))
+ assertEquals(true, isAvoidable(makeFunctionCall(arg2, arg1), arguments))
+ assertEquals(false, isAvoidable(makeFunctionCall(arg1, tail(arg2)), arguments))
+ assertEquals(true, isAvoidable(makeFunctionCall(arg1, tail(arg1)), arguments))
+ assertEquals(false, isAvoidable(makeFunctionCall(tail(arg1), tail(arg2)), arguments))
+ assertEquals(true, isAvoidable(makeFunctionCall(cons(List(nil, tail(arg1))), arg2), arguments))
+ assertEquals(false, isAvoidable(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2)), arguments))
+ assertEquals(false, isAvoidable(nil, arguments))
+
+ assertEquals(true, isAvoidable(makeFunctionCall(makeFunctionCall(arg1, arg2), tail(arg2)), arguments))
+
+ }
+
+ @Test
+ def testIsAvoidableUneccessaryStructure {
+
+ val filter = this.filter
+ import filter.isAvoidable
+
+ val arg1 = funDef.args.head.toVariable
+ val arg2 = funDef.args(1).toVariable
+ val arguments = funDef.args.map(_.id).toList
+
+ val tpe = cons(List(Error("temp"))).getType match {
+ case cct: CaseClassType => cct.classDef
+ case _ =>
+ fail(arg1 + " should have a class type")
+ null
+ }
+
+ assertEquals(false, isAvoidable(CaseClassInstanceOf(tpe, arg1), arguments))
+ assertEquals(false, isAvoidable(CaseClassInstanceOf(tpe, arg2), arguments))
+ assertEquals(false, isAvoidable(CaseClassInstanceOf(tpe, cons(List(arg1, nil))), arguments))
+ assertEquals(true, isAvoidable(CaseClassInstanceOf(tpe, tail(arg1)), arguments))
+ assertEquals(true, isAvoidable(CaseClassInstanceOf(tpe, tail(tail(arg1))), arguments))
+ assertEquals(true, isAvoidable(CaseClassInstanceOf(tpe, tail(tail(tail(tail(arg1))))), arguments))
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/RefinerTest.scala b/src/test/scala/lesynth/RefinerTest.scala
deleted file mode 100644
index 861971ed1..000000000
--- a/src/test/scala/lesynth/RefinerTest.scala
+++ /dev/null
@@ -1,209 +0,0 @@
-package lesynth
-
-import scala.util.Random
-
-import org.junit.Assert._
-import org.junit.{ Test, Ignore, Before }
-
-import insynth.leon.HoleFinder
-import insynth.leon.loader.{ LeonLoader, HoleExtractor }
-import insynth.leon._
-
-import _root_.leon.purescala.Trees.{ Expr, Hole, IntLiteral, UnitLiteral, Variable, FunctionInvocation, And }
-import _root_.leon.purescala.{ TreeOps }
-import _root_.leon.purescala.Definitions.{ Program, FunDef }
-import _root_.leon.evaluators._
-import _root_.leon.{ LeonContext, DefaultReporter, Main }
-import _root_.leon.verification.AnalysisPhase
-
-import insynth.testutil.CommonUtils
-import testutil.TestConfig
-
-class RefinerTest {
-
- import TestConfig._
- import CommonUtils._
- import TreeOps._
-
- val rnd = new Random(System.currentTimeMillis())
-
- var prog: Program = _
- var hole: Hole = _
- var holeFunDef: FunDef = _
-
- var tail: UnaryReconstructionExpression = _
- var head: UnaryReconstructionExpression = _
- var nil: Expr = _
- var cons: NaryReconstructionExpression = _
-
- @Before
- def extract = {
-
- val holeFinder = new HoleFinder(lesynthTestDir + "ListOperationsHole.scala")
-
- holeFinder.extract match {
- case Some((progE, holeE)) =>
-
- prog = progE
- hole = holeE
-
- holeFunDef = new HoleExtractor(prog, hole).extractHole match {
- case Some((hfd, _)) => hfd
- case None => fail("could not extract hole"); null
- }
-
- val loader = new LeonLoader(prog, hole)
-
- tail =
- loader.extractFields.find {
- _.expression match {
- case ure: UnaryReconstructionExpression => ure(UnitLiteral).toString.contains(".tail")
- case _ => false
- }
- } match {
- case Some(found) => found.expression.asInstanceOf[UnaryReconstructionExpression]
- case _ => fail("could not extract tail"); null
- }
-
- head =
- loader.extractFields.find {
- _.expression match {
- case ure: UnaryReconstructionExpression => ure(UnitLiteral).toString.contains(".head")
- case _ => false
- }
- } match {
- case Some(found) => found.expression.asInstanceOf[UnaryReconstructionExpression]
- case _ => fail("could not extract head"); null
- }
-
- cons =
- loader.extractCaseClasses.find {
- _.expression match {
- case nre: NaryReconstructionExpression => nre(List(UnitLiteral, UnitLiteral)).toString.contains("Cons")
- case _ => false
- }
- } match {
- case Some(found) => found.expression.asInstanceOf[NaryReconstructionExpression]
- case _ => fail("could not extract cons"); null
- }
-
- nil =
- loader.extractCaseClasses.find {
- _.expression match {
- case im: ImmediateExpression => im().toString.contains("Nil")
- case _ => false
- }
- } match {
- case Some(found) => found.expression.asInstanceOf[ImmediateExpression]()
- case _ => fail("could not extract cons"); null
- }
-
- case _ =>
- fail("HoleFinder could not extract hole from the program")
- }
- }
-
- @Test
- def testIsLess = {
-
- val refiner = new Refiner(prog, hole, holeFunDef)
- import refiner.isLess
-
- assertEquals(2, holeFunDef.args.size)
-
- val variable1 = holeFunDef.args.head
- val variable2 = holeFunDef.args(1)
-
- assertEquals(+1, isLess(cons(List(UnitLiteral, variable1.toVariable)), variable1))
- assertEquals(+1, isLess(cons(List(UnitLiteral, variable1.toVariable)), variable2))
- assertEquals(-1, isLess(tail(variable1.toVariable), variable1))
- assertEquals(+1, isLess(head(variable1.toVariable), variable1))
- assertEquals(0, isLess(variable1.toVariable, variable1))
- assertEquals(1, isLess(variable1.toVariable, variable2))
- assertEquals(1, isLess(tail(variable1.toVariable), variable2))
- assertEquals(1, isLess(head(variable1.toVariable), variable2))
- assertEquals(1, isLess(nil, variable2))
-
- }
-
- @Test
- def testIsCallLessBySize = {
-
- val refiner = new Refiner(prog, hole, holeFunDef)
- import refiner.isCallAvoidableBySize
-
- assertEquals(2, holeFunDef.args.size)
-
- val arg1 = holeFunDef.args.head.toVariable
- val arg2 = holeFunDef.args(1).toVariable
-
- def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(holeFunDef, Seq(arg1, arg2))
-
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(nil, nil)))
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg1, arg2)))
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg2, arg1)))
- assertEquals(false, isCallAvoidableBySize(makeFunctionCall(arg1, tail(arg2))))
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg1, tail(arg1))))
- assertEquals(false, isCallAvoidableBySize(makeFunctionCall(tail(arg1), tail(arg2))))
- assertEquals(true, isCallAvoidableBySize(makeFunctionCall(cons(List(nil, tail(arg1))), arg2)))
- assertEquals(false, isCallAvoidableBySize(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2))))
- assertEquals(false, isCallAvoidableBySize(nil))
-
- }
-
- @Test
- def testHasDoubleRecursion = {
-
- val refiner = new Refiner(prog, hole, holeFunDef)
- import refiner.hasDoubleRecursion
-
- assertEquals(2, holeFunDef.args.size)
-
- val arg1 = holeFunDef.args.head.toVariable
- val arg2 = holeFunDef.args(1).toVariable
-
- def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(holeFunDef, Seq(arg1, arg2))
-
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(nil, nil)))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, arg2)))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg2, arg1)))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, tail(arg2))))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, tail(arg1))))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(tail(arg1), tail(arg2))))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(cons(List(nil, tail(arg1))), arg2)))
- assertEquals(false, hasDoubleRecursion(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2))))
- assertEquals(false, hasDoubleRecursion(nil))
-
- assertEquals(false, hasDoubleRecursion(And(makeFunctionCall(arg1, arg2), makeFunctionCall(arg1, arg2))))
- assertEquals(true, hasDoubleRecursion(makeFunctionCall(makeFunctionCall(arg1, arg2), tail(arg2))))
-
- }
-
- @Test
- def testIsAvoidable = {
-
- val refiner = new Refiner(prog, hole, holeFunDef)
- import refiner.isAvoidable
-
- assertEquals(2, holeFunDef.args.size)
-
- val arg1 = holeFunDef.args.head.toVariable
- val arg2 = holeFunDef.args(1).toVariable
-
- def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(holeFunDef, Seq(arg1, arg2))
-
- assertEquals(true, isAvoidable(makeFunctionCall(nil, nil)))
- assertEquals(true, isAvoidable(makeFunctionCall(arg1, arg2)))
- assertEquals(true, isAvoidable(makeFunctionCall(arg2, arg1)))
- assertEquals(false, isAvoidable(makeFunctionCall(arg1, tail(arg2))))
- assertEquals(true, isAvoidable(makeFunctionCall(arg1, tail(arg1))))
- assertEquals(false, isAvoidable(makeFunctionCall(tail(arg1), tail(arg2))))
- assertEquals(true, isAvoidable(makeFunctionCall(cons(List(nil, tail(arg1))), arg2)))
- assertEquals(false, isAvoidable(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2))))
- assertEquals(false, isAvoidable(nil))
-
- assertEquals(true, isAvoidable(makeFunctionCall(makeFunctionCall(arg1, arg2), tail(arg2))))
-
- }
-
-}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/TryOutSynthesizerExamplesTest.scala b/src/test/scala/lesynth/TryOutSynthesizerExamplesTest.scala
deleted file mode 100755
index 2655b3ef7..000000000
--- a/src/test/scala/lesynth/TryOutSynthesizerExamplesTest.scala
+++ /dev/null
@@ -1,672 +0,0 @@
-package lesynth
-
-import org.junit.Assert._
-import org.junit.{ Test, Ignore }
-
-import testutil.TestConfig
-
-import scala.collection.mutable.{ Map => MutableMap }
-import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{ LinkedList => MutableList }
-import scala.util.matching.Regex
-import scala.collection.mutable.PriorityQueue
-
-import scala.tools.nsc.{ Settings => NSCSettings, MainGenericRunner }
-
-import leon.{ Main => LeonMain, Reporter, DefaultReporter, SilentReporter, Settings, 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, VarDecl, Program, ObjectDef }
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.TreeOps
-import leon.plugin.ExtractionPhase
-
-import insynth.util.logging.HasLogger
-import insynth.interfaces.Declaration
-import insynth.InSynth
-import insynth.reconstruction.codegen.CodeGenerator
-import insynth.leon.loader.LeonLoader
-import insynth.leon.LeonDeclaration
-import insynth.leon.ImmediateExpression
-import insynth.engine.InitialEnvironmentBuilder
-import insynth.leon.LeonQueryBuilder
-import insynth.interfaces.{ Loader, Declaration, QueryBuilder }
-import insynth.engine.{ Engine, InitialEnvironmentBuilder }
-import insynth.engine.scheduler.WeightScheduler
-import insynth.structures.ContainerNode
-import insynth.util.TimeOut
-import insynth.Config
-import insynth.reconstruction.Reconstructor
-import insynth.leon.TypeTransformer
-import insynth.leon.HoleFinder
-import insynth.leon.loader.HoleExtractor
-import insynth.reconstruction.Output
-
-class TryOutSynthesizerExamplesTest {
-
- @Test
- def tryOut {
- import TestConfig._
-
- val synthesizer = new TryOutSynthesizerExamples(lesynthTestDir + "ListOperationsHole.scala")
-
- val report = synthesizer.synthesize
- assertTrue(report.isSuccess)
- println(report.summaryString)
- }
-
-}
-
-class TryOutSynthesizerExamples(
- fileName: String,
- // number of condition expressions to try before giving up on that branch expression
- numberOfBooleanSnippets: Int = 5,
- numberOfCounterExamplesToGenerate: Int = 5,
- leonTimeout: Int = 2, // seconds
- analyzeSynthesizedFunctionOnly: Boolean = false,
- showLeonOutput: Boolean = false,
- reporter: Reporter = new DefaultReporter,
- collectCounterExamplesFromLeon: Boolean = false) extends HasLogger {
-
- info("Synthesizer:")
- info("fileName: %s".format(fileName))
- info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
- info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
- info("leonTimeout: %d".format(leonTimeout))
-
- // some synthesis instance information
- private var program: Program = _
- private var hole: Hole = _
- private var holeFunDef: FunDef = _
- // initial declarations
- private var allDeclarations: List[Declaration] = _
- // objects used in the synthesis
- private var loader: LeonLoader = _
- private var inSynth: InSynth = _
- private var inSynthBoolean: InSynth = _
- private var refiner: Refiner = _
- private var solver: Solver = _
- private var ctx: LeonContext = _
- private var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = _
- private var initialPrecondition: Expr = _
-
- // flag denoting if a correct body has been synthesized
- private var found = false
-
- // 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 = _
-
- // time
- var startTime: Long = _
- var verTime: Long = 0
- var synTime: Long = 0
-
- // filtering/ranking with examples support
- var exampleRunner: ExampleRunner = _
- val numberOfTestsInIteration = 50
- val numberOfCheckInIteration = 5
-
- // TODO function to check specifically
- def analyzeProgram = {
-
- val temp = System.currentTimeMillis
- Globals.allSolved = Some(true)
-
- val report = AnalysisPhase.run(ctx)(program)
-
- val time = System.currentTimeMillis - temp
- fine("Analysis took: " + time + ", from report: " + report.totalTime)
-
- // accumulate
- verTime += time
-
- report
- }
-
- // 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)))
- val temp = System.currentTimeMillis
-
- // 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) {
-
- fine("found coounterexample: " + 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 =
- inSynth.getExpressions(getCurrentBuilder)
-
- def synthesizeBooleanExpressions =
- inSynthBoolean.getExpressions(getCurrentBuilder)
-
- def interactivePause = {
- System.out.println("Press Any Key To Continue...");
- new java.util.Scanner(System.in).nextLine();
- }
-
- def initialize = {
-
- // TODO lose this - globals are bad
- Globals.allSolved = None
-
- // extract hole
- new HoleFinder(fileName).extract match {
- case Some((matchProgram, matchHole: Hole)) =>
- program = matchProgram
- hole = matchHole
- case None => throw new RuntimeException("Cannot find hole")
- }
-
- // 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, 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
- holeFunDef = loader.holeDef
- fine("postcondition is: " + holeFunDef.getPostcondition)
-
- // 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
- val directSubclassMap = loader.directSubclassesMap
- val variableDeclarations = loader.variableDeclarations
- // map from identifier into a set of possible subclasses
- variableRefinements = MutableMap.empty
- for (varDec <- variableDeclarations) {
- varDec match {
- case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, LeonVariable(id))) =>
- variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
- case _ =>
- }
- }
-
- // calculate cases that should not happen
- refiner = new Refiner(program, hole, holeFunDef)
- fine("Refiner initialized. Recursive call: " + refiner.recurentExpression)
-
- exampleRunner = new ExampleRunner(holeFunDef)
- exampleRunner.counterExamples ++= introduceCounterExamples
- }
-
- def countPassedExamples(snippet: Expr) = {
- 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)
-
- val count = exampleRunner.countPassed(accumulatedExpression)
-
- holeFunDef.precondition = oldPreconditionSaved
- holeFunDef.body = oldBodySaved
-
- count
- }
-
- def introduceCounterExamples = {
- val argumentIds = holeFunDef.args.map(_.id)
- hole.getType match {
- case ct: ClassType =>
- val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
-
- val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
-
- val nilClass = nilClassSet.head
- val consClass = consClassSet.head
-
- var counter = 0
- def getIntLiteral = { counter += 1; IntLiteral(counter) }
-
- val list0 = () => CaseClass(nilClass, Nil)
- val list1 = () => CaseClass(consClass, getIntLiteral :: list0() :: Nil)
- val list2 = () => CaseClass(consClass, getIntLiteral :: list1() :: Nil)
- val list3 = () => CaseClass(consClass, getIntLiteral :: list2() :: Nil)
- val list4 = () => CaseClass(consClass, getIntLiteral :: list3() :: Nil)
-
- val lists = List(list0, list1, list2, list3 /*, list4*/ )
-
- for (l1 <- lists; l2 <- lists)
- yield Map(argumentIds(0) -> l1(), argumentIds(1) -> l2())
-
- case _ =>
- throw new RuntimeException("Could not produce initial examples: Could not match hole type")
- }
- }
-
- def synthesize: Report = {
- reporter.info("Synthesis called on file: " + fileName)
-
- // get start time
- startTime = System.currentTimeMillis
-
- reporter.info("Initializing synthesizer: ")
- reporter.info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
- reporter.info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
- 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
- }
-
- // initial snippets (will update in the loop)
- var snippets = synthesizeBranchExpressions
- // iterate while the program is not valid
- import scala.util.control.Breaks._
- var iteration = 0
- breakable {
- while (keepGoing) {
- // next iteration
- iteration += 1
- reporter.info("####################################")
- reporter.info("######Iteration #" + iteration + " ###############")
- reporter.info("####################################")
-
- // just printing of expressions
- finest(
- ((snippets zip Iterator.range(0, 200).toStream) map {
- case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet
- }).mkString("\n"))
- reporter.info("# precondition is: " + holeFunDef.precondition.getOrElse(BooleanLiteral(true)))
- reporter.info("# accumulatingPrecondition is: " + accumulatingPrecondition)
- reporter.info("# accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
- reporter.info("####################################")
-
- // ordering of expressions according to passed examples
- var pq = new PriorityQueue[(Expr, Int)]()(
- new Ordering[(Expr, Int)] {
- def compare(pair1: (Expr, Int), pair2: (Expr, Int)) =
- pair1._2.compare(pair2._2)
- })
- var numberOfTested = 0
-
- // just printing of expressions and pass counts
- finest(
- ((snippets zip Iterator.range(0, 200).toStream) map {
- case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet +
- " pass count is " + countPassedExamples(snippet.getSnippet)
- }).mkString("\n"))
- //interactivePause
-
- // found precondition?
- found = false
- // try to find it
- breakable {
- // go through all snippets
- for (snippet <- snippets; val snippetTree = snippet.getSnippet) {
- finest("snippetTree is: " + snippetTree)
-
- // skip avoidable calls
- if (!refiner.isAvoidable(snippetTree)) {
-
- // passed example pairs
- val passCount = countPassedExamples(snippetTree)
-
- if (passCount == exampleRunner.counterExamples.size) {
- info("All examples passed. Testing snippet " + snippetTree + " right away")
- if (tryToSynthesizeBranch(snippetTree)) {
- // will set found if correct body is found
- break
- }
- } else {
- info("snippet with pass count filtered: " + (snippetTree, passCount))
- pq.enqueue((snippetTree, 100 + (passCount * (iteration - 1)) - snippet.getWeight.toInt))
- }
-
- } else {
- fine("Refiner filtered this snippet: " + snippetTree)
- } // if (!refiner.isAvoidable(snippetTree)) {
-
- // check if we this makes one test iteration
- if (numberOfTested >= numberOfTestsInIteration) {
- fine("Queue contents: " + pq.mkString(", "))
- fine("head of queue is: " + pq.head)
-
- //interactivePause
- // go and check the topmost numberOfCheckInIteration
- for (i <- 1 to math.min(numberOfCheckInIteration, pq.size)) {
- val nextSnippet = pq.dequeue._1
- info("dequeued nextSnippet: " + nextSnippet)
- //interactivePause
-
- if (tryToSynthesizeBranch(nextSnippet)) {
- break
- }
- }
-
- numberOfTested = 0
- } else
- numberOfTested += 1
-
- } // for (snippet <- snippets
- } // breakable { for (snippet <- snippets
-
- // if did not found for any of the branch expressions
- if (found) {
- val endTime = System.currentTimeMillis
- reporter.info("We are done, in time: " + (endTime - startTime))
- return new FullReport(holeFunDef, (endTime - startTime))
- }
-
- // get new snippets
- snippets = synthesizeBranchExpressions
-
- fine("filtering based on: " + holeFunDef.precondition.get)
- fine("counterexamples before filter: " + exampleRunner.counterExamples.size)
- exampleRunner.filter(holeFunDef.precondition.get)
- fine("counterexamples after filter: " + exampleRunner.counterExamples.size)
- fine("counterexamples after filter: " + exampleRunner.counterExamples.mkString("\n"))
- }
- } //breakable { while (!keepGoing) {
-
- EmptyReport
- }
-
- def tryToSynthesizeBranch(snippetTree: Expr): 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)
- holeFunDef.body = Some(newBody)
-
- // precondition
- val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
- holeFunDef.precondition = Some(initialPrecondition)
-
- snippetTree.setType(hole.desiredType)
- //holeFunDef.getBody.setType(hole.desiredType)
-
- // TODO spare one analyzing step
- // analyze the program
- fine("analyzing program for funDef:" + holeFunDef)
- analyzeProgram
-
- // 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
- }
-
- // store appropriate values here, will be update in a finally branch
- var bodyToRestore = oldBody
- var preconditionToRestore = Some(oldPrecondition)
-
- // because first initial test
- holeFunDef.precondition = preconditionToRestore
-
- // get counterexamples
- fine("Going to generating counterexamples: " + holeFunDef)
- val (maps, precondition) = generateCounterexamples(program, holeFunDef, 5)
-
- // collect (add) counterexamples from leon
- if (collectCounterExamplesFromLeon)
- exampleRunner.counterExamples ++= maps
-
- // 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
- // }
-
- // 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 take numberOfBooleanSnippets
- // just printing of expressions
- finest(
- ((innerSnippets zip Iterator.range(0, 500).toStream) map {
- case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet
- }).mkString("\n"))
-
- for (innerSnippetTree <- innerSnippets map { _.getSnippet }) {
- fine("boolean snippet is: " + innerSnippetTree)
-
- val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, precondition)
-
- // if precondition found
- if (innerFound) {
- reporter.info("Precondition " + innerPrec + " found for " + snippetTree)
-
- innerPrec match {
- case s @ Some(_) =>
- // new precondition (restore in finally)
- preconditionToRestore = s
- case _ =>
- }
- return true
- }
-
- } // iterating over all boolean solutions
-
- reporter.info("No precondition found for branch expression: " + snippetTree)
- return false
-
- } // if ( !maps.isEmpty ) {
- // no counter examples, we just say that we cannot do anything
- false
- } // try
- finally {
- // set these to the FunDef
- holeFunDef.precondition = preconditionToRestore
- // restore old body (we accumulate expression)
- holeFunDef.body = Some(oldBody)
- }
- }
-
- def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: 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 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
- analyzeProgram
- // program is valid, we have a branch
- if (Globals.allSolved == Some(true)) {
- // we found a branch
- reporter.info("Wow! We found a branch!")
-
- // 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)
-
- // check for refinements
- checkRefinements(innerSnippetTree) match {
- case Some(refinementPair @ (id, classType)) =>
- fine("And now we have refinement type: " + refinementPair)
- fine("variableRefinements(id) before" + variableRefinements(id))
- variableRefinements(id) -= loader.classMap(classType.id)
- fine("variableRefinements(id) after" + variableRefinements(id))
-
- // if we have a single subclass possible to refine
- if (variableRefinements(id).size == 1) {
- reporter.info("We do variable refinement for " + id)
-
- val newType = variableRefinements(id).head
- fine("new type is: " + newType)
-
- // update declarations
- allDeclarations =
- for (dec <- allDeclarations)
- yield dec match {
- case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, LeonVariable(`id`))) =>
- LeonDeclaration(
- imex, TypeTransformer(newType), newType)
- case _ =>
- dec
- }
-
- } else
- fine("we cannot do variable refinement :(")
- case _ =>
- }
-
- // found a boolean snippet, break
- (true, preconditionToRestore)
- } else {
- // reset funDef and continue with next boolean snippet
- val preconditionToRestore = Some(accumulatingPrecondition)
- (false, preconditionToRestore)
- }
-
- case _ =>
-
- fine("solver filtered out the precondition (does not imply counterexamples)")
- (false, None)
- } //solveReturn match { (for implying counterexamples)
- } // notFalseSolveReturn match {
- }
-
- // inspect the expression if some refinements can be done
- def checkRefinements(expr: Expr) = expr match {
- case CaseClassInstanceOf(classDef, LeonVariable(id)) =>
- Some((id, classDef))
- case _ =>
- None
- }
-
-}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/TryOutTest.scala b/src/test/scala/lesynth/TryOutTest.scala
deleted file mode 100644
index d3a44e941..000000000
--- a/src/test/scala/lesynth/TryOutTest.scala
+++ /dev/null
@@ -1,639 +0,0 @@
-package lesynth
-
-import org.junit.Assert._
-import org.junit.{ Test, Ignore }
-
-import scala.collection.mutable.{ Map => MutableMap }
-import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{ LinkedList => MutableList }
-import scala.util.matching.Regex
-import scala.collection.mutable.PriorityQueue
-
-import scala.tools.nsc.{ Settings => NSCSettings, MainGenericRunner }
-
-import leon.{ Main => LeonMain, DefaultReporter, SilentReporter, Settings, 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, VarDecl, Program, ObjectDef }
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.purescala.TreeOps
-import leon.plugin.ExtractionPhase
-
-import insynth.util.logging.HasLogger
-import insynth.interfaces.Declaration
-import insynth.InSynth
-import insynth.reconstruction.codegen.CodeGenerator
-import insynth.leon.loader.LeonLoader
-import insynth.leon.LeonDeclaration
-import insynth.leon.ImmediateExpression
-import insynth.engine.InitialEnvironmentBuilder
-import insynth.leon.LeonQueryBuilder
-import insynth.interfaces.{ Loader, Declaration, QueryBuilder }
-import insynth.engine.{ Engine, InitialEnvironmentBuilder }
-import insynth.engine.scheduler.WeightScheduler
-import insynth.structures.ContainerNode
-import insynth.util.TimeOut
-import insynth.Config
-import insynth.reconstruction.Reconstructor
-import insynth.leon.TypeTransformer
-import insynth.leon.HoleFinder
-import insynth.leon.loader.HoleExtractor
-
-import testutil.TestConfig
-
-class TryOutTest extends HasLogger {
-
- import TestConfig.lesynthTestDir
-
- @Test
- def test1 {
- synthesize(lesynthTestDir + "ListOperationsHole.scala")
- }
-
- def analyzeProgram(program: Program) {
- import leon.Main._
-
- val temp = System.currentTimeMillis
- Globals.allSolved = Some(true)
-
- val reporter = new SilentReporter()
- val args = Array("no file!", "--timeout=2")
- val ctx = processOptions(reporter, args.toList)
-
- AnalysisPhase.run(ctx)(program)
-
- val time = System.currentTimeMillis - temp
- println("analysis took " + time)
- verTime += time
- }
-
- 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)))
-
- // 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(program)
-
- // check if solver could solved this instance
- if (Globals.allSolved == Some(false) && !Globals.asMap.isEmpty) {
-
- fine("found coounterexample: " + Globals.asMap)
-
- // add current counterexample
- maps :+= Globals.asMap
- // prevent this counterexample to reoccur
- val precAddition = Not(And(Globals.asMap map { case (id, value) => Equals(LeonVariable(id), value) } toSeq))
- precondition = And(Seq(precondition, precAddition))
- funDef.precondition = Some(precondition)
- } else
- changed = false
-
- ind += 1
- }
-
- // return found counterexamples and the formed precondition
- (maps, precondition)
- }
-
- def assertL1L2Refinements(variableRefinements: MutableMap[Identifier, MutableSet[ClassType]]) =
- for (
- pair @ (varName, nameSet) <- List(
- ("l2", Set("Nil", "Cons")),
- ("l1", Set("Nil", "Cons")))
- ) assertTrue(
- "pair " + pair + " not found. Found: " + variableRefinements.mkString(", "),
- (false /: variableRefinements) {
- (res, extr) =>
- extr match {
- case (id, classTypeSet) => res ||
- (
- id.name == varName &&
- (true /: nameSet) {
- (res, innerName) => res && classTypeSet.exists(_.classDef.id.name == innerName)
- })
- case _ => false
- }
- })
-
- private var program: Program = _
-
- private var hole: Hole = _
- private var holeFunDef: FunDef = _
-
- private var allDeclarations: List[Declaration] = _
-
- private var loader: LeonLoader = _
-
- private var inSynth: InSynth = _
- private var codeGenerator: CodeGenerator = _
-
- private var refiner: Refiner = _
-
- var found = false
-
- // 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 = _
-
- var solver: Solver = _
- //
- var ctx: LeonContext = _
- //
- var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = _
-
- var initialPrecondition: Expr = _
-
- var startTime: Long = _
-
- var verTime: Long = 0
- var synTime: Long = 0
-
- // number of condition expressions to try before giving up on that branch expression
- val numberOfBooleanSnippets = 5
-
- def synthesizeExpressions =
- inSynth.getExpressions
-
- def initialize(fileName: String) = {
-
- import leon.Main._
-
- val reporter = new SilentReporter
- val args = Array(fileName, "--timeout=2")
- ctx = processOptions(reporter, args.toList)
-
- // extract information about the program
-// extractInformation(ctx, fileName)
-
- codeGenerator = new CodeGenerator
-
- new HoleFinder(fileName).extract match {
- case Some((matchProgram, matchHole: Hole)) =>
- program = matchProgram
- hole = matchHole
- case None => fail("could not find hole")
- }
-
- solver = //new FairZ3Solver(ctx)
- new TimeoutSolver(new FairZ3Solver(ctx), 2)
-
- loader = new LeonLoader(program, hole, false)
- // create new insynth object
- inSynth = new InSynth(loader, true)
-
- // save all declarations seen
- allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-
- // funDef of the hole
- holeFunDef = loader.holeDef
- println("postcondition is: " + holeFunDef.getPostcondition)
-
- // 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
- val directSubclassMap = loader.directSubclassesMap
- val variableDeclarations = loader.variableDeclarations
-
- // map from identifier into a set of possible subclasses
- variableRefinements = MutableMap.empty
- for (varDec <- variableDeclarations) {
- varDec match {
- case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, LeonVariable(id))) =>
- variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
- case _ =>
- }
- }
-
- // calculate cases that should not happen
- refiner = new Refiner(program, hole, holeFunDef)
- fine("Refiner recursive call: " + refiner.recurentExpression)
-
- }
-
- def synthesize(fileName: String): Unit = {
- // get start time
- startTime = System.currentTimeMillis
-
- initialize(fileName)
-
- // keeps status of validity
- var keepGoing = Globals.allSolved match {
- case Some(true) => false
- case _ => true
- }
-
- var snippets = synthesizeExpressions
-
- // iterate while the program is not valid
- import scala.util.control.Breaks._
- var iteration = 0
- breakable {
- while (keepGoing) {
- // next iteration
- iteration += 1
- println("####################################")
- println("######Iteration #" + iteration + " ###############")
- println("####################################")
-
- // just printing of expressions
- for ((snippetTree, ind) <- (snippets map { _.getSnippet }) zip Iterator.range(0, 500).toStream) {
- println(ind + " snippetTree is: " + snippetTree)
- }
- println("precondition is: " + holeFunDef.precondition.getOrElse(BooleanLiteral(true)))
- println("accumulatingPrecondition is: " + accumulatingPrecondition)
- println("accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
- // System.out.println("Press Any Key To Continue...");
- // new java.util.Scanner(System.in).nextLine();
-
- // found precondition?
- found = false
- // try to find it
- breakable {
- // go through all snippets
- for (
- snippet <- snippets /*filter { _.getSnippet.toString == "concat(Nil(), Nil())" }*/ ;
- val snippetTree = snippet.getSnippet
- ) {
- // debugging
- println("snippetTree is: " + snippetTree)
- snippetTree.toString match {
- case "Cons(l1.head, concat(l1.tail, l2))" |
- "Cons(l1.head, concat(l2, l1.tail))" |
- "Cons(l2.head, concat(l2.tail, l1))" |
- "Cons(l2.head, concat(l1, l2.tail))" =>
- println("snippetTree is: " + snippetTree)
-// System.out.println("Press Any Key To Continue...");
-// new java.util.Scanner(System.in).nextLine();
- case _ =>
- }
-
- // System.out.println("Press Any Key To Continue...");
- // new java.util.Scanner(System.in).nextLine();
-
- // skip pure recursive call
- if (!refiner.isAvoidable(snippetTree)) {
- if (tryToSynthesizeBranch(snippetTree)) {
- break
- }
- } else {
- println("We are skipping this snippetTree: " + snippetTree)
- }
-
- } // for (snippet <- snippets
- } // breakable { for (snippet <- snippets
-
- // if did not found for any of the branch expressions
- if (found) {
- info("we are done !")
-// System.out.println("Press Any Key To Continue...");
-// new java.util.Scanner(System.in).nextLine();
- return
- }
-
- val inSynth = new InSynth(allDeclarations, hole.desiredType, true)
- snippets = inSynth.getExpressions
-
- }
- } //breakable { while (!keepGoing) {
-
- // get end time
- val endTime = System.currentTimeMillis
- println("whole process took time: " + (endTime - startTime))
-
- }
-
- def tryToSynthesizeBranch(snippetTree: Expr): Boolean = {
- import leon.purescala.TreeOps.searchAndReplaceDFS
- // replace hole in the body with current snippet tree
-
- // val oldBody = holeFunDef.getBody
- // val newBody = searchAndReplaceDFS(
- // _ match {
- // case _: Hole => Some(snippetTree)
- // case _ => None
- // })(oldBody)
- val oldBody = holeFunDef.getBody
- val newBody = accumulatingExpression(snippetTree)
-
- holeFunDef.body = Some(newBody)
- // save old precondition
- val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
-
- holeFunDef.precondition = Some(initialPrecondition)
-
- // analyze the program
- println("analyzing program for funDef:" + holeFunDef)
-
- snippetTree.setType(hole.desiredType)
- holeFunDef.getBody.setType(hole.desiredType)
-
- analyzeProgram(program)
-
- // check if solver could solved this instance
- if (Globals.allSolved == Some(true)) {
- // mark the branch found
- found = true
-
- println("Wooooooow we have a winner!")
- println("************************************")
- println("*********And the winner is**********")
- println(accumulatingExpression(snippetTree))
- println("************************************")
-
- // get end time
- val endTime = System.currentTimeMillis
- println("whole process took time: " + (endTime - startTime))
- //println("verTime, testTime" + verTime + ", " + ExampleRunner.testTime)
-
-// System.out.println("Press Any Key To Continue...");
-// new java.util.Scanner(System.in).nextLine();
-
- return true
- }
-
- // store appropriate values here, will be update in a finally branch
- var bodyToRestore = oldBody
- var preconditionToRestore = Some(oldPrecondition)
-
- // because first initial test
- holeFunDef.precondition = preconditionToRestore
-
- // debug
- println("Going to generating counterexamples: " + holeFunDef)
- // System.out.println("Press Any Key To Continue...");
- // new java.util.Scanner(System.in).nextLine();
-
- // println("Counterexample cheking: ")
- // println("Counterexamples: " + ExampleRunner.counterExamples.mkString("\n"))
- // val counterExampleCheck = ExampleRunner.check(BooleanLiteral(true), newBody, holeFunDef.getPostcondition)
- // println("Result of check: " + counterExampleCheck )
- //
- val temp = System.currentTimeMillis
- // get counterexamples
- val (maps, precondition) = generateCounterexamples(program, holeFunDef, 5)
- val temptime = System.currentTimeMillis - temp
- println("gen counterexamples took " + temptime)
- verTime += temptime
-
- // collect (add) counterexamples
- //ExampleRunner.counterExamples ++= maps
-
- 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
- }
-
- // will modify funDef body and precondition, restore it later
- try {
- // TODO is this okay?
- // if there are no returned counterexamples just go to the next snippet
- // and so far counter examples passed
- if (!maps.isEmpty /*&& counterExampleCheck */ ) {
- // proceed with synthesizing boolean expressions
- assertEquals(5, maps.size)
- // set program to the solver
- solver.setProgram(program)
-
- // initialize builder with previously seen declarations
- val newBuilder = new InitialEnvironmentBuilder
- newBuilder.addDeclarations(allDeclarations)
-
- fine("all declarations now, size: " + newBuilder.getAllDeclarations.size)
-
- // synthesize solution
- val queryBuilder = new LeonQueryBuilder(BooleanType)
- val query = queryBuilder.getQuery
- val engine = new Engine(newBuilder, query, new WeightScheduler(), TimeOut(Config.getTimeOutSlot))
- val solution = engine.run()
- assertNotNull(solution)
-
- assertNotNull(codeGenerator)
- assertNotNull(allDeclarations)
- // reconstruct (only defined number of boolean expressions)
- val innerSnippets = Reconstructor(solution.getNodes.head, codeGenerator, true) take numberOfBooleanSnippets
- checkDeclarations(inSynth)
-
- // debugging
- for ((snippetTree, ind) <- (innerSnippets map { _.getSnippet }) zip Iterator.range(0, 20).toStream) {
- println(ind + " boolean snippetTree is: " + snippetTree)
- }
- // System.out.println("Press Any Key To Continue...");
- // new java.util.Scanner(System.in).nextLine();
-
- // precondition found?
- found = false
-
- // iterate over boolean snippets
- val iterator = innerSnippets.iterator
- while (!found && iterator.hasNext) {
- val innerSnippetTree = iterator.next.getSnippet
-
- // debug
- println("boolean snippet is: " + innerSnippetTree)
- // System.out.println("Press Any Key To Continue...");
- // new java.util.Scanner(System.in).nextLine();
-
- val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, precondition)
-
- //found = innerFound
- innerPrec match {
- case s @ Some(_) =>
- preconditionToRestore = s
- case _ =>
- }
-
- if (innerFound)
- return true
-
- } // iterating over all boolean solutions
-
- // if none of boolean solutions work, restore body (in finally)
- //holeFunDef.body = Some(oldBody)
-
- assertTrue(!found)
- info("not found :(, we give up on this branch expression")
- return false
-
- } // if ( !maps.isEmpty ) {
-
- false
- } // try
- finally {
- // set these to the FunDef
- holeFunDef.precondition = preconditionToRestore
- // restore old body (we accumulate expression)
- holeFunDef.body = Some(oldBody)
- }
- }
-
- def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: Expr): (Boolean, Option[Expr]) = {
-
- // debug
- // println("boolean snippet is: " + innerSnippetTree)
- // System.out.println("Press Any Key To Continue...");
- // new java.util.Scanner(System.in).nextLine();
-
- // 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 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) =>
- // old precondition is not here, it is before counterexamples are derived!
- //val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
-
- // if expression implies counterexamples add it to the precondition and try to validate program
- holeFunDef.precondition = Some(newCondition)
- // do analysis
- analyzeProgram(program)
- // program is valid, we have a branch
- if (Globals.allSolved == Some(true)) {
- // we found a branch
- info("Wow! we found a branch!")
-
- // 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)
-
- // check for refinements
- checkRefinements(innerSnippetTree) match {
- case Some(refinementPair @ (id, classType)) =>
- fine("And now we have refinement type: " + refinementPair)
- fine("variableRefinements(id) before" + variableRefinements(id))
- variableRefinements(id) -= loader.classMap(classType.id)
- fine("variableRefinements(id) after" + variableRefinements(id))
-
- // if we have a single subclass possible to refine
- if (variableRefinements(id).size == 1) {
- fine("wow we an do variable refinement for " + id)
-
- val newType = variableRefinements(id).head
- fine("new type is: " + newType)
-
- // update declarations
- allDeclarations =
- for (dec <- allDeclarations)
- yield dec match {
- case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, LeonVariable(`id`))) =>
- LeonDeclaration(
- imex, TypeTransformer(newType), newType)
- case _ =>
- dec
- }
-
- } else
- fine("we cannot do variable refinement :(")
- case _ =>
- }
- // found a boolean snippet, break
- (true, preconditionToRestore)
- } else {
- // reset funDef and continue with next boolean snippet
- val preconditionToRestore = Some(accumulatingPrecondition)
- (false, preconditionToRestore)
- }
-
- case _ =>
- println("precondition was not applied")
- (false, None)
- } //solveReturn match { (for implying counterexamples)
- } // notFalseSolveReturn match {
- }
-
- // inspect the expression if some refinements can be done
- def checkRefinements(expr: Expr) = expr match {
- case CaseClassInstanceOf(classDef, LeonVariable(id)) =>
- Some((id, classDef))
- case _ =>
- None
- }
-
- def extractInformation(ctx: LeonContext, file: String) =
- new HoleFinder(file).extract
-
- // assert that there is not function that returns a function
- def checkDeclarations(inSynth: InSynth) = {
- assertFalse(
- "We should not have a declaration which returns a function (not valid in Leon)",
- (false /: inSynth.getCurrentBuilder.getAllDeclarations) {
- case (res, dec: LeonDeclaration) =>
- res ||
- (dec.getDomainType match {
- case FunctionType(_, _: FunctionType) => true
- case _ => false
- })
- })
- }
-
-}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/TryOutTestWithFiltering.scala b/src/test/scala/lesynth/TryOutTestWithFiltering.scala
deleted file mode 100644
index 3c65777d0..000000000
--- a/src/test/scala/lesynth/TryOutTestWithFiltering.scala
+++ /dev/null
@@ -1,768 +0,0 @@
-//package lesynth
-//
-//import org.junit.Assert._
-//import org.junit.{ Test, Ignore }
-//
-//import scala.collection.mutable.{ Map => MutableMap }
-//import scala.collection.mutable.{ Set => MutableSet }
-//import scala.collection.mutable.{ LinkedList => MutableList }
-//import scala.util.matching.Regex
-//import scala.collection.mutable.PriorityQueue
-//
-//import scala.tools.nsc.{ Settings => NSCSettings, MainGenericRunner }
-//
-//import leon.{ Main => LeonMain, DefaultReporter, Settings, 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, VarDecl, Program, ObjectDef }
-//import leon.purescala.Common.{ Identifier, FreshIdentifier }
-//import leon.purescala.TreeOps
-//import leon.plugin.ExtractionPhase
-//
-//import insynth.util.logging.HasLogger
-//import insynth.interfaces.Declaration
-//import insynth.InSynth
-//import insynth.reconstruction.codegen.CodeGenerator
-//import insynth.leon.loader.LeonLoader
-//import insynth.leon.LeonDeclaration
-//import insynth.leon.ImmediateExpression
-//import insynth.engine.InitialEnvironmentBuilder
-//import insynth.leon.LeonQueryBuilder
-//import insynth.interfaces.{ Loader, Declaration, QueryBuilder }
-//import insynth.engine.{ Engine, InitialEnvironmentBuilder }
-//import insynth.engine.scheduler.WeightScheduler
-//import insynth.structures.ContainerNode
-//import insynth.util.TimeOut
-//import insynth.Config
-//import insynth.reconstruction.Reconstructor
-//import insynth.leon.TypeTransformer
-//import insynth.leon.HoleFinder
-//
-//class TryOutTest extends HasLogger {
-//
-// def analyzeProgram(program: Program) {
-// import leon.Main._
-//
-// val temp = System.currentTimeMillis
-// Globals.allSolved = Some(true)
-//
-// val reporter = new DefaultReporter()
-// val args = Array("no file!", "--timeout=2")
-// val ctx = processOptions(reporter, args.toList)
-//
-// AnalysisPhase.run(ctx)(program)
-//
-// val time = System.currentTimeMillis - temp
-// println("analysis took " + time)
-// verTime += time
-// }
-//
-// 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)))
-//
-// // 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(program)
-//
-// // check if solver could solved this instance
-// if (Globals.allSolved == Some(false) && !Globals.asMap.isEmpty) {
-//
-// fine("found coounterexample: " + Globals.asMap)
-//
-// // add current counterexample
-// maps :+= Globals.asMap
-// // prevent this counterexample to reoccur
-// val precAddition = Not(And(Globals.asMap map { case (id, value) => Equals(LeonVariable(id), value) } toSeq))
-// precondition = And(Seq(precondition, precAddition))
-// funDef.precondition = Some(precondition)
-// } else
-// changed = false
-//
-// ind += 1
-// }
-//
-// // return found counterexamples and the formed precondition
-// (maps, precondition)
-// }
-//
-// // assert that there is not function that returns a function
-// def checkDeclarations(inSynth: InSynth) = {
-// assertFalse(
-// "We should not have a declaration which returns a function (not valid in Leon)",
-// (false /: inSynth.getCurrentBuilder.getAllDeclarations) {
-// case (res, dec: LeonDeclaration) =>
-// res ||
-// (dec.getDomainType match {
-// case FunctionType(_, _: FunctionType) => true
-// case _ => false
-// })
-// })
-// }
-//
-// def assertL1L2Refinements(variableRefinements: MutableMap[Identifier, MutableSet[ClassType]]) =
-// for (
-// pair @ (varName, nameSet) <- List(
-// ("l2", Set("Nil", "Cons")),
-// ("l1", Set("Nil", "Cons")))
-// ) assertTrue(
-// "pair " + pair + " not found. Found: " + variableRefinements.mkString(", "),
-// (false /: variableRefinements) {
-// (res, extr) =>
-// extr match {
-// case (id, classTypeSet) => res ||
-// (
-// id.name == varName &&
-// (true /: nameSet) {
-// (res, innerName) => res && classTypeSet.exists(_.classDef.id.name == innerName)
-// })
-// case _ => false
-// }
-// })
-//
-// private var program: Program = _
-//
-// private var hole: Hole = _
-// private var holeFunDef: FunDef = _
-//
-// private var allDeclarations: List[Declaration] = _
-//
-// private var loader: LeonLoader = _
-//
-// private var inSynth: InSynth = _
-// private var codeGenerator: CodeGenerator = _
-//
-// private var refiner: Refiner = _
-//
-// // 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 = _
-//
-// var solver: Solver = _
-// //
-// var ctx: LeonContext = _
-// //
-// var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = _
-//
-// var initialPrecondition: Expr = _
-//
-// var startTime: Long = _
-//
-// var verTime: Long = 0
-// var synTime: Long = 0
-//
-// // number of condition expressions to try before giving up on that branch expression
-// val numberOfBooleanSnippets = 20
-//
-// def introduceCounterExamples = {
-// var argumentIds = holeFunDef.args.map(_.id)
-// assertEquals(2, argumentIds.size)
-//
-// Globals.hole.getType match {
-// case ct: ClassType =>
-// val leonLoader = LeonLoader(program, hole, false)
-//
-// leonLoader.load
-//
-// val setSubclasses = leonLoader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
-// assertEquals(2, setSubclasses.size)
-//
-// val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
-// assertEquals(1, nilClassSet.size)
-//
-// val nilClass = nilClassSet.head
-// val consClass = consClassSet.head
-//
-// var counter = 0
-// def getIntLiteral = { counter += 1; IntLiteral(counter) }
-//
-// val list0 = () => CaseClass(nilClass, Nil)
-// val list1 = () => CaseClass(consClass, getIntLiteral :: list0() :: Nil)
-// val list2 = () => CaseClass(consClass, getIntLiteral :: list1() :: Nil)
-// val list3 = () => CaseClass(consClass, getIntLiteral :: list2() :: Nil)
-// val list4 = () => CaseClass(consClass, getIntLiteral :: list3() :: Nil)
-//
-// val lists = List(list0, list1, list2, list3 /*, list4*/ )
-//
-// for (l1 <- lists; l2 <- lists) {
-// ExampleRunner.counterExamples :+=
-// Map(argumentIds(0) -> l1(),
-// argumentIds(1) -> l2())
-// }
-// case _ =>
-// fail
-// }
-//
-// }
-//
-// def synthesizeExpressions =
-// inSynth.getExpressions
-//
-// def initialize(fileName: String) = {
-//
-// import leon.Main._
-//
-// val reporter = new DefaultReporter
-// val args = Array(fileName, "--timeout=2")
-// ctx = processOptions(reporter, args.toList)
-//
-// // extract information about the program
-// extractInformation(ctx, fileName)
-//
-// codeGenerator = new CodeGenerator
-//
-// // program and hole objects should be extracted
-// (Globals.program, Globals.hole) match {
-// case (Some(matchProgram), matchHole: Hole) =>
-// program = matchProgram
-// hole = matchHole
-//
-// solver = //new FairZ3Solver(ctx)
-// new TimeoutSolver(new FairZ3Solver(ctx), Globals.timeout)
-//
-// loader = new LeonLoader(program, hole, false)
-// // create new insynth object
-// inSynth = new InSynth(loader, true)
-//
-// // save all declarations seen
-// allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-//
-// // funDef of the hole
-// holeFunDef = Globals.holeFunDef
-// println("postcondition is: " + holeFunDef.getPostcondition)
-//
-// // 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
-// val directSubclassMap = loader.directSubclassesMap
-// val variableDeclarations = loader.variableDeclarations
-//
-// // map from identifier into a set of possible subclasses
-// variableRefinements = MutableMap.empty
-// for (varDec <- variableDeclarations) {
-// varDec match {
-// case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, LeonVariable(id))) =>
-// variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
-// case _ =>
-// }
-// }
-//
-// // calculate cases that should not happen
-// refiner = new Refiner(program, hole)
-// fine("Refiner recursive call: " + refiner.recurentExpression)
-// case _ => fail()
-// }
-// }
-//
-// @Test
-// def test1 {
-// synthesize("testcases/insynth/ListOperationsHole.scala")
-// }
-//
-// def synthesize(fileName: String): Unit = {
-// // get start time
-// startTime = System.currentTimeMillis
-//
-// initialize(fileName)
-//
-// // keeps status of validity
-// var keepGoing = Globals.allSolved match {
-// case Some(true) => false
-// case _ => true
-// }
-//
-// var snippets = synthesizeExpressions
-//
-// introduceCounterExamples
-// println("counterexamples after introduce: " + ExampleRunner.counterExamples.mkString("\n"))
-//
-// // iterate while the program is not valid
-// import scala.util.control.Breaks._
-// var iteration = 0
-// breakable {
-// while (keepGoing) {
-// // next iteration
-// iteration += 1
-// println("####################################")
-// println("######Iteration #" + iteration + " ###############")
-// println("####################################")
-//
-// // just printing of expressions
-// // for ((snippetTree, ind) <- (snippets map { _.getSnippet }) zip Iterator.range(0, 20).toStream) {
-// // println(ind + " snippetTree is: " + snippetTree)
-// // }
-// println("precondition is: " + holeFunDef.precondition.getOrElse(BooleanLiteral(true)))
-// println("accumulatingPrecondition is: " + accumulatingPrecondition)
-// println("accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-//
-// var pq = new PriorityQueue[(Expr, Int)]()(
-// new Ordering[(Expr, Int)] {
-// def compare(pair1: (Expr, Int), pair2: (Expr, Int)) =
-// pair1._2.compare(pair2._2)
-// })
-// var tested = 0
-//
-// // found precondition?
-// var found = false
-// // try to find it
-// breakable {
-// // go through all snippets
-// for (
-// snippet <- snippets /*filter { _.getSnippet.toString == "concat(Nil(), Nil())" }*/ ;
-// val snippetTree = snippet.getSnippet
-// ) {
-// // debugging
-// println("snippetTree is: " + snippetTree)
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-//
-// // TODO is never empty now with introduce
-// val passCount =
-// //if (ExampleRunner.counterExamples.isEmpty)
-// if (iteration == 1)
-// ExampleRunner.counterExamples.size
-// else {
-//
-// val oldPreconditionSaved = holeFunDef.precondition
-// val oldBodySaved = holeFunDef.body
-//
-// // restore initial precondition
-// holeFunDef.precondition = Some(initialPrecondition)
-//
-// assertEquals(BooleanLiteral(true), initialPrecondition)
-//
-// // get the whole body (if else...)
-// val accumulatedExpression = accumulatingExpression(snippetTree)
-// // set appropriate body to the function for the correct evaluation
-// holeFunDef.body = Some(accumulatedExpression)
-//
-// // if (snippetTree.toString == "Cons(l2.head, concat(l1, l2.tail))") {
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-// // }
-// val count = ExampleRunner.countPassed(accumulatedExpression)
-//
-// // if (snippetTree.toString == "Cons(l2.head, concat(l1, l2.tail))") {
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-// // }
-//
-// holeFunDef.precondition = oldPreconditionSaved
-// holeFunDef.body = oldBodySaved
-//
-// count
-// }
-//
-// val okay =
-// passCount == ExampleRunner.counterExamples.size
-// if (!okay) {
-// // println("snippet with pass count filtered: " + (snippet, passCount))
-// pq.enqueue((snippetTree, 100 + (passCount * (iteration - 1)) - snippet.getWeight.toInt))
-// }
-//
-// // skip pure recursive call
-// if (!refiner.isAvoidable(snippetTree) && okay) {
-// if (tryToSynthesizeBranch(snippetTree)) {
-// found = true
-// pq.clear
-// break
-// }
-// } else {
-// // println("We are skipping this snippetTree since it is the recursive call: " + Refiner.recurentExpressions)
-// }
-//
-// if (tested >= 500) {
-// println("queue is: " + pq.mkString("\n"))
-// println("head of queue is: " + pq.head)
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-// for (i <- 1 to 5) {
-// val nextSnippet = pq.dequeue._1
-// println("nextSnippet is: " + nextSnippet)
-//
-// if (tryToSynthesizeBranch(nextSnippet)) {
-// found = true
-// pq.clear
-// break
-// }
-// }
-// tested = 0
-// } else
-// tested += 1
-// } // for (snippet <- snippets
-// } // breakable { for (snippet <- snippets
-//
-// // if did not found for any of the branch expressions
-// if (!found) {
-// info("we are done :(")
-// return
-// }
-//
-// // debug
-// assertTrue(found)
-// info("variable declarations now:")
-// info(allDeclarations.filter(
-// _ match {
-// case LeonDeclaration(_, _, _, imex @ ImmediateExpression(_, _: LeonVariable)) =>
-// true
-// case _ =>
-// false
-// }).mkString(" ,"))
-//
-// info("okay we found one branch")
-//
-// // synthesize snippets for next branch
-// info("synthesizing new snippets")
-//
-// val newBuilder = new InitialEnvironmentBuilder
-// newBuilder.addDeclarations(allDeclarations)
-// fine("all declarations now, size: " + newBuilder.getAllDeclarations.size)
-// val queryBuilder = new LeonQueryBuilder(hole.desiredType)
-// val query = queryBuilder.getQuery
-// val engine = new Engine(newBuilder, query, new WeightScheduler(), TimeOut(Config.getTimeOutSlot))
-// val proofTree = engine.run()
-// assertNotNull(proofTree)
-// assertEquals(1, proofTree.getNodes.size)
-//
-// println("filtering based on: " + holeFunDef.precondition.get)
-// println("counterexamples before filter: " + ExampleRunner.counterExamples.size)
-// ExampleRunner.filter(holeFunDef.precondition.get)
-// println("counterexamples after filter: " + ExampleRunner.counterExamples.size)
-// println("counterexamples after filter: " + ExampleRunner.counterExamples.mkString("\n"))
-//
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-//
-// snippets = Reconstructor(proofTree.getNodes.head, codeGenerator)
-//
-// // ADHOC filter out counterexamples that have Nil (adhoc!)
-// // ExampleRunner.counterExamples = ExampleRunner.counterExamples filterNot {
-// // map =>
-// // (false /: map.values) {
-// // (res, value) =>
-// // res || value.toString.startsWith("Nil")
-// // }
-// // }
-//
-// }
-// } //breakable { while (!keepGoing) {
-//
-// // get end time
-// val endTime = System.currentTimeMillis
-// println("whole process took time: " + (endTime - startTime))
-//
-// }
-//
-// def tryToSynthesizeBranch(snippetTree: Expr): Boolean = {
-// import leon.purescala.TreeOps.searchAndReplaceDFS
-// // replace hole in the body with current snippet tree
-//
-// // val oldBody = holeFunDef.getBody
-// // val newBody = searchAndReplaceDFS(
-// // _ match {
-// // case _: Hole => Some(snippetTree)
-// // case _ => None
-// // })(oldBody)
-// val oldBody = holeFunDef.getBody
-// val newBody = accumulatingExpressionMatch(snippetTree)
-//
-// holeFunDef.body = Some(newBody)
-// // save old precondition
-// val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
-//
-// holeFunDef.precondition = Some(initialPrecondition)
-//
-// // analyze the program
-// analyzeProgram(program)
-//
-// // check if solver could solved this instance
-// if (Globals.allSolved == Some(true)) {
-// // mark the branch found
-// //found = true
-//
-// println("Wooooooow we have a winner!")
-// println("************************************")
-// println("*********And the winner is**********")
-// println(accumulatingExpression(snippetTree))
-// println("************************************")
-//
-// // get end time
-// val endTime = System.currentTimeMillis
-// println("whole process took time: " + (endTime - startTime))
-// //println("verTime, testTime" + verTime + ", " + ExampleRunner.testTime)
-//
-// System.out.println("Press Any Key To Continue...");
-// new java.util.Scanner(System.in).nextLine();
-//
-// return true
-// }
-//
-// // store appropriate values here, will be update in a finally branch
-// var bodyToRestore = oldBody
-// var preconditionToRestore = Some(oldPrecondition)
-//
-// // because first initial test
-// holeFunDef.precondition = preconditionToRestore
-//
-// // debug
-// println("Going to generating counterexamples: " + holeFunDef)
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-//
-// // println("Counterexample cheking: ")
-// // println("Counterexamples: " + ExampleRunner.counterExamples.mkString("\n"))
-// // val counterExampleCheck = ExampleRunner.check(BooleanLiteral(true), newBody, holeFunDef.getPostcondition)
-// // println("Result of check: " + counterExampleCheck )
-// //
-// val temp = System.currentTimeMillis
-// // get counterexamples
-// val (maps, precondition) = generateCounterexamples(program, holeFunDef, 5)
-// val temptime = System.currentTimeMillis - temp
-// println("gen counterexamples took " + temptime)
-// verTime += temptime
-//
-// // collect (add) counterexamples
-// //ExampleRunner.counterExamples ++= maps
-//
-// 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
-// }
-//
-// // will modify funDef body and precondition, restore it later
-// try {
-// // TODO is this okay?
-// // if there are no returned counterexamples just go to the next snippet
-// // and so far counter examples passed
-// if (!maps.isEmpty /*&& counterExampleCheck */ ) {
-// // proceed with synthesizing boolean expressions
-// assertEquals(5, maps.size)
-// // set program to the solver
-// solver.setProgram(program)
-//
-// // initialize builder with previously seen declarations
-// val newBuilder = new InitialEnvironmentBuilder
-// newBuilder.addDeclarations(allDeclarations)
-//
-// fine("all declarations now, size: " + newBuilder.getAllDeclarations.size)
-//
-// // synthesize solution
-// val queryBuilder = new LeonQueryBuilder(BooleanType)
-// val query = queryBuilder.getQuery
-// val engine = new Engine(newBuilder, query, new WeightScheduler(), TimeOut(Config.getTimeOutSlot))
-// val solution = engine.run()
-// assertNotNull(solution)
-//
-// assertNotNull(codeGenerator)
-// assertNotNull(allDeclarations)
-// // reconstruct (only defined number of boolean expressions)
-// val innerSnippets = Reconstructor(solution.getNodes.head, codeGenerator) take numberOfBooleanSnippets
-// checkDeclarations(inSynth)
-//
-// // debugging
-// // for ((snippetTree, ind) <- (innerSnippets map { _.getSnippet }) zip Iterator.range(0, 20).toStream) {
-// // println(ind + " boolean snippetTree is: " + snippetTree)
-// // }
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-//
-// // precondition found?
-// var found = false
-//
-// // iterate over boolean snippets
-// val iterator = innerSnippets.iterator
-// while (!found && iterator.hasNext) {
-// val innerSnippetTree = iterator.next.getSnippet
-//
-// // debug
-// println("boolean snippet is: " + innerSnippetTree)
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-//
-// val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, precondition)
-//
-// found = innerFound
-// innerPrec match {
-// case s @ Some(_) =>
-// preconditionToRestore = s
-// case _ =>
-// }
-//
-// if (found)
-// return true
-//
-// } // iterating over all boolean solutions
-//
-// // if none of boolean solutions work, restore body (in finally)
-// //holeFunDef.body = Some(oldBody)
-//
-// assertTrue(!found)
-// info("not found :(, we give up on this branch expression")
-// return false
-//
-// } // if ( !maps.isEmpty ) {
-//
-// false
-// } // try
-// finally {
-// // set these to the FunDef
-// holeFunDef.precondition = preconditionToRestore
-// // restore old body (we accumulate expression)
-// holeFunDef.body = Some(oldBody)
-// }
-// }
-//
-// def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: Expr): (Boolean, Option[Expr]) = {
-//
-// // debug
-// // println("boolean snippet is: " + innerSnippetTree)
-// // System.out.println("Press Any Key To Continue...");
-// // new java.util.Scanner(System.in).nextLine();
-//
-// // 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 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) =>
-// // old precondition is not here, it is before counterexamples are derived!
-// //val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
-//
-// // if expression implies counterexamples add it to the precondition and try to validate program
-// holeFunDef.precondition = Some(newCondition)
-// // do analysis
-// analyzeProgram(program)
-// // program is valid, we have a branch
-// if (Globals.allSolved == Some(true)) {
-// // we found a branch
-// info("Wow! we found a branch!")
-//
-// // update accumulating expression
-// val oldAccumulatingExpression = accumulatingExpression
-// val newAccumulatingExpression =
-// (finalExpr: Expr) =>
-// oldAccumulatingExpression(IfExpr(innerSnippetTree, snippetTree, finalExpr))
-//
-// 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)
-//
-// // check for refinements
-// checkRefinements(innerSnippetTree) match {
-// case Some(refinementPair @ (id, classType)) =>
-// fine("And now we have refinement type: " + refinementPair)
-// fine("variableRefinements(id) before" + variableRefinements(id))
-// variableRefinements(id) -= loader.classMap(classType.id)
-// fine("variableRefinements(id) after" + variableRefinements(id))
-//
-// // if we have a single subclass possible to refine
-// if (variableRefinements(id).size == 1) {
-// fine("wow we an do variable refinement for " + id)
-//
-// val newType = variableRefinements(id).head
-// fine("new type is: " + newType)
-//
-// // update declarations
-// allDeclarations =
-// for (dec <- allDeclarations)
-// yield dec match {
-// case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, LeonVariable(`id`))) =>
-// LeonDeclaration(
-// imex, TypeTransformer(newType), newType)
-// case _ =>
-// dec
-// }
-//
-// } else
-// fine("we cannot do variable refinement :(")
-// case _ =>
-// }
-// // found a boolean snippet, break
-// (true, preconditionToRestore)
-// } else {
-// // reset funDef and continue with next boolean snippet
-// val preconditionToRestore = Some(accumulatingPrecondition)
-// (false, preconditionToRestore)
-// }
-//
-// case _ =>
-// println("precondition was not applied")
-// (false, None)
-// } //solveReturn match { (for implying counterexamples)
-// } // notFalseSolveReturn match {
-// }
-//
-// // inspect the expression if some refinements can be done
-// def checkRefinements(expr: Expr) = expr match {
-// case CaseClassInstanceOf(classDef, LeonVariable(id)) =>
-// Some((id, classDef))
-// case _ =>
-// None
-// }
-//
-// def extractInformation(ctx: LeonContext, file: String) =
-// new HoleFinder(file).extract
-//
-//}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/VariableRefinerTest.scala b/src/test/scala/lesynth/VariableRefinerTest.scala
index f1be15d79..b45282229 100644
--- a/src/test/scala/lesynth/VariableRefinerTest.scala
+++ b/src/test/scala/lesynth/VariableRefinerTest.scala
@@ -12,6 +12,8 @@ import leon.purescala.Trees._
import insynth.leon._
+import lesynth.refinement._
+
class VariableRefinerTest extends FunSpec with GivenWhenThen {
val listClassId = FreshIdentifier("List")
diff --git a/src/test/scala/lesynth/VerifierTest.scala b/src/test/scala/lesynth/VerifierTest.scala
new file mode 100644
index 000000000..3eb0c5a60
--- /dev/null
+++ b/src/test/scala/lesynth/VerifierTest.scala
@@ -0,0 +1,90 @@
+package lesynth
+
+import org.junit.Assert._
+import org.junit._
+import org.scalatest._
+import org.scalatest.matchers._
+
+import insynth.leon.loader.LeonLoader
+
+import _root_.leon.purescala._
+import _root_.leon.evaluators._
+import _root_.leon.solvers._
+
+import util._
+
+class VerifierTest extends FunSpec {
+
+ import Utils._
+ import Scaffold._
+ import TestConfig._
+
+ describe("Concrete verifier: ") {
+ val testCaseFileName = lesynthTestDir + "/verifier/ListConcat.scala"
+
+ val problems = forFile(testCaseFileName)
+ assert(problems.size == 1)
+
+ for ((sctx, funDef, problem) <- problems) {
+
+ val timeoutSolver = new TimeoutSolver(sctx.solver, 2000L)
+
+ describe("A Verifier") {
+ it("should verify first correct concat body") {
+ funDef.body = getFunDefByName(sctx.program, "goodConcat1").body
+
+ val verifier = new Verifier(timeoutSolver.getNewSolver, problem)
+
+ verifier.analyzeFunction(funDef)._1
+ }
+
+ it("should verify 2nd correct concat body") {
+ funDef.body = getFunDefByName(sctx.program, "goodConcat2").body
+
+ val verifier = new Verifier(timeoutSolver.getNewSolver, problem)
+
+ verifier.analyzeFunction(funDef)._1
+ }
+
+ it("should not verify an incorrect concat body") {
+ funDef.body = getFunDefByName(sctx.program, "badConcat1").body
+
+ val verifier = new Verifier(timeoutSolver.getNewSolver, problem)
+
+ ! verifier.analyzeFunction(funDef)._1
+ }
+ }
+ }
+ }
+
+ describe("Relaxed verifier: ") {
+ val testCaseFileName = lesynthTestDir + "/verifier/BinarySearchTree.scala"
+
+ val problems = forFile(testCaseFileName)
+ assert(problems.size == 1)
+
+ for ((sctx, funDef, problem) <- problems) {
+
+ val timeoutSolver = new TimeoutSolver(sctx.solver, 1000L)
+
+ describe("A RelaxedVerifier on BST") {
+ it("should verify a correct member body") {
+ funDef.body = getFunDefByName(sctx.program, "goodMember").body
+
+ val verifier = new RelaxedVerifier(timeoutSolver.getNewSolver, problem)
+
+ verifier.analyzeFunction(funDef)._1
+ }
+
+ it("should not verify an incorrect member body") {
+ funDef.body = getFunDefByName(sctx.program, "badMember").body
+
+ val verifier = new Verifier(timeoutSolver.getNewSolver, problem)
+
+ verifier.analyzeFunction(funDef)._1
+ }
+ }
+ }
+ }
+
+}
diff --git a/src/test/scala/lesynth/util/Scaffold.scala b/src/test/scala/lesynth/util/Scaffold.scala
new file mode 100644
index 000000000..218337fcd
--- /dev/null
+++ b/src/test/scala/lesynth/util/Scaffold.scala
@@ -0,0 +1,96 @@
+package lesynth
+package util
+
+import org.scalatest.FunSuite
+import org.scalatest.matchers.ShouldMatchers._
+
+import java.io.{BufferedWriter, FileWriter, File}
+
+import leon._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.solvers.z3._
+import leon.solvers.Solver
+import leon.synthesis._
+import leon.synthesis.utils._
+
+object Scaffold {
+
+ def forProgram(content: String): Iterable[(SynthesisContext, FunDef, Problem)] = {
+
+ val ctx = LeonContext(
+ settings = Settings(
+ synthesis = true,
+ xlang = false,
+ verify = false
+ ),
+ files = List(),
+ reporter = new SilentReporter
+ )
+// Settings.showIDs = true
+
+ val pipeline = leon.plugin.TemporaryInputPhase andThen leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
+
+ val (program, results) = try {
+ pipeline.run(ctx)((content, Nil))
+ } catch {
+ case _ =>
+ fail("Error while processing")
+ }
+
+ extractProblems(ctx, program, results)
+ }
+
+ def forFile(file: String): Iterable[(SynthesisContext, FunDef, Problem)] = {
+ val programFile = new File(file)
+
+ val ctx = LeonContext(
+ settings = Settings(
+ synthesis = true,
+ xlang = false,
+ verify = false
+ ),
+ files = List(programFile),
+ reporter = new SilentReporter
+ )
+
+ val pipeline = leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
+
+ val (program, results) = try {
+ pipeline.run(ctx)(file :: Nil)
+ } catch {
+ case _ =>
+ fail("Error while processing " + file)
+ }
+
+ extractProblems(ctx, program, results)
+ }
+
+ private def extractProblems(ctx: LeonContext, program: Program,
+ problemMap: Map[leon.purescala.Definitions.FunDef,Seq[leon.synthesis.Problem]]) = {
+
+ val opts = SynthesisOptions()
+
+ val solver = new FairZ3Solver(ctx)
+ solver.setProgram(program)
+
+ val simpleSolver = new UninterpretedZ3Solver(ctx)
+ simpleSolver.setProgram(program)
+
+ for ((f, ps) <- problemMap; p <- ps)
+ yield {
+ val sctx = SynthesisContext(ctx,
+ opts,
+ Some(f),
+ program,
+ solver,
+ simpleSolver,
+ new SilentReporter,
+ new java.util.concurrent.atomic.AtomicBoolean)
+
+ (sctx, f, p)
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/util/TestConfig.scala b/src/test/scala/lesynth/util/TestConfig.scala
new file mode 100644
index 000000000..cdcb14fdc
--- /dev/null
+++ b/src/test/scala/lesynth/util/TestConfig.scala
@@ -0,0 +1,40 @@
+package lesynth
+package util
+
+import java.util.logging.FileHandler
+import java.util.logging.Level
+import java.util.logging.SimpleFormatter
+
+import insynth.Config
+
+// used to configure global setting before tests are run
+object TestConfig {
+
+ // create a file handler with appropriate path (no appending)
+ val inSynthHandler = new FileHandler("insynthleon.txt", true);
+ // set to log all levels
+ inSynthHandler.setLevel(Level.ALL);
+ // set simple text formatter
+ inSynthHandler.setFormatter(new SimpleFormatter);
+
+ Config.setLoggerHandler(inSynthHandler)
+
+ val testDir = "testcases/insynth-leon-tests/"
+
+ val synthesisTestDir = "testcases/insynth-synthesis-tests/"
+
+ val lesynthTestDir = "testcases/lesynth/test/"
+
+ val HOME_FOLDER = "/home/kuraj/"
+
+ val classpathArray = Array(
+ "target/scala-2.9.2/classes",
+ "library/target/scala-2.9.2/classes",
+ "unmanaged/64/cafebabe_2.9.2-1.2.jar",
+ "unmanaged/64/scalaz3.jar",
+ HOME_FOLDER + ".ivy2/cache/com.typesafe.akka/akka-actor/jars/akka-actor-2.0.4.jar",
+ HOME_FOLDER + ".ivy2/cache/com.typesafe/config/bundles/config-0.3.1.jar",
+ HOME_FOLDER + ".sbt/boot/scala-2.9.2/lib/scala-library.jar",
+ HOME_FOLDER + ".sbt/boot/scala-2.9.2/lib/scala-compiler.jar"
+ )
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/util/Utils.scala b/src/test/scala/lesynth/util/Utils.scala
new file mode 100644
index 000000000..56fb6c6e4
--- /dev/null
+++ b/src/test/scala/lesynth/util/Utils.scala
@@ -0,0 +1,33 @@
+package lesynth
+package util
+
+import org.scalatest.FunSuite
+import org.scalatest.matchers.ShouldMatchers._
+
+import java.io.{BufferedWriter, FileWriter, File}
+
+import leon._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.solvers.z3._
+import leon.solvers.Solver
+import leon.synthesis._
+import leon.synthesis.utils._
+
+object Utils {
+
+ def getFunDefByName(program: Program, name: String) = {
+ assert(program.definedFunctions.exists({
+ funDef: FunDef => funDef.id.name == name
+ }), "Function " + name + " not found. All functions: " + program.definedFunctions.map(_.id.name).mkString(", "))
+
+ program.definedFunctions.find({
+ funDef: FunDef => funDef.id.name == name
+ }) match {
+ case Some(res) => res
+ case _ => null
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/testcases/lesynth/BinarySearchTree.scala b/testcases/lesynth/BinarySearchTree.scala
deleted file mode 100644
index cada54218..000000000
--- a/testcases/lesynth/BinarySearchTree.scala
+++ /dev/null
@@ -1,94 +0,0 @@
-import scala.collection.immutable.Set
-
-import leon.Annotations._
-import leon.Utils._
-
-object BinarySearchTree {
- sealed abstract class Tree
- case class Node(left: Tree, value: Int, right: Tree) extends Tree
- case class Leaf() extends Tree
-
- def contents(tree: Tree): Set[Int] = tree match {
- case Leaf() => Set.empty[Int]
- case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
- }
-
- def isSorted(tree: Tree): Boolean = tree match {
- case Leaf() => true
- case Node(Leaf(), v, Leaf()) => true
- case Node(l@Node(_, vIn, _), v, Leaf()) => v > vIn && isSorted(l)
- case Node(Leaf(), v, r@Node(_, vIn, _)) => v < vIn && isSorted(r)
- case Node(l@Node(_, vInLeft, _), v, r@Node(_, vInRight, _)) =>
- v > vInLeft && v < vInRight && isSorted(l) && isSorted(r)
- }
-
- def member(tree: Tree, value: Int): Boolean = {
- require(isSorted(tree))
- tree.isInstanceOf[Node]
- } ensuring (res => res && contents(tree).contains(value) ||
- (!res && !contents(tree).contains(value)))
-
-// def member(tree: Tree, value: Int): Boolean = {
-// require(isSorted(tree))
-// tree match {
-// case Leaf() => false
-// case n @ Node(l, v, r) => if (v < value) {
-// member(r, value)
-// } else if (v > value) {
-// member(l, value)
-// } else {
-// true
-// }
-// }
-// } ensuring (_ || !(contents(tree) == contents(tree) ++ Set(value)))
-//
-// def insert(tree: Tree, value: Int): Node = {
-// require(isSorted(tree))
-// tree match {
-// case Leaf() => Node(Leaf(), value, Leaf())
-// case n @ Node(l, v, r) => if (v < value) {
-// Node(l, v, insert(r, value))
-// } else if (v > value) {
-// Node(insert(l, value), v, r)
-// } else {
-// n
-// }
-// }
-// } ensuring (res => contents(res) == contents(tree) ++ Set(value) && isSorted(res))
-
- // def treeMin(tree: Node): Int = {
- // require(isSorted(tree).sorted)
- // tree match {
- // case Node(left, v, _) => left match {
- // case Leaf() => v
- // case n@Node(_, _, _) => treeMin(n)
- // }
- // }
- // }
- //
- // def treeMax(tree: Node): Int = {
- // require(isSorted(tree).sorted)
- // tree match {
- // case Node(_, v, right) => right match {
- // case Leaf() => v
- // case n@Node(_, _, _) => treeMax(n)
- // }
- // }
- // }
-
-// def remove(tree: Tree, value: Int): Node = {
-// require(isSorted(tree))
-// tree match {
-// case l @ Leaf() => l
-// case n @ Node(l, v, r) => if (v < value) {
-// Node(l, v, insert(r, value))
-// } else if (v > value) {
-// Node(insert(l, value), v, r)
-// } else {
-// n
-// }
-// }
-// } ensuring (contents(_) == contents(tree) -- Set(value))
-
-}
-
diff --git a/testcases/lesynth/InsertionSortFull.scala b/testcases/lesynth/InsertionSortFull.scala
deleted file mode 100644
index 6b68a439e..000000000
--- a/testcases/lesynth/InsertionSortFull.scala
+++ /dev/null
@@ -1,51 +0,0 @@
-import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
-
-object InsertionSort {
- sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
- case class Nil() extends List
-
- def size(l : List) : Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def contents(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
- }
-
- def isSorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x, Nil()) => true
- case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
-
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def sortedIns(e: Int, l: List): List = {
- require(isSorted(l))
- l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) =>
- if (x <= e) Cons(x,sortedIns(e, xs))
- else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
- && isSorted(res)
- && size(res) == size(l) + 1
- )
-
- /* Insertion sort yields a sorted list of same size and content as the input
- * list */
- def sort(l: List): List = (l match {
- case Nil() => Nil()
- case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
- && isSorted(res)
- && size(res) == size(l)
- )
-
-}
diff --git a/testcases/lesynth/InsertionSortHoleInsert.scala b/testcases/lesynth/InsertionSortHoleInsert.scala
deleted file mode 100644
index cde3aaacd..000000000
--- a/testcases/lesynth/InsertionSortHoleInsert.scala
+++ /dev/null
@@ -1,54 +0,0 @@
-import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
-
-object InsertionSort {
- sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
- case class Nil() extends List
-
- def size(l : List) : Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def contents(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
- }
-
- def isSorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x, Nil()) => true
- case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
-
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def sortedIns(e: Int, l: List): List = {
- require(isSorted(l))
- hole(l)
-// val cond1: Boolean = /*!*/
-// l match {
-// case Nil() => /*!*/ // Cons(e,Nil())
-// case Cons(x,xs) =>
-// val cond2: Boolean = /*!*/
-// if (x <= e) /*!*/ // Cons(x,sortedIns(e, xs))
-// else /*!*/ // Cons(e, l)
-// }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
- && isSorted(res)
- && size(res) == size(l) + 1
- )
-
- /* Insertion sort yields a sorted list of same size and content as the input
- * list */
- def sort(l: List): List = (l match {
- case Nil() => Nil()
- case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
- && isSorted(res)
- && size(res) == size(l)
- )
-
-}
diff --git a/testcases/lesynth/InsertionSortHoleSort.scala b/testcases/lesynth/InsertionSortHoleSort.scala
deleted file mode 100644
index 7931fcc8a..000000000
--- a/testcases/lesynth/InsertionSortHoleSort.scala
+++ /dev/null
@@ -1,53 +0,0 @@
-import scala.collection.immutable.Set
-import leon.Annotations._
-import leon.Utils._
-
-object InsertionSort {
- sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
- case class Nil() extends List
-
- def size(l : List) : Int = (l match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def contents(l: List): Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
- }
-
- def isSorted(l: List): Boolean = l match {
- case Nil() => true
- case Cons(x, Nil()) => true
- case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
-
- /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
- * the expected content and size */
- def sortedIns(e: Int, l: List): List = {
- require(isSorted(l))
- l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) =>
- if (x <= e) Cons(x,sortedIns(e, xs))
- else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
- && isSorted(res)
- && size(res) == size(l) + 1
-)
-
- /* Insertion sort yields a sorted list of same size and content as the input
- * list */
- def xxsort(l: List): List = ({
- hole(l)
-// val cond: Boolean = /*!*/
-// case Nil() => /*!*/ // Nil()
-// case Cons(x,xs) => /*!*/ // sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
- && isSorted(res)
- && size(res) == size(l)
- )
-
-}
diff --git a/testcases/lesynth/ListOperations.scala b/testcases/lesynth/ListOperations.scala
deleted file mode 100644
index 424a38aa0..000000000
--- a/testcases/lesynth/ListOperations.scala
+++ /dev/null
@@ -1,45 +0,0 @@
-import scala.collection.immutable.Set
-
-import leon.Utils._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
-// def content(l: List) : Set[Int] = l match {
-// case Nil() => Set.empty
-// case Cons(head, tail) => Set(head) ++ content(tail)
-// }
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(head, tail) => Set(head) ++ content(tail)
- }
-
- def size(l: List) : Int = l match {
- case Nil() => 0
- case Cons(head, tail) => 1 + size(tail)
- }
-
- def isEmpty(l: List) = l match {
- case Nil() => true
- case Cons(_, _) => false
- }
-
- def concat(l1: List, l2: List) : List = ({
-
- l1 match {
- case Nil() => l2
- case Cons(l1Head, l1Tail) =>
- l1 match {
- case Nil() => l2
- case _ => Cons(l1Head, Cons(l1Head, concat(l1Tail, l2)))
- }
- }
-
- }) ensuring(res =>
- content(res) == content(l1) ++ content(l2) &&
- size(res) == size(l1) + size(l2)
- )
-
-}
diff --git a/testcases/lesynth/ListOperationsHole.scala b/testcases/lesynth/ListOperationsHole.scala
deleted file mode 100644
index bd3cb28e6..000000000
--- a/testcases/lesynth/ListOperationsHole.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-import scala.collection.immutable.Set
-
-import leon.Utils._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(head, tail) => Set(head) ++ content(tail)
- }
-
-// def isEmpty(l: List) = l match {
-// case Nil() => true
-// case Cons(_, _) => false
-// }
-
- def concat(l1: List, l2: List) : List = ({
- hole(l1)
- }) ensuring(res => content(res) == content(l1) ++ content(l2))
-
-}
diff --git a/testcases/lesynth/ListOperationsHole2.scala b/testcases/lesynth/ListOperationsHole2.scala
deleted file mode 100644
index c1dcf85ac..000000000
--- a/testcases/lesynth/ListOperationsHole2.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-import scala.collection.immutable.Set
-
-import leon.Utils._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(head, tail) => Set(head) ++ content(tail)
- }
-
-// def isEmpty(l: List) = l match {
-// case Nil() => true
-// case Cons(_, _) => false
-// }
-
- def concat(l1: List, l2: List) : List = ({
- hole[List](throw new RuntimeException)
- }) ensuring(res => content(res) == content(l1) ++ content(l2))
-
-}
diff --git a/testcases/lesynth/MergeSortHole.scala b/testcases/lesynth/MergeSortHole.scala
deleted file mode 100644
index 339554c2c..000000000
--- a/testcases/lesynth/MergeSortHole.scala
+++ /dev/null
@@ -1,81 +0,0 @@
-import scala.collection.immutable.Set
-
-import leon.Utils._
-
-object MergeSort {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- sealed abstract class PairAbs
- case class Pair(fst : List, snd : List) extends PairAbs
-
- def contents(l : List) : Set[Int] = l match {
- case Nil() => Set.empty
- case Cons(x,xs) => contents(xs) ++ Set(x)
- }
-
- def isSorted(l : List) : Boolean = l match {
- case Nil() => true
- case Cons(x,xs) => xs match {
- case Nil() => true
- case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
- }
- }
-
- def size(list : List) : Int = list match {
- case Nil() => 0
- case Cons(x,xs) => 1 + size(xs)
- }
-
- def splithelper(aList : List, bList : List, n : Int) : Pair = {
- if (n <= 0) Pair(aList,bList)
- else
- bList match {
- case Nil() => Pair(aList,bList)
- case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
- }
- } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
-
-// def split(list : List, n : Int): Pair = {
-// splithelper(Nil(),list,n)
-// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
-
- def split(list: List): Pair = {
- splithelper(Nil(),list,2)
- } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
-
- def merge(aList : List, bList : List) : List = {
- require(isSorted(aList) && isSorted(bList))
- bList match {
- case Nil() => aList
- case Cons(x,xs) =>
- aList match {
- case Nil() => bList
- case Cons(y,ys) =>
- if (y < x)
- Cons(y,merge(ys, bList))
- else
- Cons(x,merge(aList, xs))
- }
- }
- } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
-
- def isEmpty(list: List) : Boolean = list match {
- case Nil() => true
- case Cons(x,xs) => false
- }
-
- def xxmergeSort(list : List) : List = ({
- hole[List](list)
-// list match {
-// case Nil() => list
-// case Cons(x,Nil()) => list
-// case _ =>
-// val p = split(list,size(list)/2)
-// merge(mergeSort(p.fst), mergeSort(p.snd))
-
-// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
- }) ensuring(res => contents(res) == contents(list) && isSorted(res))
-
-}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
index 4faa50286..56ceaaa9b 100644
--- a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
@@ -15,26 +15,36 @@ object BatchedQueue {
def content(p: Queue): Set[Int] =
content(p.f) ++ content(p.r)
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def size(q: Queue) : Int =
+ size(q.f) + size(q.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
case class Queue(f: List, r: List)
def rev_append(aList: List, bList: List): List = (aList match {
case Nil => bList
case Cons(x, xs) => rev_append(xs, Cons(x, bList))
- }) ensuring (content(_) == content(aList) ++ content(bList))
-
- def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
-
+ }) ensuring (
+ res =>
+ content(res) == content(aList) ++ content(bList) &&
+ size(res) == size(aList) + size(bList)
+ )
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (
+ res =>
+ content(res) == content(list) && size(res) == size(list)
+ )
+
def invariantList(q:Queue, f: List, r: List): Boolean = {
rev_append(q.f, q.r) == rev_append(f, r) &&
{ if (q.f == Nil) q.r == Nil else true }
}
-
- def tail(p: Queue): Queue = {
- p.f match {
- case Nil => p
- case Cons(_, xs) => checkf(xs, p.r)
- }
- }
//(f match {
// case Nil => Queue(reverse(r), Nil)
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
index 6541b33b5..cf30f2f1b 100644
--- a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
@@ -15,6 +15,8 @@ object BatchedQueue {
def content(p: Queue): Set[Int] =
content(p.f) ++ content(p.r)
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
case class Queue(f: List, r: List)
def rev_append(aList: List, bList: List): List = (aList match {
@@ -24,24 +26,28 @@ object BatchedQueue {
def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
- def invariantList(q:Queue, f: List, r: List): Boolean = {
- rev_append(q.f, q.r) == rev_append(f, r) &&
- { if (q.f == Nil) q.r == Nil else true }
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
}
-
+
+ def head(p: Queue): Set[Int] = (
+ p.f match {
+ case Nil => Set[Int]()
+ case Cons(x, xs) => Set(x)
+ }) ensuring (
+ res =>
+ if (isEmpty(p)) true
+ else content(p) == res ++ content(tail(p)))
+
def tail(p: Queue): Queue = {
p.f match {
case Nil => p
case Cons(_, xs) => checkf(xs, p.r)
}
}
-
- def checkf(f: List, r: List): Queue = (f match {
- case Nil => Queue(reverse(r), Nil)
- case _ => Queue(f, r)
- }) ensuring {
- res => content(res) == content(f) ++ content(r)
- }
//
// def last(p: Queue): Int = {
// require(!isEmpty(p))
@@ -54,7 +60,16 @@ object BatchedQueue {
def snoc(p: Queue, x: Int): Queue =
choose { (res: Queue) =>
content(res) == content(p) ++ Set(x) &&
- (p.f == Nil || content(tail(res)) ++
- Set(x) == content(tail(res)))
+ (if (isEmpty(p)) true
+ else content(tail(res)) ++ Set(x) == content(tail(res)))
}
+
+ def main(args: Array[String]): Unit = {
+ val pair = Queue(Cons(4, Nil), Cons(3, Nil))
+
+ println(head(pair))
+ println(content(pair) == head(pair) ++ content(tail(pair)))
+
+ println(head(Queue(Nil, Nil)))
+ }
}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
index d35737dab..83253e101 100644
--- a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
@@ -15,42 +15,67 @@ object BatchedQueue {
def content(p: Queue): Set[Int] =
content(p.f) ++ content(p.r)
- def isEmpty(p: Queue): Boolean = p.f == Nil
+ def size(l: List): Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def size(q: Queue): Int =
+ size(q.f) + size(q.r)
+
+// def isEmpty(p: Queue): Boolean = p.f == Nil && p.r == Nil
case class Queue(f: List, r: List)
def rev_append(aList: List, bList: List): List = (aList match {
case Nil => bList
case Cons(x, xs) => rev_append(xs, Cons(x, bList))
- }) ensuring (content(_) == content(aList) ++ content(bList))
+ }) ensuring (
+ res =>
+ content(res) == content(aList) ++ content(bList) &&
+ size(res) == size(aList) + size(bList))
- def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+ def reverse(list: List) = rev_append(list, Nil) ensuring (
+ res =>
+ content(res) == content(list) && size(res) == size(list))
- def invariantList(q:Queue, f: List, r: List): Boolean = {
- rev_append(q.f, q.r) == rev_append(f, r) &&
- { if (q.f == Nil) q.r == Nil else true }
- }
-
def checkf(f: List, r: List): Queue = (f match {
case Nil => Queue(reverse(r), Nil)
case _ => Queue(f, r)
}) ensuring {
- res => content(res) == content(f) ++ content(r)
+ res =>
+ content(res) == content(f) ++ content(r) &&
+ size(res) == size(f) + size(r)
}
+
+ def head(p: Queue): List = {
+ p.f match {
+ case Nil => Nil
+ case Cons(x, xs) => Cons(x, Nil)
+ }
+ }
+
+ def correctQueue(q:Queue) = if (q.f == Nil) q.r == Nil else true
- def tail(p: Queue): Queue = {
- require( if (p.f == Nil) p.r == Nil else true )
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r)
+ }
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
// p.f match {
// case Nil => p
// case Cons(_, xs) => checkf(xs, p.r)
// }
+ def tail(p: Queue): List = {
+ require(correctQueue(p))
choose {
- (res: Queue) =>
- p.f match {
- case Nil => isEmpty(res)
- case Cons(x, xs) => content(res) ++ Set(x) == content(p) && content(res) != content(p)
- }
+ (res: List) =>
+ invariantList(p, merge(head(p), res), Nil)
}
}
-
+
}
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala b/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
index 987c538c4..82be984ba 100644
--- a/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
+++ b/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
@@ -42,7 +42,7 @@ object MergeSort {
// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
def split(list: List): Pair = {
- splithelper(Nil(),list,size(list)/2)
+ splithelper(Nil(),list,2)
} ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
def merge(aList : List, bList : List) : List = {
diff --git a/testcases/lesynth/synthesis/Other/Addresses.scala b/testcases/lesynth/synthesis/Other/Addresses.scala
new file mode 100644
index 000000000..1563ee5eb
--- /dev/null
+++ b/testcases/lesynth/synthesis/Other/Addresses.scala
@@ -0,0 +1,85 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(a: Int, b: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def setA(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(a, l1) => Set(a) ++ setA(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def hasPrivate(l: List): Boolean = l match {
+ case Nil => false
+ case Cons(a, l1) =>
+ if (a.priv) true
+ else hasPrivate(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ hasPrivate(res.pers) && !hasPrivate(res.business)
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
index 6b9a73a9c..2c14f9619 100644
--- a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
+++ b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
@@ -3,21 +3,16 @@ import leon.Annotations._
import leon.Utils._
object Addresses {
- case class Info(
- address: Int,
- zipcode: Int,
- local: Boolean
- )
- case class Address(info: Info, priv: Boolean)
+ case class Address(a: Int, b: Int, priv: Boolean)
sealed abstract class List
case class Cons(a: Address, tail:List) extends List
case object Nil extends List
- def content(l: List) : Set[Address] = l match {
+ def setA(l: List) : Set[Address] = l match {
case Nil => Set.empty[Address]
- case Cons(addr, l1) => Set(addr) ++ content(l1)
+ case Cons(a, l1) => Set(a) ++ setA(l1)
}
def size(l: List) : Int = l match {
@@ -42,13 +37,6 @@ object Addresses {
case class AddressBook(business : List, pers : List)
def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
-
- def isEmpty(ab: AddressBook) = size(ab) == 0
-
- def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
-
- def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
-
// def makeAddressBook(l: List): AddressBook = (l match {
// case Nil => AddressBook(Nil, Nil)
@@ -97,7 +85,8 @@ object Addresses {
def makeAddressBook(l: List): AddressBook =
choose {
(res: AddressBook) =>
- size(res) == size(l) && addressBookInvariant(res)
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business)
}
}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
index c22541f8c..c13af538a 100644
--- a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
+++ b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
@@ -10,9 +10,9 @@ object Addresses {
case class Cons(a: Address, tail:List) extends List
case object Nil extends List
- def content(l: List) : Set[Address] = l match {
+ def setA(l: List) : Set[Address] = l match {
case Nil => Set.empty[Address]
- case Cons(addr, l1) => Set(addr) ++ content(l1)
+ case Cons(a, l1) => Set(a) ++ setA(l1)
}
def size(l: List) : Int = l match {
@@ -41,16 +41,7 @@ object Addresses {
def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
-
- def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
-
- def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
- def merge(l1: List, l2: List): List = l1 match {
- case Nil => l2
- case Cons(a, tail) => Cons(a, merge(tail, l2))
- }
-
// def makeAddressBook(l: List): AddressBook = (l match {
// case Nil => AddressBook(Nil, Nil)
// case Cons(a, l1) => {
@@ -99,8 +90,7 @@ object Addresses {
choose {
(res: AddressBook) =>
size(res) == size(l) &&
- allPrivate(res.pers) && allBusiness(res.business) &&
- content(res) == content(l)
+ allPrivate(res.pers) && allBusiness(res.business)
}
}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala b/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
index 0d6d8c067..c40625ad4 100644
--- a/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
+++ b/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
@@ -3,21 +3,16 @@ import leon.Annotations._
import leon.Utils._
object Addresses {
- case class Info(
- address: Int,
- zipcode: Int,
- phoneNumber: Int
- )
- case class Address(info: Info, priv: Boolean)
+ case class Address(a: Int, b: Int, priv: Boolean)
sealed abstract class List
case class Cons(a: Address, tail:List) extends List
case object Nil extends List
- def content(l: List) : Set[Address] = l match {
+ def setA(l: List) : Set[Address] = l match {
case Nil => Set.empty[Address]
- case Cons(addr, l1) => Set(addr) ++ content(l1)
+ case Cons(a, l1) => Set(a) ++ setA(l1)
}
def size(l: List) : Int = l match {
@@ -41,15 +36,13 @@ object Addresses {
case class AddressBook(business : List, pers : List)
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
-
- def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
-
- def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
-
- def isEmpty(ab: AddressBook) = size(ab) == 0
- def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+ def isEmpty(ab: AddressBook) = size(ab) == 0
def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
--
GitLab