More examples

tests/boolean/reason_about_comprehensions_coincidence_count.heyvl

@@ -0,0 +1,86 @@
+// RUN: @caesar @file
+
+// coincidence count examples from the paper "Reasoning about Comprehensions with First-Order SMT Solvers" (Section 4.2)
+domain Count {
+    // count { int i in (0 : m), int j in (0 : n) :: f [i] == g[j] }
+    // = sum { int i in (0 : m) :: count { int j in (0 : n) :: f [i] == g[j] } }
+
+    // sum_induction_below
+    func sum(lo_s: UInt, hi_s: UInt, lo_c: UInt, hi_c: UInt, f: []Int, g: []Int): Int =
+        ite(lo_s < hi_s, sum(lo_s + 1, hi_s, lo_c, hi_c, f, g) + count(lo_c, hi_c, /* i */ lo_s, f, g), 0)
+
+    axiom sum_unit forall lo_s: UInt, hi_s: UInt, lo_c: UInt, hi_c: UInt, f: []Int, g: []Int @trigger(sum(lo_s, hi_s, lo_c, hi_c, f, g)) .
+        (forall k: UInt . (lo_s <= k && k < hi_s) ==> (count(lo_c, hi_c, k, f, g) == 0)) ==> (sum(lo_s, hi_s, lo_c, hi_c, f, g) == 0)
+
+    axiom sum_split_range forall lo_s: UInt, mid_s: UInt, hi_s: UInt, lo_c: UInt, hi_c: UInt, f: []Int, g: []Int @trigger(sum(lo_s, mid_s, lo_c, hi_c, f, g), sum(mid_s, hi_s, lo_c, hi_c, f, g)) @trigger(sum(lo_s, mid_s, lo_c, hi_c, f, g), sum(lo_s, hi_s, lo_c, hi_c, f, g)) .
+            (lo_s <= mid_s && mid_s <= hi_s) ==> (sum(lo_s, mid_s, lo_c, hi_c, f, g) + sum(mid_s, hi_s, lo_c, hi_c, f, g) == sum(lo_s, hi_s, lo_c, hi_c, f, g))
+
+    axiom sum_same_term forall lo_s: UInt, hi_s: UInt, lo_c1: UInt, hi_c1: UInt, f1: []Int, g1: []Int, lo_c2: UInt, hi_c2: UInt, f2: []Int, g2: []Int @trigger(sum(lo_s, hi_s, lo_c1, hi_c1, f1, g1), sum(lo_s, hi_s, lo_c2, hi_c2, f2, g2)) .
+            (forall k: UInt . (lo_s <= k && k < hi_s) ==> (count(lo_c1, hi_c1, k, f1, g1) == count(lo_c2, hi_c2, k, f2, g2))) ==> (sum(lo_s, hi_s, lo_c1, hi_c1, f1, g1) == sum(lo_s, hi_s, lo_c2, hi_c2, f2, g2))
+
+    // count_induction_below
+    func count(lo_c: UInt, hi_c: UInt, i: UInt, f: []Int, g: []Int): Int =
+        ite(lo_c < hi_c, count(lo_c + 1, hi_c, i, f, g) + ite(select(f, i) == select(g, lo_c), 1, 0), 0)
+
+    axiom count_unit forall lo_c: UInt, hi_c: UInt, i : UInt, f: []Int, g: []Int @trigger(count(lo_c, hi_c, i, f, g)) .
+            (forall k: UInt . (lo_c <= k && k < hi_c && select(f, i) == select(g, k)) ==> (1 == 0)) ==> (count(lo_c, hi_c, i, f, g) == 0)
+
+    axiom count_split_range forall lo_c: UInt, mid_c: UInt, hi_c: UInt, i: UInt, f: []Int, g: []Int @trigger(count(lo_c, mid_c, i, f, g), count(mid_c, hi_c, i, f, g)) @trigger(count(lo_c, mid_c, i, f, g), count(lo_c, hi_c, i, f, g)) .
+            (lo_c <= mid_c && mid_c <= hi_c) ==> (count(lo_c, mid_c, i, f, g) + count(mid_c, hi_c, i, f, g) == count(lo_c, hi_c, i, f, g))
+
+    axiom count_same_term forall lo_c: UInt, hi_c: UInt, i1: UInt, f1: []Int, g1: []Int, i2: UInt, f2: []Int, g2: []Int @trigger(count(lo_c, hi_c, i1, f1, g1), count(lo_c, hi_c, i2, f2, g2)) .
+            (forall k: UInt . (lo_c <= k && k < hi_c) ==> ((select(f1, i1) == select(g1, k)) == (select(f2, i2) == select(g2, k)))) ==> (count(lo_c, hi_c, i1, f1, g1) == count(lo_c, hi_c, i2, f2, g2))
+}
+
+// todo: currently only the countTest below runs
+/*proc CoincidenceCount1(f: []Int, g: []Int) -> (ct: UInt)
+    pre ?(forall i: UInt, j: UInt . (i < j && j < len(f)) ==> (select(f, i) < select(f, j))) // f is sorted list
+    pre ?(forall i: UInt, j: UInt . (i < j && j < len(g)) ==> (select(g, i) < select(g, j))) // g is sorted list
+    post ?(ct == sum(0, len(f), 0, len(g), f, g))
+{
+    ct = 0;
+    var m: UInt = 0;
+    var n: UInt = 0;
+
+    @invariant(?(
+        ct == sum(0, m, 0, n, f, g) &&
+        m <= len(f) && n <= len(g) &&
+        m == len(f) || (forall j: UInt . (j < n) ==> (select(g, j) < select(f, m))) &&
+        n == len(g) || (forall i: UInt . (i < n) ==> (select(f, i) < select(g, n)))
+    ))
+    while (m < len(f) && n < len(g)) {
+        if (select(f, m) < select(g, n)) {
+            m = m + 1;
+        } else {
+            if (select(g, n) < select(f, m)) {
+                n = n + 1;
+            } else {
+                ct = ct + 1;
+                m = m + 1;
+                n = n + 1;
+            }
+        }
+    }
+}*/
+
+proc countTest() -> ()
+{
+    var f: []Int
+    var g: []Int
+
+    assume ?(len(f) == 3)
+    assume ?(select(f, 0) == 0)
+    assume ?(select(f, 1) == 1)
+    assume ?(select(f, 2) == 2)
+
+    assume ?(len(g) == 2)
+    assume ?(select(g, 0) == 2)
+    assume ?(select(g, 1) == 3)
+
+    assert ?(sum(0, len(f), 0, len(g), f, g) == 1)
+}
+
+/*proc smokeTest() -> ()
+{
+    assert ?(false)
+}*/

