pretty formatting of SMT2 types in error messages

Author: Daniel Kroening

src/solvers/smt2/smt2_parser.cpp

@@ -10,6 +10,22 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 
+std::ostream &operator<<(std::ostream &out, const smt2_parsert::smt2_format &f)
+{
+  if(f.type.id() == ID_unsignedbv)
+    out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')';
+  else if(f.type.id() == ID_bool)
+    out << "Bool";
+  else if(f.type.id() == ID_integer)
+    out << "Int";
+  else if(f.type.id() == ID_real)
+    out << "Real";
+  else
+    out << "? " << f.type.id();
+
+  return out;
+}
+
 void smt2_parsert::command_sequence()
 {
   exit=false;
@@ -360,8 +376,8 @@ exprt smt2_parsert::multi_ary(irep_idt id, const exprt::operandst &op)
       {
         error() << "expression must have operands with matching types,"
                    " but got `"
-                << op[0].type().pretty()
-                << "' and `" << op[i].type().pretty() << '\'' << eom;
+                << smt2_format(op[0].type()) << "' and `"
+                << smt2_format(op[i].type()) << '\'' << eom;
         return nil_exprt();
       }
     }
@@ -385,8 +401,8 @@ exprt smt2_parsert::binary_predicate(irep_idt id, const exprt::operandst &op)
     {
       error() << "expression must have operands with matching types,"
                  " but got `"
-              << op[0].type().pretty()
-              << "' and `" << op[1].type().pretty() << '\'' << eom;
+              << smt2_format(op[0].type()) << "' and `"
+              << smt2_format(op[1].type()) << '\'' << eom;
       return nil_exprt();
     }
 

src/solvers/smt2/smt2_parser.h

@@ -43,6 +43,15 @@ class smt2_parsert:public smt2_tokenizert
   using id_mapt=std::map<irep_idt, idt>;
   id_mapt id_map;
 
+  struct smt2_format
+  {
+    explicit smt2_format(const typet &_type) : type(_type)
+    {
+    }
+
+    const typet type;
+  };
+
 protected:
   bool exit;
   void command_sequence();
@@ -82,4 +91,6 @@ class smt2_parsert:public smt2_tokenizert
   exprt cast_bv_to_unsigned(const exprt &);
 };
 
+std::ostream &operator<<(std::ostream &, const smt2_parsert::smt2_format &);
+
 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H