From: Andres Noetzli Date: Wed, 22 Jun 2022 22:26:23 +0000 (-0700) Subject: Remove `Command::clone()` (#8903) X-Git-Tag: cvc5-1.0.1~41 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d6992f469cae24556dd7e7c1e4c59c90b0b57536;p=cvc5.git 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 fe02770cf..9420b0251 100644 --- 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& 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& 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& 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& 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 e17105f1e..65adafce6 100644 --- 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& 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& 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& 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 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& datatypes); const std::vector& 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 */