Added names to built-in axioms and missind QIDs to built-in quantifiers, to avoid nameless quantifiers in SMT output (#927)

Author: marcoeilers

src/main/resources/dafny_axioms/maps.vpr

@@ -12,39 +12,39 @@ domain $Map[K, V] {
 
   /* ** Cardinality */
 
-  axiom {
+  axiom Map_card_nonneg {
     forall m : $Map[K, V] :: { Map_card(m) } 0 <= Map_card(m)
   }
 
   /* added second trigger set */
-  axiom {
+  axiom Map_domain_card {
     forall m : $Map[K, V] :: { |Map_domain(m)| } {Map_card(m)} |Map_domain(m)| == Map_card(m)
   }
 
   /* ** Disjointness */
 
   /* split in both directions */
-  axiom {
+  axiom Map_disjoint_def1 {
     forall m1 : $Map[K, V], m2 : $Map[K, V] :: { Map_disjoint(m1, m2) }
       Map_disjoint(m1, m2) ==>
         (forall k : K :: { k in Map_domain(m1) } {k in Map_domain(m2) }
           !(k in Map_domain(m1)) || !(k in Map_domain(m2)))
   }
 
-  axiom {
+  axiom Map_disjoint_def2 {
     forall m1 : $Map[K, V], m2 : $Map[K, V] :: { Map_disjoint(m1, m2) }
       !Map_disjoint(m1, m2) ==>
         (exists k : K :: (k in Map_domain(m1)) && (k in Map_domain(m2)))
   }
 
   /* ** Empty */
-  axiom {
+  axiom Map_empty_domain {
     forall k : K :: { k in Map_domain((Map_empty() : $Map[K, V])) }
       !(k in Map_domain((Map_empty() : $Map[K, V])))
   }
 
   /* split last part in both directions */
-  axiom {
+  axiom Map_card_zero {
     forall m : $Map[K, V] :: { Map_card(m) }
       (Map_card(m) == 0 <==> m == Map_empty()) &&
       (Map_card(m) != 0 ==> exists u : K :: u in Map_domain(m)) &&
@@ -53,14 +53,14 @@ domain $Map[K, V] {
 
   /* Equality */
   // this axiom is only needed in one direction; the other is implied by the next axiom
-    axiom {
+    axiom Map_equal_def {
       forall m1 : $Map[K, V], m2 : $Map[K, V] :: { Map_equal(m1, m2) }
           ((forall k : K :: { k in Map_domain(m1) } { k in Map_domain(m2) } k in Map_domain(m1) <==> k in Map_domain(m2)) &&
            (forall k : K :: { Map_apply(m1, k) } { Map_apply(m2, k) } k in Map_domain(m1) ==> Map_apply(m1, k) == Map_apply(m2, k)))
              ==>  Map_equal(m1, m2)
     }
 
-  axiom {
+  axiom Map_equal_ext {
     forall m1 : $Map[K, V], m2 : $Map[K, V] :: { Map_equal(m1, m2) }
       Map_equal(m1, m2) ==> m1 == m2
   }
@@ -69,15 +69,15 @@ domain $Map[K, V] {
 
 /* added second trigger set (cf. example3 test case, test3)
 /* could also add {Map_update(m,k1,v), Map_apply(m,k1)} as another alternative trigger, but seems subsumed given that we need to know k2 is in a domain */
-  axiom {
+  axiom Map_update_domain {
     forall m : $Map[K, V], k1 : K, k2 : K, v : V ::
       { k2 in Map_domain(Map_update(m, k1, v)) } {k2 in Map_domain(m), Map_update(m, k1, v)} { Map_apply(Map_update(m, k1, v), k2) }
         (k1 == k2 ==> k2 in Map_domain(Map_update(m, k1, v)) && Map_apply(Map_update(m, k1, v), k2) == v) &&
         (k1 != k2 ==> (k2 in Map_domain(Map_update(m, k1, v)) <==> k2 in Map_domain(m)) && (k2 in Map_domain(m) ==> Map_apply(Map_update(m, k1, v), k2) == Map_apply(m, k2)))
   }
 
 /* added second trigger set (not sure of a test case needing it, though) */
-  axiom {
+  axiom Map_update_card {
     forall m : $Map[K, V], k : K, v : V :: { Map_card(Map_update(m, k, v)) } { Map_card(m), Map_update(m, k, v)}
       (k in Map_domain(m) ==> Map_card(Map_update(m, k, v)) == Map_card(m)) &&
       (!(k in Map_domain(m)) ==> Map_card(Map_update(m, k, v)) == Map_card(m) + 1)
@@ -91,20 +91,20 @@ domain $Map[K, V] {
 //        exists k : K :: { k in Map_domain(m) } { Map_apply(m, k) }
 //          k in Map_domain(m) && v == Map_apply(m, k)
 //  }
-  axiom {
+  axiom Map_values_contains {
     forall m : $Map[K, V], v : V :: { v in Map_values(m) }
       v in Map_values(m) ==>
           Map_range_domain_skolem(m,v) in Map_domain(m) && v == Map_apply(m, Map_range_domain_skolem(m,v))
   }
 
-  axiom {
+  axiom Map_values_nonempty {
     forall m : $Map[K, V], k : K :: { Map_apply(m, k) } { k in Map_domain(m) }
        (k in Map_domain(m)
           ==> |Map_values(m)| > 0) // weaker than the axiom below, but with weaker triggering
   }
 
   /* no need for an "in" term to match this one; cf. example3 test case test5 */
-  axiom {
+  axiom Map_values_contains {
     forall m : $Map[K, V], k : K :: { Map_apply(m, k) } // { k in Map_domain(m) }  // REMOVED trigger - this can create issues if several maps share the domain
        (k in Map_domain(m)
           ==> Map_apply(m, k) in Map_values(m))

src/main/resources/dafny_axioms/multisets.vpr

@@ -9,96 +9,96 @@ define Math_clip(a) a < 0 ? 0 : a
 domain $Multiset[E] {
     function Multiset_count(ms: $Multiset[E], x: E): Int
 
-    axiom {
+    axiom MS_count_nonneg {
         forall ms: $Multiset[E], x: E :: { Multiset_count(ms, x) }
             Multiset_count(ms, x) >= 0
     }
 
     function Multiset_card(ms: $Multiset[E]): Int
-    axiom {
+    axiom MS_card_nonneg {
         forall s: $Multiset[E] :: { Multiset_card(s) } 0 <= Multiset_card(s)
     }
 
     function Multiset_empty(): $Multiset[E]
-    axiom {
+    axiom MS_empty_count {
         forall o: E :: { Multiset_count(Multiset_empty(), o) } Multiset_count(Multiset_empty(), o) == 0
     }
-    axiom {
+    axiom MS_card_zero {
         forall s: $Multiset[E] :: { Multiset_card(s) }
             (Multiset_card(s) == 0 <==> s == Multiset_empty()) &&
             (Multiset_card(s) != 0 ==> (exists x: E :: 0 < Multiset_count(s, x)))
     }
 
     function Multiset_singleton(e: E): $Multiset[E]
 
-    axiom {
+    axiom MS_singleton_count {
         forall r: E, o: E :: { Multiset_count(Multiset_singleton(r), o) }
             (Multiset_count(Multiset_singleton(r), o) == 1 <==> r == o) &&
             (Multiset_count(Multiset_singleton(r), o) == 0 <==> r != o)
     }
-    axiom {
+    axiom MS_singleton_card {
         forall r: E :: { Multiset_singleton(r) } Multiset_card(Multiset_singleton(r)) == 1 && Multiset_count(Multiset_singleton(r), r) == 1
     }
-    axiom {
+    axiom MS_unionone_empty {
         forall r: E :: { Multiset_singleton(r) } Multiset_singleton(r) == Multiset_unionone(Multiset_empty(), r)
     }
 
     function Multiset_unionone(ms: $Multiset[E], t: E): $Multiset[E]
-    axiom {
+    axiom MS_unionone_count {
         forall a: $Multiset[E], x: E, o: E :: { Multiset_count(Multiset_unionone(a, x), o) } { Multiset_unionone(a, x), Multiset_count(a, o) }
             Multiset_count(Multiset_unionone(a, x), o) == (x == o ? Multiset_count(a, o) + 1 : Multiset_count(a, o))
     }
-    axiom {
+    axiom MS_unionone_card {
         forall a: $Multiset[E], x: E :: { Multiset_card(Multiset_unionone(a, x)) } { Multiset_unionone(a, x), Multiset_card(a) }
             Multiset_card(Multiset_unionone(a, x)) == Multiset_card(a) + 1
     }
-    axiom {
+    axiom MS_unionone_positive {
         forall a: $Multiset[E], x: E :: { Multiset_unionone(a, x) }
             Multiset_count(Multiset_unionone(a, x), x) > 0 && Multiset_card(Multiset_unionone(a, x)) > 0
     }
 
     function Multiset_union(ms0: $Multiset[E], ms1: $Multiset[E]): $Multiset[E]
-    axiom {
+    axiom MS_union_count {
         forall a: $Multiset[E], b: $Multiset[E], o: E :: { Multiset_count(Multiset_union(a, b), o) } { Multiset_union(a, b), Multiset_count(a, o), Multiset_count(b, o) }
             Multiset_count(Multiset_union(a, b), o) == Multiset_count(a, o) + Multiset_count(b, o)
     }
-    axiom {
+    axiom MS_union_card {
         forall a: $Multiset[E], b: $Multiset[E] :: { Multiset_card(Multiset_union(a, b)) } { Multiset_card(a), Multiset_union(a, b) } { Multiset_card(b), Multiset_union(a, b) }
             Multiset_card(Multiset_union(a, b)) == Multiset_card(a) + Multiset_card(b)
     }
 
     function Multiset_intersection(ms0: $Multiset[E], ms1: $Multiset[E]): $Multiset[E]
-    axiom {
+    axiom MS_intersect_count {
         forall a: $Multiset[E], b: $Multiset[E], o: E :: { Multiset_count(Multiset_intersection(a, b), o) }
             Multiset_count(Multiset_intersection(a, b), o) == Math_min(Multiset_count(a, o), Multiset_count(b, o))
     }
-    axiom {
+    axiom MS_intersect_absorb1 {
         forall a: $Multiset[E], b: $Multiset[E] :: { Multiset_intersection(Multiset_intersection(a, b), b) }
             Multiset_intersection(Multiset_intersection(a, b), b) == Multiset_intersection(a, b)
     }
-    axiom {
+    axiom MS_intersect_absorb2 {
         forall a: $Multiset[E], b: $Multiset[E] :: { Multiset_intersection(a, Multiset_intersection(a, b)) }
             Multiset_intersection(a, Multiset_intersection(a, b)) == Multiset_intersection(a, b)
     }
 
     function Multiset_difference(ms0: $Multiset[E], ms1: $Multiset[E]): $Multiset[E]
-    axiom {
+    axiom MS_diff_count1 {
         forall a: $Multiset[E], b: $Multiset[E], o: E :: { Multiset_count(Multiset_difference(a, b), o) }
             Multiset_count(Multiset_difference(a, b), o) == Math_clip(Multiset_count(a, o) - Multiset_count(b, o))
     }
-    axiom {
+    axiom MS_diff_count2 {
         forall a: $Multiset[E], b: $Multiset[E], y: E :: { Multiset_difference(a, b), Multiset_count(b, y), Multiset_count(a, y) }
             Multiset_count(a, y) <= Multiset_count(b, y) ==> Multiset_count(Multiset_difference(a, b), y) == 0
     }
-    axiom {
+    axiom MS_diff_card {
         forall a: $Multiset[E], b: $Multiset[E] ::
             { Multiset_card(Multiset_difference(a, b)) }
             Multiset_card(Multiset_difference(a, b)) + Multiset_card(Multiset_difference(b, a)) + 2 * Multiset_card(Multiset_intersection(a, b)) == Multiset_card(Multiset_union(a, b)) &&
             Multiset_card(Multiset_difference(a, b)) == Multiset_card(a) - Multiset_card(Multiset_intersection(a, b))
     }
 
     function Multiset_subset(ms0: $Multiset[E], ms1: $Multiset[E]): Bool
-    axiom {
+    axiom MS_subset_def {
         forall a: $Multiset[E], b: $Multiset[E] :: { Multiset_subset(a, b) }
             Multiset_subset(a, b) <==> (forall o: E :: { Multiset_count(a, o) } { Multiset_count(b, o) } Multiset_count(a, o) <= Multiset_count(b, o))
     }
@@ -111,18 +111,18 @@ domain $Multiset[E] {
     }
     */
     function Multiset_skolem_diff(s0: $Multiset[E], s1: $Multiset[E]): E
-    axiom {
+    axiom MS_equal_def {
         forall a: $Multiset[E], b: $Multiset[E] :: { Multiset_equal(a, b) }
             (Multiset_equal(a, b) && a==b) ||
             (!Multiset_equal(a, b) && a != b && Multiset_skolem_diff(a, b) == Multiset_skolem_diff(b, a) && Multiset_count(a, Multiset_skolem_diff(a, b)) != Multiset_count(b, Multiset_skolem_diff(a, b)))
     }
-    axiom {
+    axiom MS_equal_ext {
         forall a: $Multiset[E], b: $Multiset[E] :: { Multiset_equal(a, b) }
             Multiset_equal(a, b) ==> a == b
     }
 
     function Multiset_disjoint(ms0: $Multiset[E], ms1: $Multiset[E]): Bool
-    axiom {
+    axiom MS_disjoint_def {
         forall a: $Multiset[E], b: $Multiset[E] :: { Multiset_disjoint(a, b) }
             Multiset_disjoint(a, b) <==> (forall o: E :: { Multiset_count(a, o) } { Multiset_count(b, o) } Multiset_count(a, o) == 0 || Multiset_count(b, o) == 0)
     }