Refactor quantifier instantiation in solvers/flattening

Author: danpoe

src/solvers/flattening/boolbv.cpp

@@ -463,9 +463,9 @@ literalt boolbvt::convert_rest(const exprt &expr)
   else if(expr.id()==ID_extractbit)
     return convert_extractbit(to_extractbit_expr(expr));
   else if(expr.id()==ID_forall)
-    return convert_quantifier(expr);
+    return convert_quantifier(to_quantifier_expr(expr));
   else if(expr.id()==ID_exists)
-    return convert_quantifier(expr);
+    return convert_quantifier(to_quantifier_expr(expr));
   else if(expr.id()==ID_let)
   {
     bvt bv=convert_let(to_let_expr(expr));

src/solvers/flattening/boolbv.h

@@ -131,7 +131,7 @@ class boolbvt:public arrayst
   virtual literalt convert_verilog_case_equality(
     const binary_relation_exprt &expr);
   virtual literalt convert_ieee_float_rel(const exprt &expr);
-  virtual literalt convert_quantifier(const exprt &expr);
+  virtual literalt convert_quantifier(const quantifier_exprt &expr);
 
   virtual bvt convert_index(const exprt &array, const mp_integer &index);
   virtual bvt convert_index(const index_exprt &expr);

src/solvers/flattening/boolbv_quantifier.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/invariant.h>
+#include <util/optional.h>
 #include <util/replace_expr.h>
 #include <util/simplify_expr.h>
 
@@ -135,83 +136,74 @@ exprt get_quantifier_var_max(
   return res;
 }
 
-bool instantiate_quantifier(exprt &expr,
-                            const namespacet &ns)
+optionalt<exprt>
+instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
 {
   PRECONDITION(expr.id() == ID_forall || expr.id() == ID_exists);
 
-  DATA_INVARIANT(
-    expr.operands().size() == 2,
-    "quantifier expressions shall have two operands");
-
-  DATA_INVARIANT(
-    expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
-
-  exprt var_expr=expr.op0();
+  const symbol_exprt &var_expr = expr.symbol();
 
   /**
    * We need to rewrite the forall/exists quantifier into
    * an OR/AND expr.
    **/
-  exprt re(expr);
-  exprt tmp(re.op1());
-  re.swap(tmp);
-  re=simplify_expr(re, ns);
+
+  const exprt &re = simplify_expr(expr.where(), ns);
 
   if(re.is_true() || re.is_false())
   {
-    expr=re;
-    return true;
+    return re;
   }
 
-  exprt min_i=get_quantifier_var_min(var_expr, re);
-  exprt max_i=get_quantifier_var_max(var_expr, re);
-  exprt body_expr=re;
-  if(var_expr.is_false() ||
-     min_i.is_false() ||
-     max_i.is_false() ||
-     body_expr.is_false())
-    return false;
+  const exprt &min_i = get_quantifier_var_min(var_expr, re);
+  const exprt &max_i = get_quantifier_var_max(var_expr, re);
 
-  mp_integer lb, ub;
-  to_integer(min_i, lb);
-  to_integer(max_i, ub);
+  if(min_i.is_false() || max_i.is_false())
+    return nullopt;
+
+  mp_integer lb = numeric_cast_v<mp_integer>(min_i);
+  mp_integer ub = numeric_cast_v<mp_integer>(max_i);
 
   if(lb>ub)
-    return false;
+    return nullopt;
 
-  bool res=true;
   std::vector<exprt> expr_insts;
   for(mp_integer i=lb; i<=ub; ++i)
   {
-    exprt constraint_expr=body_expr;
+    exprt constraint_expr = re;
     replace_expr(var_expr,
                  from_integer(i, var_expr.type()),
                  constraint_expr);
     expr_insts.push_back(constraint_expr);
   }
+
   if(expr.id()==ID_forall)
   {
-    expr=conjunction(expr_insts);
+    return conjunction(expr_insts);
   }
-  if(expr.id()==ID_exists)
+  else if(expr.id() == ID_exists)
   {
-    expr=disjunction(expr_insts);
+    return disjunction(expr_insts);
   }
 
-  return res;
+  UNREACHABLE;
+  return nullopt;
 }
 
-literalt boolbvt::convert_quantifier(const exprt &src)
+literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
 {
   PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
 
-  exprt expr(src);
-  if(!instantiate_quantifier(expr, ns))
+  quantifier_exprt expr(src);
+  const auto res = instantiate_quantifier(expr, ns);
+
+  if(!res)
+  {
     return SUB::convert_rest(src);
+  }
 
   quantifiert quantifier;
-  quantifier.expr=expr;
+  quantifier.expr = *res;
   quantifier_list.push_back(quantifier);
 
   literalt l=prop.new_variable();