Merge pull request #6315 from diffblue/smt2_operand_checking

SMT-LIB2 parser: extract repeated code for operand type checking

Author: kroening

src/solvers/smt2/smt2_parser.cpp

@@ -345,11 +345,9 @@ exprt smt2_parsert::cast_bv_to_unsigned(const exprt &expr)
   return typecast_exprt(expr, unsignedbv_typet(width));
 }
 
-exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op)
+void smt2_parsert::check_matching_operand_types(
+  const exprt::operandst &op) const
 {
-  if(op.empty())
-    throw error("expression must have at least one operand");
-
   for(std::size_t i = 1; i < op.size(); i++)
   {
     if(op[i].type() != op[0].type())
@@ -360,6 +358,14 @@ exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op)
                     << smt2_format(op[i].type()) << '\'';
     }
   }
+}
+
+exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op)
+{
+  if(op.empty())
+    throw error("expression must have at least one operand");
+
+  check_matching_operand_types(op);
 
   exprt result(id, op[0].type());
   result.operands() = op;
@@ -371,13 +377,7 @@ exprt smt2_parsert::binary_predicate(irep_idt id, const exprt::operandst &op)
   if(op.size()!=2)
     throw error("expression must have two operands");
 
-  if(op[0].type() != op[1].type())
-  {
-    throw error() << "expression must have operands with matching types,"
-                     " but got '"
-                  << smt2_format(op[0].type()) << "' and '"
-                  << smt2_format(op[1].type()) << '\'';
-  }
+  check_matching_operand_types(op);
 
   return binary_predicate_exprt(op[0], id, op[1]);
 }
@@ -395,8 +395,7 @@ exprt smt2_parsert::binary(irep_idt id, const exprt::operandst &op)
   if(op.size()!=2)
     throw error("expression must have two operands");
 
-  if(op[0].type() != op[1].type())
-    throw error("expression must have operands with matching types");
+  check_matching_operand_types(op);
 
   return binary_exprt(op[0], id, op[1], op[0].type());
 }

src/solvers/smt2/smt2_parser.h

@@ -75,12 +75,12 @@ class smt2_parsert
 
   bool exit;
 
-  smt2_tokenizert::smt2_errort error(const std::string &message)
+  smt2_tokenizert::smt2_errort error(const std::string &message) const
   {
     return smt2_tokenizer.error(message);
   }
 
-  smt2_tokenizert::smt2_errort error()
+  smt2_tokenizert::smt2_errort error() const
   {
     return smt2_tokenizer.error();
   }
@@ -158,6 +158,7 @@ class smt2_parsert
   exprt::operandst operands();
   typet function_signature_declaration();
   signature_with_parameter_idst function_signature_definition();
+  void check_matching_operand_types(const exprt::operandst &) const;
   exprt multi_ary(irep_idt, const exprt::operandst &);
   exprt binary_predicate(irep_idt, const exprt::operandst &);
   exprt binary(irep_idt, const exprt::operandst &);

src/solvers/smt2/smt2_tokenizer.h

@@ -92,13 +92,13 @@ class smt2_tokenizert
   }
 
   /// generate an error exception, pre-filled with a message
-  smt2_errort error(const std::string &message)
+  smt2_errort error(const std::string &message) const
   {
     return smt2_errort(message, line_no);
   }
 
   /// generate an error exception
-  smt2_errort error()
+  smt2_errort error() const
   {
     return smt2_errort(line_no);
   }