From 0d41fa569947556336e09150ec71443fc6fe08ab Mon Sep 17 00:00:00 2001
From: Ivan Kuraj <ivan.kuraj@epfl.ch>
Date: Thu, 21 Mar 2013 16:09:24 +0100
Subject: [PATCH] Added added necessary sources and tests for insynth and
condition abduction, and two synthesis rules (immediate and deferred
instantiation)
---
src/main/scala/insynth/InSynth.scala | 71 ++
src/main/scala/insynth/leon/CommonTypes.scala | 14 +
.../scala/insynth/leon/LeonDeclaration.scala | 51 ++
src/main/scala/insynth/leon/LeonQuery.scala | 20 +
.../scala/insynth/leon/LeonQueryBuilder.scala | 24 +
.../leon/ReconstructionExpression.scala | 73 ++
.../scala/insynth/leon/TypeTransformer.scala | 52 ++
.../leon/loader/DeclarationFactory.scala | 75 ++
.../insynth/leon/loader/HoleExtractor.scala | 106 +++
.../scala/insynth/leon/loader/LoadSpec.scala | 6 +
.../scala/insynth/leon/loader/Loader.scala | 239 ++++++
.../scala/insynth/leon/loader/PreLoader.scala | 262 ++++++
.../scala/insynth/reconstruction/Output.scala | 12 +
.../reconstruction/Reconstructor.scala | 53 ++
.../codegen/CodeGenerator.scala | 119 +++
src/main/scala/lesynth/ExampleRunner.scala | 130 +++
src/main/scala/lesynth/Globals.scala | 22 +
src/main/scala/lesynth/InputExamples.scala | 148 ++++
src/main/scala/lesynth/Refiner.scala | 98 +++
src/main/scala/lesynth/Report.scala | 60 ++
.../scala/lesynth/SynthesizerExamples.scala | 725 +++++++++++++++++
...ConditionAbductionSynthesisImmediate.scala | 61 ++
.../ConditionAbductionSynthesisTwoPhase.scala | 71 ++
.../reconstruction/CodeGeneratorTest.scala | 63 ++
.../reconstruction/PhaseCombinationTest.scala | 74 ++
.../reconstruction/ReconstructorTest.scala | 95 +++
.../testutil/CommonLeonExpressions.scala | 20 +
src/test/scala/lesynth/AnalyzerTest.scala | 49 ++
src/test/scala/lesynth/RefinerTest.scala | 209 +++++
.../TryOutSynthesizerExamplesTest.scala | 672 +++++++++++++++
src/test/scala/lesynth/TryOutTest.scala | 639 +++++++++++++++
.../lesynth/TryOutTestWithFiltering.scala | 768 ++++++++++++++++++
testcases/lesynth/InsertionSortFull.scala | 51 ++
.../lesynth/InsertionSortHoleInsert.scala | 54 ++
testcases/lesynth/InsertionSortHoleSort.scala | 53 ++
testcases/lesynth/ListOperations.scala | 45 +
testcases/lesynth/ListOperationsHole.scala | 24 +
testcases/lesynth/ListOperationsHole2.scala | 24 +
testcases/lesynth/MergeSortHole.scala | 81 ++
39 files changed, 5413 insertions(+)
create mode 100644 src/main/scala/insynth/InSynth.scala
create mode 100644 src/main/scala/insynth/leon/CommonTypes.scala
create mode 100644 src/main/scala/insynth/leon/LeonDeclaration.scala
create mode 100644 src/main/scala/insynth/leon/LeonQuery.scala
create mode 100644 src/main/scala/insynth/leon/LeonQueryBuilder.scala
create mode 100644 src/main/scala/insynth/leon/ReconstructionExpression.scala
create mode 100644 src/main/scala/insynth/leon/TypeTransformer.scala
create mode 100644 src/main/scala/insynth/leon/loader/DeclarationFactory.scala
create mode 100644 src/main/scala/insynth/leon/loader/HoleExtractor.scala
create mode 100644 src/main/scala/insynth/leon/loader/LoadSpec.scala
create mode 100644 src/main/scala/insynth/leon/loader/Loader.scala
create mode 100644 src/main/scala/insynth/leon/loader/PreLoader.scala
create mode 100644 src/main/scala/insynth/reconstruction/Output.scala
create mode 100644 src/main/scala/insynth/reconstruction/Reconstructor.scala
create mode 100644 src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
create mode 100644 src/main/scala/lesynth/ExampleRunner.scala
create mode 100644 src/main/scala/lesynth/Globals.scala
create mode 100755 src/main/scala/lesynth/InputExamples.scala
create mode 100755 src/main/scala/lesynth/Refiner.scala
create mode 100755 src/main/scala/lesynth/Report.scala
create mode 100755 src/main/scala/lesynth/SynthesizerExamples.scala
create mode 100755 src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
create mode 100755 src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
create mode 100644 src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
create mode 100644 src/test/scala/insynth/reconstruction/PhaseCombinationTest.scala
create mode 100644 src/test/scala/insynth/reconstruction/ReconstructorTest.scala
create mode 100644 src/test/scala/insynth/testutil/CommonLeonExpressions.scala
create mode 100644 src/test/scala/lesynth/AnalyzerTest.scala
create mode 100644 src/test/scala/lesynth/RefinerTest.scala
create mode 100755 src/test/scala/lesynth/TryOutSynthesizerExamplesTest.scala
create mode 100644 src/test/scala/lesynth/TryOutTest.scala
create mode 100644 src/test/scala/lesynth/TryOutTestWithFiltering.scala
create mode 100644 testcases/lesynth/InsertionSortFull.scala
create mode 100644 testcases/lesynth/InsertionSortHoleInsert.scala
create mode 100644 testcases/lesynth/InsertionSortHoleSort.scala
create mode 100644 testcases/lesynth/ListOperations.scala
create mode 100644 testcases/lesynth/ListOperationsHole.scala
create mode 100644 testcases/lesynth/ListOperationsHole2.scala
create mode 100644 testcases/lesynth/MergeSortHole.scala
diff --git a/src/main/scala/insynth/InSynth.scala b/src/main/scala/insynth/InSynth.scala
new file mode 100644
index 000000000..bcba1f478
--- /dev/null
+++ b/src/main/scala/insynth/InSynth.scala
@@ -0,0 +1,71 @@
+package insynth
+
+import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFactory }
+import insynth.reconstruction.codegen.CodeGenerator
+import insynth.reconstruction.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 InSynth(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 = {
+ 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) = {
+ val proofTree = solver.getProofTree(builder)
+
+ 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 InSynth {
+
+ def apply(declarations: List[Declaration], goalType: Type, ordered: Boolean) =
+ new InSynth(declarations, goalType, ordered)
+
+// def apply(program: Program, hole: Hole, ordered: Boolean) =
+// new InSynth(new LeonLoader(program, hole).load, hole.getType, ordered)
+
+ def apply(loader: LeonLoader, ordered: Boolean) =
+ new InSynth(loader.load, loader.hole.getType, ordered)
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/CommonTypes.scala b/src/main/scala/insynth/leon/CommonTypes.scala
new file mode 100644
index 000000000..1e7f5ba62
--- /dev/null
+++ b/src/main/scala/insynth/leon/CommonTypes.scala
@@ -0,0 +1,14 @@
+package insynth.leon
+
+import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
+
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Common.FreshIdentifier
+import leon.purescala.Definitions.AbstractClassDef
+
+object CommonTypes {
+
+ val LeonBottomType = AbstractClassType(new AbstractClassDef(FreshIdentifier("$IDontCare$")))
+ val InSynthBottomType = Const("$IDontCare$")
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/LeonDeclaration.scala b/src/main/scala/insynth/leon/LeonDeclaration.scala
new file mode 100644
index 000000000..40255fb76
--- /dev/null
+++ b/src/main/scala/insynth/leon/LeonDeclaration.scala
@@ -0,0 +1,51 @@
+package insynth.leon
+
+import insynth.structures.SuccinctType
+import insynth.interfaces.Declaration
+import insynth.structures.Weight._
+
+import leon.purescala.TypeTrees.{ TypeTree => LeonType }
+import leon.purescala.Trees.Expr
+
+case class LeonDeclaration(
+ override val inSynthType: SuccinctType, override val weight: Weight,
+ val leonType: LeonType, val expression: ReconstructionExpression
+)
+extends Declaration(inSynthType, weight) {
+
+ def this(expression: ReconstructionExpression, inSynthType: SuccinctType,
+ leonType: LeonType, commutative: Boolean, weight: Weight
+ ) = {
+ this(inSynthType, weight, leonType, expression)
+ isCommunitative = commutative
+ }
+
+ def this(expression: ReconstructionExpression, inSynthType: SuccinctType, leonType: LeonType)
+ = this(inSynthType, 1.0f, leonType, expression)
+
+ var isCommunitative = false
+
+ private var query = false
+
+ def getDomainType = leonType
+
+ def getSimpleName = expression.toString
+
+ override def toString = getSimpleName + ":" + inSynthType + ":" + leonType + "[" + expression + "]"
+
+}
+
+object LeonDeclaration {
+
+ def apply(expression: ReconstructionExpression, inSynthType: SuccinctType, leonType: LeonType)
+ = new LeonDeclaration(expression, inSynthType, leonType)
+
+ def apply(expression: ReconstructionExpression, inSynthType: SuccinctType,
+ leonType: LeonType, weight: Weight
+ ) = new LeonDeclaration(inSynthType, weight, leonType, expression)
+
+ def apply(expression: ReconstructionExpression, inSynthType: SuccinctType,
+ leonType: LeonType, commutative: Boolean, weight: Weight
+ ) = new LeonDeclaration(expression, inSynthType, leonType, commutative, weight)
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/LeonQuery.scala b/src/main/scala/insynth/leon/LeonQuery.scala
new file mode 100644
index 000000000..c4e1dc70c
--- /dev/null
+++ b/src/main/scala/insynth/leon/LeonQuery.scala
@@ -0,0 +1,20 @@
+package insynth.leon
+
+import insynth.leon.loader.DeclarationFactory
+import insynth.engine.InitialSender
+import insynth.structures.SuccinctType
+import insynth.interfaces.Query
+
+import leon.purescala.TypeTrees._
+import leon.purescala.Common.FreshIdentifier
+
+case class LeonQuery(override val inSynthRetType: SuccinctType, decl: LeonDeclaration, sender: InitialSender)
+extends Query(inSynthRetType) {
+
+ def getSolution = sender.getAnswers
+
+ def getDeclaration = decl
+
+ def getSender = sender
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/LeonQueryBuilder.scala b/src/main/scala/insynth/leon/LeonQueryBuilder.scala
new file mode 100644
index 000000000..e8b63a103
--- /dev/null
+++ b/src/main/scala/insynth/leon/LeonQueryBuilder.scala
@@ -0,0 +1,24 @@
+package insynth.leon
+
+import insynth.leon.loader.DeclarationFactory
+import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
+import insynth.engine.InitialSender
+import insynth.interfaces.QueryBuilder
+
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Common.FreshIdentifier
+import leon.purescala.Definitions.AbstractClassDef
+
+import CommonTypes._
+
+class LeonQueryBuilder(leonGoalType: LeonType) extends QueryBuilder(TypeTransformer(leonGoalType)) {
+
+ val leonRetType = LeonBottomType
+ val leonType = FunctionType(List(leonGoalType), leonRetType)
+
+ val inSynthRetType = InSynthBottomType
+ val inSynthType = Arrow(TSet(tpe), inSynthRetType)
+
+ def getQuery = LeonQuery(inSynthRetType, new LeonDeclaration(QueryExpression, inSynthType, leonType), new InitialSender())
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/ReconstructionExpression.scala b/src/main/scala/insynth/leon/ReconstructionExpression.scala
new file mode 100644
index 000000000..26731b2ef
--- /dev/null
+++ b/src/main/scala/insynth/leon/ReconstructionExpression.scala
@@ -0,0 +1,73 @@
+package insynth.leon
+
+import leon.purescala.TypeTrees.{ TypeTree => LeonType }
+import leon.purescala.Trees.Expr
+import leon.purescala.Common.Identifier
+
+trait ReconstructionExpression {
+
+ def getSimpleName: String
+
+ override def toString = getSimpleName
+
+}
+
+case object QueryExpression extends ReconstructionExpression {
+
+ def getSimpleName = "query"
+
+}
+
+case object ErrorExpression extends ReconstructionExpression {
+
+ def getSimpleName = "error"
+
+}
+
+object ImmediateExpression {
+
+ def apply(id: Identifier, expr: Expr): ImmediateExpression = ImmediateExpression(id.toString, expr)
+
+}
+
+case class ImmediateExpression( name: String, expr: Expr ) extends ReconstructionExpression {
+
+ def this(id: Identifier, expr: Expr) = this(id.toString, expr)
+
+ def apply( ) = expr
+
+ def getSimpleName: String = name
+
+}
+
+object UnaryReconstructionExpression {
+
+ def apply(id: Identifier, funToExpr: Expr => Expr): UnaryReconstructionExpression = UnaryReconstructionExpression(id.toString, funToExpr)
+
+}
+
+case class UnaryReconstructionExpression( name: String, funToExpr: Expr => Expr ) extends ReconstructionExpression {
+
+ def this(id: Identifier, funToExpr: Expr => Expr) = this(id.toString, funToExpr)
+
+ def apply( op: Expr ) = funToExpr(op)
+
+ def getSimpleName: String = name
+
+}
+
+object NaryReconstructionExpression {
+
+ def apply(id: Identifier, funToExpr: List[Expr] => Expr): NaryReconstructionExpression = NaryReconstructionExpression(id.toString, funToExpr)
+
+}
+
+case class NaryReconstructionExpression( name: String, funToExpr: List[Expr] => Expr ) extends ReconstructionExpression {
+
+ def this(id: Identifier, funToExpr: List[Expr] => Expr) = this(id.toString, funToExpr)
+
+ def apply( op: List[Expr] ) = funToExpr(op)
+
+ def getSimpleName: String = name
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/TypeTransformer.scala b/src/main/scala/insynth/leon/TypeTransformer.scala
new file mode 100644
index 000000000..d8358f7d1
--- /dev/null
+++ b/src/main/scala/insynth/leon/TypeTransformer.scala
@@ -0,0 +1,52 @@
+package insynth.leon
+
+import insynth.structures._
+
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, BottomType => LeonBottomType, _ }
+import leon.purescala.Common.FreshIdentifier
+import leon.purescala.Definitions._
+
+object TypeTransformer extends ( LeonType => SuccinctType ) {
+
+ def apply(typeDef: ClassTypeDef): SuccinctType = {
+ implicit def singletonList(x: SuccinctType) = List(x)
+
+ typeDef match {
+ case abs: AbstractClassDef => Const(abs.id.name)
+ case caseClassDef: CaseClassDef => Const(caseClassDef.id.name)
+ }
+ }
+
+ def apply(leonType: LeonType): SuccinctType = {
+ implicit def singletonList(x: SuccinctType) = List(x)
+
+ leonType match {
+ case Untyped => throw new RuntimeException("Should not happen at this point")
+ case AnyType => Const("Any")
+ case LeonBottomType => BottomType //Const("Bottom")
+ case BooleanType => Const("Boolean")
+ case UnitType => Const("Unit")
+ case Int32Type => Const("Int")
+ case ListType(baseType) => Instance("List", this(baseType) )
+ case ArrayType(baseType) => Instance("Array", this(baseType) )
+ case TupleType(baseTypes) => Instance("Tuple", baseTypes map { this(_) } toList )
+ case SetType(baseType) => Instance("Set", this(baseType) )
+ case MultisetType(baseType) => Instance("MultiSet", this(baseType) )
+ case MapType(from, to) => Instance("Map", List( this(from), this(to) ))
+ case FunctionType(froms, to) => transformFunction(to, froms)
+ case c: ClassType => Const(c.id.name)
+ }
+ }
+
+ private def transformFunction(fun: LeonType, params: List[LeonType]): SuccinctType = fun match {
+ case FunctionType(froms, to) =>
+ transformFunction(to, params ++ froms)
+ case Untyped => throw new RuntimeException("Should not happen at this point")
+ // query will have this
+ case LeonBottomType =>
+ Arrow( TSet(params map this distinct), this(fun) )
+ case t =>
+ Arrow( TSet(params map this distinct), this(t) )
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/loader/DeclarationFactory.scala b/src/main/scala/insynth/leon/loader/DeclarationFactory.scala
new file mode 100644
index 000000000..16c2bd6df
--- /dev/null
+++ b/src/main/scala/insynth/leon/loader/DeclarationFactory.scala
@@ -0,0 +1,75 @@
+package insynth.leon.loader
+
+import insynth.leon.{ LeonDeclaration => Declaration, ReconstructionExpression,
+ ErrorExpression, UnaryReconstructionExpression, ImmediateExpression }
+import insynth.engine.InitialEnvironmentBuilder
+import insynth.structures.{ SuccinctType => InSynthType, Variable => InSynthVariable, _}
+import insynth.leon.TypeTransformer
+
+import leon.purescala.Definitions.{ Program, FunDef, ClassTypeDef, VarDecl }
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.Trees._
+
+object DeclarationFactory {
+
+ val WEIGHT_FOR_LITERALS = 5f
+
+ val listOfInstanceTypes = List(BooleanType, Int32Type)
+
+ def makeDeclaration(expression: ReconstructionExpression, leonType: LeonType) = {
+ val inSynthType = TypeTransformer(leonType)
+ Declaration(expression, inSynthType, leonType)
+ }
+
+ def makeLiteral(expression: ReconstructionExpression, leonType: LeonType) = {
+ val inSynthType = TypeTransformer(leonType)
+ Declaration(expression, inSynthType, leonType, WEIGHT_FOR_LITERALS)
+ }
+
+ def makeDeclaration(expression: ReconstructionExpression, leonType: LeonType, commutative: Boolean) = {
+ val inSynthType = TypeTransformer(leonType)
+ Declaration(expression, inSynthType, leonType)
+ }
+
+ def makeArgumentDeclaration(id: Identifier) = {
+ val leonType = id.getType
+ val inSynthType = TypeTransformer(leonType)
+ Declaration(ImmediateExpression(id, Variable(id)), inSynthType, leonType)
+ }
+
+ def makeArgumentDeclaration(varDecl: VarDecl) = {
+ val leonType = varDecl.getType
+ val inSynthType = TypeTransformer(leonType)
+ Declaration(ImmediateExpression(varDecl.id, Variable(varDecl.id)), inSynthType, leonType)
+ }
+
+ def makeInheritance(from: ClassTypeDef, to: ClassTypeDef) = {
+ val expr = UnaryReconstructionExpression(from + " is " + to, 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 inSynthType = Arrow(TSet(TypeTransformer(from)), TypeTransformer(to))
+ Declaration(expr, inSynthType, FunctionType(List(from), to))
+ }
+
+ def makeDeclarationForTypes(types: List[LeonType])(makeFunction: LeonType => _) =
+ for (tpe <- types)
+ makeFunction(tpe)
+
+ def yieldDeclarationForTypes(types: List[LeonType])(makeFunction: LeonType => Declaration) =
+ for (tpe <- types)
+ yield makeFunction(tpe)
+
+ def makeAbstractDeclaration(inSynthType: InSynthType) = {
+ throw new RuntimeException
+ Declaration(getAbsExpression(inSynthType), inSynthType, null)
+ }
+
+ // define this for abstract declarations
+ def getAbsExpression(inSynthType: InSynthType) =
+ ErrorExpression
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/loader/HoleExtractor.scala b/src/main/scala/insynth/leon/loader/HoleExtractor.scala
new file mode 100644
index 000000000..10ee46b04
--- /dev/null
+++ b/src/main/scala/insynth/leon/loader/HoleExtractor.scala
@@ -0,0 +1,106 @@
+package insynth.leon.loader
+
+import insynth.leon.{ ImmediateExpression, LeonDeclaration }
+
+import leon.purescala.Definitions.{ Program, FunDef }
+import leon.purescala.Trees._
+import leon.purescala.Extractors._
+import leon.purescala.Common.{ Identifier }
+
+class HoleExtractor(program: Program, hole: Hole) {
+
+ import DeclarationFactory._
+
+ def extractHole: Option[(FunDef, List[LeonDeclaration])] = {
+
+ // the list of declarations to be returned
+ //var list = scala.collection.mutable.MutableList[Declaration]()
+
+ // XXX we currently go through all functions, not efficient!
+ var foundHoleCount = 0
+ for (
+ funDef <-program.definedFunctions;
+ if funDef.hasBody;
+ val (foundHole, declarations) = scanMethod(funDef.getBody);
+ if foundHole;
+ val argDeclarations = funDef.args map { makeArgumentDeclaration(_) }
+ ) {
+ // hack
+ //Globals.holeFunDef = funDef
+
+ foundHoleCount+=1
+
+ return Some((funDef, argDeclarations.toList ++ declarations))
+ }
+ //assert(foundHoleCount <= 1)
+
+ None
+
+ }
+
+ def scanMethod(functionBody: Expr): (Boolean, Set[LeonDeclaration]) = {
+
+ case class LocalPair(foundHole: Boolean, currentSet: Set[Identifier]) {
+ def ++?(pair: Pair[Boolean, Set[Identifier]]): (Boolean, Set[Identifier]) = {
+ val (foundHoleSec, currentSetSec) = pair
+ if (foundHole)
+ (true, currentSet)
+ else (foundHoleSec, currentSet ++ currentSetSec)
+ }
+ def +(id: Identifier): (Boolean, Set[Identifier]) = {
+ (foundHole, currentSet + id)
+ }
+ def /:\(pair: Pair[Boolean, Set[Identifier]]): (Boolean, Set[Identifier]) = {
+ if (foundHole)
+ (foundHole, currentSet)
+ else
+ pair
+ }
+ }
+ implicit def localPairCast(pair: Pair[Boolean, Set[Identifier]]) = LocalPair(pair._1, pair._2)
+
+ def allIdentifiers(expr: Expr) : (Boolean, Set[Identifier]) = expr match {
+ case l @ Let(binder, e, b) => allIdentifiers(e) /:\ ( allIdentifiers(b) + binder )
+// case l @ LetVar(binder, e, b) => allIdentifiers(e) /:\ ( allIdentifiers(b) + binder )
+// case l @ LetDef(fd, b) =>
+// allIdentifiers(fd.getBody) /:\ ( allIdentifiers(b) + fd.id )
+
+ //case block @ Block(exprs, last)
+ // NOTE: NAryOperator covers block
+ case n @ NAryOperator(args, _) =>
+ ((false, Set[Identifier]()) /: (args map (allIdentifiers(_)))) {
+ case (currentPair, newPair) => currentPair /:\ newPair
+ }
+ case b @ BinaryOperator(a1,a2,_) => allIdentifiers(a1) ++? allIdentifiers(a2)
+ case u @ UnaryOperator(a,_) => allIdentifiers(a)
+ case i @ IfExpr(a1,a2,a3) => allIdentifiers(a1) /:\ allIdentifiers(a2) /:\ allIdentifiers(a3)
+ case m @ MatchExpr(scrut, cses) =>
+ // ??
+ allIdentifiers(scrut) ++?
+ ( (false, Set[Identifier]()) /: ( cses map {
+ cse =>
+ val rhsResult = allIdentifiers(cse.rhs)
+ (rhsResult._1, rhsResult._2 ++ cse.pattern.allIdentifiers)
+ })
+ ) {
+ case (currentPair, newPair) => currentPair ++? newPair
+ }
+ case Variable(id) => (false, Set.empty)
+ case h: Hole => (true, Set.empty)
+ case t: Terminal => (false, Set.empty)
+ }
+
+ val (foundHole, collectedIdentifiers) = allIdentifiers(functionBody)
+
+ (
+ foundHole,
+ for ( id <- collectedIdentifiers )
+ yield makeDeclaration(
+ ImmediateExpression( id, Variable(id) ),
+ id.getType
+ )
+ )
+
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/loader/LoadSpec.scala b/src/main/scala/insynth/leon/loader/LoadSpec.scala
new file mode 100644
index 000000000..835e1f8fc
--- /dev/null
+++ b/src/main/scala/insynth/leon/loader/LoadSpec.scala
@@ -0,0 +1,6 @@
+package insynth.leon.loader
+
+/** defines what to load in the PreLoader */
+class LoadSpec {
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/loader/Loader.scala b/src/main/scala/insynth/leon/loader/Loader.scala
new file mode 100644
index 000000000..f318a7a36
--- /dev/null
+++ b/src/main/scala/insynth/leon/loader/Loader.scala
@@ -0,0 +1,239 @@
+package insynth.leon.loader
+
+import insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression, ImmediateExpression, UnaryReconstructionExpression }
+import insynth.structures.{ SuccinctType => InSynthType }
+import insynth.interfaces.Loader
+import insynth.util.logging.HasLogger
+
+import leon.purescala.Definitions.{ Program, FunDef }
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Trees.{ Hole, Expr, FunctionInvocation, _ }
+import leon.purescala.Common.{ Identifier }
+import leon.purescala.Definitions.{ AbstractClassDef, CaseClassDef, ClassTypeDef }
+
+case class LeonLoader(program: Program, hole: Hole,
+ variables: List[Identifier], loadArithmeticOps: Boolean = true) extends Loader with HasLogger {
+ //var temporaryDesiredType: LeonType = Int32Type
+
+ lazy val classMap: Map[Identifier, ClassType] = extractClasses
+
+ lazy val directSubclassesMap: Map[ClassType, Set[ClassType]] = initializeSubclassesMap(program)
+
+ // arguments + all found variables in the hole function
+ lazy val variableDeclarations: Seq[Declaration] = variables.map(DeclarationFactory.makeArgumentDeclaration(_))
+
+ //lazy val holeDef = initResults._3
+
+ lazy val initResults = init
+
+ import DeclarationFactory._
+
+ def load: List[Declaration] = initResults
+
+ private def init = {
+
+ // the list of declarations to be returned
+ var list = scala.collection.mutable.MutableList[Declaration]()
+
+ /* add declarations to builder */
+
+ // add function declarations
+ for( funDef@FunDef(id, returnType, args, _, _, _) <- program.definedFunctions ) {
+ val leonFunctionType = FunctionType(args map { _.tpe } toList, returnType)
+
+ val newDeclaration = makeDeclaration(
+ NaryReconstructionExpression( id, { args: List[Expr] => FunctionInvocation(funDef, args) } ),
+ leonFunctionType
+ )
+
+ list += newDeclaration
+ fine("Leon loader added declaration: " + newDeclaration)
+ }
+
+ // add predefs and literals
+ list ++= PreLoader(loadArithmeticOps)
+
+ list ++= extractInheritances
+
+ list ++= extractCaseClasses
+
+ list ++= extractFields
+
+ list ++= extractClassDependentDeclarations
+
+ list ++= variableDeclarations
+
+ list.toList
+
+ // no need for doing this (we will have everything from the synthesis problem context)
+// new HoleExtractor(program, hole).extractHole match {
+// case Some((holeDef, decls)) =>
+// list ++= decls
+//
+// (list.toList, decls, holeDef)
+// case _ =>
+// throw new RuntimeException("Hole extractor problem")
+// }
+ }
+
+ def initializeSubclassesMap(program: Program) = {
+ val seqOfPairs = for (classDef <- program.definedClasses)
+ yield classDef match {
+ case caseClassDef: CaseClassDef =>
+ val caseClassType = classMap(classDef.id)
+ ( caseClassType, Set[ClassType]( /*caseClassType*/ ) )
+ case absClassDef: AbstractClassDef =>
+ val childrenTypes = for (child <- absClassDef.knownChildren)
+ yield classMap(child.id)
+ ( classMap(absClassDef.id), childrenTypes.toSet )
+ }
+
+ seqOfPairs.toMap
+ }
+
+ def extractClasses: Map[Identifier, ClassType] = {
+ (
+ for (classDef <- program.definedClasses)
+ yield classDef match {
+ case caseClassDef: CaseClassDef => ( classDef.id, CaseClassType(caseClassDef) )
+ case absClassDef: AbstractClassDef => ( absClassDef.id, AbstractClassType(absClassDef) )
+ }
+ ) toMap
+ }
+
+ // TODO add anyref to all and all to bottom ???
+ def extractInheritances: Seq[Declaration] = {
+
+ def extractInheritancesRec(classDef: ClassTypeDef): List[Declaration] =
+ classDef match {
+ case abs: AbstractClassDef =>
+ Nil ++
+ (
+ for (child <- abs.knownChildren)
+ yield makeInheritance(
+ classMap(child.id), classMap(abs.id)
+ )
+ ) ++ (
+ for (child <- abs.knownChildren)
+ yield extractInheritancesRec(child)
+ ).flatten
+ case _ =>
+ Nil
+ }
+
+// (for (classHierarchyRoot <- program.classHierarchyRoots)
+// yield extractInheritancesRec(classHierarchyRoot)).flatten.toList
+
+ for (classHierarchyRoot <- program.classHierarchyRoots;
+ inheritance <- extractInheritancesRec(classHierarchyRoot))
+ yield inheritance
+ }
+
+ def extractFields: Seq[Declaration] = {
+ def extractFields(classDef: ClassTypeDef) = classDef match {
+ case abs: AbstractClassDef =>
+ // this case does not seem to work
+ //abs.fields
+ Seq.empty
+ case cas: CaseClassDef =>
+ for (field <- cas.fields)
+ yield makeDeclaration(
+ UnaryReconstructionExpression( "Field(" + cas + "." + field.id + ")", { CaseClassSelector(cas, _: Expr, field.id) } ),
+ FunctionType(List(classMap(cas.id)), field.id.getType)
+ )
+ }
+
+ for (classDef <- program.definedClasses;
+ decl <- extractFields(classDef))
+ yield decl
+ }
+
+ def extractCaseClasses: Seq[Declaration] = {
+ for (caseClassDef@CaseClassDef(id, parent, fields) <- program.definedClasses)
+ yield fields match {
+ case Nil => makeDeclaration(
+ ImmediateExpression( "Cst(" + id + ")", { CaseClass(caseClassDef, Nil) } ),
+ classMap(id)
+ )
+ case _ => makeDeclaration(
+ NaryReconstructionExpression( "Cst(" + id + ")", { CaseClass(caseClassDef, _: List[Expr]) } ),
+ FunctionType(fields map { _.id.getType } toList, classMap(id))
+ )
+ }
+ }
+
+ def extractClassDependentDeclarations: Seq[Declaration] = {
+// def getClassDef(id: Identifier): CaseClassDef = {
+// program.caseClassDef(id.name)
+// program.definedClasses.find( _.id == `id` ) match {
+// case Some(classDef) => classDef
+// case _ => throw new RuntimeException
+// }
+// }
+
+ for ( classDef@CaseClassDef(_, _, _) <- program.definedClasses filter { _.isInstanceOf[CaseClassDef] };
+ if classDef.hasParent)
+ yield makeDeclaration(
+ UnaryReconstructionExpression( "isInstance[" + classDef.id + "]", { CaseClassInstanceOf(classDef, _: Expr)
+ } ),
+ FunctionType(List(classMap(classDef.parent.get.id)), BooleanType)
+ )
+ }
+
+ // XXX does not care about hiding, does not see function arguments
+
+// def loadLocals(functionBody: Expr, hole: Expr): Set[Declaration] = {
+// scanMethod(functionBody, hole)._2
+// }
+
+}
+
+// old load function
+// def load(program: Program, hole: Hole): List[Declaration] = {
+// initializeClassMap(program)
+//
+// var list: scala.collection.mutable.LinkedList[Declaration] = scala.collection.mutable.LinkedList()
+//
+// /* add declarations to builder */
+//
+// // add function declarations
+// for( funDef@FunDef(id, returnType, args, _, _, _) <- program.definedFunctions ) {
+// val leonFunctionType = FunctionType(args map { _.tpe } toList, returnType)
+//
+// val newDeclaration = makeDeclaration(
+// NaryReconstructionExpression( id, { args: List[Expr] => FunctionInvocation(funDef, args) } ),
+// leonFunctionType
+// )
+//
+// list :+= newDeclaration
+// }
+//
+// // add predefs and literals
+// list ++= PreLoader()
+//
+// list ++= extractInheritances(program)
+//
+// list ++= extractCaseClasses(program)
+////
+//// builder.addDeclarations( extractClassDependentDeclarations(program) )
+//
+// // XXX we currently go through all functions, not efficient!
+// var foundHoleCount = 0
+// for (
+// funDef <-program.definedFunctions;
+// if funDef.hasBody;
+// val (foundHole, declarations) = scanMethod(funDef.getBody, hole);
+// if foundHole;
+// val argDeclarations = funDef.args map { makeArgumentDeclaration(_) }
+// ) {
+// // hack
+// Globals.holeFunDef = funDef
+// foundHoleCount+=1
+//
+// list ++= declarations.toList
+// list ++= argDeclarations
+// }
+// assert(foundHoleCount <= 1)
+//
+// list toList
+// }
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/loader/PreLoader.scala b/src/main/scala/insynth/leon/loader/PreLoader.scala
new file mode 100644
index 000000000..1f72ac43b
--- /dev/null
+++ b/src/main/scala/insynth/leon/loader/PreLoader.scala
@@ -0,0 +1,262 @@
+package insynth.leon.loader
+
+import insynth.structures.{ SuccinctType => InSynthType }
+import insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression => NAE, ImmediateExpression => IE }
+import insynth.engine.InitialEnvironmentBuilder
+
+import leon.purescala.Definitions.{ Program, FunDef }
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Common.{ Identifier }
+import leon.purescala.Trees._
+
+object PreLoader extends ( (Boolean) => List[Declaration] ) {
+
+ import DeclarationFactory._
+
+ def apply(loadArithmeticOps: Boolean = true): List[Declaration] = {
+
+ val supportedBaseTypes = List(BooleanType, Int32Type)
+ var list = scala.collection.mutable.MutableList[Declaration]()
+
+ list += getAnd
+ list += getNot
+
+ list += getLessEquals
+ list ++= getEquals(supportedBaseTypes)
+
+ if (loadArithmeticOps)
+ list ++= getArithmeticOps
+
+ list toList
+ }
+
+ def getAnd =
+ // case And(args) if args.isEmpty => BooleanLiteral(true)
+ makeDeclaration(
+ makeNAE("And", { case List(arg1, arg2) => And( List(arg1, arg2) ) }),
+ FunctionType( List(BooleanType, BooleanType), BooleanType )
+ )
+
+ def getNot =
+ // case Not(arg) => rec(ctx, arg) match {
+ makeDeclaration(
+ makeNAE( "Not", { case List(arg) => Not( arg ) } ),
+ FunctionType( List(BooleanType), BooleanType )
+ )
+
+ def getOr =
+ // case Or(args) if args.isEmpty => BooleanLiteral(false)
+ makeDeclaration(
+ makeNAE( "Or", { case List(arg1, arg2) => Or( List(arg1, arg2) ) } ),
+ FunctionType( List(BooleanType, BooleanType), BooleanType )
+ )
+
+ def getImplies =
+ // case Implies(l, r) => (rec(ctx, l), rec(ctx, r)) match {
+ makeDeclaration(
+ makeNAE( "=>", { case List(left, right) => Implies( left, right ) } ),
+ FunctionType( List(BooleanType, BooleanType), BooleanType )
+ )
+
+ def getIff =
+ //case Iff(le, re) => (rec(ctx, le), rec(ctx, re)) match {
+ makeDeclaration(
+ makeNAE( "<=>", { case List(left, right) => Iff( left, right ) } ),
+ FunctionType( List(BooleanType, BooleanType), BooleanType )
+ )
+
+ def getEquals(listOfInstanceTypes: List[LeonType]) =
+ // case Equals(le, re) => {
+ yieldDeclarationForTypes(listOfInstanceTypes) {
+ x: LeonType =>
+ makeDeclaration(
+ makeNAE( "=", { case List(left, right) => Equals( left, right ) } ),
+ FunctionType( List(x, x), BooleanType ),
+ true
+ )
+ }
+
+ def getArithmeticOps = {
+ // case Plus(l, r) => (rec(ctx, l), rec(ctx, r)) match {
+ makeDeclaration(
+ makeNAE( "+", { case List(left, right) => Plus( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), Int32Type )
+ ) ::
+ // case Minus(l, r) => (rec(ctx, l), rec(ctx, r)) match {
+ makeDeclaration(
+ makeNAE( "-", { case List(left, right) => Minus( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), Int32Type )
+ ) ::
+ // case UMinus(e) => rec(ctx, e) match {
+ makeDeclaration(
+ makeNAE( "UMinus", { case List(e) => UMinus( e ) } ),
+ FunctionType( List(Int32Type), Int32Type )
+ ) ::
+ //case Times(l, r) => (rec(ctx, l), rec(ctx, r)) match {
+ makeDeclaration(
+ makeNAE( "*", { case List(left, right) => Times( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), Int32Type )
+ ) ::
+ // case Division(l, r) => (rec(ctx, l), rec(ctx, r)) match {
+ makeDeclaration(
+ makeNAE( "/", { case List(left, right) => Division( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), Int32Type )
+ ) ::
+ // case Modulo(l,r) => (rec(ctx,l), rec(ctx,r)) match {
+ makeDeclaration(
+ makeNAE( "%", { case List(left, right) => Modulo( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), Int32Type )
+ ) :: Nil
+ }
+
+ def getLessThan =
+ // case LessThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
+ makeDeclaration(
+ makeNAE( "<", { case List(left, right) => LessThan( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), BooleanType )
+ )
+
+ def getGreaterThan =
+ // case GreaterThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
+ makeDeclaration(
+ makeNAE( ">", { case List(left, right) => LessThan( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), BooleanType )
+ )
+
+ def getLessEquals =
+ // case LessEquals(l,r) => (rec(ctx,l), rec(ctx,r)) match {
+ makeDeclaration(
+ makeNAE( "<=", { case List(left, right) => LessEquals( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), BooleanType )
+ )
+
+ def getGreaterEquals =
+ // case GreaterEquals(l,r) => (rec(ctx,l), rec(ctx,r)) match {
+ makeDeclaration(
+ makeNAE( ">=", { case List(left, right) => GreaterEquals( left, right ) } ),
+ FunctionType( List(Int32Type, Int32Type), BooleanType )
+ )
+
+ // currently Leon has some troubles with sets
+ def getSetOperations(listOfInstanceTypes: List[LeonType]) = {
+
+ // case SetUnion(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
+ yieldDeclarationForTypes(listOfInstanceTypes) {
+ x: LeonType =>
+ makeDeclaration(
+ makeNAE( "SetUnion", { case List(left, right) => SetUnion( left, right ) } ),
+ FunctionType( List(SetType(x), SetType(x)), SetType(x) )
+ )
+ } ++
+ //case SetIntersection(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
+ yieldDeclarationForTypes(listOfInstanceTypes) {
+ x: LeonType =>
+ makeDeclaration(
+ makeNAE( "SetIntersection", { case List(left, right) => SetIntersection( left, right ) } ),
+ FunctionType( List(SetType(x), SetType(x)), SetType(x) )
+ )
+ } ++
+ //case SetDifference(s1,s2) => (rec(ctx,s1), rec(ctx,s2)) match {
+ yieldDeclarationForTypes(listOfInstanceTypes) {
+ x: LeonType =>
+ makeDeclaration(
+ makeNAE( "SetDifference", { case List(left, right) => SetDifference( left, right ) } ),
+ FunctionType( List(SetType(x), SetType(x)), SetType(x) )
+ )
+ } ++
+ //case ElementOfSet(el,s) => (rec(ctx,el), rec(ctx,s)) match {
+ yieldDeclarationForTypes(listOfInstanceTypes) {
+ x: LeonType =>
+ makeDeclaration(
+ makeNAE( "ElementOfSet", { case List(left, right) => ElementOfSet( left, right ) } ),
+ FunctionType( List(x, SetType(x)), BooleanType )
+ )
+ } ++
+ // case SetCardinality(s) => {
+ yieldDeclarationForTypes(listOfInstanceTypes) {
+ x: LeonType =>
+ makeDeclaration(
+ makeNAE( "SetCardinality", { case List(set) => SetCardinality( set ) } ),
+ FunctionType( List(SetType(x)), Int32Type )
+ )
+ }
+
+ }
+
+ // not covered atm
+// case CaseClass(cd, args) => CaseClass(cd, args.map(rec(ctx, _)))
+// case CaseClassInstanceOf(cd, expr) => {
+// case CaseClassSelector(cd, expr, sel) => {
+
+ // we do not synthesize ifs explicitly
+ //case IfExpr(cond, then, elze) => {
+ def getIfExpr(listOfInstanceTypes: List[LeonType]) = {
+ yieldDeclarationForTypes(listOfInstanceTypes) {
+ x: LeonType =>
+ makeDeclaration(
+ makeNAE( "If", { case List(cond: Expr, then: Expr, elze: Expr) => IfExpr(cond, then, elze) } ),
+ FunctionType( List(BooleanType, x, x), x )
+ )
+ }
+ }
+
+// no arrays atm
+// case f @ ArrayFill(length, default) => {
+// case ArrayLength(a) =>
+// case ArrayUpdated(a, i, v) =>
+// case ArraySelect(a, i) =>
+// case FiniteArray(exprs) =>
+
+ // no maps atm
+// case g @ MapGet(m,k) => (rec(ctx,m), rec(ctx,k)) match {
+// case u @ MapUnion(m1,m2) => (rec(ctx,m1), rec(ctx,m2)) match {
+// case i @ MapIsDefinedAt(m,k) => (rec(ctx,m), rec(ctx,k)) match {
+
+ // needed?
+// case Distinct(args) => {
+
+ // not covered atm
+ // case Tuple(ts) => {
+ // case TupleSelect(t, i) => {
+ // should produce all declarations with tupleselect
+
+ // needed?
+ //case Waypoint(_, arg) => rec(ctx, arg)
+ //case FunctionInvocation(fd, args) => {
+
+ def getLiteralDeclarations = {
+
+ var list = scala.collection.mutable.MutableList[Declaration]()
+
+// case i @ IntLiteral(_) => i
+ list += makeLiteral(
+ IE( "IntLit", IntLiteral(0) ),
+ Int32Type
+ )
+// case b @ BooleanLiteral(_) => b
+ list += makeLiteral(
+ IE( "BoolLit", BooleanLiteral(false) ),
+ BooleanType
+ )
+// case u @ UnitLiteral => u
+ list += makeLiteral(
+ IE( "UnitLit", UnitLiteral ),
+ UnitType
+ )
+
+// case e @ EmptySet(_) => e
+ // NOTE sets are removed in Leon
+// yieldDeclarationForTypes(listOfInstanceTypes) {
+// x: LeonType =>
+// list += makeDeclaration(
+// IE( "SetLit", EmptySet(x) ),
+// SetType(x)
+// )
+// }
+
+ list toList
+ }
+
+ def makeNAE( name: String, fun: List[Expr]=>Expr ): NAE = NAE( name, fun )
+
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/reconstruction/Output.scala b/src/main/scala/insynth/reconstruction/Output.scala
new file mode 100644
index 000000000..fbe07c096
--- /dev/null
+++ b/src/main/scala/insynth/reconstruction/Output.scala
@@ -0,0 +1,12 @@
+package insynth.reconstruction
+
+import insynth.structures.Weight._
+import leon.purescala.Trees.Expr
+
+/**
+ * Encapsulation of the result output from the reconstruction phase, non UI dependent
+ */
+case class Output(snippet: Expr, weight: Weight){
+ def getSnippet = snippet
+ def getWeight = weight
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/reconstruction/Reconstructor.scala b/src/main/scala/insynth/reconstruction/Reconstructor.scala
new file mode 100644
index 000000000..159f399af
--- /dev/null
+++ b/src/main/scala/insynth/reconstruction/Reconstructor.scala
@@ -0,0 +1,53 @@
+package insynth.reconstruction
+
+import insynth.structures.{ SimpleNode, Weight }
+import insynth.reconstruction.intermediate.IntermediateTransformer
+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
+
+/**
+ * Object for reconstruction of proof trees into output(s)
+ */
+object Reconstructor extends ( (SimpleNode, CodeGenerator, Boolean) => Stream[Output]) with HasLogger {
+
+ def apply(tree: SimpleNode, codeGenerator: CodeGenerator, streamOrdered: Boolean = false) = {
+ // logging
+ entering("apply", FormatSuccinctNode(tree, 8).toString)
+
+ // 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))
+
+ // create an ordered/unordered extractor
+ val extractor =
+ if (streamOrdered)
+ new Extractor(new OrderedStreamFactory[LambdaNode])
+ else
+ new Extractor(new UnorderedStreamFactory[LambdaNode])
+
+ // generate streams of lambda trees
+ val extractedTrees = extractor(transformedTree)
+
+ // logging
+ info("extractor phase done")
+ fine("got streamable " + FormatStreamUtils(extractor.transformedStreamable))
+
+ // 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/codegen/CodeGenerator.scala b/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
new file mode 100644
index 000000000..76663ae7a
--- /dev/null
+++ b/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
@@ -0,0 +1,119 @@
+package insynth.reconstruction.codegen
+
+import scala.text.Document
+import scala.text.Document.empty
+
+//import ch.epfl.insynth.reconstruction.intermediate._
+//import ch.epfl.insynth.trees
+//import ch.epfl.insynth.print._
+//import ch.epfl.insynth.reconstruction.combinator.{ NormalDeclaration, AbsDeclaration }
+import insynth.leon.{ LeonDeclaration => DomainDeclaration, _ }
+import insynth.reconstruction.stream._
+
+import insynth.util.format.{ FormatLeonType => FormatDomainType, FormatIntermediate }
+import insynth.util.logging.HasLogger
+
+import leon.purescala.Trees.{ Expr }
+import leon.purescala.TypeTrees.{ TypeTree => DomainType, FunctionType => Function }
+import leon.purescala.{ TypeTrees => domain }
+import leon.purescala.Trees.{ Expr => CodeGenOutput }
+
+/**
+ * class that converts an intermediate tree into a list of output elements (elements
+ * capable of Scala code generation)
+ * should be extended to provide syntax-style variants
+ */
+class CodeGenerator extends (Node => CodeGenOutput) with HasLogger {
+
+ /**
+ * takes the tree and calls the recursive function and maps documents to Output elements
+ * @param tree root of intermediate (sub)tree to transform
+ * @return list of output (code snippet) elements
+ */
+ def apply(tree: Node) = {
+ // match the starting tree to an application that produces query type
+ tree match {
+ case Application(domain.FunctionType(_, _ /* BottomType */), queryDec :: List(innerApp)) =>
+ transform(innerApp)
+ case _ => throw new RuntimeException
+ }
+ }
+
+ /** transform context determines the place of the element to transform */
+ object TransformContext extends Enumeration {
+ type TransformContext = Value
+ // expression, application, parameter, argument (in a function), single parameter
+ val Expr, App, Par, Arg, SinglePar = Value
+ }
+ // import all transform context values
+ import TransformContext._
+
+ /**
+ * main method (recursive) for transforming a intermediate (sub)tree
+ * @param tree root node of the (sub)tree to transform
+ * @return list of documents containing all combinations of available expression for
+ * the given (sub)tree
+ */
+ def transform(tree: Node): CodeGenOutput = {
+ tree match {
+ // variable (declared previously as arguments)
+ case Variable(tpe, name) =>
+ // what to do here
+ throw new RuntimeException
+ // identifier from the scope
+ case Identifier(tpe, DomainDeclaration(_, _, _, im: ImmediateExpression)) =>
+ im()
+ // apply parameters in the tail of params according to the head of params
+ case app@Application(tpe, params) => {
+ // match the application definition term
+ params.head match {
+ case Identifier(_, decl) => {
+ info("Generating application: " + decl + " with params: " + params + " params.size = " + params.size)
+
+ // for an expression of each parameters yield the appropriate transformed expression
+ val paramsExpr: List[CodeGenOutput] = params.tail.map(transform _)
+
+ decl.expression match {
+ // identifier is a function
+ case NaryReconstructionExpression(_, fun) =>
+ info("NaryReconstructionExpression with params: " + paramsExpr + " paramsExpr.size = " + paramsExpr.size)
+ assert(paramsExpr.size >= 1)
+
+ // return application of transformed parameters to fun
+ fun(paramsExpr)
+
+ // identifier is an immediate expression
+ case ImmediateExpression(_, expr) =>
+ assert(paramsExpr.isEmpty)
+ expr
+
+ // identifier is an unary operator
+ case UnaryReconstructionExpression(_, fun) =>
+ assert(paramsExpr.size == 1)
+ fun(paramsExpr.head)
+
+ // this should not happen
+ case _ => throw new RuntimeException
+ }
+ } // case Identifier
+
+ case innerApp@Application(appType: domain.FunctionType, params) =>
+ warning("cannot have app head: " + innerApp + " in application " + app)
+ throw new RuntimeException
+
+ // function that is created as an argument or anything else
+ case /*Identifier(_, _:AbsDeclaration) | */_:Variable | _ =>
+ throw new RuntimeException
+
+ } // params.head match
+ }
+
+ // abstraction first creates all of its arguments
+ case Abstraction(tpe, vars, subtrees) =>
+ assert(vars.size > 0)
+ throw new RuntimeException
+
+ } // tree match
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/ExampleRunner.scala b/src/main/scala/lesynth/ExampleRunner.scala
new file mode 100644
index 000000000..f32f5c6a3
--- /dev/null
+++ b/src/main/scala/lesynth/ExampleRunner.scala
@@ -0,0 +1,130 @@
+package lesynth
+
+import scala.collection.mutable.{ Map => MutableMap }
+import scala.collection.mutable.{ Set => MutableSet }
+import scala.collection.mutable.{ LinkedList => MutableList }
+
+import leon.{ Main => LeonMain, DefaultReporter, Settings, LeonContext }
+import leon.evaluators._
+import leon.solvers.Solver
+import leon.solvers.z3.{ FairZ3Solver }
+import leon.verification.AnalysisPhase
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Trees._
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.TreeOps
+
+import insynth.util.logging.HasLogger
+
+class ExampleRunner(program: Program, maxSteps: Int = 2000) extends HasLogger {
+
+ import TreeOps._
+
+ var counterExamples = MutableList[Map[Identifier, Expr]]()
+
+ val leonEmptyContext = LeonContext()
+
+ // its okay to construct just one, prog is not use in the default evaluator
+ lazy val defaultEvaluator = {
+ val ev = new DefaultEvaluator(leonEmptyContext, program)
+ ev.maxSteps = maxSteps
+ ev
+ }
+
+ def evaluate(expr: Expr, mapping: Map[Identifier, Expr]) = {
+ fine("to evaluate: " + expr + " for mapping: " + mapping)
+ defaultEvaluator.eval(expr, mapping) match {
+ case EvaluationSuccessful(BooleanLiteral(true)) =>
+ fine("Eval succeded: EvaluationSuccessful(true)")
+ true
+ case m =>
+ fine("Eval failed: " + m)
+ false
+ }
+ }
+
+ def evaluateToResult(expr: Expr, mapping: Map[Identifier, Expr]) = {
+ fine("to evaluate: " + expr + " for mapping: " + mapping)
+ defaultEvaluator.eval(expr, mapping)
+ }
+
+ /** filter counterexamples according to an expression (precondition) */
+ def filter(prec: Expr) = {
+ entering("filter(" + prec + ")")
+ fine("Old counterExamples.size: " + counterExamples.size)
+ counterExamples = counterExamples filter {
+ evaluate(prec, _)
+ }
+ fine("New counterExamples.size: " + counterExamples.size)
+ }
+
+ /** count how many examples pass */
+ def countPassed(expressionToCheck: Expr) = {
+ // TODO body dont have set type in synthesizer
+// val expressionToCheck =
+// //Globals.bodyAndPostPlug(exp)
+// {
+// val resFresh = FreshIdentifier("result", true).setType(body.getType)
+// Let(
+// resFresh, body,
+// replace(Map(ResultVariable() -> Variable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition)))
+// }
+ fine("expressionToCheck: " + expressionToCheck)
+
+ (0 /: counterExamples) {
+ (res, ce) =>
+ {
+ if (evaluate(expressionToCheck, ce)) res + 1
+ else res
+ }
+ }
+ }
+
+// def countPassedAndTerminating(body: Expr): Int = {
+// // TODO body dont have set type in synthesizer
+// val expressionToCheck =
+// //Globals.bodyAndPostPlug(exp)
+// {
+// val resFresh = FreshIdentifier("result", true).setType(body.getType)
+// Let(
+// resFresh, body,
+// replace(Map(ResultVariable() -> Variable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition)))
+// }
+// fine("expressionToCheck: " + expressionToCheck)
+//
+// (0 /: counterExamples) {
+// (res, ce) =>
+// {
+// evaluateToResult(expressionToCheck, ce) match {
+// case EvaluationSuccessful(BooleanLiteral(true)) =>
+// res + 1
+// case EvaluationError("Stack overflow") =>
+// return -counterExamples.size
+// case m =>
+// res
+// }
+// }
+// }
+// }
+
+ // check if this body passes all examples
+// def check(body: Expr): Boolean = {
+// val examplesToCheck = counterExamples
+// val expressionToCheck = Globals.bodyAndPostPlug(body)
+// fine("Expression to check: " + expressionToCheck)
+//
+// var res = true
+// val iterator = counterExamples.iterator
+//
+// while (res && iterator.hasNext) {
+// val currentExample = iterator.next
+// res = evaluate(expressionToCheck, currentExample)
+//
+// if (!res) fine("Failed example: " + currentExample)
+// }
+//
+// return res
+// }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/Globals.scala b/src/main/scala/lesynth/Globals.scala
new file mode 100644
index 000000000..a42136a79
--- /dev/null
+++ b/src/main/scala/lesynth/Globals.scala
@@ -0,0 +1,22 @@
+package lesynth
+
+import leon.purescala.Common.Identifier
+import leon.purescala.Definitions.{ Program, FunDef }
+import leon.purescala.Trees.{ Expr, Error, Hole }
+
+object Globals {
+
+ //var bodyAndPostPlug: (Expr => Expr) = _
+
+ //var timeout = 2
+
+ var allSolved: Option[Boolean] = None
+
+// var program: Option[Program] = None
+//
+ var hole: Hole = _
+//
+ var asMap: Map[Identifier, Expr] = _
+//
+// var holeFunDef: FunDef = _
+}
diff --git a/src/main/scala/lesynth/InputExamples.scala b/src/main/scala/lesynth/InputExamples.scala
new file mode 100755
index 000000000..00fa92c27
--- /dev/null
+++ b/src/main/scala/lesynth/InputExamples.scala
@@ -0,0 +1,148 @@
+package lesynth
+
+import leon.{ Main => LeonMain, Reporter, DefaultReporter, SilentReporter, Settings, LeonContext }
+import leon.solvers.{ Solver, TimeoutSolver }
+import leon.solvers.z3.{ FairZ3Solver }
+import leon.verification.AnalysisPhase
+import leon.plugin.ExtractionPhase
+import leon.purescala.TypeTrees.{ ClassType, CaseClassType, Int32Type }
+import leon.purescala.Trees.{ IntLiteral, CaseClass }
+import leon.purescala.Definitions.{ FunDef, VarDecls }
+import leon.purescala.Common.Identifier
+
+import insynth.leon.loader.{ HoleExtractor, LeonLoader }
+
+object InputExamples {
+
+ def getInputExamples(argumentIds: Seq[Identifier], loader: LeonLoader) = {
+ argumentIds match {
+ case singleArgument :: Nil if isList(singleArgument) =>
+ introduceOneListArgumentExamples(argumentIds, loader)
+ case first :: second :: Nil if isList(first) && isList(second) =>
+ introduceTwoListArgumentsExamples(argumentIds, loader)
+ case first :: second :: Nil if isInt(first) && isList(second) =>
+ introduceExamplesIntList(argumentIds, loader)
+ case _ => null
+ }
+ }
+
+ def introduceExamplesIntList(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = {
+
+ // list type
+ val ct = argumentIds(1).getType.asInstanceOf[ClassType]
+
+ val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
+
+ val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
+
+ val nilClass = nilClassSet.head
+ val consClass = consClassSet.head
+
+ var counter = 10
+ def getIntLiteral = { counter+=1; IntLiteral(counter) }
+ val intLiteral = IntLiteral(5)
+
+ val list0 = CaseClass(nilClass, Nil)
+ val list1 = CaseClass(consClass, IntLiteral(10) :: list0 :: Nil)
+ val list32 = CaseClass(consClass, IntLiteral(5) :: CaseClass(consClass, IntLiteral(7) :: list1 :: Nil) :: Nil)
+
+ Map(argumentIds(0) -> IntLiteral(3), argumentIds(1) -> list32) ::
+ Map(argumentIds(0) -> IntLiteral(2), argumentIds(1) -> list32) ::
+ Map(argumentIds(0) -> IntLiteral(3), argumentIds(1) -> list0) ::
+ Map(argumentIds(0) -> IntLiteral(2), argumentIds(1) -> list0) ::
+ Map(argumentIds(0) -> IntLiteral(6), argumentIds(1) -> list32) ::
+ Map(argumentIds(0) -> IntLiteral(9), argumentIds(1) -> list32) ::
+ Nil
+ }
+
+ def introduceOneListArgumentExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = {
+
+ // list type
+ val ct = argumentIds(0).getType.asInstanceOf[ClassType]
+
+ val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
+
+ val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
+
+ val nilClass = nilClassSet.head
+ val consClass = consClassSet.head
+
+ var counter = 10
+ def getIntLiteral = { counter+=1; IntLiteral(counter) }
+ val intLiteral = IntLiteral(5)
+
+ val list0 = CaseClass(nilClass, Nil)
+ val list1 = CaseClass(consClass, IntLiteral(10) :: list0 :: Nil)
+ val list2s = CaseClass(consClass, IntLiteral(5) :: list1 :: Nil)
+ val list2u = CaseClass(consClass, IntLiteral(5) :: list1 :: Nil)
+ val list3s = CaseClass(consClass, IntLiteral(5) :: list2s :: Nil)
+ val list3u1 = CaseClass(consClass, IntLiteral(5) :: list2u :: Nil)
+ val list3u2 = CaseClass(consClass, IntLiteral(15) :: list2s :: Nil)
+ val list3u3 = CaseClass(consClass, IntLiteral(15) :: list2u :: Nil)
+
+ for (list <- List(list0, list1, list2s, list2u, list3s, list3u1, list3u2, list3u3))
+ yield Map(argumentIds(0) -> list)
+ }
+
+ def introduceTwoListArgumentsExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = {
+
+ loader.hole.getType match {
+ case ct: ClassType =>
+ val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
+
+ val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
+
+ val nilClass = nilClassSet.head
+ val consClass = consClassSet.head
+
+ var counter = 0
+ def getIntLiteral = { counter+=1; IntLiteral(counter) }
+
+ val list0 = () => CaseClass(nilClass, Nil)
+ val list1 = () => CaseClass(consClass, getIntLiteral :: list0() :: Nil)
+ val list2 = () => CaseClass(consClass, getIntLiteral :: list1() :: Nil)
+ val list3 = () => CaseClass(consClass, getIntLiteral :: list2() :: Nil)
+ val list4 = () => CaseClass(consClass, getIntLiteral :: list3() :: Nil)
+
+ val lists = List(list0, list1, list2, list3/*, list4*/)
+
+ for(l1 <- lists; l2 <- lists)
+ yield Map(argumentIds(0) -> l1(), argumentIds(1) -> l2())
+
+ case _ =>
+ null
+ }
+ }
+
+ def isList(id: Identifier) = id.getType.toString == "List"
+ def isInt(id: Identifier) = id.getType == Int32Type
+
+// def introduceOneListArgumentExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = {
+//
+// // list type
+// val ct = argumentIds(0).getType.asInstanceOf[ClassType]
+//
+// val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
+//
+// val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
+//
+// val nilClass = nilClassSet.head
+// val consClass = consClassSet.head
+//
+// var counter = 10
+// def getIntLiteral = { counter+=1; IntLiteral(counter) }
+// val intLiteral = IntLiteral(5)
+//
+// val list0 = CaseClass(nilClass, Nil)
+// val list1 = CaseClass(consClass, IntLiteral(5) :: list0 :: Nil)
+// val list2 = CaseClass(consClass, IntLiteral(3) :: list1 :: Nil)
+// val list3 = CaseClass(consClass, IntLiteral(1) :: list2 :: Nil)
+// val list32 = CaseClass(consClass, IntLiteral(10) :: CaseClass(consClass, IntLiteral(7) :: list1 :: Nil) :: Nil)
+//
+// val lists = List(list0, list1, list2, list3, list32)
+//
+// for(l1 <- lists)
+// yield Map(argumentIds(0) -> l1)
+//
+// }
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/Refiner.scala b/src/main/scala/lesynth/Refiner.scala
new file mode 100755
index 000000000..c5dda1dbd
--- /dev/null
+++ b/src/main/scala/lesynth/Refiner.scala
@@ -0,0 +1,98 @@
+package lesynth
+
+import leon.purescala.Trees._
+import leon.purescala.Definitions.{ Program, VarDecl, FunDef, VarDecls }
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.TreeOps
+import leon.plugin.ExtractionPhase
+
+import insynth.leon.loader.LeonLoader
+
+import insynth.util.logging.HasLogger
+
+class Refiner(program: Program, hole: Hole, holeFunDef: FunDef) extends HasLogger {
+ import Globals._
+
+ def isAvoidable(expr: Expr, funDefArgs: List[Identifier]) = {
+ fine(
+ "Results for refining " + expr + ", are: " +
+ " ,recurentExpression == expr " + (recurentExpression == expr) +
+ " ,isCallAvoidableBySize(expr) " + isCallAvoidableBySize(expr, funDefArgs) +
+ " ,hasDoubleRecursion(expr) " + hasDoubleRecursion(expr)
+ )
+ recurentExpression == expr || isCallAvoidableBySize(expr, funDefArgs) || hasDoubleRecursion(expr)
+ }
+
+ //val holeFunDef = Globals.holeFunDef
+
+ val recurentExpression: Expr =
+ if (holeFunDef.hasBody) {
+ FunctionInvocation(holeFunDef, holeFunDef.args map { varDecl => Variable(varDecl.id) })
+ } else
+ Error("Hole FunDef should have a body")
+
+ // check according to size
+ // true - YES, false - NO or don't know
+ // basically a lexicographic (well-founded) ordering
+ def isCallAvoidableBySize(expr: Expr, funDefArgs: List[Identifier]) = {
+
+ def isBadInvocation(expr2: Expr) = expr2 match {
+ case FunctionInvocation(`holeFunDef`, args) =>
+ (0 /: (args zip holeFunDef.args.map(_.id))) {
+ case (res, (arg, par)) if res == 0 => isLess(arg, par)
+ case (res, _) => res
+ } >= 0
+ case _ => false
+ }
+
+ import TreeOps.treeCatamorphism
+
+ treeCatamorphism(
+ isBadInvocation,
+ (b1: Boolean, b2: Boolean) => b1 || b2,
+ (t: Expr, b: Boolean) => b || isBadInvocation(t),
+ expr
+ )
+ }
+
+ def isLess(arg: Expr, variable: Identifier): Int = {
+ def getSize(arg: Expr, size: Int): Int = arg match {
+ //case FunctionInvocation(_, args) => -1 // if some random calls are involved
+ case CaseClassSelector(cas, expr, fieldId) if fieldId.name == "tail" => getSize(expr, size - 1)
+ case CaseClassSelector(cas, expr, fieldId) if fieldId.name == "head" => size + 1
+ case CaseClass(caseClassDef, head :: tail :: Nil) => getSize(tail, size + 1)
+ case CaseClass(caseClassDef, Nil) => 1
+ case v: Variable => if (v.id == variable) size else {
+ fine("variable IDs do not match: " + v.id.uniqueName + " and " + variable.uniqueName )
+ 1
+ }
+ case _ => //throw new RuntimeException("Could not match " + arg + " in getSize")
+ -1
+ }
+
+ getSize(arg, 0)
+ }
+
+ def hasDoubleRecursion(expr: Expr) = {
+ var found = false
+
+ def findRecursion(expr: Expr) = expr match {
+ case FunctionInvocation(`holeFunDef`, args) => true
+ case _ => false
+ }
+
+ def findRecursionInCall(expr: Expr, b: Boolean) = expr match {
+ case FunctionInvocation(`holeFunDef`, args) =>
+ if (b) found = true
+ true
+ case _ => b
+ }
+
+ import TreeOps.treeCatamorphism
+
+ treeCatamorphism(findRecursion, (b1: Boolean, b2: Boolean) => b1 || b2, findRecursionInCall, expr)
+
+ found
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/Report.scala b/src/main/scala/lesynth/Report.scala
new file mode 100755
index 000000000..993a9f862
--- /dev/null
+++ b/src/main/scala/lesynth/Report.scala
@@ -0,0 +1,60 @@
+package lesynth
+
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+
+trait Report {
+ def summaryString: String
+
+ def isSuccess: Boolean
+}
+
+case object EmptyReport extends Report {
+ import Report._
+
+ implicit val width = 70
+
+ override def summaryString =
+ infoHeader +
+ ("║ %-" + width + "s ║\n").format("No solution found for this synthesis problem.") +
+ infoFooter
+
+ override def isSuccess = false
+}
+
+case class FullReport(val function: FunDef, val totalTime: Long/*, innerVerificationReport */) extends Report {
+
+ import Report._
+
+ implicit val width = 70
+
+ override def summaryString : String = {
+ infoHeader +
+ function.toString.split("\n").map {
+ ("║ %-" + (width - 2) + "s ║\n").format(_)
+ }.mkString +
+ infoSep +
+ ("║ Total time: %" + (width - 15) + ".2fs ║\n").format(totalTime.toDouble/1000) +
+ infoFooter
+ }
+
+ override def isSuccess = true
+}
+
+object Report {
+ //def emptyReport : Report = new Report(Nil)
+
+ def fit(str : String, maxLength : Int) : String = {
+ if(str.length <= maxLength) {
+ str
+ } else {
+ str.substring(0, maxLength - 1) + "…"
+ }
+ }
+
+ def infoSep(implicit width: Int) : String = "╟" + ("┄" * width) + "╢\n"
+ def infoFooter(implicit width: Int) : String = "╚" + ("═" * width) + "╝"
+ def infoHeader(implicit width: Int) : String = ". ┌─────────┐\n" +
+ "╔═╡ Summary ╞" + ("═" * (width - 12)) + "╗\n" +
+ "║ └─────────┘" + (" " * (width - 12)) + "║\n"
+
+}
diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/lesynth/SynthesizerExamples.scala
new file mode 100755
index 000000000..39cdcde6c
--- /dev/null
+++ b/src/main/scala/lesynth/SynthesizerExamples.scala
@@ -0,0 +1,725 @@
+package lesynth
+
+import scala.collection.mutable.{ Map => MutableMap }
+import scala.collection.mutable.{ Set => MutableSet }
+import scala.collection.mutable.PriorityQueue
+
+import leon.{Reporter, DefaultReporter, SilentReporter, LeonContext}
+import leon.solvers.{ Solver, TimeoutSolver }
+import leon.solvers.z3.{ FairZ3Solver }
+import leon.verification.AnalysisPhase
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Trees.{ Variable => LeonVariable, _ }
+import leon.purescala.Definitions.{FunDef, Program}
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.TreeOps
+
+import insynth.util.logging.HasLogger
+import insynth.interfaces.Declaration
+import insynth.InSynth
+import insynth.leon.loader.LeonLoader
+import insynth.leon.LeonDeclaration
+import insynth.leon.ImmediateExpression
+import insynth.engine.InitialEnvironmentBuilder
+import insynth.interfaces.Declaration
+import insynth.engine.InitialEnvironmentBuilder
+import insynth.leon.TypeTransformer
+import insynth.reconstruction.Output
+import leon.synthesis.Problem
+import leon.Main.processOptions
+import leon.purescala.TypeTrees._
+
+import scala.collection.mutable.{Map => MutableMap}
+import scala.collection.mutable.{Set => MutableSet}
+import scala.util.control.Breaks.break
+import scala.util.control.Breaks.breakable
+
+class SynthesizerForRuleExamples(
+ // some synthesis instance information
+ val solver: Solver,
+ val program: Program,
+ val desiredType: LeonType,
+ val holeFunDef: FunDef,
+ val problem: Problem,
+ val freshResVar: LeonVariable,
+ // number of condition expressions to try before giving up on that branch expression
+ numberOfBooleanSnippets: Int = 5,
+ numberOfCounterExamplesToGenerate: Int = 5,
+ leonTimeout: Int = 2, // seconds
+ analyzeSynthesizedFunctionOnly: Boolean = false,
+ showLeonOutput: Boolean = false,
+ reporter: Reporter = new DefaultReporter,
+ //examples: List[Map[Identifier, Expr]] = Nil,
+ // we need the holeDef to know the right ids
+ introduceExamples: ((Seq[Identifier], LeonLoader) => List[Map[Identifier, Expr]]) = { (_, _) => Nil },
+ collectCounterExamplesFromLeon: Boolean = false,
+ filterOutAlreadySeenBranchExpressions: Boolean = true,
+ useStringSetForFilterOutAlreadySeenBranchExpressions: Boolean = true,
+ numberOfTestsInIteration: Int = 50,
+ numberOfCheckInIteration: Int = 5
+) extends HasLogger {
+
+ val fileName: String = "noFileName"
+
+ info("Synthesizer:")
+ info("fileName: %s".format(fileName))
+ info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
+ info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
+ info("leonTimeout: %d".format(leonTimeout))
+ //info("examples: " + examples.mkString(", "))
+
+ info("holeFunDef: %s".format(holeFunDef))
+ info("problem: %s".format(problem.toString))
+
+ private var hole: Hole = _
+ // initial declarations
+ private var allDeclarations: List[Declaration] = _
+ // objects used in the synthesis
+ private var loader: LeonLoader = _
+ private var inSynth: InSynth = _
+ private var inSynthBoolean: InSynth = _
+ private var refiner: Refiner = _
+ //private var solver: Solver = _
+ private var ctx: LeonContext = _
+ private var initialPrecondition: Expr = _
+ private var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = _
+ // can be used to unnecessary syntheses
+ private var variableRefinedBranch = false
+ private var variableRefinedCondition = true // assure initial synthesis
+ private var booleanExpressionsSaved: Stream[Output] = _
+
+ private var seenBranchExpressions: Set[String] = Set.empty
+
+ // flag denoting if a correct body has been synthesized
+ private var found = false
+
+ // accumulate precondition for the remaining branch to synthesize
+ private var accumulatingPrecondition: Expr = _
+ // accumulate the final expression of the hole
+ private var accumulatingExpression: Expr => Expr = _
+ //private var accumulatingExpressionMatch: Expr => Expr = _
+
+ // time
+ var startTime: Long = _
+ var verTime: Long = 0
+ var synTime: Long = 0
+
+ // filtering/ranking with examples support
+ var exampleRunner: ExampleRunner = _
+
+ def analyzeProgram = {
+
+ val temp = System.currentTimeMillis
+ Globals.allSolved = Some(true)
+
+ import TreeOps._
+
+ val body = holeFunDef.getBody
+ val theExpr = {
+ val resFresh = FreshIdentifier("result", true).setType(body.getType)
+ val bodyAndPost =
+ Let(
+ resFresh, body,
+ replace(Map(ResultVariable() -> LeonVariable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition))
+ )
+
+ val withPrec = if( holeFunDef.precondition.isEmpty) {
+ bodyAndPost
+ } else {
+ Implies(matchToIfThenElse(holeFunDef.precondition.get), bodyAndPost)
+ }
+
+ withPrec
+ }
+
+ Globals.allSolved = solver.solve(theExpr)
+ fine("solver said " + Globals.allSolved + " for " + theExpr)
+ //interactivePause
+
+ val time = System.currentTimeMillis - temp
+ //fine("Analysis took: " + time + ", from report: " + report.totalTime)
+
+ // accumulate
+ verTime += time
+ }
+
+ // TODO return boolean (do not do unecessary analyze)
+ def generateCounterexamples(program: Program, funDef: FunDef, number: Int): (Seq[Map[Identifier, Expr]], Expr) = {
+
+ fine("generate counter examples with funDef.prec= " + funDef.precondition.getOrElse(BooleanLiteral(true)))
+ val temp = System.currentTimeMillis
+
+ // get current precondition
+ var precondition = funDef.precondition.getOrElse(BooleanLiteral(true))
+ // where we will accumulate counterexamples as sequence of maps
+ var maps: Seq[Map[Identifier, Expr]] = Seq.empty
+
+ // iterate specific number of times or until no further counterexample can be generated
+ var changed = true
+ var ind = 0
+ while (ind < number && changed) {
+
+ // analyze the program
+ analyzeProgram
+
+ // check if solver could solved this instance
+ if (Globals.allSolved == Some(false) && !Globals.asMap.isEmpty) {
+
+ fine("found coounterexample: " + Globals.asMap)
+ // add current counterexample
+ maps :+= Globals.asMap
+
+ // prevent this counterexample to re-occur
+ val precAddition = Not(And(Globals.asMap map { case (id, value) => Equals(LeonVariable(id), value) } toSeq))
+ precondition = And(Seq(precondition, precAddition))
+ // update precondition
+ funDef.precondition = Some(precondition)
+ } else
+ changed = false
+
+ ind += 1
+ }
+
+ val temptime = System.currentTimeMillis - temp
+ fine("Generation of counter-examples took: " + temptime)
+ verTime += temptime
+
+ // return found counterexamples and the formed precondition
+ (maps, precondition)
+ }
+
+ def getCurrentBuilder = new InitialEnvironmentBuilder(allDeclarations)
+
+ def synthesizeBranchExpressions =
+ inSynth.getExpressions(getCurrentBuilder)
+
+ def synthesizeBooleanExpressions = {
+ if ( variableRefinedCondition ) {
+ // store for later fetch (will memoize values)
+ booleanExpressionsSaved =
+ inSynthBoolean.getExpressions(getCurrentBuilder) take numberOfBooleanSnippets
+ // reset flag
+ variableRefinedCondition = false
+ }
+
+ booleanExpressionsSaved
+ }
+
+ def interactivePause = {
+ System.out.println("Press Any Key To Continue...");
+ new java.util.Scanner(System.in).nextLine();
+ }
+
+ def getNewExampleQueue = PriorityQueue[(Expr, Int)]()(
+ new Ordering[(Expr, Int)] {
+ def compare(pair1: (Expr, Int), pair2: (Expr, Int)) =
+ pair1._2.compare(pair2._2)
+ })
+
+ def initialize = {
+
+ hole = Hole(desiredType)
+
+ // TODO lose this - globals are bad
+ Globals.allSolved = None
+
+ // context needed for verification
+ import leon.Main._
+// val reporter =
+// if (showLeonOutput) new DefaultReporter
+// else new SilentReporter
+//
+// val args =
+// if (analyzeSynthesizedFunctionOnly)
+// Array(fileName, "--timeout=" + leonTimeout, "--functions=" + holeFunDef.id.name)
+// else
+// Array(fileName, "--timeout=" + leonTimeout)
+// info("Leon context array: " + args.mkString(","))
+// ctx = processOptions(reporter, args.toList)
+
+ //solver = //new FairZ3Solver(ctx)
+ // new TimeoutSolver(new FairZ3Solver(ctx), leonTimeout)
+
+ // create new insynth object
+ loader = new LeonLoader(program, hole, problem.as, false)
+ inSynth = new InSynth(loader, true)
+ // save all declarations seen
+ allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+ // make conditions synthesizer
+ inSynthBoolean = new InSynth(allDeclarations, BooleanType, true)
+
+ // funDef of the hole
+ fine("postcondition is: " + holeFunDef.getPostcondition)
+
+ // accumulate precondition for the remaining branch to synthesize
+ accumulatingPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+ // save initial precondition
+ initialPrecondition = accumulatingPrecondition
+ // accumulate the final expression of the hole
+ accumulatingExpression = (finalExp: Expr) => finalExp
+ //accumulatingExpressionMatch = accumulatingExpression
+
+ // each variable of super type can actually have a subtype
+ // get sine declaration maps to be able to refine them
+ val directSubclassMap = loader.directSubclassesMap
+ val variableDeclarations = loader.variableDeclarations
+ // map from identifier into a set of possible subclasses
+ variableRefinements = MutableMap.empty
+ for (varDec <- variableDeclarations) {
+ varDec match {
+ case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, LeonVariable(id))) =>
+ variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
+ case _ =>
+ }
+ }
+
+ // calculate cases that should not happen
+ refiner = new Refiner(program, hole, holeFunDef)
+ fine("Refiner initialized. Recursive call: " + refiner.recurentExpression)
+
+ exampleRunner = new ExampleRunner(program)
+ exampleRunner.counterExamples ++= //examples
+ introduceExamples(holeFunDef.args.map(_.id), loader)
+
+ fine("Introduced examples: " + exampleRunner.counterExamples.mkString(", "))
+ }
+
+ def countPassedExamples(snippet: Expr) = {
+ val oldPreconditionSaved = holeFunDef.precondition
+ val oldBodySaved = holeFunDef.body
+
+ // restore initial precondition
+ holeFunDef.precondition = Some(initialPrecondition)
+
+ // get the whole body (if else...)
+ val accumulatedExpression = accumulatingExpression(snippet)
+ // set appropriate body to the function for the correct evaluation
+ holeFunDef.body = Some(accumulatedExpression)
+
+
+ import TreeOps._
+ val expressionToCheck =
+ //Globals.bodyAndPostPlug(exp)
+ {
+ val resFresh = FreshIdentifier("result", true).setType(accumulatedExpression.getType)
+ Let(
+ resFresh, accumulatedExpression,
+ replace(Map(ResultVariable() -> LeonVariable(resFresh)), matchToIfThenElse(holeFunDef.getPostcondition)))
+ }
+
+ fine("going to count passed for: " + holeFunDef)
+ fine("going to count passed for: " + expressionToCheck)
+
+ val count = exampleRunner.countPassed(expressionToCheck)
+// if (snippet.toString == "Cons(l1.head, concat(l1.tail, l2))")
+// interactivePause
+
+ holeFunDef.precondition = oldPreconditionSaved
+ holeFunDef.body = oldBodySaved
+
+ count
+ }
+
+ def synthesize: Report = {
+ reporter.info("Synthesis called on file: " + fileName)
+
+ // get start time
+ startTime = System.currentTimeMillis
+
+ reporter.info("Initializing synthesizer: ")
+ reporter.info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
+ reporter.info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
+ reporter.info("leonTimeout: %d".format(leonTimeout))
+ initialize
+ reporter.info("Synthesizer initialized")
+
+ // keeps status of validity
+ var keepGoing = Globals.allSolved match {
+ case Some(true) => false
+ case _ => true
+ }
+
+ // initial snippets (will update in the loop)
+ var snippets = synthesizeBranchExpressions
+ var snippetsIterator = snippets.iterator
+
+ // ordering of expressions according to passed examples
+ var pq = getNewExampleQueue
+
+ // iterate while the program is not valid
+ import scala.util.control.Breaks._
+ var iteration = 0
+ breakable {
+ while (keepGoing) {
+ // next iteration
+ iteration += 1
+ reporter.info("####################################")
+ reporter.info("######Iteration #" + iteration + " ###############")
+ reporter.info("####################################")
+ reporter.info("# precondition is: " + holeFunDef.precondition.getOrElse(BooleanLiteral(true)))
+ reporter.info("# accumulatingPrecondition is: " + accumulatingPrecondition)
+ reporter.info("# accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
+ reporter.info("####################################")
+
+ var numberOfTested = 0
+
+ // just printing of expressions and pass counts
+ fine( {
+ val (it1, it2) = snippetsIterator.duplicate // we are dealing with iterators, need to duplicate
+ val logString = ((it1 zip Iterator.range(0, numberOfTestsInIteration)) map {
+ case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet +
+ " pass count is " + countPassedExamples(snippet.getSnippet)
+ }).mkString("\n")
+ snippetsIterator = it2
+ logString
+ })
+ //interactivePause
+
+ reporter.info("Going into a enumeration/testing phase.")
+ fine("evaluating examples: " + exampleRunner.counterExamples.mkString("\n"))
+
+ // found precondition?
+ found = false
+ // try to find it
+ breakable {
+ // go through all snippets
+ for (
+ snippet <- snippetsIterator; val snippetTree = snippet.getSnippet;
+ // filter if seen
+ if ! (seenBranchExpressions contains snippetTree.toString)
+ ) {
+ finest("snippetTree is: " + snippetTree)
+ // note that we do not add snippets to the set of seen if enqueued
+
+ // skip avoidable calls
+ if (!refiner.isAvoidable(snippetTree, problem.as)) {
+
+ // passed example pairs
+ val passCount = countPassedExamples(snippetTree)
+
+ if (passCount == exampleRunner.counterExamples.size) {
+ info("All examples passed. Testing snippet " + snippetTree + " right away")
+
+ if (tryToSynthesizeBranch(snippetTree)) {
+ // will set found if correct body is found
+ break
+ }
+ } else {
+ if (passCount > 0) {
+ finest("Snippet with pass count goes into queue: " + (snippetTree, passCount))
+ pq.enqueue((snippetTree, 100 + (passCount * iteration) - snippet.getWeight.toInt))
+ }
+ else {
+ fine("Snippet with pass count was dropped: " + (snippetTree, passCount) +
+ " while number of examples was: " + exampleRunner.counterExamples.size)
+ // add to seen if branch was not found for it
+ seenBranchExpressions += snippetTree.toString
+ }
+ }
+
+ } else {
+ fine("Refiner filtered this snippet: " + snippetTree)
+ seenBranchExpressions += snippetTree.toString
+ } // if (!refiner.isAvoidable(snippetTree)) {
+
+ // check if we this makes one test iteration
+ if (numberOfTested >= numberOfTestsInIteration) {
+ reporter.info("Finalizing enumeration/testing phase.")
+ fine("Queue contents: " + pq.toList.take(10).mkString("\n"))
+ fine({ if (pq.isEmpty) "queue is empty" else "head of queue is: " + pq.head })
+
+ //interactivePause
+ // go and check the topmost numberOfCheckInIteration
+ for (i <- 1 to math.min(numberOfCheckInIteration, pq.size)) {
+ val nextSnippet = pq.dequeue._1
+ fine("dequeued nextSnippet: " + nextSnippet)
+ //interactivePause
+
+ if (tryToSynthesizeBranch(nextSnippet)) {
+ break
+ }
+
+ // dont drop snippets that were on top of queue (they may be good for else ... part)
+ //seenBranchExpressions += nextSnippet.toString
+ }
+
+ numberOfTested = 0
+ } else
+ numberOfTested += 1
+
+ } // for (snippet <- snippets
+ } // breakable { for (snippet <- snippets
+
+ // if did not found for any of the branch expressions
+ if (found) {
+ val endTime = System.currentTimeMillis
+ reporter.info("We are done, in time: " + (endTime - startTime))
+ return new FullReport(holeFunDef, (endTime - startTime))
+ }
+
+ if ( variableRefinedBranch ) {
+ fine("Variable refined, doing branch synthesis again")
+ // get new snippets
+ snippets = synthesizeBranchExpressions
+ snippetsIterator = snippets.iterator
+ pq = getNewExampleQueue
+
+ // reset flag
+ variableRefinedBranch = false
+ } else
+ // reseting iterator needed because we may have some expressions that previously did not work
+ snippetsIterator = snippets.iterator
+
+ fine("filtering based on: " + holeFunDef.precondition.get)
+ fine("counterexamples before filter: " + exampleRunner.counterExamples.size)
+ exampleRunner.filter(holeFunDef.precondition.get)
+ fine("counterexamples after filter: " + exampleRunner.counterExamples.size)
+ fine("counterexamples after filter: " + exampleRunner.counterExamples.mkString("\n"))
+ }
+ } //breakable { while (!keepGoing) {
+
+ EmptyReport
+ }
+
+ def tryToSynthesizeBranch(snippetTree: Expr): Boolean = {
+ // replace hole in the body with the whole if-then-else structure, with current snippet tree
+ val oldBody = holeFunDef.getBody
+ val newBody = accumulatingExpression(snippetTree)
+ holeFunDef.body = Some(newBody)
+
+ // precondition
+ val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+ holeFunDef.precondition = Some(initialPrecondition)
+
+ snippetTree.setType(hole.desiredType)
+ //holeFunDef.getBody.setType(hole.desiredType)
+
+ // TODO spare one analyzing step
+ // analyze the program
+ fine("analyzing program for funDef:" + holeFunDef)
+ analyzeProgram
+
+ // check if solver could solved this instance
+ if (Globals.allSolved == Some(true)) {
+ // mark the branch found
+ found = true
+
+ reporter.info("Wooooooow we have a winner!")
+ reporter.info("************************************")
+ reporter.info("*********And the winner is**********")
+ reporter.info(accumulatingExpression(snippetTree).toString)
+ reporter.info("************************************")
+
+ return true
+ }
+
+ // store appropriate values here, will be update in a finally branch
+ var bodyToRestore = oldBody
+ var preconditionToRestore = Some(oldPrecondition)
+
+ // because first initial test
+ holeFunDef.precondition = preconditionToRestore
+
+ // get counterexamples
+ fine("Going to generating counterexamples: " + holeFunDef)
+ val (maps, precondition) = generateCounterexamples(program, holeFunDef, numberOfCounterExamplesToGenerate)
+
+ // collect (add) counterexamples from leon
+ if (collectCounterExamplesFromLeon)
+ exampleRunner.counterExamples ++= maps
+
+ // this should not be possible
+ // val keepGoing = Globals.allSolved match {
+ // case Some(true) => false
+ // case _ => true
+ // }
+ //
+ // // if no counterexamples and all are solved, we are done
+ // if (maps.isEmpty && !keepGoing) {
+ // // mark the branch found
+ // found = true
+ //
+ // println("Wooooooow we have a winner!")
+ // println("************************************")
+ // println("*********And the winner is**********")
+ // println(accumulatingExpression(snippetTree))
+ // println("************************************")
+ //
+ // return true
+ // }
+
+ //if(maps.isEmpty) throw new RuntimeException("asdasdasd")
+
+ // will modify funDef body and precondition, restore it later
+ try {
+ if (!maps.isEmpty) {
+ // proceed with synthesizing boolean expressions
+ //solver.setProgram(program)
+
+ // reconstruct (only defined number of boolean expressions)
+ val innerSnippets = synthesizeBooleanExpressions
+ // just printing of expressions
+ fine(
+ ((innerSnippets zip Iterator.range(0, numberOfBooleanSnippets).toStream) map {
+ case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet
+ }).mkString("\n"))
+
+ for (
+ innerSnippetTree <- innerSnippets map { _.getSnippet };
+ if (
+ { val flag = !refiner.isAvoidable(innerSnippetTree, problem.as)
+ if (!flag) fine("Refiner filtered this snippet: " + innerSnippetTree)
+ flag }
+ )
+ ) {
+ fine("boolean snippet is: " + innerSnippetTree)
+
+ val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, precondition)
+
+ // if precondition found
+ if (innerFound) {
+ reporter.info("Precondition " + innerPrec + " found for " + snippetTree)
+
+ innerPrec match {
+ case s @ Some(_) =>
+ // new precondition (restore in finally)
+ preconditionToRestore = s
+ case _ =>
+ }
+ return true
+ }
+
+ } // iterating over all boolean solutions
+
+ reporter.info("No precondition found for branch expression: " + snippetTree)
+ return false
+
+ } // if ( !maps.isEmpty ) {
+ // no counter examples, we just say that we cannot do anything
+ false
+ } // try
+ finally {
+ // set these to the FunDef
+ holeFunDef.precondition = preconditionToRestore
+ // restore old body (we accumulate expression)
+ holeFunDef.body = Some(oldBody)
+ }
+ }
+
+ def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: Expr): (Boolean, Option[Expr]) = {
+
+ // new condition together with existing precondition
+ val newCondition = And(Seq(accumulatingPrecondition, innerSnippetTree))
+
+ // new expression should not be false
+ val notFalseEquivalence = Not(newCondition)
+ val notFalseSolveReturn = solver.solve(notFalseEquivalence)
+ fine("solve for not false returned: " + notFalseSolveReturn)
+
+ notFalseSolveReturn match {
+ case Some(true) =>
+ (false, None)
+ case None =>
+ (false, None)
+ // nothing here
+ // here, our expression is not contradictory, continue
+ case Some(false) =>
+ // check if synthesized boolean expression implies precondition (counterexamples)
+ val implyExpression = Implies(newCondition, precondition)
+ fine("implyExpression is: " + implyExpression)
+
+ // check if synthesized condition implies counter-examples
+ val solveReturn = solver.solve(implyExpression)
+ fine("solve returned: " + solveReturn)
+
+ solveReturn match {
+ case Some(true) =>
+ // if expression implies counterexamples add it to the precondition and try to validate program
+ holeFunDef.precondition = Some(newCondition)
+ // do analysis
+ analyzeProgram
+ // program is valid, we have a branch
+ if (Globals.allSolved == Some(true)) {
+ // we found a branch
+ reporter.info("We found a branch, for expression %s, with condition %s.".format(snippetTree, innerSnippetTree))
+
+ // update accumulating expression
+ val oldAccumulatingExpression = accumulatingExpression
+ val newAccumulatingExpression =
+ (finalExpr: Expr) =>
+ oldAccumulatingExpression({
+ val innerIf = IfExpr(innerSnippetTree, snippetTree, finalExpr)
+ innerIf.setType(snippetTree.getType)
+ innerIf
+ })
+
+ accumulatingExpression = newAccumulatingExpression
+
+ // update accumulating precondition
+ fine("updating accumulatingPrecondition")
+ accumulatingPrecondition = And(Seq(accumulatingPrecondition, Not(innerSnippetTree)))
+ fine("updating hole fun precondition and body (to be hole)")
+
+ // set to set new precondition
+ val preconditionToRestore = Some(accumulatingPrecondition)
+
+ // check for refinements
+ checkRefinements(innerSnippetTree) match {
+ case Some(refinementPair @ (id, classType)) =>
+ fine("And now we have refinement type: " + refinementPair)
+ fine("variableRefinements(id) before" + variableRefinements(id))
+ variableRefinements(id) -= loader.classMap(classType.id)
+ fine("variableRefinements(id) after" + variableRefinements(id))
+
+ // if we have a single subclass possible to refine
+ if (variableRefinements(id).size == 1) {
+ reporter.info("We do variable refinement for " + id)
+
+ val newType = variableRefinements(id).head
+ fine("new type is: " + newType)
+
+ // update declarations
+ allDeclarations =
+ for (dec <- allDeclarations)
+ yield dec match {
+ case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, LeonVariable(`id`))) =>
+ LeonDeclaration(
+ imex, TypeTransformer(newType), newType)
+ case _ =>
+ dec
+ }
+
+ // the reason for two flags is for easier management of re-syntheses only if needed
+ variableRefinedBranch = true
+ variableRefinedCondition = true
+
+ } else
+ fine("we cannot do variable refinement :(")
+ case _ =>
+ }
+
+ // found a boolean snippet, break
+ (true, preconditionToRestore)
+ } else {
+ // reset funDef and continue with next boolean snippet
+ val preconditionToRestore = Some(accumulatingPrecondition)
+ (false, preconditionToRestore)
+ }
+
+ case _ =>
+
+ fine("solver filtered out the precondition (does not imply counterexamples)")
+ (false, None)
+ } //solveReturn match { (for implying counterexamples)
+ } // notFalseSolveReturn match {
+ }
+
+ // inspect the expression if some refinements can be done
+ def checkRefinements(expr: Expr) = expr match {
+ case CaseClassInstanceOf(classDef, LeonVariable(id)) =>
+ Some((id, classDef))
+ case _ =>
+ None
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
new file mode 100755
index 000000000..bf54519c2
--- /dev/null
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
@@ -0,0 +1,61 @@
+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.{ Rule, RuleInstantiation, SynthesisContext, Problem, Solution }
+import InputExamples._
+import lesynth.SynthesizerForRuleExamples
+
+case object ConditionAbductionSynthesisImmediate extends Rule("Condition abduction synthesis (immediate).") {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
+ val solver = sctx.solver
+ val program = sctx.program
+ val reporter = sctx.reporter
+
+ p.xs match {
+ case givenVariable :: Nil =>
+ val desiredType = givenVariable.getType
+ val holeFunDef = sctx.functionContext.get
+
+ // temporary hack, should not mutate FunDef
+ val oldPostcondition = holeFunDef.postcondition
+ val oldPrecondition = holeFunDef.precondition
+ try {
+ val freshResID = FreshIdentifier("result").setType(holeFunDef.returnType)
+ val freshResVar = Variable(freshResID)
+ holeFunDef.postcondition = Some(replace(
+ Map(givenVariable.toVariable -> ResultVariable().setType(holeFunDef.returnType)), p.phi)
+ )
+ holeFunDef.precondition = Some(p.pc)
+
+ val synthesizer = new SynthesizerForRuleExamples(
+ solver, program, desiredType, holeFunDef, p, freshResVar,
+ reporter = reporter,
+ introduceExamples = introduceTwoListArgumentsExamples
+ )
+
+ synthesizer.synthesize match {
+ case EmptyReport => None
+ case FullReport(resFunDef, _) =>
+ List(
+ RuleInstantiation.immediateSuccess(p, this,
+ Solution(resFunDef.getPrecondition, Set.empty, resFunDef.body.get)
+ )
+ )
+ }
+ } finally {
+ holeFunDef.postcondition = oldPostcondition
+ holeFunDef.precondition = oldPrecondition
+ }
+ case _ =>
+ throw new RuntimeException("should not")
+ Nil
+ }
+
+ }
+}
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
new file mode 100755
index 000000000..a48556285
--- /dev/null
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -0,0 +1,71 @@
+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 InputExamples._
+import lesynth.SynthesizerForRuleExamples
+
+case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abduction synthesis (two phase).") {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+
+ p.xs match {
+ case givenVariable :: Nil =>
+ List(new RuleInstantiation(p, this, SolutionBuilder.none, "Condition abduction") {
+ def apply(sctx: SynthesisContext): RuleApplicationResult = {
+ try {
+ val solver = new TimeoutSolver(sctx.solver, 2000L)
+ val program = sctx.program
+ val reporter = sctx.reporter
+
+ val desiredType = givenVariable.getType
+ val holeFunDef = sctx.functionContext.get
+
+ // temporary hack, should not mutate FunDef
+ val oldPostcondition = holeFunDef.postcondition
+ val oldPrecondition = holeFunDef.precondition
+
+ try {
+ val freshResID = FreshIdentifier("result").setType(holeFunDef.returnType)
+ val freshResVar = Variable(freshResID)
+
+ holeFunDef.postcondition = Some(replace(
+ Map(givenVariable.toVariable -> ResultVariable().setType(holeFunDef.returnType)), p.phi))
+ holeFunDef.precondition = Some(p.pc)
+
+ val synthesizer = new SynthesizerForRuleExamples(
+ solver, program, desiredType, holeFunDef, p, freshResVar,
+ 20, 2, 1,
+ reporter = reporter,
+ introduceExamples = getInputExamples)
+
+ synthesizer.synthesize match {
+ case EmptyReport => RuleApplicationImpossible
+ case FullReport(resFunDef, _) =>
+ RuleSuccess(Solution(resFunDef.getPrecondition, Set.empty, resFunDef.body.get))
+ }
+ } catch {
+ case e: Throwable =>
+ sctx.reporter.warning("Condition abduction crashed: " + e.getMessage)
+ e.printStackTrace
+ RuleApplicationImpossible
+ } finally {
+ holeFunDef.postcondition = oldPostcondition
+ holeFunDef.precondition = oldPrecondition
+ }
+ }
+ }
+ })
+ case _ =>
+ throw new RuntimeException("should not")
+ Nil
+ }
+ }
+}
diff --git a/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala b/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
new file mode 100644
index 000000000..c9b7c528b
--- /dev/null
+++ b/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
@@ -0,0 +1,63 @@
+package insynth.reconstruction
+
+import org.junit.Assert._
+import org.junit.{ Test, Ignore }
+
+import insynth.reconstruction.codegen.CodeGenerator
+
+import leon.purescala.Trees._
+
+import insynth.testutil.{ CommonLambda, CommonDeclarations }
+
+// NOTE function cannot return function in Leon, no need to test that
+
+class CodeGeneratorTest {
+
+ import CommonLambda._
+ import CommonDeclarations._
+
+ val codeGenerator = new CodeGenerator
+
+ @Test
+ def testBooleanToIntIntermediateLambda {
+ val codeGenResult = codeGenerator(constructBooleanToIntIntermediateLambda.head)
+
+ assertEquals(
+ FunctionInvocation(functionBoolToIntFunDef, List(BooleanLiteral(false))),
+ codeGenResult
+ )
+ }
+
+ @Test
+ def testThreeParFunction {
+
+ val generated =
+ for (intermediateTree <- constructThreeParFunctionIntermediateLambda(4))
+ yield codeGenerator(intermediateTree)
+
+ val baseCase = FunctionInvocation(threeParFunctionDef, List(IntLiteral(0), IntLiteral(0), BooleanLiteral(false)))
+
+ val message = "Generated:\n" + generated.mkString("\n")
+
+ assertTrue(baseCase + " not found. " + message, generated contains baseCase)
+
+ val oneLevCase1 = FunctionInvocation(threeParFunctionDef, List(baseCase, IntLiteral(0), BooleanLiteral(false)))
+ val oneLevCase2 = FunctionInvocation(threeParFunctionDef, List(baseCase, baseCase, BooleanLiteral(false)))
+
+ assertTrue(oneLevCase1 + " not found. " + message, generated contains oneLevCase1)
+ assertTrue(oneLevCase2 + " not found. " + message, generated contains oneLevCase2)
+
+ val twoLevCase1 = FunctionInvocation(threeParFunctionDef, List(oneLevCase1, IntLiteral(0), BooleanLiteral(false)))
+ val twoLevCase2 = FunctionInvocation(threeParFunctionDef, List(baseCase, oneLevCase2, BooleanLiteral(false)))
+
+ assertTrue(twoLevCase1 + " not found. " + message, generated contains twoLevCase1)
+ assertTrue(twoLevCase2 + " not found. " + message, generated contains twoLevCase2)
+
+// val threeLevCase1 = FunctionInvocation(threeParFunctionDef, List(oneLevCase1, twoLevCase2, BooleanLiteral(false)))
+// val threeLevCase2 = FunctionInvocation(threeParFunctionDef, List(twoLevCase2, threeLevCase1, BooleanLiteral(false)))
+//
+// assertTrue(threeLevCase1 + " not found. " + message, generated contains threeLevCase1)
+// assertTrue(threeLevCase2 + " not found. " + message, generated contains threeLevCase2)
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/insynth/reconstruction/PhaseCombinationTest.scala b/src/test/scala/insynth/reconstruction/PhaseCombinationTest.scala
new file mode 100644
index 000000000..46a41a1a1
--- /dev/null
+++ b/src/test/scala/insynth/reconstruction/PhaseCombinationTest.scala
@@ -0,0 +1,74 @@
+package insynth.reconstruction
+
+import org.junit.{ Test, Ignore }
+import org.junit.Assert._
+
+import insynth.reconstruction.intermediate.IntermediateTransformer
+import insynth.reconstruction.stream.{ Extractor, UnorderedStreamFactory }
+import insynth.reconstruction.codegen.CodeGenerator
+
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ FreshIdentifier }
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees.{ Variable => LeonVariable, _ }
+
+import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonIntermediate, CommonLambda, CommonLeonExpressions }
+
+class PhaseCombinationTest {
+
+ import CommonDeclarations._
+ import CommonProofTrees._
+ import CommonIntermediate._
+ import CommonLambda._
+ import CommonLeonExpressions._
+
+ @Test
+ def treeBoolToInt {
+ val (queryNode, query) = exampleBoolToInt
+
+ val intermediateTree = IntermediateTransformer(queryNode)
+
+ val codeGenerator = new CodeGenerator
+
+ val extractor = new Extractor(new UnorderedStreamFactory)
+
+ val extractorResults = extractor(intermediateTree) take 1
+
+ assertEquals(1, extractorResults.size)
+
+ val codeGenResult = codeGenerator(extractorResults.head._1)
+
+ assertEquals(FunctionInvocation(functionBoolToIntFunDef, List(BooleanLiteral(false))), codeGenResult)
+ }
+
+ @Test
+ def treeIntToIntBoth {
+ val queryNode = exampleIntToIntBoth
+
+ val intermediateTree = IntermediateTransformer(queryNode)
+
+ assertEquals(constructIntToIntIntermediateBoth, intermediateTree)
+
+ val extractor = new Extractor(new UnorderedStreamFactory)
+
+ val extractorResults = (extractor(intermediateTree) take (5 * 2 * 2)) map { _._1 }
+
+ assertEquals(5 * 4, extractorResults.size)
+
+ for (node <- constructIntAndBoolToIntIntermediateLambda(5))
+ assertTrue(node + " is not extracted.", extractorResults contains node)
+
+ val codeGenerator = new CodeGenerator
+
+ val expressions = extractorResults.map(codeGenerator(_)).toSet
+
+ assertTrue(expressions contains boolInv)
+ assertTrue(expressions contains inv1WithBoolInv)
+ assertTrue(expressions contains inv1WithInt)
+ assertTrue(expressions contains inv2WithInt)
+ assertTrue(expressions contains inv3WithInt)
+ assertTrue(expressions contains inv2WithBoolInv)
+ assertTrue(expressions contains inv3WithBoolInv)
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/insynth/reconstruction/ReconstructorTest.scala b/src/test/scala/insynth/reconstruction/ReconstructorTest.scala
new file mode 100644
index 000000000..1c1f6b5df
--- /dev/null
+++ b/src/test/scala/insynth/reconstruction/ReconstructorTest.scala
@@ -0,0 +1,95 @@
+package insynth.reconstruction
+
+import org.junit.{ Test, Ignore, BeforeClass, AfterClass }
+import org.junit.Assert._
+
+import insynth.reconstruction.codegen.CodeGenerator
+import insynth.Config
+
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ FreshIdentifier }
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees.{ Variable => LeonVariable, _ }
+
+import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLeonExpressions, CommonUtils }
+
+class ReconstructorTest {
+
+ import CommonDeclarations._
+ import CommonProofTrees._
+ import CommonLeonExpressions._
+ import CommonUtils._
+
+ val codegen = new CodeGenerator
+
+ @Test
+ def treeBoolToInt {
+ val (queryNode, query) = exampleBoolToInt
+
+ val expStream = Reconstructor(queryNode, codegen)
+
+ assertEquals(1, expStream.size)
+
+ val codeGenResult = expStream.head
+
+ assertEquals(FunctionInvocation(functionBoolToIntFunDef, List(BooleanLiteral(false))), codeGenResult.snippet)
+ assertEquals(0f, codeGenResult.weight, 0f)
+ }
+
+ @Test
+ def treeIntToIntBoth {
+ val queryNode = exampleIntToIntBoth
+
+ val expStream = Reconstructor(queryNode, codegen)
+
+ val expressions = expStream.map(_.snippet).take(20).toSet
+
+ assertTrue(expressions contains boolInv)
+ assertTrue(expressions contains inv1WithBoolInv)
+ assertTrue(expressions contains inv1WithInt)
+ assertTrue(expressions contains inv2WithInt)
+ assertTrue(expressions contains inv3WithInt)
+ assertTrue(expressions contains inv2WithBoolInv)
+ assertTrue(expressions contains inv3WithBoolInv)
+ }
+
+ @Test
+ def treeIntToIntBothOrdered {
+ val queryNode = exampleIntToIntBoth
+
+ val expStream = Reconstructor(queryNode, codegen, true)
+
+ val expressions = assertTake(expStream, 20).map(_.snippet)
+
+ val listOfExpressions = List(boolInv, inv1WithInt, inv1WithBoolInv, inv2WithInt,
+ inv3WithInt, inv2WithBoolInv, inv3WithBoolInv)
+
+ for (exp <- listOfExpressions)
+ assertTrue(expressions.toSet contains exp)
+
+ val listOfExpressionsOrder = List(boolInv, inv1WithBoolInv, inv2WithInt,
+ inv2WithBoolInv, inv3WithBoolInv)
+
+ for (ind <- 0 until listOfExpressionsOrder.size - 1)
+ assertTrue("Expression " + listOfExpressionsOrder(ind) + " (position " + expressions.indexOf(listOfExpressionsOrder(ind)) +
+ ") should occur before expression " + listOfExpressionsOrder(ind+1) + " (position " + expressions.indexOf(listOfExpressionsOrder(ind + 1)) + ")",
+ expressions.indexOf(listOfExpressionsOrder(ind)) < expressions.indexOf(listOfExpressionsOrder(ind+1)))
+
+ }
+
+}
+
+//object ReconstructorTest {
+//
+// var useEnumerationOrdering: Boolean = _
+//
+// @BeforeClass
+// def saveFlag = {
+// useEnumerationOrdering = Config.useEnumerationOrdering
+// Config.useEnumerationOrdering = false
+// }
+//
+// @AfterClass
+// def restoreFlag = Config.useEnumerationOrdering = useEnumerationOrdering
+//
+//}
diff --git a/src/test/scala/insynth/testutil/CommonLeonExpressions.scala b/src/test/scala/insynth/testutil/CommonLeonExpressions.scala
new file mode 100644
index 000000000..2ce2d4246
--- /dev/null
+++ b/src/test/scala/insynth/testutil/CommonLeonExpressions.scala
@@ -0,0 +1,20 @@
+package insynth.testutil
+
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ FreshIdentifier }
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees.{ Variable => _, _ }
+
+object CommonLeonExpressions {
+
+ import CommonDeclarations._
+
+ val boolInv = FunctionInvocation(functionBoolToIntFunDef, List(booleanLiteral))
+ val inv1WithBoolInv = FunctionInvocation(functionIntToIntFunDef, List(boolInv))
+ val inv1WithInt = FunctionInvocation(functionIntToIntFunDef, List(intLiteral))
+ val inv2WithInt = FunctionInvocation(functionIntToIntFunDef, List(inv1WithInt))
+ val inv3WithInt = FunctionInvocation(functionIntToIntFunDef, List(inv2WithInt))
+ val inv2WithBoolInv = FunctionInvocation(functionIntToIntFunDef, List(inv1WithBoolInv))
+ val inv3WithBoolInv = FunctionInvocation(functionIntToIntFunDef, List(inv2WithBoolInv))
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/AnalyzerTest.scala b/src/test/scala/lesynth/AnalyzerTest.scala
new file mode 100644
index 000000000..166da8159
--- /dev/null
+++ b/src/test/scala/lesynth/AnalyzerTest.scala
@@ -0,0 +1,49 @@
+package lesynth
+
+import scala.util.Random
+
+import org.junit.Assert._
+import org.junit.{ Test, Ignore }
+
+import insynth.leon.HoleFinder
+import insynth.leon.loader.LeonLoader
+
+import _root_.leon.purescala.Trees.{ Hole, IntLiteral }
+import _root_.leon.purescala.TreeOps
+import _root_.leon.evaluators._
+import _root_.leon.{ LeonContext, DefaultReporter, Main }
+import _root_.leon.verification.AnalysisPhase
+
+import insynth.testutil.CommonUtils
+import testutil.TestConfig
+
+class AnalyzerTest {
+
+ import TestConfig._
+ import CommonUtils._
+ import TreeOps._
+
+ val rnd = new Random(System.currentTimeMillis())
+
+ @Test
+ def testModel = {
+ val holeFinder = new HoleFinder(lesynthTestDir + "ListOperations.scala")
+
+ holeFinder.extract match {
+ case Some((prog, hole)) =>
+
+ val reporter = new DefaultReporter()
+ val args = Array("testcases/insynth/ListOperations.scala", "--timeout=2")
+
+ val ctx = Main.processOptions(reporter, args.toList)
+
+ val verReport = AnalysisPhase.run(ctx)(prog)
+
+ assertTrue(Globals.asMap.size > 0)
+
+ case _ =>
+ fail("HoleFinder could not extract hole from the program")
+ }
+ }
+
+}
diff --git a/src/test/scala/lesynth/RefinerTest.scala b/src/test/scala/lesynth/RefinerTest.scala
new file mode 100644
index 000000000..861971ed1
--- /dev/null
+++ b/src/test/scala/lesynth/RefinerTest.scala
@@ -0,0 +1,209 @@
+package lesynth
+
+import scala.util.Random
+
+import org.junit.Assert._
+import org.junit.{ Test, Ignore, Before }
+
+import insynth.leon.HoleFinder
+import insynth.leon.loader.{ LeonLoader, HoleExtractor }
+import insynth.leon._
+
+import _root_.leon.purescala.Trees.{ Expr, Hole, IntLiteral, UnitLiteral, Variable, FunctionInvocation, And }
+import _root_.leon.purescala.{ TreeOps }
+import _root_.leon.purescala.Definitions.{ Program, FunDef }
+import _root_.leon.evaluators._
+import _root_.leon.{ LeonContext, DefaultReporter, Main }
+import _root_.leon.verification.AnalysisPhase
+
+import insynth.testutil.CommonUtils
+import testutil.TestConfig
+
+class RefinerTest {
+
+ import TestConfig._
+ import CommonUtils._
+ import TreeOps._
+
+ val rnd = new Random(System.currentTimeMillis())
+
+ var prog: Program = _
+ var hole: Hole = _
+ var holeFunDef: FunDef = _
+
+ var tail: UnaryReconstructionExpression = _
+ var head: UnaryReconstructionExpression = _
+ var nil: Expr = _
+ var cons: NaryReconstructionExpression = _
+
+ @Before
+ def extract = {
+
+ val holeFinder = new HoleFinder(lesynthTestDir + "ListOperationsHole.scala")
+
+ holeFinder.extract match {
+ case Some((progE, holeE)) =>
+
+ prog = progE
+ hole = holeE
+
+ holeFunDef = new HoleExtractor(prog, hole).extractHole match {
+ case Some((hfd, _)) => hfd
+ case None => fail("could not extract hole"); null
+ }
+
+ val loader = new LeonLoader(prog, hole)
+
+ tail =
+ loader.extractFields.find {
+ _.expression match {
+ case ure: UnaryReconstructionExpression => ure(UnitLiteral).toString.contains(".tail")
+ case _ => false
+ }
+ } match {
+ case Some(found) => found.expression.asInstanceOf[UnaryReconstructionExpression]
+ case _ => fail("could not extract tail"); null
+ }
+
+ head =
+ loader.extractFields.find {
+ _.expression match {
+ case ure: UnaryReconstructionExpression => ure(UnitLiteral).toString.contains(".head")
+ case _ => false
+ }
+ } match {
+ case Some(found) => found.expression.asInstanceOf[UnaryReconstructionExpression]
+ case _ => fail("could not extract head"); null
+ }
+
+ cons =
+ loader.extractCaseClasses.find {
+ _.expression match {
+ case nre: NaryReconstructionExpression => nre(List(UnitLiteral, UnitLiteral)).toString.contains("Cons")
+ case _ => false
+ }
+ } match {
+ case Some(found) => found.expression.asInstanceOf[NaryReconstructionExpression]
+ case _ => fail("could not extract cons"); null
+ }
+
+ nil =
+ loader.extractCaseClasses.find {
+ _.expression match {
+ case im: ImmediateExpression => im().toString.contains("Nil")
+ case _ => false
+ }
+ } match {
+ case Some(found) => found.expression.asInstanceOf[ImmediateExpression]()
+ case _ => fail("could not extract cons"); null
+ }
+
+ case _ =>
+ fail("HoleFinder could not extract hole from the program")
+ }
+ }
+
+ @Test
+ def testIsLess = {
+
+ val refiner = new Refiner(prog, hole, holeFunDef)
+ import refiner.isLess
+
+ assertEquals(2, holeFunDef.args.size)
+
+ val variable1 = holeFunDef.args.head
+ val variable2 = holeFunDef.args(1)
+
+ assertEquals(+1, isLess(cons(List(UnitLiteral, variable1.toVariable)), variable1))
+ assertEquals(+1, isLess(cons(List(UnitLiteral, variable1.toVariable)), variable2))
+ assertEquals(-1, isLess(tail(variable1.toVariable), variable1))
+ assertEquals(+1, isLess(head(variable1.toVariable), variable1))
+ assertEquals(0, isLess(variable1.toVariable, variable1))
+ assertEquals(1, isLess(variable1.toVariable, variable2))
+ assertEquals(1, isLess(tail(variable1.toVariable), variable2))
+ assertEquals(1, isLess(head(variable1.toVariable), variable2))
+ assertEquals(1, isLess(nil, variable2))
+
+ }
+
+ @Test
+ def testIsCallLessBySize = {
+
+ val refiner = new Refiner(prog, hole, holeFunDef)
+ import refiner.isCallAvoidableBySize
+
+ assertEquals(2, holeFunDef.args.size)
+
+ val arg1 = holeFunDef.args.head.toVariable
+ val arg2 = holeFunDef.args(1).toVariable
+
+ def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(holeFunDef, Seq(arg1, arg2))
+
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(nil, nil)))
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg1, arg2)))
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg2, arg1)))
+ assertEquals(false, isCallAvoidableBySize(makeFunctionCall(arg1, tail(arg2))))
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(arg1, tail(arg1))))
+ assertEquals(false, isCallAvoidableBySize(makeFunctionCall(tail(arg1), tail(arg2))))
+ assertEquals(true, isCallAvoidableBySize(makeFunctionCall(cons(List(nil, tail(arg1))), arg2)))
+ assertEquals(false, isCallAvoidableBySize(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2))))
+ assertEquals(false, isCallAvoidableBySize(nil))
+
+ }
+
+ @Test
+ def testHasDoubleRecursion = {
+
+ val refiner = new Refiner(prog, hole, holeFunDef)
+ import refiner.hasDoubleRecursion
+
+ assertEquals(2, holeFunDef.args.size)
+
+ val arg1 = holeFunDef.args.head.toVariable
+ val arg2 = holeFunDef.args(1).toVariable
+
+ def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(holeFunDef, Seq(arg1, arg2))
+
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(nil, nil)))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, arg2)))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg2, arg1)))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, tail(arg2))))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(arg1, tail(arg1))))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(tail(arg1), tail(arg2))))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(cons(List(nil, tail(arg1))), arg2)))
+ assertEquals(false, hasDoubleRecursion(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2))))
+ assertEquals(false, hasDoubleRecursion(nil))
+
+ assertEquals(false, hasDoubleRecursion(And(makeFunctionCall(arg1, arg2), makeFunctionCall(arg1, arg2))))
+ assertEquals(true, hasDoubleRecursion(makeFunctionCall(makeFunctionCall(arg1, arg2), tail(arg2))))
+
+ }
+
+ @Test
+ def testIsAvoidable = {
+
+ val refiner = new Refiner(prog, hole, holeFunDef)
+ import refiner.isAvoidable
+
+ assertEquals(2, holeFunDef.args.size)
+
+ val arg1 = holeFunDef.args.head.toVariable
+ val arg2 = holeFunDef.args(1).toVariable
+
+ def makeFunctionCall(arg1: Expr, arg2: Expr) = FunctionInvocation(holeFunDef, Seq(arg1, arg2))
+
+ assertEquals(true, isAvoidable(makeFunctionCall(nil, nil)))
+ assertEquals(true, isAvoidable(makeFunctionCall(arg1, arg2)))
+ assertEquals(true, isAvoidable(makeFunctionCall(arg2, arg1)))
+ assertEquals(false, isAvoidable(makeFunctionCall(arg1, tail(arg2))))
+ assertEquals(true, isAvoidable(makeFunctionCall(arg1, tail(arg1))))
+ assertEquals(false, isAvoidable(makeFunctionCall(tail(arg1), tail(arg2))))
+ assertEquals(true, isAvoidable(makeFunctionCall(cons(List(nil, tail(arg1))), arg2)))
+ assertEquals(false, isAvoidable(makeFunctionCall(cons(List(nil, tail(arg1))), tail(arg2))))
+ assertEquals(false, isAvoidable(nil))
+
+ assertEquals(true, isAvoidable(makeFunctionCall(makeFunctionCall(arg1, arg2), tail(arg2))))
+
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/TryOutSynthesizerExamplesTest.scala b/src/test/scala/lesynth/TryOutSynthesizerExamplesTest.scala
new file mode 100755
index 000000000..2655b3ef7
--- /dev/null
+++ b/src/test/scala/lesynth/TryOutSynthesizerExamplesTest.scala
@@ -0,0 +1,672 @@
+package lesynth
+
+import org.junit.Assert._
+import org.junit.{ Test, Ignore }
+
+import testutil.TestConfig
+
+import scala.collection.mutable.{ Map => MutableMap }
+import scala.collection.mutable.{ Set => MutableSet }
+import scala.collection.mutable.{ LinkedList => MutableList }
+import scala.util.matching.Regex
+import scala.collection.mutable.PriorityQueue
+
+import scala.tools.nsc.{ Settings => NSCSettings, MainGenericRunner }
+
+import leon.{ Main => LeonMain, Reporter, DefaultReporter, SilentReporter, Settings, LeonContext }
+import leon.solvers.{ Solver, TimeoutSolver }
+import leon.solvers.z3.{ FairZ3Solver }
+import leon.verification.AnalysisPhase
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Trees.{ Variable => LeonVariable, _ }
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.TreeOps
+import leon.plugin.ExtractionPhase
+
+import insynth.util.logging.HasLogger
+import insynth.interfaces.Declaration
+import insynth.InSynth
+import insynth.reconstruction.codegen.CodeGenerator
+import insynth.leon.loader.LeonLoader
+import insynth.leon.LeonDeclaration
+import insynth.leon.ImmediateExpression
+import insynth.engine.InitialEnvironmentBuilder
+import insynth.leon.LeonQueryBuilder
+import insynth.interfaces.{ Loader, Declaration, QueryBuilder }
+import insynth.engine.{ Engine, InitialEnvironmentBuilder }
+import insynth.engine.scheduler.WeightScheduler
+import insynth.structures.ContainerNode
+import insynth.util.TimeOut
+import insynth.Config
+import insynth.reconstruction.Reconstructor
+import insynth.leon.TypeTransformer
+import insynth.leon.HoleFinder
+import insynth.leon.loader.HoleExtractor
+import insynth.reconstruction.Output
+
+class TryOutSynthesizerExamplesTest {
+
+ @Test
+ def tryOut {
+ import TestConfig._
+
+ val synthesizer = new TryOutSynthesizerExamples(lesynthTestDir + "ListOperationsHole.scala")
+
+ val report = synthesizer.synthesize
+ assertTrue(report.isSuccess)
+ println(report.summaryString)
+ }
+
+}
+
+class TryOutSynthesizerExamples(
+ fileName: String,
+ // number of condition expressions to try before giving up on that branch expression
+ numberOfBooleanSnippets: Int = 5,
+ numberOfCounterExamplesToGenerate: Int = 5,
+ leonTimeout: Int = 2, // seconds
+ analyzeSynthesizedFunctionOnly: Boolean = false,
+ showLeonOutput: Boolean = false,
+ reporter: Reporter = new DefaultReporter,
+ collectCounterExamplesFromLeon: Boolean = false) extends HasLogger {
+
+ info("Synthesizer:")
+ info("fileName: %s".format(fileName))
+ info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
+ info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
+ info("leonTimeout: %d".format(leonTimeout))
+
+ // some synthesis instance information
+ private var program: Program = _
+ private var hole: Hole = _
+ private var holeFunDef: FunDef = _
+ // initial declarations
+ private var allDeclarations: List[Declaration] = _
+ // objects used in the synthesis
+ private var loader: LeonLoader = _
+ private var inSynth: InSynth = _
+ private var inSynthBoolean: InSynth = _
+ private var refiner: Refiner = _
+ private var solver: Solver = _
+ private var ctx: LeonContext = _
+ private var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = _
+ private var initialPrecondition: Expr = _
+
+ // flag denoting if a correct body has been synthesized
+ private var found = false
+
+ // accumulate precondition for the remaining branch to synthesize
+ private var accumulatingPrecondition: Expr = _
+ // accumulate the final expression of the hole
+ private var accumulatingExpression: Expr => Expr = _
+ //private var accumulatingExpressionMatch: Expr => Expr = _
+
+ // time
+ var startTime: Long = _
+ var verTime: Long = 0
+ var synTime: Long = 0
+
+ // filtering/ranking with examples support
+ var exampleRunner: ExampleRunner = _
+ val numberOfTestsInIteration = 50
+ val numberOfCheckInIteration = 5
+
+ // TODO function to check specifically
+ def analyzeProgram = {
+
+ val temp = System.currentTimeMillis
+ Globals.allSolved = Some(true)
+
+ val report = AnalysisPhase.run(ctx)(program)
+
+ val time = System.currentTimeMillis - temp
+ fine("Analysis took: " + time + ", from report: " + report.totalTime)
+
+ // accumulate
+ verTime += time
+
+ report
+ }
+
+ // TODO return boolean (do not do unecessary analyze)
+ def generateCounterexamples(program: Program, funDef: FunDef, number: Int): (Seq[Map[Identifier, Expr]], Expr) = {
+
+ fine("generate counter examples with funDef.prec= " + funDef.precondition.getOrElse(BooleanLiteral(true)))
+ val temp = System.currentTimeMillis
+
+ // get current precondition
+ var precondition = funDef.precondition.getOrElse(BooleanLiteral(true))
+ // where we will accumulate counterexamples as sequence of maps
+ var maps: Seq[Map[Identifier, Expr]] = Seq.empty
+
+ // iterate specific number of times or until no further counterexample can be generated
+ var changed = true
+ var ind = 0
+ while (ind < number && changed) {
+
+ // analyze the program
+ analyzeProgram
+
+ // check if solver could solved this instance
+ if (Globals.allSolved == Some(false) && !Globals.asMap.isEmpty) {
+
+ fine("found coounterexample: " + Globals.asMap)
+ // add current counterexample
+ maps :+= Globals.asMap
+
+ // prevent this counterexample to re-occur
+ val precAddition = Not(And(Globals.asMap map { case (id, value) => Equals(LeonVariable(id), value) } toSeq))
+ precondition = And(Seq(precondition, precAddition))
+ // update precondition
+ funDef.precondition = Some(precondition)
+ } else
+ changed = false
+
+ ind += 1
+ }
+
+ val temptime = System.currentTimeMillis - temp
+ fine("Generation of counter-examples took: " + temptime)
+ verTime += temptime
+
+ // return found counterexamples and the formed precondition
+ (maps, precondition)
+ }
+
+ def getCurrentBuilder = new InitialEnvironmentBuilder(allDeclarations)
+
+ def synthesizeBranchExpressions =
+ inSynth.getExpressions(getCurrentBuilder)
+
+ def synthesizeBooleanExpressions =
+ inSynthBoolean.getExpressions(getCurrentBuilder)
+
+ def interactivePause = {
+ System.out.println("Press Any Key To Continue...");
+ new java.util.Scanner(System.in).nextLine();
+ }
+
+ def initialize = {
+
+ // TODO lose this - globals are bad
+ Globals.allSolved = None
+
+ // extract hole
+ new HoleFinder(fileName).extract match {
+ case Some((matchProgram, matchHole: Hole)) =>
+ program = matchProgram
+ hole = matchHole
+ case None => throw new RuntimeException("Cannot find hole")
+ }
+
+ // context needed for verification
+ import leon.Main._
+ val reporter =
+ if (showLeonOutput) new DefaultReporter
+ else new SilentReporter
+
+ val args =
+ if (analyzeSynthesizedFunctionOnly)
+ Array(fileName, "--timeout=" + leonTimeout, "--functions=" + holeFunDef.id.name)
+ else
+ Array(fileName, "--timeout=" + leonTimeout)
+ info("Leon context array: " + args.mkString(","))
+ ctx = processOptions(reporter, args.toList)
+
+ solver = //new FairZ3Solver(ctx)
+ new TimeoutSolver(new FairZ3Solver(ctx), leonTimeout)
+
+ // create new insynth object
+ loader = new LeonLoader(program, hole, false)
+ inSynth = new InSynth(loader, true)
+ // save all declarations seen
+ allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+ // make conditions synthesizer
+ inSynthBoolean = new InSynth(allDeclarations, BooleanType, true)
+
+ // funDef of the hole
+ holeFunDef = loader.holeDef
+ fine("postcondition is: " + holeFunDef.getPostcondition)
+
+ // accumulate precondition for the remaining branch to synthesize
+ accumulatingPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+ // save initial precondition
+ initialPrecondition = accumulatingPrecondition
+ // accumulate the final expression of the hole
+ accumulatingExpression = (finalExp: Expr) => finalExp
+ //accumulatingExpressionMatch = accumulatingExpression
+
+ // each variable of super type can actually have a subtype
+ // get sine declaration maps to be able to refine them
+ val directSubclassMap = loader.directSubclassesMap
+ val variableDeclarations = loader.variableDeclarations
+ // map from identifier into a set of possible subclasses
+ variableRefinements = MutableMap.empty
+ for (varDec <- variableDeclarations) {
+ varDec match {
+ case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, LeonVariable(id))) =>
+ variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
+ case _ =>
+ }
+ }
+
+ // calculate cases that should not happen
+ refiner = new Refiner(program, hole, holeFunDef)
+ fine("Refiner initialized. Recursive call: " + refiner.recurentExpression)
+
+ exampleRunner = new ExampleRunner(holeFunDef)
+ exampleRunner.counterExamples ++= introduceCounterExamples
+ }
+
+ def countPassedExamples(snippet: Expr) = {
+ val oldPreconditionSaved = holeFunDef.precondition
+ val oldBodySaved = holeFunDef.body
+
+ // restore initial precondition
+ holeFunDef.precondition = Some(initialPrecondition)
+
+ // get the whole body (if else...)
+ val accumulatedExpression = accumulatingExpression(snippet)
+ // set appropriate body to the function for the correct evaluation
+ holeFunDef.body = Some(accumulatedExpression)
+
+ val count = exampleRunner.countPassed(accumulatedExpression)
+
+ holeFunDef.precondition = oldPreconditionSaved
+ holeFunDef.body = oldBodySaved
+
+ count
+ }
+
+ def introduceCounterExamples = {
+ val argumentIds = holeFunDef.args.map(_.id)
+ hole.getType match {
+ case ct: ClassType =>
+ val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
+
+ val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
+
+ val nilClass = nilClassSet.head
+ val consClass = consClassSet.head
+
+ var counter = 0
+ def getIntLiteral = { counter += 1; IntLiteral(counter) }
+
+ val list0 = () => CaseClass(nilClass, Nil)
+ val list1 = () => CaseClass(consClass, getIntLiteral :: list0() :: Nil)
+ val list2 = () => CaseClass(consClass, getIntLiteral :: list1() :: Nil)
+ val list3 = () => CaseClass(consClass, getIntLiteral :: list2() :: Nil)
+ val list4 = () => CaseClass(consClass, getIntLiteral :: list3() :: Nil)
+
+ val lists = List(list0, list1, list2, list3 /*, list4*/ )
+
+ for (l1 <- lists; l2 <- lists)
+ yield Map(argumentIds(0) -> l1(), argumentIds(1) -> l2())
+
+ case _ =>
+ throw new RuntimeException("Could not produce initial examples: Could not match hole type")
+ }
+ }
+
+ def synthesize: Report = {
+ reporter.info("Synthesis called on file: " + fileName)
+
+ // get start time
+ startTime = System.currentTimeMillis
+
+ reporter.info("Initializing synthesizer: ")
+ reporter.info("numberOfBooleanSnippets: %d".format(numberOfBooleanSnippets))
+ reporter.info("numberOfCounterExamplesToGenerate: %d".format(numberOfCounterExamplesToGenerate))
+ reporter.info("leonTimeout: %d".format(leonTimeout))
+ initialize
+ reporter.info("Synthesizer initialized")
+
+ // keeps status of validity
+ var keepGoing = Globals.allSolved match {
+ case Some(true) => false
+ case _ => true
+ }
+
+ // initial snippets (will update in the loop)
+ var snippets = synthesizeBranchExpressions
+ // iterate while the program is not valid
+ import scala.util.control.Breaks._
+ var iteration = 0
+ breakable {
+ while (keepGoing) {
+ // next iteration
+ iteration += 1
+ reporter.info("####################################")
+ reporter.info("######Iteration #" + iteration + " ###############")
+ reporter.info("####################################")
+
+ // just printing of expressions
+ finest(
+ ((snippets zip Iterator.range(0, 200).toStream) map {
+ case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet
+ }).mkString("\n"))
+ reporter.info("# precondition is: " + holeFunDef.precondition.getOrElse(BooleanLiteral(true)))
+ reporter.info("# accumulatingPrecondition is: " + accumulatingPrecondition)
+ reporter.info("# accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
+ reporter.info("####################################")
+
+ // ordering of expressions according to passed examples
+ var pq = new PriorityQueue[(Expr, Int)]()(
+ new Ordering[(Expr, Int)] {
+ def compare(pair1: (Expr, Int), pair2: (Expr, Int)) =
+ pair1._2.compare(pair2._2)
+ })
+ var numberOfTested = 0
+
+ // just printing of expressions and pass counts
+ finest(
+ ((snippets zip Iterator.range(0, 200).toStream) map {
+ case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet +
+ " pass count is " + countPassedExamples(snippet.getSnippet)
+ }).mkString("\n"))
+ //interactivePause
+
+ // found precondition?
+ found = false
+ // try to find it
+ breakable {
+ // go through all snippets
+ for (snippet <- snippets; val snippetTree = snippet.getSnippet) {
+ finest("snippetTree is: " + snippetTree)
+
+ // skip avoidable calls
+ if (!refiner.isAvoidable(snippetTree)) {
+
+ // passed example pairs
+ val passCount = countPassedExamples(snippetTree)
+
+ if (passCount == exampleRunner.counterExamples.size) {
+ info("All examples passed. Testing snippet " + snippetTree + " right away")
+ if (tryToSynthesizeBranch(snippetTree)) {
+ // will set found if correct body is found
+ break
+ }
+ } else {
+ info("snippet with pass count filtered: " + (snippetTree, passCount))
+ pq.enqueue((snippetTree, 100 + (passCount * (iteration - 1)) - snippet.getWeight.toInt))
+ }
+
+ } else {
+ fine("Refiner filtered this snippet: " + snippetTree)
+ } // if (!refiner.isAvoidable(snippetTree)) {
+
+ // check if we this makes one test iteration
+ if (numberOfTested >= numberOfTestsInIteration) {
+ fine("Queue contents: " + pq.mkString(", "))
+ fine("head of queue is: " + pq.head)
+
+ //interactivePause
+ // go and check the topmost numberOfCheckInIteration
+ for (i <- 1 to math.min(numberOfCheckInIteration, pq.size)) {
+ val nextSnippet = pq.dequeue._1
+ info("dequeued nextSnippet: " + nextSnippet)
+ //interactivePause
+
+ if (tryToSynthesizeBranch(nextSnippet)) {
+ break
+ }
+ }
+
+ numberOfTested = 0
+ } else
+ numberOfTested += 1
+
+ } // for (snippet <- snippets
+ } // breakable { for (snippet <- snippets
+
+ // if did not found for any of the branch expressions
+ if (found) {
+ val endTime = System.currentTimeMillis
+ reporter.info("We are done, in time: " + (endTime - startTime))
+ return new FullReport(holeFunDef, (endTime - startTime))
+ }
+
+ // get new snippets
+ snippets = synthesizeBranchExpressions
+
+ fine("filtering based on: " + holeFunDef.precondition.get)
+ fine("counterexamples before filter: " + exampleRunner.counterExamples.size)
+ exampleRunner.filter(holeFunDef.precondition.get)
+ fine("counterexamples after filter: " + exampleRunner.counterExamples.size)
+ fine("counterexamples after filter: " + exampleRunner.counterExamples.mkString("\n"))
+ }
+ } //breakable { while (!keepGoing) {
+
+ EmptyReport
+ }
+
+ def tryToSynthesizeBranch(snippetTree: Expr): Boolean = {
+ // replace hole in the body with the whole if-then-else structure, with current snippet tree
+ val oldBody = holeFunDef.getBody
+ val newBody = accumulatingExpression(snippetTree)
+ holeFunDef.body = Some(newBody)
+
+ // precondition
+ val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+ holeFunDef.precondition = Some(initialPrecondition)
+
+ snippetTree.setType(hole.desiredType)
+ //holeFunDef.getBody.setType(hole.desiredType)
+
+ // TODO spare one analyzing step
+ // analyze the program
+ fine("analyzing program for funDef:" + holeFunDef)
+ analyzeProgram
+
+ // check if solver could solved this instance
+ if (Globals.allSolved == Some(true)) {
+ // mark the branch found
+ found = true
+
+ reporter.info("Wooooooow we have a winner!")
+ reporter.info("************************************")
+ reporter.info("*********And the winner is**********")
+ reporter.info(accumulatingExpression(snippetTree).toString)
+ reporter.info("************************************")
+
+ return true
+ }
+
+ // store appropriate values here, will be update in a finally branch
+ var bodyToRestore = oldBody
+ var preconditionToRestore = Some(oldPrecondition)
+
+ // because first initial test
+ holeFunDef.precondition = preconditionToRestore
+
+ // get counterexamples
+ fine("Going to generating counterexamples: " + holeFunDef)
+ val (maps, precondition) = generateCounterexamples(program, holeFunDef, 5)
+
+ // collect (add) counterexamples from leon
+ if (collectCounterExamplesFromLeon)
+ exampleRunner.counterExamples ++= maps
+
+ // this should not be possible
+ // val keepGoing = Globals.allSolved match {
+ // case Some(true) => false
+ // case _ => true
+ // }
+ //
+ // // if no counterexamples and all are solved, we are done
+ // if (maps.isEmpty && !keepGoing) {
+ // // mark the branch found
+ // found = true
+ //
+ // println("Wooooooow we have a winner!")
+ // println("************************************")
+ // println("*********And the winner is**********")
+ // println(accumulatingExpression(snippetTree))
+ // println("************************************")
+ //
+ // return true
+ // }
+
+ // will modify funDef body and precondition, restore it later
+ try {
+ if (!maps.isEmpty) {
+ // proceed with synthesizing boolean expressions
+ solver.setProgram(program)
+
+ // reconstruct (only defined number of boolean expressions)
+ val innerSnippets = synthesizeBooleanExpressions take numberOfBooleanSnippets
+ // just printing of expressions
+ finest(
+ ((innerSnippets zip Iterator.range(0, 500).toStream) map {
+ case ((snippet: Output, ind: Int)) => ind + ": snippet is " + snippet.getSnippet
+ }).mkString("\n"))
+
+ for (innerSnippetTree <- innerSnippets map { _.getSnippet }) {
+ fine("boolean snippet is: " + innerSnippetTree)
+
+ val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, precondition)
+
+ // if precondition found
+ if (innerFound) {
+ reporter.info("Precondition " + innerPrec + " found for " + snippetTree)
+
+ innerPrec match {
+ case s @ Some(_) =>
+ // new precondition (restore in finally)
+ preconditionToRestore = s
+ case _ =>
+ }
+ return true
+ }
+
+ } // iterating over all boolean solutions
+
+ reporter.info("No precondition found for branch expression: " + snippetTree)
+ return false
+
+ } // if ( !maps.isEmpty ) {
+ // no counter examples, we just say that we cannot do anything
+ false
+ } // try
+ finally {
+ // set these to the FunDef
+ holeFunDef.precondition = preconditionToRestore
+ // restore old body (we accumulate expression)
+ holeFunDef.body = Some(oldBody)
+ }
+ }
+
+ def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: Expr): (Boolean, Option[Expr]) = {
+
+ // new condition together with existing precondition
+ val newCondition = And(Seq(accumulatingPrecondition, innerSnippetTree))
+
+ // new expression should not be false
+ val notFalseEquivalence = Not(newCondition)
+ val notFalseSolveReturn = solver.solve(notFalseEquivalence)
+ fine("solve for not false returned: " + notFalseSolveReturn)
+
+ notFalseSolveReturn match {
+ case Some(true) =>
+ (false, None)
+ case None =>
+ (false, None)
+ // nothing here
+ // here, our expression is not contradictory, continue
+ case Some(false) =>
+ // check if synthesized boolean expression implies precondition (counterexamples)
+ val implyExpression = Implies(newCondition, precondition)
+ fine("implyExpression is: " + implyExpression)
+
+ // check if synthesized condition implies counter-examples
+ val solveReturn = solver.solve(implyExpression)
+ fine("solve returned: " + solveReturn)
+
+ solveReturn match {
+ case Some(true) =>
+ // if expression implies counterexamples add it to the precondition and try to validate program
+ holeFunDef.precondition = Some(newCondition)
+ // do analysis
+ analyzeProgram
+ // program is valid, we have a branch
+ if (Globals.allSolved == Some(true)) {
+ // we found a branch
+ reporter.info("Wow! We found a branch!")
+
+ // update accumulating expression
+ val oldAccumulatingExpression = accumulatingExpression
+ val newAccumulatingExpression =
+ (finalExpr: Expr) =>
+ oldAccumulatingExpression({
+ val innerIf = IfExpr(innerSnippetTree, snippetTree, finalExpr)
+ innerIf.setType(snippetTree.getType)
+ innerIf
+ })
+
+ accumulatingExpression = newAccumulatingExpression
+
+ // update accumulating precondition
+ fine("updating accumulatingPrecondition")
+ accumulatingPrecondition = And(Seq(accumulatingPrecondition, Not(innerSnippetTree)))
+ fine("updating hole fun precondition and body (to be hole)")
+
+ // set to set new precondition
+ val preconditionToRestore = Some(accumulatingPrecondition)
+
+ // check for refinements
+ checkRefinements(innerSnippetTree) match {
+ case Some(refinementPair @ (id, classType)) =>
+ fine("And now we have refinement type: " + refinementPair)
+ fine("variableRefinements(id) before" + variableRefinements(id))
+ variableRefinements(id) -= loader.classMap(classType.id)
+ fine("variableRefinements(id) after" + variableRefinements(id))
+
+ // if we have a single subclass possible to refine
+ if (variableRefinements(id).size == 1) {
+ reporter.info("We do variable refinement for " + id)
+
+ val newType = variableRefinements(id).head
+ fine("new type is: " + newType)
+
+ // update declarations
+ allDeclarations =
+ for (dec <- allDeclarations)
+ yield dec match {
+ case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, LeonVariable(`id`))) =>
+ LeonDeclaration(
+ imex, TypeTransformer(newType), newType)
+ case _ =>
+ dec
+ }
+
+ } else
+ fine("we cannot do variable refinement :(")
+ case _ =>
+ }
+
+ // found a boolean snippet, break
+ (true, preconditionToRestore)
+ } else {
+ // reset funDef and continue with next boolean snippet
+ val preconditionToRestore = Some(accumulatingPrecondition)
+ (false, preconditionToRestore)
+ }
+
+ case _ =>
+
+ fine("solver filtered out the precondition (does not imply counterexamples)")
+ (false, None)
+ } //solveReturn match { (for implying counterexamples)
+ } // notFalseSolveReturn match {
+ }
+
+ // inspect the expression if some refinements can be done
+ def checkRefinements(expr: Expr) = expr match {
+ case CaseClassInstanceOf(classDef, LeonVariable(id)) =>
+ Some((id, classDef))
+ case _ =>
+ None
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/TryOutTest.scala b/src/test/scala/lesynth/TryOutTest.scala
new file mode 100644
index 000000000..d3a44e941
--- /dev/null
+++ b/src/test/scala/lesynth/TryOutTest.scala
@@ -0,0 +1,639 @@
+package lesynth
+
+import org.junit.Assert._
+import org.junit.{ Test, Ignore }
+
+import scala.collection.mutable.{ Map => MutableMap }
+import scala.collection.mutable.{ Set => MutableSet }
+import scala.collection.mutable.{ LinkedList => MutableList }
+import scala.util.matching.Regex
+import scala.collection.mutable.PriorityQueue
+
+import scala.tools.nsc.{ Settings => NSCSettings, MainGenericRunner }
+
+import leon.{ Main => LeonMain, DefaultReporter, SilentReporter, Settings, LeonContext }
+import leon.solvers.{ Solver, TimeoutSolver }
+import leon.solvers.z3.{ FairZ3Solver }
+import leon.verification.AnalysisPhase
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+import leon.purescala.Trees.{ Variable => LeonVariable, _ }
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.purescala.TreeOps
+import leon.plugin.ExtractionPhase
+
+import insynth.util.logging.HasLogger
+import insynth.interfaces.Declaration
+import insynth.InSynth
+import insynth.reconstruction.codegen.CodeGenerator
+import insynth.leon.loader.LeonLoader
+import insynth.leon.LeonDeclaration
+import insynth.leon.ImmediateExpression
+import insynth.engine.InitialEnvironmentBuilder
+import insynth.leon.LeonQueryBuilder
+import insynth.interfaces.{ Loader, Declaration, QueryBuilder }
+import insynth.engine.{ Engine, InitialEnvironmentBuilder }
+import insynth.engine.scheduler.WeightScheduler
+import insynth.structures.ContainerNode
+import insynth.util.TimeOut
+import insynth.Config
+import insynth.reconstruction.Reconstructor
+import insynth.leon.TypeTransformer
+import insynth.leon.HoleFinder
+import insynth.leon.loader.HoleExtractor
+
+import testutil.TestConfig
+
+class TryOutTest extends HasLogger {
+
+ import TestConfig.lesynthTestDir
+
+ @Test
+ def test1 {
+ synthesize(lesynthTestDir + "ListOperationsHole.scala")
+ }
+
+ def analyzeProgram(program: Program) {
+ import leon.Main._
+
+ val temp = System.currentTimeMillis
+ Globals.allSolved = Some(true)
+
+ val reporter = new SilentReporter()
+ val args = Array("no file!", "--timeout=2")
+ val ctx = processOptions(reporter, args.toList)
+
+ AnalysisPhase.run(ctx)(program)
+
+ val time = System.currentTimeMillis - temp
+ println("analysis took " + time)
+ verTime += time
+ }
+
+ def generateCounterexamples(program: Program, funDef: FunDef, number: Int): (Seq[Map[Identifier, Expr]], Expr) = {
+
+ fine("generate counter examples with funDef.prec= " + funDef.precondition.getOrElse(BooleanLiteral(true)))
+
+ // get current precondition
+ var precondition = funDef.precondition.getOrElse(BooleanLiteral(true))
+ // where we will accumulate counterexamples as sequence of maps
+ var maps: Seq[Map[Identifier, Expr]] = Seq.empty
+
+ // iterate specific number of times or until no further counterexample can be generated
+ var changed = true
+ var ind = 0
+ while (ind < number && changed) {
+
+ // analyze the program
+ analyzeProgram(program)
+
+ // check if solver could solved this instance
+ if (Globals.allSolved == Some(false) && !Globals.asMap.isEmpty) {
+
+ fine("found coounterexample: " + Globals.asMap)
+
+ // add current counterexample
+ maps :+= Globals.asMap
+ // prevent this counterexample to reoccur
+ val precAddition = Not(And(Globals.asMap map { case (id, value) => Equals(LeonVariable(id), value) } toSeq))
+ precondition = And(Seq(precondition, precAddition))
+ funDef.precondition = Some(precondition)
+ } else
+ changed = false
+
+ ind += 1
+ }
+
+ // return found counterexamples and the formed precondition
+ (maps, precondition)
+ }
+
+ def assertL1L2Refinements(variableRefinements: MutableMap[Identifier, MutableSet[ClassType]]) =
+ for (
+ pair @ (varName, nameSet) <- List(
+ ("l2", Set("Nil", "Cons")),
+ ("l1", Set("Nil", "Cons")))
+ ) assertTrue(
+ "pair " + pair + " not found. Found: " + variableRefinements.mkString(", "),
+ (false /: variableRefinements) {
+ (res, extr) =>
+ extr match {
+ case (id, classTypeSet) => res ||
+ (
+ id.name == varName &&
+ (true /: nameSet) {
+ (res, innerName) => res && classTypeSet.exists(_.classDef.id.name == innerName)
+ })
+ case _ => false
+ }
+ })
+
+ private var program: Program = _
+
+ private var hole: Hole = _
+ private var holeFunDef: FunDef = _
+
+ private var allDeclarations: List[Declaration] = _
+
+ private var loader: LeonLoader = _
+
+ private var inSynth: InSynth = _
+ private var codeGenerator: CodeGenerator = _
+
+ private var refiner: Refiner = _
+
+ var found = false
+
+ // accumulate precondition for the remaining branch to synthesize
+ private var accumulatingPrecondition: Expr = _
+ // accumulate the final expression of the hole
+ private var accumulatingExpression: Expr => Expr = _
+ //private var accumulatingExpressionMatch: Expr => Expr = _
+
+ var solver: Solver = _
+ //
+ var ctx: LeonContext = _
+ //
+ var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = _
+
+ var initialPrecondition: Expr = _
+
+ var startTime: Long = _
+
+ var verTime: Long = 0
+ var synTime: Long = 0
+
+ // number of condition expressions to try before giving up on that branch expression
+ val numberOfBooleanSnippets = 5
+
+ def synthesizeExpressions =
+ inSynth.getExpressions
+
+ def initialize(fileName: String) = {
+
+ import leon.Main._
+
+ val reporter = new SilentReporter
+ val args = Array(fileName, "--timeout=2")
+ ctx = processOptions(reporter, args.toList)
+
+ // extract information about the program
+// extractInformation(ctx, fileName)
+
+ codeGenerator = new CodeGenerator
+
+ new HoleFinder(fileName).extract match {
+ case Some((matchProgram, matchHole: Hole)) =>
+ program = matchProgram
+ hole = matchHole
+ case None => fail("could not find hole")
+ }
+
+ solver = //new FairZ3Solver(ctx)
+ new TimeoutSolver(new FairZ3Solver(ctx), 2)
+
+ loader = new LeonLoader(program, hole, false)
+ // create new insynth object
+ inSynth = new InSynth(loader, true)
+
+ // save all declarations seen
+ allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+
+ // funDef of the hole
+ holeFunDef = loader.holeDef
+ println("postcondition is: " + holeFunDef.getPostcondition)
+
+ // accumulate precondition for the remaining branch to synthesize
+ accumulatingPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+ // save initial precondition
+ initialPrecondition = accumulatingPrecondition
+ // accumulate the final expression of the hole
+ accumulatingExpression = (finalExp: Expr) => finalExp
+ //accumulatingExpressionMatch = accumulatingExpression
+
+ // each variable of super type can actually have a subtype
+ // get sine declaration maps to be able to refine them
+ val directSubclassMap = loader.directSubclassesMap
+ val variableDeclarations = loader.variableDeclarations
+
+ // map from identifier into a set of possible subclasses
+ variableRefinements = MutableMap.empty
+ for (varDec <- variableDeclarations) {
+ varDec match {
+ case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, LeonVariable(id))) =>
+ variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
+ case _ =>
+ }
+ }
+
+ // calculate cases that should not happen
+ refiner = new Refiner(program, hole, holeFunDef)
+ fine("Refiner recursive call: " + refiner.recurentExpression)
+
+ }
+
+ def synthesize(fileName: String): Unit = {
+ // get start time
+ startTime = System.currentTimeMillis
+
+ initialize(fileName)
+
+ // keeps status of validity
+ var keepGoing = Globals.allSolved match {
+ case Some(true) => false
+ case _ => true
+ }
+
+ var snippets = synthesizeExpressions
+
+ // iterate while the program is not valid
+ import scala.util.control.Breaks._
+ var iteration = 0
+ breakable {
+ while (keepGoing) {
+ // next iteration
+ iteration += 1
+ println("####################################")
+ println("######Iteration #" + iteration + " ###############")
+ println("####################################")
+
+ // just printing of expressions
+ for ((snippetTree, ind) <- (snippets map { _.getSnippet }) zip Iterator.range(0, 500).toStream) {
+ println(ind + " snippetTree is: " + snippetTree)
+ }
+ println("precondition is: " + holeFunDef.precondition.getOrElse(BooleanLiteral(true)))
+ println("accumulatingPrecondition is: " + accumulatingPrecondition)
+ println("accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
+ // System.out.println("Press Any Key To Continue...");
+ // new java.util.Scanner(System.in).nextLine();
+
+ // found precondition?
+ found = false
+ // try to find it
+ breakable {
+ // go through all snippets
+ for (
+ snippet <- snippets /*filter { _.getSnippet.toString == "concat(Nil(), Nil())" }*/ ;
+ val snippetTree = snippet.getSnippet
+ ) {
+ // debugging
+ println("snippetTree is: " + snippetTree)
+ snippetTree.toString match {
+ case "Cons(l1.head, concat(l1.tail, l2))" |
+ "Cons(l1.head, concat(l2, l1.tail))" |
+ "Cons(l2.head, concat(l2.tail, l1))" |
+ "Cons(l2.head, concat(l1, l2.tail))" =>
+ println("snippetTree is: " + snippetTree)
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
+ case _ =>
+ }
+
+ // System.out.println("Press Any Key To Continue...");
+ // new java.util.Scanner(System.in).nextLine();
+
+ // skip pure recursive call
+ if (!refiner.isAvoidable(snippetTree)) {
+ if (tryToSynthesizeBranch(snippetTree)) {
+ break
+ }
+ } else {
+ println("We are skipping this snippetTree: " + snippetTree)
+ }
+
+ } // for (snippet <- snippets
+ } // breakable { for (snippet <- snippets
+
+ // if did not found for any of the branch expressions
+ if (found) {
+ info("we are done !")
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
+ return
+ }
+
+ val inSynth = new InSynth(allDeclarations, hole.desiredType, true)
+ snippets = inSynth.getExpressions
+
+ }
+ } //breakable { while (!keepGoing) {
+
+ // get end time
+ val endTime = System.currentTimeMillis
+ println("whole process took time: " + (endTime - startTime))
+
+ }
+
+ def tryToSynthesizeBranch(snippetTree: Expr): Boolean = {
+ import leon.purescala.TreeOps.searchAndReplaceDFS
+ // replace hole in the body with current snippet tree
+
+ // val oldBody = holeFunDef.getBody
+ // val newBody = searchAndReplaceDFS(
+ // _ match {
+ // case _: Hole => Some(snippetTree)
+ // case _ => None
+ // })(oldBody)
+ val oldBody = holeFunDef.getBody
+ val newBody = accumulatingExpression(snippetTree)
+
+ holeFunDef.body = Some(newBody)
+ // save old precondition
+ val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+
+ holeFunDef.precondition = Some(initialPrecondition)
+
+ // analyze the program
+ println("analyzing program for funDef:" + holeFunDef)
+
+ snippetTree.setType(hole.desiredType)
+ holeFunDef.getBody.setType(hole.desiredType)
+
+ analyzeProgram(program)
+
+ // check if solver could solved this instance
+ if (Globals.allSolved == Some(true)) {
+ // mark the branch found
+ found = true
+
+ println("Wooooooow we have a winner!")
+ println("************************************")
+ println("*********And the winner is**********")
+ println(accumulatingExpression(snippetTree))
+ println("************************************")
+
+ // get end time
+ val endTime = System.currentTimeMillis
+ println("whole process took time: " + (endTime - startTime))
+ //println("verTime, testTime" + verTime + ", " + ExampleRunner.testTime)
+
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
+
+ return true
+ }
+
+ // store appropriate values here, will be update in a finally branch
+ var bodyToRestore = oldBody
+ var preconditionToRestore = Some(oldPrecondition)
+
+ // because first initial test
+ holeFunDef.precondition = preconditionToRestore
+
+ // debug
+ println("Going to generating counterexamples: " + holeFunDef)
+ // System.out.println("Press Any Key To Continue...");
+ // new java.util.Scanner(System.in).nextLine();
+
+ // println("Counterexample cheking: ")
+ // println("Counterexamples: " + ExampleRunner.counterExamples.mkString("\n"))
+ // val counterExampleCheck = ExampleRunner.check(BooleanLiteral(true), newBody, holeFunDef.getPostcondition)
+ // println("Result of check: " + counterExampleCheck )
+ //
+ val temp = System.currentTimeMillis
+ // get counterexamples
+ val (maps, precondition) = generateCounterexamples(program, holeFunDef, 5)
+ val temptime = System.currentTimeMillis - temp
+ println("gen counterexamples took " + temptime)
+ verTime += temptime
+
+ // collect (add) counterexamples
+ //ExampleRunner.counterExamples ++= maps
+
+ val keepGoing = Globals.allSolved match {
+ case Some(true) => false
+ case _ => true
+ }
+
+ // if no counterexamples and all are solved, we are done
+ if (maps.isEmpty && !keepGoing) {
+ // mark the branch found
+ found = true
+
+ println("Wooooooow we have a winner!")
+ println("************************************")
+ println("*********And the winner is**********")
+ println(accumulatingExpression(snippetTree))
+ println("************************************")
+
+ return true
+ }
+
+ // will modify funDef body and precondition, restore it later
+ try {
+ // TODO is this okay?
+ // if there are no returned counterexamples just go to the next snippet
+ // and so far counter examples passed
+ if (!maps.isEmpty /*&& counterExampleCheck */ ) {
+ // proceed with synthesizing boolean expressions
+ assertEquals(5, maps.size)
+ // set program to the solver
+ solver.setProgram(program)
+
+ // initialize builder with previously seen declarations
+ val newBuilder = new InitialEnvironmentBuilder
+ newBuilder.addDeclarations(allDeclarations)
+
+ fine("all declarations now, size: " + newBuilder.getAllDeclarations.size)
+
+ // synthesize solution
+ val queryBuilder = new LeonQueryBuilder(BooleanType)
+ val query = queryBuilder.getQuery
+ val engine = new Engine(newBuilder, query, new WeightScheduler(), TimeOut(Config.getTimeOutSlot))
+ val solution = engine.run()
+ assertNotNull(solution)
+
+ assertNotNull(codeGenerator)
+ assertNotNull(allDeclarations)
+ // reconstruct (only defined number of boolean expressions)
+ val innerSnippets = Reconstructor(solution.getNodes.head, codeGenerator, true) take numberOfBooleanSnippets
+ checkDeclarations(inSynth)
+
+ // debugging
+ for ((snippetTree, ind) <- (innerSnippets map { _.getSnippet }) zip Iterator.range(0, 20).toStream) {
+ println(ind + " boolean snippetTree is: " + snippetTree)
+ }
+ // System.out.println("Press Any Key To Continue...");
+ // new java.util.Scanner(System.in).nextLine();
+
+ // precondition found?
+ found = false
+
+ // iterate over boolean snippets
+ val iterator = innerSnippets.iterator
+ while (!found && iterator.hasNext) {
+ val innerSnippetTree = iterator.next.getSnippet
+
+ // debug
+ println("boolean snippet is: " + innerSnippetTree)
+ // System.out.println("Press Any Key To Continue...");
+ // new java.util.Scanner(System.in).nextLine();
+
+ val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, precondition)
+
+ //found = innerFound
+ innerPrec match {
+ case s @ Some(_) =>
+ preconditionToRestore = s
+ case _ =>
+ }
+
+ if (innerFound)
+ return true
+
+ } // iterating over all boolean solutions
+
+ // if none of boolean solutions work, restore body (in finally)
+ //holeFunDef.body = Some(oldBody)
+
+ assertTrue(!found)
+ info("not found :(, we give up on this branch expression")
+ return false
+
+ } // if ( !maps.isEmpty ) {
+
+ false
+ } // try
+ finally {
+ // set these to the FunDef
+ holeFunDef.precondition = preconditionToRestore
+ // restore old body (we accumulate expression)
+ holeFunDef.body = Some(oldBody)
+ }
+ }
+
+ def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: Expr): (Boolean, Option[Expr]) = {
+
+ // debug
+ // println("boolean snippet is: " + innerSnippetTree)
+ // System.out.println("Press Any Key To Continue...");
+ // new java.util.Scanner(System.in).nextLine();
+
+ // new condition together with existing precondition
+ val newCondition = And(Seq(accumulatingPrecondition, innerSnippetTree))
+
+ // new expression should not be false
+ val notFalseEquivalence = Not(newCondition)
+ val notFalseSolveReturn = solver.solve(notFalseEquivalence)
+ fine("solve for not false returned: " + notFalseSolveReturn)
+ notFalseSolveReturn match {
+ case Some(true) =>
+ (false, None)
+ case None =>
+ (false, None)
+ // nothing here
+ // here, our expression is not contradictory, continue
+ case Some(false) =>
+ // check if synthesized boolean expression implies precondition (counterexamples)
+ val implyExpression = Implies(newCondition, precondition)
+ fine("implyExpression is: " + implyExpression)
+
+ // check if synthesized condition implies counter-examples
+ val solveReturn = solver.solve(implyExpression)
+ fine("solve returned: " + solveReturn)
+
+ solveReturn match {
+ case Some(true) =>
+ // old precondition is not here, it is before counterexamples are derived!
+ //val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+
+ // if expression implies counterexamples add it to the precondition and try to validate program
+ holeFunDef.precondition = Some(newCondition)
+ // do analysis
+ analyzeProgram(program)
+ // program is valid, we have a branch
+ if (Globals.allSolved == Some(true)) {
+ // we found a branch
+ info("Wow! we found a branch!")
+
+ // update accumulating expression
+ val oldAccumulatingExpression = accumulatingExpression
+ val newAccumulatingExpression =
+ (finalExpr: Expr) =>
+ oldAccumulatingExpression({
+ val innerIf = IfExpr(innerSnippetTree, snippetTree, finalExpr)
+ innerIf.setType(snippetTree.getType)
+ innerIf
+ })
+
+ accumulatingExpression = newAccumulatingExpression
+
+ // update accumulating precondition
+ fine("updating accumulatingPrecondition")
+ accumulatingPrecondition = And(Seq(accumulatingPrecondition, Not(innerSnippetTree)))
+ fine("updating hole fun precondition and body (to be hole)")
+
+ // set to set new precondition
+ val preconditionToRestore = Some(accumulatingPrecondition)
+
+ // check for refinements
+ checkRefinements(innerSnippetTree) match {
+ case Some(refinementPair @ (id, classType)) =>
+ fine("And now we have refinement type: " + refinementPair)
+ fine("variableRefinements(id) before" + variableRefinements(id))
+ variableRefinements(id) -= loader.classMap(classType.id)
+ fine("variableRefinements(id) after" + variableRefinements(id))
+
+ // if we have a single subclass possible to refine
+ if (variableRefinements(id).size == 1) {
+ fine("wow we an do variable refinement for " + id)
+
+ val newType = variableRefinements(id).head
+ fine("new type is: " + newType)
+
+ // update declarations
+ allDeclarations =
+ for (dec <- allDeclarations)
+ yield dec match {
+ case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, LeonVariable(`id`))) =>
+ LeonDeclaration(
+ imex, TypeTransformer(newType), newType)
+ case _ =>
+ dec
+ }
+
+ } else
+ fine("we cannot do variable refinement :(")
+ case _ =>
+ }
+ // found a boolean snippet, break
+ (true, preconditionToRestore)
+ } else {
+ // reset funDef and continue with next boolean snippet
+ val preconditionToRestore = Some(accumulatingPrecondition)
+ (false, preconditionToRestore)
+ }
+
+ case _ =>
+ println("precondition was not applied")
+ (false, None)
+ } //solveReturn match { (for implying counterexamples)
+ } // notFalseSolveReturn match {
+ }
+
+ // inspect the expression if some refinements can be done
+ def checkRefinements(expr: Expr) = expr match {
+ case CaseClassInstanceOf(classDef, LeonVariable(id)) =>
+ Some((id, classDef))
+ case _ =>
+ None
+ }
+
+ def extractInformation(ctx: LeonContext, file: String) =
+ new HoleFinder(file).extract
+
+ // assert that there is not function that returns a function
+ def checkDeclarations(inSynth: InSynth) = {
+ assertFalse(
+ "We should not have a declaration which returns a function (not valid in Leon)",
+ (false /: inSynth.getCurrentBuilder.getAllDeclarations) {
+ case (res, dec: LeonDeclaration) =>
+ res ||
+ (dec.getDomainType match {
+ case FunctionType(_, _: FunctionType) => true
+ case _ => false
+ })
+ })
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/TryOutTestWithFiltering.scala b/src/test/scala/lesynth/TryOutTestWithFiltering.scala
new file mode 100644
index 000000000..3c65777d0
--- /dev/null
+++ b/src/test/scala/lesynth/TryOutTestWithFiltering.scala
@@ -0,0 +1,768 @@
+//package lesynth
+//
+//import org.junit.Assert._
+//import org.junit.{ Test, Ignore }
+//
+//import scala.collection.mutable.{ Map => MutableMap }
+//import scala.collection.mutable.{ Set => MutableSet }
+//import scala.collection.mutable.{ LinkedList => MutableList }
+//import scala.util.matching.Regex
+//import scala.collection.mutable.PriorityQueue
+//
+//import scala.tools.nsc.{ Settings => NSCSettings, MainGenericRunner }
+//
+//import leon.{ Main => LeonMain, DefaultReporter, Settings, LeonContext }
+//import leon.solvers.{ Solver, TimeoutSolver }
+//import leon.solvers.z3.{ FairZ3Solver }
+//import leon.verification.AnalysisPhase
+//import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
+//import leon.purescala.Trees.{ Variable => LeonVariable, _ }
+//import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+//import leon.purescala.Common.{ Identifier, FreshIdentifier }
+//import leon.purescala.TreeOps
+//import leon.plugin.ExtractionPhase
+//
+//import insynth.util.logging.HasLogger
+//import insynth.interfaces.Declaration
+//import insynth.InSynth
+//import insynth.reconstruction.codegen.CodeGenerator
+//import insynth.leon.loader.LeonLoader
+//import insynth.leon.LeonDeclaration
+//import insynth.leon.ImmediateExpression
+//import insynth.engine.InitialEnvironmentBuilder
+//import insynth.leon.LeonQueryBuilder
+//import insynth.interfaces.{ Loader, Declaration, QueryBuilder }
+//import insynth.engine.{ Engine, InitialEnvironmentBuilder }
+//import insynth.engine.scheduler.WeightScheduler
+//import insynth.structures.ContainerNode
+//import insynth.util.TimeOut
+//import insynth.Config
+//import insynth.reconstruction.Reconstructor
+//import insynth.leon.TypeTransformer
+//import insynth.leon.HoleFinder
+//
+//class TryOutTest extends HasLogger {
+//
+// def analyzeProgram(program: Program) {
+// import leon.Main._
+//
+// val temp = System.currentTimeMillis
+// Globals.allSolved = Some(true)
+//
+// val reporter = new DefaultReporter()
+// val args = Array("no file!", "--timeout=2")
+// val ctx = processOptions(reporter, args.toList)
+//
+// AnalysisPhase.run(ctx)(program)
+//
+// val time = System.currentTimeMillis - temp
+// println("analysis took " + time)
+// verTime += time
+// }
+//
+// def generateCounterexamples(program: Program, funDef: FunDef, number: Int): (Seq[Map[Identifier, Expr]], Expr) = {
+//
+// fine("generate counter examples with funDef.prec= " + funDef.precondition.getOrElse(BooleanLiteral(true)))
+//
+// // get current precondition
+// var precondition = funDef.precondition.getOrElse(BooleanLiteral(true))
+// // where we will accumulate counterexamples as sequence of maps
+// var maps: Seq[Map[Identifier, Expr]] = Seq.empty
+//
+// // iterate specific number of times or until no further counterexample can be generated
+// var changed = true
+// var ind = 0
+// while (ind < number && changed) {
+//
+// // analyze the program
+// analyzeProgram(program)
+//
+// // check if solver could solved this instance
+// if (Globals.allSolved == Some(false) && !Globals.asMap.isEmpty) {
+//
+// fine("found coounterexample: " + Globals.asMap)
+//
+// // add current counterexample
+// maps :+= Globals.asMap
+// // prevent this counterexample to reoccur
+// val precAddition = Not(And(Globals.asMap map { case (id, value) => Equals(LeonVariable(id), value) } toSeq))
+// precondition = And(Seq(precondition, precAddition))
+// funDef.precondition = Some(precondition)
+// } else
+// changed = false
+//
+// ind += 1
+// }
+//
+// // return found counterexamples and the formed precondition
+// (maps, precondition)
+// }
+//
+// // assert that there is not function that returns a function
+// def checkDeclarations(inSynth: InSynth) = {
+// assertFalse(
+// "We should not have a declaration which returns a function (not valid in Leon)",
+// (false /: inSynth.getCurrentBuilder.getAllDeclarations) {
+// case (res, dec: LeonDeclaration) =>
+// res ||
+// (dec.getDomainType match {
+// case FunctionType(_, _: FunctionType) => true
+// case _ => false
+// })
+// })
+// }
+//
+// def assertL1L2Refinements(variableRefinements: MutableMap[Identifier, MutableSet[ClassType]]) =
+// for (
+// pair @ (varName, nameSet) <- List(
+// ("l2", Set("Nil", "Cons")),
+// ("l1", Set("Nil", "Cons")))
+// ) assertTrue(
+// "pair " + pair + " not found. Found: " + variableRefinements.mkString(", "),
+// (false /: variableRefinements) {
+// (res, extr) =>
+// extr match {
+// case (id, classTypeSet) => res ||
+// (
+// id.name == varName &&
+// (true /: nameSet) {
+// (res, innerName) => res && classTypeSet.exists(_.classDef.id.name == innerName)
+// })
+// case _ => false
+// }
+// })
+//
+// private var program: Program = _
+//
+// private var hole: Hole = _
+// private var holeFunDef: FunDef = _
+//
+// private var allDeclarations: List[Declaration] = _
+//
+// private var loader: LeonLoader = _
+//
+// private var inSynth: InSynth = _
+// private var codeGenerator: CodeGenerator = _
+//
+// private var refiner: Refiner = _
+//
+// // accumulate precondition for the remaining branch to synthesize
+// private var accumulatingPrecondition: Expr = _
+// // accumulate the final expression of the hole
+// private var accumulatingExpression: Expr => Expr = _
+// private var accumulatingExpressionMatch: Expr => Expr = _
+//
+// var solver: Solver = _
+// //
+// var ctx: LeonContext = _
+// //
+// var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = _
+//
+// var initialPrecondition: Expr = _
+//
+// var startTime: Long = _
+//
+// var verTime: Long = 0
+// var synTime: Long = 0
+//
+// // number of condition expressions to try before giving up on that branch expression
+// val numberOfBooleanSnippets = 20
+//
+// def introduceCounterExamples = {
+// var argumentIds = holeFunDef.args.map(_.id)
+// assertEquals(2, argumentIds.size)
+//
+// Globals.hole.getType match {
+// case ct: ClassType =>
+// val leonLoader = LeonLoader(program, hole, false)
+//
+// leonLoader.load
+//
+// val setSubclasses = leonLoader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
+// assertEquals(2, setSubclasses.size)
+//
+// val (nilClassSet, consClassSet) = setSubclasses.partition(_.fieldsIds.size == 0)
+// assertEquals(1, nilClassSet.size)
+//
+// val nilClass = nilClassSet.head
+// val consClass = consClassSet.head
+//
+// var counter = 0
+// def getIntLiteral = { counter += 1; IntLiteral(counter) }
+//
+// val list0 = () => CaseClass(nilClass, Nil)
+// val list1 = () => CaseClass(consClass, getIntLiteral :: list0() :: Nil)
+// val list2 = () => CaseClass(consClass, getIntLiteral :: list1() :: Nil)
+// val list3 = () => CaseClass(consClass, getIntLiteral :: list2() :: Nil)
+// val list4 = () => CaseClass(consClass, getIntLiteral :: list3() :: Nil)
+//
+// val lists = List(list0, list1, list2, list3 /*, list4*/ )
+//
+// for (l1 <- lists; l2 <- lists) {
+// ExampleRunner.counterExamples :+=
+// Map(argumentIds(0) -> l1(),
+// argumentIds(1) -> l2())
+// }
+// case _ =>
+// fail
+// }
+//
+// }
+//
+// def synthesizeExpressions =
+// inSynth.getExpressions
+//
+// def initialize(fileName: String) = {
+//
+// import leon.Main._
+//
+// val reporter = new DefaultReporter
+// val args = Array(fileName, "--timeout=2")
+// ctx = processOptions(reporter, args.toList)
+//
+// // extract information about the program
+// extractInformation(ctx, fileName)
+//
+// codeGenerator = new CodeGenerator
+//
+// // program and hole objects should be extracted
+// (Globals.program, Globals.hole) match {
+// case (Some(matchProgram), matchHole: Hole) =>
+// program = matchProgram
+// hole = matchHole
+//
+// solver = //new FairZ3Solver(ctx)
+// new TimeoutSolver(new FairZ3Solver(ctx), Globals.timeout)
+//
+// loader = new LeonLoader(program, hole, false)
+// // create new insynth object
+// inSynth = new InSynth(loader, true)
+//
+// // save all declarations seen
+// allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+//
+// // funDef of the hole
+// holeFunDef = Globals.holeFunDef
+// println("postcondition is: " + holeFunDef.getPostcondition)
+//
+// // accumulate precondition for the remaining branch to synthesize
+// accumulatingPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+// // save initial precondition
+// initialPrecondition = accumulatingPrecondition
+// // accumulate the final expression of the hole
+// accumulatingExpression = (finalExp: Expr) => finalExp
+// accumulatingExpressionMatch = accumulatingExpression
+//
+// // each variable of super type can actually have a subtype
+// // get sine declaration maps to be able to refine them
+// val directSubclassMap = loader.directSubclassesMap
+// val variableDeclarations = loader.variableDeclarations
+//
+// // map from identifier into a set of possible subclasses
+// variableRefinements = MutableMap.empty
+// for (varDec <- variableDeclarations) {
+// varDec match {
+// case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, LeonVariable(id))) =>
+// variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
+// case _ =>
+// }
+// }
+//
+// // calculate cases that should not happen
+// refiner = new Refiner(program, hole)
+// fine("Refiner recursive call: " + refiner.recurentExpression)
+// case _ => fail()
+// }
+// }
+//
+// @Test
+// def test1 {
+// synthesize("testcases/insynth/ListOperationsHole.scala")
+// }
+//
+// def synthesize(fileName: String): Unit = {
+// // get start time
+// startTime = System.currentTimeMillis
+//
+// initialize(fileName)
+//
+// // keeps status of validity
+// var keepGoing = Globals.allSolved match {
+// case Some(true) => false
+// case _ => true
+// }
+//
+// var snippets = synthesizeExpressions
+//
+// introduceCounterExamples
+// println("counterexamples after introduce: " + ExampleRunner.counterExamples.mkString("\n"))
+//
+// // iterate while the program is not valid
+// import scala.util.control.Breaks._
+// var iteration = 0
+// breakable {
+// while (keepGoing) {
+// // next iteration
+// iteration += 1
+// println("####################################")
+// println("######Iteration #" + iteration + " ###############")
+// println("####################################")
+//
+// // just printing of expressions
+// // for ((snippetTree, ind) <- (snippets map { _.getSnippet }) zip Iterator.range(0, 20).toStream) {
+// // println(ind + " snippetTree is: " + snippetTree)
+// // }
+// println("precondition is: " + holeFunDef.precondition.getOrElse(BooleanLiteral(true)))
+// println("accumulatingPrecondition is: " + accumulatingPrecondition)
+// println("accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+//
+// var pq = new PriorityQueue[(Expr, Int)]()(
+// new Ordering[(Expr, Int)] {
+// def compare(pair1: (Expr, Int), pair2: (Expr, Int)) =
+// pair1._2.compare(pair2._2)
+// })
+// var tested = 0
+//
+// // found precondition?
+// var found = false
+// // try to find it
+// breakable {
+// // go through all snippets
+// for (
+// snippet <- snippets /*filter { _.getSnippet.toString == "concat(Nil(), Nil())" }*/ ;
+// val snippetTree = snippet.getSnippet
+// ) {
+// // debugging
+// println("snippetTree is: " + snippetTree)
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+//
+// // TODO is never empty now with introduce
+// val passCount =
+// //if (ExampleRunner.counterExamples.isEmpty)
+// if (iteration == 1)
+// ExampleRunner.counterExamples.size
+// else {
+//
+// val oldPreconditionSaved = holeFunDef.precondition
+// val oldBodySaved = holeFunDef.body
+//
+// // restore initial precondition
+// holeFunDef.precondition = Some(initialPrecondition)
+//
+// assertEquals(BooleanLiteral(true), initialPrecondition)
+//
+// // get the whole body (if else...)
+// val accumulatedExpression = accumulatingExpression(snippetTree)
+// // set appropriate body to the function for the correct evaluation
+// holeFunDef.body = Some(accumulatedExpression)
+//
+// // if (snippetTree.toString == "Cons(l2.head, concat(l1, l2.tail))") {
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+// // }
+// val count = ExampleRunner.countPassed(accumulatedExpression)
+//
+// // if (snippetTree.toString == "Cons(l2.head, concat(l1, l2.tail))") {
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+// // }
+//
+// holeFunDef.precondition = oldPreconditionSaved
+// holeFunDef.body = oldBodySaved
+//
+// count
+// }
+//
+// val okay =
+// passCount == ExampleRunner.counterExamples.size
+// if (!okay) {
+// // println("snippet with pass count filtered: " + (snippet, passCount))
+// pq.enqueue((snippetTree, 100 + (passCount * (iteration - 1)) - snippet.getWeight.toInt))
+// }
+//
+// // skip pure recursive call
+// if (!refiner.isAvoidable(snippetTree) && okay) {
+// if (tryToSynthesizeBranch(snippetTree)) {
+// found = true
+// pq.clear
+// break
+// }
+// } else {
+// // println("We are skipping this snippetTree since it is the recursive call: " + Refiner.recurentExpressions)
+// }
+//
+// if (tested >= 500) {
+// println("queue is: " + pq.mkString("\n"))
+// println("head of queue is: " + pq.head)
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+// for (i <- 1 to 5) {
+// val nextSnippet = pq.dequeue._1
+// println("nextSnippet is: " + nextSnippet)
+//
+// if (tryToSynthesizeBranch(nextSnippet)) {
+// found = true
+// pq.clear
+// break
+// }
+// }
+// tested = 0
+// } else
+// tested += 1
+// } // for (snippet <- snippets
+// } // breakable { for (snippet <- snippets
+//
+// // if did not found for any of the branch expressions
+// if (!found) {
+// info("we are done :(")
+// return
+// }
+//
+// // debug
+// assertTrue(found)
+// info("variable declarations now:")
+// info(allDeclarations.filter(
+// _ match {
+// case LeonDeclaration(_, _, _, imex @ ImmediateExpression(_, _: LeonVariable)) =>
+// true
+// case _ =>
+// false
+// }).mkString(" ,"))
+//
+// info("okay we found one branch")
+//
+// // synthesize snippets for next branch
+// info("synthesizing new snippets")
+//
+// val newBuilder = new InitialEnvironmentBuilder
+// newBuilder.addDeclarations(allDeclarations)
+// fine("all declarations now, size: " + newBuilder.getAllDeclarations.size)
+// val queryBuilder = new LeonQueryBuilder(hole.desiredType)
+// val query = queryBuilder.getQuery
+// val engine = new Engine(newBuilder, query, new WeightScheduler(), TimeOut(Config.getTimeOutSlot))
+// val proofTree = engine.run()
+// assertNotNull(proofTree)
+// assertEquals(1, proofTree.getNodes.size)
+//
+// println("filtering based on: " + holeFunDef.precondition.get)
+// println("counterexamples before filter: " + ExampleRunner.counterExamples.size)
+// ExampleRunner.filter(holeFunDef.precondition.get)
+// println("counterexamples after filter: " + ExampleRunner.counterExamples.size)
+// println("counterexamples after filter: " + ExampleRunner.counterExamples.mkString("\n"))
+//
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+//
+// snippets = Reconstructor(proofTree.getNodes.head, codeGenerator)
+//
+// // ADHOC filter out counterexamples that have Nil (adhoc!)
+// // ExampleRunner.counterExamples = ExampleRunner.counterExamples filterNot {
+// // map =>
+// // (false /: map.values) {
+// // (res, value) =>
+// // res || value.toString.startsWith("Nil")
+// // }
+// // }
+//
+// }
+// } //breakable { while (!keepGoing) {
+//
+// // get end time
+// val endTime = System.currentTimeMillis
+// println("whole process took time: " + (endTime - startTime))
+//
+// }
+//
+// def tryToSynthesizeBranch(snippetTree: Expr): Boolean = {
+// import leon.purescala.TreeOps.searchAndReplaceDFS
+// // replace hole in the body with current snippet tree
+//
+// // val oldBody = holeFunDef.getBody
+// // val newBody = searchAndReplaceDFS(
+// // _ match {
+// // case _: Hole => Some(snippetTree)
+// // case _ => None
+// // })(oldBody)
+// val oldBody = holeFunDef.getBody
+// val newBody = accumulatingExpressionMatch(snippetTree)
+//
+// holeFunDef.body = Some(newBody)
+// // save old precondition
+// val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+//
+// holeFunDef.precondition = Some(initialPrecondition)
+//
+// // analyze the program
+// analyzeProgram(program)
+//
+// // check if solver could solved this instance
+// if (Globals.allSolved == Some(true)) {
+// // mark the branch found
+// //found = true
+//
+// println("Wooooooow we have a winner!")
+// println("************************************")
+// println("*********And the winner is**********")
+// println(accumulatingExpression(snippetTree))
+// println("************************************")
+//
+// // get end time
+// val endTime = System.currentTimeMillis
+// println("whole process took time: " + (endTime - startTime))
+// //println("verTime, testTime" + verTime + ", " + ExampleRunner.testTime)
+//
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
+//
+// return true
+// }
+//
+// // store appropriate values here, will be update in a finally branch
+// var bodyToRestore = oldBody
+// var preconditionToRestore = Some(oldPrecondition)
+//
+// // because first initial test
+// holeFunDef.precondition = preconditionToRestore
+//
+// // debug
+// println("Going to generating counterexamples: " + holeFunDef)
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+//
+// // println("Counterexample cheking: ")
+// // println("Counterexamples: " + ExampleRunner.counterExamples.mkString("\n"))
+// // val counterExampleCheck = ExampleRunner.check(BooleanLiteral(true), newBody, holeFunDef.getPostcondition)
+// // println("Result of check: " + counterExampleCheck )
+// //
+// val temp = System.currentTimeMillis
+// // get counterexamples
+// val (maps, precondition) = generateCounterexamples(program, holeFunDef, 5)
+// val temptime = System.currentTimeMillis - temp
+// println("gen counterexamples took " + temptime)
+// verTime += temptime
+//
+// // collect (add) counterexamples
+// //ExampleRunner.counterExamples ++= maps
+//
+// val keepGoing = Globals.allSolved match {
+// case Some(true) => false
+// case _ => true
+// }
+//
+// // if no counterexamples and all are solved, we are done
+// if (maps.isEmpty && !keepGoing) {
+// // mark the branch found
+// //found = true
+//
+// println("Wooooooow we have a winner!")
+// println("************************************")
+// println("*********And the winner is**********")
+// println(accumulatingExpression(snippetTree))
+// println("************************************")
+//
+// return true
+// }
+//
+// // will modify funDef body and precondition, restore it later
+// try {
+// // TODO is this okay?
+// // if there are no returned counterexamples just go to the next snippet
+// // and so far counter examples passed
+// if (!maps.isEmpty /*&& counterExampleCheck */ ) {
+// // proceed with synthesizing boolean expressions
+// assertEquals(5, maps.size)
+// // set program to the solver
+// solver.setProgram(program)
+//
+// // initialize builder with previously seen declarations
+// val newBuilder = new InitialEnvironmentBuilder
+// newBuilder.addDeclarations(allDeclarations)
+//
+// fine("all declarations now, size: " + newBuilder.getAllDeclarations.size)
+//
+// // synthesize solution
+// val queryBuilder = new LeonQueryBuilder(BooleanType)
+// val query = queryBuilder.getQuery
+// val engine = new Engine(newBuilder, query, new WeightScheduler(), TimeOut(Config.getTimeOutSlot))
+// val solution = engine.run()
+// assertNotNull(solution)
+//
+// assertNotNull(codeGenerator)
+// assertNotNull(allDeclarations)
+// // reconstruct (only defined number of boolean expressions)
+// val innerSnippets = Reconstructor(solution.getNodes.head, codeGenerator) take numberOfBooleanSnippets
+// checkDeclarations(inSynth)
+//
+// // debugging
+// // for ((snippetTree, ind) <- (innerSnippets map { _.getSnippet }) zip Iterator.range(0, 20).toStream) {
+// // println(ind + " boolean snippetTree is: " + snippetTree)
+// // }
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+//
+// // precondition found?
+// var found = false
+//
+// // iterate over boolean snippets
+// val iterator = innerSnippets.iterator
+// while (!found && iterator.hasNext) {
+// val innerSnippetTree = iterator.next.getSnippet
+//
+// // debug
+// println("boolean snippet is: " + innerSnippetTree)
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+//
+// val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(snippetTree, innerSnippetTree, precondition)
+//
+// found = innerFound
+// innerPrec match {
+// case s @ Some(_) =>
+// preconditionToRestore = s
+// case _ =>
+// }
+//
+// if (found)
+// return true
+//
+// } // iterating over all boolean solutions
+//
+// // if none of boolean solutions work, restore body (in finally)
+// //holeFunDef.body = Some(oldBody)
+//
+// assertTrue(!found)
+// info("not found :(, we give up on this branch expression")
+// return false
+//
+// } // if ( !maps.isEmpty ) {
+//
+// false
+// } // try
+// finally {
+// // set these to the FunDef
+// holeFunDef.precondition = preconditionToRestore
+// // restore old body (we accumulate expression)
+// holeFunDef.body = Some(oldBody)
+// }
+// }
+//
+// def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr, precondition: Expr): (Boolean, Option[Expr]) = {
+//
+// // debug
+// // println("boolean snippet is: " + innerSnippetTree)
+// // System.out.println("Press Any Key To Continue...");
+// // new java.util.Scanner(System.in).nextLine();
+//
+// // new condition together with existing precondition
+// val newCondition = And(Seq(accumulatingPrecondition, innerSnippetTree))
+//
+// // new expression should not be false
+// val notFalseEquivalence = Not(newCondition)
+// val notFalseSolveReturn = solver.solve(notFalseEquivalence)
+// fine("solve for not false returned: " + notFalseSolveReturn)
+// notFalseSolveReturn match {
+// case Some(true) =>
+// (false, None)
+// case None =>
+// (false, None)
+// // nothing here
+// // here, our expression is not contradictory, continue
+// case Some(false) =>
+// // check if synthesized boolean expression implies precondition (counterexamples)
+// val implyExpression = Implies(newCondition, precondition)
+// fine("implyExpression is: " + implyExpression)
+//
+// // check if synthesized condition implies counter-examples
+// val solveReturn = solver.solve(implyExpression)
+// fine("solve returned: " + solveReturn)
+//
+// solveReturn match {
+// case Some(true) =>
+// // old precondition is not here, it is before counterexamples are derived!
+// //val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
+//
+// // if expression implies counterexamples add it to the precondition and try to validate program
+// holeFunDef.precondition = Some(newCondition)
+// // do analysis
+// analyzeProgram(program)
+// // program is valid, we have a branch
+// if (Globals.allSolved == Some(true)) {
+// // we found a branch
+// info("Wow! we found a branch!")
+//
+// // update accumulating expression
+// val oldAccumulatingExpression = accumulatingExpression
+// val newAccumulatingExpression =
+// (finalExpr: Expr) =>
+// oldAccumulatingExpression(IfExpr(innerSnippetTree, snippetTree, finalExpr))
+//
+// accumulatingExpression = newAccumulatingExpression
+//
+// // update accumulating precondition
+// fine("updating accumulatingPrecondition")
+// accumulatingPrecondition = And(Seq(accumulatingPrecondition, Not(innerSnippetTree)))
+// fine("updating hole fun precondition and body (to be hole)")
+//
+// // set to set new precondition
+// val preconditionToRestore = Some(accumulatingPrecondition)
+//
+// // check for refinements
+// checkRefinements(innerSnippetTree) match {
+// case Some(refinementPair @ (id, classType)) =>
+// fine("And now we have refinement type: " + refinementPair)
+// fine("variableRefinements(id) before" + variableRefinements(id))
+// variableRefinements(id) -= loader.classMap(classType.id)
+// fine("variableRefinements(id) after" + variableRefinements(id))
+//
+// // if we have a single subclass possible to refine
+// if (variableRefinements(id).size == 1) {
+// fine("wow we an do variable refinement for " + id)
+//
+// val newType = variableRefinements(id).head
+// fine("new type is: " + newType)
+//
+// // update declarations
+// allDeclarations =
+// for (dec <- allDeclarations)
+// yield dec match {
+// case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, LeonVariable(`id`))) =>
+// LeonDeclaration(
+// imex, TypeTransformer(newType), newType)
+// case _ =>
+// dec
+// }
+//
+// } else
+// fine("we cannot do variable refinement :(")
+// case _ =>
+// }
+// // found a boolean snippet, break
+// (true, preconditionToRestore)
+// } else {
+// // reset funDef and continue with next boolean snippet
+// val preconditionToRestore = Some(accumulatingPrecondition)
+// (false, preconditionToRestore)
+// }
+//
+// case _ =>
+// println("precondition was not applied")
+// (false, None)
+// } //solveReturn match { (for implying counterexamples)
+// } // notFalseSolveReturn match {
+// }
+//
+// // inspect the expression if some refinements can be done
+// def checkRefinements(expr: Expr) = expr match {
+// case CaseClassInstanceOf(classDef, LeonVariable(id)) =>
+// Some((id, classDef))
+// case _ =>
+// None
+// }
+//
+// def extractInformation(ctx: LeonContext, file: String) =
+// new HoleFinder(file).extract
+//
+//}
\ No newline at end of file
diff --git a/testcases/lesynth/InsertionSortFull.scala b/testcases/lesynth/InsertionSortFull.scala
new file mode 100644
index 000000000..6b68a439e
--- /dev/null
+++ b/testcases/lesynth/InsertionSortFull.scala
@@ -0,0 +1,51 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ def size(l : List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def sortedIns(e: Int, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) =>
+ if (x <= e) Cons(x,sortedIns(e, xs))
+ else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+}
diff --git a/testcases/lesynth/InsertionSortHoleInsert.scala b/testcases/lesynth/InsertionSortHoleInsert.scala
new file mode 100644
index 000000000..cde3aaacd
--- /dev/null
+++ b/testcases/lesynth/InsertionSortHoleInsert.scala
@@ -0,0 +1,54 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ def size(l : List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def sortedIns(e: Int, l: List): List = {
+ require(isSorted(l))
+ hole(l)
+// val cond1: Boolean = /*!*/
+// l match {
+// case Nil() => /*!*/ // Cons(e,Nil())
+// case Cons(x,xs) =>
+// val cond2: Boolean = /*!*/
+// if (x <= e) /*!*/ // Cons(x,sortedIns(e, xs))
+// else /*!*/ // Cons(e, l)
+// }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+}
diff --git a/testcases/lesynth/InsertionSortHoleSort.scala b/testcases/lesynth/InsertionSortHoleSort.scala
new file mode 100644
index 000000000..7931fcc8a
--- /dev/null
+++ b/testcases/lesynth/InsertionSortHoleSort.scala
@@ -0,0 +1,53 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ def size(l : List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def sortedIns(e: Int, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) =>
+ if (x <= e) Cons(x,sortedIns(e, xs))
+ else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+)
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def xxsort(l: List): List = ({
+ hole(l)
+// val cond: Boolean = /*!*/
+// case Nil() => /*!*/ // Nil()
+// case Cons(x,xs) => /*!*/ // sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+}
diff --git a/testcases/lesynth/ListOperations.scala b/testcases/lesynth/ListOperations.scala
new file mode 100644
index 000000000..424a38aa0
--- /dev/null
+++ b/testcases/lesynth/ListOperations.scala
@@ -0,0 +1,45 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+// def content(l: List) : Set[Int] = l match {
+// case Nil() => Set.empty
+// case Cons(head, tail) => Set(head) ++ content(tail)
+// }
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil() => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def isEmpty(l: List) = l match {
+ case Nil() => true
+ case Cons(_, _) => false
+ }
+
+ def concat(l1: List, l2: List) : List = ({
+
+ l1 match {
+ case Nil() => l2
+ case Cons(l1Head, l1Tail) =>
+ l1 match {
+ case Nil() => l2
+ case _ => Cons(l1Head, Cons(l1Head, concat(l1Tail, l2)))
+ }
+ }
+
+ }) ensuring(res =>
+ content(res) == content(l1) ++ content(l2) &&
+ size(res) == size(l1) + size(l2)
+ )
+
+}
diff --git a/testcases/lesynth/ListOperationsHole.scala b/testcases/lesynth/ListOperationsHole.scala
new file mode 100644
index 000000000..bd3cb28e6
--- /dev/null
+++ b/testcases/lesynth/ListOperationsHole.scala
@@ -0,0 +1,24 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+// def isEmpty(l: List) = l match {
+// case Nil() => true
+// case Cons(_, _) => false
+// }
+
+ def concat(l1: List, l2: List) : List = ({
+ hole(l1)
+ }) ensuring(res => content(res) == content(l1) ++ content(l2))
+
+}
diff --git a/testcases/lesynth/ListOperationsHole2.scala b/testcases/lesynth/ListOperationsHole2.scala
new file mode 100644
index 000000000..c1dcf85ac
--- /dev/null
+++ b/testcases/lesynth/ListOperationsHole2.scala
@@ -0,0 +1,24 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+// def isEmpty(l: List) = l match {
+// case Nil() => true
+// case Cons(_, _) => false
+// }
+
+ def concat(l1: List, l2: List) : List = ({
+ hole[List](throw new RuntimeException)
+ }) ensuring(res => content(res) == content(l1) ++ content(l2))
+
+}
diff --git a/testcases/lesynth/MergeSortHole.scala b/testcases/lesynth/MergeSortHole.scala
new file mode 100644
index 000000000..339554c2c
--- /dev/null
+++ b/testcases/lesynth/MergeSortHole.scala
@@ -0,0 +1,81 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def xxmergeSort(list : List) : List = ({
+ hole[List](list)
+// list match {
+// case Nil() => list
+// case Cons(x,Nil()) => list
+// case _ =>
+// val p = split(list,size(list)/2)
+// merge(mergeSort(p.fst), mergeSort(p.snd))
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+ }) ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
--
GitLab