Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	src/smt/command.cpp	Lines:	693	1272	54.5 %
Date:	2021-08-06	Branches:	514	1565	32.8 %

/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Abdalrhman Mohamed, Morgan Deters
 *
 * 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 command objects.
 */

#include "smt/command.h"

#include <exception>
#include <iostream>
#include <iterator>
#include <sstream>
#include <utility>
#include <vector>

#include "api/cpp/cvc5.h"
#include "base/check.h"
#include "base/modal_exception.h"
#include "base/output.h"
#include "expr/expr_iomanip.h"
#include "expr/node.h"
#include "expr/symbol_manager.h"
#include "expr/type_node.h"
#include "options/options.h"
#include "options/main_options.h"
#include "options/printer_options.h"
#include "options/smt_options.h"
#include "printer/printer.h"
#include "proof/unsat_core.h"
#include "smt/dump.h"
#include "smt/model.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "util/unsafe_interrupt_exception.h"
#include "util/utility.h"

using namespace std;

namespace cvc5 {

std::string sexprToString(api::Term sexpr)
{
  // if sexpr is a constant string, return the stored constant string. We don't
  // call Term::toString as its result depends on the output language.
  // Notice that we only check for string constants. The sexprs generated by the
  // parser don't contains other constants, so we can ignore them.
  if (sexpr.isStringValue())
  {
    // convert std::wstring to std::string
    std::wstring wstring = sexpr.getStringValue();
    return std::string(wstring.cbegin(), wstring.cend());
  }

  // if sexpr is not a spec constant, make sure it is an array of sub-sexprs
  Assert(sexpr.getKind() == api::SEXPR);

  std::stringstream ss;
  auto it = sexpr.begin();

  // recursively print the sub-sexprs
  ss << '(' << sexprToString(*it);
  ++it;
  while (it != sexpr.end())
  {
    ss << ' ' << sexprToString(*it);
    ++it;
  }
  ss << ')';

  return ss.str();
}

const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
const CommandInterrupted* CommandInterrupted::s_instance =
    new CommandInterrupted();

std::ostream& operator<<(std::ostream& out, const Command& c)
{
  c.toStream(out,
             Node::setdepth::getDepth(out),
             Node::dag::getDag(out),
             Node::setlanguage::getLanguage(out));
  return out;
}

ostream& operator<<(ostream& out, const Command* c)
{
  if (c == NULL)
  {
    out << "null";
  }
  else
  {
    out << *c;
  }
  return out;
}

std::ostream& operator<<(std::ostream& out, const CommandStatus& s)
{
  s.toStream(out, Node::setlanguage::getLanguage(out));
  return out;
}

ostream& operator<<(ostream& out, const CommandStatus* s)
{
  if (s == NULL)
  {
    out << "null";
  }
  else
  {
    out << *s;
  }
  return out;
}

/* output stream insertion operator for benchmark statuses */
std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
{
  switch (status)
  {
    case SMT_SATISFIABLE: return out << "sat";

    case SMT_UNSATISFIABLE: return out << "unsat";

    case SMT_UNKNOWN: return out << "unknown";

    default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
  }
}

/* -------------------------------------------------------------------------- */
/* class CommandPrintSuccess                                                  */
/* -------------------------------------------------------------------------- */

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

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

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

std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
{
  cps.applyPrintSuccess(out);
  return out;
}

/* -------------------------------------------------------------------------- */
/* class Command                                                              */
/* -------------------------------------------------------------------------- */

Command::Command() : d_commandStatus(nullptr), d_muted(false) {}

Command::Command(const Command& cmd)
{
  d_commandStatus =
      (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
  d_muted = cmd.d_muted;
}

Command::~Command()
{
  if (d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance())
  {
    delete d_commandStatus;
  }
}

bool Command::ok() const
{
  // either we haven't run the command yet, or it ran successfully
  return d_commandStatus == NULL
         || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
}

bool Command::fail() const
{
  return d_commandStatus != NULL
         && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
}

bool Command::interrupted() const
{
  return d_commandStatus != NULL
         && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
}

void Command::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out)
{
  invoke(solver, sm);
  if (!(isMuted() && ok()))
  {
    printResult(
        out,
        std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
  }
}

std::string Command::toString() const
{
  std::stringstream ss;
  toStream(ss);
  return ss.str();
}

void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const
{
  Printer::getPrinter(language)->toStream(out, this);
}

void Command::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (d_commandStatus != NULL)
  {
    if ((!ok() && verbosity >= 1) || verbosity >= 2)
    {
      out << *d_commandStatus;
    }
  }
}

void Command::resetSolver(api::Solver* solver)
{
  std::unique_ptr<Options> opts = std::make_unique<Options>();
  opts->copyValues(*solver->d_originalOptions);
  // This reconstructs a new solver object at the same memory location as the
  // current one. Note that this command does not own the solver object!
  // It may be safer to instead make the ResetCommand a special case in the
  // CommandExecutor such that this reconstruction can be done within the
  // CommandExecutor, who actually owns the solver.
  solver->~Solver();
  new (solver) api::Solver(opts.get());
}

Node Command::termToNode(const api::Term& term) { return term.getNode(); }

std::vector<Node> Command::termVectorToNodes(
    const std::vector<api::Term>& terms)
{
  return api::Term::termVectorToNodes(terms);
}

TypeNode Command::sortToTypeNode(const api::Sort& sort)
{
  return sort.getTypeNode();
}

std::vector<TypeNode> Command::sortVectorToTypeNodes(
    const std::vector<api::Sort>& sorts)
{
  return api::Sort::sortVectorToTypeNodes(sorts);
}

TypeNode Command::grammarToTypeNode(api::Grammar* grammar)
{
  return grammar == nullptr ? TypeNode::null()
                            : sortToTypeNode(grammar->resolve());
}

Options& Command::getOriginalOptionsFrom(api::Solver* s)
{
  return *s->d_originalOptions.get();
}

/* -------------------------------------------------------------------------- */
/* class EmptyCommand                                                         */
/* -------------------------------------------------------------------------- */

EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
std::string EmptyCommand::getName() const { return d_name; }
void EmptyCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  /* empty commands have no implementation */
  d_commandStatus = CommandSuccess::instance();
}

Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
std::string EmptyCommand::getCommandName() const { return "empty"; }

void EmptyCommand::toStream(std::ostream& out,
                            int toDepth,
                            size_t dag,
                            OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
}

/* -------------------------------------------------------------------------- */
/* class EchoCommand                                                          */
/* -------------------------------------------------------------------------- */

EchoCommand::EchoCommand(std::string output)
{
  // escape all double-quotes
  size_t pos = 0;
  while ((pos = output.find('"', pos)) != string::npos)
  {
    output.replace(pos, 1, "\"\"");
    pos += 2;
  }
  d_output = '"' + output + '"';
}

std::string EchoCommand::getOutput() const { return d_output; }
void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  /* we don't have an output stream here, nothing to do */
  d_commandStatus = CommandSuccess::instance();
}

