/*********************                                                        */
/*! \file command.h
 ** \verbatim
 ** Original author: mdeters
 ** Major contributors: none
 ** Minor contributors (to current version): cconway, dejan
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** See the file COPYING in the top-level source directory for licensing
 ** information.\endverbatim
 **
 ** \brief Implementation of the command pattern on SmtEngines.
 **
 ** Implementation of the command pattern on SmtEngines.  Command
 ** objects are generated by the parser (typically) to implement the
 ** commands in parsed input (see Parser::parseNextCommand()), or by
 ** client code.
 **/

#include "cvc4_public.h"

#ifndef __CVC4__COMMAND_H
#define __CVC4__COMMAND_H

#include <iostream>
#include <sstream>
#include <string>
#include <vector>
#include <map>

#include "expr/expr.h"
#include "expr/type.h"
#include "util/result.h"
#include "util/sexpr.h"
#include "util/datatype.h"

namespace CVC4 {

class SmtEngine;
class Command;

std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;

/** The status an SMT benchmark can have */
enum BenchmarkStatus {
  /** Benchmark is satisfiable */
  SMT_SATISFIABLE,
  /** Benchmark is unsatisfiable */
  SMT_UNSATISFIABLE,
  /** The status of the benchmark is unknown */
  SMT_UNKNOWN
};

std::ostream& operator<<(std::ostream& out,
                         BenchmarkStatus status) CVC4_PUBLIC;

class CVC4_PUBLIC Command {
public:
  virtual ~Command() {}

  virtual void invoke(SmtEngine* smtEngine) = 0;
  virtual void invoke(SmtEngine* smtEngine, std::ostream& out);

  virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false,
                        OutputLanguage language = language::output::LANG_AST) const;

  std::string toString() const;

  virtual void printResult(std::ostream& out) const;

};/* class Command */

/**
 * EmptyCommands are the residue of a command after the parser handles
 * them (and there's nothing left to do).
 */
class CVC4_PUBLIC EmptyCommand : public Command {
protected:
  std::string d_name;
public:
  EmptyCommand(std::string name = "");
  std::string getName() const;
  void invoke(SmtEngine* smtEngine);
};/* class EmptyCommand */

class CVC4_PUBLIC AssertCommand : public Command {
protected:
  BoolExpr d_expr;
public:
  AssertCommand(const BoolExpr& e);
  BoolExpr getExpr() const;
  void invoke(SmtEngine* smtEngine);
};/* class AssertCommand */

class CVC4_PUBLIC PushCommand : public Command {
public:
  void invoke(SmtEngine* smtEngine);
};/* class PushCommand */

class CVC4_PUBLIC PopCommand : public Command {
public:
  void invoke(SmtEngine* smtEngine);
};/* class PopCommand */

class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
protected:
  std::string d_symbol;
public:
  DeclarationDefinitionCommand(const std::string& id);
  std::string getSymbol() const;
};/* class DeclarationDefinitionCommand */

class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
protected:
  Type d_type;
public:
  DeclareFunctionCommand(const std::string& id, Type type);
  Type getType() const;
  void invoke(SmtEngine* smtEngine);
};/* class DeclareFunctionCommand */

class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
protected:
  size_t d_arity;
  Type d_type;
public:
  DeclareTypeCommand(const std::string& id, size_t arity, Type t);
  size_t getArity() const;
  Type getType() const;
  void invoke(SmtEngine* smtEngine);
};/* class DeclareTypeCommand */

class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
protected:
  std::vector<Type> d_params;
  Type d_type;
public:
  DefineTypeCommand(const std::string& id, Type t);
  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t);
  const std::vector<Type>& getParameters() const;
  Type getType() const;
  void invoke(SmtEngine* smtEngine);
};/* class DefineTypeCommand */

class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
protected:
  Expr d_func;
  std::vector<Expr> d_formals;
  Expr d_formula;
public:
  DefineFunctionCommand(const std::string& id, Expr func, Expr formula);
  DefineFunctionCommand(const std::string& id, Expr func,
                        const std::vector<Expr>& formals, Expr formula);
  Expr getFunction() const;
  const std::vector<Expr>& getFormals() const;
  Expr getFormula() const;
  void invoke(SmtEngine* smtEngine);
};/* class DefineFunctionCommand */

/**
 * This differs from DefineFunctionCommand only in that it instructs
 * the SmtEngine to "remember" this function for later retrieval with
 * getAssignment().  Used for :named attributes in SMT-LIBv2.
 */
class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
public:
  DefineNamedFunctionCommand(const std::string& id, Expr func,
                             const std::vector<Expr>& formals, Expr formula);
  void invoke(SmtEngine* smtEngine);
};/* class DefineNamedFunctionCommand */

class CVC4_PUBLIC CheckSatCommand : public Command {
protected:
  BoolExpr d_expr;
  Result d_result;
public:
  CheckSatCommand();
  CheckSatCommand(const BoolExpr& expr);
  BoolExpr getExpr() const;
  void invoke(SmtEngine* smtEngine);
  Result getResult() const;
  void printResult(std::ostream& out) const;
};/* class CheckSatCommand */

