smt2_solver: implement (echo "string")

Author: Daniel Kroening

src/solvers/smt2/smt2_solver.cpp

@@ -41,6 +41,22 @@ class smt2_solvert:public smt2_parsert
   std::set<irep_idt> constants_done;
 };
 
+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())
@@ -162,6 +178,13 @@ void smt2_solvert::command(const std::string &c)
         std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
       }
     }
+    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
@@ -185,8 +208,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 )