path: root/src/smt/command.h

/******************************************************************************
 * Top contributors (to current version):
 *   Abdalrhman Mohamed, Tim King, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * 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 CVC5__COMMAND_H
#define CVC5__COMMAND_H

#include <iosfwd>
#include <sstream>
#include <string>
#include <vector>

#include "api/cpp/cvc5.h"
#include "cvc4_export.h"
#include "options/language.h"

namespace cvc5 {

namespace api {
class Solver;
class Term;
}  // namespace api

class SymbolManager;
class Command;
class CommandStatus;

namespace smt {
class Model;
}

/**
 * Convert a symbolic expression to string. This method differs from
 * Term::toString in that it does not depend on the output language.
 *
 * @param sexpr the symbolic expression to convert
 * @return the symbolic expression as string
 */
std::string sexprToString(api::Term sexpr) CVC4_EXPORT;

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

/** 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
}; /* enum BenchmarkStatus */

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

/**
 * 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_EXPORT CommandPrintSuccess
{
 public:
  /** Construct a CommandPrintSuccess with the given setting. */
  CommandPrintSuccess(bool printSuccess) : d_printSuccess(printSuccess) {}
  void applyPrintSuccess(std::ostream& out);
  static bool getPrintSuccess(std::ostream& out);
  static void setPrintSuccess(std::ostream& out, bool printSuccess);

 private:
  /** 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;

}; /* 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.
 */
std::ostream& operator<<(std::ostream& out,
                         CommandPrintSuccess cps) CVC4_EXPORT;

class CVC4_EXPORT CommandStatus
{
 protected:
  // shouldn't construct a CommandStatus (use a derived class)
  CommandStatus() {}

 public:
  virtual ~CommandStatus() {}
  void toStream(std::ostream& out,
                OutputLanguage language = language::output::LANG_AUTO) const;
  virtual CommandStatus& clone() const = 0;
}; /* class CommandStatus */

class CVC4_EXPORT CommandSuccess : public CommandStatus
{
  static const CommandSuccess* s_instance;

 public:
  static const CommandSuccess* instance() { return s_instance; }
  CommandStatus& clone() const override
  {
    return const_cast<CommandSuccess&>(*this);
  }
}; /* class CommandSuccess */

class CVC4_EXPORT CommandInterrupted : public CommandStatus
{
  static const CommandInterrupted* s_instance;

 public:
  static const CommandInterrupted* instance() { return s_instance; }
  CommandStatus& clone() const override
  {
    return const_cast<CommandInterrupted&>(*this);
  }
}; /* class CommandInterrupted */

class CVC4_EXPORT CommandUnsupported : public CommandStatus
{
 public:
  CommandStatus& clone() const override
  {
    return *new CommandUnsupported(*this);
  }
}; /* class CommandSuccess */

class CVC4_EXPORT CommandFailure : public CommandStatus
{
  std::string d_message;

 public:
  CommandFailure(std::string message) : d_message(message) {}
  CommandFailure& clone() const override { return *new CommandFailure(*this); }
  std::string getMessage() const { return d_message; }
}; /* class CommandFailure */

/**
 * The execution of the command resulted in a non-fatal error and further
 * commands can be processed. This status is for example used when a user asks
 * for an unsat core in a place that is not immediately preceded by an
 * unsat/valid response.
 */
class CVC4_EXPORT CommandRecoverableFailure : public CommandStatus
{
  std::string d_message;

 public:
  CommandRecoverableFailure(std::string message) : d_message(message) {}
  CommandRecoverableFailure& clone() const override
  {
    return *new CommandRecoverableFailure(*this);
  }
  std::string getMessage() const { return d_message; }
}; /* class CommandRecoverableFailure */

class CVC4_EXPORT Command
{
 public:
  typedef CommandPrintSuccess printsuccess;

  Command();
  Command(const Command& cmd);

  virtual ~Command();

  /**
   * Invoke the command on the solver and symbol manager sm.
   */
  virtual void invoke(api::Solver* solver, SymbolManager* sm) = 0;
  /**
   * Same as above, and prints the result to output stream out.
   */
  virtual void invoke(api::Solver* solver,
                      SymbolManager* sm,
                      std::ostream& out);

