introduce literal_vector_exprt

This introduces an expression, analogously to literal_exprt, which holds a
vector of literals.

This enables an implementation of boolbvt::handle, which returns the
literal_vector_exprt for the given bit-vector typed expression.

Author: kroening

src/solvers/flattening/boolbv.cpp

@@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <algorithm>
-
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
@@ -24,6 +22,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/floatbv/float_utils.h>
 
+#include "literal_vector_expr.h"
+
+#include <algorithm>
+
 endianness_mapt boolbvt::endianness_map(const typet &type) const
 {
   const bool little_endian =
@@ -78,6 +80,15 @@ const bvt &boolbvt::convert_bv(
   return cache_entry;
 }
 
+exprt boolbvt::handle(const exprt &expr)
+{
+  if(expr.type().id() == ID_bool)
+    return prop_conv_solvert::handle(expr);
+  auto bv = convert_bv(expr);
+  set_frozen(bv); // for incremental usage
+  return literal_vector_exprt{bv, expr.type()};
+}
+
 /// Print that the expression of x has failed conversion,
 /// then return a vector of x's width.
 bvt boolbvt::conversion_failed(const exprt &expr)
@@ -242,6 +253,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   }
   else if(expr.id() == ID_find_first_set)
     return convert_bv(simplify_expr(to_find_first_set_expr(expr).lower(), ns));
+  else if(expr.id() == ID_literal_vector)
+    return to_literal_vector_expr(expr).bv();
 
   return conversion_failed(expr);
 }

src/solvers/flattening/boolbv.h

@@ -69,6 +69,7 @@ class boolbvt:public arrayst
   exprt get(const exprt &expr) const override;
   void set_to(const exprt &expr, bool value) override;
   void print_assignment(std::ostream &out) const override;
+  exprt handle(const exprt &) override;
 
   void clear_cache() override
   {

src/solvers/flattening/literal_vector_expr.h

@@ -0,0 +1,78 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_FLATTENING_LITERAL_VECTOR_EXPR_H
+#define CPROVER_SOLVERS_FLATTENING_LITERAL_VECTOR_EXPR_H
+
+#include <util/std_expr.h>
+#include <util/string2int.h>
+
+#include <solvers/prop/literal.h>
+
+class literal_vector_exprt : public nullary_exprt
+{
+public:
+  literal_vector_exprt(const bvt &__bv, typet __type)
+    : nullary_exprt(ID_literal_vector, std::move(__type))
+  {
+    bv(__bv);
+  }
+
+  bvt bv() const
+  {
+    auto &sub = find(ID_literals).get_sub();
+    bvt result;
+    result.reserve(sub.size());
+    for(auto &literal_irep : sub)
+    {
+      literalt l;
+      l.set(literalt::var_not(
+        unsafe_string2signedlonglong(literal_irep.id_string())));
+      result.push_back(l);
+    }
+    return result;
+  }
+
+  void bv(const bvt &bv)
+  {
+    auto &sub = add(ID_literals).get_sub();
+    sub.clear();
+    sub.reserve(bv.size());
+    for(auto &literal : bv)
+      sub.emplace_back(irept{std::to_string(literal.get())});
+  }
+};
+
+template <>
+inline bool can_cast_expr<literal_vector_exprt>(const exprt &base)
+{
+  return base.id() == ID_literal_vector;
+}
+
+/// Cast a generic exprt to a \ref literal_vector_exprt. This is an unchecked
+/// conversion. \a expr must be known to be \ref literal_vector_exprt.
+/// \param expr: Source expression
+/// \return Object of type \ref literal_vector_exprt
+/// \ingroup gr_std_expr
+inline const literal_vector_exprt &to_literal_vector_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_literal_vector);
+  literal_vector_exprt::check(expr);
+  return static_cast<const literal_vector_exprt &>(expr);
+}
+
+/// \copydoc to_literal_expr(const exprt &)
+/// \ingroup gr_std_expr
+inline literal_vector_exprt &to_literal_vector_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_literal_vector);
+  literal_vector_exprt::check(expr);
+  return static_cast<literal_vector_exprt &>(expr);
+}
+
+#endif // CPROVER_SOLVERS_FLATTENING_LITERAL_VECTOR_EXPR_H

src/util/irep_ids.def

@@ -407,6 +407,8 @@ IREP_ID_ONE(is_static_assert)
 IREP_ID_ONE(is_virtual)
 IREP_ID_TWO(C_is_virtual, #is_virtual)
 IREP_ID_ONE(literal)
+IREP_ID_ONE(literal_vector)
+IREP_ID_ONE(literals)
 IREP_ID_ONE(member_initializers)
 IREP_ID_ONE(member_initializer)
 IREP_ID_ONE(method_qualifier)