Merge pull request #6388 from thomasspriggs/tas/comment-regex

Address incremental SMT2 related code review comments from PR6357

Author: TGWDB

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -49,7 +49,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         return expr_identifier.first;
       });
   std::stack<exprt> to_be_defined;
-  const auto dependencies_needed = [&](const exprt &expr) {
+  const auto push_dependencies_needed = [&](const exprt &expr) {
     bool result = false;
     for(const auto &dependency : gather_dependent_expressions(expr))
     {
@@ -60,11 +60,11 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
     }
     return result;
   };
-  dependencies_needed(expr);
+  push_dependencies_needed(expr);
   while(!to_be_defined.empty())
   {
     const exprt current = to_be_defined.top();
-    if(dependencies_needed(current))
+    if(push_dependencies_needed(current))
       continue;
     if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
     {
@@ -81,7 +81,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
       }
       else
       {
-        if(dependencies_needed(symbol->value))
+        if(push_dependencies_needed(symbol->value))
           continue;
         const smt_define_function_commandt function{
           symbol->name, {}, convert_expr_to_smt(symbol->value)};

src/solvers/smt2_incremental/smt_terms.cpp

@@ -50,13 +50,19 @@ bool smt_bool_literal_termt::value() const
 
 static bool is_valid_smt_identifier(irep_idt identifier)
 {
-  static const std::regex valid{R"(^[^\|]*$)"};
+  // The below regex matches a complete string which does not contain the `|`
+  // character. So it would match the string `foo bar`, but not `|foo bar|`.
+  static const std::regex valid{"[^\\|]*"};
   return std::regex_match(id2string(identifier), valid);
 }
 
 smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort)
   : smt_termt(ID_smt_identifier_term, std::move(sort))
 {
+  // The below invariant exists as a sanity check that the string being used for
+  // the identifier is in unescaped form. This is because the escaping and
+  // unescaping are implementation details of the printing to string and
+  // response parsing respectively, not part of the underlying data.
   INVARIANT(
     is_valid_smt_identifier(identifier),
     R"(Identifiers may not contain | characters.)");