Merge pull request #287 from theyoucheng/quantifier2

kroening · web-flow · commit 31a821f5e53e · 2016-11-07T13:08:41.000Z
Added support for quantifiers (forall and exists).
diff --git a/regression/cbmc/Quantifiers-assertion/main.c b/regression/cbmc/Quantifiers-assertion/main.c
@@ -0,0 +1,23 @@
+int main()
+{
+
+  int c[2][2];
+  c[0][0]=0;
+  c[0][1]=1;
+  c[1][0]=1;
+  c[1][1]=2;
+
+  __CPROVER_assert(__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "Exists-Exists: successful");
+
+  __CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-NotExists: successful");
+
+  __CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-Exists: failed");
+
+  __CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-Forall: failed");
+
+  __CPROVER_assert(!__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotForall-Forall: successful");
+
+  __CPROVER_assert(!__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotForall-NotForall: successful");
+
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] Exists-Exists: successful: SUCCESS$
+^\[main.assertion.2\] NotExists-NotExists: successful: SUCCESS$
+^\[main.assertion.3\] NotExists-Exists: failed: FAILURE$
+^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
+^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
+^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
+
+^\*\* 2 of 6 failed (2 iterations)$
+^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-assignment/main.c b/regression/cbmc/Quantifiers-assignment/main.c
@@ -0,0 +1,18 @@
+int main()
+{
+  int a[2];
+  a[0]=1;
+  a[1]=2;
+
+  int x=__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 };
+  int y=__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<2 };
+  int z1=__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<1.5 };
+  int z2=__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<2*10 };
+
+  assert(x);
+  assert(y);
+  assert(z1);
+  assert(z2);
+
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] assertion x: SUCCESS$
+^\[main.assertion.2\] assertion y: FAILURE$
+^\[main.assertion.3\] assertion z1: SUCCESS$
+^\[main.assertion.4\] assertion z2: SUCCESS$
+
+^\*\* 1 of 4 failed (2 iterations)$
+^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-copy/main.c b/regression/cbmc/Quantifiers-copy/main.c
@@ -0,0 +1,20 @@
+int main()
+{
+  int a[5];
+  int b[5];
+  
+  a[0]=0;
+  a[1]=1;
+  a[2]=2;
+  a[3]=3;
+  a[4]=4;
+
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> b[i]==a[i]});
+
+  assert(b[0]==0);
+  assert(b[1]==1);
+  assert(b[2]==2);
+  assert(b[3]==3);
+  assert(b[4]==4);
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] assertion b\[(signed long int)0\] == 0: SUCCESS$
+^\[main.assertion.2\] assertion b\[(signed long int)1\] == 1: SUCCESS$
+^\[main.assertion.3\] assertion b\[(signed long int)2\] == 2: SUCCESS$
+^\[main.assertion.4\] assertion b\[(signed long int)3\] == 3: SUCCESS$
+^\[main.assertion.5\] assertion b\[(signed long int)4\] == 4: SUCCESS$
+
+^\*\* 0 of 5 failed (1 iteration)$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-if/main.c b/regression/cbmc/Quantifiers-if/main.c
@@ -0,0 +1,23 @@
+int main()
+{
+  int a[2];
+  a[0]=1;
+  a[1]=2;
+
+  if(__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
+    __CPROVER_assert(0, "failure 1");
+
+  if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
+    __CPROVER_assert(0, "failure 2");
+
+  if(__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=2 && a[i]<=10 })
+    __CPROVER_assert(0, "success 1");
+
+  if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=2 && a[i]<=10 })
+    __CPROVER_assert(0, "failure 3");
+
+  if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 })
+    __CPROVER_assert(0, "success 2");
+
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] failure 1: FAILURE$
+^\[main.assertion.2\] failure 2: FAILURE$
+^\[main.assertion.3\] success 1: SUCCESS$
+^\[main.assertion.4\] failure 3: FAILURE$
+^\[main.assertion.5\] success 2: SUCCESS$
+
+^\*\* 3 of 5 failed (2 iterations)$
+^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-initialisation/main.c b/regression/cbmc/Quantifiers-initialisation/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  int a[5];
+  
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> a[i]==i+1});
+
+  assert(a[0]==1);
+  assert(a[1]==2);
+  assert(a[2]==3);
+  assert(a[3]==4);
+  assert(a[4]==5);
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] assertion a\[(signed long int)0\] == 1: SUCCESS$
+^\[main.assertion.2\] assertion a\[(signed long int)1\] == 2: SUCCESS$
+^\[main.assertion.3\] assertion a\[(signed long int)2\] == 3: SUCCESS$
+^\[main.assertion.4\] assertion a\[(signed long int)3\] == 4: SUCCESS$
+^\[main.assertion.5\] assertion a\[(signed long int)4\] == 5: SUCCESS$
+
+^\*\* 0 of 5 failed (1 iteration)$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-initialisation2/main.c b/regression/cbmc/Quantifiers-initialisation2/main.c
@@ -0,0 +1,18 @@
+int main()
+{
+  int a[10];
+  int c[10];
+
+  // C# style
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<9+1) ==> a[i]>=1 && a[i]<=10 });
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<10) ==>  __CPROVER_forall{int j; (j>i && j<10) ==> a[j]>a[i]} });
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<9) ==> c[i+1]>=c[i] });
+
+
+  __CPROVER_assert(__CPROVER_forall {unsigned i; (i>=0 && i<10) ==> a[i]>=1 && a[i]<=10}, "forall a[]");
+  assert(a[9]>a[1]);
+  assert(a[2]>a[3]);
+  __CPROVER_assert(__CPROVER_forall {unsigned i; (i>=1 && i<10) ==> c[i-1]<=c[i]}, "forall c[]");
+  assert(c[3]>=c[1]);
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] forall a\[\]: SUCCESS$
+^\[main.assertion.2\] assertion a\[(signed long int)9\] > a\[(signed long int)1\]: SUCCESS$
+^\[main.assertion.3\] assertion a\[(signed long int)2\] > a\[(signed long int)3\]: FAILURE$
+^\[main.assertion.4\] forall c\[\]: SUCCESS$
+^\[main.assertion.5\] assertion c\[(signed long int)3\] >= c\[(signed long int)1\]: SUCCESS$
+
+^\*\* 1 of 5 failed (2 iterations)$
+^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/main.c b/regression/cbmc/Quantifiers-invalid-var-range/main.c
@@ -0,0 +1,10 @@
+int main()
+{
+
+  int a[3][3];
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==>  __CPROVER_exists{int j; (j>=i && j<3) ==> a[i][j]==10} });
+
+  assert(a[0][0]==10||a[0][1]==10||a[0][2]==10);
+
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^\*\* Results:$
+
+^\*\* 0 of 1 failed (1 iteration)$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not-exists/main.c b/regression/cbmc/Quantifiers-not-exists/main.c
@@ -0,0 +1,30 @@
+int main()
+{
+
+  int a[2][2];
+  int b[2][2];
+  int c[2][2];
+  int d[2][2];
+
+  __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> a[i][j]<=10}) });
+
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> b[i][j]>=1 && b[i][j]<=10}) });
+
+  __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });
+
+  __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> d[i][j]>=1 && d[i][j]<=10}) });
+
+
+  assert(a[0][0]>10);
+
+  assert( (b[0][0]<1||b[0][0]>10) && (b[0][1]<1||b[0][1]>10));
+  assert( (b[1][0]<1||b[1][0]>10) && (b[1][1]<1||b[1][1]>10));
+
+  assert(c[0][0]==0 || c[0][1]==0 || c[1][0]<=10 || c[1][1]<=10);
+
+  assert( ((d[0][0]<1||d[0][0]>10) || (d[0][1]<1||d[0][1]>10)) );
+  assert( ((d[1][0]<1||d[1][0]>10) || (d[1][1]<1||d[1][1]>10)) );
+
+
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] assertion a\[(signed long int)0\]\[(signed long int)0\] > 10: SUCCESS$
+^\[main.assertion.2\] assertion tmp_if_expr$3: SUCCESS$
+^\[main.assertion.3\] assertion tmp_if_expr$6: SUCCESS$
+^\[main.assertion.4\] assertion tmp_if_expr$9: SUCCESS$
+^\[main.assertion.5\] assertion tmp_if_expr$12: SUCCESS$
+^\[main.assertion.6\] assertion tmp_if_expr$15: SUCCESS$
+
+^\*\* 0 of 6 failed (1 iteration)$
+^\VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not/main.c b/regression/cbmc/Quantifiers-not/main.c
@@ -0,0 +1,23 @@
+int main()
+{
+  int a[2];
+  a[0]=1;
+  a[1]=2;
+
+  if(!__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
+    __CPROVER_assert(0, "success 1");
+
+  if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
+    __CPROVER_assert(0, "success 2");
+
+  if(!__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=2 && a[i]<=10 })
+    __CPROVER_assert(0, "failure 1");
+
+  if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=2 && a[i]<=10 })
+    __CPROVER_assert(0, "success 3");
+
+  if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 })
+    __CPROVER_assert(0, "failure 2");
+
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] success 1: SUCCESS$
+^\[main.assertion.2\] success 2: SUCCESS$
+^\[main.assertion.3\] failure 1: FAILURE$
+^\[main.assertion.4\] success 3: SUCCESS$
+^\[main.assertion.5\] failure 2: FAILURE$
+
+^\*\* 2 of 5 failed (2 iterations)$
+^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/main.c b/regression/cbmc/Quantifiers-two-dimension-array/main.c
@@ -0,0 +1,15 @@
+int main()
+{
+  int a[2][2];
+  int b[2][2];
+  
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> a[i][j]==i+j}) });
+  __CPROVER_assume(__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> b[i][j]==i+j+1}) });
+
+  assert(a[0][0]==0);
+  assert(a[0][1]==1);
+  assert(a[1][0]==1);
+  assert(a[1][1]==2);
+  assert(b[0][0]==1 || b[0][1]==2 || b[1][0]==2 || b[1][1]==3);
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] assertion a\[(signed long int)0\]\[(signed long int)0\] == 0: SUCCESS$
+^\[main.assertion.2\] assertion a\[(signed long int)0\]\[(signed long int)1\] == 1: SUCCESS$
+^\[main.assertion.3\] assertion a\[(signed long int)1\]\[(signed long int)0\] == 1: SUCCESS$
+^\[main.assertion.4\] assertion a\[(signed long int)1\]\[(signed long int)1\] == 2: SUCCESS$
+^\[main.assertion.5\] assertion tmp_if_expr$3: SUCCESS$
+
+^\*\* 0 of 5 failed (1 iteration)$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-type/main.c b/regression/cbmc/Quantifiers-type/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  int a[2];
+  int b[2];
+
+  __CPROVER_assume( __CPROVER_forall { float i; (i>=0 && i<2) ==> a[i]>=10 && a[i]<=10 } );
+  __CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
+
+  assert(a[0]==10 && a[1]==10);
+  assert(b[0]==10 && b[1]==10);
+
+  return 0;                
+}
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] assertion tmp_if_expr$1: FAILURE$
+^\[main.assertion.2\] assertion tmp_if_expr$2: SUCCESS$
+
+^\*\* 1 of 2 failed (2 iterations)$
+^\VERIFICATION FAILED$
diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
