Merge pull request #6940 from diffblue/smt2-simple-symbol

SMT2 backend: generate simple symbols

Author: tautschnig

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
@@ -218,7 +220,7 @@ void smt2_convt::write_footer()
   if(solver!=solvert::BOOLECTOR)
   {
     for(const auto &id : smt2_identifiers)
-      out << "(get-value (|" << id << "|))"
+      out << "(get-value (" << id << "))"
           << "\n";
   }
 
@@ -260,7 +262,7 @@ void smt2_convt::define_object_size(
         << "((_ extract " << h << " " << l << ") ";
     convert_expr(ptr);
     out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
-        << "(= |" << id << "| (_ bv" << *object_size << " " << size_width
+        << "(= " << id << " (_ bv" << *object_size << " " << size_width
         << "))))\n";
 
     ++number;
@@ -837,16 +839,17 @@ literalt smt2_convt::convert(const exprt &expr)
     out << " () Bool)\n";
     out << "(assert (= ";
     convert_literal(l);
+    out << ' ';
     convert_expr(prepared_expr);
     out << "))\n";
   }
   else
   {
-    defined_expressions[expr] =
-      std::string{"|B"} + std::to_string(l.var_no()) + "|";
-    out << "(define-fun ";
-    convert_literal(l);
-    out << " () Bool ";
+    auto identifier =
+      convert_identifier(std::string{"B"} + std::to_string(l.var_no()));
+    defined_expressions[expr] = identifier;
+    smt2_identifiers.insert(identifier);
+    out << "(define-fun " << identifier << " () Bool ";
     convert_expr(prepared_expr);
     out << ")\n";
   }
@@ -874,12 +877,15 @@ void smt2_convt::convert_literal(const literalt l)
     if(l.sign())
       out << "(not ";
 
-    out << "|B" << l.var_no() << "|";
+    const auto identifier =
+      convert_identifier("B" + std::to_string(l.var_no()));
+
+    out << identifier;
 
     if(l.sign())
       out << ")";
 
-    smt2_identifiers.insert("B"+std::to_string(l.var_no()));
+    smt2_identifiers.insert(identifier);
   }
 }
 
@@ -900,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;
+  std::string result = "|";
 
-  for(std::size_t i=0; i<identifier.size(); i++)
+  for(auto ch : identifier)
   {
-    char ch=identifier[i];
-
     switch(ch)
     {
     case '|':
@@ -928,6 +953,8 @@ std::string smt2_convt::convert_identifier(const irep_idt &identifier)
     }
   }
 
+  result += '|';
+
   return result;
 }
 
@@ -989,7 +1016,7 @@ void smt2_convt::convert_floatbv(const exprt &expr)
   if(expr.id()==ID_symbol)
   {
     const irep_idt &id = to_symbol_expr(expr).get_identifier();
-    out << '|' << convert_identifier(id) << '|';
+    out << convert_identifier(id);
     return;
   }
 
@@ -1003,9 +1030,9 @@ void smt2_convt::convert_floatbv(const exprt &expr)
   INVARIANT(
     !expr.operands().empty(), "non-symbol expressions shall have operands");
 
