From fa9db94319ed171b6ebfab9a49e7dfa864bf7a1e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 4 Apr 2013 15:34:20 +0200
Subject: [PATCH] Check whether pc to ADTInduction is inductive before
propagating it
---
.../scala/leon/synthesis/heuristics/ADTInduction.scala | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 39ff4d4c2..4d6342bae 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -2,6 +2,7 @@ package leon
package synthesis
package heuristics
+import solvers.TimeoutSolver
import purescala.Common._
import purescala.Trees._
import purescala.Extractors._
@@ -11,14 +12,16 @@ import purescala.Definitions._
case object ADTInduction extends Rule("ADT Induction") with Heuristic {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+ val tsolver = new TimeoutSolver(sctx.solver, 500L)
val candidates = p.as.collect {
- case IsTyped(origId, AbstractClassType(cd)) => (origId, cd)
+ case IsTyped(origId, AbstractClassType(cd)) if isInductiveOn(tsolver)(p.pc, origId) => (origId, cd)
}
val instances = for (candidate <- candidates) yield {
val (origId, cd) = candidate
val oas = p.as.filterNot(_ == origId)
+
val resType = TupleType(p.xs.map(_.getType))
val inductOn = FreshIdentifier(origId.name, true).setType(origId.getType)
@@ -89,13 +92,14 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
SimpleCase(caze, calls.foldLeft(sol.term){ case (t, (binders, callargs)) => LetTuple(binders, FunctionInvocation(newFun, callargs), t) })
}
- if (sols.exists(_.pre != BooleanLiteral(true))) {
+ // Might be overly picky with obviously true pre (a.is[Cons] OR a.is[Nil])
+ if (false && sols.exists(_.pre != BooleanLiteral(true))) {
// Required to avoid an impossible cases, which suffices to
// allow invalid programs. This might be too strong though: we
// might only have to enforce it on solutions of base cases.
None
} else {
- val funPre = substAll(substMap, Or(globalPre))
+ val funPre = substAll(substMap, And(p.pc, Or(globalPre)))
val funPost = substAll(substMap, p.phi)
val outerPre = Or(globalPre)
--
GitLab