Add constraints for bounded quantification

These can only be omitted when the instantiations trivially make them true. This
surfaced further misinterpretations in the regression tests of the "==>"
operator: bounded existential quantification should generally use &&.

Author: tautschnig

regression/cbmc/Quantifiers-assertion/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-if/main.c

@@ -9,16 +9,16 @@ int main()
   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 })
+  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 })
+  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 })
+  if(__CPROVER_exists { int i; (i>=0 && i<2) && a[i]>=5 && a[i]<=10 })
     __CPROVER_assert(0, "success 2");
   // clang-format on
 

regression/cbmc/Quantifiers-invalid-var-range/main.c

@@ -4,7 +4,8 @@ int main()
   int a[3][3];
   // clang-format off
   // clang-format would rewrite the "==>" as "== >"
-  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==>  __CPROVER_exists{int j; (j>=i && j<3) ==> a[i][j]==10} });
+  // NOLINTNEXTLINE(whitespace/line_length)
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==>  __CPROVER_exists{int j; (j>=i && j<3) && a[i][j]==10} });
   // clang-format on
 
   assert(a[0][0]==10||a[0][1]==10||a[0][2]==10);

regression/cbmc/Quantifiers-not-exists/test.desc

@@ -1,15 +1,7 @@
-KNOWNBUG
+CORE
 main.c
-
-^\*\* Results:$
-^\[main.assertion.5\] line 28 assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.6\] line 30 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.7\] line 31 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.8\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.9\] line 35 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.10\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
-^\*\* 0 of 10 failed
-^VERIFICATION SUCCESSFUL$
+--cover location
+^\*\* 1 of 46 covered \(2.2%\)
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/Quantifiers-not/main.c

@@ -9,16 +9,16 @@ int main()
   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 })
+  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 })
+  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 })
+  if(!__CPROVER_exists { int i; (i>=0 && i<2) && a[i]>=5 && a[i]<=10 })
     __CPROVER_assert(0, "failure 2");
   // clang-format on
 

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^\*\* Results:$

src/solvers/flattening/boolbv_quantifier.cpp

@@ -169,11 +169,31 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
 
   if(expr.id()==ID_forall)
   {
-    return conjunction(expr_insts);
+    // maintain the domain constraint if it isn't guaranteed by the
+    // instantiations (for a disjunction the domain constraint is implied by the
+    // instantiations)
+    if(re.id() == ID_and)
+    {
+      expr_insts.push_back(binary_predicate_exprt(
+        var_expr, ID_gt, from_integer(lb, var_expr.type())));
+      expr_insts.push_back(binary_predicate_exprt(
+        var_expr, ID_le, from_integer(ub, var_expr.type())));
+    }
+    return simplify_expr(conjunction(expr_insts), ns);
   }
   else if(expr.id() == ID_exists)
   {
-    return disjunction(expr_insts);
+    // maintain the domain constraint if it isn't trivially satisfied by the
+    // instantiations (for a conjunction the instantiations are stronger
+    // constraints)
+    if(re.id() == ID_or)
+    {
+      expr_insts.push_back(binary_predicate_exprt(
+        var_expr, ID_gt, from_integer(lb, var_expr.type())));
+      expr_insts.push_back(binary_predicate_exprt(
+        var_expr, ID_le, from_integer(ub, var_expr.type())));
+    }
+    return simplify_expr(disjunction(expr_insts), ns);
   }
 
   UNREACHABLE;