path: root/src/expr/command.h

/*********************                                                        */
/*! \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"
#include "util/proof.h"

namespace CVC4 {

class SmtEngine;
class Command;
class CommandStatus;

std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() 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) throw() CVC4_PUBLIC;

/**
 * IOStream manipulator to print success messages or not.
 *
 *   out << Command::printsuccess(false) << CommandSuccess();
 *
 * prints nothing, but
 *
 *   out << Command::printsuccess(true) << CommandSuccess();
 *
 * prints a success message (in a manner appropriate for the current
 * output language).
 */
class CVC4_PUBLIC CommandPrintSuccess {
  /**
   * The allocated index in ios_base for our depth setting.
   */
  static const int s_iosIndex;

  /**
   * The default setting, for ostreams that haven't yet had a
   * setdepth() applied to them.
   */
  static const int s_defaultPrintSuccess = false;

  /**
   * When this manipulator is used, the setting is stored here.
   */
  bool d_printSuccess;

public:
  /**
   * Construct a CommandPrintSuccess with the given setting.
   */
  CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {}

  inline void applyPrintSuccess(std::ostream& out) throw() {
    out.iword(s_iosIndex) = d_printSuccess;
  }

  static inline bool getPrintSuccess(std::ostream& out) throw() {
    return out.iword(s_iosIndex);
  }

  static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() {
    out.iword(s_iosIndex) = printSuccess;
  }

  /**
   * Set the print-success state on the output stream for the current
   * stack scope.  This makes sure the old state is reset on the
   * stream after normal OR exceptional exit from the scope, using the
   * RAII C++ idiom.
   */
  class Scope {
    std::ostream& d_out;
    bool d_oldPrintSuccess;

  public:

    inline Scope(std::ostream& out, bool printSuccess) throw() :
      d_out(out),
      d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) {
      CommandPrintSuccess::setPrintSuccess(out, printSuccess);
    }

    inline ~Scope() throw() {
      CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess);
    }

  };/* class CommandPrintSuccess::Scope */

};/* class CommandPrintSuccess */

/**
 * Sets the default print-success setting when pretty-printing an Expr
 * to an ostream.  Use like this:
 *
 *   // let out be an ostream, e an Expr
 *   out << Expr::setdepth(n) << e << endl;
 *
 * The depth stays permanently (until set again) with the stream.
 */
inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC;
inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() {
  cps.applyPrintSuccess(out);
  return out;
}

class CVC4_PUBLIC CommandStatus {
protected:
  // shouldn't construct a CommandStatus (use a derived class)
  CommandStatus() throw() {}
public:
  virtual ~CommandStatus() throw() {}
  void toStream(std::ostream& out,
                OutputLanguage language = language::output::LANG_AST) const throw();
};/* class CommandStatus */

class CVC4_PUBLIC CommandSuccess : public CommandStatus {
  static const CommandSuccess* s_instance;
public:
  static const CommandSuccess* instance() throw() { return s_instance; }
};/* class CommandSuccess */

class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
};/* class CommandSuccess */

class CVC4_PUBLIC CommandFailure : public CommandStatus {
  std::string d_message;
public:
  CommandFailure(std::string message) throw() : d_message(message) {}
  ~CommandFailure() throw() {}
  std::string getMessage() const throw() { return d_message; }
};/* class CommandFailure */

class CVC4_PUBLIC Command {
protected:
  /**
   * This field contains a command status if the command has been
   * invoked, or NULL if it has not.  This field is either a
   * dynamically-allocated pointer, or it's a pointer to the singleton
   * CommandSuccess instance.  Doing so is somewhat asymmetric, but
   * it avoids the need to dynamically allocate memory in the common
   * case of a successful command.
   */
  const CommandStatus* d_commandStatus;

public:
  typedef CommandPrintSuccess printsuccess;

  Command() throw();
  virtual ~Command() throw();

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

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

  std::string toString() const throw();

  /** Either the command hasn't run yet, or it completed successfully. */
  bool ok() const throw();

  /** Get the command status (it's NULL if we haven't run yet). */
  const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }

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

};/* 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 = "") throw();
  ~EmptyCommand() throw() {}
  std::string getName() const throw();
  void invoke(SmtEngine* smtEngine) throw();
};/* class EmptyCommand */

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

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

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

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

class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
protected:
  Type d_type;
public:
  DeclareFunctionCommand(const std::string& id, Type type) throw();
  ~DeclareFunctionCommand() throw() {}
  Type getType() const throw();
  void invoke(SmtEngine* smtEngine) throw();
};/* 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) throw();
  ~DeclareTypeCommand() throw() {}
  size_t getArity() const throw();
  Type getType() const throw();
  void invoke(SmtEngine* smtEngine) throw();
};/* 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) throw();
  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
  ~DefineTypeCommand() throw() {}
  const std::vector<Type>& getParameters() const throw();
  Type getType() const throw();
  void invoke(SmtEngine* smtEngine) throw();
};/* 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) throw();
  DefineFunctionCommand(const std::string& id, Expr func,
                        const std::vector<Expr>& formals, Expr formula) throw();
  ~DefineFunctionCommand() throw() {}
  Expr getFunction() const throw();
  const std::vector<Expr>& getFormals() const throw();
  Expr getFormula() const throw();
  void invoke(SmtEngine* smtEngine) throw();
};/* 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) throw();
  void invoke(SmtEngine* smtEngine) throw();
};/* class DefineNamedFunctionCommand */

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

class CVC4_PUBLIC QueryCommand : public Command {
protected:
  BoolExpr d_expr;
  Result d_result;
public:
  QueryCommand(const BoolExpr& e) throw();
  ~QueryCommand() throw() {}
  BoolExpr getExpr() const throw();
  void invoke(SmtEngine* smtEngine) throw();
  Result getResult() const throw();
  void printResult(std::ostream& out) const throw();
};/* 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) throw();
  ~SimplifyCommand() throw() {}
  Expr getTerm() const throw();
  void invoke(SmtEngine* smtEngine) throw();
  Expr getResult() const throw();
  void printResult(std::ostream& out) const throw();
};/* class SimplifyCommand */

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

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

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

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

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

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

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

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

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

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

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

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

class CVC4_PUBLIC CommentCommand : public Command {
  std::string d_comment;
public:
  CommentCommand(std::string comment) throw();
  ~CommentCommand() throw() {}
  std::string getComment() const throw();
  void invoke(SmtEngine* smtEngine) throw();
};/* 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() throw();
  ~CommandSequence() throw();

  void addCommand(Command* cmd) throw();

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

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

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

  iterator begin() throw();
  iterator end() throw();

};/* class CommandSequence */

class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
public:
  ~DeclarationSequence() throw() {}
};/* class DeclarationSequence */

}/* CVC4 namespace */

#endif /* __CVC4__COMMAND_H */