smt2_solver: implement (echo "string")

Author: Daniel Kroening

src/solvers/smt2/smt2_solver.cpp

@@ -47,6 +47,22 @@ class smt2_solvert:public smt2_parsert
   } status;
 };
 
+static std::string smt2_string_literal(const std::string &s)
+{
+  // " is the only escape sequence
+  std::string result;
+  result += '"';
+
+  for(const auto &c : s)
+    if(c == '"')
+      result += "\"\"";
+    else
+      result += c;
+
+  result += '"';
+  return result;
+}
+
 void smt2_solvert::define_constants(const exprt &expr)
 {
   for(const auto &op : expr.operands())
@@ -228,6 +244,13 @@ void smt2_solvert::command(const std::string &c)
 
       std::cout << ")\n";
     }
+    else if(c == "echo")
+    {
+      if(next_token() != STRING_LITERAL)
+        std::cout << "expected string literal" << '\n';
+      else
+        std::cout << smt2_string_literal(buffer) << '\n';
+    }
     else if(c=="simplify")
     {
       // this is a command that Z3 appears to implement
@@ -251,8 +274,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 )