/*! \file printer.h
** \verbatim
** Top contributors (to current version):
- ** Abdalrhman Mohamed, Tim King, Aina Niemetz
+ ** Abdalrhman Mohamed, Andrew Reynolds, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
class Command;
class CommandStatus;
-class NodeCommand;
class UnsatCore;
+class InstantiationList;
+class SkolemList;
class Printer
{
/** Write an UnsatCore out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const UnsatCore& core) const;
+ /** Write an instantiation list out to a stream with this Printer. */
+ virtual void toStream(std::ostream& out, const InstantiationList& is) const;
+
+ /** Write a skolem list out to a stream with this Printer. */
+ virtual void toStream(std::ostream& out, const SkolemList& sks) const;
+
/** Print empty command */
virtual void toStreamCmdEmpty(std::ostream& out,
const std::string& name) const;
/** Print declare-sort command */
virtual void toStreamCmdDeclareType(std::ostream& out,
- const std::string& id,
- size_t arity,
TypeNode type) const;
/** Print define-sort command */
/** Print synth-fun command */
virtual void toStreamCmdSynthFun(std::ostream& out,
- const std::string& sym,
+ Node f,
const std::vector<Node>& vars,
- TypeNode range,
bool isInv,
- TypeNode sygusType) const;
+ TypeNode sygusType = TypeNode::null()) const;
/** Print constraint command */
virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
/** Derived classes can construct, but no one else. */
Printer() {}
- /** write model response to command */
- virtual void toStream(std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const = 0;
+ /**
+ * To stream model sort. This prints the appropriate output for type
+ * tn declared via declare-sort or declare-datatype.
+ */
+ virtual void toStreamModelSort(std::ostream& out,
+ const smt::Model& m,
+ TypeNode tn) const = 0;
+
+ /**
+ * To stream model term. This prints the appropriate output for term
+ * n declared via declare-fun.
+ */
+ virtual void toStreamModelTerm(std::ostream& out,
+ const smt::Model& m,
+ Node n) const = 0;
/** write model response to command using another language printer */
void toStreamUsing(OutputLanguage lang,
std::ostream& out,
- const smt::Model& m,
- const NodeCommand* c) const
- {
- getPrinter(lang)->toStream(out, m, c);
- }
+ const smt::Model& m) const;
/**
* Write an error to `out` stating that command `name` is not supported by