diff options
Diffstat (limited to 'src/smt/command.h')
-rw-r--r-- | src/smt/command.h | 167 |
1 files changed, 70 insertions, 97 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index 438f9febb..310850b78 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -41,6 +41,10 @@ class Solver; class Term; } // namespace api +namespace parser { +class SymbolManager; +} + class UnsatCore; class SmtEngine; class Command; @@ -202,8 +206,16 @@ class CVC4_PUBLIC Command virtual ~Command(); - virtual void invoke(api::Solver* solver) = 0; - virtual void invoke(api::Solver* solver, std::ostream& out); + /** + * Invoke the command on the solver and symbol manager sm. + */ + virtual void invoke(api::Solver* solver, parser::SymbolManager* sm) = 0; + /** + * Same as above, and prints the result to output stream out. + */ + virtual void invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out); virtual void toStream( std::ostream& out, @@ -276,13 +288,12 @@ class CVC4_PUBLIC EmptyCommand : public Command public: EmptyCommand(std::string name = ""); std::string getName() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -297,15 +308,16 @@ class CVC4_PUBLIC EchoCommand : public Command std::string getOutput() const; - void invoke(api::Solver* solver) override; - void invoke(api::Solver* solver, std::ostream& out) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -324,14 +336,13 @@ class CVC4_PUBLIC AssertCommand : public Command api::Term getTerm() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class AssertCommand */ @@ -339,13 +350,12 @@ class CVC4_PUBLIC AssertCommand : public Command class CVC4_PUBLIC PushCommand : public Command { public: - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PushCommand */ @@ -353,13 +363,12 @@ class CVC4_PUBLIC PushCommand : public Command class CVC4_PUBLIC PopCommand : public Command { public: - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PopCommand */ @@ -372,7 +381,7 @@ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command public: DeclarationDefinitionCommand(const std::string& id); - void invoke(api::Solver* solver) override = 0; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override = 0; std::string getSymbol() const; }; /* class DeclarationDefinitionCommand */ @@ -392,13 +401,12 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand bool getPrintInModelSetByUser() const; void setPrintInModel(bool p); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareFunctionCommand */ @@ -415,13 +423,12 @@ class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand size_t getArity() const; api::Sort getSort() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareSortCommand */ @@ -441,13 +448,12 @@ class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand const std::vector<api::Sort>& getParameters() const; api::Sort getSort() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DefineSortCommand */ @@ -469,13 +475,12 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand const std::vector<api::Term>& getFormals() const; api::Term getFormula() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -506,7 +511,7 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand const std::vector<api::Term>& formals, api::Term formula, bool global); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; void toStream( std::ostream& out, @@ -536,13 +541,12 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command const std::vector<std::vector<api::Term> >& getFormals() const; const std::vector<api::Term>& getFormulas() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -572,7 +576,7 @@ class CVC4_PUBLIC DeclareHeapCommand : public Command DeclareHeapCommand(api::Sort locSort, api::Sort dataSort); api::Sort getLocationSort() const; api::Sort getDataSort() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -603,13 +607,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command api::Term term, const std::string& value); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -637,14 +640,13 @@ class CVC4_PUBLIC CheckSatCommand : public Command api::Term getTerm() const; api::Result getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -666,14 +668,13 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command const std::vector<api::Term>& getTerms() const; api::Result getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -694,14 +695,13 @@ class CVC4_PUBLIC QueryCommand : public Command api::Term getTerm() const; api::Result getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class QueryCommand */ @@ -722,7 +722,7 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand * The declared sygus variable is communicated to the SMT engine in case a * synthesis conjecture is built later on. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -731,7 +731,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -772,7 +771,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand * The declared function-to-synthesize is communicated to the SMT engine in * case a synthesis conjecture is built later on. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -781,7 +780,6 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -810,7 +808,7 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command * The declared constraint is communicated to the SMT engine in case a * synthesis conjecture is built later on. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -819,7 +817,6 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -854,7 +851,7 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command * invariant constraint is built, in case an actual synthesis conjecture is * built later on. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -863,7 +860,6 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -891,7 +887,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command * and then perform a satisfiability check, whose result is stored in * d_result. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -900,7 +896,6 @@ class CVC4_PUBLIC CheckSynthCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -925,14 +920,13 @@ class CVC4_PUBLIC SimplifyCommand : public Command api::Term getTerm() const; api::Term getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SimplifyCommand */ @@ -949,14 +943,13 @@ class CVC4_PUBLIC GetValueCommand : public Command const std::vector<api::Term>& getTerms() const; api::Term getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetValueCommand */ @@ -970,14 +963,13 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command GetAssignmentCommand(); SExpr getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetAssignmentCommand */ @@ -989,14 +981,13 @@ class CVC4_PUBLIC GetModelCommand : public Command // Model is private to the library -- for now // Model* getResult() const ; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1010,13 +1001,12 @@ class CVC4_PUBLIC BlockModelCommand : public Command public: BlockModelCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class BlockModelCommand */ @@ -1028,13 +1018,12 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command BlockModelValuesCommand(const std::vector<api::Term>& terms); const std::vector<api::Term>& getTerms() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1048,13 +1037,12 @@ class CVC4_PUBLIC GetProofCommand : public Command public: GetProofCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetProofCommand */ @@ -1064,14 +1052,13 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command public: GetInstantiationsCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1084,14 +1071,13 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command public: GetSynthSolutionCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1123,14 +1109,13 @@ class CVC4_PUBLIC GetInterpolCommand : public Command * query. */ api::Term getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1175,14 +1160,13 @@ class CVC4_PUBLIC GetAbductCommand : public Command */ api::Term getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1212,7 +1196,7 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command api::Term getTerm() const; bool getDoFull() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; api::Term getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; @@ -1221,7 +1205,6 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetQuantifierEliminationCommand */ @@ -1230,7 +1213,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command { public: GetUnsatAssumptionsCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; std::vector<api::Term> getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1238,7 +1221,6 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1252,7 +1234,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command GetUnsatCoreCommand(); const std::vector<api::Term>& getUnsatCore() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1260,7 +1242,6 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1279,7 +1260,7 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command public: GetAssertionsCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; std::string getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1301,7 +1282,7 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command BenchmarkStatus getStatus() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1320,7 +1301,7 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command SetBenchmarkLogicCommand(std::string logic); std::string getLogic() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1342,7 +1323,7 @@ class CVC4_PUBLIC SetInfoCommand : public Command std::string getFlag() const; SExpr getSExpr() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1364,7 +1345,7 @@ class CVC4_PUBLIC GetInfoCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1387,13 +1368,12 @@ class CVC4_PUBLIC SetOptionCommand : public Command std::string getFlag() const; SExpr getSExpr() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetOptionCommand */ @@ -1410,14 +1390,13 @@ class CVC4_PUBLIC GetOptionCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetOptionCommand */ @@ -1438,13 +1417,12 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command public: SetExpressionNameCommand(api::Term term, std::string name); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetExpressionNameCommand */ @@ -1459,13 +1437,12 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command DatatypeDeclarationCommand(const std::vector<api::Sort>& datatypes); const std::vector<api::Sort>& getDatatypes() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DatatypeDeclarationCommand */ @@ -1474,13 +1451,12 @@ class CVC4_PUBLIC ResetCommand : public Command { public: ResetCommand() {} - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetCommand */ @@ -1489,13 +1465,12 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command { public: ResetAssertionsCommand() {} - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetAssertionsCommand */ @@ -1504,13 +1479,12 @@ class CVC4_PUBLIC QuitCommand : public Command { public: QuitCommand() {} - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class QuitCommand */ @@ -1524,13 +1498,12 @@ class CVC4_PUBLIC CommentCommand : public Command std::string getComment() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommentCommand */ @@ -1550,8 +1523,10 @@ class CVC4_PUBLIC CommandSequence : public Command void addCommand(Command* cmd); void clear(); - void invoke(api::Solver* solver) override; - void invoke(api::Solver* solver, std::ostream& out) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out) override; typedef std::vector<Command*>::iterator iterator; typedef std::vector<Command*>::const_iterator const_iterator; @@ -1567,7 +1542,6 @@ class CVC4_PUBLIC CommandSequence : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommandSequence */ @@ -1577,7 +1551,6 @@ class CVC4_PUBLIC DeclarationSequence : public CommandSequence void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; |