Merge pull request diffblue#5810 from diffblue/remove-boolbvt-literals

remove dead boolbvt::literals(...)

Author: kroening

src/solvers/flattening/boolbv.cpp

@@ -31,89 +31,6 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/floatbv/float_utils.h>
 #include <solvers/lowering/expr_lowering.h>
 
-bool boolbvt::literal(
-  const exprt &expr,
-  const std::size_t bit,
-  literalt &dest) const
-{
-  if(expr.type().id()==ID_bool)
-  {
-    INVARIANT(
-      bit == 0,
-      "boolean expressions shall be represented by a single bit and hence the "
-      "only valid bit index is 0");
-    return prop_conv_solvert::literal(to_symbol_expr(expr), dest);
-  }
-  else
-  {
-    if(expr.id()==ID_symbol ||
-       expr.id()==ID_nondet_symbol)
-    {
-      const irep_idt &identifier=expr.get(ID_identifier);
-
-      boolbv_mapt::mappingt::const_iterator it_m=
-        map.mapping.find(identifier);
-
-      if(it_m==map.mapping.end())
-        return true;
-
-      const boolbv_mapt::map_entryt &map_entry=it_m->second;
-
-      INVARIANT(
-        bit < map_entry.literal_map.size(), "bit index shall be within bounds");
-      if(!map_entry.literal_map[bit].is_set)
-        return true;
-
-      dest=map_entry.literal_map[bit].l;
-      return false;
-    }
-    else if(expr.id()==ID_index)
-    {
-      const index_exprt &index_expr=to_index_expr(expr);
-
-      std::size_t element_width=boolbv_width(index_expr.type());
-      CHECK_RETURN(element_width != 0);
-
-      const auto &index = index_expr.index();
-      PRECONDITION(index.id() == ID_constant);
-      mp_integer index_int =
-        numeric_cast_v<mp_integer>(to_constant_expr(index));
-
-      std::size_t offset =
-        numeric_cast_v<std::size_t>(index_int * element_width);
-
-      return literal(index_expr.array(), bit+offset, dest);
-    }
-    else if(expr.id()==ID_member)
-    {
-      const member_exprt &member_expr=to_member_expr(expr);
-
-      const struct_typet::componentst &components=
-        to_struct_type(expr.type()).components();
-      const irep_idt &component_name=member_expr.get_component_name();
-
-      std::size_t offset=0;
-
-      for(const auto &c : components)
-      {
-        const typet &subtype = c.type();
-
-        if(c.get_name() == component_name)
-          return literal(member_expr.struct_op(), bit + offset, dest);
-
-        std::size_t element_width=boolbv_width(subtype);
-        CHECK_RETURN(element_width != 0);
-
-        offset+=element_width;
-      }
-
-      INVARIANT(false, "struct type should have accessed component");
-    }
-  }
-
-  INVARIANT(false, "expression should have a corresponding literal");
-}
-
 /// Convert expression to vector of literalts, using an internal
 /// cache to speed up conversion if available. Also assert the resultant
 /// vector is of a specific size, and freeze any elements if appropriate.

src/solvers/flattening/boolbv.h

@@ -77,12 +77,6 @@ class boolbvt:public arrayst
     SUB::post_process();
   }
 
-  // get literals for variables/expressions, if available
-  virtual bool literal(
-    const exprt &expr,
-    std::size_t bit,
-    literalt &literal) const;
-
   enum class unbounded_arrayt { U_NONE, U_ALL, U_AUTO };
   unbounded_arrayt unbounded_array;
 

src/solvers/prop/prop_conv_solver.cpp

@@ -57,21 +57,6 @@ exprt prop_conv_solvert::handle(const exprt &expr)
   return literal_exprt(l);
 }
 
-bool prop_conv_solvert::literal(const symbol_exprt &expr, literalt &dest) const
-{
-  PRECONDITION(expr.type().id() == ID_bool);
-
-  const irep_idt &identifier = expr.get_identifier();
-
-  symbolst::const_iterator result = symbols.find(identifier);
-
-  if(result == symbols.end())
-    return true;
-
-  dest = result->second;
-  return false;
-}
-
 literalt prop_conv_solvert::get_literal(const irep_idt &identifier)
 {
   auto result =

src/solvers/prop/prop_conv_solver.h

@@ -69,9 +69,6 @@ class prop_conv_solvert : public conflict_providert,
 
   void pop() override;
 
-  // get literal for expression, if available
-  bool literal(const symbol_exprt &expr, literalt &literal) const;
-
   bool use_cache = true;
   bool equality_propagation = true;
   bool freeze_all = false; // freezing variables (for incremental solving)