Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/printer/ast/ast_printer.cpp	Lines:	50	215	23.3 %
Date:	2021-11-07	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"

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