/*! \file printer.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Andrew Reynolds, 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.
+ ** 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.\endverbatim
**
class Command;
class CommandStatus;
-class NodeCommand;
class UnsatCore;
+class InstantiationList;
+class SkolemList;
class Printer
{
virtual void toStream(std::ostream& out,
TNode n,
int toDepth,
- bool types,
size_t dag) const = 0;
/** Write a CommandStatus out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
/** Write a Model out to a stream with this Printer. */
- virtual void toStream(std::ostream& out, const Model& m) const;
+ virtual void toStream(std::ostream& out, const smt::Model& m) const;
/** 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 */
TypeNode range,
Node formula) const;
- /** Print define-named-fun command */
- virtual void toStreamCmdDefineNamedFunction(std::ostream& out,
- const std::string& id,
- const std::vector<Node>& formals,
- TypeNode range,
- Node formula) const;
-
/** Print define-fun-rec command */
virtual void toStreamCmdDefineFunctionRec(
std::ostream& out,
/** 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;
/** Print simplify command */
virtual void toStreamCmdSimplify(std::ostream& out, Node n) const;
- /** Print expand-definitions command */
- void toStreamCmdExpandDefinitions(std::ostream& out, Node n) const;
-
/** Print get-value command */
virtual void toStreamCmdGetValue(std::ostream& out,
const std::vector<Node>& nodes) const;
/** Print comment command */
virtual void toStreamCmdComment(std::ostream& out,
const std::string& comment) const;
+ /** Declare heap command */
+ virtual void toStreamCmdDeclareHeap(std::ostream& out,
+ TypeNode locType,
+ TypeNode dataType) const;
/** Print command sequence command */
virtual void toStreamCmdCommandSequence(
/** Derived classes can construct, but no one else. */
Printer() {}
- /** write model response to command */
- virtual void toStream(std::ostream& out,
- const 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 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