void EchoCommand::invoke(api::Solver* solver,
                         SymbolManager* sm,
                         std::ostream& out)
{
  out << d_output << std::endl;
  Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
                           << std::endl;
  d_commandStatus = CommandSuccess::instance();
  printResult(
      out,
      std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
}

Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
std::string EchoCommand::getCommandName() const { return "echo"; }

void EchoCommand::toStream(std::ostream& out,
                           int toDepth,
                           size_t dag,
                           OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
}

/* -------------------------------------------------------------------------- */
/* class AssertCommand                                                        */
/* -------------------------------------------------------------------------- */

AssertCommand::AssertCommand(const api::Term& t) : d_term(t) {}

api::Term AssertCommand::getTerm() const { return d_term; }
void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->assertFormula(d_term);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* AssertCommand::clone() const { return new AssertCommand(d_term); }

std::string AssertCommand::getCommandName() const { return "assert"; }

void AssertCommand::toStream(std::ostream& out,
                             int toDepth,
                             size_t dag,
                             OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdAssert(out, termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class PushCommand                                                          */
/* -------------------------------------------------------------------------- */

void PushCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->push();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* PushCommand::clone() const { return new PushCommand(); }
std::string PushCommand::getCommandName() const { return "push"; }

void PushCommand::toStream(std::ostream& out,
                           int toDepth,
                           size_t dag,
                           OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdPush(out);
}

/* -------------------------------------------------------------------------- */
/* class PopCommand                                                           */
/* -------------------------------------------------------------------------- */

void PopCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->pop();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* PopCommand::clone() const { return new PopCommand(); }
std::string PopCommand::getCommandName() const { return "pop"; }

void PopCommand::toStream(std::ostream& out,
                          int toDepth,
                          size_t dag,
                          OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdPop(out);
}

/* -------------------------------------------------------------------------- */
/* class CheckSatCommand                                                      */
/* -------------------------------------------------------------------------- */

CheckSatCommand::CheckSatCommand() : d_term() {}

CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {}

api::Term CheckSatCommand::getTerm() const { return d_term; }
void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
                           << std::endl;
  try
  {
    d_result =
        d_term.isNull() ? solver->checkSat() : solver->checkSatAssuming(d_term);

    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Result CheckSatCommand::getResult() const { return d_result; }
void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    Trace("dtview::command") << "* RESULT: " << d_result << std::endl;
    out << d_result << endl;
  }
}

Command* CheckSatCommand::clone() const
{
  CheckSatCommand* c = new CheckSatCommand(d_term);
  c->d_result = d_result;
  return c;
}

std::string CheckSatCommand::getCommandName() const { return "check-sat"; }

void CheckSatCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
                               OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdCheckSat(out, termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class CheckSatAssumingCommand                                              */
/* -------------------------------------------------------------------------- */

CheckSatAssumingCommand::CheckSatAssumingCommand(api::Term term)
    : d_terms({term})
{
}

CheckSatAssumingCommand::CheckSatAssumingCommand(
    const std::vector<api::Term>& terms)
    : d_terms(terms)
{
}

const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const
{
  return d_terms;
}

void CheckSatAssumingCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
                           << " )~" << std::endl;
  try
  {
    d_result = solver->checkSatAssuming(d_terms);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Result CheckSatAssumingCommand::getResult() const
{
  Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
  return d_result;
}

void CheckSatAssumingCommand::printResult(std::ostream& out,
                                          uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    out << d_result << endl;
  }
}

Command* CheckSatAssumingCommand::clone() const
{
  CheckSatAssumingCommand* c = new CheckSatAssumingCommand(d_terms);
  c->d_result = d_result;
  return c;
}

std::string CheckSatAssumingCommand::getCommandName() const
{
  return "check-sat-assuming";
}

void CheckSatAssumingCommand::toStream(std::ostream& out,
                                       int toDepth,
                                       size_t dag,
                                       OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(
      out, termVectorToNodes(d_terms));
}

/* -------------------------------------------------------------------------- */
/* class QueryCommand                                                         */
/* -------------------------------------------------------------------------- */

QueryCommand::QueryCommand(const api::Term& t) : d_term(t) {}

api::Term QueryCommand::getTerm() const { return d_term; }
void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_result = solver->checkEntailed(d_term);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Result QueryCommand::getResult() const { return d_result; }
void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    out << d_result << endl;
  }
}

Command* QueryCommand::clone() const
{
  QueryCommand* c = new QueryCommand(d_term);
  c->d_result = d_result;
  return c;
}

std::string QueryCommand::getCommandName() const { return "query"; }

void QueryCommand::toStream(std::ostream& out,
                            int toDepth,
                            size_t dag,
                            OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdQuery(out, termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class DeclareSygusVarCommand */
/* -------------------------------------------------------------------------- */

DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
                                               api::Term var,
                                               api::Sort sort)
    : DeclarationDefinitionCommand(id), d_var(var), d_sort(sort)
{
}

api::Term DeclareSygusVarCommand::getVar() const { return d_var; }
api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; }

void DeclareSygusVarCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  d_commandStatus = CommandSuccess::instance();
}

Command* DeclareSygusVarCommand::clone() const
{
  return new DeclareSygusVarCommand(d_symbol, d_var, d_sort);
}

std::string DeclareSygusVarCommand::getCommandName() const
{
  return "declare-var";
}

void DeclareSygusVarCommand::toStream(std::ostream& out,
                                      int toDepth,
                                      size_t dag,
                                      OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdDeclareVar(
      out, termToNode(d_var), sortToTypeNode(d_sort));
}

/* -------------------------------------------------------------------------- */
/* class SynthFunCommand                                                      */
/* -------------------------------------------------------------------------- */

SynthFunCommand::SynthFunCommand(const std::string& id,
                                 api::Term fun,
                                 const std::vector<api::Term>& vars,
                                 api::Sort sort,
                                 bool isInv,
                                 api::Grammar* g)
    : DeclarationDefinitionCommand(id),
      d_fun(fun),
      d_vars(vars),
      d_sort(sort),
      d_isInv(isInv),
      d_grammar(g)
{
}

api::Term SynthFunCommand::getFunction() const { return d_fun; }

const std::vector<api::Term>& SynthFunCommand::getVars() const
{
  return d_vars;
}

api::Sort SynthFunCommand::getSort() const { return d_sort; }
bool SynthFunCommand::isInv() const { return d_isInv; }

const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }

void SynthFunCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  sm->addFunctionToSynthesize(d_fun);
  d_commandStatus = CommandSuccess::instance();
}

Command* SynthFunCommand::clone() const
{
  return new SynthFunCommand(
      d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
}

std::string SynthFunCommand::getCommandName() const
{
  return d_isInv ? "synth-inv" : "synth-fun";
}

void SynthFunCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
                               OutputLanguage language) const
{
  std::vector<Node> nodeVars = termVectorToNodes(d_vars);
  Printer::getPrinter(language)->toStreamCmdSynthFun(
      out,
      termToNode(d_fun),
      nodeVars,
      d_isInv,
      d_grammar == nullptr ? TypeNode::null() : grammarToTypeNode(d_grammar));
}