  virtual void toStream(
      std::ostream& out,
      int toDepth = -1,

      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const = 0;

  std::string toString() const;

  virtual std::string getCommandName() const = 0;

  /**
   * If false, instruct this Command not to print a success message.
   */
  void setMuted(bool muted) { d_muted = muted; }
  /**
   * Determine whether this Command will print a success message.
   */
  bool isMuted() { return d_muted; }
  /**
   * Either the command hasn't run yet, or it completed successfully
   * (CommandSuccess, not CommandUnsupported or CommandFailure).
   */
  bool ok() const;

  /**
   * The command completed in a failure state (CommandFailure, not
   * CommandSuccess or CommandUnsupported).
   */
  bool fail() const;

  /**
   * The command was ran but was interrupted due to resource limiting.
   */
  bool interrupted() const;

  /** Get the command status (it's NULL if we haven't run yet). */
  const CommandStatus* getCommandStatus() const { return d_commandStatus; }
  virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const;

  /**
   * Clone this Command (make a shallow copy).
   */
  virtual Command* clone() const = 0;

  /**
   * 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;

  /**
   * True if this command is "muted"---i.e., don't print "success" on
   * successful execution.
   */
  bool d_muted;

 protected:
  // These methods rely on Command being a friend of classes in the API.
  // Subclasses of command should use these methods for conversions,
  // which is currently necessary for e.g. printing commands.
  /** Helper to convert a Term to an internal Node */
  static Node termToNode(const api::Term& term);
  /** Helper to convert a vector of Terms to internal Nodes. */
  static std::vector<Node> termVectorToNodes(
      const std::vector<api::Term>& terms);
  /** Helper to convert a Sort to an internal TypeNode */
  static TypeNode sortToTypeNode(const api::Sort& sort);
  /** Helper to convert a vector of Sorts to internal TypeNodes. */
  static std::vector<TypeNode> sortVectorToTypeNodes(
      const std::vector<api::Sort>& sorts);
  /** Helper to convert a Grammar to an internal TypeNode */
  static TypeNode grammarToTypeNode(api::Grammar* grammar);
  /** Get original options from the solver (for ResetCommand) */
  Options& getOriginalOptionsFrom(api::Solver* s);
}; /* class Command */

/**
 * EmptyCommands are the residue of a command after the parser handles
 * them (and there's nothing left to do).
 */
class CVC4_EXPORT EmptyCommand : public Command
{
 public:
  EmptyCommand(std::string name = "");
  std::string getName() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  std::string d_name;
}; /* class EmptyCommand */

class CVC4_EXPORT EchoCommand : public Command
{
 public:
  EchoCommand(std::string output = "");

  std::string getOutput() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void invoke(api::Solver* solver,
              SymbolManager* sm,
              std::ostream& out) override;

  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  std::string d_output;
}; /* class EchoCommand */

class CVC4_EXPORT AssertCommand : public Command
{
 protected:
  api::Term d_term;
  bool d_inUnsatCore;

 public:
  AssertCommand(const api::Term& t, bool inUnsatCore = true);

  api::Term getTerm() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;

  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class AssertCommand */

class CVC4_EXPORT PushCommand : public Command
{
 public:
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class PushCommand */

class CVC4_EXPORT PopCommand : public Command
{
 public:
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class PopCommand */

class CVC4_EXPORT DeclarationDefinitionCommand : public Command
{
 protected:
  std::string d_symbol;

 public:
  DeclarationDefinitionCommand(const std::string& id);

  void invoke(api::Solver* solver, SymbolManager* sm) override = 0;
  std::string getSymbol() const;
}; /* class DeclarationDefinitionCommand */

class CVC4_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand
{
 protected:
  api::Term d_func;
  api::Sort d_sort;

 public:
  DeclareFunctionCommand(const std::string& id, api::Term func, api::Sort sort);
  api::Term getFunction() const;
  api::Sort getSort() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DeclareFunctionCommand */

class CVC4_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
{
 protected:
  size_t d_arity;
  api::Sort d_sort;

 public:
  DeclareSortCommand(const std::string& id, size_t arity, api::Sort sort);

  size_t getArity() const;
  api::Sort getSort() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DeclareSortCommand */

class CVC4_EXPORT DefineSortCommand : public DeclarationDefinitionCommand
{
 protected:
  std::vector<api::Sort> d_params;
  api::Sort d_sort;

 public:
  DefineSortCommand(const std::string& id, api::Sort sort);
  DefineSortCommand(const std::string& id,
                    const std::vector<api::Sort>& params,
                    api::Sort sort);

  const std::vector<api::Sort>& getParameters() const;
  api::Sort getSort() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DefineSortCommand */

class CVC4_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
{
 public:
  DefineFunctionCommand(const std::string& id,
                        api::Term func,
                        api::Term formula,
                        bool global);
  DefineFunctionCommand(const std::string& id,
                        api::Term func,
                        const std::vector<api::Term>& formals,
                        api::Term formula,
                        bool global);

  api::Term getFunction() const;
  const std::vector<api::Term>& getFormals() const;
  api::Term getFormula() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** The function we are defining */
  api::Term d_func;
  /** The formal arguments for the function we are defining */
  std::vector<api::Term> d_formals;
  /** The formula corresponding to the body of the function we are defining */
  api::Term d_formula;
  /**
   * Stores whether this definition is global (i.e. should persist when
   * popping the user context.
   */
  bool d_global;
}; /* class DefineFunctionCommand */

/**
 * The command when parsing define-fun-rec or define-funs-rec.
 * This command will assert a set of quantified formulas that specify
 * the (mutually recursive) function definitions provided to it.
 */
class CVC4_EXPORT DefineFunctionRecCommand : public Command
{
 public:
  DefineFunctionRecCommand(api::Term func,
                           const std::vector<api::Term>& formals,
                           api::Term formula,
                           bool global);
  DefineFunctionRecCommand(const std::vector<api::Term>& funcs,
                           const std::vector<std::vector<api::Term> >& formals,
                           const std::vector<api::Term>& formula,
                           bool global);

  const std::vector<api::Term>& getFunctions() const;
  const std::vector<std::vector<api::Term> >& getFormals() const;
  const std::vector<api::Term>& getFormulas() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** functions we are defining */
  std::vector<api::Term> d_funcs;
  /** formal arguments for each of the functions we are defining */
  std::vector<std::vector<api::Term> > d_formals;
  /** formulas corresponding to the bodies of the functions we are defining */
  std::vector<api::Term> d_formulas;
  /**
   * Stores whether this definition is global (i.e. should persist when
   * popping the user context.
   */
  bool d_global;
}; /* class DefineFunctionRecCommand */

/**
 * In separation logic inputs, which is an extension of smt2 inputs, this
 * corresponds to the command:
 *   (declare-heap (T U))
 * where T is the location sort and U is the data sort.
 */
class CVC4_EXPORT DeclareHeapCommand : public Command
{
 public:
  DeclareHeapCommand(api::Sort locSort, api::Sort dataSort);
  api::Sort getLocationSort() const;
  api::Sort getDataSort() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** The location sort */
  api::Sort d_locSort;
  /** The data sort */
  api::Sort d_dataSort;
};

/**
 * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
 *  via the syntax (! expr :attr)
 */
class CVC4_EXPORT SetUserAttributeCommand : public Command
{
 public:
  SetUserAttributeCommand(const std::string& attr, api::Term term);
  SetUserAttributeCommand(const std::string& attr,
                          api::Term term,
                          const std::vector<api::Term>& values);
  SetUserAttributeCommand(const std::string& attr,
                          api::Term term,
                          const std::string& value);

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 private:
  SetUserAttributeCommand(const std::string& attr,
                          api::Term term,
                          const std::vector<api::Term>& termValues,
                          const std::string& strValue);

