Merge pull request #3926 from tautschnig/quantifier-fixes

Cleanup boolbv quantifier instantiation

Author: tautschnig

regression/cbmc/Quantifiers-not-exists/main.c renamed to regression/cbmc-cover/Quantifiers-not-exists/main.c

@@ -1,6 +1,5 @@
 int main()
 {
-
   int a[2][2];
   int b[2][2];
   int c[2][2];
@@ -25,16 +24,15 @@ int main()
 
   assert(0);
 
-  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(a[0][0] > 10);
 
-  assert(c[0][0]==0 || c[0][1]==0 || c[1][0]<=10 || c[1][1]<=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( ((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)) );
+  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;
 }

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

@@ -0,0 +1,12 @@
+CORE
+main.c
+--cover location
+^\*\* 1 of 46 covered \(2.2%\)
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+All assertions are unreachable as each of the __CPROVER_assume evaluate to false
+(!exists i. i>=0 && i<2 ==> ... is equivalent to forall i. i>=0 && i<2 && ...,
+where neither i>=0 nor i<2 is actually true for all values of i).

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

@@ -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-not/main.c

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

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

@@ -238,6 +238,11 @@ class boolbvt:public arrayst
   class quantifiert
   {
   public:
+    quantifiert(exprt _expr, literalt _l)
+      : expr(std::move(_expr)), l(std::move(_l))
+    {
+    }
+
     exprt expr;
     literalt l;
   };

src/solvers/flattening/boolbv.h

@@ -9,28 +9,23 @@ Author: Daniel Kroening, [email protected]
 #include "boolbv.h"
 
 #include <util/arith_tools.h>
+#include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/optional.h>
 #include <util/replace_expr.h>
 #include <util/simplify_expr.h>
 
 /// A method to detect equivalence between experts that can contain typecast
-bool expr_eq(const exprt &expr1, const exprt &expr2)
+static bool expr_eq(const exprt &expr1, const exprt &expr2)
 {
-  exprt e1=expr1, e2=expr2;
-  if(expr1.id()==ID_typecast)
-    e1=expr1.op0();
-  if(expr2.id()==ID_typecast)
-    e2=expr2.op0();
-  return e1==e2;
+  return skip_typecast(expr1) == skip_typecast(expr2);
 }
 
 /// To obtain the min value for the quantifier variable of the specified
 /// forall/exists operator. The min variable is in the form of "!(var_expr >
 /// constant)".
-exprt get_quantifier_var_min(
-  const exprt &var_expr,
-  const exprt &quantifier_expr)
+static exprt
+get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
 {
   PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and);
 
@@ -75,9 +70,8 @@ exprt get_quantifier_var_min(
 
 /// To obtain the max value for the quantifier variable of the specified
 /// forall/exists operator.
-exprt get_quantifier_var_max(
-  const exprt &var_expr,
-  const exprt &quantifier_expr)
+static exprt
+get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
 {
   PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and);
   exprt res = false_exprt();
@@ -132,27 +126,25 @@ exprt get_quantifier_var_max(
   return res;
 }
 
-optionalt<exprt>
+static optionalt<exprt>
 instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
 {
-  PRECONDITION(expr.id() == ID_forall || expr.id() == ID_exists);
-
   const symbol_exprt &var_expr = expr.symbol();
 
   /**
    * We need to rewrite the forall/exists quantifier into
    * an OR/AND expr.
    **/
 
-  const exprt &re = simplify_expr(expr.where(), ns);
+  const exprt re = simplify_expr(expr.where(), ns);
 
   if(re.is_true() || re.is_false())
   {
     return re;
   }
 
-  const exprt &min_i = get_quantifier_var_min(var_expr, re);
-  const exprt &max_i = get_quantifier_var_max(var_expr, re);
+  const exprt min_i = get_quantifier_var_min(var_expr, re);
+  const exprt max_i = get_quantifier_var_max(var_expr, re);
 
   if(min_i.is_false() || max_i.is_false())
     return nullopt;
@@ -175,50 +167,57 @@ 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;
-  return nullopt;
 }
 
 literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
 {
   PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
 
-  quantifier_exprt expr(src);
-  const auto res = instantiate_quantifier(expr, ns);
+  const auto res = instantiate_quantifier(src, ns);
 
-  if(!res)
-  {
-    return SUB::convert_rest(src);
-  }
-
-  quantifiert quantifier;
-  quantifier.expr = *res;
-  quantifier_list.push_back(quantifier);
+  if(res)
+    return convert_bool(*res);
 
-  literalt l=prop.new_variable();
-  quantifier_list.back().l=l;
+  // we failed to instantiate here, need to pass to post-processing
+  quantifier_list.emplace_back(quantifiert(src, prop.new_variable()));
 
-  return l;
+  return quantifier_list.back().l;
 }
 
 void boolbvt::post_process_quantifiers()
 {
-  std::set<exprt> instances;
-
   if(quantifier_list.empty())
     return;
 
-  for(auto it=quantifier_list.begin();
-      it!=quantifier_list.end();
-      ++it)
-  {
-    prop.set_equal(convert_bool(it->expr), it->l);
-  }
+  // we do not yet have any elaborate post-processing
+  for(const auto &q : quantifier_list)
+    conversion_failed(q.expr);
 }