Merge pull request #274 from romainbrenguier/string-solver-flattening

adding a convert_function_application in the flattening that will be …

Author: Daniel Kroening

src/solvers/flattening/boolbv.cpp

@@ -334,11 +334,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_function_application)
   {
-    // record
-    functions.record(to_function_application_expr(expr));
-
-    // make it free bits
-    return prop.new_variables(boolbv_width(expr.type()));
+    return convert_function_application(to_function_application_expr(expr));
   }
   else if(expr.id()==ID_reduction_or  || expr.id()==ID_reduction_and  ||
           expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
@@ -502,6 +498,30 @@ bvt boolbvt::convert_symbol(const exprt &expr)
 
   return bv;
 }
+
+
+/*******************************************************************\
+
+Function: boolbvt::convert_function_application
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bvt boolbvt::convert_function_application(
+  const function_application_exprt &expr)
+{
+  // record
+  functions.record(expr);
+
+  // make it free bits
+  return prop.new_variables(boolbv_width(expr.type()));
+}
+
 
 /*******************************************************************\
 

src/solvers/flattening/boolbv.h

@@ -169,6 +169,7 @@ class boolbvt:public arrayst
   virtual bvt convert_bv_reduction(const unary_exprt &expr);
   virtual bvt convert_not(const not_exprt &expr);
   virtual bvt convert_power(const binary_exprt &expr);
+  virtual bvt convert_function_application(const function_application_exprt &expr);
 
   virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest);
   virtual void make_free_bv_expr(const typet &type, exprt &dest);