add support for let_exprt

Author: Daniel Kroening

src/ansi-c/expr2c.cpp

@@ -944,6 +944,26 @@ std::string expr2ct::convert_with(
   return dest;
 }
 
+std::string expr2ct::convert_let(
+  const let_exprt &src,
+  unsigned precedence)
+{
+  if(src.operands().size()<3)
+    return convert_norep(src, precedence);
+
+  unsigned p0;
+  std::string op0=convert_with_precedence(src.op0(), p0);
+
+  std::string dest="LET ";
+  dest+=convert(src.symbol());
+  dest+='=';
+  dest+=convert(src.value());
+  dest+=" IN ";
+  dest+=convert(src.where());
+
+  return dest;
+}
+
 std::string expr2ct::convert_update(
   const exprt &src,
   unsigned precedence)
@@ -3936,6 +3956,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_sizeof)
     return convert_sizeof(src, precedence);
 
+  else if(src.id()==ID_let)
+    return convert_let(to_let_expr(src), precedence=16);
+
   else if(src.id()==ID_type)
     return convert(src.type());
 

src/ansi-c/expr2c_class.h

@@ -253,6 +253,7 @@ class expr2ct
   std::string convert_designated_initializer(const exprt &src, unsigned &precedence);
   std::string convert_concatenation(const exprt &src, unsigned &precedence);
   std::string convert_sizeof(const exprt &src, unsigned &precedence);
+  std::string convert_let(const let_exprt &, unsigned precedence);
 
   std::string convert_struct(
     const exprt &src,

src/solvers/Makefile

@@ -125,6 +125,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_ieee_float_rel.cpp \
       flattening/boolbv_if.cpp \
       flattening/boolbv_index.cpp \
+      flattening/boolbv_let.cpp \
       flattening/boolbv_map.cpp \
       flattening/boolbv_member.cpp \
       flattening/boolbv_mod.cpp \

src/solvers/flattening/boolbv.cpp

@@ -278,14 +278,10 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_array_of)
     return convert_array_of(to_array_of_expr(expr));
   else if(expr.id()==ID_let)
-  {
-    // const let_exprt &let_expr=to_let_expr(expr);
-    throw "let is todo";
-  }
+    return convert_let(to_let_expr(expr));
   else if(expr.id()==ID_function_application)
-  {
-    return convert_function_application(to_function_application_expr(expr));
-  }
+    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 ||
           expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
@@ -463,6 +459,15 @@ literalt boolbvt::convert_rest(const exprt &expr)
     return convert_quantifier(expr);
   else if(expr.id()==ID_exists)
     return convert_quantifier(expr);
+  else if(expr.id()==ID_let)
+  {
+    bvt bv=convert_let(to_let_expr(expr));
+
+    DATA_INVARIANT(bv.size()==1,
+      "convert_let must return 1-bit vector for boolean let");
+
+    return bv[0];
+  }
   else if(expr.id()==ID_index)
   {
     bvt bv=convert_index(to_index_expr(expr));

src/solvers/flattening/boolbv.h

@@ -145,6 +145,7 @@ class boolbvt:public arrayst
   virtual bvt convert_complex_real(const exprt &expr);
   virtual bvt convert_complex_imag(const exprt &expr);
   virtual bvt convert_lambda(const exprt &expr);
+  virtual bvt convert_let(const let_exprt &);
   virtual bvt convert_array_of(const array_of_exprt &expr);
   virtual bvt convert_union(const union_exprt &expr);
   virtual bvt convert_bv_typecast(const typecast_exprt &expr);

src/solvers/flattening/boolbv_let.cpp

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "boolbv.h"
+
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+bvt boolbvt::convert_let(const let_exprt &expr)
+{
+  const bvt value_bv=convert_bv(expr.value());
+
+  // We expect the identifiers of the bound symbols to be unique,
+  // and thus, these can go straight into the symbol to literal map.
+  // This property also allows us to cache any subexpressions.
+  const irep_idt &id=expr.symbol().get_identifier();
+
+  // the symbol shall be visible during the recursive call
+  // to convert_bv
+  map.set_literals(id, expr.symbol().type(), value_bv);
+  bvt result_bv=convert_bv(expr.where());
+
+  // now remove, no longer needed
+  map.erase_literals(id, expr.symbol().type());
+
+  return result_bv;
+}

src/solvers/flattening/boolbv_map.cpp

@@ -146,3 +146,10 @@ void boolbv_mapt::set_literals(
     mb.l=literal;
   }
 }
+
+void boolbv_mapt::erase_literals(
+  const irep_idt &identifier,
+  const typet &)
+{
+  mapping.erase(identifier);
+}

src/solvers/flattening/boolbv_map.h

@@ -75,6 +75,10 @@ class boolbv_mapt
     const typet &type,
     const bvt &literals);
 
+  void erase_literals(
+    const irep_idt &identifier,
+    const typet &type);
+
 protected:
   propt ∝
   const namespacet &ns;

src/solvers/prop/prop_conv.cpp

@@ -327,8 +327,25 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
   }
   else if(expr.id()==ID_let)
   {
-    // const let_exprt &let_expr=to_let_expr(expr);
-    throw "let is todo";
+    const let_exprt &let_expr=to_let_expr(expr);
+
+    // first check whether this is all boolean
+    if(let_expr.value().type().id()==ID_bool &&
+       let_expr.where().type().id()==ID_bool)
+    {
+      literalt value=convert(let_expr.value());
+
+      // We expect the identifier of the bound symbols to be unique,
+      // and thus, these can go straight into the symbol map.
+      // This property also allows us to cache any subexpressions.
+      const irep_idt &id=let_expr.symbol().get_identifier();
+      symbols[id]=value;
+      literalt result=convert(let_expr.where());
+
+      // remove again
+      symbols.erase(id);
+      return result;
+    }
   }
 
   return convert_rest(expr);