smt2_solver: implement (echo "string")

regression/smt2_solver/echo/echo1.desc

@@ -0,0 +1,9 @@
+CORE
+echo1.smt2
+
+^EXIT=20$
+^SIGNAL=0$
+\(error "line 2: expected string literal"\)
+"whatnot"
+"what""not"
+--

regression/smt2_solver/echo/echo1.smt2

@@ -0,0 +1,9 @@
+; error: must be string literal
+(echo 123)
+
+; ok
+(echo "whatnot")
+
+; with escaping
+(echo "what""not")
+

src/solvers/smt2/smt2_format.cpp

@@ -57,6 +57,23 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
     {
       out << value;
     }
+    else if(expr_type.id() == ID_string)
+    {
+      const auto &value_string = id2string(value);
+
+      out << '"';
+
+      for(const auto &c : value_string)
+      {
+        // " is the only escape sequence
+        if(c == '"')
+          out << '"' << '"';
+        else
+          out << c;
+      }
+
+      out << '"';
+    }
     else
       DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string());
   }

src/solvers/smt2/smt2_solver.cpp

@@ -225,6 +225,13 @@ void smt2_solvert::command(const std::string &c)
 
       std::cout << ")\n";
     }
+    else if(c == "echo")
+    {
+      if(next_token() != STRING_LITERAL)
+        throw error("expected string literal");
+
+      std::cout << smt2_format(constant_exprt(buffer, string_typet())) << '\n';
+    }
     else if(c == "simplify")
     {
       // this is a command that Z3 appears to implement
@@ -248,8 +255,6 @@ void smt2_solvert::command(const std::string &c)
     | ( define-fun-rec hfunction_def i )
     | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
     | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
-    | ( echo hstringi )
-    | ( exit )
     | ( get-assertions )
     | ( get-assignment )
     | ( get-info hinfo_flag i )