-  out << "(|float_bv." << expr.id()
-      << floatbv_suffix(expr)
-      << '|';
+  out << '('
+      << convert_identifier(
+           "float_bv." + expr.id_string() + floatbv_suffix(expr));
 
   forall_operands(it, expr)
   {
@@ -1023,13 +1050,13 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     const irep_idt &id = to_symbol_expr(expr).get_identifier();
     DATA_INVARIANT(!id.empty(), "symbol must have identifier");
-    out << '|' << convert_identifier(id) << '|';
+    out << convert_identifier(id);
   }
   else if(expr.id()==ID_nondet_symbol)
   {
     const irep_idt &id = to_nondet_symbol_expr(expr).get_identifier();
     DATA_INVARIANT(!id.empty(), "nondet symbol must have identifier");
-    out << '|' << convert_identifier("nondet_"+id2string(id)) << '|';
+    out << convert_identifier("nondet_" + id2string(id));
   }
   else if(expr.id()==ID_smt2_symbol)
   {
@@ -2149,7 +2176,7 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(
     const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
   {
-    out << "|" << object_sizes[*object_size] << "|";
+    out << object_sizes[*object_size];
   }
   else if(expr.id()==ID_let)
   {
@@ -4619,7 +4646,7 @@ void smt2_convt::set_to(const exprt &expr, bool value)
         smt2_identifiers.insert(smt2_identifier);
 
         out << "; set_to true (equal)\n";
-        out << "(define-fun |" << smt2_identifier << '|';
+        out << "(define-fun " << smt2_identifier;
 
         if(equal_expr.lhs().type().id() == ID_mathematical_function)
         {
@@ -4803,7 +4830,7 @@ void smt2_convt::find_symbols(const exprt &expr)
       smt2_identifiers.insert(smt2_identifier);
 
       out << "; find_symbols\n";
-      out << "(declare-fun |" << smt2_identifier << '|';
+      out << "(declare-fun " << smt2_identifier;
 
       if(expr.type().id() == ID_mathematical_function)
       {
@@ -4982,8 +5009,9 @@ void smt2_convt::find_symbols(const exprt &expr)
   {
     if(object_sizes.find(*object_size) == object_sizes.end())
     {
-      const irep_idt id = "object_size." + std::to_string(object_sizes.size());
-      out << "(declare-fun |" << id << "| () ";
+      const irep_idt id = convert_identifier(
+        "object_size." + std::to_string(object_sizes.size()));
+      out << "(declare-fun " << id << " () ";
       convert_type(object_size->type());
       out << ")"
           << "\n";
@@ -5016,8 +5044,8 @@ void smt2_convt::find_symbols(const exprt &expr)
              to_multi_ary_expr(expr).op0().type().id() == ID_floatbv)))
   // clang-format on
   {
-    irep_idt function=
-      "|float_bv."+expr.id_string()+floatbv_suffix(expr)+"|";
+    irep_idt function =
+      convert_identifier("float_bv." + expr.id_string() + floatbv_suffix(expr));
 
     if(bvfp_set.insert(function).second)
     {

src/solvers/smt2/smt2_dec.cpp

@@ -130,6 +130,14 @@ decision_proceduret::resultt smt2_dect::dec_solve()
   return read_result(in);
 }
 
+static std::string drop_quotes(std::string src)
+{
+  if(src.size() >= 2 && src.front() == '|' && src.back() == '|')
+    return std::string(src, 1, src.size() - 2);
+  else
+    return src;
+}
+
 decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
 {
   std::string line;
@@ -199,22 +207,25 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
 
   for(auto &assignment : identifier_map)
   {
-    std::string conv_id = convert_identifier(assignment.first);
+    std::string conv_id = drop_quotes(convert_identifier(assignment.first));
     const irept &value = parsed_values[conv_id];
     assignment.second.value = parse_rec(value, assignment.second.type);
   }
 
   // Booleans
   for(unsigned v=0; v<no_boolean_variables; v++)
   {
-    const std::string boolean_identifier = "B" + std::to_string(v);
+    const std::string boolean_identifier =
+      convert_identifier("B" + std::to_string(v));
     boolean_assignment[v] = [&]() {
-      const auto found_parsed_value = parsed_values.find(boolean_identifier);
+      const auto found_parsed_value =
+        parsed_values.find(drop_quotes(boolean_identifier));
       if(found_parsed_value != parsed_values.end())
+      {
         return found_parsed_value->second.id() == ID_true;
+      }
       // Work out the value based on what set_to was called with.
-      const auto found_set_value =
-        set_values.find('|' + boolean_identifier + '|');
+      const auto found_set_value = set_values.find(boolean_identifier);
       if(found_set_value != set_values.end())
         return found_set_value->second;
       // Old code used the computation

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

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -19,7 +19,7 @@
 
 static std::string escape_identifier(const irep_idt &identifier)
 {
-  return std::string{"|"} + smt2_convt::convert_identifier(identifier) + "|";
+  return smt2_convt::convert_identifier(identifier);
 }
 
 class smt_index_output_visitort : public smt_index_const_downcast_visitort

unit/solvers/smt2/smt2_conv.cpp

@@ -8,11 +8,12 @@ TEST_CASE(
   "smt2_convt::convert_identifier character escaping.",
   "[core][solvers][smt2]")
 {
-  const auto no_escaping_characters = "abcdefghijklmnopqrstuvwxyz0123456789$";
+  const std::string no_escaping_characters =
+    "abcdefghijklmnopqrstuvwxyz0123456789$";
   CHECK(
     smt2_convt::convert_identifier(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("\\") == "|&92;|");
+  CHECK(smt2_convt::convert_identifier("|") == "|&124;|");
+  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(