Remove unused constraint_select_one

Author: danpoe

src/solvers/Makefile

@@ -99,7 +99,6 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_concatenation.cpp \
       flattening/boolbv_cond.cpp \
       flattening/boolbv_constant.cpp \
-      flattening/boolbv_constraint_select_one.cpp \
       flattening/boolbv_div.cpp \
       flattening/boolbv_equality.cpp \
       flattening/boolbv_extractbit.cpp \

src/solvers/flattening/boolbv.cpp

@@ -182,8 +182,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
 
   if(expr.id()==ID_index)
     return convert_index(to_index_expr(expr));
-  else if(expr.id()==ID_constraint_select_one)
-    return convert_constraint_select_one(expr);
   else if(expr.id()==ID_member)
     return convert_member(to_member_expr(expr));
   else if(expr.id()==ID_with)

src/solvers/flattening/boolbv.h

@@ -140,7 +140,6 @@ class boolbvt:public arrayst
   virtual bvt convert_bswap(const bswap_exprt &expr);
   virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
   virtual bvt convert_byte_update(const byte_update_exprt &expr);
-  virtual bvt convert_constraint_select_one(const exprt &expr);
   virtual bvt convert_if(const if_exprt &expr);
   virtual bvt convert_struct(const struct_exprt &expr);
   virtual bvt convert_array(const exprt &expr);

src/solvers/flattening/boolbv_constant.cpp

@@ -6,7 +6,6 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
 bvt boolbvt::convert_constant(const constant_exprt &expr)
@@ -28,14 +27,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
 
     forall_operands(it, expr)
     {
-      const bvt &tmp=convert_bv(*it);
-
-      if(tmp.size()!=op_width)
-      {
-        error().source_location=expr.find_source_location();
-        error() << "convert_constant: unexpected operand width" << eom;
-        throw 0;
-      }
+      const bvt &tmp = convert_bv(*it, op_width);
 
       for(std::size_t j=0; j<op_width; j++)
         bv[offset+j]=tmp[j];
@@ -80,13 +72,11 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
   {
     const std::string &binary=id2string(expr.get_value());
 
-    if(binary.size()!=width)
-    {
-      error().source_location=expr.find_source_location();
-      error() << "wrong value length in constant: "
-              << expr.pretty() << eom;
-      throw 0;
-    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      binary.size() == width,
+      "constant binary value should be equal to the bitvector width",
+      expr.find_source_location(),
+      expr.pretty());
 
     for(std::size_t i=0; i<width; i++)
     {
@@ -110,13 +100,11 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
   {
     const std::string &binary=id2string(expr.get_value());
 
-    if(binary.size()*2!=width)
-    {
-      error().source_location=expr.find_source_location();
-      error() << "wrong value length in constant: "
-              << expr.pretty() << eom;
-      throw 0;
-    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      binary.size() * 2 == width,
+      "constant verilog value width should be half the bitvector width",
+      expr.find_source_location(),
+      expr.pretty());
 
     for(std::size_t i=0; i<binary.size(); i++)
     {
@@ -146,10 +134,11 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
         break;
 
       default:
-        error().source_location=expr.find_source_location();
-        error() << "unknown character in Verilog constant:"
-                << expr.pretty() << eom;
-        throw 0;
+        DATA_INVARIANT_WITH_DIAGNOSTICS(
+          false,
+          "verilog constant should only contain symbols 0, 1, x, z, and ?",
+          expr.find_source_location(),
+          expr.pretty());
       }
     }
 

src/solvers/flattening/boolbv_constraint_select_one.cpp

@@ -233,30 +233,6 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
 
     return prop.lselect(convert(op[0]), convert(op[1]), convert(op[2]));
   }
-  else if(expr.id()==ID_constraint_select_one)
-  {
-    if(op.size()<2)
-      throw "constraint_select_one takes at least two operands";
-
-    std::vector<literalt> op_bv;
-    op_bv.resize(op.size());
-
-    unsigned i=0;
-    forall_operands(it, expr)
-      op_bv[i++]=convert(*it);
-
-    // add constraints
-
-    bvt b;
-    b.reserve(op_bv.size()-1);
-
-    for(unsigned i=1; i<op_bv.size(); i++)
-      b.push_back(prop.lequal(op_bv[0], op_bv[i]));
-
-    prop.l_set_to_true(prop.lor(b));
-
-    return op_bv[0];
-  }
   else if(expr.id()==ID_or || expr.id()==ID_and || expr.id()==ID_xor ||
           expr.id()==ID_nor || expr.id()==ID_nand)
   {

src/solvers/prop/prop_conv.cpp

@@ -1796,12 +1796,6 @@ void smt2_convt::convert_expr(const exprt &expr)
     convert_expr(let_expr.where());
     out << ')'; // let
   }
-  else if(expr.id()==ID_constraint_select_one)
-  {
-    UNEXPECTEDCASE(
-      "smt2_convt::convert_expr: `"+expr.id_string()+
-      "' is not yet supported");
-  }
   else if(expr.id() == ID_bswap)
   {
     if(expr.operands().size() != 1)

src/solvers/smt2/smt2_conv.cpp

@@ -298,7 +298,6 @@ IREP_ID_ONE(predecrement)
 IREP_ID_ONE(integer_bits)
 IREP_ID_ONE(KnR)
 IREP_ID_TWO(C_KnR, #KnR)
-IREP_ID_ONE(constraint_select_one)
 IREP_ID_ONE(cond)
 IREP_ID_ONE(bv_literals)
 IREP_ID_ONE(isfinite)