From 039486a1bfd7a2c99b100909ec772a2c99f920f3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 2 Nov 2012 14:58:59 +0100
Subject: [PATCH] Simplify generic transform, silence reporters
---
src/main/scala/leon/purescala/TreeOps.scala | 41 ++++++++++++++++---
.../scala/leon/synthesis/Complexity.scala | 12 +++++-
src/main/scala/leon/synthesis/Rules.scala | 2 +-
.../scala/leon/synthesis/SynthesisPhase.scala | 8 ++--
.../scala/leon/synthesis/Synthesizer.scala | 1 -
5 files changed, 51 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index dcad10769..2bec96b30 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -954,7 +954,7 @@ object TreeOps {
def genericTransform[C](pre: (Expr, C) => (Expr, C),
post: (Expr, C) => (Expr, C),
- combiner: (Expr, C, Seq[C]) => C)(init: C)(expr: Expr) = {
+ combiner: (Seq[C]) => C)(init: C)(expr: Expr) = {
def rec(eIn: Expr, cIn: C): (Expr, C) = {
@@ -968,20 +968,20 @@ object TreeOps {
val (e1, c) = rec(e, ctx)
val newE = builder(e1)
- (newE, combiner(newE, cIn, Seq(c)))
+ (newE, combiner(Seq(c)))
case BinaryOperator(e1, e2, builder) =>
val (ne1, c1) = rec(e1, ctx)
val (ne2, c2) = rec(e2, ctx)
val newE = builder(ne1, ne2)
- (newE, combiner(newE, cIn, Seq(c1, c2)))
+ (newE, combiner(Seq(c1, c2)))
case NAryOperator(es, builder) =>
val (nes, cs) = es.map{ rec(_, ctx)}.unzip
val newE = builder(nes)
- (newE, combiner(newE, cIn, cs))
+ (newE, combiner(cs))
case e =>
sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
@@ -993,7 +993,7 @@ object TreeOps {
rec(expr, init)
}
- private def noCombiner[C](e: Expr, initC: C, subCs: Seq[C]) = initC
+ private def noCombiner(subCs: Seq[Unit]) = ()
def simpleTransform(pre: Expr => Expr, post: Expr => Expr)(expr: Expr) = {
val newPre = (e: Expr, c: Unit) => (pre(e), ())
@@ -1303,6 +1303,37 @@ object TreeOps {
rec(expr, Nil)
}
+ def formulaSize(e: Expr): Int = e match {
+ case t: Terminal =>
+ 1
+
+ case UnaryOperator(e, builder) =>
+ formulaSize(e)+1
+
+ case BinaryOperator(e1, e2, builder) =>
+ formulaSize(e1)+formulaSize(e2)+1
+
+ case NAryOperator(es, _) =>
+ es.map(formulaSize).foldRight(0)(_ + _)+1
+ }
+
+ def collectChooses(e: Expr): List[Choose] = {
+ def post(e: Expr, cs: List[Choose]) = {
+ val newCs = e match {
+ case c: Choose => c :: cs
+ case _ => cs
+ }
+
+ (e, newCs)
+ }
+
+ def combiner(cs: Seq[List[Choose]]) = {
+ cs.foldLeft(List[Choose]())(_ ::: _)
+ }
+
+ genericTransform[List[Choose]]((_, _), post, combiner)(List())(e)._2
+ }
+
def valuateWithModel(model: Map[Identifier, Expr])(id: Identifier): Expr = {
model.getOrElse(id, simplestValue(id.getType))
}
diff --git a/src/main/scala/leon/synthesis/Complexity.scala b/src/main/scala/leon/synthesis/Complexity.scala
index eb967a4b2..8106beed5 100644
--- a/src/main/scala/leon/synthesis/Complexity.scala
+++ b/src/main/scala/leon/synthesis/Complexity.scala
@@ -2,6 +2,7 @@ package leon
package synthesis
import purescala.Trees._
+import purescala.TreeOps._
abstract class Complexity[T <: Complexity[T]] extends Ordered[T] {
def compare(that: T) = this.value - that.value
@@ -21,9 +22,16 @@ case class TaskComplexity(t: Task) extends Complexity[TaskComplexity] {
}
case class SolutionComplexity(s: Solution) extends Complexity[SolutionComplexity] {
- lazy val value = 42
+ lazy val value = {
+ val chooses = collectChooses(s.term)
+ val chooseCost = 1000 * chooses.foldLeft(0)((i, c) => i + (math.pow(2, c.vars.size).toInt + formulaSize(c.pred)))
+
+ formulaSize(s.pre) + formulaSize(s.term) + chooseCost
+ }
}
case class ProblemComplexity(p: Problem) extends Complexity[ProblemComplexity] {
- lazy val value = 42
+ lazy val value = {
+ math.pow(2, p.xs.size).toInt + formulaSize(p.phi)
+ }
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 021f03b82..7210ef271 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -276,7 +276,7 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 20, 0) {
}
}
-class GiveUp(synth: Synthesizer) extends Rule("GiveUp", synth, 0, 100) {
+class GiveUp(synth: Synthesizer) extends Rule("GiveUp", synth, -100000, 100) {
def applyOn(task: Task): RuleResult = {
RuleSuccess(Solution.choose(task.problem))
}
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 7754d81f6..7adfb5aef 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -21,12 +21,12 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
)
def run(ctx: LeonContext)(p: Program): Program = {
- val quietReporter = new QuietReporter
+ val reporter = new SilentReporter
val solvers = List(
- new TrivialSolver(quietReporter),
- new FairZ3Solver(quietReporter)
+ new TrivialSolver(reporter),
+ new FairZ3Solver(reporter)
)
- val uninterpretedZ3 = new UninterpretedZ3Solver(quietReporter)
+ val uninterpretedZ3 = new UninterpretedZ3Solver(reporter)
uninterpretedZ3.setProgram(p)
var inPlace = false
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index bff158220..d18bd0cb1 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -39,7 +39,6 @@ class Synthesizer(val r: Reporter,
for (p <- subProblems; r <- rules) yield {
workList += new Task(this, task, p, r)
}
-
}
if (generateDerivationTrees) {
--
GitLab