/* -------------------------------------------------------------------------- */
/* class SygusConstraintCommand */
/* -------------------------------------------------------------------------- */

SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
{
}

void SygusConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->addSygusConstraint(d_term);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Term SygusConstraintCommand::getTerm() const { return d_term; }

Command* SygusConstraintCommand::clone() const
{
  return new SygusConstraintCommand(d_term);
}

std::string SygusConstraintCommand::getCommandName() const
{
  return "constraint";
}

void SygusConstraintCommand::toStream(std::ostream& out,
                                      int toDepth,
                                      size_t dag,
                                      OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdConstraint(out, termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class SygusInvConstraintCommand */
/* -------------------------------------------------------------------------- */

SygusInvConstraintCommand::SygusInvConstraintCommand(
    const std::vector<api::Term>& predicates)
    : d_predicates(predicates)
{
}

SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv,
                                                     const api::Term& pre,
                                                     const api::Term& trans,
                                                     const api::Term& post)
    : SygusInvConstraintCommand(std::vector<api::Term>{inv, pre, trans, post})
{
}

void SygusInvConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->addSygusInvConstraint(
        d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

const std::vector<api::Term>& SygusInvConstraintCommand::getPredicates() const
{
  return d_predicates;
}

Command* SygusInvConstraintCommand::clone() const
{
  return new SygusInvConstraintCommand(d_predicates);
}

std::string SygusInvConstraintCommand::getCommandName() const
{
  return "inv-constraint";
}

void SygusInvConstraintCommand::toStream(std::ostream& out,
                                         int toDepth,
                                         size_t dag,
                                         OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdInvConstraint(
      out,
      termToNode(d_predicates[0]),
      termToNode(d_predicates[1]),
      termToNode(d_predicates[2]),
      termToNode(d_predicates[3]));
}

/* -------------------------------------------------------------------------- */
/* class CheckSynthCommand                                                    */
/* -------------------------------------------------------------------------- */

void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_result = solver->checkSynth();
    d_commandStatus = CommandSuccess::instance();
    d_solution.clear();
    // check whether we should print the status
    if (!d_result.isUnsat()
        || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF
        || options::sygusOut() == options::SygusSolutionOutMode::STATUS)
    {
      if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD)
      {
        d_solution << "fail" << endl;
      }
      else
      {
        d_solution << d_result << endl;
      }
    }
    // check whether we should print the solution
    if (d_result.isUnsat()
        && options::sygusOut() != options::SygusSolutionOutMode::STATUS)
    {
      std::vector<api::Term> synthFuns = sm->getFunctionsToSynthesize();
      d_solution << "(" << std::endl;
      Printer* p = Printer::getPrinter(language::output::LANG_SYGUS_V2);
      for (api::Term& f : synthFuns)
      {
        api::Term sol = solver->getSynthSolution(f);
        std::vector<api::Term> formals;
        if (sol.getKind() == api::LAMBDA)
        {
          formals.insert(formals.end(), sol[0].begin(), sol[0].end());
          sol = sol[1];
        }
        api::Sort rangeSort = f.getSort();
        if (rangeSort.isFunction())
        {
          rangeSort = rangeSort.getFunctionCodomainSort();
        }
        p->toStreamCmdDefineFunction(d_solution,
                                     f.toString(),
                                     termVectorToNodes(formals),
                                     sortToTypeNode(rangeSort),
                                     termToNode(sol));
      }
      d_solution << ")" << std::endl;
    }
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Result CheckSynthCommand::getResult() const { return d_result; }
void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    out << d_solution.str();
  }
}

Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }

std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }

void CheckSynthCommand::toStream(std::ostream& out,
                                 int toDepth,
                                 size_t dag,
                                 OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
}

/* -------------------------------------------------------------------------- */
/* class ResetCommand                                                         */
/* -------------------------------------------------------------------------- */

void ResetCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    sm->reset();
    resetSolver(solver);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* ResetCommand::clone() const { return new ResetCommand(); }
std::string ResetCommand::getCommandName() const { return "reset"; }

void ResetCommand::toStream(std::ostream& out,
                            int toDepth,
                            size_t dag,
                            OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdReset(out);
}

/* -------------------------------------------------------------------------- */
/* class ResetAssertionsCommand                                               */
/* -------------------------------------------------------------------------- */

void ResetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    sm->resetAssertions();
    solver->resetAssertions();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* ResetAssertionsCommand::clone() const
{
  return new ResetAssertionsCommand();
}

std::string ResetAssertionsCommand::getCommandName() const
{
  return "reset-assertions";
}

void ResetAssertionsCommand::toStream(std::ostream& out,
                                      int toDepth,
                                      size_t dag,
                                      OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
}

/* -------------------------------------------------------------------------- */
/* class QuitCommand                                                          */
/* -------------------------------------------------------------------------- */

void QuitCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  Dump("benchmark") << *this;
  d_commandStatus = CommandSuccess::instance();
}

Command* QuitCommand::clone() const { return new QuitCommand(); }
std::string QuitCommand::getCommandName() const { return "exit"; }

void QuitCommand::toStream(std::ostream& out,
                           int toDepth,
                           size_t dag,
                           OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdQuit(out);
}

/* -------------------------------------------------------------------------- */
/* class CommentCommand                                                       */
/* -------------------------------------------------------------------------- */

CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
std::string CommentCommand::getComment() const { return d_comment; }
void CommentCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  Dump("benchmark") << *this;
  d_commandStatus = CommandSuccess::instance();
}

Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
std::string CommentCommand::getCommandName() const { return "comment"; }

void CommentCommand::toStream(std::ostream& out,
                              int toDepth,
                              size_t dag,
                              OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
}

/* -------------------------------------------------------------------------- */
/* class CommandSequence                                                      */
/* -------------------------------------------------------------------------- */

CommandSequence::CommandSequence() : d_index(0) {}
CommandSequence::~CommandSequence()
{
  for (unsigned i = d_index; i < d_commandSequence.size(); ++i)
  {
    delete d_commandSequence[i];
  }
}

void CommandSequence::addCommand(Command* cmd)
{
  d_commandSequence.push_back(cmd);
}

void CommandSequence::clear() { d_commandSequence.clear(); }
void CommandSequence::invoke(api::Solver* solver, SymbolManager* sm)
{
  for (; d_index < d_commandSequence.size(); ++d_index)
  {
    d_commandSequence[d_index]->invoke(solver, sm);
    if (!d_commandSequence[d_index]->ok())
    {
      // abort execution
      d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
      return;
    }
    delete d_commandSequence[d_index];
  }

  AlwaysAssert(d_commandStatus == NULL);
  d_commandStatus = CommandSuccess::instance();
}