  const std::string d_attr;
  const api::Term d_term;
  const std::vector<api::Term> d_termValues;
  const std::string d_strValue;
}; /* class SetUserAttributeCommand */

/**
 * The command when parsing check-sat.
 * This command will check satisfiability of the input formula.
 */
class CVC4_EXPORT CheckSatCommand : public Command
{
 public:
  CheckSatCommand();
  CheckSatCommand(const api::Term& term);

  api::Term getTerm() const;
  api::Result getResult() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 private:
  api::Term d_term;
  api::Result d_result;
}; /* class CheckSatCommand */

/**
 * The command when parsing check-sat-assuming.
 * This command will assume a set of formulas and check satisfiability of the
 * input formula under these assumptions.
 */
class CVC4_EXPORT CheckSatAssumingCommand : public Command
{
 public:
  CheckSatAssumingCommand(api::Term term);
  CheckSatAssumingCommand(const std::vector<api::Term>& terms);

  const std::vector<api::Term>& getTerms() const;
  api::Result getResult() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 private:
  std::vector<api::Term> d_terms;
  api::Result d_result;
}; /* class CheckSatAssumingCommand */

class CVC4_EXPORT QueryCommand : public Command
{
 protected:
  api::Term d_term;
  api::Result d_result;
  bool d_inUnsatCore;

 public:
  QueryCommand(const api::Term& t, bool inUnsatCore = true);

  api::Term getTerm() const;
  api::Result getResult() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class QueryCommand */

/* ------------------- sygus commands  ------------------ */

/** Declares a sygus universal variable */
class CVC4_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand
{
 public:
  DeclareSygusVarCommand(const std::string& id, api::Term var, api::Sort sort);
  /** returns the declared variable */
  api::Term getVar() const;
  /** returns the declared variable's sort */
  api::Sort getSort() const;
  /** invokes this command
   *
   * The declared sygus variable is communicated to the SMT engine in case a
   * synthesis conjecture is built later on.
   */
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  /** creates a copy of this command */
  Command* clone() const override;
  /** returns this command's name */
  std::string getCommandName() const override;
  /** prints this command */
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** the declared variable */
  api::Term d_var;
  /** the declared variable's sort */
  api::Sort d_sort;
};

/** Declares a sygus function-to-synthesize
 *
 * This command is also used for the special case in which we are declaring an
 * invariant-to-synthesize
 */
class CVC4_EXPORT SynthFunCommand : public DeclarationDefinitionCommand
{
 public:
  SynthFunCommand(const std::string& id,
                  api::Term fun,
                  const std::vector<api::Term>& vars,
                  api::Sort sort,
                  bool isInv,
                  api::Grammar* g);
  /** returns the function-to-synthesize */
  api::Term getFunction() const;
  /** returns the input variables of the function-to-synthesize */
  const std::vector<api::Term>& getVars() const;
  /** returns the sygus sort of the function-to-synthesize */
  api::Sort getSort() const;
  /** returns whether the function-to-synthesize should be an invariant */
  bool isInv() const;
  /** Get the sygus grammar given for the synth fun command */
  const api::Grammar* getGrammar() const;

