SMT2: do not quote simple symbols

The |...| for quoting are unneccesary when the symbol name meets the
definition of a simple symbol.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -41,6 +41,8 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/lowering/expr_lowering.h>
 #include <solvers/prop/literal_expr.h>
 
+#include "smt2_tokenizer.h"
+
 // Mark different kinds of error conditions
 
 // Unexpected types and other combinations not implemented and not
@@ -904,18 +906,37 @@ void smt2_convt::pop()
   assumptions.clear();
 }
 
+static bool is_smt2_simple_identifier(const std::string &identifier)
+{
+  if(identifier.empty())
+    return false;
+
+  if(isdigit(identifier[0]))
+    return false;
+
+  for(auto ch : id2string(identifier))
+  {
+    if(!is_smt2_simple_symbol_character(ch))
+      return false;
+  }
+
+  return true;
+}
+
 std::string smt2_convt::convert_identifier(const irep_idt &identifier)
 {
+  // Is this a "simple identifier"?
+  if(is_smt2_simple_identifier(id2string(identifier)))
+    return id2string(identifier);
+
   // Backslashes are disallowed in quoted symbols just for simplicity.
   // Otherwise, for Common Lisp compatibility they would have to be treated
   // as escaping symbols.
 
   std::string result = "|";
 
-  for(std::size_t i=0; i<identifier.size(); i++)
+  for(auto ch : identifier)
   {
-    char ch=identifier[i];
-
     switch(ch)
     {
     case '|':

src/solvers/smt2/smt2_tokenizer.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2_tokenizer.h"
 
-bool smt2_tokenizert::is_simple_symbol_character(char ch)
+bool is_smt2_simple_symbol_character(char ch)
 {
   // any non-empty sequence of letters, digits and the characters
   // ~ ! @ $ % ^ & * _ - + = < > . ? /
@@ -32,7 +32,7 @@ smt2_tokenizert::tokent smt2_tokenizert::get_simple_symbol()
   char ch;
   while(in->get(ch))
   {
-    if(is_simple_symbol_character(ch))
+    if(is_smt2_simple_symbol_character(ch))
     {
       buffer+=ch;
     }
@@ -294,7 +294,7 @@ void smt2_tokenizert::get_token_from_stream()
         token = get_decimal_numeral();
         return;
       }
-      else if(is_simple_symbol_character(ch))
+      else if(is_smt2_simple_symbol_character(ch))
       {
         in->unget();
         token = get_simple_symbol();

src/solvers/smt2/smt2_tokenizer.h

@@ -120,7 +120,6 @@ class smt2_tokenizert
   tokent get_simple_symbol();
   tokent get_quoted_symbol();
   tokent get_string_literal();
-  static bool is_simple_symbol_character(char);
 
   /// read a token from the input stream and store it in 'token'
   void get_token_from_stream();
@@ -135,4 +134,6 @@ operator<<(smt2_tokenizert::smt2_errort &&e, const T &message)
   return std::move(e);
 }
 
+bool is_smt2_simple_symbol_character(char);
+
 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H

unit/solvers/smt2/smt2_conv.cpp

@@ -12,8 +12,8 @@ TEST_CASE(
     "abcdefghijklmnopqrstuvwxyz0123456789$";
   CHECK(
     smt2_convt::convert_identifier(no_escaping_characters) ==
-    "|" + no_escaping_characters + "|");
+    no_escaping_characters);
   CHECK(smt2_convt::convert_identifier("\\") == "|&92;|");
   CHECK(smt2_convt::convert_identifier("|") == "|&124;|");
-  CHECK(smt2_convt::convert_identifier("&") == "|&38;|");
+  CHECK(smt2_convt::convert_identifier("&") == "&");
 }

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -13,7 +13,7 @@
 
 TEST_CASE("Test smt_indext to string conversion", "[core][smt2_incremental]")
 {
-  CHECK(smt_to_smt2_string(smt_symbol_indext{"green"}) == "|green|");
+  CHECK(smt_to_smt2_string(smt_symbol_indext{"green"}) == "green");
   CHECK(smt_to_smt2_string(smt_numeral_indext{42}) == "42");
 }
 
@@ -36,7 +36,7 @@ TEST_CASE(
 {
   CHECK(
     smt_to_smt2_string(smt_bit_vector_theoryt::extract(7, 3)(
-      smt_bit_vector_constant_termt{0, 8})) == "((_ |extract| 7 3) (_ bv0 8))");
+      smt_bit_vector_constant_termt{0, 8})) == "((_ extract 7 3) (_ bv0 8))");
 }
 
 TEST_CASE(
@@ -55,7 +55,7 @@ TEST_CASE(
   {
     CHECK(
       smt_to_smt2_string(smt_identifier_termt{"abc", smt_bool_sortt{}}) ==
-      "|abc|");
+      "abc");
     CHECK(
       smt_to_smt2_string(smt_identifier_termt{"\\", smt_bool_sortt{}}) ==
       "|&92;|");
@@ -67,7 +67,7 @@ TEST_CASE(
         "foo",
         smt_bool_sortt{},
         {smt_symbol_indext{"bar"}, smt_numeral_indext{42}}}) ==
-      "(_ |foo| |bar| 42)");
+      "(_ foo bar 42)");
   }
 }
 
@@ -78,8 +78,7 @@ TEST_CASE(
   CHECK(
     smt_to_smt2_string(smt_core_theoryt::equal(
       smt_identifier_termt{"foo", smt_bit_vector_sortt{32}},
-      smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})) ==
-    "(|=| |foo| |bar|)");
+      smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})) == "(= foo bar)");
 }
 
 TEST_CASE(
@@ -102,7 +101,7 @@ TEST_CASE(
 {
   CHECK(
     smt_to_smt2_string(smt_get_value_commandt{
-      smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value (|foo|))");
+      smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value (foo))");
 }
 
 TEST_CASE(
@@ -138,7 +137,7 @@ TEST_CASE(
     smt_to_smt2_string(smt_declare_function_commandt{
       smt_identifier_termt{"f", smt_bit_vector_sortt{31}},
       {smt_bit_vector_sortt{32}, smt_bit_vector_sortt{33}}}) ==
-    "(declare-fun |f| ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))");
+    "(declare-fun f ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))");
 }
 
 TEST_CASE(
@@ -151,8 +150,8 @@ TEST_CASE(
   CHECK(
     smt_to_smt2_string(smt_define_function_commandt{
       "f", {g, h}, smt_core_theoryt::equal(g, h)}) ==
-    "(define-fun |f| ((|g| (_ BitVec 32)) (|h| (_ BitVec 32))) Bool (|=| |g| "
-    "|h|))");
+    "(define-fun f ((g (_ BitVec 32)) (h (_ BitVec 32))) Bool (= g "
+    "h))");
 }
 
 TEST_CASE(