diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala index 97f1cb96e0f4696a920968c1d112ba433e317b09..4cf59480101c3e5ff7b7a0dca22a47aeb200704e 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 7f312deeff48bd97b258f9df5a5d382c53bc622d..f8cced1f3e06dca99de04d55a356a066cb5d1028 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