SMT2 backend: move quoting into convert_identifier

kroening · kroening · commit c594d0790ca4 · 2022-06-16T18:32:14.000+01:00
The quotes |...| are now added in one place by convert_identifier, instead
of asking all consumers of identifiers to do this.
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -218,7 +218,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 +260,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 +837,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 +875,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);
   }
 }
 
@@ -906,7 +910,7 @@ std::string smt2_convt::convert_identifier(const irep_idt &identifier)
   // 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++)
   {
@@ -928,6 +932,8 @@ std::string smt2_convt::convert_identifier(const irep_idt &identifier)
     }
   }
 
+  result += '|';
+
   return result;
 }
 
@@ -989,7 +995,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 +1009,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 +1029,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 +2155,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 +4625,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 +4809,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 +4988,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 +5023,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)
     {
diff --git a/src/solvers/smt2/smt2_dec.cpp b/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
diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp b/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
diff --git a/unit/solvers/smt2/smt2_conv.cpp b/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;");
+    "|" + no_escaping_characters + "|");
+  CHECK(smt2_convt::convert_identifier("\\") == "|&92;|");
+  CHECK(smt2_convt::convert_identifier("|") == "|&124;|");
+  CHECK(smt2_convt::convert_identifier("&") == "|&38;|");
 }

Original file line number	Diff line number	Diff line change
`@@ -218,7 +218,7 @@ void smt2_convt::write_footer()`
`218`	`218`	`if(solver!=solvert::BOOLECTOR)`
`219`	`219`	`{`
`220`	`220`	`for(const auto &id : smt2_identifiers)`
`221`		`- out << "(get-value (\|" << id << "\|))"`
	`221`	`+ out << "(get-value (" << id << "))"`
`222`	`222`	`<< "\n";`
`223`	`223`	`}`
`224`	`224`
`@@ -260,7 +260,7 @@ void smt2_convt::define_object_size(`
`260`	`260`	`<< "((_ extract " << h << " " << l << ") ";`
`261`	`261`	`convert_expr(ptr);`
`262`	`262`	`out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"`
`263`		`- << "(= \|" << id << "\| (_ bv" << *object_size << " " << size_width`
	`263`	`+ << "(= " << id << " (_ bv" << *object_size << " " << size_width`
`264`	`264`	`<< "))))\n";`
`265`	`265`
`266`	`266`	`++number;`
`@@ -837,16 +837,17 @@ literalt smt2_convt::convert(const exprt &expr)`
`837`	`837`	`out << " () Bool)\n";`
`838`	`838`	`out << "(assert (= ";`
`839`	`839`	`convert_literal(l);`
	`840`	`+ out << ' ';`
`840`	`841`	`convert_expr(prepared_expr);`
`841`	`842`	`out << "))\n";`
`842`	`843`	`}`
`843`	`844`	`else`
`844`	`845`	`{`
`845`		`- defined_expressions[expr] =`
`846`		`- std::string{"\|B"} + std::to_string(l.var_no()) + "\|";`
`847`		`- out << "(define-fun ";`
`848`		`- convert_literal(l);`
`849`		`- out << " () Bool ";`
	`846`	`+ auto identifier =`
	`847`	`+ convert_identifier(std::string{"B"} + std::to_string(l.var_no()));`
	`848`	`+ defined_expressions[expr] = identifier;`
	`849`	`+ smt2_identifiers.insert(identifier);`
	`850`	`+ out << "(define-fun " << identifier << " () Bool ";`
`850`	`851`	`convert_expr(prepared_expr);`
`851`	`852`	`out << ")\n";`
`852`	`853`	`}`
`@@ -874,12 +875,15 @@ void smt2_convt::convert_literal(const literalt l)`
`874`	`875`	`if(l.sign())`
`875`	`876`	`out << "(not ";`
`876`	`877`
`877`		`- out << "\|B" << l.var_no() << "\|";`
	`878`	`+ const auto identifier =`
	`879`	`+ convert_identifier("B" + std::to_string(l.var_no()));`
	`880`	`+`
	`881`	`+ out << identifier;`
`878`	`882`
`879`	`883`	`if(l.sign())`
`880`	`884`	`out << ")";`
`881`	`885`
`882`		`- smt2_identifiers.insert("B"+std::to_string(l.var_no()));`
	`886`	`+ smt2_identifiers.insert(identifier);`
`883`	`887`	`}`
`884`	`888`	`}`
`885`	`889`
`@@ -906,7 +910,7 @@ std::string smt2_convt::convert_identifier(const irep_idt &identifier)`
`906`	`910`	`// Otherwise, for Common Lisp compatibility they would have to be treated`
`907`	`911`	`// as escaping symbols.`
`908`	`912`
`909`		`- std::string result;`
	`913`	`+ std::string result = "\|";`
`910`	`914`
`911`	`915`	`for(std::size_t i=0; i<identifier.size(); i++)`
`912`	`916`	`{`
`@@ -928,6 +932,8 @@ std::string smt2_convt::convert_identifier(const irep_idt &identifier)`
`928`	`932`	`}`
`929`	`933`	`}`
`930`	`934`
	`935`	`+ result += '\|';`
	`936`	`+`
`931`	`937`	`return result;`
`932`	`938`	`}`
`933`	`939`
`@@ -989,7 +995,7 @@ void smt2_convt::convert_floatbv(const exprt &expr)`
`989`	`995`	`if(expr.id()==ID_symbol)`
`990`	`996`	`{`
`991`	`997`	`const irep_idt &id = to_symbol_expr(expr).get_identifier();`
`992`		`- out << '\|' << convert_identifier(id) << '\|';`
	`998`	`+ out << convert_identifier(id);`
