Cleanup boolbv quantifier instantiation

1) Do not take references of temporaries.
2) No need to involve post_processing, instantiated expressions can be converted
immediately.
3) Use skip_typecast rather than local, partial typecast skipping.
4) No need for redundant precondition checks.
5) Mark file-local procedures static.

Author: tautschnig

src/solvers/flattening/boolbv.h

@@ -61,7 +61,6 @@ class boolbvt:public arrayst
 
   void post_process() override
   {
-    post_process_quantifiers();
     functions.post_process();
     SUB::post_process();
   }
@@ -234,19 +233,6 @@ class boolbvt:public arrayst
   // unbounded arrays
   bool is_unbounded_array(const typet &type) const override;
 
-  // quantifier instantiations
-  class quantifiert
-  {
-  public:
-    exprt expr;
-    literalt l;
-  };
-
-  typedef std::list<quantifiert> quantifier_listt;
-  quantifier_listt quantifier_list;
-
-  void post_process_quantifiers();
-
   typedef std::vector<std::size_t> offset_mapt;
   offset_mapt build_offset_map(const struct_typet &src);
 

src/solvers/flattening/boolbv_quantifier.cpp

@@ -9,26 +9,22 @@ 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(
+static exprt get_quantifier_var_min(
   const exprt &var_expr,
   const exprt &quantifier_expr)
 {
@@ -75,7 +71,7 @@ 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(
+static exprt get_quantifier_var_max(
   const exprt &var_expr,
   const exprt &quantifier_expr)
 {
@@ -132,27 +128,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;
@@ -183,42 +177,18 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &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);
-
-  if(!res)
-  {
-    return SUB::convert_rest(src);
-  }
-
-  quantifiert quantifier;
-  quantifier.expr = *res;
-  quantifier_list.push_back(quantifier);
-
-  literalt l=prop.new_variable();
-  quantifier_list.back().l=l;
+  const auto res = instantiate_quantifier(src, ns);
 
-  return 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)
+  if(res)
   {
-    prop.set_equal(convert_bool(it->expr), it->l);
+    return convert_bool(*res);
   }
+  else
+    return SUB::convert_rest(src);
 }