From f85b4bce3a4572bac3f3e589e10ee5a191141d6d Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Tue, 5 Nov 2024 10:00:47 +0100
Subject: [PATCH 01/10] Basic functionality (simplify and get shortest for
 small ruleset)

---
 .../deepsimplifier/DeepSimplifier.scala       | 140 +++++++++++++
 .../deepsimplifier/DeepSimplifierTest.scala   | 188 ++++++++++++++++++
 2 files changed, 328 insertions(+)
 create mode 100644 src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
 create mode 100644 src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala

diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
new file mode 100644
index 000000000..cd015d99b
--- /dev/null
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
@@ -0,0 +1,140 @@
+package viper.silver.ast.utility.deepsimplifier
+
+import viper.silver.ast._
+import viper.silver.ast.utility.rewriter.StrategyBuilder
+
+import scala.collection.mutable
+import scala.collection.mutable._
+
+object DeepSimplifier {
+
+  def simplify[N <: Node](n: N): N = {
+
+    val visited: ArrayBuffer[N] = ArrayBuffer(n)
+    val queue: mutable.Queue[N] = mutable.Queue(n)
+
+    while(queue.nonEmpty){
+      val currnode: N = queue.dequeue()
+      //val generated: ArrayBuffer[N] = recursiveSimplify(currnode)
+      val generated: ArrayBuffer[N] = pfSimplify(currnode).asInstanceOf[ArrayBuffer[N]]
+
+      for(g <- generated if !visited.contains(g)) {
+        //println("new g: " + g)
+        visited.append(g)
+        queue.enqueue(g)
+      }
+      queue.enqueueAll(generated)
+    }
+
+    println("result simplify: " + visited)
+
+    getShortest(visited)
+  }
+
+  // only called with nonempty ArrayBuffers TODO: what happens if empty?
+  // TODO: make private
+
+  def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
+    visited.minBy(treeSize)
+  }
+
+  // "counts every node twice", ie "LocalVar("a", Bool)()" is counted once as "a" and once as "Bool", at least it's consistent
+  // TODO: make private
+  def treeSize[N <: Node](n: N): Int = {
+    n.reduceTree[Int]((node, count) => (count.sum + 1))
+  }
+
+  def pfSimplify[N <: Node](n: N): ArrayBuffer[Node] = {
+
+    val result: ArrayBuffer[Node] = ArrayBuffer()
+
+    val cases: List[PartialFunction[Node, Node]] = List(
+      { case Not(Not(single)) => single},
+      { case root@Or(TrueLit(), _) => TrueLit()(root.pos, root.info)},
+      { case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info)}
+    )
+
+    result ++= cases.collect{ case lcase if lcase.isDefinedAt(n) => lcase(n)}
+
+    result
+  }
+
+  //TODO: make private
+  //TODO: does not necessarily need to know what type n itself is?
+  // just be able to apply simpOneNode to a child and return the simplified version with the same child
+  // use nodes? BinExp?
+  //TODO: why fallthrough?
+
+  def recursiveSimplify[N <: Node](n: N): ArrayBuffer[N] = {
+
+    val result: ArrayBuffer[N] = ArrayBuffer()
+    val versions: ArrayBuffer[N] = ArrayBuffer()
+
+    result ++= simpOneNode(n)
+
+    /*n.children.map {child =>
+      val simps = simpOneNode(child).map {
+        simp => n.replace (case child => simp)
+      }
+    }
+
+    n.*/
+    
+    n match {
+      case LocalVar => (result) ++= versions
+
+      case Not(a) =>
+        val childrenS: ArrayBuffer[N] = recursiveSimplify(a.asInstanceOf[N])
+        for (c <- childrenS) {
+          result += Not(c.asInstanceOf[Exp])().asInstanceOf[N]
+        }
+
+        (result) ++= simpOneNode(n)
+
+      case And(a, b) =>
+        val aS: ArrayBuffer[N] = recursiveSimplify(a.asInstanceOf[N])
+        val bS: ArrayBuffer[N] = recursiveSimplify(b.asInstanceOf[N])
+
+        for (saS <- aS) {
+          for (sbS <- bS) {
+            result += And(saS.asInstanceOf[Exp], sbS.asInstanceOf[Exp])().asInstanceOf[N]
+          }
+        }
+      case _ =>
+    }
+    (result)
+  }
+
+  //TODO: make private, remove test4 from DeepSimplifierTest
+  //TODO: figure out how to add result without casting to N (asInstanceOf[N])
+  //TODO: better pattern matching (?)
+
+  def simpOneNode[N <: Node](n: Node): ArrayBuffer[N] = {
+
+    val result: ArrayBuffer[N] = ArrayBuffer()
+
+    if(n.isInstanceOf[Not] && n.asInstanceOf[Not].exp.isInstanceOf[Not]) {
+      result += n.asInstanceOf[Not].exp.asInstanceOf[Not].exp.asInstanceOf[N]
+    }
+    if(n.isInstanceOf[And] && n.asInstanceOf[And].left.isInstanceOf[TrueLit]) {
+      result += n.asInstanceOf[And].right.asInstanceOf[N]
+    }
+    if(n.isInstanceOf[And] && n.asInstanceOf[And].right.isInstanceOf[TrueLit]) {
+      result += n.asInstanceOf[And].left.asInstanceOf[N]
+    }
+
+    result
+  }
+
+  /*def contains(n: Node): Boolean = {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+    val c = Or(a, b)()
+
+    val visited: List[Node] = List(c)
+
+    visited.contains(n)
+  }*/
+}
diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
new file mode 100644
index 000000000..5700ab0ba
--- /dev/null
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
@@ -0,0 +1,188 @@
+package viper.silver.ast.utility.deepsimplifier
+
+import org.scalatest.funsuite.AnyFunSuite
+
+import scala.language.implicitConversions
+import org.scalatest.matchers.should.Matchers
+import viper.silver.ast.DomainBinExp.unapply
+import viper.silver.ast.{Node, _}
+import viper.silver.ast.utility.deepsimplifier.DeepSimplifier._
+
+import scala.collection.mutable.ArrayBuffer
+
+class DeepSimplifierTest extends AnyFunSuite with Matchers{
+
+  test("test1") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+
+    simplify(Implies(a, b)()) should be(Implies(a, b)())
+
+    println(Implies(a, b)())
+    println(simplify(Implies(a, b)()))
+  }
+
+  test("test2") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+
+    simplify(Or(a, b)()) should be(Implies(a, b)())
+
+    println(Or(a, b)())
+    println(simplify(Implies(a, b)()))
+  }
+
+  test("test3") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+    val c = Or(a, b)()
+
+    val d = LocalVar("a", Bool)()
+    val e = LocalVar("b", Bool)()
+
+    val f = Or(d, e)()
+
+
+    c should be(f)
+
+    println(c)
+    println(f)
+  }
+
+  /*test("test4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+    val c = Or(a, b)()
+
+    contains(c) should be(true)
+  }*/
+
+  test("test4") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(a)())()
+
+    println(b)
+    //println(genSimp(b))
+
+    true should be(true)
+  }
+
+  test("test5") {
+    val a = LocalVar("a", Bool)()
+    val b = And(a, a)()
+
+    println(b)
+    println(a.getClass)
+
+    true should be(true)
+  }
+
+  test("test6") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(a)())()
+    val c = Not(Not(b)())()
+    val tru = TrueLit()()
+    val d = Or(c, tru)()
+
+    println(d)
+    println(simplify(d))
+
+    true should be(true)
+  }
+
+  test("test7") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(Not(a)())())()
+
+    println(b)
+    println(recursiveSimplify(b))
+
+    true should be(true)
+  }
+
+  test("test8") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = And(a, Not(a)())()
+    val d = And(b, c)()
+
+
+    println(d)
+    println(recursiveSimplify(d))
+
+    true should be(true)
+  }
+
+  test("test9") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(a)())()
+    val c = And(a, Not(a)())()
+    val d = And(b, c)()
+
+
+    println(d)
+    println(recursiveSimplify(d))
+
+    true should be(true)
+  }
+
+  test("test10") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Or(a, Not(a)())()
+    val d = Or(b, c)()
+
+
+    println(d)
+    println()
+    println(pfSimplify(d))
+
+    true should be(true)
+  }
+
+  test("test11") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(a)())()
+
+    println(b)
+    println(pfSimplify(b))
+
+    true should be(true)
+  }
+
+  test("test12") {
+    val a = LocalVar("a", Bool)()
+    val tru = TrueLit()()
+    val b = Not(Not(a)())()
+    val c = Or(a, tru)()
+
+    println(c)
+    println(treeSize(a))
+    println(treeSize(tru))
+    println(treeSize(c))
+    println(pfSimplify(c))
+
+    true should be(true)
+  }
+
+  test("test13") {
+    val a = LocalVar("a", Bool)()
+    val b = Or(Not(Not(a)())(), a)()
+    val c = Or(Not(a)(), a)()
+
+    val buf = ArrayBuffer[Node](a, b, c)
+
+    println(getShortest(buf))
+
+    true should be(true)
+  }
+
+
+}

From d7cc0a921ff71e650146d2ff9ee9b817081efd67 Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Mon, 18 Nov 2024 19:24:56 +0100
Subject: [PATCH 02/10] new simplify (pfSimplify)

---
 .../deepsimplifier/DeepSimplifier.scala       | 95 ++++---------------
 .../deepsimplifier/DeepSimplifierTest.scala   | 23 ++++-
 2 files changed, 36 insertions(+), 82 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
index cd015d99b..5dc9be928 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
@@ -1,7 +1,6 @@
 package viper.silver.ast.utility.deepsimplifier
 
 import viper.silver.ast._
-import viper.silver.ast.utility.rewriter.StrategyBuilder
 
 import scala.collection.mutable
 import scala.collection.mutable._
