From c7f64da8b8bb1cdf08e9c67cbb2c0371028bafa8 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Sat, 14 Nov 2015 18:58:26 +0100
Subject: [PATCH] Fix BVNot symbol and add purescala pretty printer support
---
src/main/scala/leon/genc/CConverter.scala | 2 +-
src/main/scala/leon/purescala/PrettyPrinter.scala | 1 +
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
index e1b4a4790..d8a52687c 100644
--- a/src/main/scala/leon/genc/CConverter.scala
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -337,7 +337,7 @@ class CConverter(val ctx: LeonContext, val prog: Program) {
case BVTimes(lhs, rhs) => buildBinOp(lhs, "*", rhs)
case BVDivision(lhs, rhs) => buildBinOp(lhs, "/", rhs)
case BVRemainder(lhs, rhs) => buildBinOp(lhs, "%", rhs)
- case BVNot(rhs) => buildUnOp ( "!", rhs) // TODO check if this one isn't in fact '~'
+ case BVNot(rhs) => buildUnOp ( "~", rhs)
case BVAnd(lhs, rhs) => buildBinOp(lhs, "&", rhs)
case BVOr(lhs, rhs) => buildBinOp(lhs, "|", rhs)
case BVXOr(lhs, rhs) => buildBinOp(lhs, "^", rhs)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7bebde2f8..f2be95fb0 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -164,6 +164,7 @@ class PrettyPrinter(opts: PrinterOptions,
case Or(exprs) => optP { p"${nary(exprs, "| || ")}" } // Ugliness award! The first | is there to shield from stripMargin()
case Not(Equals(l, r)) => optP { p"$l \u2260 $r" }
case Implies(l,r) => optP { p"$l ==> $r" }
+ case BVNot(expr) => p"~$expr"
case UMinus(expr) => p"-$expr"
case BVUMinus(expr) => p"-$expr"
case RealUMinus(expr) => p"-$expr"
--
GitLab