/******************************************************************************

 * 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 SolverEngines.

 *

 * Command objects are generated by the parser (typically) to implement the

 * commands in parsed input (see Parser::parseNextCommand()), or by client

 * code.

 */

#include "cvc5_public.h"

#ifndef CVC5__COMMAND_H

#define CVC5__COMMAND_H

#include <iosfwd>

#include <sstream>

#include <string>

#include <vector>

#include "api/cpp/cvc5.h"

#include "cvc5_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) CVC5_EXPORT;

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

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

std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC5_EXPORT;

std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC5_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) CVC5_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 CVC5_EXPORT CommandPrintSuccess

{

 public:

  /** Construct a CommandPrintSuccess with the given setting. */

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

{

 protected:

  // shouldn't construct a CommandStatus (use a derived class)

 public:

  void toStream(std::ostream& out,

                Language language = Language::LANG_AUTO) const;

  virtual CommandStatus& clone() const = 0;

}; /* class CommandStatus */

{

  static const CommandSuccess* s_instance;

 public:

  {

  }

}; /* class CommandSuccess */

{

  static const CommandInterrupted* s_instance;

 public:

  static const CommandInterrupted* instance() { return s_instance; }

  {

  }

}; /* class CommandInterrupted */

{

 public:

  {

  }

}; /* class CommandSuccess */

{

  std::string d_message;

 public:

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

 */

{

  std::string d_message;

 public:

  {

  }

}; /* class CommandRecoverableFailure */

class CVC5_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,

                        Language language = Language::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.

   */

  /**

   * Determine whether this Command will print a success message.

   */

  /**

   * 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). */

  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;

  /**

   * Reset the given solver in-place (keep the object at the same memory

   * location).

   */

  static void resetSolver(api::Solver* solver);

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

}; /* class Command */

/**

 * EmptyCommands are the residue of a command after the parser handles

 * them (and there's nothing left to do).

 */

{

 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,

                Language language = Language::LANG_AUTO) const override;

 protected:

  std::string d_name;

}; /* class EmptyCommand */

{

 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,

                Language language = Language::LANG_AUTO) const override;

 protected:

  std::string d_output;

}; /* class EchoCommand */

{

 protected:

  api::Term d_term;

 public:

  AssertCommand(const api::Term& t);

  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,

                Language language = Language::LANG_AUTO) const override;

}; /* class AssertCommand */

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class PushCommand */

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class PopCommand */

{

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

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class DeclareFunctionCommand */

{

 protected:

  api::Term d_func;

  api::Sort d_sort;

  std::vector<api::Term> d_initValue;

 public:

  DeclarePoolCommand(const std::string& id,

                     api::Term func,

                     api::Sort sort,

                     const std::vector<api::Term>& initValue);

  api::Term getFunction() const;

  api::Sort getSort() const;

  const std::vector<api::Term>& getInitialValue() 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class DeclarePoolCommand */

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class DeclareSortCommand */

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class DefineSortCommand */

{

 public:

  DefineFunctionCommand(const std::string& id,

                        api::Sort sort,

                        api::Term formula);

  DefineFunctionCommand(const std::string& id,

                        const std::vector<api::Term>& formals,

                        api::Sort sort,

                        api::Term formula);

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

  api::Sort getSort() 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,

                Language language = Language::LANG_AUTO) const override;

 protected:

  /** The formal arguments for the function we are defining */

  std::vector<api::Term> d_formals;

  /** The co-domain sort of the function we are defining */

  api::Sort d_sort;

  /** The formula corresponding to the body of the function we are defining */

  api::Term d_formula;

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

 */

{

 public:

  DefineFunctionRecCommand(api::Term func,

                           const std::vector<api::Term>& formals,

                           api::Term formula);

  DefineFunctionRecCommand(const std::vector<api::Term>& funcs,

                           const std::vector<std::vector<api::Term> >& formals,

                           const std::vector<api::Term>& formula);

  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,

                Language language = Language::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;

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

 */

{

 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,

                Language language = Language::LANG_AUTO) const override;

 protected:

  /** The location sort */

  api::Sort d_locSort;

  /** The data sort */

  api::Sort d_dataSort;

};

/**

 * The command when parsing check-sat.

 * This command will check satisfiability of the input formula.

 */

{

 public:

  CheckSatCommand();

  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,

                Language language = Language::LANG_AUTO) const override;

 private:

  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.

 */

{

 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,

                Language language = Language::LANG_AUTO) const override;

 private:

  std::vector<api::Term> d_terms;

  api::Result d_result;

}; /* class CheckSatAssumingCommand */

{

 protected:

  api::Term d_term;

  api::Result d_result;

 public:

  QueryCommand(const api::Term& t);

  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,

                Language language = Language::LANG_AUTO) const override;

}; /* class QueryCommand */

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

/** Declares a sygus universal variable */

{

 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,

                Language language = Language::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

 */

{

 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,

                Language language = Language::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 */

{

 public:

  SygusConstraintCommand(const api::Term& t, bool isAssume = false);

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

                Language language = Language::LANG_AUTO) const override;

 protected:

  /** the declared constraint */

  api::Term d_term;

  /** true if this is a sygus assumption */

  bool d_isAssume;

};

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

 */

{

 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,

                Language language = Language::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 */

{

 public:

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

                Language language = Language::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

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class SimplifyCommand */

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class GetValueCommand */

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class GetAssignmentCommand */

{

 public:

  GetModelCommand();

  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,

                Language language = Language::LANG_AUTO) const override;

 protected:

  /** Result of printing the model */

  std::string d_result;

}; /* class GetModelCommand */

/** The command to block models. */

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class BlockModelCommand */

/** The command to block model values. */

{

 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,

                Language language = Language::LANG_AUTO) const override;

 protected:

  /** The terms we are blocking */

  std::vector<api::Term> d_terms;

}; /* class BlockModelValuesCommand */

{

 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,

                Language language = Language::LANG_AUTO) const override;

 private:

  /** the result of the getProof call */

  std::string d_result;

}; /* class GetProofCommand */

{

 public:

  GetInstantiationsCommand();

  static bool isEnabled(api::Solver* solver, const api::Result& res);

  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,

                Language language = Language::LANG_AUTO) const override;

 protected:

  api::Solver* d_solver;

}; /* class GetInstantiationsCommand */

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

 */

{

 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,

                Language language = Language::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.

 */

{

 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,

                Language language = Language::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 */

{

 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,

                Language language = Language::LANG_AUTO) const override;

}; /* class GetQuantifierEliminationCommand */

{

 public: