From b081084b82053544b860ebf729857f15b10486e3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 23 Oct 2012 01:52:53 +0200
Subject: [PATCH] Implement Assert, score solutions to order them
---
src/main/scala/leon/synthesis/Rules.scala | 49 ++++++++++++++++---
src/main/scala/leon/synthesis/Solution.scala | 4 +-
.../scala/leon/synthesis/Synthesizer.scala | 1 -
src/main/scala/leon/synthesis/Task.scala | 11 +++--
4 files changed, 50 insertions(+), 15 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 13129acdf..00c8af3a2 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -9,7 +9,8 @@ object Rules {
def all(synth: Synthesizer) = List(
new OnePoint(synth),
new Ground(synth),
- new CaseSplit(synth)
+ new CaseSplit(synth),
+ new Assert(synth)
)
}
@@ -43,11 +44,11 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
val newProblem = Problem(p.as, subst(x -> e, And(others)), oxs)
val onSuccess: List[Solution] => Solution = {
- case List(Solution(pre, term)) =>
+ case List(Solution(pre, term, sc)) =>
if (oxs.isEmpty) {
- Solution(pre, e)
+ Solution(pre, e, sc)
} else {
- Solution(pre, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))) )
+ Solution(pre, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))), sc)
}
case _ => Solution.none
}
@@ -73,13 +74,13 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
synth.solveSAT(p.phi) match {
case (Some(true), model) =>
val onSuccess: List[Solution] => Solution = {
- case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe))
+ case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe), 200)
}
List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
case (Some(false), model) =>
val onSuccess: List[Solution] => Solution = {
- case Nil => Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))
+ case Nil => Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200)
}
List(new Task(synth, parent, this, p, Nil, onSuccess, 200))
@@ -100,7 +101,8 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
val sub2 = Problem(p.as, o2, p.xs)
val onSuccess: List[Solution] => Solution = {
- case List(s1, s2) => Solution(Or(s1.pre, s2.pre), IfExpr(s1.pre, s1.term, s2.term))
+ case List(s1, s2) => Solution(Or(s1.pre, s2.pre), IfExpr(s1.pre, s1.term, s2.term), 100)
+ case _ => Solution.none
}
List(new Task(synth, parent, this, p, List(sub1, sub2), onSuccess, 100))
@@ -109,3 +111,36 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
}
}
}
+
+class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
+ def isApplicable(p: Problem, parent: Task): List[Task] = {
+ p.phi match {
+ case TopLevelAnds(exprs) =>
+ val xsSet = p.xs.toSet
+
+ val (exprsA, others) = exprs.partition(e => (variablesOf(e) & xsSet).isEmpty)
+
+ if (!exprsA.isEmpty) {
+ if (others.isEmpty) {
+ val onSuccess: List[Solution] => Solution = {
+ case Nil => Solution(And(exprsA), BooleanLiteral(true), 150)
+ case _ => Solution.none
+ }
+
+ List(new Task(synth, parent, this, p, Nil, onSuccess, 150))
+ } else {
+ val onSuccess: List[Solution] => Solution = {
+ case List(s) => Solution(And(s.pre +: exprsA), s.term, 150)
+ case _ => Solution.none
+ }
+
+ List(new Task(synth, parent, this, p, List(p.copy(phi = And(others))), onSuccess, 150))
+ }
+ } else {
+ Nil
+ }
+ case _ =>
+ Nil
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 8346a9a60..f9e9f28c3 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -5,12 +5,12 @@ import leon.purescala.Trees._
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
-case class Solution(pre: Expr, term: Expr) {
+case class Solution(pre: Expr, term: Expr, score: Score = 0) {
override def toString = "⟨ "+pre+" | "+term+" ⟩"
}
object Solution {
- def choose(p: Problem): Solution = Solution(BooleanLiteral(true), Choose(p.xs, p.phi))
+ def choose(p: Problem): Solution = Solution(BooleanLiteral(true), Choose(p.xs, p.phi), 0)
def none: Solution = throw new Exception("Unexpected failure to construct solution")
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 437556701..12da7a5e3 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -40,7 +40,6 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
alternatives.find(_.isSuccess) match {
case Some(ss) =>
- info(" => Success!")
ss.succeeded()
case None =>
info(" => Possible Next Steps:")
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 7941afea6..fd6702c81 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -27,15 +27,16 @@ class Task(
def subSucceeded(p: Problem, s: Solution) {
assert(subProblems contains p, "Problem "+p+" is unknown to me ?!?")
- assert(!(subSolutions contains p), "I already have a solution for "+p+" ?!?")
- subSolutions += p -> s
+ if (subSolutions.get(p).map(_.score).getOrElse(-1) < s.score) {
+ subSolutions += p -> s
- if (subSolutions.size == subProblems.size) {
+ if (subSolutions.size == subProblems.size) {
- val solution = onSuccess(subProblems map subSolutions)
+ val solution = onSuccess(subProblems map subSolutions)
- synth.onTaskSucceeded(this, solution)
+ synth.onTaskSucceeded(this, solution)
+ }
}
}
--
GitLab