pkgs/by-name/bo/boogie/install-check-file.bpl

   1 // RUN: %parallel-boogie "%s" > "%t"
   2 // RUN: %diff "%s.expect" "%t"
   3 type X;
   4
   5 function {:builtin "MapAdd"} mapadd([X]int, [X]int) : [X]int;
   6 function {:builtin "MapSub"} mapsub([X]int, [X]int) : [X]int;
   7 function {:builtin "MapMul"} mapmul([X]int, [X]int) : [X]int;
   8 function {:builtin "MapDiv"} mapdiv([X]int, [X]int) : [X]int;
   9 function {:builtin "MapMod"} mapmod([X]int, [X]int) : [X]int;
  10 function {:builtin "MapConst"} mapconstint(int) : [X]int;
  11 function {:builtin "MapConst"} mapconstbool(bool) : [X]bool;
  12 function {:builtin "MapAnd"} mapand([X]bool, [X]bool) : [X]bool;
  13 function {:builtin "MapOr"} mapor([X]bool, [X]bool) : [X]bool;
  14 function {:builtin "MapNot"} mapnot([X]bool) : [X]bool;
  15 function {:builtin "MapIte"} mapiteint([X]bool, [X]int, [X]int) : [X]int;
  16 function {:builtin "MapIte"} mapitebool([X]bool, [X]bool, [X]bool) : [X]bool;
  17 function {:builtin "MapLe"} maple([X]int, [X]int) : [X]bool;
  18 function {:builtin "MapLt"} maplt([X]int, [X]int) : [X]bool;
  19 function {:builtin "MapGe"} mapge([X]int, [X]int) : [X]bool;
  20 function {:builtin "MapGt"} mapgt([X]int, [X]int) : [X]bool;
  21 function {:builtin "MapEq"} mapeq([X]int, [X]int) : [X]bool;
  22 function {:builtin "MapIff"} mapiff([X]bool, [X]bool) : [X]bool;
  23 function {:builtin "MapImp"} mapimp([X]bool, [X]bool) : [X]bool;
  24
  25
  26
  27 const FF: [X]bool;
  28 axiom FF == mapconstbool(false);
  29
  30 const TT: [X]bool;
  31 axiom TT == mapconstbool(true);
  32
  33 const MultisetEmpty: [X]int;
  34 axiom MultisetEmpty == mapconstint(0);
  35
  36 function {:inline} MultisetSingleton(x: X) : [X]int
  37 {
  38   MultisetEmpty[x := 1]
  39 }
  40
  41 function {:inline} MultisetPlus(a: [X]int, b: [X]int) : [X]int
  42 {
  43   mapadd(a, b)
  44 }
  45
  46 function {:inline} MultisetMinus(a: [X]int, b: [X]int)  : [X]int
  47 {
  48   mapiteint(mapgt(a, b), mapsub(a, b), mapconstint(0))
  49 }
  50
  51 procedure foo() {
  52   var x: X;
  53
  54   assert FF != TT;
  55   assert mapnot(FF) == TT;
  56
  57   assert MultisetSingleton(x) != MultisetEmpty;
  58   assert MultisetPlus(MultisetEmpty, MultisetSingleton(x)) == MultisetSingleton(x);
  59   assert MultisetMinus(MultisetPlus(MultisetEmpty, MultisetSingleton(x)), MultisetSingleton(x)) == MultisetEmpty;
  60   assert MultisetMinus(MultisetEmpty, MultisetSingleton(x)) == MultisetEmpty;
  61 }