From 0b5af50545d93128256acabcd09ec09996f495f6 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Mon, 27 May 2013 12:32:24 +0530
Subject: AbsHoudini: Added support for quantifiers

---
 Test/AbsHoudini/Answer      | 48 +++++++++++++++++++++++++++++++++++++++++++++
 Test/AbsHoudini/pred5.bpl   | 24 +++++++++++++++++++++++
 Test/AbsHoudini/quant1.bpl  |  7 +++++++
 Test/AbsHoudini/quant2.bpl  | 24 +++++++++++++++++++++++
 Test/AbsHoudini/quant3.bpl  |  7 +++++++
 Test/AbsHoudini/quant4.bpl  |  7 +++++++
 Test/AbsHoudini/quant5.bpl  | 11 +++++++++++
 Test/AbsHoudini/runtest.bat |  8 +++++++-
 8 files changed, 135 insertions(+), 1 deletion(-)
 create mode 100644 Test/AbsHoudini/pred5.bpl
 create mode 100644 Test/AbsHoudini/quant1.bpl
 create mode 100644 Test/AbsHoudini/quant2.bpl
 create mode 100644 Test/AbsHoudini/quant3.bpl
 create mode 100644 Test/AbsHoudini/quant4.bpl
 create mode 100644 Test/AbsHoudini/quant5.bpl

(limited to 'Test/AbsHoudini')

diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer
index 58da416e..db2f6631 100644
--- a/Test/AbsHoudini/Answer
+++ b/Test/AbsHoudini/Answer
@@ -439,3 +439,51 @@ function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : boo
 }
 
 Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred5.bpl --------------------
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+  x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant1.bpl --------------------
+function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 2
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant2.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 1
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant3.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant4.bpl --------------------
+function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool
+{
+  true
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- quant5.bpl --------------------
+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool
+{
+  x >= 5 && x <= 5
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl
new file mode 100644
index 00000000..6940e820
--- /dev/null
+++ b/Test/AbsHoudini/pred5.bpl
@@ -0,0 +1,24 @@
+function {:existential true} b1(x: bool) : bool;
+
+procedure main() 
+{
+   var i: int;
+   var x: int;
+   var arr: [int] int;
+
+   i := 0;
+
+   while(*) 
+     invariant b1((i >= 0) && (forall j: int :: (0 <= j && j < i) ==> arr[j] == 0));
+   {
+       havoc x;
+       assume x == 0;
+
+       arr[i] := x;
+       i := i + 1;
+   }
+
+   havoc x;
+   assume x >= 0 && x < i;
+   assert b1(arr[x] == 0);
+}
diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl
new file mode 100644
index 00000000..e12525b6
--- /dev/null
+++ b/Test/AbsHoudini/quant1.bpl
@@ -0,0 +1,7 @@
+function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool;
+
+procedure foo ()
+{
+  assert (forall x: int :: (0 <= x && x <= 2) ==> b1(x));
+}
+
diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl
new file mode 100644
index 00000000..5a491877
--- /dev/null
+++ b/Test/AbsHoudini/quant2.bpl
@@ -0,0 +1,24 @@
+function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
+
+procedure main() 
+{
+   var i: int;
+   var x: int;
+   var arr: [int] int;
+
+   i := 0;
+
+   while(*) 
+     invariant (i >= 0) && (forall j: int :: (0 <= j && j < i) ==> b1(arr[j]));
+   {
+       havoc x;
+       assume x == 0 || x == 1;
+
+       arr[i] := x;
+       i := i + 1;
+   }
+
+   havoc x;
+   assume x >= 0 && x < i;
+   assert arr[x] == 0 || arr[x] == 1;
+}
diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl
new file mode 100644
index 00000000..cc0ef79e
--- /dev/null
+++ b/Test/AbsHoudini/quant3.bpl
@@ -0,0 +1,7 @@
+function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
+
+procedure foo ()
+{
+  assert (exists x: int :: (0 <= x && x <= 2) && b1(x));
+}
+
diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl
new file mode 100644
index 00000000..55947f1f
--- /dev/null
+++ b/Test/AbsHoudini/quant4.bpl
@@ -0,0 +1,7 @@
+function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool;
+
+procedure foo ()
+{
+  assert (exists x: int :: (0 <= x && x <= 2) && b1());
+}
+
diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl
new file mode 100644
index 00000000..dfc44e47
--- /dev/null
+++ b/Test/AbsHoudini/quant5.bpl
@@ -0,0 +1,11 @@
+function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
+
+procedure foo ()
+{
+  var arr: [int] int;
+  assume (forall x: int :: arr[x] == 0);
+  arr[5] := 1;
+
+  assert (exists x: int :: arr[x] == 1 && b1(x));
+}
+
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat
index 0bc74dfc..4d70be0e 100644
--- a/Test/AbsHoudini/runtest.bat
+++ b/Test/AbsHoudini/runtest.bat
@@ -15,8 +15,14 @@ for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
   %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1  /abstractHoudini:IA[ConstantProp] %%f
 )
 
-for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl) do (
+for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl pred5.bpl) do (
   echo .
   echo -------------------- %%f --------------------
   %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1  /abstractHoudini:PredicateAbs %%f
 )
+
+for %%f in (quant1.bpl quant2.bpl quant3.bpl quant4.bpl quant5.bpl) do (
+  echo .
+  echo -------------------- %%f --------------------
+  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:HoudiniConst /z3opt:MBQI=true %%f
+)
-- 
cgit v1.2.3