`993`	`999`	`return;`
`994`	`1000`	`}`
`995`	`1001`
`@@ -1003,9 +1009,9 @@ void smt2_convt::convert_floatbv(const exprt &expr)`
`1003`	`1009`	`INVARIANT(`
`1004`	`1010`	`!expr.operands().empty(), "non-symbol expressions shall have operands");`
`1005`	`1011`
`1006`		`- out << "(\|float_bv." << expr.id()`
`1007`		`- << floatbv_suffix(expr)`
`1008`		`- << '\|';`
	`1012`	`+ out << '('`
	`1013`	`+ << convert_identifier(`
	`1014`	`+ "float_bv." + expr.id_string() + floatbv_suffix(expr));`
`1009`	`1015`
`1010`	`1016`	`forall_operands(it, expr)`
`1011`	`1017`	`{`
`@@ -1023,13 +1029,13 @@ void smt2_convt::convert_expr(const exprt &expr)`
`1023`	`1029`	`{`
`1024`	`1030`	`const irep_idt &id = to_symbol_expr(expr).get_identifier();`
`1025`	`1031`	`DATA_INVARIANT(!id.empty(), "symbol must have identifier");`
`1026`		`- out << '\|' << convert_identifier(id) << '\|';`
	`1032`	`+ out << convert_identifier(id);`
`1027`	`1033`	`}`
`1028`	`1034`	`else if(expr.id()==ID_nondet_symbol)`
`1029`	`1035`	`{`
`1030`	`1036`	`const irep_idt &id = to_nondet_symbol_expr(expr).get_identifier();`
`1031`	`1037`	`DATA_INVARIANT(!id.empty(), "nondet symbol must have identifier");`
`1032`		`- out << '\|' << convert_identifier("nondet_"+id2string(id)) << '\|';`
	`1038`	`+ out << convert_identifier("nondet_" + id2string(id));`
`1033`	`1039`	`}`
`1034`	`1040`	`else if(expr.id()==ID_smt2_symbol)`
`1035`	`1041`	`{`
`@@ -2149,7 +2155,7 @@ void smt2_convt::convert_expr(const exprt &expr)`
`2149`	`2155`	`else if(`
`2150`	`2156`	`const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))`
`2151`	`2157`	`{`
`2152`		`- out << "\|" << object_sizes[*object_size] << "\|";`
	`2158`	`+ out << object_sizes[*object_size];`
`2153`	`2159`	`}`
`2154`	`2160`	`else if(expr.id()==ID_let)`
`2155`	`2161`	`{`
`@@ -4619,7 +4625,7 @@ void smt2_convt::set_to(const exprt &expr, bool value)`
`4619`	`4625`	`smt2_identifiers.insert(smt2_identifier);`
`4620`	`4626`
`4621`	`4627`	`out << "; set_to true (equal)\n";`
`4622`		`- out << "(define-fun \|" << smt2_identifier << '\|';`
	`4628`	`+ out << "(define-fun " << smt2_identifier;`
`4623`	`4629`
`4624`	`4630`	`if(equal_expr.lhs().type().id() == ID_mathematical_function)`
`4625`	`4631`	`{`
`@@ -4803,7 +4809,7 @@ void smt2_convt::find_symbols(const exprt &expr)`
`4803`	`4809`	`smt2_identifiers.insert(smt2_identifier);`
`4804`	`4810`
`4805`	`4811`	`out << "; find_symbols\n";`
`4806`		`- out << "(declare-fun \|" << smt2_identifier << '\|';`
	`4812`	`+ out << "(declare-fun " << smt2_identifier;`
`4807`	`4813`
`4808`	`4814`	`if(expr.type().id() == ID_mathematical_function)`
`4809`	`4815`	`{`
`@@ -4982,8 +4988,9 @@ void smt2_convt::find_symbols(const exprt &expr)`
`4982`	`4988`	`{`
`4983`	`4989`	`if(object_sizes.find(*object_size) == object_sizes.end())`
`4984`	`4990`	`{`
`4985`		`- const irep_idt id = "object_size." + std::to_string(object_sizes.size());`
`4986`		`- out << "(declare-fun \|" << id << "\| () ";`
	`4991`	`+ const irep_idt id = convert_identifier(`
	`4992`	`+ "object_size." + std::to_string(object_sizes.size()));`
	`4993`	`+ out << "(declare-fun " << id << " () ";`
`4987`	`4994`	`convert_type(object_size->type());`
`4988`	`4995`	`out << ")"`
`4989`	`4996`	`<< "\n";`
`@@ -5016,8 +5023,8 @@ void smt2_convt::find_symbols(const exprt &expr)`
`5016`	`5023`	`to_multi_ary_expr(expr).op0().type().id() == ID_floatbv)))`
`5017`	`5024`	`// clang-format on`
`5018`	`5025`	`{`
`5019`		`- irep_idt function=`
`5020`		`- "\|float_bv."+expr.id_string()+floatbv_suffix(expr)+"\|";`
	`5026`	`+ irep_idt function =`
	`5027`	`+ convert_identifier("float_bv." + expr.id_string() + floatbv_suffix(expr));`
`5021`	`5028`
`5022`	`5029`	`if(bvfp_set.insert(function).second)`
`5023`	`5030`	`{`
Original file line number	Diff line number	Diff line change
`@@ -19,7 +19,7 @@`
`19`	`19`
`20`	`20`	`static std::string escape_identifier(const irep_idt &identifier)`
`21`	`21`	`{`
`22`		`- return std::string{"\|"} + smt2_convt::convert_identifier(identifier) + "\|";`
	`22`	`+ return smt2_convt::convert_identifier(identifier);`
`23`	`23`	`}`
`24`	`24`
`25`	`25`	`class smt_index_output_visitort : public smt_index_const_downcast_visitort`