fixed bugs in typechecking of linear sets

added regressions to linear sets
removed the need to supply the builtin map operations manually

6 files changed, 13 insertions, 43 deletions

diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index 40a0ab1c..c89bd793 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -1,3 +1,5 @@
+type X;

+

 function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)

 {

     currsize <= newsize && (ghostLock == nil <==> currsize == newsize)

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 63a7fc0d..8379925f 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,3 +1,5 @@
+type X;

+

 const nil: X;

 var l: X;

 var x: int;

diff --git a/Test/og/Maps.bpl b/Test/og/Maps.bpl
deleted file mode 100644
index 5f302034..00000000
--- a/Test/og/Maps.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-type X;

-

-function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int;

-function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int;

-function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int;

-function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int;

-function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int;

-function {:builtin "MapConst"} MapConstInt(int) : [X]int;

-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

-function {:builtin "MapAnd"} MapAnd([X]bool, [X]bool) : [X]bool;

-function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

-function {:builtin "MapNot"} MapNot([X]bool) : [X]bool;

-function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int;

-function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool;

-function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool;

-function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool;

-function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool;

-function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool;

-function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool;

-function {:builtin "MapIff"} MapIff([X]bool, [X]bool) : [X]bool;

-function {:builtin "MapImp"} MapImp([X]bool, [X]bool) : [X]bool;

-

-

-

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 1a0cde42..04ad0df2 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -1,12 +1,7 @@
-function {:inline} Subset(a: [X]bool, b: [X]bool) : bool

-{

-    MapImp(a, b) == MapConstBool(true)

-}

-

-function {:inline} In(a: X, b: [X]bool) : bool

-{

-    b[a]

-}

+type X;

+function {:builtin "MapConst"} MapConstInt(int) : [X]int;

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

 

 function {:inline} None() : [X]bool

 {

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index a91100b6..0df45254 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -1,12 +1,7 @@
-function {:inline} Subset(a: [X]bool, b: [X]bool) : bool

-{

-    MapImp(a, b) == MapConstBool(true)

-}

-

-function {:inline} In(a: X, b: [X]bool) : bool

-{

-    b[a]

-}

+type X;

+function {:builtin "MapConst"} MapConstInt(int) : [X]int;

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

 

 function {:inline} None() : [X]bool

 {

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 197f33f7..b00a3dda 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -12,6 +12,6 @@ for %%f in (foo.bpl bar.bpl one.bpl) do (
 for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl) do (

   echo.

   echo -------------------- %%f --------------------

-  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis  /OwickiGries:OwickiGriesDesugared.bpl %%f Maps.bpl

+  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis  /OwickiGries:OwickiGriesDesugared.bpl %%f

 )