Remove `Command::clone()` (#8903)

This code was unused. This is work towards a streamlined parser API.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index fe02770cf2d41777e78c118b09c6716b00ee5c4a..9420b0251808715ea59b5626fe369f9aeb123ca8 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -36,7 +36,6 @@
 #include "options/smt_options.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"
-#include "smt/model.h"
 #include "util/smt2_quote_string.h"
 #include "util/utility.h"
 
@@ -243,7 +242,6 @@ void EmptyCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   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) const
@@ -276,8 +274,6 @@ void EchoCommand::invoke(cvc5::Solver* solver,
   printResult(out);
 }
 
-Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
-
 std::string EchoCommand::getCommandName() const { return "echo"; }
 
 void EchoCommand::toStream(std::ostream& out) const
@@ -305,8 +301,6 @@ void AssertCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* AssertCommand::clone() const { return new AssertCommand(d_term); }
-
 std::string AssertCommand::getCommandName() const { return "assert"; }
 
 void AssertCommand::toStream(std::ostream& out) const
@@ -333,7 +327,6 @@ void PushCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* PushCommand::clone() const { return new PushCommand(d_nscopes); }
 std::string PushCommand::getCommandName() const { return "push"; }
 
 void PushCommand::toStream(std::ostream& out) const
@@ -360,7 +353,6 @@ void PopCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* PopCommand::clone() const { return new PopCommand(d_nscopes); }
 std::string PopCommand::getCommandName() const { return "pop"; }
 
 void PopCommand::toStream(std::ostream& out) const
@@ -396,13 +388,6 @@ void CheckSatCommand::printResult(std::ostream& out) const
   out << d_result << endl;
 }
 
-Command* CheckSatCommand::clone() const
-{
-  CheckSatCommand* c = new CheckSatCommand();
-  c->d_result = d_result;
-  return c;
-}
-
 std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
 
 void CheckSatCommand::toStream(std::ostream& out) const
@@ -456,13 +441,6 @@ void CheckSatAssumingCommand::printResult(std::ostream& out) const
   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";