  /** invokes this command
   *
   * The declared function-to-synthesize is communicated to the SMT engine in
   * case a synthesis conjecture is built later on.
   */
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  /** creates a copy of this command */
  Command* clone() const override;
  /** returns this command's name */
  std::string getCommandName() const override;
  /** prints this command */
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** the function-to-synthesize */
  api::Term d_fun;
  /** the input variables of the function-to-synthesize */
  std::vector<api::Term> d_vars;
  /** sort of the function-to-synthesize */
  api::Sort d_sort;
  /** whether the function-to-synthesize should be an invariant */
  bool d_isInv;
  /** optional grammar for the possible values of the function-to-sytnhesize */
  api::Grammar* d_grammar;
};

/** Declares a sygus constraint */
class CVC4_EXPORT SygusConstraintCommand : public Command
{
 public:
  SygusConstraintCommand(const api::Term& t);
  /** returns the declared constraint */
  api::Term getTerm() const;
  /** invokes this command
   *
   * The declared constraint is communicated to the SMT engine in case a
   * synthesis conjecture is built later on.
   */
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  /** creates a copy of this command */
  Command* clone() const override;
  /** returns this command's name */
  std::string getCommandName() const override;
  /** prints this command */
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** the declared constraint */
  api::Term d_term;
};

/** Declares a sygus invariant constraint
 *
 * Invarint constraints are declared in a somewhat implicit manner in the SyGuS
 * language: they are declared in terms of the previously declared
 * invariant-to-synthesize, precondition, transition relation and condition.
 *
 * The actual constraint must be built such that the invariant is not stronger
 * than the precondition, not weaker than the postcondition and inductive
 * w.r.t. the transition relation.
 */
class CVC4_EXPORT SygusInvConstraintCommand : public Command
{
 public:
  SygusInvConstraintCommand(const std::vector<api::Term>& predicates);
  SygusInvConstraintCommand(const api::Term& inv,
                            const api::Term& pre,
                            const api::Term& trans,
                            const api::Term& post);
  /** returns the place holder predicates */
  const std::vector<api::Term>& getPredicates() const;
  /** invokes this command
   *
   * The place holders are communicated to the SMT engine and the actual
   * invariant constraint is built, in case an actual synthesis conjecture is
   * built later on.
   */
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  /** creates a copy of this command */
  Command* clone() const override;
  /** returns this command's name */
  std::string getCommandName() const override;
  /** prints this command */
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** the place holder predicates with which to build the actual constraint
   * (i.e. the invariant, precondition, transition relation and postcondition)
   */
  std::vector<api::Term> d_predicates;
};

/** Declares a synthesis conjecture */
class CVC4_EXPORT CheckSynthCommand : public Command
{
 public:
  CheckSynthCommand(){};
  /** returns the result of the check-synth call */
  api::Result getResult() const;
  /** prints the result of the check-synth-call */
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  /** invokes this command
   *
   * This invocation makes the SMT engine build a synthesis conjecture based on
   * previously declared information (such as universal variables,
   * functions-to-synthesize and so on), set up attributes to guide the solving,
   * and then perform a satisfiability check, whose result is stored in
   * d_result.
   */
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  /** creates a copy of this command */
  Command* clone() const override;
  /** returns this command's name */
  std::string getCommandName() const override;
  /** prints this command */
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** result of the check-synth call */
  api::Result d_result;
  /** string stream that stores the output of the solution */
  std::stringstream d_solution;
};

/* ------------------- sygus commands  ------------------ */

// this is TRANSFORM in the CVC presentation language
class CVC4_EXPORT SimplifyCommand : public Command
{
 protected:
  api::Term d_term;
  api::Term d_result;

 public:
  SimplifyCommand(api::Term term);

  api::Term getTerm() const;
  api::Term getResult() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SimplifyCommand */

class CVC4_EXPORT GetValueCommand : public Command
{
 protected:
  std::vector<api::Term> d_terms;
  api::Term d_result;

 public:
  GetValueCommand(api::Term term);
  GetValueCommand(const std::vector<api::Term>& terms);

  const std::vector<api::Term>& getTerms() const;
  api::Term getResult() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetValueCommand */

class CVC4_EXPORT GetAssignmentCommand : public Command
{
 protected:
  api::Term d_result;

 public:
  GetAssignmentCommand();

  api::Term getResult() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetAssignmentCommand */

class CVC4_EXPORT GetModelCommand : public Command
{
 public:
  GetModelCommand();

  // Model is private to the library -- for now
  // Model* getResult() const ;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  smt::Model* d_result;
}; /* class GetModelCommand */

/** The command to block models. */
class CVC4_EXPORT BlockModelCommand : public Command
{
 public:
  BlockModelCommand();

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class BlockModelCommand */

/** The command to block model values. */
class CVC4_EXPORT BlockModelValuesCommand : public Command
{
 public:
  BlockModelValuesCommand(const std::vector<api::Term>& terms);

