diff options
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/printer.cpp | 8 | ||||
| -rw-r--r-- | src/printer/printer.h | 5 |
2 files changed, 13 insertions, 0 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 6ab419b85..19d14eb09 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -190,6 +190,14 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out, printUnknownCommand(out, "declare-fun"); } +void Printer::toStreamCmdDeclarePool(std::ostream& out, + const std::string& id, + TypeNode type, + const std::vector<Node>& initValue) const +{ + printUnknownCommand(out, "declare-pool"); +} + void Printer::toStreamCmdDeclareType(std::ostream& out, TypeNode type) const { diff --git a/src/printer/printer.h b/src/printer/printer.h index aeffc76eb..86f3dbb2b 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -87,6 +87,11 @@ class Printer virtual void toStreamCmdDeclareFunction(std::ostream& out, const std::string& id, TypeNode type) const; + /** Print declare-pool command */ + virtual void toStreamCmdDeclarePool(std::ostream& out, + const std::string& id, + TypeNode type, + const std::vector<Node>& initValue) const; /** Print declare-sort command */ virtual void toStreamCmdDeclareType(std::ostream& out, |