void CommandSequence::invoke(api::Solver* solver,
                             SymbolManager* sm,
                             std::ostream& out)
{
  for (; d_index < d_commandSequence.size(); ++d_index)
  {
    d_commandSequence[d_index]->invoke(solver, sm, out);
    if (!d_commandSequence[d_index]->ok())
    {
      // abort execution
      d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
      return;
    }
    delete d_commandSequence[d_index];
  }

  AlwaysAssert(d_commandStatus == NULL);
  d_commandStatus = CommandSuccess::instance();
}

Command* CommandSequence::clone() const
{
  CommandSequence* seq = new CommandSequence();
  for (const_iterator i = begin(); i != end(); ++i)
  {
    seq->addCommand((*i)->clone());
  }
  seq->d_index = d_index;
  return seq;
}

CommandSequence::const_iterator CommandSequence::begin() const
{
  return d_commandSequence.begin();
}

CommandSequence::const_iterator CommandSequence::end() const
{
  return d_commandSequence.end();
}

CommandSequence::iterator CommandSequence::begin()
{
  return d_commandSequence.begin();
}

CommandSequence::iterator CommandSequence::end()
{
  return d_commandSequence.end();
}

std::string CommandSequence::getCommandName() const { return "sequence"; }

void CommandSequence::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
                               OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
                                                            d_commandSequence);
}

/* -------------------------------------------------------------------------- */
/* class DeclarationSequence                                                  */
/* -------------------------------------------------------------------------- */

void DeclarationSequence::toStream(std::ostream& out,
                                   int toDepth,
                                   size_t dag,
                                   OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
      out, d_commandSequence);
}

/* -------------------------------------------------------------------------- */
/* class DeclarationDefinitionCommand                                         */
/* -------------------------------------------------------------------------- */

DeclarationDefinitionCommand::DeclarationDefinitionCommand(
    const std::string& id)
    : d_symbol(id)
{
}

std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }

/* -------------------------------------------------------------------------- */
/* class DeclareFunctionCommand                                               */
/* -------------------------------------------------------------------------- */

DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
                                               api::Term func,
                                               api::Sort sort)
    : DeclarationDefinitionCommand(id), d_func(func), d_sort(sort)
{
}

api::Term DeclareFunctionCommand::getFunction() const { return d_func; }
api::Sort DeclareFunctionCommand::getSort() const { return d_sort; }

void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  // mark that it will be printed in the model
  sm->addModelDeclarationTerm(d_func);
  d_commandStatus = CommandSuccess::instance();
}

Command* DeclareFunctionCommand::clone() const
{
  DeclareFunctionCommand* dfc =
      new DeclareFunctionCommand(d_symbol, d_func, d_sort);
  return dfc;
}

std::string DeclareFunctionCommand::getCommandName() const
{
  return "declare-fun";
}

void DeclareFunctionCommand::toStream(std::ostream& out,
                                      int toDepth,
                                      size_t dag,
                                      OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdDeclareFunction(
      out, d_func.toString(), sortToTypeNode(d_sort));
}

/* -------------------------------------------------------------------------- */
/* class DeclareFunctionCommand                                               */
/* -------------------------------------------------------------------------- */

DeclarePoolCommand::DeclarePoolCommand(const std::string& id,
                                       api::Term func,
                                       api::Sort sort,
                                       const std::vector<api::Term>& initValue)
    : DeclarationDefinitionCommand(id),
      d_func(func),
      d_sort(sort),
      d_initValue(initValue)
{
}

api::Term DeclarePoolCommand::getFunction() const { return d_func; }
api::Sort DeclarePoolCommand::getSort() const { return d_sort; }
const std::vector<api::Term>& DeclarePoolCommand::getInitialValue() const
{
  return d_initValue;
}

void DeclarePoolCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  // Notice that the pool is already declared by the parser so that it the
  // symbol is bound eagerly. This is analogous to DeclareSygusVarCommand.
  // Hence, we do nothing here.
  d_commandStatus = CommandSuccess::instance();
}

Command* DeclarePoolCommand::clone() const
{
  DeclarePoolCommand* dfc =
      new DeclarePoolCommand(d_symbol, d_func, d_sort, d_initValue);
  return dfc;
}

std::string DeclarePoolCommand::getCommandName() const
{
  return "declare-pool";
}

void DeclarePoolCommand::toStream(std::ostream& out,
                                  int toDepth,
                                  size_t dag,
                                  OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdDeclarePool(
      out,
      d_func.toString(),
      sortToTypeNode(d_sort),
      termVectorToNodes(d_initValue));
}

/* -------------------------------------------------------------------------- */
/* class DeclareSortCommand                                                   */
/* -------------------------------------------------------------------------- */

DeclareSortCommand::DeclareSortCommand(const std::string& id,
                                       size_t arity,
                                       api::Sort sort)
    : DeclarationDefinitionCommand(id), d_arity(arity), d_sort(sort)
{
}

size_t DeclareSortCommand::getArity() const { return d_arity; }
api::Sort DeclareSortCommand::getSort() const { return d_sort; }
void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  // mark that it will be printed in the model
  sm->addModelDeclarationSort(d_sort);
  d_commandStatus = CommandSuccess::instance();
}

Command* DeclareSortCommand::clone() const
{
  return new DeclareSortCommand(d_symbol, d_arity, d_sort);
}

std::string DeclareSortCommand::getCommandName() const
{
  return "declare-sort";
}

void DeclareSortCommand::toStream(std::ostream& out,
                                  int toDepth,
                                  size_t dag,
                                  OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdDeclareType(out,
                                                        sortToTypeNode(d_sort));
}

/* -------------------------------------------------------------------------- */
/* class DefineSortCommand                                                    */
/* -------------------------------------------------------------------------- */

DefineSortCommand::DefineSortCommand(const std::string& id, api::Sort sort)
    : DeclarationDefinitionCommand(id), d_params(), d_sort(sort)
{
}

DefineSortCommand::DefineSortCommand(const std::string& id,
                                     const std::vector<api::Sort>& params,
                                     api::Sort sort)
    : DeclarationDefinitionCommand(id), d_params(params), d_sort(sort)
{
}

const std::vector<api::Sort>& DefineSortCommand::getParameters() const
{
  return d_params;
}

api::Sort DefineSortCommand::getSort() const { return d_sort; }
void DefineSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  d_commandStatus = CommandSuccess::instance();
}

Command* DefineSortCommand::clone() const
{
  return new DefineSortCommand(d_symbol, d_params, d_sort);
}

std::string DefineSortCommand::getCommandName() const { return "define-sort"; }

void DefineSortCommand::toStream(std::ostream& out,
                                 int toDepth,
                                 size_t dag,
                                 OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdDefineType(
      out, d_symbol, sortVectorToTypeNodes(d_params), sortToTypeNode(d_sort));
}

/* -------------------------------------------------------------------------- */
/* class DefineFunctionCommand                                                */
/* -------------------------------------------------------------------------- */

DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                             api::Term func,
                                             api::Term formula,
                                             bool global)
    : DeclarationDefinitionCommand(id),
      d_func(func),
      d_formals(),
      d_formula(formula),
      d_global(global)
{
}