tests/boolean/reason_about_comprehensions_sum.heyvl

@@ -1,6 +1,6 @@
 // RUN: @caesar --limited-functions --force-ematching @file
 
-// Sum examples from the paper "Reasoning about Comprehensions with First-Order SMT Solvers" (Section 3.4)
+// Sum examples from the paper "Reasoning about Comprehensions with First-Order SMT Solvers" (Section 4.1)
 
 domain Sum {
     // When using limited functions, although one axiom can be created from the other using the split_range axiom,

tests/boolean/reason_about_comprehensions_sum_with_assume.heyvl

@@ -0,0 +1,39 @@
+// RUN: @caesar --limited-functions --force-ematching @file
+
+// Sum examples from the paper "Reasoning about Comprehensions with First-Order SMT Solvers" (Section 4.1)
+
+domain Sum {
+    // Induction below axiom
+    func elementSum(lo: UInt, hi: UInt, a: []Int): Int = ite(lo < hi, select(a, lo) + elementSum(lo + 1, hi, a), 0)
+}
+
+// Test that we can also verify Sum1 by equivalently assume(ing) the axiom in the proc body
+proc Sum1(a: []Int) -> (s: Int)
+    post ?(s == elementSum(0, len(a), a))
+{
+    s = 0;
+    var n: UInt = 0;
+
+    // induction_above
+    assume ?(forall lo: UInt, hi: UInt, a: []Int @trigger(elementSum(lo, hi, a)) .
+                   elementSum(lo, hi, a) == ite(lo < hi, select(a, hi - 1) + elementSum(lo, hi - 1, a), 0))
+
+    @invariant(?(n <= len(a) && s == elementSum(0, n, a)))
+    while (n < len(a)) {
+        s = s + select(a, n);
+        n = n + 1;
+    }
+}
+/*
+proc Sum2(a: []Int) -> (s: Int)
+    post ?(s == elementSum(0, len(a), a))
+{
+    s = 0;
+
+    var n: UInt = len(a);
+    @invariant(?(n <= len(a) && s == elementSum(n, len(a), a)))
+    while (1 <= n) {
+        s = s + select(a, n - 1);
+        n = n - 1;
+    }
+}*/