From 8d08a5526dc113ce51563b6949f82ba50eef4250 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 28 Oct 2016 17:22:02 +0200
Subject: [PATCH] Fixed call blocker positioning
---
.../solvers/unrolling/TemplateGenerator.scala | 29 ++++++++++++++-----
.../inox/solvers/unrolling/Templates.scala | 2 +-
2 files changed, 22 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 62c214b69..83acb6e04 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -183,12 +183,17 @@ trait TemplateGenerator { self: Templates =>
storeGuarded(pathVar, Equals(newExpr, rec(pathVar, x, pol)))
case x :: xs =>
+ val newRes: Variable = Variable(FreshIdentifier("res", true), BooleanType)
+ storeExpr(newRes)
+
+ val xrec = rec(pathVar, x, pol)
+ storeGuarded(pathVar, Equals(newRes, xrec))
+
val newBool: Variable = Variable(FreshIdentifier("b", true), BooleanType)
storeCond(pathVar, newBool)
- val xrec = rec(pathVar, x, pol)
- iff(and(pathVar, xrec), newBool)
- storeGuarded(pathVar, implies(not(xrec), not(newExpr)))
+ storeGuarded(pathVar, implies(not(newRes), not(newExpr)))
+ iff(and(pathVar, newRes), newBool)
recAnd(newBool, xs)
@@ -212,12 +217,17 @@ trait TemplateGenerator { self: Templates =>
storeGuarded(pathVar, Equals(newExpr, rec(pathVar, x, None)))
case x :: xs =>
+ val newRes: Variable = Variable(FreshIdentifier("res", true), BooleanType)
+ storeExpr(newRes)
+
+ val xrec = rec(pathVar, x, pol)
+ storeGuarded(pathVar, Equals(newRes, xrec))
+
val newBool: Variable = Variable(FreshIdentifier("b", true), BooleanType)
storeCond(pathVar, newBool)
- val xrec = rec(pathVar, x, None)
- storeGuarded(pathVar, implies(xrec, newExpr))
- iff(and(pathVar, not(xrec)), newBool)
+ storeGuarded(pathVar, implies(newRes, newExpr))
+ iff(and(pathVar, not(newRes)), newBool)
recOr(newBool, xs)
@@ -235,17 +245,20 @@ trait TemplateGenerator { self: Templates =>
val newBool1 : Variable = Variable(FreshIdentifier("b", true), BooleanType)
val newBool2 : Variable = Variable(FreshIdentifier("b", true), BooleanType)
val newExpr : Variable = Variable(FreshIdentifier("e", true), i.getType)
+ val condVar : Variable = Variable(FreshIdentifier("c", true), BooleanType)
storeCond(pathVar, newBool1)
storeCond(pathVar, newBool2)
storeExpr(newExpr)
+ storeExpr(condVar)
val crec = rec(pathVar, cond, None)
val trec = rec(newBool1, thenn, None)
val erec = rec(newBool2, elze, None)
- iff(and(pathVar, cond), newBool1)
- iff(and(pathVar, not(cond)), newBool2)
+ storeGuarded(pathVar, Equals(condVar, crec))
+ iff(and(pathVar, condVar), newBool1)
+ iff(and(pathVar, not(condVar)), newBool2)
storeGuarded(newBool1, Equals(newExpr, trec))
storeGuarded(newBool2, Equals(newExpr, erec))
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index ddf72be38..bdd3a9b97 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -59,7 +59,7 @@ trait Templates extends TemplateGenerator
def canUnroll: Boolean = managers.exists(_.unrollGeneration.isDefined)
def unroll: Clauses = {
assert(canUnroll, "Impossible to unroll further")
- val generation = managers.flatMap(_.unrollGeneration).min
+ val generation = managers.flatMap(_.unrollGeneration).min + 1
if (generation > currentGen) {
currentGen = generation
}
--
GitLab