class CVC4_PUBLIC QueryCommand : public Command {
protected:
  BoolExpr d_expr;
  Result d_result;
public:
  QueryCommand(const BoolExpr& e);
  BoolExpr getExpr() const;
  void invoke(SmtEngine* smtEngine);
  Result getResult() const;
  void printResult(std::ostream& out) const;
};/* class QueryCommand */

// this is TRANSFORM in the CVC presentation language
class CVC4_PUBLIC SimplifyCommand : public Command {
protected:
  Expr d_term;
  Expr d_result;
public:
  SimplifyCommand(Expr term);
  Expr getTerm() const;
  void invoke(SmtEngine* smtEngine);
  Expr getResult() const;
  void printResult(std::ostream& out) const;
};/* class SimplifyCommand */

class CVC4_PUBLIC GetValueCommand : public Command {
protected:
  Expr d_term;
  Expr d_result;
public:
  GetValueCommand(Expr term);
  Expr getTerm() const;
  void invoke(SmtEngine* smtEngine);
  Expr getResult() const;
  void printResult(std::ostream& out) const;
};/* class GetValueCommand */

class CVC4_PUBLIC GetAssignmentCommand : public Command {
protected:
  SExpr d_result;
public:
  GetAssignmentCommand();
  void invoke(SmtEngine* smtEngine);
  SExpr getResult() const;
  void printResult(std::ostream& out) const;
};/* class GetAssignmentCommand */

class CVC4_PUBLIC GetAssertionsCommand : public Command {
protected:
  std::string d_result;
public:
  GetAssertionsCommand();
  void invoke(SmtEngine* smtEngine);
  std::string getResult() const;
  void printResult(std::ostream& out) const;
};/* class GetAssertionsCommand */

class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
protected:
  std::string d_result;
  BenchmarkStatus d_status;
public:
  SetBenchmarkStatusCommand(BenchmarkStatus status);
  BenchmarkStatus getStatus() const;
  void invoke(SmtEngine* smtEngine);
};/* class SetBenchmarkStatusCommand */

class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
protected:
  std::string d_result;
  std::string d_logic;
public:
  SetBenchmarkLogicCommand(std::string logic);
  std::string getLogic() const;
  void invoke(SmtEngine* smtEngine);
};/* class SetBenchmarkLogicCommand */

class CVC4_PUBLIC SetInfoCommand : public Command {
protected:
  std::string d_flag;
  SExpr d_sexpr;
  std::string d_result;
public:
  SetInfoCommand(std::string flag, const SExpr& sexpr);
  std::string getFlag() const;
  SExpr getSExpr() const;
  void invoke(SmtEngine* smtEngine);
  std::string getResult() const;
  void printResult(std::ostream& out) const;
};/* class SetInfoCommand */

class CVC4_PUBLIC GetInfoCommand : public Command {
protected:
  std::string d_flag;
  std::string d_result;
public:
  GetInfoCommand(std::string flag);
  std::string getFlag() const;
  void invoke(SmtEngine* smtEngine);
  std::string getResult() const;
  void printResult(std::ostream& out) const;
};/* class GetInfoCommand */

class CVC4_PUBLIC SetOptionCommand : public Command {
protected:
  std::string d_flag;
  SExpr d_sexpr;
  std::string d_result;
public:
  SetOptionCommand(std::string flag, const SExpr& sexpr);
  std::string getFlag() const;
  SExpr getSExpr() const;
  void invoke(SmtEngine* smtEngine);
  std::string getResult() const;
  void printResult(std::ostream& out) const;
};/* class SetOptionCommand */

class CVC4_PUBLIC GetOptionCommand : public Command {
protected:
  std::string d_flag;
  std::string d_result;
public:
  GetOptionCommand(std::string flag);
  std::string getFlag() const;
  void invoke(SmtEngine* smtEngine);
  std::string getResult() const;
  void printResult(std::ostream& out) const;
};/* class GetOptionCommand */

class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
private:
  std::vector<DatatypeType> d_datatypes;
public:
  DatatypeDeclarationCommand(const DatatypeType& datatype);
  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
  const std::vector<DatatypeType>& getDatatypes() const;
  void invoke(SmtEngine* smtEngine);
};/* class DatatypeDeclarationCommand */

class CVC4_PUBLIC QuitCommand : public Command {
public:
  QuitCommand();
  void invoke(SmtEngine* smtEngine);
};/* class QuitCommand */

class CVC4_PUBLIC CommentCommand : public Command {
  std::string d_comment;
public:
  CommentCommand(std::string comment);
  std::string getComment() const;
  void invoke(SmtEngine* smtEngine);
};/* class CommentCommand */

class CVC4_PUBLIC CommandSequence : public Command {
private:
  /** All the commands to be executed (in sequence) */
  std::vector<Command*> d_commandSequence;
  /** Next command to be executed */
  unsigned int d_index;
public:
  CommandSequence();
  ~CommandSequence();

  void addCommand(Command* cmd);

  void invoke(SmtEngine* smtEngine);
  void invoke(SmtEngine* smtEngine, std::ostream& out);

  typedef std::vector<Command*>::iterator iterator;
  typedef std::vector<Command*>::const_iterator const_iterator;

  const_iterator begin() const;
  const_iterator end() const;

  iterator begin();
  iterator end();

};/* class CommandSequence */

class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
public:
};/* class DeclarationSequence */

}/* CVC4 namespace */

#endif /* __CVC4__COMMAND_H */