From 71ebadc57d1d3beeba90f8f11fc71e925288ce0a Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 14 Dec 2012 19:53:38 +0100
Subject: [PATCH] Prevent double negations by construction.
This commit finally ensures that { And, Or, Not } are never nested
inside instances of the same class. (The change for And or Or was
already made some time ago.)
---
src/main/scala/leon/purescala/Trees.scala | 20 +++++++++++++++++++-
1 file changed, 19 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 741b3fcaa..8877c17af 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -275,8 +275,26 @@ object Trees {
override def hashCode: Int = left.hashCode + right.hashCode
}
- case class Not(expr: Expr) extends Expr with FixedType {
+ object Not {
+ def apply(expr : Expr) : Expr = expr match {
+ case Not(e) => e
+ case _ => new Not(expr)
+ }
+
+ def unapply(not : Not) : Option[Expr] = {
+ if(not != null) Some(not.expr) else None
+ }
+ }
+
+ class Not private (val expr: Expr) extends Expr with FixedType {
val fixedType = BooleanType
+
+ override def equals(that: Any) : Boolean = (that != null) && (that match {
+ case n : Not => n.expr == expr
+ case _ => false
+ })
+
+ override def hashCode : Int = expr.hashCode ^ Int.MinValue
}
object Equals {
--
GitLab