diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
commit | 25e9c72dd689d3b621b901220794c652a3ba589a (patch) | |
tree | 58b14dd3818f3e7a8ca3311a0457716e7753a95e /src/expr/command.h | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 43 |
1 files changed, 20 insertions, 23 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index d0b72c3dd..50d382038 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -62,7 +62,8 @@ public: virtual void invoke(SmtEngine* smtEngine) = 0; virtual void invoke(SmtEngine* smtEngine, std::ostream& out); virtual ~Command() {}; - virtual void toStream(std::ostream&) const = 0; + virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, + OutputLanguage language = language::output::LANG_AST) const; std::string toString() const; virtual void printResult(std::ostream& out) const; };/* class Command */ @@ -77,7 +78,7 @@ protected: public: EmptyCommand(std::string name = ""); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getName() const { return d_name; } };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { @@ -86,19 +87,17 @@ protected: public: AssertCommand(const BoolExpr& e); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + BoolExpr getExpr() const { return d_expr; } };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { public: void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { public: void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; };/* class PopCommand */ class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { @@ -110,7 +109,6 @@ public: DeclarationCommand(const std::vector<std::string>& ids, Type t); const std::vector<std::string>& getDeclaredSymbols() const; Type getDeclaredType() const; - void toStream(std::ostream& out) const; };/* class DeclarationCommand */ class CVC4_PUBLIC DefineFunctionCommand : public Command { @@ -123,7 +121,9 @@ public: const std::vector<Expr>& formals, Expr formula); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + Expr getFunction() const { return d_func; } + const std::vector<Expr>& getFormals() const { return d_formals; } + Expr getFormula() const { return d_formula; } };/* class DefineFunctionCommand */ /** @@ -137,7 +137,6 @@ public: const std::vector<Expr>& formals, Expr formula); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; };/* class DefineNamedFunctionCommand */ class CVC4_PUBLIC CheckSatCommand : public Command { @@ -147,9 +146,9 @@ protected: public: CheckSatCommand(const BoolExpr& expr); void invoke(SmtEngine* smtEngine); + BoolExpr getExpr() const { return d_expr; } Result getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { @@ -159,9 +158,9 @@ protected: public: QueryCommand(const BoolExpr& e); void invoke(SmtEngine* smtEngine); + BoolExpr getExpr() const { return d_expr; } Result getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class QueryCommand */ // this is TRANSFORM in the CVC presentation language @@ -172,9 +171,9 @@ protected: public: SimplifyCommand(Expr term); void invoke(SmtEngine* smtEngine); + Expr getTerm() const { return d_term; } Expr getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class SimplifyCommand */ class CVC4_PUBLIC GetValueCommand : public Command { @@ -184,9 +183,9 @@ protected: public: GetValueCommand(Expr term); void invoke(SmtEngine* smtEngine); + Expr getTerm() const { return d_term; } Expr getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class GetValueCommand */ class CVC4_PUBLIC GetAssignmentCommand : public Command { @@ -197,7 +196,6 @@ public: void invoke(SmtEngine* smtEngine); SExpr getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class GetAssignmentCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { @@ -208,7 +206,6 @@ public: void invoke(SmtEngine* smtEngine); std::string getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class GetAssertionsCommand */ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { @@ -218,7 +215,7 @@ protected: public: SetBenchmarkStatusCommand(BenchmarkStatus status); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + BenchmarkStatus getStatus() const { return d_status; } };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { @@ -228,7 +225,7 @@ protected: public: SetBenchmarkLogicCommand(std::string logic); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getLogic() const { return d_logic; } };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { @@ -239,7 +236,8 @@ protected: public: SetInfoCommand(std::string flag, SExpr& sexpr); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getFlag() const { return d_flag; } + SExpr getSExpr() const { return d_sexpr; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class SetInfoCommand */ @@ -251,7 +249,7 @@ protected: public: GetInfoCommand(std::string flag); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getFlag() const { return d_flag; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class GetInfoCommand */ @@ -264,7 +262,8 @@ protected: public: SetOptionCommand(std::string flag, SExpr& sexpr); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getFlag() const { return d_flag; } + SExpr getSExpr() const { return d_sexpr; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class SetOptionCommand */ @@ -276,7 +275,7 @@ protected: public: GetOptionCommand(std::string flag); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getFlag() const { return d_flag; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class GetOptionCommand */ @@ -288,13 +287,12 @@ public: DatatypeDeclarationCommand(const DatatypeType& datatype); DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + const std::vector<DatatypeType>& getDatatypes() const { return d_datatypes; } };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC QuitCommand : public EmptyCommand { public: QuitCommand(); - void toStream(std::ostream& out) const; };/* class QuitCommand */ class CVC4_PUBLIC CommandSequence : public Command { @@ -309,7 +307,6 @@ public: void invoke(SmtEngine* smtEngine); void invoke(SmtEngine* smtEngine, std::ostream& out); void addCommand(Command* cmd); - void toStream(std::ostream& out) const; typedef std::vector<Command*>::iterator iterator; typedef std::vector<Command*>::const_iterator const_iterator; |