(proof-new) Instantiation list utility (#5768)

[cvc5.git] / src / printer / printer.h

diff --git a/src/printer/printer.h b/src/printer/printer.h
index af280cb4094390bafc22301a96ede848e6abb571..835dbe798e58dd9630c68cf94a95c0299a9aeeb7 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -2,10 +2,10 @@
 /*! \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
  **
@@ -32,8 +32,9 @@ namespace CVC4 {
 
 class Command;
 class CommandStatus;
-class NodeCommand;
 class UnsatCore;
+class InstantiationList;
+class SkolemList;
 
 class Printer
 {
@@ -51,18 +52,23 @@ 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;
@@ -87,8 +93,6 @@ class Printer
 
   /** Print declare-sort command */
   virtual void toStreamCmdDeclareType(std::ostream& out,
-                                      const std::string& id,
-                                      size_t arity,
                                       TypeNode type) const;
 
   /** Print define-sort command */
@@ -104,13 +108,6 @@ class Printer
                                          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,
@@ -141,11 +138,10 @@ class Printer
 
   /** 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;
@@ -160,9 +156,6 @@ class Printer
   /** 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;
@@ -260,6 +253,10 @@ class Printer
   /** 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(
@@ -273,19 +270,26 @@ class Printer
   /** 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