From 94ad8d44a8f26ce2941e0bf9fc182562b6d6a969 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 6 Jan 2016 16:47:45 +0100
Subject: [PATCH] Small improvements
---
.../scala/leon/grammars/DepthBoundedGrammar.scala | 3 ---
src/main/scala/leon/grammars/Label.scala | 2 ++
src/main/scala/leon/purescala/Definitions.scala | 10 +++++-----
src/main/scala/leon/synthesis/graph/Graph.scala | 13 ++++++-------
.../scala/leon/synthesis/rules/CEGISLike.scala | 14 +++++++-------
5 files changed, 20 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/leon/grammars/DepthBoundedGrammar.scala b/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
index 65708427e..7ec864e03 100644
--- a/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
+++ b/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
@@ -3,9 +3,6 @@
package leon
package grammars
-import purescala.Types._
-import purescala.Expressions._
-
case class DepthBoundedGrammar[T](g: ExpressionGrammar[Label[T]], bound: Int) extends ExpressionGrammar[Label[T]] {
def computeProductions(l: Label[T])(implicit ctx: LeonContext): Seq[Gen] = g.computeProductions(l).flatMap {
case gen =>
diff --git a/src/main/scala/leon/grammars/Label.scala b/src/main/scala/leon/grammars/Label.scala
index 456f184e7..aaaaccf30 100644
--- a/src/main/scala/leon/grammars/Label.scala
+++ b/src/main/scala/leon/grammars/Label.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
package leon
package grammars
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 4b89493e1..792e43c56 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -406,13 +406,13 @@ object Definitions {
def subDefinitions = params ++ tparams ++ directlyNestedFuns.toList
/** Duplication of this [[FunDef]].
- * @note This will not replace recursive function calls
+ * @note This will not replace recursive function calls in [[fullBody]]
*/
def duplicate(
- id: Identifier = this.id.freshen,
- tparams: Seq[TypeParameterDef] = this.tparams,
- params: Seq[ValDef] = this.params,
- returnType: TypeTree = this.returnType
+ id: Identifier = this.id.freshen,
+ tparams: Seq[TypeParameterDef] = this.tparams,
+ params: Seq[ValDef] = this.params,
+ returnType: TypeTree = this.returnType
): FunDef = {
val fd = new FunDef(id, tparams, params, returnType)
fd.fullBody = this.fullBody
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index ead04c8bc..6183c2858 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -28,11 +28,10 @@ sealed class Graph(val cm: CostModel, problem: Problem) {
}
sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
- var parents: List[Node] = parent.toList
- var descendants: List[Node] = Nil
def asString(implicit ctx: LeonContext): String
+ var descendants: List[Node] = Nil
// indicates whether this particular node has already been expanded
var isExpanded: Boolean = false
def expand(hctx: SearchContext)
@@ -53,7 +52,7 @@ sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
cm.isImpossible(cost)
}
- // For non-terminals, selected childs for solution
+ // For non-terminals, selected children for solution
var selected: List[Node] = Nil
def composeSolutions(sols: List[Stream[Solution]]): Stream[Solution]
@@ -94,7 +93,7 @@ sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
def updateCost(): Unit = {
cost = computeCost()
- parents.foreach(_.updateCost())
+ parent.foreach(_.updateCost())
}
}
@@ -136,7 +135,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
info(prefix+"Solved"+(if(sol.isTrusted) "" else " (untrusted)")+" with: "+sol.asString+"...")
}
- parents.foreach{ p =>
+ parent.foreach{ p =>
p.updateCost()
if (isSolved) {
p.onSolved(this)
@@ -172,7 +171,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
// Everything is solved correctly
if (solveds.size == descendants.size) {
isSolved = true
- parents.foreach(_.onSolved(this))
+ parent.foreach(_.onSolved(this))
}
}
@@ -221,7 +220,7 @@ class OrNode(cm: CostModel, parent: Option[Node], val p: Problem) extends Node(c
def onSolved(desc: Node): Unit = {
isSolved = true
selected = List(desc)
- parents.foreach(_.onSolved(this))
+ parent.foreach(_.onSolved(this))
}
def composeSolutions(solss: List[Stream[Solution]]): Stream[Solution] = {
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 4f03c9bed..4824d3e53 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -114,9 +114,9 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
private var slots = Map[SizedLabel[T], Int]().withDefaultValue(0)
- private def streamOf(t: SizedLabel[T]): Stream[Identifier] = {
- FreshIdentifier(t.asString, t.getType, true) #:: streamOf(t)
- }
+ private def streamOf(t: SizedLabel[T]): Stream[Identifier] = Stream.continually(
+ FreshIdentifier(t.asString, t.getType, true)
+ )
def rewind(): Unit = {
slots = Map[SizedLabel[T], Int]().withDefaultValue(0)
@@ -385,8 +385,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
//println(programCTree.asString)
//println(".. "*30)
- //val evaluator = new DualEvaluator(sctx.context, programCTree, CodeGenParams.default)
- val evaluator = new DefaultEvaluator(sctx.context, programCTree)
+ //val evaluator = new DualEvaluator(sctx.context, programCTree, CodeGenParams.default)
+ val evaluator = new DefaultEvaluator(sctx.context, programCTree)
tester =
{ (ex: Example, bValues: Set[Identifier]) =>
@@ -679,7 +679,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
baseExampleInputs += InExample(p.as.map(a => simplestValue(a.getType)))
} else {
val solverf = sctx.solverFactory
- val solver = solverf.getNewSolver.setTimeout(exSolverTo)
+ val solver = solverf.getNewSolver().setTimeout(exSolverTo)
solver.assertCnstr(p.pc)
@@ -892,8 +892,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
} else {
result = Some(RuleFailed())
}
- }
}
+ }
case Some(None) =>
skipCESearch = true
--
GitLab