Merge branch 'dev' into fix-utwente-fmt#1215

sakehl · Jun 25, 2024 · 0e97812 · 0e97812
2 parents ae2a7e7 + 523623e
commit 0e97812
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 14 deletions.
diff --git a/examples/publications/2020/permutations/permutation.pvl b/examples/publications/2020/permutations/permutation.pvl
@@ -38,6 +38,7 @@ ensures (\forall T q; {:count<T>(xs[i -> e], q):} == (
 ));
 void lemma_count_of_replace<T>(seq<T> xs, int i, T e) {
     if(i != 0) {
+        assert xs[i -> e] == (xs.head :: xs.tail[i-1 -> e]);
         lemma_count_of_replace<T>(xs.tail, i-1, e);
     }
 }

diff --git a/examples/verifythis/2018/challenge2.pvl b/examples/verifythis/2018/challenge2.pvl
@@ -30,20 +30,25 @@ class ColoredTiles {
   pure boolean has_false_in_prefix(seq<boolean> s,int k)
    = (\exists int y;0<=y && y < k+1 && y<|s|; s[y]==false);
 
-  ensures (s1 == s2) == (prefix + s1 == prefix + s2);
-  void lemma_uniqueness_prefix(seq<boolean> s1,seq<boolean> s2,seq<boolean> prefix){
-    if (|s1| == |s2|){
-      seq<boolean> s3 = prefix + s1;
-      seq<boolean> s4 = prefix + s2;
-      par lemma_up_par (int y=0..|s1|)
-        requires s3 == prefix + s1;
-        requires s4 == prefix + s2;
-        requires |s1| == |s2|;
-        ensures (s1[y]==s2[y]) == (s3[|prefix|+y]==s4[|prefix|+y]);
-      {
+  ensures left != right ==> (prefix + left != prefix + right);
+  void lemma_uniqueness_prefix(seq<boolean> left, seq<boolean> right, seq<boolean> prefix) {
+    if (|left| == |right|) {
+      int i = 0;
+
+      loop_invariant 0 <= i && i <= |left|;
+      loop_invariant (\forall int j = 0..i; left[j] == right[j]);
+      for(; i < |left| && left[i] == right[i]; i++) {
+
       }
+
+      if(i == |left|) {
+        assert left == right;
+      } else {
+        assert (prefix+left)[i + |prefix|] != (prefix+right)[i + |prefix|];
+      }
+    } else {
+      assert |prefix + left| != |prefix + right|;
     }
-    return;
   }
 
   requires l <= k && 0 <= l;

diff --git a/src/col/vct/col/ast/node/NodeSubnodeOps.scala b/src/col/vct/col/ast/node/NodeSubnodeOps.scala
@@ -49,8 +49,11 @@ trait NodeSubnodeOps[G] {
     None
   }
 
-  def exists[T](f: PartialFunction[Node[G], Boolean]): Boolean =
-    collectFirst(f).getOrElse(false)
+  def exists[T](f: PartialFunction[Node[G], Boolean]): Boolean = {
+    var res = false
+    visit(node => res = res || f.lift(node).getOrElse(false))
+    res
+  }
 
   def count[T](f: PartialFunction[Node[G], Unit]): Int = {
     var result: Int = 0