From ac1cabcc940ff2b10df927439c7fdea7e6a937d3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 13 Nov 2012 17:07:41 +0100
Subject: [PATCH] Attach preconditions
---
src/main/scala/leon/synthesis/Heuristics.scala | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 4cf594801..309136349 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -46,7 +46,15 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
val onSuccess: List[Solution] => Solution = {
case List(base, gt, lt) =>
+ val preIn = 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)))
+ val preOut = subst(inductOn -> Variable(origId), preIn)
+
val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
+
+ newFun.precondition = Some(preIn)
+
newFun.body = Some(
IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
base.toExpr,
@@ -55,13 +63,8 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
, LetTuple(postXs, FunctionInvocation(newFun, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
)
- 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)))))
+ Solution(preOut, LetDef(newFun, FunctionInvocation(newFun, Seq(Variable(origId)))))
case _ =>
Solution.none
}
--
GitLab