DefineFunctionCommand::DefineFunctionCommand(
    const std::string& id,
    api::Term func,
    const std::vector<api::Term>& formals,
    api::Term formula,
    bool global)
    : DeclarationDefinitionCommand(id),
      d_func(func),
      d_formals(formals),
      d_formula(formula),
      d_global(global)
{
}

api::Term DefineFunctionCommand::getFunction() const { return d_func; }
const std::vector<api::Term>& DefineFunctionCommand::getFormals() const
{
  return d_formals;
}

api::Term DefineFunctionCommand::getFormula() const { return d_formula; }
void DefineFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    if (!d_func.isNull())
    {
      solver->defineFun(d_func, d_formals, d_formula, d_global);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* DefineFunctionCommand::clone() const
{
  return new DefineFunctionCommand(
      d_symbol, d_func, d_formals, d_formula, d_global);
}

std::string DefineFunctionCommand::getCommandName() const
{
  return "define-fun";
}

void DefineFunctionCommand::toStream(std::ostream& out,
                                     int toDepth,
                                     size_t dag,
                                     OutputLanguage language) const
{
  TypeNode rangeType = termToNode(d_func).getType();
  if (rangeType.isFunction())
  {
    rangeType = rangeType.getRangeType();
  }
  Printer::getPrinter(language)->toStreamCmdDefineFunction(
      out,
      d_func.toString(),
      termVectorToNodes(d_formals),
      rangeType,
      termToNode(d_formula));
}

/* -------------------------------------------------------------------------- */
/* class DefineFunctionRecCommand                                             */
/* -------------------------------------------------------------------------- */

DefineFunctionRecCommand::DefineFunctionRecCommand(

    api::Term func,
    const std::vector<api::Term>& formals,
    api::Term formula,
    bool global)
    : d_global(global)
{
  d_funcs.push_back(func);
  d_formals.push_back(formals);
  d_formulas.push_back(formula);
}

DefineFunctionRecCommand::DefineFunctionRecCommand(

    const std::vector<api::Term>& funcs,
    const std::vector<std::vector<api::Term>>& formals,
    const std::vector<api::Term>& formulas,
    bool global)
    : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global)
{
}

const std::vector<api::Term>& DefineFunctionRecCommand::getFunctions() const
{
  return d_funcs;
}

const std::vector<std::vector<api::Term>>&
DefineFunctionRecCommand::getFormals() const
{
  return d_formals;
}

const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
{
  return d_formulas;
}

void DefineFunctionRecCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* DefineFunctionRecCommand::clone() const
{
  return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global);
}

std::string DefineFunctionRecCommand::getCommandName() const
{
  return "define-fun-rec";
}

void DefineFunctionRecCommand::toStream(std::ostream& out,
                                        int toDepth,
                                        size_t dag,
                                        OutputLanguage language) const
{
  std::vector<std::vector<Node>> formals;
  formals.reserve(d_formals.size());
  for (const std::vector<api::Term>& formal : d_formals)
  {
    formals.push_back(termVectorToNodes(formal));
  }

  Printer::getPrinter(language)->toStreamCmdDefineFunctionRec(
      out, termVectorToNodes(d_funcs), formals, termVectorToNodes(d_formulas));
}
/* -------------------------------------------------------------------------- */
/* class DeclareHeapCommand                                                   */
/* -------------------------------------------------------------------------- */
DeclareHeapCommand::DeclareHeapCommand(api::Sort locSort, api::Sort dataSort)
    : d_locSort(locSort), d_dataSort(dataSort)
{
}

api::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; }
api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }

void DeclareHeapCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  solver->declareSeparationHeap(d_locSort, d_dataSort);
}

Command* DeclareHeapCommand::clone() const
{
  return new DeclareHeapCommand(d_locSort, d_dataSort);
}

std::string DeclareHeapCommand::getCommandName() const
{
  return "declare-heap";
}

void DeclareHeapCommand::toStream(std::ostream& out,
                                  int toDepth,
                                  size_t dag,
                                  OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdDeclareHeap(
      out, sortToTypeNode(d_locSort), sortToTypeNode(d_dataSort));
}

/* -------------------------------------------------------------------------- */
/* class SetUserAttributeCommand                                              */
/* -------------------------------------------------------------------------- */

SetUserAttributeCommand::SetUserAttributeCommand(
    const std::string& attr,
    api::Term term,
    const std::vector<api::Term>& termValues,
    const std::string& strValue)
    : d_attr(attr), d_term(term), d_termValues(termValues), d_strValue(strValue)
{
}

SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
                                                 api::Term term)
    : SetUserAttributeCommand(attr, term, {}, "")
{
}

SetUserAttributeCommand::SetUserAttributeCommand(
    const std::string& attr,
    api::Term term,
    const std::vector<api::Term>& values)
    : SetUserAttributeCommand(attr, term, values, "")
{
}

SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
                                                 api::Term term,
                                                 const std::string& value)
    : SetUserAttributeCommand(attr, term, {}, value)
{
}

void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    if (!d_term.isNull())
    {
      solver->getSmtEngine()->setUserAttribute(d_attr,
                                               termToNode(d_term),
                                               termVectorToNodes(d_termValues),
                                               d_strValue);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* SetUserAttributeCommand::clone() const
{
  return new SetUserAttributeCommand(d_attr, d_term, d_termValues, d_strValue);
}

std::string SetUserAttributeCommand::getCommandName() const
{
  return "set-user-attribute";
}

void SetUserAttributeCommand::toStream(std::ostream& out,
                                       int toDepth,
                                       size_t dag,
                                       OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdSetUserAttribute(
      out, d_attr, termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class SimplifyCommand                                                      */
/* -------------------------------------------------------------------------- */

SimplifyCommand::SimplifyCommand(api::Term term) : d_term(term) {}
api::Term SimplifyCommand::getTerm() const { return d_term; }
void SimplifyCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_result = solver->simplify(d_term);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Term SimplifyCommand::getResult() const { return d_result; }
void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    out << d_result << endl;
  }
}

Command* SimplifyCommand::clone() const
{
  SimplifyCommand* c = new SimplifyCommand(d_term);
  c->d_result = d_result;
  return c;
}

std::string SimplifyCommand::getCommandName() const { return "simplify"; }

void SimplifyCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
                               OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdSimplify(out, termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class GetValueCommand                                                      */
/* -------------------------------------------------------------------------- */

GetValueCommand::GetValueCommand(api::Term term) : d_terms()
{
  d_terms.push_back(term);
}

GetValueCommand::GetValueCommand(const std::vector<api::Term>& terms)
    : d_terms(terms)
{
  PrettyCheckArgument(
      terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
}

const std::vector<api::Term>& GetValueCommand::getTerms() const
{
  return d_terms;
}
void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    std::vector<api::Term> result = solver->getValue(d_terms);
    Assert(result.size() == d_terms.size());
    for (int i = 0, size = d_terms.size(); i < size; i++)
    {
      api::Term request = d_terms[i];
      api::Term value = result[i];
      result[i] = solver->mkTerm(api::SEXPR, request, value);
    }
    d_result = solver->mkTerm(api::SEXPR, result);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Term GetValueCommand::getResult() const { return d_result; }
void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    expr::ExprDag::Scope scope(out, false);
    out << d_result << endl;
  }
}

Command* GetValueCommand::clone() const
{
  GetValueCommand* c = new GetValueCommand(d_terms);
  c->d_result = d_result;
  return c;
}

std::string GetValueCommand::getCommandName() const { return "get-value"; }

void GetValueCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
                               OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetValue(
      out, termVectorToNodes(d_terms));
}