@@ -493,11 +471,6 @@ void DeclareSygusVarCommand::invoke(cvc5::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";
@@ -546,12 +519,6 @@ void SynthFunCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   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";
@@ -600,11 +567,6 @@ void SygusConstraintCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 cvc5::Term SygusConstraintCommand::getTerm() const { return d_term; }
 
-Command* SygusConstraintCommand::clone() const
-{
-  return new SygusConstraintCommand(d_term, d_isAssume);
-}
-
 std::string SygusConstraintCommand::getCommandName() const
 {
   return d_isAssume ? "assume" : "constraint";
@@ -659,11 +621,6 @@ const std::vector<cvc5::Term>& SygusInvConstraintCommand::getPredicates() const
   return d_predicates;
 }
 
-Command* SygusInvConstraintCommand::clone() const
-{
-  return new SygusInvConstraintCommand(d_predicates);
-}
-
 std::string SygusInvConstraintCommand::getCommandName() const
 {
   return "inv-constraint";
@@ -752,8 +709,6 @@ void CheckSynthCommand::printResult(std::ostream& out) const
   out << d_solution.str();
 }
 
-Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
-
 std::string CheckSynthCommand::getCommandName() const
 {
   return d_isNext ? "check-synth-next" : "check-synth";
@@ -789,7 +744,6 @@ void ResetCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* ResetCommand::clone() const { return new ResetCommand(); }
 std::string ResetCommand::getCommandName() const { return "reset"; }
 
 void ResetCommand::toStream(std::ostream& out) const
@@ -815,11 +769,6 @@ void ResetAssertionsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* ResetAssertionsCommand::clone() const
-{
-  return new ResetAssertionsCommand();
-}
-
 std::string ResetAssertionsCommand::getCommandName() const
 {
   return "reset-assertions";
@@ -839,7 +788,6 @@ void QuitCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   d_commandStatus = CommandSuccess::instance();
 }
 
-Command* QuitCommand::clone() const { return new QuitCommand(); }
 std::string QuitCommand::getCommandName() const { return "exit"; }
 
 void QuitCommand::toStream(std::ostream& out) const
@@ -904,17 +852,6 @@ void CommandSequence::invoke(cvc5::Solver* solver,
   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();
@@ -975,13 +912,6 @@ void DeclareFunctionCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   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";
@@ -1023,13 +953,6 @@ void DeclarePoolCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   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";
@@ -1089,13 +1012,6 @@ void DeclareOracleFunCommand::invoke(Solver* solver, SymbolManager* sm)
   d_commandStatus = CommandSuccess::instance();
 }
 
-Command* DeclareOracleFunCommand::clone() const
-{
-  DeclareOracleFunCommand* dfc =
-      new DeclareOracleFunCommand(d_id, d_sort, d_binName);
-  return dfc;
-}
-
 std::string DeclareOracleFunCommand::getCommandName() const
 {
   return "declare-oracle-fun";
@@ -1131,11 +1047,6 @@ void DeclareSortCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   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";
@@ -1173,11 +1084,6 @@ void DefineSortCommand::invoke(cvc5::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) const
@@ -1237,11 +1143,6 @@ void DefineFunctionCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* DefineFunctionCommand::clone() const
-{
-  return new DefineFunctionCommand(d_symbol, d_formals, d_sort, d_formula);
-}
-
 std::string DefineFunctionCommand::getCommandName() const
 {
   return "define-fun";
@@ -1307,11 +1208,6 @@ void DefineFunctionRecCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* DefineFunctionRecCommand::clone() const
-{
-  return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas);
-}
-
 std::string DefineFunctionRecCommand::getCommandName() const
 {
   return "define-fun-rec";
@@ -1345,11 +1241,6 @@ void DeclareHeapCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   solver->declareSepHeap(d_locSort, d_dataSort);
 }
 
-Command* DeclareHeapCommand::clone() const
-{
-  return new DeclareHeapCommand(d_locSort, d_dataSort);
-}
-
 std::string DeclareHeapCommand::getCommandName() const
 {
   return "declare-heap";
@@ -1386,13 +1277,6 @@ void SimplifyCommand::printResult(std::ostream& out) const
   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) const
@@ -1453,13 +1337,6 @@ void GetValueCommand::printResult(std::ostream& out) const
   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) const
@@ -1516,13 +1393,6 @@ void GetAssignmentCommand::printResult(std::ostream& out) const
   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";
@@ -1559,13 +1429,6 @@ void GetModelCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetModelCommand::printResult(std::ostream& out) const { 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) const
@@ -1597,12 +1460,6 @@ void BlockModelCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* BlockModelCommand::clone() const
-{
-  BlockModelCommand* c = new BlockModelCommand(d_mode);
-  return c;
-}
-
 std::string BlockModelCommand::getCommandName() const { return "block-model"; }
 
 void BlockModelCommand::toStream(std::ostream& out) const
@@ -1644,12 +1501,6 @@ void BlockModelValuesCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* BlockModelValuesCommand::clone() const
-{
-  BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms);
-  return c;
-}
-
 std::string BlockModelValuesCommand::getCommandName() const
 {
   return "block-model-values";
@@ -1685,12 +1536,6 @@ void GetProofCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetProofCommand::printResult(std::ostream& out) const { out << d_result; }
 
-Command* GetProofCommand::clone() const
-{
-  GetProofCommand* c = new GetProofCommand();
-  return c;
-}
-
 std::string GetProofCommand::getCommandName() const { return "get-proof"; }
 
 void GetProofCommand::toStream(std::ostream& out) const
@@ -1730,14 +1575,6 @@ void GetInstantiationsCommand::printResult(std::ostream& out) const
   out << d_solver->getInstantiations();
 }
 
-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";
@@ -1811,14 +1648,6 @@ void GetInterpolantCommand::printResult(std::ostream& out) const
   }
 }
 
-Command* GetInterpolantCommand::clone() const
-{
-  GetInterpolantCommand* c =
-      new GetInterpolantCommand(d_name, d_conj, d_sygus_grammar);
-  c->d_result = d_result;
-  return c;
-}
-
 std::string GetInterpolantCommand::getCommandName() const
 {
   return "get-interpolant";
@@ -1868,13 +1697,6 @@ void GetInterpolantNextCommand::printResult(std::ostream& out) const
   }
 }
 
