Verify preconditions for heuristics

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 = {

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)))
+  }
 }
 
 

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)))
   }
 }
 

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 {

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)