/* -------------------------------------------------------------------------- */
/* class GetAssignmentCommand                                                 */
/* -------------------------------------------------------------------------- */

GetAssignmentCommand::GetAssignmentCommand() {}
void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    std::map<api::Term, std::string> enames = sm->getExpressionNames();
    std::vector<api::Term> terms;
    std::vector<std::string> names;
    for (const std::pair<const api::Term, std::string>& e : enames)
    {
      terms.push_back(e.first);
      names.push_back(e.second);
    }
    // Must use vector version of getValue to ensure error is thrown regardless
    // of whether terms is empty.
    std::vector<api::Term> values = solver->getValue(terms);
    Assert(values.size() == names.size());
    std::vector<api::Term> sexprs;
    for (size_t i = 0, nterms = terms.size(); i < nterms; i++)
    {
      // Treat the expression name as a variable name as opposed to a string
      // constant to avoid printing double quotes around the name.
      api::Term name = solver->mkVar(solver->getBooleanSort(), names[i]);
      sexprs.push_back(solver->mkTerm(api::SEXPR, name, values[i]));
    }
    d_result = solver->mkTerm(api::SEXPR, sexprs);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Term GetAssignmentCommand::getResult() const { return d_result; }
void GetAssignmentCommand::printResult(std::ostream& out,
                                       uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    out << d_result << endl;
  }
}

Command* GetAssignmentCommand::clone() const
{
  GetAssignmentCommand* c = new GetAssignmentCommand();
  c->d_result = d_result;
  return c;
}

std::string GetAssignmentCommand::getCommandName() const
{
  return "get-assignment";
}

void GetAssignmentCommand::toStream(std::ostream& out,
                                    int toDepth,
                                    size_t dag,
                                    OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
}

/* -------------------------------------------------------------------------- */
/* class GetModelCommand                                                      */
/* -------------------------------------------------------------------------- */

GetModelCommand::GetModelCommand() : d_result(nullptr) {}
void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_result = solver->getSmtEngine()->getModel();
    // set the model declarations, which determines what is printed in the model
    d_result->clearModelDeclarations();
    std::vector<api::Sort> declareSorts = sm->getModelDeclareSorts();
    for (const api::Sort& s : declareSorts)
    {
      d_result->addDeclarationSort(sortToTypeNode(s));
    }
    std::vector<api::Term> declareTerms = sm->getModelDeclareTerms();
    for (const api::Term& t : declareTerms)
    {
      d_result->addDeclarationTerm(termToNode(t));
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (RecoverableModalException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

/* Model is private to the library -- for now
Model* GetModelCommand::getResult() const  {
  return d_result;
}
*/

void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    out << *d_result;
  }
}

Command* GetModelCommand::clone() const
{
  GetModelCommand* c = new GetModelCommand();
  c->d_result = d_result;
  return c;
}

std::string GetModelCommand::getCommandName() const { return "get-model"; }

void GetModelCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
                               OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetModel(out);
}

/* -------------------------------------------------------------------------- */
/* class BlockModelCommand */
/* -------------------------------------------------------------------------- */

BlockModelCommand::BlockModelCommand() {}
void BlockModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->blockModel();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* BlockModelCommand::clone() const
{
  BlockModelCommand* c = new BlockModelCommand();
  return c;
}

std::string BlockModelCommand::getCommandName() const { return "block-model"; }

void BlockModelCommand::toStream(std::ostream& out,
                                 int toDepth,
                                 size_t dag,
                                 OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdBlockModel(out);
}

/* -------------------------------------------------------------------------- */
/* class BlockModelValuesCommand */
/* -------------------------------------------------------------------------- */

BlockModelValuesCommand::BlockModelValuesCommand(
    const std::vector<api::Term>& terms)
    : d_terms(terms)
{
  PrettyCheckArgument(terms.size() >= 1,
                      terms,
                      "cannot block-model-values of an empty set of terms");
}

const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const
{
  return d_terms;
}
void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->blockModelValues(d_terms);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (UnsafeInterruptException& e)
  {
    d_commandStatus = new CommandInterrupted();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* BlockModelValuesCommand::clone() const
{
  BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms);
  return c;
}

std::string BlockModelValuesCommand::getCommandName() const
{
  return "block-model-values";
}

void BlockModelValuesCommand::toStream(std::ostream& out,
                                       int toDepth,
                                       size_t dag,
                                       OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdBlockModelValues(
      out, termVectorToNodes(d_terms));
}

/* -------------------------------------------------------------------------- */
/* class GetProofCommand                                                      */
/* -------------------------------------------------------------------------- */

GetProofCommand::GetProofCommand() {}
void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_result = solver->getProof();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (ok())
  {
    out << d_result;
  }
  else
  {
    this->Command::printResult(out, verbosity);
  }
}

Command* GetProofCommand::clone() const
{
  GetProofCommand* c = new GetProofCommand();
  return c;
}

std::string GetProofCommand::getCommandName() const { return "get-proof"; }

void GetProofCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
                               OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetProof(out);
}

/* -------------------------------------------------------------------------- */
/* class GetInstantiationsCommand                                             */
/* -------------------------------------------------------------------------- */

GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
bool GetInstantiationsCommand::isEnabled(api::Solver* solver,
                                         const api::Result& res)
{
  return (solver->getOptions().printer.instFormatMode
              != options::InstFormatMode::SZS
          && (res.isSat()
              || (res.isSatUnknown()
                  && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
         || res.isUnsat() || res.isEntailed();
}
void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_solver = solver;
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetInstantiationsCommand::printResult(std::ostream& out,
                                           uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    d_solver->printInstantiations(out);
  }
}

Command* GetInstantiationsCommand::clone() const
{
  GetInstantiationsCommand* c = new GetInstantiationsCommand();
  // c->d_result = d_result;
  c->d_solver = d_solver;
  return c;
}

std::string GetInstantiationsCommand::getCommandName() const
{
  return "get-instantiations";
}

void GetInstantiationsCommand::toStream(std::ostream& out,
                                        int toDepth,
                                        size_t dag,
                                        OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
}

/* -------------------------------------------------------------------------- */
/* class GetInterpolCommand                                                   */
/* -------------------------------------------------------------------------- */

GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj)
    : d_name(name), d_conj(conj), d_resultStatus(false)
{
}
GetInterpolCommand::GetInterpolCommand(const std::string& name,
                                       api::Term conj,
                                       api::Grammar* g)
    : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
{
}

api::Term GetInterpolCommand::getConjecture() const { return d_conj; }

const api::Grammar* GetInterpolCommand::getGrammar() const
{
  return d_sygus_grammar;
}

api::Term GetInterpolCommand::getResult() const { return d_result; }

void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    if (d_sygus_grammar == nullptr)
    {
      d_resultStatus = solver->getInterpolant(d_conj, d_result);
    }
    else
    {
      d_resultStatus =
          solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetInterpolCommand::printResult(std::ostream& out,
                                     uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    expr::ExprDag::Scope scope(out, false);
    if (d_resultStatus)
    {
      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
          << std::endl;
    }
    else
    {
      out << "none" << std::endl;
    }
  }
}

Command* GetInterpolCommand::clone() const
{
  GetInterpolCommand* c =
      new GetInterpolCommand(d_name, d_conj, d_sygus_grammar);
  c->d_result = d_result;
  c->d_resultStatus = d_resultStatus;
  return c;
}

std::string GetInterpolCommand::getCommandName() const
{
  return "get-interpol";
}

void GetInterpolCommand::toStream(std::ostream& out,
                                  int toDepth,
                                  size_t dag,
                                  OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetInterpol(
      out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
}

/* -------------------------------------------------------------------------- */
/* class GetAbductCommand                                                     */
/* -------------------------------------------------------------------------- */

GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj)
    : d_name(name), d_conj(conj), d_resultStatus(false)
{
}
GetAbductCommand::GetAbductCommand(const std::string& name,
                                   api::Term conj,
                                   api::Grammar* g)
    : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
{
}

api::Term GetAbductCommand::getConjecture() const { return d_conj; }

const api::Grammar* GetAbductCommand::getGrammar() const
{
  return d_sygus_grammar;
}

std::string GetAbductCommand::getAbductName() const { return d_name; }
api::Term GetAbductCommand::getResult() const { return d_result; }

void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    if (d_sygus_grammar == nullptr)
    {
      d_resultStatus = solver->getAbduct(d_conj, d_result);
    }
    else
    {
      d_resultStatus = solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    expr::ExprDag::Scope scope(out, false);
    if (d_resultStatus)
    {
      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
          << std::endl;
    }
    else
    {
      out << "none" << std::endl;
    }
  }
}

Command* GetAbductCommand::clone() const
{
  GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar);
  c->d_result = d_result;
  c->d_resultStatus = d_resultStatus;
  return c;
}

std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }

void GetAbductCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
                                OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetAbduct(
      out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
}

/* -------------------------------------------------------------------------- */
/* class GetQuantifierEliminationCommand                                      */
/* -------------------------------------------------------------------------- */

GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
    : d_term(), d_doFull(true)
{
}
GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
    const api::Term& term, bool doFull)
    : d_term(term), d_doFull(doFull)
{
}

api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
void GetQuantifierEliminationCommand::invoke(api::Solver* solver,
                                             SymbolManager* sm)
{
  try
  {
    if (d_doFull)
    {
      d_result = solver->getQuantifierElimination(d_term);
    }
    else
    {
      d_result = solver->getQuantifierEliminationDisjunct(d_term);
    }
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

api::Term GetQuantifierEliminationCommand::getResult() const
{
  return d_result;
}
void GetQuantifierEliminationCommand::printResult(std::ostream& out,
                                                  uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    out << d_result << endl;
  }
}

Command* GetQuantifierEliminationCommand::clone() const
{
  GetQuantifierEliminationCommand* c =
      new GetQuantifierEliminationCommand(d_term, d_doFull);
  c->d_result = d_result;
  return c;
}

std::string GetQuantifierEliminationCommand::getCommandName() const
{
  return d_doFull ? "get-qe" : "get-qe-disjunct";
}

void GetQuantifierEliminationCommand::toStream(std::ostream& out,
                                               int toDepth,
                                               size_t dag,
                                               OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
      out, termToNode(d_term));
}

/* -------------------------------------------------------------------------- */
/* class GetUnsatAssumptionsCommand                                           */
/* -------------------------------------------------------------------------- */

GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}

void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_result = solver->getUnsatAssumptions();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::vector<api::Term> GetUnsatAssumptionsCommand::getResult() const
{
  return d_result;
}

void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
                                             uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    container_to_stream(out, d_result, "(", ")\n", " ");
  }
}

Command* GetUnsatAssumptionsCommand::clone() const
{
  GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
  c->d_result = d_result;
  return c;
}

std::string GetUnsatAssumptionsCommand::getCommandName() const
{
  return "get-unsat-assumptions";
}

void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
                                          int toDepth,
                                          size_t dag,
                                          OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
}

/* -------------------------------------------------------------------------- */
/* class GetUnsatCoreCommand                                                  */
/* -------------------------------------------------------------------------- */

GetUnsatCoreCommand::GetUnsatCoreCommand() : d_sm(nullptr) {}
void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_sm = sm;
    d_result = solver->getUnsatCore();

    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

void GetUnsatCoreCommand::printResult(std::ostream& out,
                                      uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    if (options::dumpUnsatCoresFull())
    {
      // use the assertions
      UnsatCore ucr(termVectorToNodes(d_result));
      ucr.toStream(out);
    }
    else
    {
      // otherwise, use the names
      std::vector<std::string> names;
      d_sm->getExpressionNames(d_result, names, true);
      UnsatCore ucr(names);
      ucr.toStream(out);
    }
  }
}

const std::vector<api::Term>& GetUnsatCoreCommand::getUnsatCore() const
{
  // of course, this will be empty if the command hasn't been invoked yet
  return d_result;
}

Command* GetUnsatCoreCommand::clone() const
{
  GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
  c->d_sm = d_sm;
  c->d_result = d_result;
  return c;
}

std::string GetUnsatCoreCommand::getCommandName() const
{
  return "get-unsat-core";
}

void GetUnsatCoreCommand::toStream(std::ostream& out,
                                   int toDepth,
                                   size_t dag,
                                   OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
}

/* -------------------------------------------------------------------------- */
/* class GetAssertionsCommand                                                 */
/* -------------------------------------------------------------------------- */

GetAssertionsCommand::GetAssertionsCommand() {}
void GetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    stringstream ss;
    const vector<api::Term> v = solver->getAssertions();
    ss << "(\n";
    copy(v.begin(), v.end(), ostream_iterator<api::Term>(ss, "\n"));
    ss << ")\n";
    d_result = ss.str();
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string GetAssertionsCommand::getResult() const { return d_result; }
void GetAssertionsCommand::printResult(std::ostream& out,
                                       uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else
  {
    out << d_result;
  }
}

Command* GetAssertionsCommand::clone() const
{
  GetAssertionsCommand* c = new GetAssertionsCommand();
  c->d_result = d_result;
  return c;
}

