/*********************                                                        */
/*! \file printer.h
 ** \verbatim
 ** Top contributors (to current version):
 **   Morgan Deters, Tim King, Andrew Reynolds
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2018 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.\endverbatim
 **
 ** \brief Base of the pretty-printer interface
 **
 ** Base of the pretty-printer interface.
 **/

#include "cvc4_private.h"

#ifndef __CVC4__PRINTER__PRINTER_H
#define __CVC4__PRINTER__PRINTER_H

#include <map>
#include <string>

#include "expr/node.h"
#include "options/language.h"
#include "smt/command.h"
#include "smt/model.h"
#include "util/sexpr.h"

namespace CVC4 {

class Printer
{
 public:
  /**
   * Since the printers are managed as unique_ptr, we need public acces to
   * the virtual destructor.
   */
  virtual ~Printer() {}

  /** Get the Printer for a given OutputLanguage */
  static Printer* getPrinter(OutputLanguage lang);

  /** Write a Node out to a stream with this Printer. */
  virtual void toStream(std::ostream& out,
                        TNode n,
                        int toDepth,
                        bool types,
                        size_t dag) const = 0;

  /** Write a Command out to a stream with this Printer. */
  virtual void toStream(std::ostream& out,
                        const Command* c,
                        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;

  /** Write an UnsatCore out to a stream with this Printer. */
  virtual void toStream(std::ostream& out, const UnsatCore& core) const;

  /**
   * Write the term that sygus datatype term n
   * encodes to a stream with this Printer.
   * For example, consider the datatype term
   *   (C_plus (C_minus C_x C_0) C_y)
   * where C_plus, C_minus, C_x, C_0, C_y are constructors
   * whose sygus operators are PLUS, MINUS, x, 0, y.
   * In this case, this method is equivalent to printing
   * the integer term:
   *   (PLUS (MINUS x 0) y)
   * This method may make calls to sygus printing callback
   * methods stored in sygus datatype constructors.
   */
  virtual void toStreamSygus(std::ostream& out, TNode n) const;

 protected:
  /** Derived classes can construct, but no one else. */
  Printer() {}

  /** write model response to command */
  virtual void toStream(std::ostream& out,
                        const Model& m,
                        const Command* c) const = 0;

  /** write model response to command using another language printer */
  void toStreamUsing(OutputLanguage lang,
                     std::ostream& out,
                     const Model& m,
                     const Command* c) const
  {
    getPrinter(lang)->toStream(out, m, c);
  }

 private:
  /** Disallow copy, assignment  */
  Printer(const Printer&) CVC4_UNDEFINED;
  Printer& operator=(const Printer&) CVC4_UNDEFINED;

  /** Make a Printer for a given OutputLanguage */
  static std::unique_ptr<Printer> makePrinter(OutputLanguage lang);

  /** Printers for each OutputLanguage */
  static std::unique_ptr<Printer> d_printers[language::output::LANG_MAX];

}; /* class Printer */

}  // namespace CVC4

#endif /* __CVC4__PRINTER__PRINTER_H */