From 8a7bedd17adc0d80a67670f05d401955d719e9b9 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 4 Dec 2015 15:36:57 +0100
Subject: [PATCH] Fix bug Ravi found in TemplateGenerator for && and ||
---
.../solvers/templates/TemplateGenerator.scala | 35 +++++++++++++++++--
1 file changed, 33 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 3ec1f060f..ab026ba3a 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -228,6 +228,25 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
}(e)
}
+ def groupWhile[T](es: Seq[T])(p: T => Boolean): Seq[Seq[T]] = {
+ var res: Seq[Seq[T]] = Nil
+
+ var c = es
+ while (!c.isEmpty) {
+ val (span, rest) = c.span(p)
+
+ if (span.isEmpty) {
+ res :+= Seq(rest.head)
+ c = rest.tail
+ } else {
+ res :+= span
+ c = rest
+ }
+ }
+
+ res
+ }
+
def rec(pathVar: Identifier, expr: Expr): Expr = {
expr match {
case a @ Assert(cond, err, body) =>
@@ -274,10 +293,22 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
implies(rec(pathVar, lhs), rec(pathVar, rhs))
case a @ And(parts) =>
- andJoin(parts.map(rec(pathVar, _)))
+ if (requireDecomposition(a)) {
+ val partitions = groupWhile(parts)(!requireDecomposition(_))
+ val ifExpr = partitions.map(andJoin).reduceRight((a,b) => IfExpr(a, b, BooleanLiteral(false)))
+ rec(pathVar, ifExpr)
+ } else {
+ a
+ }
case o @ Or(parts) =>
- orJoin(parts.map(rec(pathVar, _)))
+ if (requireDecomposition(o)) {
+ val partitions = groupWhile(parts)(!requireDecomposition(_))
+ val ifExpr = partitions.map(orJoin).reduceRight((a,b) => IfExpr(a, BooleanLiteral(true), b))
+ rec(pathVar, ifExpr)
+ } else {
+ o
+ }
case i @ IfExpr(cond, thenn, elze) => {
if(!requireDecomposition(i)) {
--
GitLab