std::string GetAssertionsCommand::getCommandName() const
{
  return "get-assertions";
}

void GetAssertionsCommand::toStream(std::ostream& out,
                                    int toDepth,
                                    size_t dag,
                                    OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
}

/* -------------------------------------------------------------------------- */
/* class SetBenchmarkStatusCommand                                            */
/* -------------------------------------------------------------------------- */

SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
    : d_status(status)
{
}

BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
{
  return d_status;
}

void SetBenchmarkStatusCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    stringstream ss;
    ss << d_status;
    solver->setInfo("status", ss.str());
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* SetBenchmarkStatusCommand::clone() const
{
  return new SetBenchmarkStatusCommand(d_status);
}

std::string SetBenchmarkStatusCommand::getCommandName() const
{
  return "set-info";
}

void SetBenchmarkStatusCommand::toStream(std::ostream& out,
                                         int toDepth,
                                         size_t dag,
                                         OutputLanguage language) const
{
  Result::Sat status = Result::SAT_UNKNOWN;
  switch (d_status)
  {
    case BenchmarkStatus::SMT_SATISFIABLE: status = Result::SAT; break;
    case BenchmarkStatus::SMT_UNSATISFIABLE: status = Result::UNSAT; break;
    case BenchmarkStatus::SMT_UNKNOWN: status = Result::SAT_UNKNOWN; break;
  }

  Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, status);
}

/* -------------------------------------------------------------------------- */
/* class SetBenchmarkLogicCommand                                             */
/* -------------------------------------------------------------------------- */

SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
    : d_logic(logic)
{
}

std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
void SetBenchmarkLogicCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->setLogic(d_logic);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* SetBenchmarkLogicCommand::clone() const
{
  return new SetBenchmarkLogicCommand(d_logic);
}

std::string SetBenchmarkLogicCommand::getCommandName() const
{
  return "set-logic";
}

void SetBenchmarkLogicCommand::toStream(std::ostream& out,
                                        int toDepth,
                                        size_t dag,
                                        OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
}

/* -------------------------------------------------------------------------- */
/* class SetInfoCommand                                                       */
/* -------------------------------------------------------------------------- */

SetInfoCommand::SetInfoCommand(const std::string& flag,
                               const std::string& value)
    : d_flag(flag), d_value(value)
{
}

const std::string& SetInfoCommand::getFlag() const { return d_flag; }
const std::string& SetInfoCommand::getValue() const { return d_value; }
void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->setInfo(d_flag, d_value);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException&)
  {
    // As per SMT-LIB spec, silently accept unknown set-info keys
    d_commandStatus = CommandSuccess::instance();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* SetInfoCommand::clone() const
{
  return new SetInfoCommand(d_flag, d_value);
}

std::string SetInfoCommand::getCommandName() const { return "set-info"; }

void SetInfoCommand::toStream(std::ostream& out,
                              int toDepth,
                              size_t dag,
                              OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_value);
}

/* -------------------------------------------------------------------------- */
/* class GetInfoCommand                                                       */
/* -------------------------------------------------------------------------- */

GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
std::string GetInfoCommand::getFlag() const { return d_flag; }
void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    std::vector<api::Term> v;
    v.push_back(solver->mkString(":" + d_flag));
    v.push_back(solver->mkString(solver->getInfo(d_flag)));
    d_result = sexprToString(solver->mkTerm(api::SEXPR, v));
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException& e)
  {
    d_commandStatus = new CommandRecoverableFailure(e.what());
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string GetInfoCommand::getResult() const { return d_result; }
void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else if (d_result != "")
  {
    out << d_result << endl;
  }
}

Command* GetInfoCommand::clone() const
{
  GetInfoCommand* c = new GetInfoCommand(d_flag);
  c->d_result = d_result;
  return c;
}

std::string GetInfoCommand::getCommandName() const { return "get-info"; }

void GetInfoCommand::toStream(std::ostream& out,
                              int toDepth,
                              size_t dag,
                              OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
}

/* -------------------------------------------------------------------------- */
/* class SetOptionCommand                                                     */
/* -------------------------------------------------------------------------- */

SetOptionCommand::SetOptionCommand(const std::string& flag,
                                   const std::string& value)
    : d_flag(flag), d_value(value)
{
}

const std::string& SetOptionCommand::getFlag() const { return d_flag; }
const std::string& SetOptionCommand::getValue() const { return d_value; }
void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    solver->setOption(d_flag, d_value);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException&)
  {
    d_commandStatus = new CommandUnsupported();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

Command* SetOptionCommand::clone() const
{
  return new SetOptionCommand(d_flag, d_value);
}

std::string SetOptionCommand::getCommandName() const { return "set-option"; }

void SetOptionCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
                                OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_value);
}

/* -------------------------------------------------------------------------- */
/* class GetOptionCommand                                                     */
/* -------------------------------------------------------------------------- */

GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
std::string GetOptionCommand::getFlag() const { return d_flag; }
void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  try
  {
    d_result = solver->getOption(d_flag);
    d_commandStatus = CommandSuccess::instance();
  }
  catch (api::CVC5ApiRecoverableException&)
  {
    d_commandStatus = new CommandUnsupported();
  }
  catch (exception& e)
  {
    d_commandStatus = new CommandFailure(e.what());
  }
}

std::string GetOptionCommand::getResult() const { return d_result; }
void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
  if (!ok())
  {
    this->Command::printResult(out, verbosity);
  }
  else if (d_result != "")
  {
    out << d_result << endl;
  }
}

Command* GetOptionCommand::clone() const
{
  GetOptionCommand* c = new GetOptionCommand(d_flag);
  c->d_result = d_result;
  return c;
}

std::string GetOptionCommand::getCommandName() const { return "get-option"; }

void GetOptionCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
                                OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
}

/* -------------------------------------------------------------------------- */
/* class DatatypeDeclarationCommand                                           */
/* -------------------------------------------------------------------------- */

DatatypeDeclarationCommand::DatatypeDeclarationCommand(
    const api::Sort& datatype)
    : d_datatypes()
{
  d_datatypes.push_back(datatype);
}

DatatypeDeclarationCommand::DatatypeDeclarationCommand(
    const std::vector<api::Sort>& datatypes)
    : d_datatypes(datatypes)
{
}

const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const
{
  return d_datatypes;
}

void DatatypeDeclarationCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
  d_commandStatus = CommandSuccess::instance();
}

Command* DatatypeDeclarationCommand::clone() const
{
  return new DatatypeDeclarationCommand(d_datatypes);
}

std::string DatatypeDeclarationCommand::getCommandName() const
{
  return "declare-datatypes";
}

void DatatypeDeclarationCommand::toStream(std::ostream& out,
                                          int toDepth,
                                          size_t dag,
                                          OutputLanguage language) const
{
  Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
      out, sortVectorToTypeNodes(d_datatypes));
}

}  // namespace cvc5

Generated by: GCOVR (Version 3.2)