Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/printer/ast/ast_printer.cpp	Lines:	50	215	23.3 %
Date:	2021-09-30	Branches:	51	250	20.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Abdalrhman Mohamed, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The pretty-printer interface for the AST output language.
 */
#include "printer/ast/ast_printer.h"

#include <iostream>
#include <string>
#include <typeinfo>
#include <vector>

#include "expr/node_manager_attributes.h"  // for VarNameAttr
#include "expr/node_visitor.h"
#include "options/language.h"  // for LANG_AST
#include "printer/let_binding.h"
#include "smt/command.h"
#include "smt/node_command.h"

using namespace std;

namespace cvc5 {
namespace printer {
namespace ast {

void AstPrinter::toStream(std::ostream& out,
                          TNode n,
                          int toDepth,
                          size_t dag) const
{
  if(dag != 0) {
    LetBinding lbind(dag + 1);
    toStreamWithLetify(out, n, toDepth, &lbind);
  } else {
    toStream(out, n, toDepth);
  }
}

void AstPrinter::toStream(std::ostream& out,
                          TNode n,
                          int toDepth,
                          LetBinding* lbind) const
{
  // null
  if(n.getKind() == kind::NULL_EXPR) {
    out << "null";
    return;
  }

  // variable
  if(n.getMetaKind() == kind::metakind::VARIABLE) {
    string s;
    if(n.getAttribute(expr::VarNameAttr(), s)) {
      out << s;
    } else {
      out << "var_" << n.getId();
    }
    return;
  }

  out << '(' << n.getKind();
  if(n.getMetaKind() == kind::metakind::CONSTANT) {
    // constant
    out << ' ';
    kind::metakind::NodeValueConstPrinter::toStream(out, n);
  }
  else if (n.isClosure())
  {
    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
    {
      // body is re-letified
      if (i == 1)
      {
        toStreamWithLetify(out, n[i], toDepth, lbind);
        continue;
      }
      toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - 1, lbind);
    }
  }
  else
  {
    // operator
    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
      out << ' ';
      if(toDepth != 0) {
        toStream(
            out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
      } else {
        out << "(...)";
      }
    }
    for(TNode::iterator i = n.begin(),
          iend = n.end();
        i != iend;
        ++i) {
      if(i != iend) {
        out << ' ';
      }
      if(toDepth != 0) {
        toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, lbind);
      } else {
        out << "(...)";
      }
    }
  }
  out << ')';
}/* AstPrinter::toStream(TNode) */

template <class T>
static bool tryToStream(std::ostream& out, const Command* c);

template <class T>
static bool tryToStream(std::ostream& out, const CommandStatus* s);

void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const
{
  if(tryToStream<CommandSuccess>(out, s) ||
     tryToStream<CommandFailure>(out, s) ||
     tryToStream<CommandUnsupported>(out, s) ||
     tryToStream<CommandInterrupted>(out, s)) {
    return;
  }

  out << "ERROR: don't know how to print a CommandStatus of class: "
      << typeid(*s).name() << endl;

}/* AstPrinter::toStream(CommandStatus*) */

void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const
{
  out << "Model()";
}

void AstPrinter::toStreamModelSort(std::ostream& out,
                                   TypeNode tn,
                                   const std::vector<Node>& elements) const
{
  // shouldn't be called; only the non-Command* version above should be
  Unreachable();
}

void AstPrinter::toStreamModelTerm(std::ostream& out,
                                   const Node& n,
                                   const Node& value) const
{
  // shouldn't be called; only the non-Command* version above should be
  Unreachable();
}

void AstPrinter::toStreamCmdEmpty(std::ostream& out,
                                  const std::string& name) const
{
  out << "EmptyCommand(" << name << ')' << std::endl;
}

void AstPrinter::toStreamCmdEcho(std::ostream& out,
                                 const std::string& output) const
{
  out << "EchoCommand(" << output << ')' << std::endl;
}

void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
{
  out << "Assert(" << n << ')' << std::endl;
}

void AstPrinter::toStreamCmdPush(std::ostream& out) const
{
  out << "Push()" << std::endl;
}

void AstPrinter::toStreamCmdPop(std::ostream& out) const {
  out << "Pop()" << std::endl;
}

void AstPrinter::toStreamCmdCheckSat(std::ostream& out) const
{
  out << "CheckSat()" << std::endl;
}

void AstPrinter::toStreamCmdCheckSatAssuming(
    std::ostream& out, const std::vector<Node>& nodes) const
{
  out << "CheckSatAssuming( << ";
  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
  out << ">> )" << std::endl;
}

void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
{
  out << "Query(" << n << ')' << std::endl;
}

void AstPrinter::toStreamCmdReset(std::ostream& out) const
{
  out << "Reset()" << std::endl;
}

void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
{
  out << "ResetAssertions()" << std::endl;
}

void AstPrinter::toStreamCmdQuit(std::ostream& out) const
{
  out << "Quit()" << std::endl;
}

void AstPrinter::toStreamCmdDeclarationSequence(
    std::ostream& out, const std::vector<Command*>& sequence) const
{
  out << "DeclarationSequence[" << endl;
  for (CommandSequence::const_iterator i = sequence.cbegin();
       i != sequence.cend();
       ++i)
  {
    out << *i << endl;
  }
  out << "]" << std::endl;
}

void AstPrinter::toStreamCmdCommandSequence(
    std::ostream& out, const std::vector<Command*>& sequence) const
{
  out << "CommandSequence[" << endl;
  for (CommandSequence::const_iterator i = sequence.cbegin();
       i != sequence.cend();
       ++i)
  {
    out << *i << endl;
  }
  out << "]" << std::endl;
}

void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
                                            const std::string& id,
                                            TypeNode type) const
{
  out << "Declare(" << id << "," << type << ')' << std::endl;
}

