Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/printer/ast/ast_printer.cpp	Lines:	39	224	17.4 %
Date:	2021-05-22	Branches:	45	258	17.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,
                                   const smt::Model& m,
                                   TypeNode tn) const
{
  // shouldn't be called; only the non-Command* version above should be
  Unreachable();
}

void AstPrinter::toStreamModelTerm(std::ostream& out,
                                   const smt::Model& m,
                                   Node n) 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, Node n) const
{
  if (n.isNull())
  {
    out << "CheckSat()";
  }
  else
  {
    out << "CheckSat(" << n << ')';
  }
  out << 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::toStreamCmdSetBenchmarkStatus(std::ostream& out,
                                               Result::Sat status) const
{
  out << "SetBenchmarkStatus(" << status << ')' << 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::toStreamCmdComment(std::ostream& out,
                                    const std::string& comment) const
{
  out << "CommentCommand([" << comment << "])" << 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		void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const
125		{
126		if(tryToStream<CommandSuccess>(out, s) \|\|
127		tryToStream<CommandFailure>(out, s) \|\|
128		tryToStream<CommandUnsupported>(out, s) \|\|
129		tryToStream<CommandInterrupted>(out, s)) {
130		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		const smt::Model& m,
145		TypeNode tn) 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 smt::Model& m,
153		Node n) 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, Node n) const
186		{
187		if (n.isNull())
188		{
189		out << "CheckSat()";
190		}
191		else
192		{
193		out << "CheckSat(" << n << ')';
194		}
195		out << std::endl;
196		}
197
198		void AstPrinter::toStreamCmdCheckSatAssuming(
199		std::ostream& out, const std::vector<Node>& nodes) const
200		{
201		out << "CheckSatAssuming( << ";
202		copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
203		out << ">> )" << std::endl;
204		}
205
206		void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
207		{
208		out << "Query(" << n << ')' << std::endl;
209		}
210
211		void AstPrinter::toStreamCmdReset(std::ostream& out) const
212		{
213		out << "Reset()" << std::endl;
214		}
215
216		void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
217		{
218		out << "ResetAssertions()" << std::endl;
219		}
220
221		void AstPrinter::toStreamCmdQuit(std::ostream& out) const
222		{
223		out << "Quit()" << std::endl;
224		}
225
226		void AstPrinter::toStreamCmdDeclarationSequence(
227		std::ostream& out, const std::vector<Command*>& sequence) const
228		{
229		out << "DeclarationSequence[" << endl;
230		for (CommandSequence::const_iterator i = sequence.cbegin();
231		i != sequence.cend();
232		++i)
233		{
234		out << *i << endl;
235		}
236		out << "]" << std::endl;
237		}
238
239		void AstPrinter::toStreamCmdCommandSequence(
240		std::ostream& out, const std::vector<Command*>& sequence) const
241		{
242		out << "CommandSequence[" << endl;
243		for (CommandSequence::const_iterator i = sequence.cbegin();
244		i != sequence.cend();
245		++i)
246		{
247		out << *i << endl;
248		}
249		out << "]" << std::endl;
250		}
251
252		void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
253		const std::string& id,
254		TypeNode type) const
255		{
256		out << "Declare(" << id << "," << type << ')' << std::endl;
257		}
258
259		void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
260		const std::string& id,
261		const std::vector<Node>& formals,
262		TypeNode range,
263		Node formula) const
264		{
265		out << "DefineFunction( \"" << id << "\", [";
266		if (formals.size() > 0)
267		{
268		copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
269		out << formals.back();
270		}
271		out << "], << " << formula << " >> )" << std::endl;
272		}
273
274		void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
275		TypeNode type) const
276		{
277		out << "DeclareType(" << type << ')' << std::endl;
278		}
279
280		void AstPrinter::toStreamCmdDefineType(std::ostream& out,
281		const std::string& id,
282		const std::vector<TypeNode>& params,
283		TypeNode t) const
284		{
285		out << "DefineType(" << id << ",[";
286		if (params.size() > 0)
287		{
288		copy(params.begin(),
289		params.end() - 1,
290		ostream_iterator<TypeNode>(out, ", "));
291		out << params.back();
292		}
293		out << "]," << t << ')' << std::endl;
294		}
295
296		void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
297		{
298		out << "Simplify( << " << n << " >> )" << std::endl;
299		}
300
301		void AstPrinter::toStreamCmdGetValue(std::ostream& out,
302		const std::vector<Node>& nodes) const
303		{
304		out << "GetValue( << ";
305		copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
306		out << ">> )" << std::endl;
307		}
308
309		void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
310		{
311		out << "GetModel()" << std::endl;
312		}
313
314		void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
315		{
316		out << "GetAssignment()" << std::endl;
317		}
318
319		void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
320		{
321		out << "GetAssertions()" << std::endl;
322		}
323
324		void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
325		{
326		out << "GetProof()" << std::endl;
327		}
328
329		void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
330		{
331		out << "GetUnsatCore()" << std::endl;
332		}
333
334		void AstPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
335		Result::Sat status) const
336		{
337		out << "SetBenchmarkStatus(" << status << ')' << std::endl;
338		}
339
340		void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
341		const std::string& logic) const
342		{
343		out << "SetBenchmarkLogic(" << logic << ')' << std::endl;
344		}
345
346		void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
347		const std::string& flag,
348		const std::string& value) const
349		{
350		out << "SetInfo(" << flag << ", " << value << ')' << std::endl;
351		}
352
353		void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
354		const std::string& flag) const
355		{
356		out << "GetInfo(" << flag << ')' << std::endl;
357		}
358
359		void AstPrinter::toStreamCmdSetOption(std::ostream& out,
360		const std::string& flag,
361		const std::string& value) const
362		{
363		out << "SetOption(" << flag << ", " << value << ')' << std::endl;
364		}
365
366		void AstPrinter::toStreamCmdGetOption(std::ostream& out,
367		const std::string& flag) const
368		{
369		out << "GetOption(" << flag << ')' << std::endl;
370		}
371
372		void AstPrinter::toStreamCmdDatatypeDeclaration(
373		std::ostream& out, const std::vector<TypeNode>& datatypes) const
374		{
375		out << "DatatypeDeclarationCommand([";
376		for (const TypeNode& t : datatypes)
377		{
378		out << t << ";" << endl;
379		}
380		out << "])" << std::endl;
381		}
382
383		void AstPrinter::toStreamCmdComment(std::ostream& out,
384		const std::string& comment) const
385		{
386		out << "CommentCommand([" << comment << "])" << std::endl;
387		}
388
389	2	void AstPrinter::toStreamWithLetify(std::ostream& out,
390		Node n,
391		int toDepth,
392		LetBinding* lbind) const
393		{
394	2	if (lbind == nullptr)
395		{
396		toStream(out, n, toDepth);
397		return;
398		}
399	4	std::stringstream cparen;
400	4	std::vector<Node> letList;
401	2	lbind->letify(n, letList);
402	2	if (!letList.empty())
403		{
404		std::map<Node, uint32_t>::const_iterator it;
405		out << "(LET ";
406		cparen << ")";
407		bool first = true;
408		for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
409		{
410		if (!first)
411		{
412		out << ", ";
413		}
414		else
415		{
416		first = false;
417		}
418		Node nl = letList[i];
419		uint32_t id = lbind->getId(nl);
420		out << "_let_" << id << " := ";
421		Node nlc = lbind->convert(nl, "_let_", false);
422		toStream(out, nlc, toDepth, lbind);
423		}
424		out << " IN ";
425		}
426	4	Node nc = lbind->convert(n, "_let_");
427		// print the body, passing the lbind object
428	2	toStream(out, nc, toDepth, lbind);
429	2	out << cparen.str();
430	2	lbind->popScope();
431		}
432
433		template <class T>
434		static bool tryToStream(std::ostream& out, const Command* c)
435		{
436		if(typeid(*c) == typeid(T)) {
437		toStream(out, dynamic_cast<const T*>(c));
438		return true;
439		}
440		return false;
441		}
442
443		static void toStream(std::ostream& out, const CommandSuccess* s)
444		{
445		if(Command::printsuccess::getPrintSuccess(out)) {
446		out << "OK" << endl;
447		}
448		}
449
450		static void toStream(std::ostream& out, const CommandInterrupted* s)
451		{
452		out << "INTERRUPTED" << endl;
453		}
454
455		static void toStream(std::ostream& out, const CommandUnsupported* s)
456		{
457		out << "UNSUPPORTED" << endl;
458		}
459
460		static void toStream(std::ostream& out, const CommandFailure* s)
461		{
462		out << s->getMessage() << endl;
463		}
464
465		template <class T>
466		static bool tryToStream(std::ostream& out, const CommandStatus* s)
467		{
468		if(typeid(*s) == typeid(T)) {
469		toStream(out, dynamic_cast<const T*>(s));
470		return true;
471		}
472		return false;
473		}
474
475		} // namespace ast
476		} // namespace printer
477	28191	} // namespace cvc5