  const std::vector<api::Term>& getTerms() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** The terms we are blocking */
  std::vector<api::Term> d_terms;
}; /* class BlockModelValuesCommand */

class CVC4_EXPORT GetProofCommand : public Command
{
 public:
  GetProofCommand();

  void invoke(api::Solver* solver, SymbolManager* sm) override;

  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;

  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 private:
  /** the result of the getProof call */
  std::string d_result;
}; /* class GetProofCommand */

class CVC4_EXPORT GetInstantiationsCommand : public Command
{
 public:
  GetInstantiationsCommand();

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  api::Solver* d_solver;
}; /* class GetInstantiationsCommand */

class CVC4_EXPORT GetSynthSolutionCommand : public Command
{
 public:
  GetSynthSolutionCommand();

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  api::Solver* d_solver;
}; /* class GetSynthSolutionCommand */

/** The command (get-interpol s B (G)?)
 *
 * This command asks for an interpolant from the current set of assertions and
 * conjecture (goal) B.
 *
 * The symbol s is the name for the interpolation predicate. If we successfully
 * find a predicate P, then the output response of this command is: (define-fun
 * s () Bool P)
 */
class CVC4_EXPORT GetInterpolCommand : public Command
{
 public:
  GetInterpolCommand(const std::string& name, api::Term conj);
  /** The argument g is the grammar of the interpolation query */
  GetInterpolCommand(const std::string& name, api::Term conj, api::Grammar* g);

  /** Get the conjecture of the interpolation query */
  api::Term getConjecture() const;
  /** Get the sygus grammar given for the interpolation query */
  const api::Grammar* getGrammar() const;
  /** Get the result of the query, which is the solution to the interpolation
   * query. */
  api::Term getResult() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** The name of the interpolation predicate */
  std::string d_name;
  /** The conjecture of the interpolation query */
  api::Term d_conj;
  /** The (optional) grammar of the interpolation query */
  api::Grammar* d_sygus_grammar;
  /** the return status of the command */
  bool d_resultStatus;
  /** the return expression of the command */
  api::Term d_result;
}; /* class GetInterpolCommand */

/** The command (get-abduct s B (G)?)
 *
 * This command asks for an abduct from the current set of assertions and
 * conjecture (goal) given by the argument B.
 *
 * The symbol s is the name for the abduction predicate. If we successfully
 * find a predicate P, then the output response of this command is:
 *   (define-fun s () Bool P)
 *
 * A grammar G can be optionally provided to indicate the syntactic restrictions
 * on the possible solutions returned.
 */
class CVC4_EXPORT GetAbductCommand : public Command
{
 public:
  GetAbductCommand(const std::string& name, api::Term conj);
  GetAbductCommand(const std::string& name, api::Term conj, api::Grammar* g);

  /** Get the conjecture of the abduction query */
  api::Term getConjecture() const;
  /** Get the grammar given for the abduction query */
  const api::Grammar* getGrammar() const;
  /** Get the name of the abduction predicate for the abduction query */
  std::string getAbductName() const;
  /** Get the result of the query, which is the solution to the abduction query.
   */
  api::Term getResult() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** The name of the abduction predicate */
  std::string d_name;
  /** The conjecture of the abduction query */
  api::Term d_conj;
  /** The (optional) grammar of the abduction query */
  api::Grammar* d_sygus_grammar;
  /** the return status of the command */
  bool d_resultStatus;
  /** the return expression of the command */
  api::Term d_result;
}; /* class GetAbductCommand */

class CVC4_EXPORT GetQuantifierEliminationCommand : public Command
{
 protected:
  api::Term d_term;
  bool d_doFull;
  api::Term d_result;

 public:
  GetQuantifierEliminationCommand();
  GetQuantifierEliminationCommand(const api::Term& term, bool doFull);