void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
                                           const std::string& id,
                                           const std::vector<Node>& formals,
                                           TypeNode range,
                                           Node formula) const
{
  out << "DefineFunction( \"" << id << "\", [";
  if (formals.size() > 0)
  {
    copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
    out << formals.back();
  }
  out << "], << " << formula << " >> )" << std::endl;
}

void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
                                        TypeNode type) const
{
  out << "DeclareType(" << type << ')' << std::endl;
}

void AstPrinter::toStreamCmdDefineType(std::ostream& out,
                                       const std::string& id,
                                       const std::vector<TypeNode>& params,
                                       TypeNode t) const
{
  out << "DefineType(" << id << ",[";
  if (params.size() > 0)
  {
    copy(params.begin(),
         params.end() - 1,
         ostream_iterator<TypeNode>(out, ", "));
    out << params.back();
  }
  out << "]," << t << ')' << std::endl;
}

void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
  out << "Simplify( << " << n << " >> )" << std::endl;
}

void AstPrinter::toStreamCmdGetValue(std::ostream& out,
                                     const std::vector<Node>& nodes) const
{
  out << "GetValue( << ";
  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
  out << ">> )" << std::endl;
}

void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
{
  out << "GetModel()" << std::endl;
}

void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
{
  out << "GetAssignment()" << std::endl;
}

void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
{
  out << "GetAssertions()" << std::endl;
}

void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
{
  out << "GetProof()" << std::endl;
}

void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
{
  out << "GetUnsatCore()" << std::endl;
}

void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                              const std::string& logic) const
{
  out << "SetBenchmarkLogic(" << logic << ')' << std::endl;
}

void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
                                    const std::string& flag,
                                    const std::string& value) const
{
  out << "SetInfo(" << flag << ", " << value << ')' << std::endl;
}

void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
                                    const std::string& flag) const
{
  out << "GetInfo(" << flag << ')' << std::endl;
}

void AstPrinter::toStreamCmdSetOption(std::ostream& out,
                                      const std::string& flag,
                                      const std::string& value) const
{
  out << "SetOption(" << flag << ", " << value << ')' << std::endl;
}

void AstPrinter::toStreamCmdGetOption(std::ostream& out,
                                      const std::string& flag) const
{
  out << "GetOption(" << flag << ')' << std::endl;
}

void AstPrinter::toStreamCmdDatatypeDeclaration(
    std::ostream& out, const std::vector<TypeNode>& datatypes) const
{
  out << "DatatypeDeclarationCommand([";
  for (const TypeNode& t : datatypes)
  {
    out << t << ";" << endl;
  }
  out << "])" << std::endl;
}

void AstPrinter::toStreamWithLetify(std::ostream& out,
                                    Node n,
                                    int toDepth,
                                    LetBinding* lbind) const
{
  if (lbind == nullptr)
  {
    toStream(out, n, toDepth);
    return;
  }
  std::stringstream cparen;
  std::vector<Node> letList;
  lbind->letify(n, letList);
  if (!letList.empty())
  {
    std::map<Node, uint32_t>::const_iterator it;
    out << "(LET ";
    cparen << ")";
    bool first = true;
    for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
    {
      if (!first)
      {
        out << ", ";
      }
      else
      {
        first = false;
      }
      Node nl = letList[i];
      uint32_t id = lbind->getId(nl);
      out << "_let_" << id << " := ";
      Node nlc = lbind->convert(nl, "_let_", false);
      toStream(out, nlc, toDepth, lbind);
    }
    out << " IN ";
  }
  Node nc = lbind->convert(n, "_let_");
  // print the body, passing the lbind object
  toStream(out, nc, toDepth, lbind);
  out << cparen.str();
  lbind->popScope();
}