@@ -13,12 +12,12 @@ object DeepSimplifier {
     val visited: ArrayBuffer[N] = ArrayBuffer(n)
     val queue: mutable.Queue[N] = mutable.Queue(n)
 
-    while(queue.nonEmpty){
+    while (queue.nonEmpty) {
       val currnode: N = queue.dequeue()
       //val generated: ArrayBuffer[N] = recursiveSimplify(currnode)
-      val generated: ArrayBuffer[N] = pfSimplify(currnode).asInstanceOf[ArrayBuffer[N]]
+      val generated: ArrayBuffer[N] = pfSimplify(currnode)
 
-      for(g <- generated if !visited.contains(g)) {
+      for (g <- generated if !visited.contains(g)) {
         //println("new g: " + g)
         visited.append(g)
         queue.enqueue(g)
@@ -44,97 +43,35 @@ object DeepSimplifier {
     n.reduceTree[Int]((node, count) => (count.sum + 1))
   }
 
-  def pfSimplify[N <: Node](n: N): ArrayBuffer[Node] = {
+  def pfSimplify[N <: Node](n: N): ArrayBuffer[N] = {
 
     val result: ArrayBuffer[Node] = ArrayBuffer()
 
-    val cases: List[PartialFunction[Node, Node]] = List(
-      { case Not(Not(single)) => single},
-      { case root@Or(TrueLit(), _) => TrueLit()(root.pos, root.info)},
-      { case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info)}
+    val cases: List[PartialFunction[N, Node]] = List(
+      { case Not(Not(single)) => single },
+      { case root@Or(TrueLit(), _) => TrueLit()(root.pos, root.info) },
+      { case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info) }
     )
 
-    result ++= cases.collect{ case lcase if lcase.isDefinedAt(n) => lcase(n)}
+    result ++= cases.collect { case lcase if lcase.isDefinedAt(n) => lcase(n) }
 
-    result
+    result.asInstanceOf[ArrayBuffer[N]]
   }
 
-  //TODO: make private
-  //TODO: does not necessarily need to know what type n itself is?
-  // just be able to apply simpOneNode to a child and return the simplified version with the same child
-  // use nodes? BinExp?
-  //TODO: why fallthrough?
-
-  def recursiveSimplify[N <: Node](n: N): ArrayBuffer[N] = {
-
+  def pfRecSimplify[N <: Node](n: N): ArrayBuffer[N] = {
     val result: ArrayBuffer[N] = ArrayBuffer()
-    val versions: ArrayBuffer[N] = ArrayBuffer()
 
-    result ++= simpOneNode(n)
-
-    /*n.children.map {child =>
-      val simps = simpOneNode(child).map {
-        simp => n.replace (case child => simp)
+    lazy val newChildrenList = n.children.zipWithIndex.flatMap { case (child: N, index) =>
+      pfSimplify(child).map { pfSimpChild =>
+        n.children.toList.updated(index, pfSimpChild)
       }
     }
-
-    n.*/
-    
-    n match {
-      case LocalVar => (result) ++= versions
-
-      case Not(a) =>
-        val childrenS: ArrayBuffer[N] = recursiveSimplify(a.asInstanceOf[N])
-        for (c <- childrenS) {
-          result += Not(c.asInstanceOf[Exp])().asInstanceOf[N]
-        }
-
-        (result) ++= simpOneNode(n)
-
-      case And(a, b) =>
-        val aS: ArrayBuffer[N] = recursiveSimplify(a.asInstanceOf[N])
-        val bS: ArrayBuffer[N] = recursiveSimplify(b.asInstanceOf[N])
-
-        for (saS <- aS) {
-          for (sbS <- bS) {
-            result += And(saS.asInstanceOf[Exp], sbS.asInstanceOf[Exp])().asInstanceOf[N]
-          }
-        }
-      case _ =>
+    result ++= newChildrenList.map {
+      newChildren => n.withChildren(newChildren)
     }
-    (result)
-  }
-
-  //TODO: make private, remove test4 from DeepSimplifierTest
-  //TODO: figure out how to add result without casting to N (asInstanceOf[N])
-  //TODO: better pattern matching (?)
-
-  def simpOneNode[N <: Node](n: Node): ArrayBuffer[N] = {
-
-    val result: ArrayBuffer[N] = ArrayBuffer()
-
-    if(n.isInstanceOf[Not] && n.asInstanceOf[Not].exp.isInstanceOf[Not]) {
-      result += n.asInstanceOf[Not].exp.asInstanceOf[Not].exp.asInstanceOf[N]
-    }
-    if(n.isInstanceOf[And] && n.asInstanceOf[And].left.isInstanceOf[TrueLit]) {
-      result += n.asInstanceOf[And].right.asInstanceOf[N]
-    }
-    if(n.isInstanceOf[And] && n.asInstanceOf[And].right.isInstanceOf[TrueLit]) {
-      result += n.asInstanceOf[And].left.asInstanceOf[N]
-    }
-
     result
   }
 
-  /*def contains(n: Node): Boolean = {
-
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-    val c = Or(a, b)()
 
-    val visited: List[Node] = List(c)
 
-    visited.contains(n)
-  }*/
 }
diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
index 5700ab0ba..562ac869a 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
@@ -12,7 +12,7 @@ import scala.collection.mutable.ArrayBuffer
 
 class DeepSimplifierTest extends AnyFunSuite with Matchers{
 
-  test("test1") {
+  /*test("test1") {
 
     val a = LocalVar("a", Bool)()
     val b = LocalVar("b", Bool)()
@@ -115,7 +115,7 @@ class DeepSimplifierTest extends AnyFunSuite with Matchers{
 
 
     println(d)
-    println(recursiveSimplify(d))
+    println(d.size)
 
     true should be(true)
   }
@@ -160,8 +160,9 @@ class DeepSimplifierTest extends AnyFunSuite with Matchers{
   test("test12") {
     val a = LocalVar("a", Bool)()
     val tru = TrueLit()()
+    val othertru = TrueLit()()
     val b = Not(Not(a)())()
-    val c = Or(a, tru)()
+    val c = Or(othertru, tru)()
 
     println(c)
     println(treeSize(a))
@@ -184,5 +185,21 @@ class DeepSimplifierTest extends AnyFunSuite with Matchers{
     true should be(true)
   }
 
+   */
+
+  test("test14") {
+    val a = LocalVar("a", Bool)()
+    val z = LocalVar("z", Bool)()
+    val b = Or(Not(Not(a)())(), a)()
+    val c = Or(Not(a)(), a)()
+    val d = Or(Not(Not(a)())(), Not(Not(Not(Not(z)())())())())()
+
+    println(d.children)
+
+    pfRecSimplify(d)
+
+    true should be(true)
+  }
+
 
 }

From 15d558dd254b6b649d637703de765b5bbefb3f45 Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Tue, 19 Nov 2024 02:37:44 +0100
Subject: [PATCH 03/10] simplify (pfSimplify and pfRecursiveSimplify) initial
 functionality

---
 .../deepsimplifier/DeepSimplifier.scala       | 49 +++++++++++++++----
 .../deepsimplifier/DeepSimplifierTest.scala   | 23 ++++++++-
 2 files changed, 60 insertions(+), 12 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
index 5dc9be928..7d5fb4d1d 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
@@ -14,15 +14,17 @@ object DeepSimplifier {
 
     while (queue.nonEmpty) {
       val currnode: N = queue.dequeue()
+      println("currnode: " + currnode)
       //val generated: ArrayBuffer[N] = recursiveSimplify(currnode)
-      val generated: ArrayBuffer[N] = pfSimplify(currnode)
+      val generated: ArrayBuffer[N] = pfRecSimplify(currnode)
+      println("generated: " + generated)
 
       for (g <- generated if !visited.contains(g)) {
         //println("new g: " + g)
+
         visited.append(g)
         queue.enqueue(g)
       }
-      queue.enqueueAll(generated)
     }
 
     println("result simplify: " + visited)
@@ -61,17 +63,44 @@ object DeepSimplifier {
   def pfRecSimplify[N <: Node](n: N): ArrayBuffer[N] = {
     val result: ArrayBuffer[N] = ArrayBuffer()
 
-    lazy val newChildrenList = n.children.zipWithIndex.flatMap { case (child: N, index) =>
-      pfSimplify(child).map { pfSimpChild =>
-        n.children.toList.updated(index, pfSimpChild)
+
+    val newChildrenList = n.children.zipWithIndex.map {
+      case (child: AtomicType, index) => {
+        //println(child)
+        //println("case1: " + ArrayBuffer(n.children.toList))
+        Nil
+        ArrayBuffer(n.children.toList)
+      }
+      case (child: N, index) => {
+        //println("case2")
+        val temp = new ArrayBuffer[List[Any]]()
+          temp ++=pfSimplify(child).map { pfSimpChild =>
+          n.children.toList.updated(index, pfSimpChild)
+        }
+        //println("case2: " + temp)
+        temp ++= pfRecSimplify(child).toList.map { recSimpChild =>
+          n.children.toList.updated(index, recSimpChild)
+        }
+        //println("case2after: " + temp)
+        temp
+      }
+      case _ => {
+        //println("case3: " + ArrayBuffer(n.children.toList))
+        ArrayBuffer(n.children.toList)
       }
     }
-    result ++= newChildrenList.map {
-      newChildren => n.withChildren(newChildren)
+    //println(n.children)
+    //println(newChildrenList)
+    var newlist = newChildrenList.map {
+      newChildren => newChildren.map{
+        oneChildren => {
+          //println(n.children)
+          //println(oneChildren)
+          n.withChildren(oneChildren) }//big performance impact! using withChildren
+      }
     }
+    newlist.map (listelem => result ++= listelem)
+    //println("result: " + result)
     result
   }
-
-
-
 }
diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
index 562ac869a..363a15d04 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
@@ -190,13 +190,32 @@ class DeepSimplifierTest extends AnyFunSuite with Matchers{
   test("test14") {
     val a = LocalVar("a", Bool)()
     val z = LocalVar("z", Bool)()
+    val y = Not(a)()
     val b = Or(Not(Not(a)())(), a)()
     val c = Or(Not(a)(), a)()
     val d = Or(Not(Not(a)())(), Not(Not(Not(Not(z)())())())())()
+    val e = Or(d, Not(Not(Not(Not(z)())())())())()
 
-    println(d.children)
+    //println(e)
+    /*
+    println(a.isInstanceOf[Node])
 
-    pfRecSimplify(d)
+    println(a.subnodes)
+    println(a.children)
+    println(a.getClass)
+    println(a.children.map(child => child.getClass))
+    println(a.subnodes.map(child => child.isInstanceOf[AtomicType]))
+
+    println(c.subnodes)
+    println(c.children)
+    println(c.getClass)
+    println(c.children.map(child => child.getClass))
+    println(c.subnodes.map(child => child.isInstanceOf[AtomicType]))
+    */
+    //println(e.subnodes)
+    //println(e.children)
+
+    println(simplify(d))
 
     true should be(true)
   }

From a8856d58972f9b1d2a8808928044a923b3498c10 Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Tue, 3 Dec 2024 09:32:15 +0100
Subject: [PATCH 04/10] additions DeepSimplifier

---
 .../deepsimplifier/DeepSimplifier.scala       |  93 +++++++++---
 .../deepsimplifier/DeepSimplifierTest.scala   | 139 ++++++++++++++----
 2 files changed, 180 insertions(+), 52 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
index 7d5fb4d1d..c0ae20bab 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
@@ -12,15 +12,13 @@ object DeepSimplifier {
     val visited: ArrayBuffer[N] = ArrayBuffer(n)
     val queue: mutable.Queue[N] = mutable.Queue(n)
 
-    while (queue.nonEmpty) {
+    while (queue.nonEmpty && visited.length < 50000) { //TODO: hardcoded stop, make this an input
       val currnode: N = queue.dequeue()
       println("currnode: " + currnode)
-      //val generated: ArrayBuffer[N] = recursiveSimplify(currnode)
       val generated: ArrayBuffer[N] = pfRecSimplify(currnode)
       println("generated: " + generated)
 
       for (g <- generated if !visited.contains(g)) {
-        //println("new g: " + g)
 
         visited.append(g)
         queue.enqueue(g)
@@ -50,9 +48,74 @@ object DeepSimplifier {
     val result: ArrayBuffer[Node] = ArrayBuffer()
 
     val cases: List[PartialFunction[N, Node]] = List(
+      { case root@Not(BoolLit(literal)) => BoolLit(!literal)(root.pos, root.info) },
+      { case root@Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info) },
+      { case root@Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(GeCmp(a, b)) => LtCmp(a, b)(root.pos, root.info) },
+      { case root@Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info) },
+
+      //TODO
+      { case root@NeCmp(left, right) => Not(EqCmp(left, right)())(root.pos, root.info)},
+
       { case Not(Not(single)) => single },
+
+      { case Or(FalseLit(), right) => right },
+      { case Or(left, FalseLit()) => left },
       { case root@Or(TrueLit(), _) => TrueLit()(root.pos, root.info) },
-      { case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info) }
+      { case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info) },
+
+      { case And(TrueLit(), right) => right },
+      { case And(left, TrueLit()) => left },
+      { case root@And(FalseLit(), _) => FalseLit()(root.pos, root.info) },
+      { case root@And(_, FalseLit()) => FalseLit()(root.pos, root.info) },
+
+      //associativity
+      //WARNING: position and info attribute not correctly maintained for lchild, left and right
+      { case root@And(lchild@And(left, right), rchild) => And(left, And(right, rchild)())(root.pos, root.info)},
+      { case root@And(lchild, rchild@And(left, right)) => And(And(lchild, left)(), right)(root.pos, root.info)},
+
+      { case root@Or(lchild@Or(left, right), uright) => Or(left, Or(right, uright)())(root.pos, root.info)},
+      { case root@Or(uleft, rchild@Or(left, right)) => Or(Or(uleft, left)(), right)(root.pos, root.info)},
+
+      //implication rules
+
+      { case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info) },
+      { case Implies(TrueLit(), consequent) => consequent },
+      { case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(), r)(root.pos, root.info) },
+
+      { case And(Implies(l1, r1), Implies(Not(l2), r2)) if(l1 == l2 && r1 == r2) => r1 },
+
+      //contrapositive
+      { case root@Implies(left, right) => Implies(Not(right)(), Not(left)())(root.pos, root.info) },
+      { case root@Implies(Not(left), Not(right)) => Implies(right, left)(root.pos, root.info) },
+
+      //modus ponens & modus tollens
+
+      //implies to or
+      { case root@Implies(left, right) => Or(Not(left)(), right)(root.pos, root.info)},
+      { case root@Or(Not(left), right) => Implies(left, right)(root.pos, root.info)},
+
+      //extended rules and/or
+      //pos attribute!!
+      { case root@Not(nchild@And(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
+      { case root@And(Not(left), Not(right)) => Not(And(left, right)())(root.pos, root.info)},
+
+
+      //de morgan
+      { case root@Not(Or(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
+      { case root@And(Not(left), Not(right)) => Not(Or(left, right)())(root.pos, root.info)},
+
+      { case root@Not(And(left, right)) => Or(Not(left)(), Not(right)())(root.pos, root.info)},
+      { case root@Or(Not(left), Not(right)) => Not(And(left, right)())(root.pos, root.info)},
+
+
+
+
+
+
+
     )
 
     result ++= cases.collect { case lcase if lcase.isDefinedAt(n) => lcase(n) }
@@ -62,45 +125,33 @@ object DeepSimplifier {
 
   def pfRecSimplify[N <: Node](n: N): ArrayBuffer[N] = {
     val result: ArrayBuffer[N] = ArrayBuffer()
-
-
+    result ++= pfSimplify(n)
     val newChildrenList = n.children.zipWithIndex.map {
       case (child: AtomicType, index) => {
-        //println(child)
-        //println("case1: " + ArrayBuffer(n.children.toList))
-        Nil
-        ArrayBuffer(n.children.toList)
+        ArrayBuffer()
       }
       case (child: N, index) => {
-        //println("case2")
         val temp = new ArrayBuffer[List[Any]]()
           temp ++=pfSimplify(child).map { pfSimpChild =>
           n.children.toList.updated(index, pfSimpChild)
         }
-        //println("case2: " + temp)
         temp ++= pfRecSimplify(child).toList.map { recSimpChild =>
           n.children.toList.updated(index, recSimpChild)
         }
-        //println("case2after: " + temp)
         temp
       }
       case _ => {
-        //println("case3: " + ArrayBuffer(n.children.toList))
-        ArrayBuffer(n.children.toList)
+        ArrayBuffer()
       }
     }
-    //println(n.children)
-    //println(newChildrenList)
+
     var newlist = newChildrenList.map {
       newChildren => newChildren.map{
         oneChildren => {
-          //println(n.children)
-          //println(oneChildren)
-          n.withChildren(oneChildren) }//big performance impact! using withChildren
+          n.withChildren(oneChildren) }//withChildren has big performance impact!
       }
     }
     newlist.map (listelem => result ++= listelem)
-    //println("result: " + result)
     result
   }
 }
diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
index 363a15d04..4e7523678 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
@@ -12,6 +12,114 @@ import scala.collection.mutable.ArrayBuffer
 
 class DeepSimplifierTest extends AnyFunSuite with Matchers{
 
+  test("not1"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = And(a, And(b,c)())()
+    val e = And(And(a,b)(), c)()
+
+    println(simplify(d))
+    println(simplify(e))
+
+    true should be(true)
+  }
+
+  test("not2"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
+
+    println(d)
+    println(simplify(d))
+
+    true should be(true)
+  }
+  test("not3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
+
+    println(d)
+    println(simplify(d))
+
+    true should be(true)
+  }
+  test("not4"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = Implies(a, b)()
+
+    println(d)
+    println(simplify(d))
+
+    true should be(true)
+  }
+  test("not5"){
+    //how do i define null in the tree?
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val z = NullLit()()
+    val y = NullLit()()
+    val c = LocalVar("c", Bool)()
+    val aa = EqCmp(a, z)()
+    val bb = EqCmp(b, y)()
+    val d = And(Implies(aa, c)(), Implies(Not(aa)(), c)())()
+
+    println(d)
+    println(simplify(d))
+
+    true should be(true)
+  }
+
+  test("test1") {
+    val a = Not(LocalVar("a", Bool)())()
+    val b = Not(LocalVar("b", Bool)())()
+    val c = Or(Or(a, b)(), FalseLit()())()
+    println(simplify(c))
+    true should be(true)
+
+  }
+
+  test("test14") {
+    val a = LocalVar("a", Bool)()
+    val z = LocalVar("z", Bool)()
+    val y = Not(a)()
+    val b = Or(Not(Not(a)())(), a)()
+    val c = Or(Not(a)(), a)()
+    val d = Or(Not(Not(a)())(), Not(Not(Not(Not(z)())())())())()
+    val e = Or(d, Not(Not(Not(Not(z)())())())())()
+    val f = Or(d, Not(Not(Not(Not(FalseLit()())())())())())()
+
+    println(f)
+    /*
+    println(a.isInstanceOf[Node])
+
+    println(a.subnodes)
+    println(a.children)
+    println(a.getClass)
+    println(a.children.map(child => child.getClass))
+    println(a.subnodes.map(child => child.isInstanceOf[AtomicType]))
+
+    println(c.subnodes)
+    println(c.children)
+    println(c.getClass)
+    println(c.children.map(child => child.getClass))
+    println(c.subnodes.map(child => child.isInstanceOf[AtomicType]))
+    */
+    //println(e.subnodes)
+    //println(e.children)
+
+    println(simplify(f))
+
+    true should be(true)
+  }
+
+
+
+
+
+
   /*test("test1") {
 
     val a = LocalVar("a", Bool)()
@@ -187,38 +295,7 @@ class DeepSimplifierTest extends AnyFunSuite with Matchers{
 
    */
 
-  test("test14") {
-    val a = LocalVar("a", Bool)()
-    val z = LocalVar("z", Bool)()
-    val y = Not(a)()
-    val b = Or(Not(Not(a)())(), a)()
-    val c = Or(Not(a)(), a)()
-    val d = Or(Not(Not(a)())(), Not(Not(Not(Not(z)())())())())()
-    val e = Or(d, Not(Not(Not(Not(z)())())())())()
-
-    //println(e)
-    /*
-    println(a.isInstanceOf[Node])
-
-    println(a.subnodes)
-    println(a.children)
-    println(a.getClass)
-    println(a.children.map(child => child.getClass))
-    println(a.subnodes.map(child => child.isInstanceOf[AtomicType]))
-
-    println(c.subnodes)
-    println(c.children)
-    println(c.getClass)
-    println(c.children.map(child => child.getClass))
-    println(c.subnodes.map(child => child.isInstanceOf[AtomicType]))
-    */
-    //println(e.subnodes)
-    //println(e.children)
-
-    println(simplify(d))
 
-    true should be(true)
-  }
 
 
 }

From 80e3a5d6adcd05424e351ec8715c55200de63205 Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Sun, 15 Dec 2024 20:52:57 +0100
Subject: [PATCH 05/10] Rules Implication and EqualityComparison in
 DeepSimplifier Tests for every rule implemented in Deepsimplifier

---
 .../deepsimplifier/DeepSimplifier.scala       | 150 +++-
 .../deepsimplifier/DeepSimplifierTest.scala   | 678 ++++++++++++++++--
 2 files changed, 743 insertions(+), 85 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
index c0ae20bab..55938e24c 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
@@ -7,48 +7,57 @@ import scala.collection.mutable._
 
 object DeepSimplifier {
 
-  def simplify[N <: Node](n: N): N = {
+  def simplify[N <: Node](n: N, assumeWelldefinedness: Boolean = false, iterationLimit: Integer = 5000, printToConsole: Boolean = false): N = {
 
     val visited: ArrayBuffer[N] = ArrayBuffer(n)
     val queue: mutable.Queue[N] = mutable.Queue(n)
 
-    while (queue.nonEmpty && visited.length < 50000) { //TODO: hardcoded stop, make this an input
+    while (queue.nonEmpty && visited.length < iterationLimit) {
       val currnode: N = queue.dequeue()
-      println("currnode: " + currnode)
-      val generated: ArrayBuffer[N] = pfRecSimplify(currnode)
-      println("generated: " + generated)
+      if(printToConsole) {
+        println("currnode: " + currnode)
+      }
 
+      val generated: ArrayBuffer[N] = pfRecSimplify(currnode, assumeWelldefinedness)
+      if(printToConsole) {
+        println("generated: " + generated)
+      }
       for (g <- generated if !visited.contains(g)) {
-
         visited.append(g)
         queue.enqueue(g)
       }
     }
 
-    println("result simplify: " + visited)
+    if(printToConsole){
+      println("result simplify: " + visited)
+    }
 
     getShortest(visited)
   }
 
   // only called with nonempty ArrayBuffers TODO: what happens if empty?
-  // TODO: make private
 
-  def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
+
+  private def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
     visited.minBy(treeSize)
   }
 
   // "counts every node twice", ie "LocalVar("a", Bool)()" is counted once as "a" and once as "Bool", at least it's consistent
-  // TODO: make private
-  def treeSize[N <: Node](n: N): Int = {
+
+  private def treeSize[N <: Node](n: N): Int = {
     n.reduceTree[Int]((node, count) => (count.sum + 1))
   }
+  private def treeHasDoubleNeg[N <: Node](n: N): Boolean = {
+    n.reduceTree[Boolean]((node, doubleNegs) => doubleNegs.contains(true) || isDoubleNeg(node))
+  }
 
-  def pfSimplify[N <: Node](n: N): ArrayBuffer[N] = {
+  private def pfSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
 
     val result: ArrayBuffer[Node] = ArrayBuffer()
 
     val cases: List[PartialFunction[N, Node]] = List(
       { case root@Not(BoolLit(literal)) => BoolLit(!literal)(root.pos, root.info) },
+
       { case root@Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info) },
       { case root@Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info) },
       { case root@Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info) },
@@ -56,8 +65,16 @@ object DeepSimplifier {
       { case root@Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info) },
       { case root@Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info) },
 
-      //TODO
-      { case root@NeCmp(left, right) => Not(EqCmp(left, right)())(root.pos, root.info)},
+
+      //TODO: try to find case where these could be used, then figure out a better way to implement them
+      /*
+      { case root@NeCmp(left, right) => Not(EqCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@EqCmp(left, right) => Not(NeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@GtCmp(left, right) => Not(LeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@GeCmp(left, right) => Not(LtCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@LtCmp(left, right) => Not(GeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@LeCmp(left, right) => Not(GtCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      */
 
       { case Not(Not(single)) => single },
 
@@ -71,6 +88,14 @@ object DeepSimplifier {
       { case root@And(FalseLit(), _) => FalseLit()(root.pos, root.info) },
       { case root@And(_, FalseLit()) => FalseLit()(root.pos, root.info) },
 
+      //Idempotence
+      { case root@And(a, b) if assumeWelldefinedness && a == b => a},
+      { case root@Or(a, b) if assumeWelldefinedness && a == b => a},
+
+      { case root@And(a, b) => And(b, a)(root.pos, root.info)},
+      { case root@Or(a, b) => Or(b, a)(root.pos, root.info)},
+
+
       //associativity
       //WARNING: position and info attribute not correctly maintained for lchild, left and right
       { case root@And(lchild@And(left, right), rchild) => And(left, And(right, rchild)())(root.pos, root.info)},
@@ -80,28 +105,29 @@ object DeepSimplifier {
       { case root@Or(uleft, rchild@Or(left, right)) => Or(Or(uleft, left)(), right)(root.pos, root.info)},
 
       //implication rules
-
+      //WARNING: position and info attributes not correctly maintained
       { case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info) },
       { case Implies(TrueLit(), consequent) => consequent },
       { case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(), r)(root.pos, root.info) },
 
-      { case And(Implies(l1, r1), Implies(Not(l2), r2)) if(l1 == l2 && r1 == r2) => r1 },
+      { case And(Implies(l1, r1), Implies(Not(l2), r2)) if assumeWelldefinedness && (l1 == l2 && r1 == r2) => r1 },
+
+      { case root@And(Implies(a, b), Implies(a2, c)) if a == a2 => Implies(a, And(b, c)())(root.pos, root.info) },
+      { case And(Implies(a, b), Implies(Not(a2), b2)) if assumeWelldefinedness && a == a2 && b == b2 => b },
+      { case root@And(a, Implies(a2, b)) if a == a2 => And(a, b)(root.pos, root.info) },
 
       //contrapositive
-      { case root@Implies(left, right) => Implies(Not(right)(), Not(left)())(root.pos, root.info) },
+      //{ case root@Implies(left, right) if !(isDoubleNeg(left) || isDoubleNeg(right)) => Implies(Not(right)(), Not(left)())(root.pos, root.info) },
       { case root@Implies(Not(left), Not(right)) => Implies(right, left)(root.pos, root.info) },
 
       //modus ponens & modus tollens
 
       //implies to or
-      { case root@Implies(left, right) => Or(Not(left)(), right)(root.pos, root.info)},
-      { case root@Or(Not(left), right) => Implies(left, right)(root.pos, root.info)},
+      //{ case root@Implies(left, right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Or(Not(left)(), right)(root.pos, root.info)},
+      //{ case root@Or(Not(left), right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Implies(left, right)(root.pos, root.info)},
 
       //extended rules and/or
       //pos attribute!!
-      { case root@Not(nchild@And(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
-      { case root@And(Not(left), Not(right)) => Not(And(left, right)())(root.pos, root.info)},
-
 
       //de morgan
       { case root@Not(Or(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
@@ -110,12 +136,68 @@ object DeepSimplifier {
       { case root@Not(And(left, right)) => Or(Not(left)(), Not(right)())(root.pos, root.info)},
       { case root@Or(Not(left), Not(right)) => Not(And(left, right)())(root.pos, root.info)},
 
+      //equality comparison
+
+      { case root@EqCmp(left, right) if assumeWelldefinedness && left == right => TrueLit()(root.pos, root.info) },
+      { case root@EqCmp(BoolLit(left), BoolLit(right)) => BoolLit(left == right)(root.pos, root.info) },
+      { case root@EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info) },
+      { case root@EqCmp(left, FalseLit()) => Not(left)(root.pos, root.info) },
+      { case EqCmp(TrueLit(), right) => right },
+      { case EqCmp(left, TrueLit()) => left },
+      { case root@EqCmp(IntLit(left), IntLit(right)) => BoolLit(left == right)(root.pos, root.info) },
+      { case root@EqCmp(NullLit(), NullLit()) => TrueLit()(root.pos, root.info) },
+
+      //nonequality comparison
+
+      { case root@NeCmp(BoolLit(left), BoolLit(right)) => BoolLit(left != right)(root.pos, root.info) },
+      { case NeCmp(FalseLit(), right) => right },
+      { case NeCmp(left, FalseLit()) => left },
+      { case root@NeCmp(TrueLit(), right) => Not(right)(root.pos, root.info) },
+      { case root@NeCmp(left, TrueLit()) => Not(left)(root.pos, root.info) },
+      { case root@NeCmp(IntLit(left), IntLit(right)) => BoolLit(left != right)(root.pos, root.info) },
+      { case root@NeCmp(NullLit(), NullLit()) => FalseLit()(root.pos, root.info) },
+      { case root@NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info) },
+
+      //extended equality/nonequality comparison
+      //some possible rules could introduce more statements, but not these ones
+      { case root@EqCmp(left, right) => EqCmp(right, left)(root.pos, root.info) },
+      { case root@NeCmp(left, right) => NeCmp(right, left)(root.pos, root.info) },
+      //{ case root@EqCmp(left, right) => Not(NeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      //{ case root@NeCmp(left, right) => Not(EqCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@Not(EqCmp(left, right)) => NeCmp(left, right)(root.pos, root.info) },
+      { case root@Not(NeCmp(left, right)) => EqCmp(left, right)(root.pos, root.info) },
+      { case root@And(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => FalseLit()(root.pos, root.info)},
+      { case root@Or(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => TrueLit()(root.pos, root.info)},
+
+      //conditional expressions
+
+      { case CondExp(TrueLit(), ifTrue, _) => ifTrue },
+      { case CondExp(FalseLit(), _, ifFalse) => ifFalse },
+      { case CondExp(_, ifTrue, ifFalse) if assumeWelldefinedness && ifTrue == ifFalse => ifTrue },
+      { case root@CondExp(condition, FalseLit(), TrueLit()) => Not(condition)(root.pos, root.info) },
+      { case CondExp(condition, TrueLit(), FalseLit()) => condition },
+      { case root@CondExp(condition, FalseLit(), ifFalse) => And(Not(condition)(), ifFalse)(root.pos, root.info) },
+      { case root@CondExp(condition, TrueLit(), ifFalse) =>
+        if (ifFalse.isPure) {
+          Or(condition, ifFalse)(root.pos, root.info)
+        } else {
+          Implies(Not(condition)(), ifFalse)(root.pos, root.info)
+        }
+      },
+      { case root@CondExp(condition, ifTrue, FalseLit()) => And(condition, ifTrue)(root.pos, root.info) },
+      { case root@CondExp(condition, ifTrue, TrueLit()) => Implies(condition, ifTrue)(root.pos, root.info) },
 
+      //forall&exists
 
+      //extended rules equality comparison
 
+      //accessibility
 
-
-
+      //fieldaccess and/extends locationaccess (see Expression.scala)
+      //locationaccess: loc
+      //fieldaccess: field and loc
+      //example: fieldaccess(loc.next) && locationaccess(loc) => locationaccess(loc)
+      //fieldaccess: layers? maybe go from field -> field.parent? or is field guaranteed to be a direct child?
     )
 
     result ++= cases.collect { case lcase if lcase.isDefinedAt(n) => lcase(n) }
@@ -123,19 +205,29 @@ object DeepSimplifier {
     result.asInstanceOf[ArrayBuffer[N]]
   }
 
-  def pfRecSimplify[N <: Node](n: N): ArrayBuffer[N] = {
+  private def isSingleNeg[N <: Node](n: N): Boolean = n match {
+    case Not(_) => true
+    case _ => false
+  }
+
+  private def isDoubleNeg[N <: Node](n: N): Boolean = n match {
+    case Not(Not(_)) => true
+    case _ => false
+  }
+
+  private def pfRecSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
     val result: ArrayBuffer[N] = ArrayBuffer()
-    result ++= pfSimplify(n)
+    result ++= pfSimplify(n, assumeWelldefinedness)
     val newChildrenList = n.children.zipWithIndex.map {
       case (child: AtomicType, index) => {
         ArrayBuffer()
       }
       case (child: N, index) => {
         val temp = new ArrayBuffer[List[Any]]()
-          temp ++=pfSimplify(child).map { pfSimpChild =>
+          temp ++=pfSimplify(child, assumeWelldefinedness).map { pfSimpChild =>
           n.children.toList.updated(index, pfSimpChild)
         }
-        temp ++= pfRecSimplify(child).toList.map { recSimpChild =>
+        temp ++= pfRecSimplify(child, assumeWelldefinedness).toList.map { recSimpChild =>
           n.children.toList.updated(index, recSimpChild)
         }
         temp
@@ -145,7 +237,7 @@ object DeepSimplifier {
       }
     }
 
-    var newlist = newChildrenList.map {
+    val newlist = newChildrenList.map {
       newChildren => newChildren.map{
         oneChildren => {
           n.withChildren(oneChildren) }//withChildren has big performance impact!
diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
index 4e7523678..461503e11 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
@@ -4,59 +4,611 @@ import org.scalatest.funsuite.AnyFunSuite
 
 import scala.language.implicitConversions
 import org.scalatest.matchers.should.Matchers
-import viper.silver.ast.DomainBinExp.unapply
 import viper.silver.ast.{Node, _}
 import viper.silver.ast.utility.deepsimplifier.DeepSimplifier._
 
-import scala.collection.mutable.ArrayBuffer
-
 class DeepSimplifierTest extends AnyFunSuite with Matchers{
 
-  test("not1"){
+  test("Cmp1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(EqCmp(a,b)())()
+
+    simplify(c) should be (NeCmp(a,b)())
+  }
+
+  test("Cmp2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(NeCmp(a,b)())()
+
+    simplify(c) should be (EqCmp(a,b)())
+  }
+
+  test("Cmp3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(GtCmp(a,b)())()
+
+    simplify(c) should be (LeCmp(a,b)())
+  }
+
+  test("Cmp4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(GeCmp(a,b)())()
+
+    simplify(c) should be (LtCmp(a,b)())
+  }
+
+  test("Cmp5") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(LtCmp(a,b)())()
+
+    simplify(c) should be (GeCmp(a,b)())
+  }
+
+  test("Cmp6") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(LeCmp(a,b)())()
+
+    simplify(c) should be (GtCmp(a,b)())
+  }
+
+
+  test("notnot1") {
+    val a = LocalVar("a", Bool)()
+
+    simplify(Not(Not(a)())()) should be (a)
+  }
+
+
+  test("or1"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(FalseLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("or2"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(a, FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("or3"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(TrueLit()(), a)()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+  test("or4"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(a, TrueLit()())()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+
+  test("and1") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(TrueLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("and2") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(a, TrueLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("and3") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(FalseLit()(), a)()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("and4") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(a, FalseLit()())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("idem1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(And(a,b)(),a)()
+
+    simplify(expr, true) should (be (And(a,b)()) or be (And(b,a)()))
+  }
+
+  test("idem2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(b,And(a,b)())()
+
+    simplify(expr, true) should (be (And(a,b)()) or be (And(b,a)()))
+  }
+
+  test("idem3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(Or(a,b)(),a)()
+
+    simplify(expr, true) should (be (Or(a,b)()) or be (Or(b,a)()))
+  }
+
+  test("idem4"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(b,Or(a,b)())()
+
+    simplify(expr, true) should (be (Or(a,b)()) or be (Or(b,a)()))
+  }
+
+  //while these do cannot verify if associativity of or/and is being applied, they should catch some cases where associativity is incorrectly applied
+  test("assoc1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = And(a,And(b,c)())()
+
+    simplify(expr) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
+
+  test("assoc2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = And(And(a, b)(), c)()
+
+    simplify(expr) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
+
+  test("assoc3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = Or(a,Or(b,c)())()
+
+    simplify(expr) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
+  }
+
+  test("assoc4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = Or(Or(a, b)(), c)()
+
+    simplify(expr) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
+  }
+
+  test("and11") {
     val a = LocalVar("a", Bool)()
     val b = LocalVar("b", Bool)()
     val c = LocalVar("c", Bool)()
     val d = And(a, And(b,c)())()
-    val e = And(And(a,b)(), c)()
+    val expr = And(And(a,b)(), And(a,c)())()
 
-    println(simplify(d))
-    println(simplify(e))
+    simplify(expr, true) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
 
-    true should be(true)
+  test("or11") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = Or(a, Or(b,c)())()
+    val expr = Or(Or(a,b)(), Or(a,c)())()
+
+    simplify(expr, true) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
   }
 
-  test("not2"){
+  test("impl1") {
     val a = LocalVar("a", Bool)()
     val b = LocalVar("b", Bool)()
-    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
+    val expr = Implies(a, b)()
 
-    println(d)
-    println(simplify(d))
+    simplify(expr) should be (Implies(a, b)())
+  }
 
-    true should be(true)
+  test("impl2") {
+    val a = FalseLit()()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(a, b)()
+
+    simplify(expr) should be (TrueLit()())
   }
-  test("not3"){
+
+  test("impl3") {
+    val a = TrueLit()()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(a, b)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl4") {
+    val a = LocalVar("a", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = Implies(a,c)()
+    val expr = Implies(a, d)()
+
+    simplify(expr, true) should be (Implies(a, c)())
+  }
+
+  test("impl5") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Implies(a,b)()
+    val d = Implies(Not(a)(),b)()
+    val expr = And(c, d)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl6") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Implies(a,b)()
+    val d = Implies(Not(a)(),b)()
+    val expr = And(c, d)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl7") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(Not(b)(), Not(a)())()
+
+    simplify(expr) should be (Implies(a, b)())
+  }
+
+  test("and21") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(And(a,Not(b)())())()
+
+    simplify(expr) should be (Or(Not(a)(), b)())
+  }
+
+  test("and22") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(Or(a,b)())())
+  }
+
+  test("dem1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(Or(Not(a)(),Not(b)())())()
+
+    simplify(expr) should be (And(a,b)())
+  }
+
+  test("dem2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(Or(a,b)())())
+  }
+
+  test("dem3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(And(Not(a)(),Not(b)())())()
+
+    simplify(expr) should be (Or(a,b)())
+  }
+
+  test("dem4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(And(a,b)())())
+  }
+
+
+  test("eq1 assumeWelldefinedness") {
+    val x = LocalVar("x", Bool)()
+    val expr = EqCmp(x, x)()
+
+    simplify(expr, true) should be (TrueLit()())
+  }
+
+  test("eq2") {
+    val expr = EqCmp(BoolLit(true)(), BoolLit(true)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq2bis") {
+    val expr = EqCmp(BoolLit(true)(), BoolLit(false)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq3") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(FalseLit()(), a)()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq4") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(a, FalseLit()())()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq5") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(TrueLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq6") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(a, TrueLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq7") {
+    val expr = EqCmp(IntLit(32)(), IntLit(32)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq7bis") {
+    val expr = EqCmp(IntLit(32)(), IntLit(31)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq8") {
+    val expr = EqCmp(NullLit()(), NullLit()())()
+
+    simplify(expr) should be (TrueLit()(expr.pos, expr.info))
+  }
+
+
+
+  test("eq10") {
+    val expr = NeCmp(BoolLit(true)(), BoolLit(true)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq10bis") {
+    val expr = NeCmp(BoolLit(true)(), BoolLit(false)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq11") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(FalseLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq12") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(a, FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq13") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(TrueLit()(), a)()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq14") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(a, TrueLit()())()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq15") {
+    val expr = NeCmp(IntLit(32)(), IntLit(32)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+  test("eq15bis") {
+    val expr = NeCmp(IntLit(32)(), IntLit(31)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq16") {
+    val expr = NeCmp(NullLit()(), NullLit()())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("eq17 assumeWelldefinedness") {
+    val x = LocalVar("x", Bool)()
+    val expr = NeCmp(x, x)()
+
+    simplify(expr, true) should be (FalseLit()())
+  }
+  test("eq17bis assumeWelldefinedness") {
+    val expr = NeCmp(IntLit(5)(), IntLit(5)())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+  test("eq17ter assumeWelldefinedness") {
+    val expr = NeCmp(IntLit(5)(), IntLit(6)())()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+
+  test("eq20 assumeWelldefinedness") {
+    val a = LocalVar("a", Int)()
+    val b = LocalVar("b", Int)()
+
+    val expr = And(
+      EqCmp(a, b)(),
+      NeCmp(a, b)()
+    )()
+
+    simplify(expr, true) should be (FalseLit()())
+  }
+
+
+  test("eq21 assumeWelldefinedness") {
+    val a = LocalVar("a", Int)()
+    val b = LocalVar("b", Int)()
+
+    val expr = Or(
+      EqCmp(a, b)(),
+      NeCmp(a, b)()
+    )()
+
+    simplify(expr, true) should be (TrueLit()())
+  }
+
+  test("ce1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val ifFalse = BoolLit(false)()
+    val expr = CondExp(TrueLit()(), a, b)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("ce2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val ifFalse = BoolLit(false)()
+    val expr = CondExp(FalseLit()(), a, b)()
+
+    simplify(expr) should be (b)
+  }
+
+  test("ce3 assumeWelldefinedness") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(b, a, a)()
+
+    simplify(expr, true) should be (a)
+  }
+
+  test("ce4") {
+    val a = LocalVar("a", Bool)()
+    val expr = CondExp(a, FalseLit()(), TrueLit()())()
+
+    simplify(expr) should be (Not(a)(expr.pos, expr.info))
+  }
+
+  test("ce5") {
+    val a = LocalVar("a", Bool)()
+    val expr = CondExp(a, TrueLit()(), FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("ce6") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, FalseLit()(), Not(a)())()
+
+    simplify(expr) should be (Not(Or(a,a)())())
+  }
+  test("ce6bis assumeWelldefinedeness") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, FalseLit()(), Not(a)())()
+
+    simplify(expr, true) should be (Not(a)())
+  }
+
+  test("ce7") {
+    val a = LocalVar("a", Bool)()
+    val z = BoolLit(false)() //z must be pure/z.isPure == true
+    val expr = CondExp(a, TrueLit()(), z)()
+
+    simplify(expr) should be (a) //(a || false) = a
+  }
+
+  test("ce8") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, b, FalseLit()())()
+
+    simplify(expr) should be (And(a, b)())
+  }
+
+  test("ce9") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, b, TrueLit()())()
+
+    simplify(expr) should be (Implies(a, b)())
+  }
+
+
+
+
+
+
+
+
+
+
+
+  test("and5 assumeWelldefinedness"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = And(a, And(b,c)())()
+    val e = And(And(a,b)(), And(a,c)())()
+
+    simplify(e, true) should (be (And(And(a,b)(),c)()) or be (And(And(a,b)(),c)()))
+  }
+
+  test("implies1"){
     val a = LocalVar("a", Bool)()
     val b = LocalVar("b", Bool)()
     val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
 
-    println(d)
-    println(simplify(d))
+    simplify(d, true) should be (b)
+  }
+  test("not3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
 
-    true should be(true)
+    simplify(d, true) should be (b)
   }
-  test("not4"){
+  test("implies2"){
     val a = LocalVar("a", Bool)()
     val b = LocalVar("b", Bool)()
     val d = Implies(a, b)()
 
-    println(d)
-    println(simplify(d))
-
-    true should be(true)
+    simplify(d) should be (d)
   }
-  test("not5"){
-    //how do i define null in the tree?
+  test("implies3"){
     val a = LocalVar("a", Bool)()
     val b = LocalVar("b", Bool)()
     val z = NullLit()()
@@ -66,53 +618,67 @@ class DeepSimplifierTest extends AnyFunSuite with Matchers{
     val bb = EqCmp(b, y)()
     val d = And(Implies(aa, c)(), Implies(Not(aa)(), c)())()
 
-    println(d)
-    println(simplify(d))
-
-    true should be(true)
+    simplify(d, true) should be(c)
   }
 
   test("test1") {
-    val a = Not(LocalVar("a", Bool)())()
-    val b = Not(LocalVar("b", Bool)())()
-    val c = Or(Or(a, b)(), FalseLit()())()
-    println(simplify(c))
-    true should be(true)
-
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Or(Or(Not(a)(), Not(b)())(), FalseLit()())()
+    simplify(c) should (be (Not(And(a,b)())()) or be (Not(And(b,a)())()))
   }
 
   test("test14") {
     val a = LocalVar("a", Bool)()
     val z = LocalVar("z", Bool)()
-    val y = Not(a)()
-    val b = Or(Not(Not(a)())(), a)()
-    val c = Or(Not(a)(), a)()
     val d = Or(Not(Not(a)())(), Not(Not(Not(Not(z)())())())())()
-    val e = Or(d, Not(Not(Not(Not(z)())())())())()
     val f = Or(d, Not(Not(Not(Not(FalseLit()())())())())())()
 
-    println(f)
-    /*
-    println(a.isInstanceOf[Node])
+    simplify(f) should (be (Or(a,z)()) or be (Or(z,a)()))
+  }
 
-    println(a.subnodes)
-    println(a.children)
-    println(a.getClass)
-    println(a.children.map(child => child.getClass))
-    println(a.subnodes.map(child => child.isInstanceOf[AtomicType]))
+  test("eqcmp1") {
+    val a = LocalVar("a", Bool)()
+    val d = EqCmp(a, a)()
+    simplify(d, true) should be(TrueLit()(d.pos, d.info))
+  }
 
-    println(c.subnodes)
-    println(c.children)
-    println(c.getClass)
-    println(c.children.map(child => child.getClass))
-    println(c.subnodes.map(child => child.isInstanceOf[AtomicType]))
-    */
-    //println(e.subnodes)
-    //println(e.children)
+  test("eqcmp2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = NeCmp(a, b)()
+    val d = EqCmp(a, b)()
+    val e = And(c, d)()
+    val f = Or(c, d)()
 
-    println(simplify(f))
+    simplify(e, true) should be(FalseLit()(e.pos, e.info))
+    simplify(f, true) should be(TrueLit()(f.pos, f.info))
+  }
 
-    true should be(true)
+  test("eqcmp3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = NeCmp(a, b)()
+    val d = EqCmp(a, b)()
+    val e = And(c, d)()
+    val f = Or(c, d)()
+
+    simplify(e, true) should be(FalseLit()(e.pos, e.info))
+    simplify(f, true) should be(TrueLit()(f.pos, f.info))
+  }
+
+  test("neue") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+
+    simplify (And(Implies(a, b)(), Implies(a, c)())()) should be (Implies(a, And(b, c)())())
+
+    simplify (And(Implies(a, b)(), Implies(Not(a)(), b)())()) should be (And(Implies(a,b)(),Implies(Not(a)(), b)())())
+    simplify (And(Implies(a, b)(), Implies(Not(a)(), b)())(), true) should be (b)
+
+    simplify (And(a, Implies(a, b)())()) should be (And(a, b)())
   }
 
 

From a97d08b8813122430e89f4d80e5c5c4e095aa590 Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Sun, 15 Dec 2024 22:00:33 +0100
Subject: [PATCH 06/10] DeepSimplifier->IterativeSimplifier

Maintained code at old position, new modules IterativeSimplifier and IterativeSimplifierTest in same positions as Simplifier and SimplifierTest respectively
---
 .../ast/utility/IterativeSimplifier.scala     | 234 +++++
 .../deepsimplifier/DeepSimplifier.scala       |  17 +-
 src/test/scala/IterativeSimplifierTest.scala  | 865 ++++++++++++++++++
 3 files changed, 1100 insertions(+), 16 deletions(-)
 create mode 100644 src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
 create mode 100644 src/test/scala/IterativeSimplifierTest.scala

diff --git a/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala b/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
new file mode 100644
index 000000000..24d6bff20
--- /dev/null
+++ b/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
@@ -0,0 +1,234 @@
+package viper.silver.ast.utility
+
+import viper.silver.ast._
+
+import scala.collection.mutable
+import scala.collection.mutable._
+
+object IterativeSimplifier {
+
+  def simplify[N <: Node](n: N, assumeWelldefinedness: Boolean = false, iterationLimit: Integer = 5000, printToConsole: Boolean = false): N = {
+
+    val visited: ArrayBuffer[N] = ArrayBuffer(n)
+    val queue: mutable.Queue[N] = mutable.Queue(n)
+
+    while (queue.nonEmpty && visited.length < iterationLimit) {
+      val currnode: N = queue.dequeue()
+      if(printToConsole) {
+        println("currnode: " + currnode)
+      }
+
+      val generated: ArrayBuffer[N] = pfRecSimplify(currnode, assumeWelldefinedness)
+      if(printToConsole) {
+        println("generated: " + generated)
+      }
+      for (g <- generated if !visited.contains(g)) {
+        visited.append(g)
+        queue.enqueue(g)
+      }
+    }
+
+    if(printToConsole){
+      println("result simplify: " + visited)
+    }
+
+    getShortest(visited)
+  }
+
+  private def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
+    visited.minBy(treeSize)
+  }
+
+  // "counts every node twice", ie "LocalVar("a", Bool)()" is counted once as "a" and once as "Bool"
+  private def treeSize[N <: Node](n: N): Int = {
+    n.reduceTree[Int]((node, count) => (count.sum + 1))
+  }
+  private def treeHasDoubleNeg[N <: Node](n: N): Boolean = {
+    n.reduceTree[Boolean]((node, doubleNegs) => doubleNegs.contains(true) || isDoubleNeg(node))
+  }
+
+  private def pfSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
+
+    val result: ArrayBuffer[Node] = ArrayBuffer()
+
+    val cases: List[PartialFunction[N, Node]] = List(
+      { case root@Not(BoolLit(literal)) => BoolLit(!literal)(root.pos, root.info) },
+
+      { case root@Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info) },
+      { case root@Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(GeCmp(a, b)) => LtCmp(a, b)(root.pos, root.info) },
+      { case root@Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info) },
+      { case root@Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info) },
+
+
+      //TODO: try to find case where these could be used, then figure out a better way to implement them
+      /*
+      { case root@NeCmp(left, right) => Not(EqCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@EqCmp(left, right) => Not(NeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@GtCmp(left, right) => Not(LeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@GeCmp(left, right) => Not(LtCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@LtCmp(left, right) => Not(GeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@LeCmp(left, right) => Not(GtCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      */
+
+      { case Not(Not(single)) => single },
+
+      { case Or(FalseLit(), right) => right },
+      { case Or(left, FalseLit()) => left },
+      { case root@Or(TrueLit(), _) => TrueLit()(root.pos, root.info) },
+      { case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info) },
+
+      { case And(TrueLit(), right) => right },
+      { case And(left, TrueLit()) => left },
+      { case root@And(FalseLit(), _) => FalseLit()(root.pos, root.info) },
+      { case root@And(_, FalseLit()) => FalseLit()(root.pos, root.info) },
+
+      //Idempotence
+      { case root@And(a, b) if assumeWelldefinedness && a == b => a},
+      { case root@Or(a, b) if assumeWelldefinedness && a == b => a},
+
+      { case root@And(a, b) => And(b, a)(root.pos, root.info)},
+      { case root@Or(a, b) => Or(b, a)(root.pos, root.info)},
+
+
+      //associativity
+      //WARNING: position and info attribute not correctly maintained for lchild, left and right
+      { case root@And(And(left, right), rchild) => And(left, And(right, rchild)(root.pos, root.info))(root.pos, root.info)},
+      { case root@And(lchild, And(left, right)) => And(And(lchild, left)(root.pos, root.info), right)(root.pos, root.info)},
+
+      { case root@Or(Or(left, right), uright) => Or(left, Or(right, uright)(root.pos, root.info))(root.pos, root.info)},
+      { case root@Or(uleft, Or(left, right)) => Or(Or(uleft, left)(root.pos, root.info), right)(root.pos, root.info)},
+
+      //implication rules
+      //WARNING: position and info attributes not correctly maintained
+      { case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info) },
+      { case Implies(TrueLit(), consequent) => consequent },
+      { case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(root.pos, root.info), r)(root.pos, root.info) },
+
+      { case And(Implies(l1, r1), Implies(Not(l2), r2)) if assumeWelldefinedness && (l1 == l2 && r1 == r2) => r1 },
+
+      { case root@And(Implies(a, b), Implies(a2, c)) if a == a2 => Implies(a, And(b, c)(root.pos, root.info))(root.pos, root.info) },
+      { case And(Implies(a, b), Implies(Not(a2), b2)) if assumeWelldefinedness && a == a2 && b == b2 => b },
+      { case root@And(a, Implies(a2, b)) if a == a2 => And(a, b)(root.pos, root.info) },
+
+      //contrapositive
+      //{ case root@Implies(left, right) if !(isDoubleNeg(left) || isDoubleNeg(right)) => Implies(Not(right)(), Not(left)())(root.pos, root.info) },
+      { case root@Implies(Not(left), Not(right)) => Implies(right, left)(root.pos, root.info) },
+
+      //modus ponens & modus tollens
+
+      //implies to or
+      //{ case root@Implies(left, right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Or(Not(left)(), right)(root.pos, root.info)},
+      //{ case root@Or(Not(left), right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Implies(left, right)(root.pos, root.info)},
+
+      //extended rules and/or
+
+      //de morgan
+      { case root@Not(Or(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
+      { case root@And(Not(left), Not(right)) => Not(Or(left, right)())(root.pos, root.info)},
+
+      { case root@Not(And(left, right)) => Or(Not(left)(), Not(right)())(root.pos, root.info)},
+      { case root@Or(Not(left), Not(right)) => Not(And(left, right)())(root.pos, root.info)},
+
+      //equality comparison
+
+      { case root@EqCmp(left, right) if assumeWelldefinedness && left == right => TrueLit()(root.pos, root.info) },
+      { case root@EqCmp(BoolLit(left), BoolLit(right)) => BoolLit(left == right)(root.pos, root.info) },
+      { case root@EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info) },
+      { case root@EqCmp(left, FalseLit()) => Not(left)(root.pos, root.info) },
+      { case EqCmp(TrueLit(), right) => right },
+      { case EqCmp(left, TrueLit()) => left },
+      { case root@EqCmp(IntLit(left), IntLit(right)) => BoolLit(left == right)(root.pos, root.info) },
+      { case root@EqCmp(NullLit(), NullLit()) => TrueLit()(root.pos, root.info) },
+
+      //nonequality comparison
+
+      { case root@NeCmp(BoolLit(left), BoolLit(right)) => BoolLit(left != right)(root.pos, root.info) },
+      { case NeCmp(FalseLit(), right) => right },
+      { case NeCmp(left, FalseLit()) => left },
+      { case root@NeCmp(TrueLit(), right) => Not(right)(root.pos, root.info) },
+      { case root@NeCmp(left, TrueLit()) => Not(left)(root.pos, root.info) },
+      { case root@NeCmp(IntLit(left), IntLit(right)) => BoolLit(left != right)(root.pos, root.info) },
+      { case root@NeCmp(NullLit(), NullLit()) => FalseLit()(root.pos, root.info) },
+      { case root@NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info) },
+
+      //extended equality/nonequality comparison
+      //some possible rules could introduce more statements, but not these ones
+      { case root@EqCmp(left, right) => EqCmp(right, left)(root.pos, root.info) },
+      { case root@NeCmp(left, right) => NeCmp(right, left)(root.pos, root.info) },
+      //{ case root@EqCmp(left, right) => Not(NeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      //{ case root@NeCmp(left, right) => Not(EqCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
+      { case root@Not(EqCmp(left, right)) => NeCmp(left, right)(root.pos, root.info) },
+      { case root@Not(NeCmp(left, right)) => EqCmp(left, right)(root.pos, root.info) },
+      { case root@And(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => FalseLit()(root.pos, root.info)},
+      { case root@Or(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => TrueLit()(root.pos, root.info)},
+
+      //conditional expressions
+
+      { case CondExp(TrueLit(), ifTrue, _) => ifTrue },
+      { case CondExp(FalseLit(), _, ifFalse) => ifFalse },
+      { case CondExp(_, ifTrue, ifFalse) if assumeWelldefinedness && ifTrue == ifFalse => ifTrue },
+      { case root@CondExp(condition, FalseLit(), TrueLit()) => Not(condition)(root.pos, root.info) },
+      { case CondExp(condition, TrueLit(), FalseLit()) => condition },
+      { case root@CondExp(condition, FalseLit(), ifFalse) => And(Not(condition)(), ifFalse)(root.pos, root.info) },
+      { case root@CondExp(condition, TrueLit(), ifFalse) =>
+        if (ifFalse.isPure) {
+          Or(condition, ifFalse)(root.pos, root.info)
+        } else {
+          Implies(Not(condition)(), ifFalse)(root.pos, root.info)
+        }
+      },
+      { case root@CondExp(condition, ifTrue, FalseLit()) => And(condition, ifTrue)(root.pos, root.info) },
+      { case root@CondExp(condition, ifTrue, TrueLit()) => Implies(condition, ifTrue)(root.pos, root.info) },
+
+      //forall&exists
+    )
+
+    result ++= cases.collect { case lcase if lcase.isDefinedAt(n) => lcase(n) }
+
+    result.asInstanceOf[ArrayBuffer[N]]
+  }
+
+  private def isSingleNeg[N <: Node](n: N): Boolean = n match {
+    case Not(_) => true
+    case _ => false
+  }
+
+  private def isDoubleNeg[N <: Node](n: N): Boolean = n match {
+    case Not(Not(_)) => true
+    case _ => false
+  }
+
+  private def pfRecSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
+    val result: ArrayBuffer[N] = ArrayBuffer()
+    result ++= pfSimplify(n, assumeWelldefinedness)
+    val newChildrenList = n.children.zipWithIndex.map {
+      case (child: AtomicType, index) => {
+        ArrayBuffer()
+      }
+      case (child: N, index) => {
+        val temp = new ArrayBuffer[List[Any]]()
+          temp ++=pfSimplify(child, assumeWelldefinedness).map { pfSimpChild =>
+          n.children.toList.updated(index, pfSimpChild)
+        }
+        temp ++= pfRecSimplify(child, assumeWelldefinedness).toList.map { recSimpChild =>
+          n.children.toList.updated(index, recSimpChild)
+        }
+        temp
+      }
+      case _ => {
+        ArrayBuffer()
+      }
+    }
+
+    val newlist = newChildrenList.map {
+      newChildren => newChildren.map{
+        oneChildren => {
+          n.withChildren(oneChildren) }//withChildren has big performance impact!
+      }
+    }
+    newlist.map (listelem => result ++= listelem)
+    result
+  }
+}
diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
index 55938e24c..351497825 100644
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
@@ -35,15 +35,11 @@ object DeepSimplifier {
     getShortest(visited)
   }
 
-  // only called with nonempty ArrayBuffers TODO: what happens if empty?
-
-
   private def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
     visited.minBy(treeSize)
   }
 
-  // "counts every node twice", ie "LocalVar("a", Bool)()" is counted once as "a" and once as "Bool", at least it's consistent
-
+  // "counts every node twice", ie "LocalVar("a", Bool)()" is counted once as "a" and once as "Bool"
   private def treeSize[N <: Node](n: N): Int = {
     n.reduceTree[Int]((node, count) => (count.sum + 1))
   }
@@ -127,7 +123,6 @@ object DeepSimplifier {
       //{ case root@Or(Not(left), right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Implies(left, right)(root.pos, root.info)},
 
       //extended rules and/or
-      //pos attribute!!
 
       //de morgan
       { case root@Not(Or(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
@@ -188,16 +183,6 @@ object DeepSimplifier {
       { case root@CondExp(condition, ifTrue, TrueLit()) => Implies(condition, ifTrue)(root.pos, root.info) },
 
       //forall&exists
-
-      //extended rules equality comparison
-
-      //accessibility
-
-      //fieldaccess and/extends locationaccess (see Expression.scala)
-      //locationaccess: loc
-      //fieldaccess: field and loc
-      //example: fieldaccess(loc.next) && locationaccess(loc) => locationaccess(loc)
-      //fieldaccess: layers? maybe go from field -> field.parent? or is field guaranteed to be a direct child?
     )
 
     result ++= cases.collect { case lcase if lcase.isDefinedAt(n) => lcase(n) }
diff --git a/src/test/scala/IterativeSimplifierTest.scala b/src/test/scala/IterativeSimplifierTest.scala
new file mode 100644
index 000000000..c96dea4f6
--- /dev/null
+++ b/src/test/scala/IterativeSimplifierTest.scala
@@ -0,0 +1,865 @@
+import org.scalatest.funsuite.AnyFunSuite
+import org.scalatest.matchers.should.Matchers
+import viper.silver.ast._
+import viper.silver.ast.utility.IterativeSimplifier._
+
+import scala.language.implicitConversions
+
+class IterativeSimplifierTest extends AnyFunSuite with Matchers{
+
+  test("Cmp1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(EqCmp(a,b)())()
+
+    simplify(c) should be (NeCmp(a,b)())
+  }
+
+  test("Cmp2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(NeCmp(a,b)())()
+
+    simplify(c) should be (EqCmp(a,b)())
+  }
+
+  test("Cmp3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(GtCmp(a,b)())()
+
+    simplify(c) should be (LeCmp(a,b)())
+  }
+
+  test("Cmp4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(GeCmp(a,b)())()
+
+    simplify(c) should be (LtCmp(a,b)())
+  }
+
+  test("Cmp5") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(LtCmp(a,b)())()
+
+    simplify(c) should be (GeCmp(a,b)())
+  }
+
+  test("Cmp6") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Not(LeCmp(a,b)())()
+
+    simplify(c) should be (GtCmp(a,b)())
+  }
+
+
+  test("notnot1") {
+    val a = LocalVar("a", Bool)()
+
+    simplify(Not(Not(a)())()) should be (a)
+  }
+
+
+  test("or1"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(FalseLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("or2"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(a, FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("or3"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(TrueLit()(), a)()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+  test("or4"){
+    val a = LocalVar("a", Bool)()
+    val expr = Or(a, TrueLit()())()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+
+  test("and1") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(TrueLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("and2") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(a, TrueLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("and3") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(FalseLit()(), a)()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("and4") {
+    val a = LocalVar("a", Bool)()
+    val expr = And(a, FalseLit()())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("idem1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(And(a,b)(),a)()
+
+    simplify(expr, true) should (be (And(a,b)()) or be (And(b,a)()))
+  }
+
+  test("idem2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(b,And(a,b)())()
+
+    simplify(expr, true) should (be (And(a,b)()) or be (And(b,a)()))
+  }
+
+  test("idem3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(Or(a,b)(),a)()
+
+    simplify(expr, true) should (be (Or(a,b)()) or be (Or(b,a)()))
+  }
+
+  test("idem4"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(b,Or(a,b)())()
+
+    simplify(expr, true) should (be (Or(a,b)()) or be (Or(b,a)()))
+  }
+
+  //while these do cannot verify if associativity of or/and is being applied, they should catch some cases where associativity is incorrectly applied
+  test("assoc1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = And(a,And(b,c)())()
+
+    simplify(expr) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
+
+  test("assoc2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = And(And(a, b)(), c)()
+
+    simplify(expr) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
+
+  test("assoc3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = Or(a,Or(b,c)())()
+
+    simplify(expr) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
+  }
+
+  test("assoc4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val expr = Or(Or(a, b)(), c)()
+
+    simplify(expr) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
+  }
+
+  test("and11") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = And(a, And(b,c)())()
+    val expr = And(And(a,b)(), And(a,c)())()
+
+    simplify(expr, true) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
+  }
+
+  test("or11") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = Or(a, Or(b,c)())()
+    val expr = Or(Or(a,b)(), Or(a,c)())()
+
+    simplify(expr, true) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
+  }
+
+  test("impl1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(a, b)()
+
+    simplify(expr) should be (Implies(a, b)())
+  }
+
+  test("impl2") {
+    val a = FalseLit()()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(a, b)()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+  test("impl3") {
+    val a = TrueLit()()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(a, b)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl4") {
+    val a = LocalVar("a", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = Implies(a,c)()
+    val expr = Implies(a, d)()
+
+    simplify(expr, true) should be (Implies(a, c)())
+  }
+
+  test("impl5") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Implies(a,b)()
+    val d = Implies(Not(a)(),b)()
+    val expr = And(c, d)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl6") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Implies(a,b)()
+    val d = Implies(Not(a)(),b)()
+    val expr = And(c, d)()
+
+    simplify(expr, true) should be (b)
+  }
+
+  test("impl7") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Implies(Not(b)(), Not(a)())()
+
+    simplify(expr) should be (Implies(a, b)())
+  }
+
+  test("and21") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(And(a,Not(b)())())()
+
+    simplify(expr) should be (Or(Not(a)(), b)())
+  }
+
+  test("and22") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(Or(a,b)())())
+  }
+
+  test("dem1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(Or(Not(a)(),Not(b)())())()
+
+    simplify(expr) should be (And(a,b)())
+  }
+
+  test("dem2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = And(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(Or(a,b)())())
+  }
+
+  test("dem3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Not(And(Not(a)(),Not(b)())())()
+
+    simplify(expr) should be (Or(a,b)())
+  }
+
+  test("dem4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = Or(Not(a)(),Not(b)())()
+
+    simplify(expr) should be (Not(And(a,b)())())
+  }
+
+
+  test("eq1 assumeWelldefinedness") {
+    val x = LocalVar("x", Bool)()
+    val expr = EqCmp(x, x)()
+
+    simplify(expr, true) should be (TrueLit()())
+  }
+
+  test("eq2") {
+    val expr = EqCmp(BoolLit(true)(), BoolLit(true)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq2bis") {
+    val expr = EqCmp(BoolLit(true)(), BoolLit(false)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq3") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(FalseLit()(), a)()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq4") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(a, FalseLit()())()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq5") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(TrueLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq6") {
+    val a = LocalVar("a", Bool)()
+    val expr = EqCmp(a, TrueLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq7") {
+    val expr = EqCmp(IntLit(32)(), IntLit(32)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq7bis") {
+    val expr = EqCmp(IntLit(32)(), IntLit(31)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq8") {
+    val expr = EqCmp(NullLit()(), NullLit()())()
+
+    simplify(expr) should be (TrueLit()(expr.pos, expr.info))
+  }
+
+
+
+  test("eq10") {
+    val expr = NeCmp(BoolLit(true)(), BoolLit(true)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+
+  test("eq10bis") {
+    val expr = NeCmp(BoolLit(true)(), BoolLit(false)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq11") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(FalseLit()(), a)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq12") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(a, FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("eq13") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(TrueLit()(), a)()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq14") {
+    val a = LocalVar("a", Bool)()
+    val expr = NeCmp(a, TrueLit()())()
+
+    simplify(expr) should be (Not(a)())
+  }
+
+  test("eq15") {
+    val expr = NeCmp(IntLit(32)(), IntLit(32)())()
+
+    simplify(expr) should be (BoolLit(false)())
+  }
+  test("eq15bis") {
+    val expr = NeCmp(IntLit(32)(), IntLit(31)())()
+
+    simplify(expr) should be (BoolLit(true)())
+  }
+
+  test("eq16") {
+    val expr = NeCmp(NullLit()(), NullLit()())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+
+  test("eq17 assumeWelldefinedness") {
+    val x = LocalVar("x", Bool)()
+    val expr = NeCmp(x, x)()
+
+    simplify(expr, true) should be (FalseLit()())
+  }
+  test("eq17bis assumeWelldefinedness") {
+    val expr = NeCmp(IntLit(5)(), IntLit(5)())()
+
+    simplify(expr) should be (FalseLit()())
+  }
+  test("eq17ter assumeWelldefinedness") {
+    val expr = NeCmp(IntLit(5)(), IntLit(6)())()
+
+    simplify(expr) should be (TrueLit()())
+  }
+
+
+  test("eq20 assumeWelldefinedness") {
+    val a = LocalVar("a", Int)()
+    val b = LocalVar("b", Int)()
+
+    val expr = And(
+      EqCmp(a, b)(),
+      NeCmp(a, b)()
+    )()
+
+    simplify(expr, true) should be (FalseLit()())
+  }
+
+
+  test("eq21 assumeWelldefinedness") {
+    val a = LocalVar("a", Int)()
+    val b = LocalVar("b", Int)()
+
+    val expr = Or(
+      EqCmp(a, b)(),
+      NeCmp(a, b)()
+    )()
+
+    simplify(expr, true) should be (TrueLit()())
+  }
+
+  test("ce1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val ifFalse = BoolLit(false)()
+    val expr = CondExp(TrueLit()(), a, b)()
+
+    simplify(expr) should be (a)
+  }
+
+  test("ce2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val ifFalse = BoolLit(false)()
+    val expr = CondExp(FalseLit()(), a, b)()
+
+    simplify(expr) should be (b)
+  }
+
+  test("ce3 assumeWelldefinedness") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(b, a, a)()
+
+    simplify(expr, true) should be (a)
+  }
+
+  test("ce4") {
+    val a = LocalVar("a", Bool)()
+    val expr = CondExp(a, FalseLit()(), TrueLit()())()
+
+    simplify(expr) should be (Not(a)(expr.pos, expr.info))
+  }
+
+  test("ce5") {
+    val a = LocalVar("a", Bool)()
+    val expr = CondExp(a, TrueLit()(), FalseLit()())()
+
+    simplify(expr) should be (a)
+  }
+
+  test("ce6") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, FalseLit()(), Not(a)())()
+
+    simplify(expr) should be (Not(Or(a,a)())())
+  }
+  test("ce6bis assumeWelldefinedeness") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, FalseLit()(), Not(a)())()
+
+    simplify(expr, true) should be (Not(a)())
+  }
+
+  test("ce7") {
+    val a = LocalVar("a", Bool)()
+    val z = BoolLit(false)() //z must be pure/z.isPure == true
+    val expr = CondExp(a, TrueLit()(), z)()
+
+    simplify(expr) should be (a) //(a || false) = a
+  }
+
+  test("ce8") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, b, FalseLit()())()
+
+    simplify(expr) should be (And(a, b)())
+  }
+
+  test("ce9") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val expr = CondExp(a, b, TrueLit()())()
+
+    simplify(expr) should be (Implies(a, b)())
+  }
+
+
+
+
+
+
+
+
+
+
+
+  test("and5 assumeWelldefinedness"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+    val d = And(a, And(b,c)())()
+    val e = And(And(a,b)(), And(a,c)())()
+
+    simplify(e, true) should (be (And(And(a,b)(),c)()) or be (And(And(a,b)(),c)()))
+  }
+
+  test("implies1"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
+
+    simplify(d, true) should be (b)
+  }
+  test("not3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
+
+    simplify(d, true) should be (b)
+  }
+  test("implies2"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val d = Implies(a, b)()
+
+    simplify(d) should be (d)
+  }
+  test("implies3"){
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val z = NullLit()()
+    val y = NullLit()()
+    val c = LocalVar("c", Bool)()
+    val aa = EqCmp(a, z)()
+    val bb = EqCmp(b, y)()
+    val d = And(Implies(aa, c)(), Implies(Not(aa)(), c)())()
+
+    simplify(d, true) should be(c)
+  }
+
+  test("test1") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Or(Or(Not(a)(), Not(b)())(), FalseLit()())()
+    simplify(c) should (be (Not(And(a,b)())()) or be (Not(And(b,a)())()))
+  }
+
+  test("test14") {
+    val a = LocalVar("a", Bool)()
+    val z = LocalVar("z", Bool)()
+    val d = Or(Not(Not(a)())(), Not(Not(Not(Not(z)())())())())()
+    val f = Or(d, Not(Not(Not(Not(FalseLit()())())())())())()
+
+    simplify(f) should (be (Or(a,z)()) or be (Or(z,a)()))
+  }
+
+  test("eqcmp1") {
+    val a = LocalVar("a", Bool)()
+    val d = EqCmp(a, a)()
+    simplify(d, true) should be(TrueLit()(d.pos, d.info))
+  }
+
+  test("eqcmp2") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = NeCmp(a, b)()
+    val d = EqCmp(a, b)()
+    val e = And(c, d)()
+    val f = Or(c, d)()
+
+    simplify(e, true) should be(FalseLit()(e.pos, e.info))
+    simplify(f, true) should be(TrueLit()(f.pos, f.info))
+  }
+
+  test("eqcmp3") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = NeCmp(a, b)()
+    val d = EqCmp(a, b)()
+    val e = And(c, d)()
+    val f = Or(c, d)()
+
+    simplify(e, true) should be(FalseLit()(e.pos, e.info))
+    simplify(f, true) should be(TrueLit()(f.pos, f.info))
+  }
+
+  test("neue") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+
+    simplify (And(Implies(a, b)(), Implies(a, c)())()) should be (Implies(a, And(b, c)())())
+
+    simplify (And(Implies(a, b)(), Implies(Not(a)(), b)())()) should be (And(Implies(a,b)(),Implies(Not(a)(), b)())())
+    simplify (And(Implies(a, b)(), Implies(Not(a)(), b)())(), true) should be (b)
+
+    simplify (And(a, Implies(a, b)())()) should be (And(a, b)())
+  }
+
+
+
+
+
+
+  /*test("test1") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+
+    simplify(Implies(a, b)()) should be(Implies(a, b)())
+
+    println(Implies(a, b)())
+    println(simplify(Implies(a, b)()))
+  }
+
+  test("test2") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+
+    simplify(Or(a, b)()) should be(Implies(a, b)())
+
+    println(Or(a, b)())
+    println(simplify(Implies(a, b)()))
+  }
+
+  test("test3") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+    val c = Or(a, b)()
+
+    val d = LocalVar("a", Bool)()
+    val e = LocalVar("b", Bool)()
+
+    val f = Or(d, e)()
+
+
+    c should be(f)
+
+    println(c)
+    println(f)
+  }
+
+  /*test("test4") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+
+    val c = Or(a, b)()
+
+    contains(c) should be(true)
+  }*/
+
+  test("test4") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(a)())()
+
+    println(b)
+    //println(genSimp(b))
+
+    true should be(true)
+  }
+
+  test("test5") {
+    val a = LocalVar("a", Bool)()
+    val b = And(a, a)()
+
+    println(b)
+    println(a.getClass)
+
+    true should be(true)
+  }
+
+  test("test6") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(a)())()
+    val c = Not(Not(b)())()
+    val tru = TrueLit()()
+    val d = Or(c, tru)()
+
+    println(d)
+    println(simplify(d))
+
+    true should be(true)
+  }
+
+  test("test7") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(Not(a)())())()
+
+    println(b)
+    println(recursiveSimplify(b))
+
+    true should be(true)
+  }
+
+  test("test8") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = And(a, Not(a)())()
+    val d = And(b, c)()
+
+
+    println(d)
+    println(d.size)
+
+    true should be(true)
+  }
+
+  test("test9") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(a)())()
+    val c = And(a, Not(a)())()
+    val d = And(b, c)()
+
+
+    println(d)
+    println(recursiveSimplify(d))
+
+    true should be(true)
+  }
+
+  test("test10") {
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = Or(a, Not(a)())()
+    val d = Or(b, c)()
+
+
+    println(d)
+    println()
+    println(pfSimplify(d))
+
+    true should be(true)
+  }
+
+  test("test11") {
+    val a = LocalVar("a", Bool)()
+    val b = Not(Not(a)())()
+
+    println(b)
+    println(pfSimplify(b))
+
+    true should be(true)
+  }
+
+  test("test12") {
+    val a = LocalVar("a", Bool)()
+    val tru = TrueLit()()
+    val othertru = TrueLit()()
+    val b = Not(Not(a)())()
+    val c = Or(othertru, tru)()
+
+    println(c)
+    println(treeSize(a))
+    println(treeSize(tru))
+    println(treeSize(c))
+    println(pfSimplify(c))
+
+    true should be(true)
+  }
+
+  test("test13") {
+    val a = LocalVar("a", Bool)()
+    val b = Or(Not(Not(a)())(), a)()
+    val c = Or(Not(a)(), a)()
+
+    val buf = ArrayBuffer[Node](a, b, c)
+
+    println(getShortest(buf))
+
+    true should be(true)
+  }
+
+   */
+
+
+
+
+}

From b5ea0336636c9e350056c62a473346c30d54057b Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Sun, 15 Dec 2024 22:10:08 +0100
Subject: [PATCH 07/10] small changes

---
 .../ast/utility/IterativeSimplifier.scala     | 24 +++++--------------
 1 file changed, 6 insertions(+), 18 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala b/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
index 24d6bff20..f30c95275 100644
--- a/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
@@ -7,6 +7,12 @@ import scala.collection.mutable._
 
 object IterativeSimplifier {
 
+  /**
+   * Simplify 'n' by matching nodes in the AST with a list of transformations
+   * while storing every version of n generated and applying simplify to the stored
+   * versions until no new versions are generated or the number of versions is greater than
+   * iterationLimit
+   */
   def simplify[N <: Node](n: N, assumeWelldefinedness: Boolean = false, iterationLimit: Integer = 5000, printToConsole: Boolean = false): N = {
 
     val visited: ArrayBuffer[N] = ArrayBuffer(n)
@@ -61,17 +67,6 @@ object IterativeSimplifier {
       { case root@Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info) },
       { case root@Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info) },
 
-
-      //TODO: try to find case where these could be used, then figure out a better way to implement them
-      /*
-      { case root@NeCmp(left, right) => Not(EqCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@EqCmp(left, right) => Not(NeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@GtCmp(left, right) => Not(LeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@GeCmp(left, right) => Not(LtCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@LtCmp(left, right) => Not(GeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@LeCmp(left, right) => Not(GtCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      */
-
       { case Not(Not(single)) => single },
 
       { case Or(FalseLit(), right) => right },
@@ -113,15 +108,8 @@ object IterativeSimplifier {
       { case root@And(a, Implies(a2, b)) if a == a2 => And(a, b)(root.pos, root.info) },
 
       //contrapositive
-      //{ case root@Implies(left, right) if !(isDoubleNeg(left) || isDoubleNeg(right)) => Implies(Not(right)(), Not(left)())(root.pos, root.info) },
       { case root@Implies(Not(left), Not(right)) => Implies(right, left)(root.pos, root.info) },
 
-      //modus ponens & modus tollens
-
-      //implies to or
-      //{ case root@Implies(left, right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Or(Not(left)(), right)(root.pos, root.info)},
-      //{ case root@Or(Not(left), right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Implies(left, right)(root.pos, root.info)},
-
       //extended rules and/or
 
       //de morgan

From 0cd259fc5be4a71f19eda0273598d48c56d9316f Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Sun, 15 Dec 2024 22:11:27 +0100
Subject: [PATCH 08/10] small changes

---
 .../deepsimplifier/DeepSimplifier.scala       | 234 -----
 .../deepsimplifier/DeepSimplifierTest.scala   | 867 ------------------
 2 files changed, 1101 deletions(-)
 delete mode 100644 src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
 delete mode 100644 src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala

diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
deleted file mode 100644
index 351497825..000000000
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifier.scala
+++ /dev/null
@@ -1,234 +0,0 @@
-package viper.silver.ast.utility.deepsimplifier
-
-import viper.silver.ast._
-
-import scala.collection.mutable
-import scala.collection.mutable._
-
-object DeepSimplifier {
-
-  def simplify[N <: Node](n: N, assumeWelldefinedness: Boolean = false, iterationLimit: Integer = 5000, printToConsole: Boolean = false): N = {
-
-    val visited: ArrayBuffer[N] = ArrayBuffer(n)
-    val queue: mutable.Queue[N] = mutable.Queue(n)
-
-    while (queue.nonEmpty && visited.length < iterationLimit) {
-      val currnode: N = queue.dequeue()
-      if(printToConsole) {
-        println("currnode: " + currnode)
-      }
-
-      val generated: ArrayBuffer[N] = pfRecSimplify(currnode, assumeWelldefinedness)
-      if(printToConsole) {
-        println("generated: " + generated)
-      }
-      for (g <- generated if !visited.contains(g)) {
-        visited.append(g)
-        queue.enqueue(g)
-      }
-    }
-
-    if(printToConsole){
-      println("result simplify: " + visited)
-    }
-
-    getShortest(visited)
-  }
-
-  private def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
-    visited.minBy(treeSize)
-  }
-
-  // "counts every node twice", ie "LocalVar("a", Bool)()" is counted once as "a" and once as "Bool"
-  private def treeSize[N <: Node](n: N): Int = {
-    n.reduceTree[Int]((node, count) => (count.sum + 1))
-  }
-  private def treeHasDoubleNeg[N <: Node](n: N): Boolean = {
-    n.reduceTree[Boolean]((node, doubleNegs) => doubleNegs.contains(true) || isDoubleNeg(node))
-  }
-
-  private def pfSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
-
-    val result: ArrayBuffer[Node] = ArrayBuffer()
-
-    val cases: List[PartialFunction[N, Node]] = List(
-      { case root@Not(BoolLit(literal)) => BoolLit(!literal)(root.pos, root.info) },
-
-      { case root@Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info) },
-      { case root@Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info) },
-      { case root@Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info) },
-      { case root@Not(GeCmp(a, b)) => LtCmp(a, b)(root.pos, root.info) },
-      { case root@Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info) },
-      { case root@Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info) },
-
-
-      //TODO: try to find case where these could be used, then figure out a better way to implement them
-      /*
-      { case root@NeCmp(left, right) => Not(EqCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@EqCmp(left, right) => Not(NeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@GtCmp(left, right) => Not(LeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@GeCmp(left, right) => Not(LtCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@LtCmp(left, right) => Not(GeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@LeCmp(left, right) => Not(GtCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      */
-
-      { case Not(Not(single)) => single },
-
-      { case Or(FalseLit(), right) => right },
-      { case Or(left, FalseLit()) => left },
-      { case root@Or(TrueLit(), _) => TrueLit()(root.pos, root.info) },
-      { case root@Or(_, TrueLit()) => TrueLit()(root.pos, root.info) },
-
-      { case And(TrueLit(), right) => right },
-      { case And(left, TrueLit()) => left },
-      { case root@And(FalseLit(), _) => FalseLit()(root.pos, root.info) },
-      { case root@And(_, FalseLit()) => FalseLit()(root.pos, root.info) },
-
-      //Idempotence
-      { case root@And(a, b) if assumeWelldefinedness && a == b => a},
-      { case root@Or(a, b) if assumeWelldefinedness && a == b => a},
-
-      { case root@And(a, b) => And(b, a)(root.pos, root.info)},
-      { case root@Or(a, b) => Or(b, a)(root.pos, root.info)},
-
-
-      //associativity
-      //WARNING: position and info attribute not correctly maintained for lchild, left and right
-      { case root@And(lchild@And(left, right), rchild) => And(left, And(right, rchild)())(root.pos, root.info)},
-      { case root@And(lchild, rchild@And(left, right)) => And(And(lchild, left)(), right)(root.pos, root.info)},
-
-      { case root@Or(lchild@Or(left, right), uright) => Or(left, Or(right, uright)())(root.pos, root.info)},
-      { case root@Or(uleft, rchild@Or(left, right)) => Or(Or(uleft, left)(), right)(root.pos, root.info)},
-
-      //implication rules
-      //WARNING: position and info attributes not correctly maintained
-      { case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info) },
-      { case Implies(TrueLit(), consequent) => consequent },
-      { case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(), r)(root.pos, root.info) },
-
-      { case And(Implies(l1, r1), Implies(Not(l2), r2)) if assumeWelldefinedness && (l1 == l2 && r1 == r2) => r1 },
-
-      { case root@And(Implies(a, b), Implies(a2, c)) if a == a2 => Implies(a, And(b, c)())(root.pos, root.info) },
-      { case And(Implies(a, b), Implies(Not(a2), b2)) if assumeWelldefinedness && a == a2 && b == b2 => b },
-      { case root@And(a, Implies(a2, b)) if a == a2 => And(a, b)(root.pos, root.info) },
-
-      //contrapositive
-      //{ case root@Implies(left, right) if !(isDoubleNeg(left) || isDoubleNeg(right)) => Implies(Not(right)(), Not(left)())(root.pos, root.info) },
-      { case root@Implies(Not(left), Not(right)) => Implies(right, left)(root.pos, root.info) },
-
-      //modus ponens & modus tollens
-
-      //implies to or
-      //{ case root@Implies(left, right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Or(Not(left)(), right)(root.pos, root.info)},
-      //{ case root@Or(Not(left), right) if !(isDoubleNeg(left) || isDoubleNeg(left)) => Implies(left, right)(root.pos, root.info)},
-
-      //extended rules and/or
-
-      //de morgan
-      { case root@Not(Or(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
-      { case root@And(Not(left), Not(right)) => Not(Or(left, right)())(root.pos, root.info)},
-
-      { case root@Not(And(left, right)) => Or(Not(left)(), Not(right)())(root.pos, root.info)},
-      { case root@Or(Not(left), Not(right)) => Not(And(left, right)())(root.pos, root.info)},
-
-      //equality comparison
-
-      { case root@EqCmp(left, right) if assumeWelldefinedness && left == right => TrueLit()(root.pos, root.info) },
-      { case root@EqCmp(BoolLit(left), BoolLit(right)) => BoolLit(left == right)(root.pos, root.info) },
-      { case root@EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info) },
-      { case root@EqCmp(left, FalseLit()) => Not(left)(root.pos, root.info) },
-      { case EqCmp(TrueLit(), right) => right },
-      { case EqCmp(left, TrueLit()) => left },
-      { case root@EqCmp(IntLit(left), IntLit(right)) => BoolLit(left == right)(root.pos, root.info) },
-      { case root@EqCmp(NullLit(), NullLit()) => TrueLit()(root.pos, root.info) },
-
-      //nonequality comparison
-
-      { case root@NeCmp(BoolLit(left), BoolLit(right)) => BoolLit(left != right)(root.pos, root.info) },
-      { case NeCmp(FalseLit(), right) => right },
-      { case NeCmp(left, FalseLit()) => left },
-      { case root@NeCmp(TrueLit(), right) => Not(right)(root.pos, root.info) },
-      { case root@NeCmp(left, TrueLit()) => Not(left)(root.pos, root.info) },
-      { case root@NeCmp(IntLit(left), IntLit(right)) => BoolLit(left != right)(root.pos, root.info) },
-      { case root@NeCmp(NullLit(), NullLit()) => FalseLit()(root.pos, root.info) },
-      { case root@NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info) },
-
-      //extended equality/nonequality comparison
-      //some possible rules could introduce more statements, but not these ones
-      { case root@EqCmp(left, right) => EqCmp(right, left)(root.pos, root.info) },
-      { case root@NeCmp(left, right) => NeCmp(right, left)(root.pos, root.info) },
-      //{ case root@EqCmp(left, right) => Not(NeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      //{ case root@NeCmp(left, right) => Not(EqCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      { case root@Not(EqCmp(left, right)) => NeCmp(left, right)(root.pos, root.info) },
-      { case root@Not(NeCmp(left, right)) => EqCmp(left, right)(root.pos, root.info) },
-      { case root@And(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => FalseLit()(root.pos, root.info)},
-      { case root@Or(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => TrueLit()(root.pos, root.info)},
-
-      //conditional expressions
-
-      { case CondExp(TrueLit(), ifTrue, _) => ifTrue },
-      { case CondExp(FalseLit(), _, ifFalse) => ifFalse },
-      { case CondExp(_, ifTrue, ifFalse) if assumeWelldefinedness && ifTrue == ifFalse => ifTrue },
-      { case root@CondExp(condition, FalseLit(), TrueLit()) => Not(condition)(root.pos, root.info) },
-      { case CondExp(condition, TrueLit(), FalseLit()) => condition },
-      { case root@CondExp(condition, FalseLit(), ifFalse) => And(Not(condition)(), ifFalse)(root.pos, root.info) },
-      { case root@CondExp(condition, TrueLit(), ifFalse) =>
-        if (ifFalse.isPure) {
-          Or(condition, ifFalse)(root.pos, root.info)
-        } else {
-          Implies(Not(condition)(), ifFalse)(root.pos, root.info)
-        }
-      },
-      { case root@CondExp(condition, ifTrue, FalseLit()) => And(condition, ifTrue)(root.pos, root.info) },
-      { case root@CondExp(condition, ifTrue, TrueLit()) => Implies(condition, ifTrue)(root.pos, root.info) },
-
-      //forall&exists
-    )
-
-    result ++= cases.collect { case lcase if lcase.isDefinedAt(n) => lcase(n) }
-
-    result.asInstanceOf[ArrayBuffer[N]]
-  }
-
-  private def isSingleNeg[N <: Node](n: N): Boolean = n match {
-    case Not(_) => true
-    case _ => false
-  }
-
-  private def isDoubleNeg[N <: Node](n: N): Boolean = n match {
-    case Not(Not(_)) => true
-    case _ => false
-  }
-
-  private def pfRecSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
-    val result: ArrayBuffer[N] = ArrayBuffer()
-    result ++= pfSimplify(n, assumeWelldefinedness)
-    val newChildrenList = n.children.zipWithIndex.map {
-      case (child: AtomicType, index) => {
-        ArrayBuffer()
-      }
-      case (child: N, index) => {
-        val temp = new ArrayBuffer[List[Any]]()
-          temp ++=pfSimplify(child, assumeWelldefinedness).map { pfSimpChild =>
-          n.children.toList.updated(index, pfSimpChild)
-        }
-        temp ++= pfRecSimplify(child, assumeWelldefinedness).toList.map { recSimpChild =>
-          n.children.toList.updated(index, recSimpChild)
-        }
-        temp
-      }
-      case _ => {
-        ArrayBuffer()
-      }
-    }
-
-    val newlist = newChildrenList.map {
-      newChildren => newChildren.map{
-        oneChildren => {
-          n.withChildren(oneChildren) }//withChildren has big performance impact!
-      }
-    }
-    newlist.map (listelem => result ++= listelem)
-    result
-  }
-}
diff --git a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala b/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
deleted file mode 100644
index 461503e11..000000000
--- a/src/main/scala/viper/silver/ast/utility/deepsimplifier/DeepSimplifierTest.scala
+++ /dev/null
@@ -1,867 +0,0 @@
-package viper.silver.ast.utility.deepsimplifier
-
-import org.scalatest.funsuite.AnyFunSuite
-
-import scala.language.implicitConversions
-import org.scalatest.matchers.should.Matchers
-import viper.silver.ast.{Node, _}
-import viper.silver.ast.utility.deepsimplifier.DeepSimplifier._
-
-class DeepSimplifierTest extends AnyFunSuite with Matchers{
-
-  test("Cmp1") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Not(EqCmp(a,b)())()
-
-    simplify(c) should be (NeCmp(a,b)())
-  }
-
-  test("Cmp2") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Not(NeCmp(a,b)())()
-
-    simplify(c) should be (EqCmp(a,b)())
-  }
-
-  test("Cmp3") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Not(GtCmp(a,b)())()
-
-    simplify(c) should be (LeCmp(a,b)())
-  }
-
-  test("Cmp4") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Not(GeCmp(a,b)())()
-
-    simplify(c) should be (LtCmp(a,b)())
-  }
-
-  test("Cmp5") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Not(LtCmp(a,b)())()
-
-    simplify(c) should be (GeCmp(a,b)())
-  }
-
-  test("Cmp6") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Not(LeCmp(a,b)())()
-
-    simplify(c) should be (GtCmp(a,b)())
-  }
-
-
-  test("notnot1") {
-    val a = LocalVar("a", Bool)()
-
-    simplify(Not(Not(a)())()) should be (a)
-  }
-
-
-  test("or1"){
-    val a = LocalVar("a", Bool)()
-    val expr = Or(FalseLit()(), a)()
-
-    simplify(expr) should be (a)
-  }
-
-  test("or2"){
-    val a = LocalVar("a", Bool)()
-    val expr = Or(a, FalseLit()())()
-
-    simplify(expr) should be (a)
-  }
-
-  test("or3"){
-    val a = LocalVar("a", Bool)()
-    val expr = Or(TrueLit()(), a)()
-
-    simplify(expr) should be (TrueLit()())
-  }
-
-  test("or4"){
-    val a = LocalVar("a", Bool)()
-    val expr = Or(a, TrueLit()())()
-
-    simplify(expr) should be (TrueLit()())
-  }
-
-
-  test("and1") {
-    val a = LocalVar("a", Bool)()
-    val expr = And(TrueLit()(), a)()
-
-    simplify(expr) should be (a)
-  }
-
-  test("and2") {
-    val a = LocalVar("a", Bool)()
-    val expr = And(a, TrueLit()())()
-
-    simplify(expr) should be (a)
-  }
-
-  test("and3") {
-    val a = LocalVar("a", Bool)()
-    val expr = And(FalseLit()(), a)()
-
-    simplify(expr) should be (FalseLit()())
-  }
-
-  test("and4") {
-    val a = LocalVar("a", Bool)()
-    val expr = And(a, FalseLit()())()
-
-    simplify(expr) should be (FalseLit()())
-  }
-
-  test("idem1") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = And(And(a,b)(),a)()
-
-    simplify(expr, true) should (be (And(a,b)()) or be (And(b,a)()))
-  }
-
-  test("idem2") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = And(b,And(a,b)())()
-
-    simplify(expr, true) should (be (And(a,b)()) or be (And(b,a)()))
-  }
-
-  test("idem3"){
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = Or(Or(a,b)(),a)()
-
-    simplify(expr, true) should (be (Or(a,b)()) or be (Or(b,a)()))
-  }
-
-  test("idem4"){
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = Or(b,Or(a,b)())()
-
-    simplify(expr, true) should (be (Or(a,b)()) or be (Or(b,a)()))
-  }
-
-  //while these do cannot verify if associativity of or/and is being applied, they should catch some cases where associativity is incorrectly applied
-  test("assoc1") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = LocalVar("c", Bool)()
-    val expr = And(a,And(b,c)())()
-
-    simplify(expr) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
-  }
-
-  test("assoc2") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = LocalVar("c", Bool)()
-    val expr = And(And(a, b)(), c)()
-
-    simplify(expr) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
-  }
-
-  test("assoc3") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = LocalVar("c", Bool)()
-    val expr = Or(a,Or(b,c)())()
-
-    simplify(expr) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
-  }
-
-  test("assoc4") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = LocalVar("c", Bool)()
-    val expr = Or(Or(a, b)(), c)()
-
-    simplify(expr) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
-  }
-
-  test("and11") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = LocalVar("c", Bool)()
-    val d = And(a, And(b,c)())()
-    val expr = And(And(a,b)(), And(a,c)())()
-
-    simplify(expr, true) should (be (And(a,And(b,c)())()) or be (And(a, And(c,b)())()) or be (And(b, And(c,a)())()) or be (And(b, And(a,c)())()) or be (And(c, And(a,b)())()) or be (And(c, And(b,a)())()) or be (And(And(b,c)(), a)()) or be (And(And(c,b)(), a)()) or be (And(And(c,a)(), b)()) or be (And(And(a,c)(), b)()) or be (And(And(a,b)(), c)()) or be (And(And(b,a)(), c)()) )
-  }
-
-  test("or11") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = LocalVar("c", Bool)()
-    val d = Or(a, Or(b,c)())()
-    val expr = Or(Or(a,b)(), Or(a,c)())()
-
-    simplify(expr, true) should (be (Or(a,Or(b,c)())()) or be (Or(a, Or(c,b)())()) or be (Or(b, Or(c,a)())()) or be (Or(b, Or(a,c)())()) or be (Or(c, Or(a,b)())()) or be (Or(c, Or(b,a)())()) or be (Or(Or(b,c)(), a)()) or be (Or(Or(c,b)(), a)()) or be (Or(Or(c,a)(), b)()) or be (Or(Or(a,c)(), b)()) or be (Or(Or(a,b)(), c)()) or be (Or(Or(b,a)(), c)()) )
-  }
-
-  test("impl1") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = Implies(a, b)()
-
-    simplify(expr) should be (Implies(a, b)())
-  }
-
-  test("impl2") {
-    val a = FalseLit()()
-    val b = LocalVar("b", Bool)()
-    val expr = Implies(a, b)()
-
-    simplify(expr) should be (TrueLit()())
-  }
-
-  test("impl3") {
-    val a = TrueLit()()
-    val b = LocalVar("b", Bool)()
-    val expr = Implies(a, b)()
-
-    simplify(expr, true) should be (b)
-  }
-
-  test("impl4") {
-    val a = LocalVar("a", Bool)()
-    val c = LocalVar("c", Bool)()
-    val d = Implies(a,c)()
-    val expr = Implies(a, d)()
-
-    simplify(expr, true) should be (Implies(a, c)())
-  }
-
-  test("impl5") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Implies(a,b)()
-    val d = Implies(Not(a)(),b)()
-    val expr = And(c, d)()
-
-    simplify(expr, true) should be (b)
-  }
-
-  test("impl6") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Implies(a,b)()
-    val d = Implies(Not(a)(),b)()
-    val expr = And(c, d)()
-
-    simplify(expr, true) should be (b)
-  }
-
-  test("impl7") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = Implies(Not(b)(), Not(a)())()
-
-    simplify(expr) should be (Implies(a, b)())
-  }
-
-  test("and21") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = Not(And(a,Not(b)())())()
-
-    simplify(expr) should be (Or(Not(a)(), b)())
-  }
-
-  test("and22") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = And(Not(a)(),Not(b)())()
-
-    simplify(expr) should be (Not(Or(a,b)())())
-  }
-
-  test("dem1") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = Not(Or(Not(a)(),Not(b)())())()
-
-    simplify(expr) should be (And(a,b)())
-  }
-
-  test("dem2") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = And(Not(a)(),Not(b)())()
-
-    simplify(expr) should be (Not(Or(a,b)())())
-  }
-
-  test("dem3") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = Not(And(Not(a)(),Not(b)())())()
-
-    simplify(expr) should be (Or(a,b)())
-  }
-
-  test("dem4") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = Or(Not(a)(),Not(b)())()
-
-    simplify(expr) should be (Not(And(a,b)())())
-  }
-
-
-  test("eq1 assumeWelldefinedness") {
-    val x = LocalVar("x", Bool)()
-    val expr = EqCmp(x, x)()
-
-    simplify(expr, true) should be (TrueLit()())
-  }
-
-  test("eq2") {
-    val expr = EqCmp(BoolLit(true)(), BoolLit(true)())()
-
-    simplify(expr) should be (BoolLit(true)())
-  }
-
-  test("eq2bis") {
-    val expr = EqCmp(BoolLit(true)(), BoolLit(false)())()
-
-    simplify(expr) should be (BoolLit(false)())
-  }
-
-  test("eq3") {
-    val a = LocalVar("a", Bool)()
-    val expr = EqCmp(FalseLit()(), a)()
-
-    simplify(expr) should be (Not(a)())
-  }
-
-  test("eq4") {
-    val a = LocalVar("a", Bool)()
-    val expr = EqCmp(a, FalseLit()())()
-
-    simplify(expr) should be (Not(a)())
-  }
-
-  test("eq5") {
-    val a = LocalVar("a", Bool)()
-    val expr = EqCmp(TrueLit()(), a)()
-
-    simplify(expr) should be (a)
-  }
-
-  test("eq6") {
-    val a = LocalVar("a", Bool)()
-    val expr = EqCmp(a, TrueLit()())()
-
-    simplify(expr) should be (a)
-  }
-
-  test("eq7") {
-    val expr = EqCmp(IntLit(32)(), IntLit(32)())()
-
-    simplify(expr) should be (BoolLit(true)())
-  }
-
-  test("eq7bis") {
-    val expr = EqCmp(IntLit(32)(), IntLit(31)())()
-
-    simplify(expr) should be (BoolLit(false)())
-  }
-
-  test("eq8") {
-    val expr = EqCmp(NullLit()(), NullLit()())()
-
-    simplify(expr) should be (TrueLit()(expr.pos, expr.info))
-  }
-
-
-
-  test("eq10") {
-    val expr = NeCmp(BoolLit(true)(), BoolLit(true)())()
-
-    simplify(expr) should be (BoolLit(false)())
-  }
-
-  test("eq10bis") {
-    val expr = NeCmp(BoolLit(true)(), BoolLit(false)())()
-
-    simplify(expr) should be (BoolLit(true)())
-  }
-
-  test("eq11") {
-    val a = LocalVar("a", Bool)()
-    val expr = NeCmp(FalseLit()(), a)()
-
-    simplify(expr) should be (a)
-  }
-
-  test("eq12") {
-    val a = LocalVar("a", Bool)()
-    val expr = NeCmp(a, FalseLit()())()
-
-    simplify(expr) should be (a)
-  }
-
-  test("eq13") {
-    val a = LocalVar("a", Bool)()
-    val expr = NeCmp(TrueLit()(), a)()
-
-    simplify(expr) should be (Not(a)())
-  }
-
-  test("eq14") {
-    val a = LocalVar("a", Bool)()
-    val expr = NeCmp(a, TrueLit()())()
-
-    simplify(expr) should be (Not(a)())
-  }
-
-  test("eq15") {
-    val expr = NeCmp(IntLit(32)(), IntLit(32)())()
-
-    simplify(expr) should be (BoolLit(false)())
-  }
-  test("eq15bis") {
-    val expr = NeCmp(IntLit(32)(), IntLit(31)())()
-
-    simplify(expr) should be (BoolLit(true)())
-  }
-
-  test("eq16") {
-    val expr = NeCmp(NullLit()(), NullLit()())()
-
-    simplify(expr) should be (FalseLit()())
-  }
-
-  test("eq17 assumeWelldefinedness") {
-    val x = LocalVar("x", Bool)()
-    val expr = NeCmp(x, x)()
-
-    simplify(expr, true) should be (FalseLit()())
-  }
-  test("eq17bis assumeWelldefinedness") {
-    val expr = NeCmp(IntLit(5)(), IntLit(5)())()
-
-    simplify(expr) should be (FalseLit()())
-  }
-  test("eq17ter assumeWelldefinedness") {
-    val expr = NeCmp(IntLit(5)(), IntLit(6)())()
-
-    simplify(expr) should be (TrueLit()())
-  }
-
-
-  test("eq20 assumeWelldefinedness") {
-    val a = LocalVar("a", Int)()
-    val b = LocalVar("b", Int)()
-
-    val expr = And(
-      EqCmp(a, b)(),
-      NeCmp(a, b)()
-    )()
-
-    simplify(expr, true) should be (FalseLit()())
-  }
-
-
-  test("eq21 assumeWelldefinedness") {
-    val a = LocalVar("a", Int)()
-    val b = LocalVar("b", Int)()
-
-    val expr = Or(
-      EqCmp(a, b)(),
-      NeCmp(a, b)()
-    )()
-
-    simplify(expr, true) should be (TrueLit()())
-  }
-
-  test("ce1") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val ifFalse = BoolLit(false)()
-    val expr = CondExp(TrueLit()(), a, b)()
-
-    simplify(expr) should be (a)
-  }
-
-  test("ce2") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val ifFalse = BoolLit(false)()
-    val expr = CondExp(FalseLit()(), a, b)()
-
-    simplify(expr) should be (b)
-  }
-
-  test("ce3 assumeWelldefinedness") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = CondExp(b, a, a)()
-
-    simplify(expr, true) should be (a)
-  }
-
-  test("ce4") {
-    val a = LocalVar("a", Bool)()
-    val expr = CondExp(a, FalseLit()(), TrueLit()())()
-
-    simplify(expr) should be (Not(a)(expr.pos, expr.info))
-  }
-
-  test("ce5") {
-    val a = LocalVar("a", Bool)()
-    val expr = CondExp(a, TrueLit()(), FalseLit()())()
-
-    simplify(expr) should be (a)
-  }
-
-  test("ce6") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = CondExp(a, FalseLit()(), Not(a)())()
-
-    simplify(expr) should be (Not(Or(a,a)())())
-  }
-  test("ce6bis assumeWelldefinedeness") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = CondExp(a, FalseLit()(), Not(a)())()
-
-    simplify(expr, true) should be (Not(a)())
-  }
-
-  test("ce7") {
-    val a = LocalVar("a", Bool)()
-    val z = BoolLit(false)() //z must be pure/z.isPure == true
-    val expr = CondExp(a, TrueLit()(), z)()
-
-    simplify(expr) should be (a) //(a || false) = a
-  }
-
-  test("ce8") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = CondExp(a, b, FalseLit()())()
-
-    simplify(expr) should be (And(a, b)())
-  }
-
-  test("ce9") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val expr = CondExp(a, b, TrueLit()())()
-
-    simplify(expr) should be (Implies(a, b)())
-  }
-
-
-
-
-
-
-
-
-
-
-
-  test("and5 assumeWelldefinedness"){
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = LocalVar("c", Bool)()
-    val d = And(a, And(b,c)())()
-    val e = And(And(a,b)(), And(a,c)())()
-
-    simplify(e, true) should (be (And(And(a,b)(),c)()) or be (And(And(a,b)(),c)()))
-  }
-
-  test("implies1"){
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
-
-    simplify(d, true) should be (b)
-  }
-  test("not3"){
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val d = And(Implies(a, b)(), Implies(Not(a)(), b)())()
-
-    simplify(d, true) should be (b)
-  }
-  test("implies2"){
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val d = Implies(a, b)()
-
-    simplify(d) should be (d)
-  }
-  test("implies3"){
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val z = NullLit()()
-    val y = NullLit()()
-    val c = LocalVar("c", Bool)()
-    val aa = EqCmp(a, z)()
-    val bb = EqCmp(b, y)()
-    val d = And(Implies(aa, c)(), Implies(Not(aa)(), c)())()
-
-    simplify(d, true) should be(c)
-  }
-
-  test("test1") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Or(Or(Not(a)(), Not(b)())(), FalseLit()())()
-    simplify(c) should (be (Not(And(a,b)())()) or be (Not(And(b,a)())()))
-  }
-
-  test("test14") {
-    val a = LocalVar("a", Bool)()
-    val z = LocalVar("z", Bool)()
-    val d = Or(Not(Not(a)())(), Not(Not(Not(Not(z)())())())())()
-    val f = Or(d, Not(Not(Not(Not(FalseLit()())())())())())()
-
-    simplify(f) should (be (Or(a,z)()) or be (Or(z,a)()))
-  }
-
-  test("eqcmp1") {
-    val a = LocalVar("a", Bool)()
-    val d = EqCmp(a, a)()
-    simplify(d, true) should be(TrueLit()(d.pos, d.info))
-  }
-
-  test("eqcmp2") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = NeCmp(a, b)()
-    val d = EqCmp(a, b)()
-    val e = And(c, d)()
-    val f = Or(c, d)()
-
-    simplify(e, true) should be(FalseLit()(e.pos, e.info))
-    simplify(f, true) should be(TrueLit()(f.pos, f.info))
-  }
-
-  test("eqcmp3") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = NeCmp(a, b)()
-    val d = EqCmp(a, b)()
-    val e = And(c, d)()
-    val f = Or(c, d)()
-
-    simplify(e, true) should be(FalseLit()(e.pos, e.info))
-    simplify(f, true) should be(TrueLit()(f.pos, f.info))
-  }
-
-  test("neue") {
-
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = LocalVar("c", Bool)()
-
-    simplify (And(Implies(a, b)(), Implies(a, c)())()) should be (Implies(a, And(b, c)())())
-
-    simplify (And(Implies(a, b)(), Implies(Not(a)(), b)())()) should be (And(Implies(a,b)(),Implies(Not(a)(), b)())())
-    simplify (And(Implies(a, b)(), Implies(Not(a)(), b)())(), true) should be (b)
-
-    simplify (And(a, Implies(a, b)())()) should be (And(a, b)())
-  }
-
-
-
-
-
-
-  /*test("test1") {
-
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-
-    simplify(Implies(a, b)()) should be(Implies(a, b)())
-
-    println(Implies(a, b)())
-    println(simplify(Implies(a, b)()))
-  }
-
-  test("test2") {
-
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-
-    simplify(Or(a, b)()) should be(Implies(a, b)())
-
-    println(Or(a, b)())
-    println(simplify(Implies(a, b)()))
-  }
-
-  test("test3") {
-
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-    val c = Or(a, b)()
-
-    val d = LocalVar("a", Bool)()
-    val e = LocalVar("b", Bool)()
-
-    val f = Or(d, e)()
-
-
-    c should be(f)
-
-    println(c)
-    println(f)
-  }
-
-  /*test("test4") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-    val c = Or(a, b)()
-
-    contains(c) should be(true)
-  }*/
-
-  test("test4") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(a)())()
-
-    println(b)
-    //println(genSimp(b))
-
-    true should be(true)
-  }
-
-  test("test5") {
-    val a = LocalVar("a", Bool)()
-    val b = And(a, a)()
-
-    println(b)
-    println(a.getClass)
-
-    true should be(true)
-  }
-
-  test("test6") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(a)())()
-    val c = Not(Not(b)())()
-    val tru = TrueLit()()
-    val d = Or(c, tru)()
-
-    println(d)
-    println(simplify(d))
-
-    true should be(true)
-  }
-
-  test("test7") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(Not(a)())())()
-
-    println(b)
-    println(recursiveSimplify(b))
-
-    true should be(true)
-  }
-
-  test("test8") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = And(a, Not(a)())()
-    val d = And(b, c)()
-
-
-    println(d)
-    println(d.size)
-
-    true should be(true)
-  }
-
-  test("test9") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(a)())()
-    val c = And(a, Not(a)())()
-    val d = And(b, c)()
-
-
-    println(d)
-    println(recursiveSimplify(d))
-
-    true should be(true)
-  }
-
-  test("test10") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Or(a, Not(a)())()
-    val d = Or(b, c)()
-
-
-    println(d)
-    println()
-    println(pfSimplify(d))
-
-    true should be(true)
-  }
-
-  test("test11") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(a)())()
-
-    println(b)
-    println(pfSimplify(b))
-
-    true should be(true)
-  }
-
-  test("test12") {
-    val a = LocalVar("a", Bool)()
-    val tru = TrueLit()()
-    val othertru = TrueLit()()
-    val b = Not(Not(a)())()
-    val c = Or(othertru, tru)()
-
-    println(c)
-    println(treeSize(a))
-    println(treeSize(tru))
-    println(treeSize(c))
-    println(pfSimplify(c))
-
-    true should be(true)
-  }
-
-  test("test13") {
-    val a = LocalVar("a", Bool)()
-    val b = Or(Not(Not(a)())(), a)()
-    val c = Or(Not(a)(), a)()
-
-    val buf = ArrayBuffer[Node](a, b, c)
-
-    println(getShortest(buf))
-
-    true should be(true)
-  }
-
-   */
-
-
-
-
-}

