From 7a318dd21c1ff4f0a749b2deab6a265fd65f9063 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 13 Nov 2012 16:54:42 +0100
Subject: [PATCH] Propagate IntInduction's precondition
---
src/main/scala/leon/synthesis/Heuristics.scala | 8 +++++++-
src/main/scala/leon/synthesis/Task.scala | 10 +++++-----
2 files changed, 12 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 97f1cb96e..4cf594801 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -55,7 +55,13 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
, LetTuple(postXs, FunctionInvocation(newFun, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
)
- Solution(BooleanLiteral(true), LetDef(newFun, FunctionInvocation(newFun, Seq(Variable(origId)))))
+ val pre =
+ subst( inductOn -> Variable(origId),
+ Or(Seq(And(Equals(Variable(inductOn), IntLiteral(0)), base.pre),
+ And(GreaterThan(Variable(inductOn), IntLiteral(0)), gt.pre),
+ And(LessThan(Variable(inductOn), IntLiteral(0)), lt.pre))))
+
+ Solution(pre, LetDef(newFun, FunctionInvocation(newFun, Seq(Variable(origId)))))
case _ =>
Solution.none
}
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 7f312deef..f8cced1f3 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -80,8 +80,8 @@ class Task(synth: Synthesizer,
parent.partlySolvedBy(this, solution)
val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
- println(prefix+"Got: "+problem)
- println(prefix+"Solved with: "+solution)
+ synth.reporter.info(prefix+"Got: "+problem)
+ synth.reporter.info(prefix+"Solved with: "+solution)
Nil
case RuleMultiSteps(subProblems, interSteps, onSuccess) =>
@@ -96,10 +96,10 @@ class Task(synth: Synthesizer,
val simplestSolution = onSuccess(simplestSubSolutions)
minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
- println(prefix+"Got: "+problem)
- println(prefix+"Decomposed into:")
+ synth.reporter.info(prefix+"Got: "+problem)
+ synth.reporter.info(prefix+"Decomposed into:")
for(p <- subProblems) {
- println(prefix+" - "+p)
+ synth.reporter.info(prefix+" - "+p)
}
subProblems
--
GitLab