diff --git a/src/main/scala/insynth/InSynth.scala b/src/main/scala/insynth/InSynth.scala
index 42d386bc90735608fa63892de65fa5bbfe97f537..ae6d24a7063b9c354b384035fd1286952519ed10 100644
--- a/src/main/scala/insynth/InSynth.scala
+++ b/src/main/scala/insynth/InSynth.scala
@@ -46,6 +46,7 @@ class InSynth(declarations: List[Declaration], goalType: Type, ordered: Boolean
def getExpressions(builder: InitialEnvironmentBuilder) = {
info("InSynth synthesizing type + " + goalType + " with declarations " + builder.getAllDeclarations.mkString("\n"))
val proofTree = solver.getProofTree(builder)
+ info("Proof tree is acquired")
assert(proofTree != null, "Proof tree is null" )
assert(1 == proofTree.getNodes.size)
diff --git a/src/main/scala/insynth/InSynthTemp.scala b/src/main/scala/insynth/InSynthTemp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8c06803df352eedf8f6cea6336c1e3999275831a
--- /dev/null
+++ b/src/main/scala/insynth/InSynthTemp.scala
@@ -0,0 +1,74 @@
+package insynth
+
+import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFactory }
+import insynth.reconstruction.codegen.CodeGenerator
+import insynth.reconstruction.{ FastReconstructor => Reconstructor }
+
+import insynth.interfaces.Declaration
+import insynth.engine.InitialEnvironmentBuilder
+
+import insynth.leon.loader.LeonLoader
+import insynth.leon.LeonQueryBuilder
+
+import _root_.leon.purescala.Definitions.Program
+import _root_.leon.purescala.Trees.Hole
+import _root_.leon.purescala.TypeTrees.{ TypeTree => Type }
+
+import insynth.util.logging.HasLogger
+
+/**
+ * Main class for the synthesis process invocation
+ * @param program Leon program object that contains the hole
+ * @param hole hole in the program on which the synthesis is called
+ */
+class InSynthTemp(declarations: List[Declaration], goalType: Type, ordered: Boolean = true) extends HasLogger {
+
+// def this(program: Program, hole: Hole, ordered: Boolean) =
+// this(new LeonLoader(program, hole).load, hole.getType, ordered)
+
+ def this(loader: LeonLoader, ordered: Boolean) =
+ this(loader.load, loader.hole.getType, ordered)
+
+ lazy val solver = new Solver(declarations, new LeonQueryBuilder(goalType))
+
+ def getExpressions = {
+ info("InSynth synthesizing type + " + goalType + " with declarations " + solver.allDeclarations.mkString("\n"))
+ val proofTree = solver.getProofTree
+
+ assert(proofTree != null, "Proof tree is null" )
+ assert(1 == proofTree.getNodes.size)
+
+ val codegen = new CodeGenerator
+
+ Reconstructor(proofTree.getNodes.head, codegen, ordered)
+ }
+
+ def getExpressions(builder: InitialEnvironmentBuilder) = {
+ info("InSynth synthesizing type + " + goalType + " with declarations " + builder.getAllDeclarations.mkString("\n"))
+ val proofTree = solver.getProofTree(builder)
+ info("Proof tree is acquired")
+
+ assert(proofTree != null, "Proof tree is null" )
+ assert(1 == proofTree.getNodes.size)
+
+ val codegen = new CodeGenerator
+
+ Reconstructor(proofTree.getNodes.head, codegen, ordered)
+ }
+
+ def getCurrentBuilder = solver.currentBuilder
+
+}
+
+object InSynthTemp {
+
+ def apply(declarations: List[Declaration], goalType: Type, ordered: Boolean) =
+ new InSynthTemp(declarations, goalType, ordered)
+
+// def apply(program: Program, hole: Hole, ordered: Boolean) =
+// new InSynthTemp(new LeonLoader(program, hole).load, hole.getType, ordered)
+
+ def apply(loader: LeonLoader, ordered: Boolean) =
+ new InSynthTemp(loader.load, loader.hole.getType, ordered)
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/LeonDeclaration.scala b/src/main/scala/insynth/leon/LeonDeclaration.scala
index 40255fb76073fd2641eab93c329d69e278446d80..5c263a3dd301e1f2a6513bfe2d7b9a05ae736dd5 100644
--- a/src/main/scala/insynth/leon/LeonDeclaration.scala
+++ b/src/main/scala/insynth/leon/LeonDeclaration.scala
@@ -29,9 +29,9 @@ extends Declaration(inSynthType, weight) {
def getDomainType = leonType
- def getSimpleName = expression.toString
+ def getSimpleName = expression.getSimpleName
- override def toString = getSimpleName + ":" + inSynthType + ":" + leonType + "[" + expression + "]"
+ override def toString = getSimpleName + " : " + inSynthType + " : " + leonType + " [" + expression + "]"
}
diff --git a/src/main/scala/insynth/leon/ReconstructionExpression.scala b/src/main/scala/insynth/leon/ReconstructionExpression.scala
index 26731b2ef069d0babd578b1855b9638a595b32bf..3d9692e45af10dc9b2b1f169a61ef18596bff795 100644
--- a/src/main/scala/insynth/leon/ReconstructionExpression.scala
+++ b/src/main/scala/insynth/leon/ReconstructionExpression.scala
@@ -26,7 +26,7 @@ case object ErrorExpression extends ReconstructionExpression {
object ImmediateExpression {
- def apply(id: Identifier, expr: Expr): ImmediateExpression = ImmediateExpression(id.toString, expr)
+ def apply(id: Identifier, expr: Expr): ImmediateExpression = ImmediateExpression(id.name, expr)
}
@@ -42,7 +42,7 @@ case class ImmediateExpression( name: String, expr: Expr ) extends Reconstructi
object UnaryReconstructionExpression {
- def apply(id: Identifier, funToExpr: Expr => Expr): UnaryReconstructionExpression = UnaryReconstructionExpression(id.toString, funToExpr)
+ def apply(id: Identifier, funToExpr: Expr => Expr): UnaryReconstructionExpression = UnaryReconstructionExpression(id.name, funToExpr)
}
@@ -58,7 +58,7 @@ case class UnaryReconstructionExpression( name: String, funToExpr: Expr => Expr
object NaryReconstructionExpression {
- def apply(id: Identifier, funToExpr: List[Expr] => Expr): NaryReconstructionExpression = NaryReconstructionExpression(id.toString, funToExpr)
+ def apply(id: Identifier, funToExpr: List[Expr] => Expr): NaryReconstructionExpression = NaryReconstructionExpression(id.name, funToExpr)
}
diff --git a/src/main/scala/insynth/leon/loader/DeclarationFactory.scala b/src/main/scala/insynth/leon/loader/DeclarationFactory.scala
index 16c2bd6df1fd19fc412e91c621bf4ada55265400..809de1141df485de7a66c6ce85cdcea78bead39e 100644
--- a/src/main/scala/insynth/leon/loader/DeclarationFactory.scala
+++ b/src/main/scala/insynth/leon/loader/DeclarationFactory.scala
@@ -1,12 +1,11 @@
package insynth.leon.loader
-import insynth.leon.{ LeonDeclaration => Declaration, ReconstructionExpression,
- ErrorExpression, UnaryReconstructionExpression, ImmediateExpression }
+import insynth.leon.{ LeonDeclaration => Declaration, _ }
import insynth.engine.InitialEnvironmentBuilder
-import insynth.structures.{ SuccinctType => InSynthType, Variable => InSynthVariable, _}
+import insynth.structures.{ SuccinctType => InSynthType, Variable => InSynthVariable, _ }
import insynth.leon.TypeTransformer
-import leon.purescala.Definitions.{ Program, FunDef, ClassTypeDef, VarDecl }
+import leon.purescala.Definitions._
import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.Trees._
@@ -45,13 +44,15 @@ object DeclarationFactory {
}
def makeInheritance(from: ClassTypeDef, to: ClassTypeDef) = {
- val expr = UnaryReconstructionExpression(from + " is " + to, identity[Expr] _)
+ val expr = UnaryReconstructionExpression("[" +
+ from.id.name + "=>" + to.id.name + "]", identity[Expr] _)
val inSynthType = Arrow(TSet(TypeTransformer(from)), TypeTransformer(to))
Declaration(expr, inSynthType, Untyped)
}
def makeInheritance(from: ClassType, to: ClassType) = {
- val expr = UnaryReconstructionExpression("Inheritane(" + from.classDef + "<<is>>" + to.classDef + ")", identity[Expr] _)
+ val expr = UnaryReconstructionExpression("[" +
+ from.classDef.id.name + "=>" + to.classDef.id.name + "]", identity[Expr] _)
val inSynthType = Arrow(TSet(TypeTransformer(from)), TypeTransformer(to))
Declaration(expr, inSynthType, FunctionType(List(from), to))
}
@@ -68,6 +69,13 @@ object DeclarationFactory {
throw new RuntimeException
Declaration(getAbsExpression(inSynthType), inSynthType, null)
}
+
+// def makeFieldDeclaration(id: Identifier, caseClassDef: CaseClassType) = {
+// makeDeclaration(
+// NaryReconstructionExpression( id.name , { CaseClass(caseClassDef, _: List[Expr]) } ),
+// FunctionType(caseClassDef.fields map { _.id.getType } toList, classMap(id))
+// )
+// }
// define this for abstract declarations
def getAbsExpression(inSynthType: InSynthType) =
diff --git a/src/main/scala/insynth/leon/loader/HoleExtractor.scala b/src/main/scala/insynth/leon/loader/HoleExtractor.scala
index 2a917c3383ab979d4524cd7eff48a1b55783d119..61248d08b0f3aa093c9cb10053e67cf7ba88a2cb 100644
--- a/src/main/scala/insynth/leon/loader/HoleExtractor.scala
+++ b/src/main/scala/insynth/leon/loader/HoleExtractor.scala
@@ -21,9 +21,9 @@ class HoleExtractor(program: Program, hole: Hole) {
for (
funDef <-program.definedFunctions;
if funDef.hasBody;
- val (foundHole, declarations) = scanMethod(funDef.getBody);
+ (foundHole, declarations) = scanMethod(funDef.getBody);
if foundHole;
- val argDeclarations = funDef.args map { makeArgumentDeclaration(_) }
+ argDeclarations = funDef.args map { makeArgumentDeclaration(_) }
) {
foundHoleCount+=1
diff --git a/src/main/scala/insynth/leon/loader/Loader.scala b/src/main/scala/insynth/leon/loader/Loader.scala
index 44175bd8ecb748cd738ab1b8b7e9cebe20d600f7..47a6d517fabc7c5b4ac7739ac2b04ccca0d24a13 100644
--- a/src/main/scala/insynth/leon/loader/Loader.scala
+++ b/src/main/scala/insynth/leon/loader/Loader.scala
@@ -69,7 +69,7 @@ case class LeonLoader(program: Program, hole: Hole,
fine("adding fields of variable " + variable)
for (field <- fields)
list += makeDeclaration(
- ImmediateExpression( "Field(" + cas + "." + field.id + ")",
+ ImmediateExpression( field.id.name ,
CaseClassSelector(cas, variable.toVariable, field.id) ),
field.id.getType
)
@@ -152,7 +152,7 @@ case class LeonLoader(program: Program, hole: Hole,
case cas: CaseClassDef =>
for (field <- cas.fields)
yield makeDeclaration(
- UnaryReconstructionExpression("Field(" + cas + "." + field.id + ")", { CaseClassSelector(cas, _: Expr, field.id) }),
+ UnaryReconstructionExpression(field.id.name, { CaseClassSelector(cas, _: Expr, field.id) }),
FunctionType(List(classMap(cas.id)), field.id.getType))
}
@@ -166,11 +166,11 @@ case class LeonLoader(program: Program, hole: Hole,
for (caseClassDef@CaseClassDef(id, parent, fields) <- program.definedClasses)
yield fields match {
case Nil => makeDeclaration(
- ImmediateExpression( "Cst(" + id + ")", { CaseClass(caseClassDef, Nil) } ),
+ ImmediateExpression( id.name, { CaseClass(caseClassDef, Nil) } ),
classMap(id)
)
case _ => makeDeclaration(
- NaryReconstructionExpression( "Cst(" + id + ")", { CaseClass(caseClassDef, _: List[Expr]) } ),
+ NaryReconstructionExpression( id.name , { CaseClass(caseClassDef, _: List[Expr]) } ),
FunctionType(fields map { _.id.getType } toList, classMap(id))
)
}
diff --git a/src/main/scala/insynth/leon/loader/PreLoader.scala b/src/main/scala/insynth/leon/loader/PreLoader.scala
index ba25d94687356912889c762159cf766567bfb50f..8d420f8ad1980928f7760fd1093db65a77a77192 100644
--- a/src/main/scala/insynth/leon/loader/PreLoader.scala
+++ b/src/main/scala/insynth/leon/loader/PreLoader.scala
@@ -197,7 +197,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
x: LeonType =>
makeDeclaration(
makeNAE( "If", (args: List[Expr]) => args match {
- case List(cond, then, elze) => IfExpr(cond, then, elze)
+ 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/insynth/reconstruction/FastReconstructor.scala b/src/main/scala/insynth/reconstruction/FastReconstructor.scala
new file mode 100644
index 0000000000000000000000000000000000000000..72cba71ae22fedfdb6a60922f11ab5bee97e1218
--- /dev/null
+++ b/src/main/scala/insynth/reconstruction/FastReconstructor.scala
@@ -0,0 +1,47 @@
+package insynth.reconstruction
+
+import insynth.structures.{ SimpleNode, Weight }
+import insynth.reconstruction.shortcut._
+import insynth.reconstruction.stream.{ Node => LambdaNode, _ }
+import insynth.reconstruction.codegen.CodeGenerator
+
+import insynth.Config
+import insynth.util.format.{ FormatSuccinctNode, FormatIntermediate, FormatStreamUtils }
+import insynth.util.logging.HasLogger
+import insynth.util._
+
+/**
+ * Object for reconstruction of proof trees into output(s)
+ */
+object FastReconstructor extends ( (SimpleNode, CodeGenerator, Boolean) => Stream[Output]) with HasLogger {
+
+ def apply(tree: SimpleNode, codeGenerator: CodeGenerator, streamOrdered: Boolean = false) = {
+ // logging
+ entering("apply", FormatSuccinctNode(tree, 8).toString)
+ fine("reconstructor got proof tree size: " + ProofTreeOperations.size(tree))
+
+ // create an ordered/unordered extractor
+ val transformer =
+ if (streamOrdered)
+ new Transformer2(new OrderedStreamFactory[LambdaNode])
+ else
+ new Transformer2(new UnorderedStreamFactory[LambdaNode])
+
+ // transform the trees (first two steps of the code generation phase)
+ val extractedTrees = transformer(tree)
+
+ // logging
+ info("extractor phase done")
+
+ // for each tree, generate the code for it
+ val generatedCode = extractedTrees map {
+ resPair => Output(codeGenerator(resPair._1), resPair._2)
+ }
+
+ // logging
+ info("solutions are generated")
+
+ generatedCode
+ }
+
+}
diff --git a/src/main/scala/insynth/reconstruction/Output.scala b/src/main/scala/insynth/reconstruction/Output.scala
index fbe07c09655968c097099acf6848b2d715c5ba12..0f0a13a999c38eaf0428138401c56675560d001e 100644
--- a/src/main/scala/insynth/reconstruction/Output.scala
+++ b/src/main/scala/insynth/reconstruction/Output.scala
@@ -9,4 +9,9 @@ import leon.purescala.Trees.Expr
case class Output(snippet: Expr, weight: Weight){
def getSnippet = snippet
def getWeight = weight
+
+ override def equals(obj:Any) = {
+ obj.isInstanceOf[Output] && obj.asInstanceOf[Output].snippet == this.snippet
+ }
+
}
\ No newline at end of file
diff --git a/src/main/scala/insynth/reconstruction/Reconstructor.scala b/src/main/scala/insynth/reconstruction/Reconstructor.scala
index 159f399af5931a095476c92471f72bc3fc05357d..858719a66f1c36adf43c835a5381b744f3e2c80a 100644
--- a/src/main/scala/insynth/reconstruction/Reconstructor.scala
+++ b/src/main/scala/insynth/reconstruction/Reconstructor.scala
@@ -8,6 +8,7 @@ import insynth.reconstruction.codegen.CodeGenerator
import insynth.Config
import insynth.util.format.{ FormatSuccinctNode, FormatIntermediate, FormatStreamUtils }
import insynth.util.logging.HasLogger
+import insynth.util._
/**
* Object for reconstruction of proof trees into output(s)
@@ -17,13 +18,15 @@ object Reconstructor extends ( (SimpleNode, CodeGenerator, Boolean) => Stream[Ou
def apply(tree: SimpleNode, codeGenerator: CodeGenerator, streamOrdered: Boolean = false) = {
// logging
entering("apply", FormatSuccinctNode(tree, 8).toString)
+ fine("reconstructor got proof tree size: " + ProofTreeOperations.size(tree))
// transform the trees (first two steps of the code generation phase)
val transformedTree = IntermediateTransformer(tree)
// logging
info("intermediate transform phase done")
- fine("after intermediate " + FormatIntermediate(transformedTree))
+ finest("after intermediate " + FormatIntermediate(transformedTree))
+ fine("intermediate tree size " + IntermediateTreeOperations.size(transformedTree))
// create an ordered/unordered extractor
val extractor =
@@ -37,7 +40,7 @@ object Reconstructor extends ( (SimpleNode, CodeGenerator, Boolean) => Stream[Ou
// logging
info("extractor phase done")
- fine("got streamable " + FormatStreamUtils(extractor.transformedStreamable))
+ finest("got streamable " + FormatStreamUtils(extractor.transformedStreamable))
// for each tree, generate the code for it
val generatedCode = extractedTrees map {
diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/lesynth/SynthesizerExamples.scala
index 03d696d1219ae98291a11bf0f8cf5bea034e55b2..ddcd81a59b7a777fe499ec28e2391fa3fbb52205 100755
--- a/src/main/scala/lesynth/SynthesizerExamples.scala
+++ b/src/main/scala/lesynth/SynthesizerExamples.scala
@@ -63,13 +63,13 @@ class SynthesizerForRuleExamples(
numberOfCheckInIteration: Int = 5,
exampleRunnerSteps: Int = 4000) extends HasLogger {
- info("Synthesizer:")
- info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
- info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
-// info("leonTimeout: %d".format(leonTimeout))
+ reporter.info("Synthesizer:")
+ reporter.info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
+ reporter.info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
+// reporter.info("leonTimeout: %d".format(leonTimeout))
- info("holeFunDef: %s".format(holeFunDef))
- info("problem: %s".format(problem.toString))
+ reporter.info("holeFunDef: %s".format(holeFunDef))
+ reporter.info("problem: %s".format(problem.toString))
// flag denoting if a correct body has been synthesized
private var found = false
@@ -101,7 +101,7 @@ class SynthesizerForRuleExamples(
// store initial precondition since it will be overwritten
private var initialPrecondition: Expr = _
// accumulate precondition for the remaining branch to synthesize
- private var accumulatingPrecondition: Expr = _
+ private var accumulatingCondition: Expr = _
// accumulate the final expression of the hole
private var accumulatingExpression: Expr => Expr = _
@@ -157,7 +157,7 @@ class SynthesizerForRuleExamples(
reporter.info("######Iteration #" + iteration + " ###############")
reporter.info("####################################")
reporter.info("# precondition is: " + holeFunDef.precondition.getOrElse(BooleanLiteral(true)))
- reporter.info("# accumulatingPrecondition is: " + accumulatingPrecondition)
+ reporter.info("# accumulatingCondition is: " + accumulatingCondition)
reporter.info("# accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
reporter.info("####################################")
interactivePause
@@ -189,9 +189,9 @@ class SynthesizerForRuleExamples(
successfulCandidates
}
-// info("Got candidates of size: " + candidates.size +
+// reporter.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)
+ reporter.info("Got candidates of size: " + candidates.size)
fine("Got candidates: " + candidates.map(_.getSnippet.toString).mkString(",\n"))
interactivePause
@@ -205,24 +205,12 @@ class SynthesizerForRuleExamples(
val ranker = evaluationStrategy.getRanker(candidates, accumulatingExpression, gatheredExamples)
exampleRunner = evaluationStrategy.getExampleRunner
- info("Ranking candidates...")
+ reporter.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
- holeFunDef.precondition = oldPreconditionSaved
- holeFunDef.body = oldBodySaved
-
- // check for timeouts
- if (!keepGoing) break
-
- info("candidate with the most successfull evaluations is: " + maxCandidate.getExpr +
- " with pass count " + passed + " out of " + gatheredExamples.size)
- interactivePause
- numberOfTested += batchSize
-
// get all examples that failed evaluation to filter potential conditions
val evaluation = evaluationStrategy.getEvaluation
// evaluate all remaining examples
@@ -231,15 +219,30 @@ class SynthesizerForRuleExamples(
evaluation.evaluate(maxCandidateInd)
val (evalArray, size) = evaluation.getEvaluationVector(maxCandidateInd)
assert(size == gatheredExamples.size)
- val failedExamples = (gatheredExamples zip evalArray).filterNot {
+ val (passedExamplesPairs, failedExamplesPairs) = (gatheredExamples zip evalArray).partition {
case (ex, result) =>
result
- }.map(_._1)
- fine("Failed examples for the maximum candidate: " + failedExamples.mkString(", "))
+ }
+ val examplesPartition =
+ (passedExamplesPairs.map(_._1), failedExamplesPairs.map(_._1))
+
+ fine("Failed examples for the maximum candidate: " + examplesPartition)
+
+ // restore original precondition and body
+ holeFunDef.precondition = oldPreconditionSaved
+ holeFunDef.body = oldBodySaved
+
+ // check for timeouts
+ if (!keepGoing) break
+
+ reporter.info("candidate with the most successfull evaluations is: " + maxCandidate.getExpr +
+ " with pass count " + passed + " out of " + gatheredExamples.size)
+ interactivePause
+ numberOfTested += batchSize
// interactivePause
val currentCandidateExpr = maxCandidate.getExpr
- if (tryToSynthesizeBranch(currentCandidateExpr, failedExamples)) {
+ if (tryToSynthesizeBranch(currentCandidateExpr, examplesPartition)) {
//noBranchFoundIteration = 0
// after a branch is synthesized it makes sense to consider candidates that previously failed
@@ -272,7 +275,7 @@ class SynthesizerForRuleExamples(
}
if (variableRefinedBranch) {
- info("Variable refined, doing branch synthesis again")
+ reporter.info("Variable refined, doing branch synthesis again")
// get new snippets
snippets = synthesizeBranchExpressions
snippetsIterator = snippets.iterator
@@ -284,9 +287,9 @@ class SynthesizerForRuleExamples(
// reseting iterator needed because we may have some expressions that previously did not work
snippetsIterator = snippets.iterator
- info("Filtering based on precondition: " + holeFunDef.precondition.get)
+ reporter.info("Filtering based on precondition: " + And(initialPrecondition, accumulatingCondition))
fine("counterexamples before filter: " + gatheredExamples.size)
- exampleRunner.filter(holeFunDef.precondition.get)
+ exampleRunner.filter(And(initialPrecondition, accumulatingCondition))
gatheredExamples = exampleRunner.examples
fine("counterexamples after filter: " + gatheredExamples.size)
fine("counterexamples after filter: " + gatheredExamples.mkString("\n"))
@@ -297,7 +300,7 @@ class SynthesizerForRuleExamples(
}
def generateCounterexamples(program: Program, funDef: FunDef, number: Int): (Seq[Map[Identifier, Expr]], Expr) = {
- info("Generate counter examples with precondition " + funDef.precondition.getOrElse(BooleanLiteral(true)))
+ reporter.info("Generate counter examples with precondition " + funDef.precondition.getOrElse(BooleanLiteral(true)))
// save current precondition
var precondition = funDef.precondition.getOrElse(BooleanLiteral(true))
@@ -314,7 +317,7 @@ class SynthesizerForRuleExamples(
// check if solver could solved this instance
if (solved == false && !map.isEmpty) {
- info("Found counterexample: " + map)
+ reporter.info("Found counterexample: " + map)
// add current counterexample
maps :+= map
@@ -340,12 +343,12 @@ class SynthesizerForRuleExamples(
def getCurrentBuilder = new InitialEnvironmentBuilder(allDeclarations)
def synthesizeBranchExpressions = {
- info("Invoking synthesis for branch expressions")
+ reporter.info("Invoking synthesis for branch expressions")
synthInfo.profile(Generation) { inSynth.getExpressions(getCurrentBuilder).distinct }
}
def synthesizeBooleanExpressions = {
- info("Invoking synthesis for condition expressions")
+ reporter.info("Invoking synthesis for condition expressions")
synthInfo.start(Generation)
if (variableRefinedCondition) {
// store for later fetch (will memoize values)
@@ -364,8 +367,8 @@ class SynthesizerForRuleExamples(
}
def interactivePause = {
- System.out.println("Press Any Key To Continue...");
- new java.util.Scanner(System.in).nextLine();
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
}
def getNewExampleQueue = PriorityQueue[(Expr, Int)]()(
@@ -390,11 +393,20 @@ class SynthesizerForRuleExamples(
// interactivePause
// accumulate precondition for the remaining branch to synthesize
- accumulatingPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+ accumulatingCondition = BooleanLiteral(true)
// save initial precondition
- initialPrecondition = accumulatingPrecondition
+ initialPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+ val holeFunDefBody = holeFunDef.getBody
// accumulate the final expression of the hole
- accumulatingExpression = (finalExp: Expr) => finalExp
+ accumulatingExpression = (finalExp: Expr) => {
+ def replaceChoose(expr: Expr) = expr match {
+ case _: Choose => Some(finalExp)
+ case _ => None
+ }
+
+ import TreeOps._
+ matchToIfThenElse(searchAndReplace(replaceChoose)(holeFunDefBody))
+ }
//accumulatingExpressionMatch = accumulatingExpression
// each variable of super type can actually have a subtype
@@ -412,7 +424,8 @@ class SynthesizerForRuleExamples(
fine("Introduced examples: " + gatheredExamples.mkString("\t"))
}
- def tryToSynthesizeBranch(snippetTree: Expr, failedExamples: Seq[Example]): Boolean = {
+ def tryToSynthesizeBranch(snippetTree: Expr, examplesPartition: (Seq[Example], Seq[Example])): Boolean = {
+ val (succeededExamples, failedExamples) = examplesPartition
// replace hole in the body with the whole if-then-else structure, with current snippet tree
val oldBody = holeFunDef.getBody
val newBody = accumulatingExpression(snippetTree)
@@ -424,13 +437,13 @@ class SynthesizerForRuleExamples(
snippetTree.setType(hole.desiredType)
//holeFunDef.getBody.setType(hole.desiredType)
- info("Current candidate solution is:\n" + holeFunDef)
+ reporter.info("Current candidate solution is:\n" + holeFunDef)
if (failedExamples.isEmpty) {
// check if solver could solved this instance
fine("Analyzing program for funDef:" + holeFunDef)
val (result, map) = analyzeFunction(holeFunDef)
- info("Solver returned: " + result + " with CE " + map)
+ reporter.info("Solver returned: " + result + " with CE " + map)
if (result) {
// mark the branch found
@@ -456,12 +469,13 @@ class SynthesizerForRuleExamples(
holeFunDef.precondition = preconditionToRestore
// get counterexamples
- info("Going to generating counterexamples: " + holeFunDef)
- val (maps, precondition) = generateCounterexamples(program, holeFunDef, numberOfCounterExamplesToGenerate)
-
- // collect (add) counterexamples from leon
- if (collectCounterExamplesFromLeon)
- gatheredExamples ++= maps.map(Example(_))
+// info("Going to generating counterexamples: " + holeFunDef)
+// val (maps, precondition) = generateCounterexamples(program, holeFunDef, numberOfCounterExamplesToGenerate)
+//
+// // collect (add) counterexamples from leon
+// if (collectCounterExamplesFromLeon)
+// gatheredExamples ++= maps.map(Example(_))
+ val maps = Seq[Map[Identifier, Expr]]()
// will modify funDef body and precondition, restore it later
try {
@@ -486,11 +500,11 @@ class SynthesizerForRuleExamples(
})
) {
fine("boolean snippet is: " + innerSnippetTree)
- info("Trying: " + innerSnippetTree + " as a condition.")
+ reporter.info("Trying: " + innerSnippetTree + " as a condition.")
val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(
snippetTree, innerSnippetTree,
// counter examples represent those for which candidate fails
- (failedExamples.map(_.map) ++ maps)
+ (failedExamples.map(_.map) ++ maps), succeededExamples.map(_.map)
)
// if precondition found
@@ -522,22 +536,25 @@ class SynthesizerForRuleExamples(
}
}
- def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, counterExamples: Seq[Map[Identifier, Expr]]): (Boolean, Option[Expr]) = {
+ def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr,
+ counterExamples: Seq[Map[Identifier, Expr]], succExamples: Seq[Map[Identifier, Expr]]): (Boolean, Option[Expr]) = {
// new condition together with existing precondition
- val newCondition = And(Seq(accumulatingPrecondition, innerSnippetTree))
+ val newPrecondition = And(Seq(initialPrecondition, accumulatingCondition, innerSnippetTree))
+ val newPathCondition = And(Seq(problem.pc, accumulatingCondition, innerSnippetTree))
// new expression should not be false
// val notFalseEquivalence = Not(newCondition)
val isSatisfiable =
- checkSatisfiabilityNoMod(newCondition)
- fine("Is " + newCondition + " satisfiable: " + isSatisfiable)
+ checkSatisfiabilityNoMod(newPathCondition)
+ fine("Is " + newPathCondition + " satisfiable: " + isSatisfiable)
// continue if our expression is not contradictory
if (isSatisfiable) {
// check if synthesized boolean expression implies precondition (counterexamples)
- val implyCounterExamples = (false /: counterExamples) {
+ var hadRuntimeError = false
+ val implyCounterExamplesPre = (false /: counterExamples) {
case (false, exMapping) =>
- exampleRunner.evaluateToResult(newCondition, exMapping) match {
+ exampleRunner.evaluateToResult(newPrecondition, exMapping) match {
case EvaluationResults.Successful(BooleanLiteral(false)) => false
case r =>
@@ -545,7 +562,7 @@ class SynthesizerForRuleExamples(
val newFunId = FreshIdentifier("tempIntroducedFunction22")
val newFun = new FunDef(newFunId, holeFunDef.returnType, holeFunDef.args)
// newFun.precondition = Some(newCondition)
- newFun.precondition = holeFunDef.precondition
+ newFun.precondition = Some(initialPrecondition)
newFun.postcondition = holeFunDef.postcondition
def replaceFunDef(expr: Expr) = expr match {
@@ -560,6 +577,8 @@ class SynthesizerForRuleExamples(
IfExpr(innerSnippetTree, snippetTree, error)
import TreeOps._
+// println("ifInInnermostElse " + ifInInnermostElse)
+// println("acc expr before replace: " + accumulatingExpression(ifInInnermostElse))
val newBody = searchAndReplace(replaceFunDef)(accumulatingExpression(ifInInnermostElse))
newFun.body = Some(newBody)
@@ -569,8 +588,8 @@ class SynthesizerForRuleExamples(
val newCandidate =
Let(resFresh2, newBody,
- replace(Map(ResultVariable() -> LeonVariable(resFresh2)),
- matchToIfThenElse(newFun.getPostcondition)))
+ matchToIfThenElse(replace(Map(ResultVariable() -> LeonVariable(resFresh2)),
+ newFun.getPostcondition)))
finest("New fun for Error evaluation: " + newFun)
// println("new candidate: " + newBody)
@@ -588,9 +607,15 @@ class SynthesizerForRuleExamples(
// interactivePause
res match {
- case EvaluationResults.RuntimeError("Condition flow hit unknown path.") => false
+ case EvaluationResults.RuntimeError("Condition flow hit unknown path.") =>
+ hadRuntimeError = true
+ false
case EvaluationResults.Successful(BooleanLiteral(innerRes)) => !innerRes
- case _ => true
+ case _ =>
+ // TODO think about this
+ // I put condition into precondition so some examples will be violated?
+ println("new evalution got: " + res + " for " + newCandidate + " and " + exMapping + " newFun is " + newFun)
+ true
}
// fine("Evaluation result for " + newCondition + " on " + exMapping + " is " + r)
@@ -598,12 +623,76 @@ class SynthesizerForRuleExamples(
}
case _ => true
}
+
+ fine("implyCounterExamplesPre: " + implyCounterExamplesPre)
+
+ val implyCounterExamples = if (!implyCounterExamplesPre && hadRuntimeError) {
+ ! succExamples.exists( exMapping => {
+ // 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 = Some(initialPrecondition)
+ 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,
+ matchToIfThenElse(replace(Map(ResultVariable() -> LeonVariable(resFresh2)),
+ 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("for mapping: " + exMapping + "res is: " + res)
+// if (newCandidate.toString contains "tree.value < value")
+// interactivePause
+
+ interactivePause
+ res match {
+ case EvaluationResults.RuntimeError("Condition flow hit unknown path.") =>
+ false
+ case EvaluationResults.Successful(BooleanLiteral(innerRes)) => innerRes
+ case _ =>
+ println("new evalution got: " + res + " for " + newCandidate + " and " + exMapping)
+ false
+ }
+ })
+ } else
+ implyCounterExamplesPre
+
+
fine("implyCounterExamples: " + implyCounterExamples)
// interactivePause
if (!implyCounterExamples) {
// if expression implies counterexamples add it to the precondition and try to validate program
- holeFunDef.precondition = Some(newCondition)
+ holeFunDef.precondition = Some(newPathCondition)
// do analysis
val (valid, map) = analyzeFunction(holeFunDef)
@@ -623,19 +712,19 @@ class SynthesizerForRuleExamples(
})
accumulatingExpression = newAccumulatingExpression
- val currentBranchCondition = And(Seq(accumulatingPrecondition, innerSnippetTree))
+ val currentBranchCondition = And(Seq(accumulatingCondition, innerSnippetTree))
// update accumulating precondition
fine("updating accumulatingPrecondition")
- accumulatingPrecondition = And(Seq(accumulatingPrecondition, Not(innerSnippetTree)))
+ accumulatingCondition = And(Seq(accumulatingCondition, Not(innerSnippetTree)))
fine("updating hole fun precondition and body (to be hole)")
// set to set new precondition
- val preconditionToRestore = Some(accumulatingPrecondition)
+ val preconditionToRestore = Some(accumulatingCondition)
val variableRefinementResult = variableRefiner.checkRefinements(innerSnippetTree, currentBranchCondition, allDeclarations)
if (variableRefinementResult._1) {
- info("Variable is refined.")
+ reporter.info("Variable is refined.")
allDeclarations = variableRefinementResult._2
// the reason for two flags is for easier management of re-syntheses only if needed
@@ -645,13 +734,13 @@ class SynthesizerForRuleExamples(
// found a boolean snippet, break
(true, preconditionToRestore)
- } else {
+ } else {
// collect (add) counterexamples from leon
if (collectCounterExamplesFromLeon && !map.isEmpty)
gatheredExamples ++= (map :: Nil).map(Example(_))
// reset funDef and continue with next boolean snippet
- val preconditionToRestore = Some(accumulatingPrecondition)
+ val preconditionToRestore = Some(accumulatingCondition)
(false, preconditionToRestore)
}
} else {
diff --git a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
index 269650e6f7c7a1b3825348c119d885adb8a40cfb..e6560d3beaf9900dc64e288e97d887eacae7e384 100644
--- a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
+++ b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
@@ -25,6 +25,7 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
val evaluationContext = ctx.copy(reporter = new SilentReporter)
+ fine("building codegen evaluator with program:\n" + program)
lazy val _evaluator = new CodeGenEvaluator(evaluationContext, program, params)
override def getEvaluator = _evaluator
@@ -38,6 +39,7 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
)
def compile(expr: Expr, ids: Seq[Identifier]) = {
+ finest("Compiling expr: " + expr + " for ids: " + ids)
// this get is dubious
StopwatchCollections.get("Compilation").newStopwatch profile getEvaluator.compile(expr, ids).get
}
@@ -47,7 +49,7 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
override def evaluate(candidateInd: Int, exampleInd: Int) = {
val closure = candidateClosures(candidateInd)
- finest("Index evaluate candidate [%d]%s, for [%d]%s.".format(
+ finer("Index evaluate candidate [%d]%s, for [%d]%s.".format(
candidateInd, candidates(candidateInd).prepareExpression, exampleInd, examples(exampleInd)
))
@@ -86,15 +88,15 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
try {
evalClosure(args) match {
case Successful(BooleanLiteral(true)) =>
- finest("EvaluationSuccessful(true) for " + args)
+ fine("EvaluationSuccessful(true) for " + args)
true
case m =>
- finest("Eval failed: " + m)
+ fine("Eval failed: " + m)
false
}
} catch {
case e: StackOverflowError =>
- finest("Eval failed: " + e)
+ fine("Eval failed: " + e)
false
}
}
diff --git a/src/main/scala/lesynth/examples/InputExamples.scala b/src/main/scala/lesynth/examples/InputExamples.scala
index 71a186e420d4c2e4e8feaf3a4de9c6032d27c937..106442bbc164993164b0a1dcf12a71a1b30e1c0d 100755
--- a/src/main/scala/lesynth/examples/InputExamples.scala
+++ b/src/main/scala/lesynth/examples/InputExamples.scala
@@ -5,40 +5,44 @@ import leon.purescala.TypeTrees._
import leon.purescala.Trees._
import leon.purescala.TreeOps
import leon.purescala.Common.Identifier
+import leon.purescala.Definitions.Program
import leon.evaluators.Evaluator
import leon.synthesis.Problem
-import leon.purescala.DataGen
+import leon.LeonContext
import insynth.leon.loader.{ HoleExtractor, LeonLoader }
+import leon.datagen._
object InputExamples {
- import DataGen._
val rnd = new scala.util.Random(System.currentTimeMillis)
val MAX_INT = 1000
- def getDataGenInputExamples(evaluator: Evaluator, p: Problem,
+ def getDataGenInputExamples(ctx: LeonContext, program: Program, evaluator: Evaluator, p: Problem,
numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]]) = {
- val models = findModels(p.pc, evaluator, numOfModels, numOfTries,
- forcedFreeVars = _forcedFreeVars)
- models.toList
+ val ins = _forcedFreeVars.getOrElse(TreeOps.variablesOf(p.pc).toSeq)
+
+ val models = new NaiveDataGen(ctx, program, evaluator).generateFor(ins, p.pc, numOfModels, numOfTries)
+
+ models.toList.map(m => (ins zip m).toMap)
}
- def getDataGenInputExamplesRandomIntegers(evaluator: Evaluator, p: Problem,
+ def getDataGenInputExamplesRandomIntegers(ctx: LeonContext, program: Program, evaluator: Evaluator, p: Problem,
numOfModels: Int, numOfTries: Int, _forcedFreeVars: Option[Seq[Identifier]],
bound: Int = MAX_INT) = {
import TreeOps._
- val models = findModels(p.pc, evaluator, numOfModels, numOfTries,
- forcedFreeVars = _forcedFreeVars)
+ val ins = _forcedFreeVars.getOrElse(TreeOps.variablesOf(p.pc).toSeq)
+
+ val models = new NaiveDataGen(ctx, program, evaluator).generateFor(ins, p.pc, numOfModels, numOfTries)
def foundInteger(x: Expr) = x match {
case _:IntLiteral => Some(IntLiteral(rnd.nextInt(bound)))
case _ => None
}
- models.toList.map( innerMap =>
+ models.toList.map(m => (ins zip m).toMap).map( innerMap =>
innerMap.map( innerEl => innerEl match {
case (id, expr) => (id, searchAndReplace(foundInteger)(expr))
})
@@ -176,4 +180,4 @@ object InputExamples {
// yield Map(argumentIds(0) -> l1)
//
// }
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/ranking/Ranker.scala b/src/main/scala/lesynth/ranking/Ranker.scala
index 0137c6a98d5bb07714233c907d11c64a60ef469e..ebf6d42970ece8a984c38299c29274a1c33175a4 100644
--- a/src/main/scala/lesynth/ranking/Ranker.scala
+++ b/src/main/scala/lesynth/ranking/Ranker.scala
@@ -1,7 +1,7 @@
package lesynth
package ranking
-import util.control.Breaks._
+import scala.util.control.Breaks._
import scala.collection._
import leon.purescala.Trees.{ Variable => LeonVariable, _ }
@@ -83,6 +83,14 @@ class Ranker(candidates: IndexedSeq[Candidate], evaluation: Evaluation, checkTim
(candidates(rankings(0)), rankings(0))
}
+ def fullyEvaluate(ind: Int) = {
+ val tuple = tuples(ind)
+ for (_ <- 0 until (tuple._2 - tuple._1))
+ evaluate(ind)
+
+ tuples(ind)
+ }
+
// def getVerifiedMax = {
// val results = (for (candidate <- 0 until candidates.size)
// yield (candidate,
diff --git a/src/main/scala/lesynth/refinement/Filter.scala b/src/main/scala/lesynth/refinement/Filter.scala
index a041a49dc3f9c0924705f2a0b53493059a365f8b..90c6f25dea44c56f3e1127af488fab65e421f3cf 100755
--- a/src/main/scala/lesynth/refinement/Filter.scala
+++ b/src/main/scala/lesynth/refinement/Filter.scala
@@ -161,6 +161,8 @@ class Filter(program: Program, holeFunDef: FunDef, refiner: VariableRefiner) ext
// if we check instance of an constructor we know that it is a constant
// case CaseClassInstanceOf(_, _: CaseClass) =>
// true
+ case CaseClassInstanceOf(classDef, _: FunctionInvocation) =>
+ true
case CaseClassInstanceOf(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 910e1fa728aaefdc8440a26252feece0f5daaa15..a980e6fd98a215a6d5b7a2f960a0cd691d62ddb0 100755
--- a/src/main/scala/lesynth/refinement/VariableRefiner.scala
+++ b/src/main/scala/lesynth/refinement/VariableRefiner.scala
@@ -22,7 +22,7 @@ class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variabl
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
+ protected var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = MutableMap.empty
for (varDec <- variableDeclarations) {
varDec match {
case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, Variable(id))) =>
@@ -33,7 +33,7 @@ class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variabl
def getPossibleTypes(id: Identifier) = variableRefinements(id)
- def checkRefinements(expr: Expr, allDeclarations: List[Declaration]) =
+ def checkRefinements(expr: Expr, condition: Expr, allDeclarations: List[Declaration]) =
// check for refinements
getIdAndClassDef(expr) match {
case Some(refinementPair @ (id, classType)) if variableRefinements(id).size > 1 =>
@@ -51,25 +51,7 @@ class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variabl
// update declarations
val newDeclarations =
- for (dec <- allDeclarations)
- yield dec match {
- case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, Variable(`id`))) =>
- ((
- newType.classDef match {
- case newTypeCaseClassDef@CaseClassDef(id, parent, fields) =>
- for (field <- fields)
- yield LeonDeclaration(
- ImmediateExpression( "Field(" + newTypeCaseClassDef + "." + field.id + ")",
- CaseClassSelector(newTypeCaseClassDef, imex.expr, field.id) ),
- TypeTransformer(field.id.getType), field.id.getType
- )
- case _ =>
- Seq.empty
- }
- ): Seq[Declaration]) :+ LeonDeclaration(imex, TypeTransformer(newType), newType)
- case _ =>
- Seq(dec)
- }
+ refinedDeclarations(id, newType, allDeclarations)
(true, newDeclarations.flatten)
} else {
@@ -88,4 +70,26 @@ class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variabl
None
}
+ def refinedDeclarations(id: Identifier, newType: ClassType, allDeclarations: List[Declaration]) =
+ for (dec <- allDeclarations)
+ yield dec match {
+ case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, Variable(`id`))) =>
+ ((
+ newType.classDef match {
+ case newTypeCaseClassDef@CaseClassDef(_, parent, fields) =>
+ fine("matched case class def for refinement " + newTypeCaseClassDef)
+ for (field <- fields)
+ yield LeonDeclaration(
+ ImmediateExpression(id.name + "." + field.id.name,
+ CaseClassSelector(newTypeCaseClassDef, imex.expr, field.id) ),
+ TypeTransformer(field.id.getType), field.id.getType
+ )
+ case _ =>
+ Seq.empty
+ }
+ ): Seq[Declaration]) :+ LeonDeclaration(imex, TypeTransformer(newType), newType)
+ case _ =>
+ Seq(dec)
+ }
+
}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala b/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
new file mode 100755
index 0000000000000000000000000000000000000000..0ffe1aa469cb50e8ac917752801ffccad66ef220
--- /dev/null
+++ b/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
@@ -0,0 +1,128 @@
+package lesynth
+package refinement
+
+import scala.collection.mutable.{Map => MutableMap}
+import scala.collection.mutable.{Set => MutableSet}
+
+import leon._
+import leon.purescala.Extractors._
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.purescala.Definitions._
+import leon.solvers._
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.synthesis.Problem
+
+import insynth.interfaces._
+import insynth.leon.loader._
+import insynth.leon._
+
+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 VariableSolverRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[LeonDeclaration],
+ classMap: Map[Identifier, ClassType], solver: Solver, reporter: Reporter = new SilentReporter)
+ extends VariableRefiner(directSubclassMap, variableDeclarations, classMap, reporter) with HasLogger {
+
+ override def checkRefinements(expr: Expr, condition: Expr, allDeclarations: List[Declaration]) = {
+ val superResult = super.checkRefinements(expr, condition, allDeclarations)
+ if (superResult._1 == false) {
+ val variables = allIdentifiers(expr)
+ if (variables.size == 1) {
+ val variable = variables.head
+ variable match {
+ case oldId@IsTyped(id, AbstractClassType(cd)) if variableRefinements(id).size > 1 =>
+
+ assert(variableRefinements(id).map(_.classDef) subsetOf cd.knownDescendents.toSet)
+ //val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
+ val optCases = for (dcd <- variableRefinements(id).map(_.classDef)) yield dcd match {
+ case ccd : CaseClassDef =>
+ fine("testing variable " + id + " with condition " + condition)
+ val toSat = And(condition, CaseClassInstanceOf(ccd, Variable(id)))
+
+ fine("checking satisfiability of: " + toSat)
+ solver.solveSAT(toSat) match {
+ case (Some(false), _) =>
+ fine("variable cannot be of type " + ccd)
+ None
+ case _ =>
+ fine("variable can be of type " + ccd)
+ Some(ccd)
+ }
+ case _ =>
+ None
+ }
+
+ val cases = optCases.flatten
+ variableRefinements(id) = variableRefinements(id) & cases.map(CaseClassType(_)).toSet
+ assert(variableRefinements(id).size == cases.size)
+
+ if (cases.size == 1) {
+ // update declarations
+ val newDeclarations =
+ refinedDeclarations(id, CaseClassType(cases.head), allDeclarations)
+
+ (true, newDeclarations.flatten)
+ } else {
+ fine("cases.size != 1")
+ superResult
+ }
+
+ case id => {
+ fine("no id found for refinement that has potential refinements > 1")
+ superResult
+ }
+ }
+ } else {
+ fine("more than one variable")
+ superResult
+ }
+ }
+ else superResult
+ }
+
+ def refineProblem(p: Problem, solver: Solver) = {
+
+ val newAs = p.as.map {
+ case oldId@IsTyped(id, AbstractClassType(cd)) =>
+
+ val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
+ case ccd : CaseClassDef =>
+ val toSat = And(p.pc, CaseClassInstanceOf(ccd, Variable(id)))
+
+ val isImplied = solver.solveSAT(toSat) match {
+ case (Some(false), _) => true
+ case _ => false
+ }
+
+ println(isImplied)
+
+ if (!isImplied) {
+ Some(ccd)
+ } else {
+ None
+ }
+ case _ =>
+ None
+ }
+
+ val cases = optCases.flatten
+
+ println(id)
+ println(cases)
+
+ if (cases.size == 1) {
+// id.setType(CaseClassType(cases.head))
+ FreshIdentifier(oldId.name).setType(CaseClassType(cases.head))
+ } else oldId
+
+ case id => id
+ }
+
+ p.copy(as = newAs)
+ }
+
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
index 6f7567fd6e4bdf9c4862e4327c0c28962eff170e..5feec355e246589a57fc08e5d39f6fb5a8d55816 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
@@ -1,80 +1,80 @@
-package lesynth
-package rules
-
-import leon.purescala.Trees._
-import leon.purescala.Common._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps._
-import leon.purescala.Extractors._
-import leon.purescala.Definitions._
-import leon.synthesis._
-import leon.solvers.{ 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] = {
-
- 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)
-
- 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("Rule is not applicable for more than one output variable.")
- Nil
- }
-
- }
-}
+//package lesynth
+//package rules
+//
+//import leon.purescala.Trees._
+//import leon.purescala.Common._
+//import leon.purescala.TypeTrees._
+//import leon.purescala.TreeOps._
+//import leon.purescala.Extractors._
+//import leon.purescala.Definitions._
+//import leon.synthesis._
+//import leon.solvers.{ 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] = {
+//
+// 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)
+//
+// 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("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 53f5576114f36b789e6ea3c920eca7b195e0a9db..05a6a4cd10397e9770b011936718dd7d23076187 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -16,7 +16,7 @@ import lesynth.evaluation._
import leon.StopwatchCollections
-case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abduction synthesis (two phase).") {
+case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abduction synthesis (two phase).") with TopLevelRule {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.xs match {
@@ -33,7 +33,6 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
// temporary hack, should not mutate FunDef
val oldPostcondition = holeFunDef.postcondition
- val oldPrecondition = holeFunDef.precondition
try {
val freshResID = FreshIdentifier("result").setType(holeFunDef.returnType)
@@ -42,20 +41,18 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
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)
+ //getDataGenInputExamples(sctx.context, sctx.program, codeGenEval, p,
+ // 100, 6000, Some(p.as)) ++
+ getDataGenInputExamplesRandomIntegers(sctx.context, sctx.program, codeGenEval, p,
+ 100, 6000, Some(p.as)
// bound the random geenerator
- ,5
- )
+ ,10)
}
- val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 1000)
+ val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 5000)
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,
@@ -71,7 +68,10 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
case fr@FullReport(resFunDef, _) =>
println(fr.summaryString)
println("Compilation time: " + StopwatchCollections.get("Compilation").getMillis)
- RuleSuccess(Solution(resFunDef.getPrecondition, Set.empty, resFunDef.body.get))
+ RuleSuccess(
+ Solution(BooleanLiteral(true), Set.empty, Tuple(Seq(resFunDef.body.get)),
+ isTrusted = !synthesizer.verifier.isTimeoutUsed)
+ )
}
} catch {
case e: Throwable =>
@@ -80,13 +80,12 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
RuleApplicationImpossible
} finally {
holeFunDef.postcondition = oldPostcondition
- holeFunDef.precondition = oldPrecondition
}
}
}
})
case _ =>
- throw new RuntimeException("Rule is not applicable for more than one output variable.")
+// throw new RuntimeException("Rule is not applicable for more than one output variable.")
Nil
}
diff --git a/src/main/scala/lesynth/verification/AbstractVerifier.scala b/src/main/scala/lesynth/verification/AbstractVerifier.scala
index 5d14e85b1161ea67cfad03f6ea94ae3c650c0b8b..18e4875d57f7b80ecbd4c303d82f61caf26c5878 100644
--- a/src/main/scala/lesynth/verification/AbstractVerifier.scala
+++ b/src/main/scala/lesynth/verification/AbstractVerifier.scala
@@ -19,6 +19,7 @@ abstract class AbstractVerifier(solver: IncrementalSolver, p: Problem,
def analyzeFunction(funDef: FunDef) = {
synthInfo.start(Verification)
+ fine("Analyzing function: " + funDef)
// create an expression to verify
val theExpr = generateInductiveVerificationCondition(funDef, funDef.getBody)
@@ -84,18 +85,28 @@ abstract class AbstractVerifier(solver: IncrementalSolver, p: Problem,
val bodyAndPost =
Let(
resFresh, newBody,
- replace(Map(ResultVariable() -> resFresh.toVariable), matchToIfThenElse(p.pc))
+ replace(Map(ResultVariable() -> resFresh.toVariable), matchToIfThenElse(funDef.getPostcondition))
)
val precondition = if( isThereARecursiveCall ) {
- And( p.phi :: replacements.map( r => replace(r.getMapping, p.pc)) )
+ And( funDef.getPrecondition :: replacements.map( r => replace(r.getMapping, funDef.getPostcondition)) )
} else
- p.phi
+ funDef.getPrecondition
+// val bodyAndPost =
+// Let(
+// resFresh, newBody,
+// replace(Map(p.xs.head.toVariable -> resFresh.toVariable), matchToIfThenElse(p.phi))
+// )
+//
+// val precondition = if( isThereARecursiveCall ) {
+// And( p.pc :: replacements.map( r => replace(r.getMapping, p.phi)) )
+// } else
+// p.pc
val withPrec =
Implies(matchToIfThenElse(precondition), bodyAndPost)
- fine("Generated verification condition: " + withPrec)
+ info("Generated verification condition: " + withPrec)
withPrec
}
diff --git a/src/main/scala/lesynth/verification/RelaxedVerifier.scala b/src/main/scala/lesynth/verification/RelaxedVerifier.scala
index a1ce8db96e132c80cbab17d7f7cdab76d1be8422..07393f990a123d03fb6345eb99b653b9153cc5d7 100644
--- a/src/main/scala/lesynth/verification/RelaxedVerifier.scala
+++ b/src/main/scala/lesynth/verification/RelaxedVerifier.scala
@@ -13,8 +13,13 @@ import insynth.util.logging._
class RelaxedVerifier(solver: IncrementalSolver, p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
extends AbstractVerifier(solver, p, synthInfo) with HasLogger {
+
+ var _isTimeoutUsed = false
+
+ def isTimeoutUsed = _isTimeoutUsed
override def checkValidity(expression: Expr) = {
+ fine("Checking validity - assertCnstr: " + Not(expression))
solver.assertCnstr(Not(expression))
val solverCheckResult = solver.check
fine("Solver said " + solverCheckResult + " for " + expression)
@@ -24,6 +29,7 @@ class RelaxedVerifier(solver: IncrementalSolver, p: Problem, synthInfo: Synthesi
case Some(false) =>
true
case None =>
+ _isTimeoutUsed = true
warning("Interpreting None (timeout) as evidence for validity.")
true
}
@@ -31,6 +37,7 @@ class RelaxedVerifier(solver: IncrementalSolver, p: Problem, synthInfo: Synthesi
override def checkValidityNoMod(expression: Expr) = {
solver.push
+ fine("Checking validityNoMod - assertCnstr: " + Not(expression))
solver.assertCnstr(Not(expression))
val solverCheckResult = solver.check
fine("Solver said " + solverCheckResult + " for " + expression)
@@ -42,6 +49,7 @@ class RelaxedVerifier(solver: IncrementalSolver, p: Problem, synthInfo: Synthesi
case Some(false) =>
true
case None =>
+ _isTimeoutUsed = true
warning("Interpreting None (timeout) as evidence for validity.")
true
}
@@ -49,6 +57,7 @@ class RelaxedVerifier(solver: IncrementalSolver, p: Problem, synthInfo: Synthesi
override def checkSatisfiabilityNoMod(expression: Expr) = {
solver.push
+ fine("Checking checkSatisfiabilityNoMod - assertCnstr: " + expression)
solver.assertCnstr(expression)
val solverCheckResult = solver.check
fine("Solver said " + solverCheckResult + " for " + expression)
diff --git a/src/test/scala/insynth/InSynthTempTest.scala b/src/test/scala/insynth/InSynthTempTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..61f1d467ec5c9c63d6309b14b696d88f00889b65
--- /dev/null
+++ b/src/test/scala/insynth/InSynthTempTest.scala
@@ -0,0 +1,673 @@
+package insynth
+
+import insynth.leon._
+import insynth.leon.loader._
+import insynth.engine._
+
+import insynth.reconstruction.{ intermediate => int }
+import insynth.reconstruction.{ stream => lambda }
+import insynth.reconstruction.shortcut._
+import insynth.reconstruction.stream.{ OrderedStreamFactory }
+import insynth.reconstruction.codegen._
+import insynth.reconstruction.Output
+
+import _root_.leon.purescala.Definitions._
+import _root_.leon.purescala.Common._
+import _root_.leon.purescala.TypeTrees._
+import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
+
+import lesynth.refinement._
+import lesynth.examples._
+import lesynth.evaluation.CodeGenEvaluationStrategy
+import lesynth.ranking.Candidate
+
+import org.junit.{ Test, Ignore }
+import org.junit.Assert._
+
+import insynth.util.format._
+import insynth.util._
+import lesynth.util._
+
+import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
+
+// TODO test abstractions (vals)
+class InSynthTempTest {
+
+ import CommonDeclarations._
+ import CommonProofTrees._
+ import CommonLambda._
+ import DeclarationFactory._
+
+ import Scaffold._
+ import TestConfig._
+
+ import ProofTreeOperations.StringNode
+
+ val transformer = new Transformer2(new OrderedStreamFactory)
+ val codegen = new CodeGenerator
+
+ val maxElToOutput = 20
+
+ import lambda.Node._
+
+ def assertWeight(lambdaNode: lambda.Node, weight: Float) =
+ assertEquals(size(lambdaNode), weight, 0f)
+
+ def assertWeight(expected: Int, weight: Float) =
+ assertEquals(expected.toFloat, weight, 0f)
+
+ def assertWeight(pair: (lambda.Node, Float)) =
+ assertEquals("Node " + pair._1, size(pair._1), pair._2, 0f)
+
+ def assertTake(stream: Stream[(lambda.Node, Float)], num: Int) = {
+ val result = stream take num
+ val message = "Part of the resulting stream: " + result.take(maxElToOutput).mkString("\n")
+
+ for (ind <- 0 until result.size)
+ assertWeight(result(ind))
+ for (ind <- 0 until result.size - 1)
+ assertTrue("Weight are not in non-decreasing order.\n" + "At position " + ind + "\n" + message, stream(ind)._2 <= stream(ind + 1)._2)
+ result
+ }
+
+ def interactivePause = {
+ System.out.println("Press Any Key To Continue...");
+ new java.util.Scanner(System.in).nextLine();
+ }
+
+ @Ignore
+ def testAddresses: Unit = {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ assertEquals(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 InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ val solver = inSynth.solver
+ val solution = solver.getProofTree
+
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("AddressBook", Set(
+ StringNode("[Cons=>List]", Set(StringNode("Cons")))
+ ,
+ StringNode("pers", Set(StringNode("makeAddressBook")))
+ ))
+ ))
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("addToPers", Set(
+ StringNode("makeAddressBook", Set(
+// StringNode("l.tail", Set())
+ ))
+ ,
+ StringNode("Address", Set( ))
+ ))
+ ))
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("addToBusiness", Set(
+ StringNode("makeAddressBook", Set(
+// StringNode("l.tail", Set())
+ ))
+ ,
+ StringNode("Address", Set( ))
+ ))
+ ))
+
+ val extractorResults = assertTake(transformer(solution.getNodes.head), 1000)
+
+// val duplicityMap = (Map[Expr, Set[(lambda.Node, Float)]]() /: extractorResults) {
+// (resMap, pair) =>
+// val snippet = codegen(pair._1)
+// resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
+// }
+
+// val resTemp = transformer(solution.getNodes.head).take(100)
+//
+// println(resTemp.head)
+// val it = resTemp.iterator.buffered
+// println(it.head)
+// println(it.hasNext)
+// println(it.head)
+// println(it.hasNext)
+//
+// for (output <- extractorResults) {
+// print("%20s %5f" format (output._1, output._2))
+//
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
+// }
+// println("\nExtracted: " + extractorResults.size)
+
+ val message =
+ (for (output <- extractorResults)
+ yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
+ assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
+ assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
+//
+// println("Duplicity map size " + duplicityMap.size)
+// for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
+// println("Key: " + key)
+// println("Values: " + value.mkString("\n"))
+// }
+ }
+ }
+
+ @Ignore
+ def testAddressesWithRefinement: Unit = {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ assertEquals(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 InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+ val listVal = funDef.args.head.toVariable
+
+ val variableRefiner =
+ new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap)
+
+ val (refined, newDeclarations) =
+ variableRefiner.checkRefinements(
+ CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+ assert(refined)
+ assert(allDeclarations.size + 2 == newDeclarations.size)
+
+ val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
+ newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
+ println(declsMessage)
+
+ val builder = new InitialEnvironmentBuilder(newDeclarations)
+
+ val solver = inSynth.solver
+ val solution = solver.getProofTree(builder)
+
+ val extractorResults = assertTake(transformer(solution.getNodes.head), 1000)
+
+// val duplicityMap = (Map[Expr, Set[(lambda.Node, Float)]]() /: extractorResults) {
+// (resMap, pair) =>
+// val snippet = codegen(pair._1)
+// resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
+// }
+
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("AddressBook", Set(
+ StringNode("[Cons=>List]", Set(StringNode("Cons")))
+ ,
+ StringNode("pers", Set(StringNode("makeAddressBook")))
+ ))
+ ))
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("addToPers", Set(
+ StringNode("makeAddressBook", Set(
+ StringNode("l.tail", Set())
+ ))
+ ,
+ StringNode("a", Set( ))
+ ))
+ ))
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("addToBusiness", Set(
+ StringNode("makeAddressBook", Set(
+ StringNode("l.tail", Set())
+ ))
+ ,
+ StringNode("a", Set( ))
+ ))
+ ))
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("addToBusiness", Set(
+ StringNode("makeAddressBook", Set(
+ StringNode("l.tail", Set())
+ ))
+ ,
+ StringNode("l.a", Set( ))
+ ))
+ ))
+// val resTemp = transformer(solution.getNodes.head).take(100)
+//
+// println(resTemp.head)
+// val it = resTemp.iterator.buffered
+// println(it.head)
+// println(it.hasNext)
+// println(it.head)
+// println(it.hasNext)
+//
+// for (output <- extractorResults) {
+// print("%20s %5f" format (output._1, output._2))
+//
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
+// }
+// println("\nExtracted: " + resTemp.size)
+// println("\nExtracted: " + extractorResults.size)
+
+ val message =
+ (for (output <- extractorResults)
+ yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
+ assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
+ assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
+//
+// println("Duplicity map size " + duplicityMap.size)
+// for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
+// println("Key: " + key)
+// println("Values: " + value.mkString("\n"))
+// }
+ }
+ }
+
+ @Ignore
+ def testAddressesWithRefinementCodeGen: Unit = {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ assertEquals(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 InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+ val listVal = funDef.args.head.toVariable
+
+ val variableRefiner =
+ new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap)
+
+ val (refined, newDeclarations) =
+ variableRefiner.checkRefinements(
+ CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+ assert(refined)
+ assert(allDeclarations.size + 2 == newDeclarations.size)
+
+ val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
+ newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
+ println(declsMessage)
+
+ val builder = new InitialEnvironmentBuilder(newDeclarations)
+
+ val solver = inSynth.solver
+ val solution = solver.getProofTree(builder)
+
+ val extractorResults = assertTake(transformer(solution.getNodes.head), 20000)
+
+ var ind = 1
+ for ((output, snippet) <- extractorResults zip (extractorResults map { p => codegen(p._1) })) {
+ print("%20s %20s\n".format(snippet, output._1.toString))
+ ind +=1
+
+ if ((ind % 1000) == 0) {
+ interactivePause
+ }
+ }
+
+ val message =
+ (for (output <- extractorResults)
+ yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
+ assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
+ assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
+//
+// println("Duplicity map size " + duplicityMap.size)
+// for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
+// println("Key: " + key)
+// println("Values: " + value.mkString("\n"))
+// }
+ }
+ }
+
+ @Ignore
+ def testAddressesWithRefinementTime: Unit = {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ assertEquals(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 InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+ val listVal = funDef.args.head.toVariable
+
+ val variableRefiner =
+ new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap)
+
+ val (refined, newDeclarations) =
+ variableRefiner.checkRefinements(
+ CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+ assert(refined)
+ assert(allDeclarations.size + 2 == newDeclarations.size)
+
+ val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
+ newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
+
+ val builder = new InitialEnvironmentBuilder(newDeclarations)
+
+ val solver = inSynth.solver
+ val solution = solver.getProofTree(builder)
+
+ val startTime = System.currentTimeMillis
+ val extractorResults = assertTake(transformer(solution.getNodes.head), 5000)
+ println("Time for extracting 5000 solutions: " + (System.currentTimeMillis - startTime))
+
+// val duplicityMap = (Map[Expr, Set[(lambda.Node, Float)]]() /: extractorResults) {
+// (resMap, pair) =>
+// val snippet = codegen(pair._1)
+// resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
+// }
+
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("AddressBook", Set(
+ StringNode("[Cons=>List]", Set(StringNode("Cons")))
+ ,
+ StringNode("pers", Set(StringNode("makeAddressBook")))
+ ))
+ ))
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("addToPers", Set(
+ StringNode("makeAddressBook", Set(
+ StringNode("l.tail", Set())
+ ))
+ ,
+ StringNode("a", Set( ))
+ ))
+ ))
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("addToBusiness", Set(
+ StringNode("makeAddressBook", Set(
+ StringNode("l.tail", Set())
+ ))
+ ,
+ StringNode("a", Set( ))
+ ))
+ ))
+ assertTrue(
+ ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+ ProofTreeOperations.checkInhabitants(solution,
+ StringNode("addToBusiness", Set(
+ StringNode("makeAddressBook", Set(
+ StringNode("l.tail", Set())
+ ))
+ ,
+ StringNode("l.a", Set( ))
+ ))
+ ))
+// val resTemp = transformer(solution.getNodes.head).take(100)
+//
+// println(resTemp.head)
+// val it = resTemp.iterator.buffered
+// println(it.head)
+// println(it.hasNext)
+// println(it.head)
+// println(it.hasNext)
+//
+// for (output <- extractorResults) {
+// print("%20s %5f" format (output._1, output._2))
+//
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
+// }
+// println("\nExtracted: " + resTemp.size)
+// println("\nExtracted: " + extractorResults.size)
+
+ val message =
+ (for (output <- extractorResults)
+ yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
+ assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
+ assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
+//
+// println("Duplicity map size " + duplicityMap.size)
+// for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
+// println("Key: " + key)
+// println("Values: " + value.mkString("\n"))
+// }
+ }
+ }
+
+ @Ignore
+ def testListConcatWithRefinementCodeGen: Unit = {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthSynthesisDir + "List/ListConcat.scala")) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ assertEquals(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 InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+ val listVal = funDef.args.head.toVariable
+
+ val variableRefiner =
+ new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap)
+
+ val (refined, newDeclarations) =
+ variableRefiner.checkRefinements(
+ CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+ assert(refined)
+ assert(allDeclarations.size + 2 == newDeclarations.size)
+
+ val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
+ newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l1.tail"))
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l1.head"))
+ println(declsMessage)
+
+ val builder = new InitialEnvironmentBuilder(newDeclarations)
+
+ val solver = inSynth.solver
+ val solution = solver.getProofTree(builder)
+
+ val extractorResults = assertTake(transformer(solution.getNodes.head), 1000)
+
+ var ind = 1
+ for ((output, snippet) <- extractorResults zip (extractorResults map { p => codegen(p._1) })) {
+ print("%20s %20s\n".format(snippet, output._1.toString))
+ ind +=1
+
+ if ((ind % 1000) == 0) {
+ interactivePause
+ }
+ }
+
+// val message =
+// (for (output <- extractorResults)
+// yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
+// assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
+// assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
+//
+// println("Duplicity map size " + duplicityMap.size)
+// for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
+// println("Key: " + key)
+// println("Values: " + value.mkString("\n"))
+// }
+ }
+ }
+
+ @Test
+ def testAddressesWithRefinementBoolean: Unit = {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+ val program = sctx.program
+ val arguments = funDef.args.map(_.id)
+
+ assertEquals(1, problem.xs.size)
+ val resultVariable = problem.xs.head
+ val hole = Hole(BooleanType)
+
+ val loader = new LeonLoader(program, hole, problem.as, false)
+ val inSynth = new InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+ val listVal = funDef.args.head.toVariable
+
+ val variableRefiner =
+ new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap)
+
+ val (refined, newDeclarations) =
+ variableRefiner.checkRefinements(
+ CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+ assert(refined)
+ assert(allDeclarations.size + 2 == newDeclarations.size)
+
+ val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
+ newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
+ assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
+ println(declsMessage)
+
+ val builder = new InitialEnvironmentBuilder(newDeclarations)
+
+ val solver = inSynth.solver
+ val solution = solver.getProofTree(builder)
+
+ val extractorResults = assertTake(transformer(solution.getNodes.head), 100)
+
+// val duplicityMap = (Map[Expr, Set[(lambda.Node, Float)]]() /: extractorResults) {
+// (resMap, pair) =>
+// val snippet = codegen(pair._1)
+// resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
+// }
+
+// assertTrue(
+// ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+// ProofTreeOperations.checkInhabitants(solution,
+// StringNode("AddressBook", Set(
+// StringNode("[Cons=>List]", Set(StringNode("Cons")))
+// ,
+// StringNode("pers", Set(StringNode("makeAddressBook")))
+// ))
+// ))
+// assertTrue(
+// ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+// ProofTreeOperations.checkInhabitants(solution,
+// StringNode("addToPers", Set(
+// StringNode("makeAddressBook", Set(
+// StringNode("l.tail", Set())
+// ))
+// ,
+// StringNode("a", Set( ))
+// ))
+// ))
+// assertTrue(
+// ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+// ProofTreeOperations.checkInhabitants(solution,
+// StringNode("addToBusiness", Set(
+// StringNode("makeAddressBook", Set(
+// StringNode("l.tail", Set())
+// ))
+// ,
+// StringNode("a", Set( ))
+// ))
+// ))
+// assertTrue(
+// ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+// ProofTreeOperations.checkInhabitants(solution,
+// StringNode("addToBusiness", Set(
+// StringNode("makeAddressBook", Set(
+// StringNode("l.tail", Set())
+// ))
+// ,
+// StringNode("l.a", Set( ))
+// ))
+// ))
+// val resTemp = transformer(solution.getNodes.head).take(100)
+//
+// println(resTemp.head)
+// val it = resTemp.iterator.buffered
+// println(it.head)
+// println(it.hasNext)
+// println(it.head)
+// println(it.hasNext)
+//
+ for (output <- extractorResults) {
+ print("%20s %5f" format (output._1, output._2))
+
+ System.out.println("Press Any Key To Continue...");
+ new java.util.Scanner(System.in).nextLine();
+ }
+// println("\nExtracted: " + resTemp.size)
+// println("\nExtracted: " + extractorResults.size)
+
+// val message =
+// (for (output <- extractorResults)
+// yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
+// assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
+// assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
+//
+// println("Duplicity map size " + duplicityMap.size)
+// for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
+// println("Key: " + key)
+// println("Values: " + value.mkString("\n"))
+// }
+ }
+ }
+
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/EnumerationFastTest.scala b/src/test/scala/lesynth/EnumerationFastTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7eccbb25a1cb2cb3a6107c2c268ee6e5538aadd3
--- /dev/null
+++ b/src/test/scala/lesynth/EnumerationFastTest.scala
@@ -0,0 +1,182 @@
+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.refinement._
+import lesynth.examples._
+import lesynth.evaluation.CodeGenEvaluationStrategy
+import lesynth.ranking.Candidate
+import insynth.reconstruction.Output
+
+import insynth.util._
+import lesynth.util._
+
+class EnumerationFastTest 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 InSynthTemp(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)
+ }
+ }
+
+ test("Enumeration in Address example") {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+ 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 InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+ val listVal = funDef.args.head.toVariable
+
+ val variableRefiner =
+ new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap)
+
+ val (refined, newDeclarations) =
+ variableRefiner.checkRefinements(
+ CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+ assert(refined)
+ assert(allDeclarations.size + 2 == newDeclarations.size)
+
+ for (decl <- newDeclarations)
+ println(decl.getSimpleName)
+
+ val builder = new InitialEnvironmentBuilder(newDeclarations)
+
+// val solver = inSynth.solver
+// solver.getProofTree(builder)
+// val solution = solver.getProofTree
+//
+// import ProofTreeOperations._
+// assert(ProofTreeOperations.checkInhabitants(solution,
+// StringNode("AddressBook", Set(
+// //StringNode("[Cons=>List]", Set(StringNode("Cons"))),
+// StringNode("makeAddressBook", Set(StringNode("tail")))
+// ))
+// ))
+
+ val outputs = inSynth.getExpressions(builder)
+
+ for (output <- outputs.take(20000))
+ printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
+
+// val proofTree = inSynth.solver.getProofTree(builder)
+// val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
+// insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
+ }
+
+ }
+
+ ignore("Enumeration in Address (mergeAddressBooks) example") {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "AddressesMergeAddressBooks.scala")) {
+ 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 InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+// val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+// get.asInstanceOf[CaseClassDef]
+// val listVal = funDef.args.head.toVariable
+//
+// val variableRefiner =
+// new VariableRefiner(loader.directSubclassesMap,
+// loader.variableDeclarations, loader.classMap)
+//
+// val (refined, newDeclarations) =
+// variableRefiner.checkRefinements(
+// CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+// assert(refined)
+// assert(allDeclarations.size + 2 == newDeclarations.size)
+//
+// for (decl <- newDeclarations)
+// println(decl.getSimpleName)
+//
+// val builder = new InitialEnvironmentBuilder(newDeclarations)
+ //assert(inSynth.getCurrentBuilder.getAllDeclarations.size > 13, { throw new RuntimeException; "aaa" })
+// assert(false)
+
+ val outputs = inSynth.getExpressions//(builder)
+
+// val proofTree = inSynth.solver.getProofTree(builder)
+// val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
+// insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
+
+ for (output <- outputs.take(20000))
+ printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
+ }
+
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/EnumerationTest.scala b/src/test/scala/lesynth/EnumerationTest.scala
index 3cfd735c5ebc1f81a31d932c5ebc5bfacda8e3ad..b1a1efd5c238f96220c91c71988a5e0edb652980 100644
--- a/src/test/scala/lesynth/EnumerationTest.scala
+++ b/src/test/scala/lesynth/EnumerationTest.scala
@@ -19,12 +19,13 @@ import insynth.leon._
import insynth.leon.loader._
import insynth.engine._
-import lesynth.examples.InputExamples
+import lesynth.refinement._
+import lesynth.examples._
import lesynth.evaluation.CodeGenEvaluationStrategy
import lesynth.ranking.Candidate
import insynth.reconstruction.Output
-import lesynth.examples.Example
+import insynth.util._
import lesynth.util._
class EnumerationTest extends FunSuite {
@@ -71,5 +72,159 @@ class EnumerationTest extends FunSuite {
assert(takenRepeated.isEmpty)
}
}
+
+ ignore("Enumeration in Address example") {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+ 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 nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+ val listVal = funDef.args.head.toVariable
+
+ val variableRefiner =
+ new VariableRefiner(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap)
+
+ val (refined, newDeclarations) =
+ variableRefiner.checkRefinements(
+ CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+ assert(refined)
+ assert(allDeclarations.size + 2 == newDeclarations.size)
+
+ for (decl <- newDeclarations)
+ println(decl.getSimpleName)
+
+ val builder = new InitialEnvironmentBuilder(newDeclarations)
+
+ val solver = inSynth.solver
+ solver.getProofTree(builder)
+ val solution = solver.getProofTree
+
+ import ProofTreeOperations._
+ assert(ProofTreeOperations.checkInhabitants(solution,
+ StringNode("AddressBook", Set(
+ //StringNode("[Cons=>List]", Set(StringNode("Cons"))),
+ StringNode("makeAddressBook", Set(StringNode("tail")))
+ ))
+ ))
+
+ val outputs = inSynth.getExpressions(builder)
+
+// val proofTree = inSynth.solver.getProofTree(builder)
+// val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
+// insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
+
+// for (output <- outputs.take(20000))
+// printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
+ }
+
+ }
+
+ ignore("Enumeration in Address (mergeAddressBooks) example") {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "AddressesMergeAddressBooks.scala")) {
+ 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 nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+// get.asInstanceOf[CaseClassDef]
+// val listVal = funDef.args.head.toVariable
+//
+// val variableRefiner =
+// new VariableRefiner(loader.directSubclassesMap,
+// loader.variableDeclarations, loader.classMap)
+//
+// val (refined, newDeclarations) =
+// variableRefiner.checkRefinements(
+// CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+// assert(refined)
+// assert(allDeclarations.size + 2 == newDeclarations.size)
+//
+// for (decl <- newDeclarations)
+// println(decl.getSimpleName)
+//
+// val builder = new InitialEnvironmentBuilder(newDeclarations)
+ //assert(inSynth.getCurrentBuilder.getAllDeclarations.size > 13, { throw new RuntimeException; "aaa" })
+// assert(false)
+
+ val outputs = inSynth.getExpressions//(builder)
+
+// val proofTree = inSynth.solver.getProofTree(builder)
+// val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
+// insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
+
+ for (output <- outputs.take(20000))
+ printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
+ }
+
+ }
+
+ test("Enumeration in Address (mergeAddressBooks) example with fast reconstructor") {
+
+ for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "AddressesMergeAddressBooks.scala")) {
+ 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 InSynthTemp(loader, true)
+ // save all declarations seen
+ val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+// val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+// get.asInstanceOf[CaseClassDef]
+// val listVal = funDef.args.head.toVariable
+//
+// val variableRefiner =
+// new VariableRefiner(loader.directSubclassesMap,
+// loader.variableDeclarations, loader.classMap)
+//
+// val (refined, newDeclarations) =
+// variableRefiner.checkRefinements(
+// CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+// assert(refined)
+// assert(allDeclarations.size + 2 == newDeclarations.size)
+//
+// for (decl <- newDeclarations)
+// println(decl.getSimpleName)
+//
+// val builder = new InitialEnvironmentBuilder(newDeclarations)
+ //assert(inSynth.getCurrentBuilder.getAllDeclarations.size > 13, { throw new RuntimeException; "aaa" })
+// assert(false)
+
+ val outputs = inSynth.getExpressions//(builder)
+
+// val proofTree = inSynth.solver.getProofTree(builder)
+// val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
+// insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
+
+ for (output <- outputs.take(20000))
+ printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
+ }
+
+ }
}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/VariableRefinerTest.scala b/src/test/scala/lesynth/VariableRefinerTest.scala
index b452822297013b820408a489d7abda0aaf8fc160..49f30a53e93f0f0b9b207ea4abb9155a6171c1de 100644
--- a/src/test/scala/lesynth/VariableRefinerTest.scala
+++ b/src/test/scala/lesynth/VariableRefinerTest.scala
@@ -77,12 +77,14 @@ class VariableRefinerTest extends FunSpec with GivenWhenThen {
) :: Nil
)) {
variableRefiner.checkRefinements(CaseClassInstanceOf(nilAbstractClassDef, listVal),
+ BooleanLiteral(true),
allDeclarations)
}
and("after 2nd consequtive call, nothing should happen")
expect((false, allDeclarations)) {
variableRefiner.checkRefinements(CaseClassInstanceOf(nilAbstractClassDef, listVal),
+ BooleanLiteral(true),
allDeclarations)
}
}
diff --git a/src/test/scala/lesynth/VariableSolverRefinerTest.scala b/src/test/scala/lesynth/VariableSolverRefinerTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ba09ed5002ee1667982b98711e1fee275e83a4bf
--- /dev/null
+++ b/src/test/scala/lesynth/VariableSolverRefinerTest.scala
@@ -0,0 +1,233 @@
+package lesynth
+
+import scala.util.Random
+
+import org.scalatest.FunSpec
+import org.scalatest.GivenWhenThen
+
+import leon.purescala.Definitions._
+import leon.purescala.Common._
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+
+import insynth._
+import insynth.leon._
+import insynth.leon.loader._
+
+import lesynth.refinement._
+
+import lesynth.util._
+
+class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
+
+ import Scaffold._
+ import TestConfig._
+
+ describe("A variable solver refiner with list ADT") {
+
+ it("should refine if condition is isEmpty()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "refinement/ListConcatWithEmpty.scala")) {
+ val program = sctx.program
+ val solver = sctx.solver
+
+ val hole = Hole(funDef.getBody.getType)
+ val loader = new LeonLoader(program, hole, problem.as, false)
+ val allDeclarations = loader.load
+// val inSynth = new InSynth(loader, true)
+// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val isEmpty =
+ program.definedFunctions.find {
+ _.id.name == "isEmpty"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isEmpty"); null
+ }
+
+ val isEmptyBad =
+ program.definedFunctions.find {
+ _.id.name == "isEmptyBad"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isEmpty"); null
+ }
+
+ val listVal = funDef.args.head.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ given("a VariableSolverRefiner")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableSolverRefiner(
+ directSubclassMap, declarations, classMap, solver
+ )
+
+ val res = variableRefiner.checkRefinements(
+ isEmpty(listVal),
+ isEmpty(listVal),
+ declarations
+ )
+
+ then("declarations should be updated accordingly")
+ expect((true, declarations.size)) {
+ (res._1, res._2.size)
+ }
+
+ and("after 2nd consequtive call, nothing should happen")
+ expect((false, res._2)) {
+ val res2 = variableRefiner.checkRefinements(
+ isEmpty(listVal),
+ isEmpty(listVal),
+ res._2
+ )
+ (res2._1, res2._2)
+ }
+ }
+ }
+
+ it("should refine list to Cons if condition is hasContent()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "refinement/ListConcatWithEmpty.scala")) {
+ val program = sctx.program
+ val solver = sctx.solver
+
+ val hole = Hole(funDef.getBody.getType)
+ val loader = new LeonLoader(program, hole, problem.as, false)
+ val allDeclarations = loader.load
+// val inSynth = new InSynth(loader, true)
+// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val hasContent =
+ program.definedFunctions.find {
+ _.id.name == "hasContent"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract hasContent"); null
+ }
+
+ val listVal = funDef.args.head.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ given("a VariableSolverRefiner")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableSolverRefiner(
+ directSubclassMap, declarations, classMap, solver
+ )
+
+ val res = variableRefiner.checkRefinements(
+ hasContent(listVal),
+ hasContent(listVal),
+ declarations
+ )
+
+ then("declarations should be updated accordingly")
+ expect((true, declarations.size + 2)) {
+ (res._1, res._2.size)
+ }
+
+ and("after 2nd consequtive call, nothing should happen")
+ expect((false, res._2)) {
+ val res2 = variableRefiner.checkRefinements(
+ hasContent(listVal),
+ hasContent(listVal),
+ res._2
+ )
+ (res2._1, res2._2)
+ }
+ }
+ }
+
+ it("should not refine if condition is isEmptyBad()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "refinement/ListConcatWithEmpty.scala")) {
+ val program = sctx.program
+ val solver = sctx.solver
+
+ val hole = Hole(funDef.getBody.getType)
+ val loader = new LeonLoader(program, hole, problem.as, false)
+ val allDeclarations = loader.load
+// val inSynth = new InSynth(loader, true)
+// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val isEmpty =
+ program.definedFunctions.find {
+ _.id.name == "isEmpty"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isEmpty"); null
+ }
+
+ val isEmptyBad =
+ program.definedFunctions.find {
+ _.id.name == "isEmptyBad"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isEmpty"); null
+ }
+
+ val listVal = funDef.args.head.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ given("a VariableSolverRefiner")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableSolverRefiner(
+ directSubclassMap, declarations, classMap, solver
+ )
+
+ val res = variableRefiner.checkRefinements(
+ isEmptyBad(listVal),
+ isEmptyBad(listVal),
+ declarations
+ )
+
+ then("declarations should not be updated")
+ expect((false, res._2)) {
+ val res2 = variableRefiner.checkRefinements(
+ isEmptyBad(listVal),
+ isEmptyBad(listVal),
+ res._2
+ )
+ (res2._1, res2._2)
+ }
+ }
+ }
+
+ }
+
+ private def buildClassMap(program: Program) = {
+ val listAbstractClassDef = program.definedClasses.find(_.id.name == "List").
+ get.asInstanceOf[AbstractClassDef]
+
+ val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+
+ val consAbstractClassDef = program.definedClasses.find(_.id.name == "Cons").
+ get.asInstanceOf[CaseClassDef]
+
+ val directSubclassMap: Map[ClassType, Set[ClassType]] = Map(
+ AbstractClassType(listAbstractClassDef) ->
+ Set(CaseClassType(nilAbstractClassDef), CaseClassType(consAbstractClassDef))
+ )
+
+ val classMap: Map[Identifier, ClassType] = Map(
+ listAbstractClassDef.id -> AbstractClassType(listAbstractClassDef),
+ nilAbstractClassDef.id -> CaseClassType(nilAbstractClassDef),
+ consAbstractClassDef.id -> CaseClassType(consAbstractClassDef)
+ )
+
+ (directSubclassMap, AbstractClassType(listAbstractClassDef), classMap)
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/util/TestConfig.scala b/src/test/scala/lesynth/util/TestConfig.scala
index cdcb14fdc777b03236027ad2fd00838b5450db57..49eeeb5f3270b1461671183bcbf8d2bbe7b4b2af 100644
--- a/src/test/scala/lesynth/util/TestConfig.scala
+++ b/src/test/scala/lesynth/util/TestConfig.scala
@@ -24,6 +24,8 @@ object TestConfig {
val synthesisTestDir = "testcases/insynth-synthesis-tests/"
val lesynthTestDir = "testcases/lesynth/test/"
+
+ val lesynthSynthesisDir = "testcases/lesynth/synthesis/"
val HOME_FOLDER = "/home/kuraj/"
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
index 56ceaaa9b2a703929b6a05665d9476d3eddea77e..4faa50286c879d90d3e9fe12db58856459ee8993 100644
--- a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
@@ -15,36 +15,26 @@ 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 (
- 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)
- )
-
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ 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 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 cf30f2f1b39f732bcff1fbd7cd83a231275a9d42..6541b33b5dbce7b126d0eeac8b46858d286fa59d 100644
--- a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
@@ -15,8 +15,6 @@ 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 {
@@ -26,28 +24,24 @@ object BatchedQueue {
def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
- 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 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 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))
@@ -60,16 +54,7 @@ object BatchedQueue {
def snoc(p: Queue, x: Int): Queue =
choose { (res: Queue) =>
content(res) == content(p) ++ Set(x) &&
- (if (isEmpty(p)) true
- else content(tail(res)) ++ Set(x) == content(tail(res)))
+ (p.f == Nil || 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 83253e101f3f2d88fae44bb1f19c1b5aeed02c59..d35737dab64b76701d1904aae49dd4bfdb188a27 100644
--- a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
@@ -15,67 +15,42 @@ 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 && p.r == Nil
+ 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 (
- res =>
- content(res) == content(aList) ++ content(bList) &&
- size(res) == size(aList) + size(bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
- def reverse(list: List) = rev_append(list, Nil) ensuring (
- res =>
- content(res) == content(list) && size(res) == size(list))
+ 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) &&
- size(res) == size(f) + size(r)
+ res => content(res) == content(f) ++ content(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 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))
- }
-
+ def tail(p: Queue): Queue = {
+ require( if (p.f == Nil) p.r == Nil else true )
// p.f match {
// case Nil => p
// case Cons(_, xs) => checkf(xs, p.r)
// }
- def tail(p: Queue): List = {
- require(correctQueue(p))
choose {
- (res: List) =>
- invariantList(p, merge(head(p), res), Nil)
+ (res: Queue) =>
+ p.f match {
+ case Nil => isEmpty(res)
+ case Cons(x, xs) => content(res) ++ Set(x) == content(p) && content(res) != content(p)
+ }
}
}
-
+
}
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala b/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
index 82be984ba85dd726d3e31a6effa17531f5e8e58b..987c538c4ab36dc9b378f03fc24592210bcbd62b 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,2)
+ splithelper(Nil(),list,size(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
deleted file mode 100644
index 1563ee5ebf4bf3d505f5f0c3d68960f5b1c11e8a..0000000000000000000000000000000000000000
--- a/testcases/lesynth/synthesis/Other/Addresses.scala
+++ /dev/null
@@ -1,85 +0,0 @@
-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 2c14f9619b04732576039ac780b1136a2a03060f..6b9a73a9c1290c626d03f8a8cad3ea8f49bc8598 100644
--- a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
+++ b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
@@ -3,16 +3,21 @@ import leon.Annotations._
import leon.Utils._
object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
- case class Address(a: Int, b: Int, priv: Boolean)
+ case class Address(info: Info, 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 {
+ def content(l: List) : Set[Address] = l match {
case Nil => Set.empty[Address]
- case Cons(a, l1) => Set(a) ++ setA(l1)
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
}
def size(l: List) : Int = l match {
@@ -37,6 +42,13 @@ 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)
@@ -85,8 +97,7 @@ object Addresses {
def makeAddressBook(l: List): AddressBook =
choose {
(res: AddressBook) =>
- size(res) == size(l) &&
- allPrivate(res.pers) && allBusiness(res.business)
+ size(res) == size(l) && addressBookInvariant(res)
}
}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
index c13af538aab11dc0ff026a7be44b2517ddce0e72..c22541f8c9649c1e5485a41d5ebe4ce093d68bf2 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 setA(l: List) : Set[Address] = l match {
+ def content(l: List) : Set[Address] = l match {
case Nil => Set.empty[Address]
- case Cons(a, l1) => Set(a) ++ setA(l1)
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
}
def size(l: List) : Int = l match {
@@ -41,7 +41,16 @@ 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) => {
@@ -90,7 +99,8 @@ object Addresses {
choose {
(res: AddressBook) =>
size(res) == size(l) &&
- allPrivate(res.pers) && allBusiness(res.business)
+ allPrivate(res.pers) && allBusiness(res.business) &&
+ content(res) == content(l)
}
}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala b/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
index c40625ad431fe9646e9bfc132ad32eda729f41fb..0d6d8c0677806c687186184aa929e80032b869a8 100644
--- a/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
+++ b/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
@@ -3,16 +3,21 @@ import leon.Annotations._
import leon.Utils._
object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
- case class Address(a: Int, b: Int, priv: Boolean)
+ case class Address(info: Info, 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 {
+ def content(l: List) : Set[Address] = l match {
case Nil => Set.empty[Address]
- case Cons(a, l1) => Set(a) ++ setA(l1)
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
}
def size(l: List) : Int = l match {
@@ -36,14 +41,16 @@ 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 addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
def makeAddressBook(l: List): AddressBook = (l match {