-Command* GetInterpolantNextCommand::clone() const
-{
-  GetInterpolantNextCommand* c = new GetInterpolantNextCommand;
-  c->d_result = d_result;
-  return c;
-}
-
 std::string GetInterpolantNextCommand::getCommandName() const
 {
   return "get-interpolant-next";
@@ -1948,13 +1770,6 @@ void GetAbductCommand::printResult(std::ostream& out) const
   }
 }
 
-Command* GetAbductCommand::clone() const
-{
-  GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar);
-  c->d_result = d_result;
-  return c;
-}
-
 std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
 
 void GetAbductCommand::toStream(std::ostream& out) const
@@ -2001,13 +1816,6 @@ void GetAbductNextCommand::printResult(std::ostream& out) const
   }
 }
 
-Command* GetAbductNextCommand::clone() const
-{
-  GetAbductNextCommand* c = new GetAbductNextCommand;
-  c->d_result = d_result;
-  return c;
-}
-
 std::string GetAbductNextCommand::getCommandName() const
 {
   return "get-abduct-next";
@@ -2064,14 +1872,6 @@ void GetQuantifierEliminationCommand::printResult(std::ostream& out) const
   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";
@@ -2116,13 +1916,6 @@ void GetUnsatAssumptionsCommand::printResult(std::ostream& out) const
   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";
@@ -2182,15 +1975,6 @@ const std::vector<cvc5::Term>& GetUnsatCoreCommand::getUnsatCore() const
   return d_result;
 }
 
-Command* GetUnsatCoreCommand::clone() const
-{
-  GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
-  c->d_solver = d_solver;
-  c->d_sm = d_sm;
-  c->d_result = d_result;
-  return c;
-}
-
 std::string GetUnsatCoreCommand::getCommandName() const
 {
   return "get-unsat-core";
@@ -2252,14 +2036,6 @@ const std::map<cvc5::Term, cvc5::Term>& GetDifficultyCommand::getDifficultyMap()
   return d_result;
 }
 
-Command* GetDifficultyCommand::clone() const
-{
-  GetDifficultyCommand* c = new GetDifficultyCommand;
-  c->d_sm = d_sm;
-  c->d_result = d_result;
-  return c;
-}
-
 std::string GetDifficultyCommand::getCommandName() const
 {
   return "get-difficulty";
@@ -2309,13 +2085,6 @@ const std::vector<cvc5::Term>& GetLearnedLiteralsCommand::getLearnedLiterals()
   return d_result;
 }
 
-Command* GetLearnedLiteralsCommand::clone() const
-{
-  GetLearnedLiteralsCommand* c = new GetLearnedLiteralsCommand;
-  c->d_result = d_result;
-  return c;
-}
-
 std::string GetLearnedLiteralsCommand::getCommandName() const
 {
   return "get-learned-literals";
@@ -2355,13 +2124,6 @@ void GetAssertionsCommand::printResult(std::ostream& out) const
   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";
@@ -2395,11 +2157,6 @@ void SetBenchmarkLogicCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-Command* SetBenchmarkLogicCommand::clone() const
-{
-  return new SetBenchmarkLogicCommand(d_logic);
-}
-
 std::string SetBenchmarkLogicCommand::getCommandName() const
 {
   return "set-logic";
@@ -2444,11 +2201,6 @@ void SetInfoCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-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) const
@@ -2495,13 +2247,6 @@ void GetInfoCommand::printResult(std::ostream& out) const
   }
 }
 
-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) const
@@ -2542,11 +2287,6 @@ void SetOptionCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-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) const
@@ -2586,13 +2326,6 @@ void GetOptionCommand::printResult(std::ostream& out) const
   }
 }
 
