From 3c94cbd5a2027f219a70a1ad3fadf613aad9ffae Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 26 Jun 2015 17:15:56 +0200
Subject: [PATCH] Printing and stuff
---
src/main/scala/leon/purescala/PrettyPrinter.scala | 4 ++++
src/main/scala/leon/solvers/templates/TemplateGenerator.scala | 4 +++-
2 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 22c8c174b..57618655f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -123,6 +123,10 @@ class PrettyPrinter(opts: PrinterOptions,
} else {
p"""|?($es)"""
}
+
+ case Forall(args, e) =>
+ p"""\u2200${typed(args.map(_.id))}. $e"""
+
case e @ CaseClass(cct, args) =>
opgm.flatMap { pgm => isListLiteral(e)(pgm) } match {
case Some((tpe, elems)) =>
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 9942cc3b7..4c49c3101 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -161,7 +161,9 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
def requireDecomposition(e: Expr) = {
exists{
- case (_: FunctionInvocation) | (_: Assert) | (_: Ensuring) | (_: Choose) | (_: Application) => true
+ case (_: Choose) | (_: Forall) => true
+ case (_: Assert) | (_: Ensuring) => true
+ case (_: FunctionInvocation) | (_: Application) => true
case _ => false
}(e)
}
--
GitLab