template <class T>
static bool tryToStream(std::ostream& out, const Command* c)
{
  if(typeid(*c) == typeid(T)) {
    toStream(out, dynamic_cast<const T*>(c));
    return true;
  }
  return false;
}

static void toStream(std::ostream& out, const CommandSuccess* s)
{
  if(Command::printsuccess::getPrintSuccess(out)) {
    out << "OK" << endl;
  }
}

static void toStream(std::ostream& out, const CommandInterrupted* s)
{
  out << "INTERRUPTED" << endl;
}

static void toStream(std::ostream& out, const CommandUnsupported* s)
{
  out << "UNSUPPORTED" << endl;
}

static void toStream(std::ostream& out, const CommandFailure* s)
{
  out << s->getMessage() << endl;
}

template <class T>
static bool tryToStream(std::ostream& out, const CommandStatus* s)
{
  if(typeid(*s) == typeid(T)) {
    toStream(out, dynamic_cast<const T*>(s));
    return true;
  }
  return false;
}

}  // namespace ast
}  // namespace printer
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Abdalrhman Mohamed, Andrew Reynolds
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* The pretty-printer interface for the AST output language.
14		*/
15		#include "printer/ast/ast_printer.h"
16
17		#include <iostream>
18		#include <string>
19		#include <typeinfo>
20		#include <vector>
21
22		#include "expr/node_manager_attributes.h" // for VarNameAttr
23		#include "expr/node_visitor.h"
24		#include "options/language.h" // for LANG_AST
25		#include "printer/let_binding.h"
26		#include "smt/command.h"
27		#include "smt/node_command.h"
28
29		using namespace std;
30
31		namespace cvc5 {
32		namespace printer {
33		namespace ast {
34
35	27	void AstPrinter::toStream(std::ostream& out,
36		TNode n,
37		int toDepth,
38		size_t dag) const
39		{
40	27	if(dag != 0) {
41	4	LetBinding lbind(dag + 1);
42	2	toStreamWithLetify(out, n, toDepth, &lbind);
43		} else {
44	25	toStream(out, n, toDepth);
45		}
46	27	}
47
48	215	void AstPrinter::toStream(std::ostream& out,
49		TNode n,
50		int toDepth,
51		LetBinding* lbind) const
52		{
53		// null
54	215	if(n.getKind() == kind::NULL_EXPR) {
55		out << "null";
56		return;
57		}
58
59		// variable
60	215	if(n.getMetaKind() == kind::metakind::VARIABLE) {
61	252	string s;
62	126	if(n.getAttribute(expr::VarNameAttr(), s)) {
63	126	out << s;
64		} else {
65		out << "var_" << n.getId();
66		}
67	126	return;
68		}
69
70	89	out << '(' << n.getKind();
71	89	if(n.getMetaKind() == kind::metakind::CONSTANT) {
72		// constant
73	2	out << ' ';
74	2	kind::metakind::NodeValueConstPrinter::toStream(out, n);
75		}
76	87	else if (n.isClosure())
77		{
78		for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
79		{
80		// body is re-letified
81		if (i == 1)
82		{
83		toStreamWithLetify(out, n[i], toDepth, lbind);
84		continue;
85		}
86		toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - 1, lbind);
87		}
88		}
89		else
90		{
91		// operator
92	87	if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
93		out << ' ';
94		if(toDepth != 0) {
95		toStream(
96		out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
97		} else {
98		out << "(...)";
99		}
100		}
101	299	for(TNode::iterator i = n.begin(),
102	87	iend = n.end();
103	299	i != iend;
104		++i) {
105	212	if(i != iend) {
106	212	out << ' ';
107		}
108	212	if(toDepth != 0) {
109	188	toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, lbind);
110		} else {
111	24	out << "(...)";
112		}
113		}
114		}
115	89	out << ')';
116		}/* AstPrinter::toStream(TNode) */
117
118		template <class T>
119		static bool tryToStream(std::ostream& out, const Command* c);
120
121		template <class T>
122		static bool tryToStream(std::ostream& out, const CommandStatus* s);
123
124	1	void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const
125		{
126	2	if(tryToStream<CommandSuccess>(out, s) \|\|
127		tryToStream<CommandFailure>(out, s) \|\|
128	1	tryToStream<CommandUnsupported>(out, s) \|\|
129		tryToStream<CommandInterrupted>(out, s)) {
130	1	return;
131		}
132
133		out << "ERROR: don't know how to print a CommandStatus of class: "
134		<< typeid(*s).name() << endl;
135
136		}/* AstPrinter::toStream(CommandStatus) /
137
138		void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const
139		{
140		out << "Model()";
141		}
142
143		void AstPrinter::toStreamModelSort(std::ostream& out,
144		TypeNode tn,
145		const std::vector<Node>& elements) const
146		{
147		// shouldn't be called; only the non-Command* version above should be
148		Unreachable();
149		}
150
151		void AstPrinter::toStreamModelTerm(std::ostream& out,
152		const Node& n,
153		const Node& value) const
154		{
155		// shouldn't be called; only the non-Command* version above should be
156		Unreachable();
157		}
158
159		void AstPrinter::toStreamCmdEmpty(std::ostream& out,
160		const std::string& name) const
161		{
162		out << "EmptyCommand(" << name << ')' << std::endl;
163		}
164
165		void AstPrinter::toStreamCmdEcho(std::ostream& out,
166		const std::string& output) const
167		{
168		out << "EchoCommand(" << output << ')' << std::endl;
169		}
170
171		void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
172		{
173		out << "Assert(" << n << ')' << std::endl;
174		}
175
176		void AstPrinter::toStreamCmdPush(std::ostream& out) const
177		{
178		out << "Push()" << std::endl;
179		}
180
181		void AstPrinter::toStreamCmdPop(std::ostream& out) const {
182		out << "Pop()" << std::endl;
183		}
184
185		void AstPrinter::toStreamCmdCheckSat(std::ostream& out) const
186		{
187		out << "CheckSat()" << std::endl;
188		}
189
190		void AstPrinter::toStreamCmdCheckSatAssuming(
191		std::ostream& out, const std::vector<Node>& nodes) const
192		{
193		out << "CheckSatAssuming( << ";
194		copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
195		out << ">> )" << std::endl;
196		}
197
198		void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
199		{
200		out << "Query(" << n << ')' << std::endl;
201		}
202
203		void AstPrinter::toStreamCmdReset(std::ostream& out) const
204		{
205		out << "Reset()" << std::endl;
206		}
207
208		void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
209		{
210		out << "ResetAssertions()" << std::endl;
211		}
212
213		void AstPrinter::toStreamCmdQuit(std::ostream& out) const
214		{
215		out << "Quit()" << std::endl;
216		}
217
218		void AstPrinter::toStreamCmdDeclarationSequence(
219		std::ostream& out, const std::vector<Command*>& sequence) const
220		{
221		out << "DeclarationSequence[" << endl;
222		for (CommandSequence::const_iterator i = sequence.cbegin();
223		i != sequence.cend();
224		++i)
225		{
226		out << *i << endl;
227		}
228		out << "]" << std::endl;
229		}
230
231		void AstPrinter::toStreamCmdCommandSequence(
232		std::ostream& out, const std::vector<Command*>& sequence) const
233		{
234		out << "CommandSequence[" << endl;
235		for (CommandSequence::const_iterator i = sequence.cbegin();
236		i != sequence.cend();
237		++i)
238		{
239		out << *i << endl;
240		}
241		out << "]" << std::endl;
242		}
243
244		void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
245		const std::string& id,
246		TypeNode type) const
247		{
248		out << "Declare(" << id << "," << type << ')' << std::endl;
249		}
250
251		void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
252		const std::string& id,
253		const std::vector<Node>& formals,
254		TypeNode range,
255		Node formula) const
256		{
257		out << "DefineFunction( \"" << id << "\", [";
258		if (formals.size() > 0)
259		{
260		copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
261		out << formals.back();
262		}
263		out << "], << " << formula << " >> )" << std::endl;
264		}
265
266		void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
267		TypeNode type) const
268		{
269		out << "DeclareType(" << type << ')' << std::endl;
270		}
271
272		void AstPrinter::toStreamCmdDefineType(std::ostream& out,
273		const std::string& id,
274		const std::vector<TypeNode>& params,
275		TypeNode t) const
276		{
277		out << "DefineType(" << id << ",[";
278		if (params.size() > 0)
279		{
280		copy(params.begin(),
281		params.end() - 1,
282		ostream_iterator<TypeNode>(out, ", "));
283		out << params.back();
284		}
285		out << "]," << t << ')' << std::endl;
286		}
287
288		void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
289		{
290		out << "Simplify( << " << n << " >> )" << std::endl;
291		}
292
293		void AstPrinter::toStreamCmdGetValue(std::ostream& out,
294		const std::vector<Node>& nodes) const
295		{
296		out << "GetValue( << ";
297		copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
298		out << ">> )" << std::endl;
299		}
300
301		void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
302		{
303		out << "GetModel()" << std::endl;
304		}
305
306		void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
307		{
308		out << "GetAssignment()" << std::endl;
309		}
310
311		void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
312		{
313		out << "GetAssertions()" << std::endl;
314		}
315
316		void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
317		{
318		out << "GetProof()" << std::endl;
319		}
320
321		void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
322		{
323		out << "GetUnsatCore()" << std::endl;
324		}
325
326		void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
327		const std::string& logic) const
328		{
329		out << "SetBenchmarkLogic(" << logic << ')' << std::endl;
330		}
331
332		void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
333		const std::string& flag,
334		const std::string& value) const
335		{
336		out << "SetInfo(" << flag << ", " << value << ')' << std::endl;
337		}
338
339		void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
340		const std::string& flag) const
341		{
342		out << "GetInfo(" << flag << ')' << std::endl;
343		}
344
345		void AstPrinter::toStreamCmdSetOption(std::ostream& out,
346		const std::string& flag,
347		const std::string& value) const
348		{
349		out << "SetOption(" << flag << ", " << value << ')' << std::endl;
350		}
351
352		void AstPrinter::toStreamCmdGetOption(std::ostream& out,
353		const std::string& flag) const
354		{
355		out << "GetOption(" << flag << ')' << std::endl;
356		}
357
358		void AstPrinter::toStreamCmdDatatypeDeclaration(
359		std::ostream& out, const std::vector<TypeNode>& datatypes) const
360		{
361		out << "DatatypeDeclarationCommand([";
362		for (const TypeNode& t : datatypes)
363		{
364		out << t << ";" << endl;
365		}
366		out << "])" << std::endl;
367		}
368
369	2	void AstPrinter::toStreamWithLetify(std::ostream& out,
370		Node n,
371		int toDepth,
372		LetBinding* lbind) const
373		{
374	2	if (lbind == nullptr)
375		{
376		toStream(out, n, toDepth);
377		return;
378		}
379	4	std::stringstream cparen;
380	4	std::vector<Node> letList;
381	2	lbind->letify(n, letList);
382	2	if (!letList.empty())
383		{
384		std::map<Node, uint32_t>::const_iterator it;
385		out << "(LET ";
386		cparen << ")";
387		bool first = true;
388		for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
389		{
390		if (!first)
391		{
392		out << ", ";
393		}
394		else
395		{
396		first = false;
397		}
398		Node nl = letList[i];
399		uint32_t id = lbind->getId(nl);
400		out << "_let_" << id << " := ";
401		Node nlc = lbind->convert(nl, "_let_", false);
402		toStream(out, nlc, toDepth, lbind);
403		}
404		out << " IN ";
405		}
406	4	Node nc = lbind->convert(n, "_let_");
407		// print the body, passing the lbind object
408	2	toStream(out, nc, toDepth, lbind);
409	2	out << cparen.str();
410	2	lbind->popScope();
411		}
412
413		template <class T>
414		static bool tryToStream(std::ostream& out, const Command* c)
415		{
416		if(typeid(*c) == typeid(T)) {
417		toStream(out, dynamic_cast<const T*>(c));
418		return true;
419		}
420		return false;
421		}
422
423	1	static void toStream(std::ostream& out, const CommandSuccess* s)
424		{
425	1	if(Command::printsuccess::getPrintSuccess(out)) {
426		out << "OK" << endl;
427		}
428	1	}
429
430		static void toStream(std::ostream& out, const CommandInterrupted* s)
431		{
432		out << "INTERRUPTED" << endl;
433		}
434
435		static void toStream(std::ostream& out, const CommandUnsupported* s)
436		{
437		out << "UNSUPPORTED" << endl;
438		}
439
440		static void toStream(std::ostream& out, const CommandFailure* s)
441		{
442		out << s->getMessage() << endl;
443		}
444
445		template <class T>
446	1	static bool tryToStream(std::ostream& out, const CommandStatus* s)
447		{
448	1	if(typeid(*s) == typeid(T)) {
449	1	toStream(out, dynamic_cast<const T*>(s));
450	1	return true;
451		}
452		return false;
453		}
454
455		} // namespace ast
456		} // namespace printer
457	22755	} // namespace cvc5