-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) const
@@ -2627,11 +2360,6 @@ void DatatypeDeclarationCommand::invoke(cvc5::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";

diff --git a/src/smt/command.h b/src/smt/command.h
index e17105f1ef4f8d5974c5e201ba438cd5021174b1..65adafce6cc0591d0188f98a380f79abfedd0b6a 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -186,11 +186,6 @@ class CVC5_EXPORT Command
   /** Get the command status (it's NULL if we haven't run yet). */
   const CommandStatus* getCommandStatus() const { return d_commandStatus; }
 
-  /**
-   * 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
@@ -247,7 +242,6 @@ class CVC5_EXPORT EmptyCommand : public Command
   EmptyCommand(std::string name = "");
   std::string getName() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -267,7 +261,6 @@ class CVC5_EXPORT EchoCommand : public Command
               SymbolManager* sm,
               std::ostream& out) override;
 
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -287,7 +280,6 @@ class CVC5_EXPORT AssertCommand : public Command
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
 
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class AssertCommand */
@@ -298,7 +290,6 @@ class CVC5_EXPORT PushCommand : public Command
   PushCommand(uint32_t nscopes);
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -312,7 +303,6 @@ class CVC5_EXPORT PopCommand : public Command
   PopCommand(uint32_t nscopes);
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -346,7 +336,6 @@ class CVC5_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand
   cvc5::Sort getSort() const;
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class DeclareFunctionCommand */
@@ -368,7 +357,6 @@ class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand
   const std::vector<cvc5::Term>& getInitialValue() const;
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class DeclarePoolCommand */
@@ -385,7 +373,6 @@ class CVC5_EXPORT DeclareOracleFunCommand : public Command
   const std::string& getBinaryName() const;
 
   void invoke(Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -411,7 +398,6 @@ class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
   cvc5::Sort getSort() const;
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class DeclareSortCommand */
@@ -432,7 +418,6 @@ class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand
   cvc5::Sort getSort() const;
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class DefineSortCommand */
@@ -453,7 +438,6 @@ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
   cvc5::Term getFormula() const;
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -486,7 +470,6 @@ class CVC5_EXPORT DefineFunctionRecCommand : public Command
   const std::vector<cvc5::Term>& getFormulas() const;
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -512,7 +495,6 @@ class CVC5_EXPORT DeclareHeapCommand : public Command
   cvc5::Sort getLocationSort() const;
   cvc5::Sort getDataSort() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -534,7 +516,6 @@ class CVC5_EXPORT CheckSatCommand : public Command
   cvc5::Result getResult() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -557,7 +538,6 @@ class CVC5_EXPORT CheckSatAssumingCommand : public Command
   cvc5::Result getResult() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -566,24 +546,6 @@ class CVC5_EXPORT CheckSatAssumingCommand : public Command
   cvc5::Result d_result;
 }; /* class CheckSatAssumingCommand */
 
-class CVC5_EXPORT QueryCommand : public Command
-{
- protected:
-  cvc5::Term d_term;
-  cvc5::Result d_result;
-
- public:
-  QueryCommand(const cvc5::Term& t);
-
-  cvc5::Term getTerm() const;
-  cvc5::Result getResult() const;
-  void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out) const override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-  void toStream(std::ostream& out) const override;
-}; /* class QueryCommand */
-
 /* ------------------- sygus commands  ------------------ */
 
 /** Declares a sygus universal variable */
