From 50b038209fa22b39bcf7677af0ac5c6dfb317f2d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 13 Nov 2012 18:43:34 +0100
Subject: [PATCH] Verify preconditions for heuristics
---
src/main/scala/leon/purescala/Trees.scala | 5 +++--
src/main/scala/leon/synthesis/Heuristics.scala | 17 +++++++++++++++++
src/main/scala/leon/synthesis/Rules.scala | 4 ++--
src/main/scala/leon/synthesis/Solution.scala | 3 +++
src/main/scala/leon/synthesis/Task.scala | 16 +++++++++++-----
5 files changed, 36 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 0f987e784..edf082730 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -168,8 +168,9 @@ object Trees {
/* Propositional logic */
object And {
def apply(l: Expr, r: Expr) : Expr = (l,r) match {
- case (BooleanLiteral(true),_) => r
- case (_,BooleanLiteral(true)) => l
+ case (BooleanLiteral(false),_) => BooleanLiteral(false)
+ case (BooleanLiteral(true),_) => r
+ case (_,BooleanLiteral(true)) => l
case _ => new And(Seq(l,r))
}
def apply(exprs: Seq[Expr]) : Expr = {
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 0c92b0ed7..14352e919 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -19,6 +19,23 @@ trait Heuristic {
this: Rule =>
override def toString = "H: "+name
+
+}
+
+object HeuristicStep {
+ def verifyPre(synth: Synthesizer)(s: Solution): (Solution, Boolean) = {
+ synth.solver.solveSAT(And(Not(s.pre), s.fullTerm)) match {
+ case (Some(true), model) =>
+ synth.reporter.warning("Heuristic failed to produce strongest precondition for solution: \n"+s.toExpr)
+ (s, false)
+ case _ =>
+ (s, true)
+ }
+ }
+
+ def apply(synth: Synthesizer, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+ RuleMultiSteps(subProblems, Nil, onSuccess.andThen(verifyPre(synth)))
+ }
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index af3e7b805..b79ade73c 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -30,11 +30,11 @@ case object RuleInapplicable extends RuleResult
case class RuleSuccess(solution: Solution) extends RuleResult
case class RuleMultiSteps(subProblems: List[Problem],
steps: List[List[Solution] => List[Problem]],
- onSuccess: List[Solution] => Solution) extends RuleResult
+ onSuccess: List[Solution] => (Solution, Boolean)) extends RuleResult
object RuleStep {
def apply(subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
- RuleMultiSteps(subProblems, Nil, onSuccess)
+ RuleMultiSteps(subProblems, Nil, onSuccess.andThen((_, true)))
}
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index cf2561de5..309addbaf 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -23,6 +23,9 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
defs.foldLeft(result){ case (t, fd) => LetDef(fd, t) }
}
+
+ def fullTerm =
+ defs.foldLeft(term){ case (t, fd) => LetDef(fd, t) }
}
object Solution {
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 1176c19a7..c35e2bb24 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -35,7 +35,7 @@ class Task(synth: Synthesizer,
var steps: List[TaskStep] = Nil
var nextSteps: List[List[Solution] => List[Problem]] = Nil
- var onSuccess: List[Solution] => Solution = _
+ var onSuccess: List[Solution] => (Solution, Boolean) = _
def currentStep = steps.head
@@ -55,9 +55,15 @@ class Task(synth: Synthesizer,
steps = new TaskStep(newProblems) :: steps
} else {
- solution = Some(onSuccess(solutions))
-
- parent.partlySolvedBy(this, solution.get)
+ onSuccess(solutions) match {
+ case (s, true) =>
+ solution = Some(s)
+
+ parent.partlySolvedBy(this, solution.get)
+ case _ =>
+ // solution is there, but it is incomplete (precondition not strongest)
+ parent.partlySolvedBy(this, Solution.choose(problem))
+ }
}
}
}
@@ -94,7 +100,7 @@ class Task(synth: Synthesizer,
// To each problem we assign the most basic solution, fold on all inner
// steps, and then reconstruct final solution
val simplestSubSolutions = interSteps.foldLeft(subProblems.map(Solution.basic(_))){ (sols, step) => step(sols).map(Solution.basic(_)) }
- val simplestSolution = onSuccess(simplestSubSolutions)
+ val simplestSolution = onSuccess(simplestSubSolutions)._1
minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
synth.reporter.info(prefix+"Got: "+problem)
--
GitLab