From 47c5debaa0390ca2be34ad3a78d4ad7e26397d9f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 22 Oct 2012 15:49:32 +0200
Subject: [PATCH] Plop
---
src/main/scala/leon/purescala/Trees.scala | 9 +++++++
src/main/scala/leon/synthesis/Main.scala | 5 +++-
src/main/scala/leon/synthesis/Rules.scala | 26 ++++++++++---------
.../scala/leon/synthesis/Synthesizer.scala | 5 ++--
src/main/scala/leon/synthesis/Task.scala | 7 +++--
5 files changed, 35 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 259ce7911..04db1ab18 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -179,6 +179,15 @@ object Trees {
val fixedType = BooleanType
}
+ object TopLevelAnds { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
+ def unapply(e: Expr): Option[Seq[Expr]] = e match {
+ case And(exprs) =>
+ Some(exprs.flatMap(unapply(_).flatten))
+ case e =>
+ Some(Seq(e))
+ }
+ }
+
object Or {
def apply(l: Expr, r: Expr) : Expr = (l,r) match {
case (BooleanLiteral(false),_) => r
diff --git a/src/main/scala/leon/synthesis/Main.scala b/src/main/scala/leon/synthesis/Main.scala
index a8ed6de21..10520ef26 100644
--- a/src/main/scala/leon/synthesis/Main.scala
+++ b/src/main/scala/leon/synthesis/Main.scala
@@ -3,7 +3,10 @@ package synthesis
object Main {
def main(args : Array[String]) {
- new Synthesizer(new DefaultReporter).test()
+ val reporter = new DefaultReporter
+ val solvers = List(new TrivialSolver(reporter))
+
+ new Synthesizer(reporter, solvers).test()
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 8eca81ad7..0472c87ec 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -6,29 +6,25 @@ import purescala.Trees._
object Rules {
def all(synth: Synthesizer) = List(
- OnePoint(synth)
+ new OnePoint(synth),
+ new Ground(synth)
)
}
-abstract class Rule(val name: String) {
+abstract class Rule(val name: String, val synth: Synthesizer) {
def isApplicable(p: Problem, parent: Task): List[Task]
-
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
+
+ override def toString = name
}
-case class OnePoint(synth: Synthesizer) extends Rule("One-point") {
+class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
def isApplicable(p: Problem, parent: Task): List[Task] = {
p.phi match {
- case a : And =>
- def collectAnds(e: Expr): List[Expr] = e match {
- case And(exs) => exs.toList.flatMap(collectAnds)
- case e => List(e)
- }
-
- val exprs = collectAnds(a)
+ case TopLevelAnds(exprs) =>
val candidates = exprs.collect {
case eq @ Equals(Variable(x), e) if (p.xs contains x) && !(variablesOf(e) contains x) =>
(x, e, eq)
@@ -54,7 +50,7 @@ case class OnePoint(synth: Synthesizer) extends Rule("One-point") {
case _ => Solution.none
}
- List(new Task(synth, parent, p, List(newProblem), onSuccess, 100))
+ List(new Task(synth, parent, this, p, List(newProblem), onSuccess, 100))
} else {
Nil
}
@@ -65,3 +61,9 @@ case class OnePoint(synth: Synthesizer) extends Rule("One-point") {
}
}
}
+
+class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
+ def isApplicable(p: Problem, parent: Task): List[Task] = {
+ Nil
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index e1e8da942..3f7ba6a85 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -2,10 +2,11 @@ package leon
package synthesis
import purescala.Definitions.Program
+import Extensions.Solver
import collection.mutable.PriorityQueue
-class Synthesizer(val r: Reporter) {
+class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
import r.{error,warning,info,fatalError}
private[this] var solution: Solution = null
@@ -50,7 +51,7 @@ class Synthesizer(val r: Reporter) {
task.subSucceeded(sp, sol)
} else {
info(" => Possible Next Steps:")
- alternatives.foreach(a => info(" - "+a))
+ alternatives.foreach(t => info(" - "+t.description))
}
}
}
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index be0d75624..7941afea6 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -4,6 +4,7 @@ package synthesis
class Task(
val synth: Synthesizer,
val parent: Task,
+ val rule: Rule,
val problem: Problem,
val subProblems: List[Problem],
val onSuccess: List[Solution] => Solution,
@@ -38,7 +39,9 @@ class Task(
}
}
- override def toString = subProblems.map(p => (p, !subSolutions.get(p).isEmpty)).map{ case (p, isSolved) => p+(if(isSolved) "(OK)" else "(?)") }.mkString(" ; ")
+ override def toString = description
+
+ def description = "by "+rule.name+"("+score+"): "+problem +" ⟿ "+subProblems.mkString(" ; ")
}
-class RootTask(synth: Synthesizer, p: Problem) extends Task(synth, null, p, List(p), xs => xs.head, 0)
+class RootTask(synth: Synthesizer, p: Problem) extends Task(synth, null, null, p, List(p), xs => xs.head, 0)
--
GitLab