@@ -603,8 +565,6 @@ class CVC5_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand
    * synthesis conjecture is built later on.
    */
   void invoke(cvc5::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 */
@@ -648,8 +608,6 @@ class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand
    * case a synthesis conjecture is built later on.
    */
   void invoke(cvc5::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 */
@@ -681,8 +639,6 @@ class CVC5_EXPORT SygusConstraintCommand : public Command
    * synthesis conjecture is built later on.
    */
   void invoke(cvc5::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 */
@@ -722,8 +678,6 @@ class CVC5_EXPORT SygusInvConstraintCommand : public Command
    * built later on.
    */
   void invoke(cvc5::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 */
@@ -754,8 +708,6 @@ class CVC5_EXPORT CheckSynthCommand : public Command
    * d_result.
    */
   void invoke(cvc5::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 */
@@ -786,7 +738,6 @@ class CVC5_EXPORT SimplifyCommand : public Command
   cvc5::Term getResult() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class SimplifyCommand */
@@ -805,7 +756,6 @@ class CVC5_EXPORT GetValueCommand : public Command
   cvc5::Term getResult() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class GetValueCommand */
@@ -821,7 +771,6 @@ class CVC5_EXPORT GetAssignmentCommand : public Command
   cvc5::Term getResult() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class GetAssignmentCommand */
@@ -832,7 +781,6 @@ class CVC5_EXPORT GetModelCommand : public Command
   GetModelCommand();
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -848,7 +796,6 @@ class CVC5_EXPORT BlockModelCommand : public Command
   BlockModelCommand(modes::BlockModelsMode mode);
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -865,7 +812,6 @@ class CVC5_EXPORT BlockModelValuesCommand : public Command
 
   const std::vector<cvc5::Term>& getTerms() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -883,7 +829,6 @@ class CVC5_EXPORT GetProofCommand : public Command
 
   void printResult(std::ostream& out) const override;
 
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -900,7 +845,6 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command
   static bool isEnabled(cvc5::Solver* solver, const cvc5::Result& res);
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -936,7 +880,6 @@ class CVC5_EXPORT GetInterpolantCommand : public Command
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -964,7 +907,6 @@ class CVC5_EXPORT GetInterpolantNextCommand : public Command
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -1005,7 +947,6 @@ class CVC5_EXPORT GetAbductCommand : public Command
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -1032,7 +973,6 @@ class CVC5_EXPORT GetAbductNextCommand : public Command
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -1060,7 +1000,6 @@ class CVC5_EXPORT GetQuantifierEliminationCommand : public Command
   cvc5::Term getResult() const;
   void printResult(std::ostream& out) const override;
 
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class GetQuantifierEliminationCommand */
@@ -1072,7 +1011,6 @@ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   std::vector<cvc5::Term> getResult() const;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -1089,7 +1027,6 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
 
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -1111,7 +1048,6 @@ class CVC5_EXPORT GetDifficultyCommand : public Command
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
 
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -1131,7 +1067,6 @@ class CVC5_EXPORT GetLearnedLiteralsCommand : public Command
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
 
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 
@@ -1151,7 +1086,6 @@ class CVC5_EXPORT GetAssertionsCommand : public Command
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   std::string getResult() const;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class GetAssertionsCommand */
@@ -1166,7 +1100,6 @@ class CVC5_EXPORT SetBenchmarkLogicCommand : public Command
 
   std::string getLogic() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class SetBenchmarkLogicCommand */
@@ -1184,7 +1117,6 @@ class CVC5_EXPORT SetInfoCommand : public Command
   const std::string& getValue() const;
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class SetInfoCommand */
@@ -1203,7 +1135,6 @@ class CVC5_EXPORT GetInfoCommand : public Command
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class GetInfoCommand */
@@ -1221,7 +1152,6 @@ class CVC5_EXPORT SetOptionCommand : public Command
   const std::string& getValue() const;
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class SetOptionCommand */
@@ -1240,7 +1170,6 @@ class CVC5_EXPORT GetOptionCommand : public Command
 
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out) const override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class GetOptionCommand */
@@ -1256,7 +1185,6 @@ class CVC5_EXPORT DatatypeDeclarationCommand : public Command
   DatatypeDeclarationCommand(const std::vector<cvc5::Sort>& datatypes);
   const std::vector<cvc5::Sort>& getDatatypes() const;
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class DatatypeDeclarationCommand */
@@ -1266,7 +1194,6 @@ class CVC5_EXPORT ResetCommand : public Command
  public:
   ResetCommand() {}
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class ResetCommand */
@@ -1276,7 +1203,6 @@ class CVC5_EXPORT ResetAssertionsCommand : public Command
  public:
   ResetAssertionsCommand() {}
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class ResetAssertionsCommand */
@@ -1286,7 +1212,6 @@ class CVC5_EXPORT QuitCommand : public Command
  public:
   QuitCommand() {}
   void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class QuitCommand */
@@ -1320,7 +1245,6 @@ class CVC5_EXPORT CommandSequence : public Command
   iterator begin();
   iterator end();
 
-  Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out) const override;
 }; /* class CommandSequence */