From 2392424c148cb141f7cfd4c696c9e498b133bf3f Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Sun, 15 Dec 2024 22:37:47 +0100
Subject: [PATCH 09/10] removed comments from test

---
 src/test/scala/IterativeSimplifierTest.scala | 184 -------------------
 1 file changed, 184 deletions(-)

diff --git a/src/test/scala/IterativeSimplifierTest.scala b/src/test/scala/IterativeSimplifierTest.scala
index c96dea4f6..1836a1ee8 100644
--- a/src/test/scala/IterativeSimplifierTest.scala
+++ b/src/test/scala/IterativeSimplifierTest.scala
@@ -678,188 +678,4 @@ class IterativeSimplifierTest extends AnyFunSuite with Matchers{
 
     simplify (And(a, Implies(a, b)())()) should be (And(a, b)())
   }
-
-
-
-
-
-
-  /*test("test1") {
-
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-
-    simplify(Implies(a, b)()) should be(Implies(a, b)())
-
-    println(Implies(a, b)())
-    println(simplify(Implies(a, b)()))
-  }
-
-  test("test2") {
-
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-
-    simplify(Or(a, b)()) should be(Implies(a, b)())
-
-    println(Or(a, b)())
-    println(simplify(Implies(a, b)()))
-  }
-
-  test("test3") {
-
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-    val c = Or(a, b)()
-
-    val d = LocalVar("a", Bool)()
-    val e = LocalVar("b", Bool)()
-
-    val f = Or(d, e)()
-
-
-    c should be(f)
-
-    println(c)
-    println(f)
-  }
-
-  /*test("test4") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-
-    val c = Or(a, b)()
-
-    contains(c) should be(true)
-  }*/
-
-  test("test4") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(a)())()
-
-    println(b)
-    //println(genSimp(b))
-
-    true should be(true)
-  }
-
-  test("test5") {
-    val a = LocalVar("a", Bool)()
-    val b = And(a, a)()
-
-    println(b)
-    println(a.getClass)
-
-    true should be(true)
-  }
-
-  test("test6") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(a)())()
-    val c = Not(Not(b)())()
-    val tru = TrueLit()()
-    val d = Or(c, tru)()
-
-    println(d)
-    println(simplify(d))
-
-    true should be(true)
-  }
-
-  test("test7") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(Not(a)())())()
-
-    println(b)
-    println(recursiveSimplify(b))
-
-    true should be(true)
-  }
-
-  test("test8") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = And(a, Not(a)())()
-    val d = And(b, c)()
-
-
-    println(d)
-    println(d.size)
-
-    true should be(true)
-  }
-
-  test("test9") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(a)())()
-    val c = And(a, Not(a)())()
-    val d = And(b, c)()
-
-
-    println(d)
-    println(recursiveSimplify(d))
-
-    true should be(true)
-  }
-
-  test("test10") {
-    val a = LocalVar("a", Bool)()
-    val b = LocalVar("b", Bool)()
-    val c = Or(a, Not(a)())()
-    val d = Or(b, c)()
-
-
-    println(d)
-    println()
-    println(pfSimplify(d))
-
-    true should be(true)
-  }
-
-  test("test11") {
-    val a = LocalVar("a", Bool)()
-    val b = Not(Not(a)())()
-
-    println(b)
-    println(pfSimplify(b))
-
-    true should be(true)
-  }
-
-  test("test12") {
-    val a = LocalVar("a", Bool)()
-    val tru = TrueLit()()
-    val othertru = TrueLit()()
-    val b = Not(Not(a)())()
-    val c = Or(othertru, tru)()
-
-    println(c)
-    println(treeSize(a))
-    println(treeSize(tru))
-    println(treeSize(c))
-    println(pfSimplify(c))
-
-    true should be(true)
-  }
-
-  test("test13") {
-    val a = LocalVar("a", Bool)()
-    val b = Or(Not(Not(a)())(), a)()
-    val c = Or(Not(a)(), a)()
-
-    val buf = ArrayBuffer[Node](a, b, c)
-
-    println(getShortest(buf))
-
-    true should be(true)
-  }
-
-   */
-
-
-
-
 }