  api::Term getTerm() const;
  bool getDoFull() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  api::Term getResult() const;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;

  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetQuantifierEliminationCommand */

class CVC4_EXPORT GetUnsatAssumptionsCommand : public Command
{
 public:
  GetUnsatAssumptionsCommand();
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  std::vector<api::Term> getResult() const;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  std::vector<api::Term> d_result;
}; /* class GetUnsatAssumptionsCommand */

class CVC4_EXPORT GetUnsatCoreCommand : public Command
{
 public:
  GetUnsatCoreCommand();
  const std::vector<api::Term>& getUnsatCore() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;

  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;

 protected:
  /** The symbol manager we were invoked with */
  SymbolManager* d_sm;
  /** the result of the unsat core call */
  std::vector<api::Term> d_result;
}; /* class GetUnsatCoreCommand */

class CVC4_EXPORT GetAssertionsCommand : public Command
{
 protected:
  std::string d_result;

 public:
  GetAssertionsCommand();

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  std::string getResult() const;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetAssertionsCommand */

class CVC4_EXPORT SetBenchmarkStatusCommand : public Command
{
 protected:
  BenchmarkStatus d_status;

 public:
  SetBenchmarkStatusCommand(BenchmarkStatus status);

  BenchmarkStatus getStatus() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetBenchmarkStatusCommand */

class CVC4_EXPORT SetBenchmarkLogicCommand : public Command
{
 protected:
  std::string d_logic;

 public:
  SetBenchmarkLogicCommand(std::string logic);

  std::string getLogic() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetBenchmarkLogicCommand */

class CVC4_EXPORT SetInfoCommand : public Command
{
 protected:
  std::string d_flag;
  std::string d_value;

 public:
  SetInfoCommand(const std::string& flag, const std::string& value);

  const std::string& getFlag() const;
  const std::string& getValue() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetInfoCommand */

class CVC4_EXPORT GetInfoCommand : public Command
{
 protected:
  std::string d_flag;
  std::string d_result;

 public:
  GetInfoCommand(std::string flag);

  std::string getFlag() const;
  std::string getResult() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetInfoCommand */

class CVC4_EXPORT SetOptionCommand : public Command
{
 protected:
  std::string d_flag;
  std::string d_value;

 public:
  SetOptionCommand(const std::string& flag, const std::string& value);

  const std::string& getFlag() const;
  const std::string& getValue() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetOptionCommand */

class CVC4_EXPORT GetOptionCommand : public Command
{
 protected:
  std::string d_flag;
  std::string d_result;

 public:
  GetOptionCommand(std::string flag);

  std::string getFlag() const;
  std::string getResult() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetOptionCommand */

class CVC4_EXPORT DatatypeDeclarationCommand : public Command
{
 private:
  std::vector<api::Sort> d_datatypes;

 public:
  DatatypeDeclarationCommand(const api::Sort& datatype);

  DatatypeDeclarationCommand(const std::vector<api::Sort>& datatypes);
  const std::vector<api::Sort>& getDatatypes() const;
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DatatypeDeclarationCommand */

class CVC4_EXPORT ResetCommand : public Command
{
 public:
  ResetCommand() {}
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ResetCommand */

class CVC4_EXPORT ResetAssertionsCommand : public Command
{
 public:
  ResetAssertionsCommand() {}
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ResetAssertionsCommand */

class CVC4_EXPORT QuitCommand : public Command
{
 public:
  QuitCommand() {}
  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class QuitCommand */

class CVC4_EXPORT CommentCommand : public Command
{
  std::string d_comment;

 public:
  CommentCommand(std::string comment);

  std::string getComment() const;

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class CommentCommand */

class CVC4_EXPORT CommandSequence : public Command
{
 protected:
  /** 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 clear();

  void invoke(api::Solver* solver, SymbolManager* sm) override;
  void invoke(api::Solver* solver,
              SymbolManager* sm,
              std::ostream& out) override;

  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();

  Command* clone() const override;
  std::string getCommandName() const override;
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class CommandSequence */

class CVC4_EXPORT DeclarationSequence : public CommandSequence
{
  void toStream(
      std::ostream& out,
      int toDepth = -1,
      size_t dag = 1,
      OutputLanguage language = language::output::LANG_AUTO) const override;
};

}  // namespace cvc5

#endif /* CVC5__COMMAND_H */