From f40384bda966082f940054dcd258e382ad454265 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 6 Aug 2012 19:36:46 +0000 Subject: [PATCH] Cleanup of some command stuff, fixes broken Java build. --- src/expr/command.cpp | 98 +++++++++++++++++++++++--------------------- src/expr/command.h | 61 ++++++++++++++------------- 2 files changed, 83 insertions(+), 76 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index c127aca75..576707fca 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1145,34 +1145,37 @@ Command* DatatypeDeclarationCommand::clone() const { /* class RewriteRuleCommand */ -RewriteRuleCommand::RewriteRuleCommand(const VExpr & vars, - const std::vector< Expr> & guards, - const Expr & head, const Expr & body, - Triggers triggers) throw() : +RewriteRuleCommand::RewriteRuleCommand(const std::vector& vars, + const std::vector& guards, + Expr head, Expr body, + const Triggers& triggers) throw() : d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) { } -RewriteRuleCommand::RewriteRuleCommand(const VExpr & vars, - const Expr & head, const Expr & body) throw() : +RewriteRuleCommand::RewriteRuleCommand(const std::vector& vars, + Expr head, Expr body) throw() : d_vars(vars), d_head(head), d_body(body) { } -const RewriteRuleCommand::VExpr & RewriteRuleCommand::getVars() const throw(){ +const std::vector& RewriteRuleCommand::getVars() const throw() { return d_vars; -}; -const RewriteRuleCommand::VExpr & RewriteRuleCommand::getGuards() const throw(){ +} + +const std::vector& RewriteRuleCommand::getGuards() const throw() { return d_guards; -}; -const Expr & RewriteRuleCommand::getHead() const throw(){ +} + +Expr RewriteRuleCommand::getHead() const throw() { return d_head; -}; -const Expr & RewriteRuleCommand::getBody() const throw(){ +} + +Expr RewriteRuleCommand::getBody() const throw() { return d_body; -}; -const RewriteRuleCommand::Triggers & RewriteRuleCommand::getTriggers() const throw(){ - return d_triggers; -}; +} +const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() { + return d_triggers; +} void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() { try { @@ -1233,52 +1236,54 @@ Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCo Expr head = d_head.exportTo(exprManager, variableMap); Expr body = d_body.exportTo(exprManager, variableMap); /** Create the converted rules */ - return new RewriteRuleCommand(vars,guards,head,body,triggers); + return new RewriteRuleCommand(vars, guards, head, body, triggers); } Command* RewriteRuleCommand::clone() const { - return new RewriteRuleCommand(d_vars,d_guards,d_head,d_body,d_triggers); + return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers); } /* class PropagateRuleCommand */ -PropagateRuleCommand::PropagateRuleCommand(const VExpr & vars, - const VExpr & guards, - const VExpr & heads, - const Expr & body, - const Triggers triggers, - bool deduction - ) throw() : +PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, + const std::vector& guards, + const std::vector& heads, + Expr body, + const Triggers& triggers, + bool deduction) throw() : d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) { } -PropagateRuleCommand::PropagateRuleCommand(const VExpr & vars, - const VExpr & heads, - const Expr & body, - bool deduction - ) throw() : +PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, + const std::vector& heads, + Expr body, + bool deduction) throw() : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) { } -const PropagateRuleCommand::VExpr & PropagateRuleCommand::getVars() const throw(){ +const std::vector& PropagateRuleCommand::getVars() const throw() { return d_vars; -}; -const PropagateRuleCommand::VExpr & PropagateRuleCommand::getGuards() const throw(){ +} + +const std::vector& PropagateRuleCommand::getGuards() const throw() { return d_guards; -}; -const PropagateRuleCommand::VExpr & PropagateRuleCommand::getHeads() const throw(){ +} + +const std::vector& PropagateRuleCommand::getHeads() const throw() { return d_heads; -}; -const Expr & PropagateRuleCommand::getBody() const throw(){ +} + +Expr PropagateRuleCommand::getBody() const throw() { return d_body; -}; -const PropagateRuleCommand::Triggers & PropagateRuleCommand::getTriggers() const throw(){ +} + +const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() { return d_triggers; -}; -bool PropagateRuleCommand::isDeduction() const throw(){ - return d_deduction; -}; +} +bool PropagateRuleCommand::isDeduction() const throw() { + return d_deduction; +} void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() { try { @@ -1348,14 +1353,13 @@ Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMap /** Convert head and body */ Expr body = d_body.exportTo(exprManager, variableMap); /** Create the converted rules */ - return new PropagateRuleCommand(vars,guards,heads,body,triggers); + return new PropagateRuleCommand(vars, guards, heads, body, triggers); } Command* PropagateRuleCommand::clone() const { - return new PropagateRuleCommand(d_vars,d_guards,d_heads,d_body,d_triggers); + return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers); } - /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) throw() { diff --git a/src/expr/command.h b/src/expr/command.h index 9f1722f9f..242817575 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -600,61 +600,64 @@ public: };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC RewriteRuleCommand : public Command { +public: + typedef std::vector< std::vector< Expr > > Triggers; protected: typedef std::vector< Expr > VExpr; VExpr d_vars; VExpr d_guards; Expr d_head; Expr d_body; - typedef std::vector< std::vector< Expr > > Triggers; Triggers d_triggers; public: - RewriteRuleCommand(const VExpr & vars, - const std::vector< Expr> & guards, - const Expr & head, const Expr & body, - Triggers d_triggers - ) throw(); - RewriteRuleCommand(const VExpr & vars, - const Expr & head, const Expr & body) throw(); + RewriteRuleCommand(const std::vector& vars, + const std::vector& guards, + Expr head, + Expr body, + const Triggers& d_triggers) throw(); + RewriteRuleCommand(const std::vector& vars, + Expr head, + Expr body) throw(); ~RewriteRuleCommand() throw() {} - const VExpr & getVars() const throw(); - const VExpr & getGuards() const throw(); - const Expr & getHead() const throw(); - const Expr & getBody() const throw(); - const Triggers & getTriggers() const throw(); + const std::vector& getVars() const throw(); + const std::vector& getGuards() const throw(); + Expr getHead() const throw(); + Expr getBody() const throw(); + const Triggers& getTriggers() const throw(); void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; };/* class RewriteRuleCommand */ class CVC4_PUBLIC PropagateRuleCommand : public Command { +public: + typedef std::vector< std::vector< Expr > > Triggers; protected: typedef std::vector< Expr > VExpr; VExpr d_vars; VExpr d_guards; VExpr d_heads; Expr d_body; - typedef std::vector< std::vector< Expr > > Triggers; Triggers d_triggers; bool d_deduction; public: - PropagateRuleCommand(const VExpr & vars, - const VExpr & guards, - const VExpr & heads, - const Expr & body, - Triggers d_triggers, - /* true if we want a deduction rule */ - bool d_deduction = false - ) throw(); - PropagateRuleCommand(const VExpr & vars, - const VExpr & heads, const Expr & body, + PropagateRuleCommand(const std::vector& vars, + const std::vector& guards, + const std::vector& heads, + Expr body, + const Triggers& d_triggers, + /* true if we want a deduction rule */ + bool d_deduction = false) throw(); + PropagateRuleCommand(const std::vector& vars, + const std::vector& heads, + Expr body, bool d_deduction = false) throw(); ~PropagateRuleCommand() throw() {} - const VExpr & getVars() const throw(); - const VExpr & getGuards() const throw(); - const VExpr & getHeads() const throw(); - const Expr & getBody() const throw(); - const Triggers & getTriggers() const throw(); + const std::vector& getVars() const throw(); + const std::vector& getGuards() const throw(); + const std::vector& getHeads() const throw(); + Expr getBody() const throw(); + const Triggers& getTriggers() const throw(); bool isDeduction() const throw(); void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); -- 2.30.2