From 171054cc3a84f95325409ac9ee0986c77418e417 Mon Sep 17 00:00:00 2001
From: ghaefeli <ghaefeli@student.ethz.ch>
Date: Mon, 24 Mar 2025 15:54:01 +0100
Subject: [PATCH 10/10] adjustments

---
 .../ast/utility/IterativeSimplifier.scala     | 155 +++++++++++++++---
 src/test/scala/IterativeSimplifierTest.scala  |  21 ++-
 2 files changed, 154 insertions(+), 22 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala b/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
index f30c95275..049e37dec 100644
--- a/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/IterativeSimplifier.scala
@@ -1,11 +1,13 @@
 package viper.silver.ast.utility
 
 import viper.silver.ast._
+import viper.silver.ast.utility.Statements.EmptyStmt
+import viper.silver.utility.Common.Rational
 
 import scala.collection.mutable
 import scala.collection.mutable._
 
-object IterativeSimplifier {
+trait IterativeSimplifier {
 
   /**
    * Simplify 'n' by matching nodes in the AST with a list of transformations
@@ -41,7 +43,7 @@ object IterativeSimplifier {
     getShortest(visited)
   }
 
-  private def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
+  protected def getShortest[N <: Node](visited: ArrayBuffer[N]): N = {
     visited.minBy(treeSize)
   }
 
@@ -53,8 +55,16 @@ object IterativeSimplifier {
     n.reduceTree[Boolean]((node, doubleNegs) => doubleNegs.contains(true) || isDoubleNeg(node))
   }
 
-  private def pfSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
+  def pfSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
 
+    val result: ArrayBuffer[N] = ArrayBuffer()
+
+    result ++= pfSilverCases(n, assumeWelldefinedness)
+
+    result
+  }
+
+  protected def pfSilverCases[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
     val result: ArrayBuffer[Node] = ArrayBuffer()
 
     val cases: List[PartialFunction[N, Node]] = List(
@@ -80,15 +90,17 @@ object IterativeSimplifier {
       { case root@And(_, FalseLit()) => FalseLit()(root.pos, root.info) },
 
       //Idempotence
-      { case root@And(a, b) if assumeWelldefinedness && a == b => a},
-      { case root@Or(a, b) if assumeWelldefinedness && a == b => a},
+      { case root@And(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) && a == b => a},
+      { case root@Or(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) && a == b => a},
 
-      { case root@And(a, b) => And(b, a)(root.pos, root.info)},
-      { case root@Or(a, b) => Or(b, a)(root.pos, root.info)},
+      { case root@And(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) => And(b, a)(root.pos, root.info)},
+      { case root@Or(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) => Or(b, a)(root.pos, root.info)},
+
+      { case root@And(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) => And(b, a)(root.pos, root.info)},
+      { case root@Or(a, b) if (assumeWelldefinedness || (a.isPure && b.isPure)) => Or(b, a)(root.pos, root.info)},
 
 
       //associativity
-      //WARNING: position and info attribute not correctly maintained for lchild, left and right
       { case root@And(And(left, right), rchild) => And(left, And(right, rchild)(root.pos, root.info))(root.pos, root.info)},
       { case root@And(lchild, And(left, right)) => And(And(lchild, left)(root.pos, root.info), right)(root.pos, root.info)},
 
@@ -96,7 +108,6 @@ object IterativeSimplifier {
       { case root@Or(uleft, Or(left, right)) => Or(Or(uleft, left)(root.pos, root.info), right)(root.pos, root.info)},
 
       //implication rules
-      //WARNING: position and info attributes not correctly maintained
       { case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info) },
       { case Implies(TrueLit(), consequent) => consequent },
       { case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(root.pos, root.info), r)(root.pos, root.info) },
@@ -108,9 +119,7 @@ object IterativeSimplifier {
       { case root@And(a, Implies(a2, b)) if a == a2 => And(a, b)(root.pos, root.info) },
 
       //contrapositive
-      { case root@Implies(Not(left), Not(right)) => Implies(right, left)(root.pos, root.info) },
-
-      //extended rules and/or
+      { case root@Implies(Not(left), Not(right)) if (assumeWelldefinedness || (left.isPure && right.isPure)) => Implies(right, left)(root.pos, root.info) },
 
       //de morgan
       { case root@Not(Or(left, right)) => And(Not(left)(), Not(right)())(root.pos, root.info)},
@@ -142,18 +151,14 @@ object IterativeSimplifier {
       { case root@NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info) },
 
       //extended equality/nonequality comparison
-      //some possible rules could introduce more statements, but not these ones
       { case root@EqCmp(left, right) => EqCmp(right, left)(root.pos, root.info) },
       { case root@NeCmp(left, right) => NeCmp(right, left)(root.pos, root.info) },
-      //{ case root@EqCmp(left, right) => Not(NeCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
-      //{ case root@NeCmp(left, right) => Not(EqCmp(left, right)(root.pos, root.info))(root.pos, root.info) },
       { case root@Not(EqCmp(left, right)) => NeCmp(left, right)(root.pos, root.info) },
       { case root@Not(NeCmp(left, right)) => EqCmp(left, right)(root.pos, root.info) },
       { case root@And(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => FalseLit()(root.pos, root.info)},
       { case root@Or(EqCmp(le, re), NeCmp(ln, rn)) if assumeWelldefinedness && le == ln && re == rn => TrueLit()(root.pos, root.info)},
 
       //conditional expressions
-
       { case CondExp(TrueLit(), ifTrue, _) => ifTrue },
       { case CondExp(FalseLit(), _, ifFalse) => ifFalse },
       { case CondExp(_, ifTrue, ifFalse) if assumeWelldefinedness && ifTrue == ifFalse => ifTrue },
@@ -171,6 +176,102 @@ object IterativeSimplifier {
       { case root@CondExp(condition, ifTrue, TrueLit()) => Implies(condition, ifTrue)(root.pos, root.info) },
 
       //forall&exists
+      { case root@Forall(_, _, BoolLit(literal)) =>
+        BoolLit(literal)(root.pos, root.info) },
+      { case root@Exists(_, _, BoolLit(literal)) =>
+        BoolLit(literal)(root.pos, root.info) },
+
+      { case root@Minus(IntLit(literal)) => IntLit(-literal)(root.pos, root.info) },
+      { case Minus(Minus(single)) => single },
+
+      { case PermMinus(PermMinus(single)) => single },
+      { case PermMul(fst, FullPerm()) => fst },
+      { case PermMul(FullPerm(), snd) => snd },
+      { case root@PermMul(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val product = Rational(a, b) * Rational(c, d)
+        FractionalPerm(IntLit(product.numerator)(root.pos, root.info), IntLit(product.denominator)(root.pos, root.info))(root.pos, root.info)
+      case PermMul(_, np@NoPerm()) if assumeWelldefinedness => np
+      case PermMul(np@NoPerm(), _) if assumeWelldefinedness => np },
+
+
+      { case PermMul(wc@WildcardPerm(), _) if assumeWelldefinedness => wc },
+      { case PermMul(_, wc@WildcardPerm()) if assumeWelldefinedness => wc },
+
+      { case root@PermGeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info) },
+      { case root@PermLeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info) },
+      { case root@PermGtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info) },
+      { case root@PermLtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info) },
+
+      { case root@PermGtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) > Rational(c, d))(root.pos, root.info) },
+      { case root@PermGeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) >= Rational(c, d))(root.pos, root.info) },
+      { case root@PermLtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) < Rational(c, d))(root.pos, root.info) },
+      { case root@PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) <= Rational(c, d))(root.pos, root.info) },
+      { case root@EqCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) == Rational(c, d))(root.pos, root.info) },
+      { case root@NeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) != Rational(c, d))(root.pos, root.info) },
+
+      { case root@PermLeCmp(NoPerm(), WildcardPerm()) =>
+        TrueLit()(root.pos, root.info) },
+      { case root@NeCmp(WildcardPerm(), NoPerm()) =>
+        TrueLit()(root.pos, root.info) },
+
+      { case DebugPermMin(e0@AnyPermLiteral(a, b), e1@AnyPermLiteral(c, d)) =>
+        if (Rational(a, b) < Rational(c, d)) {
+          e0
+        } else {
+          e1
+        }
+      },
+
+      { case root@PermSub(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val diff = Rational(a, b) - Rational(c, d)
+        FractionalPerm(IntLit(diff.numerator)(root.pos, root.info), IntLit(diff.denominator)(root.pos, root.info))(root.pos, root.info) },
+      { case root@PermAdd(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val sum = Rational(a, b) + Rational(c, d)
+        FractionalPerm(IntLit(sum.numerator)(root.pos, root.info), IntLit(sum.denominator)(root.pos, root.info))(root.pos, root.info) },
+      { case PermAdd(NoPerm(), rhs) => rhs },
+      { case PermAdd(lhs, NoPerm()) => lhs },
+      { case PermSub(lhs, NoPerm()) => lhs },
+
+      { case root@GeCmp(IntLit(left), IntLit(right)) =>
+        BoolLit(left >= right)(root.pos, root.info) },
+      { case root@GtCmp(IntLit(left), IntLit(right)) =>
+        BoolLit(left > right)(root.pos, root.info) },
+      { case root@LeCmp(IntLit(left), IntLit(right)) =>
+        BoolLit(left <= right)(root.pos, root.info) },
+      { case root@LtCmp(IntLit(left), IntLit(right)) =>
+        BoolLit(left < right)(root.pos, root.info) },
+
+      { case root@Add(IntLit(left), IntLit(right)) =>
+        IntLit(left + right)(root.pos, root.info) },
+      { case root@Sub(IntLit(left), IntLit(right)) =>
+        IntLit(left - right)(root.pos, root.info) },
+      { case root@Mul(IntLit(left), IntLit(right)) =>
+        IntLit(left * right)(root.pos, root.info) },
+      /* In the general case, Viper uses the SMT division and modulo. Scala's division is not in-sync with SMT division.
+         For nonnegative dividends and divisors, all used division and modulo definitions coincide. So, in order to not
+         not make any assumptions on the SMT division, division and modulo are simplified only if the dividend and divisor
+         are nonnegative. Also see Carbon PR #448.
+       */
+      { case root@Div(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+        IntLit(left / right)(root.pos, root.info) },
+      { case root@Mod(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+        IntLit(left % right)(root.pos, root.info) },
+
+      // statement simplifications
+      { case Seqn(EmptyStmt, _) => EmptyStmt }, // remove empty Seqn (including unnecessary scopedDecls)
+      { case s@Seqn(ss, scopedDecls) if ss.contains(EmptyStmt) => // remove empty statements
+        val newSS = ss.filterNot(_ == EmptyStmt)
+        Seqn(newSS, scopedDecls)(s.pos, s.info, s.errT) },
+      { case If(_, EmptyStmt, EmptyStmt) => EmptyStmt }, // remove empty If clause
+      { case If(TrueLit(), thn, _) => thn }, // remove trivial If conditions
+      { case If(FalseLit(), _, els) => els }, // remove trivial If conditions
+
     )
 
     result ++= cases.collect { case lcase if lcase.isDefinedAt(n) => lcase(n) }
@@ -188,7 +289,7 @@ object IterativeSimplifier {
     case _ => false
   }
 
-  private def pfRecSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
+  protected def pfRecSimplify[N <: Node](n: N, assumeWelldefinedness: Boolean): ArrayBuffer[N] = {
     val result: ArrayBuffer[N] = ArrayBuffer()
     result ++= pfSimplify(n, assumeWelldefinedness)
     val newChildrenList = n.children.zipWithIndex.map {
@@ -197,9 +298,6 @@ object IterativeSimplifier {
       }
       case (child: N, index) => {
         val temp = new ArrayBuffer[List[Any]]()
-          temp ++=pfSimplify(child, assumeWelldefinedness).map { pfSimpChild =>
-          n.children.toList.updated(index, pfSimpChild)
-        }
         temp ++= pfRecSimplify(child, assumeWelldefinedness).toList.map { recSimpChild =>
           n.children.toList.updated(index, recSimpChild)
         }
@@ -219,4 +317,21 @@ object IterativeSimplifier {
     newlist.map (listelem => result ++= listelem)
     result
   }
+
+
+  private val bigIntZero = BigInt(0)
+  private val bigIntOne = BigInt(1)
+
+  object AnyPermLiteral {
+    def unapply(p: Exp): Option[(BigInt, BigInt)] = p match {
+      case FullPerm() => Some((bigIntOne, bigIntOne))
+      case NoPerm() => Some((bigIntZero, bigIntOne))
+      case FractionalPerm(IntLit(n), IntLit(d)) => Some((n, d))
+      case _ => None
+    }
+  }
 }
+
+
+object IterativeSimplifier extends IterativeSimplifier
+
diff --git a/src/test/scala/IterativeSimplifierTest.scala b/src/test/scala/IterativeSimplifierTest.scala
index 1836a1ee8..e3ed75964 100644
--- a/src/test/scala/IterativeSimplifierTest.scala
+++ b/src/test/scala/IterativeSimplifierTest.scala
@@ -526,12 +526,14 @@ class IterativeSimplifierTest extends AnyFunSuite with Matchers{
     simplify(expr) should be (a)
   }
 
-  test("ce6") {
+  test("ce6 ispure") {
     val a = LocalVar("a", Bool)()
     val b = LocalVar("b", Bool)()
     val expr = CondExp(a, FalseLit()(), Not(a)())()
 
-    simplify(expr) should be (Not(Or(a,a)())())
+    println(simplify(expr))
+
+    simplify(expr) should be (Not(a)())
   }
   test("ce6bis assumeWelldefinedeness") {
     val a = LocalVar("a", Bool)()
@@ -678,4 +680,19 @@ class IterativeSimplifierTest extends AnyFunSuite with Matchers{
 
     simplify (And(a, Implies(a, b)())()) should be (And(a, b)())
   }
+
+  test("neue2") {
+
+    val a = LocalVar("a", Bool)()
+    val b = LocalVar("b", Bool)()
+    val c = LocalVar("c", Bool)()
+
+    println(simplify(And(a, And(And(a,b)(), c)())(), true, 5000, true))
+
+    true should be (true)
+  }
+
+
+
+
 }