diff options
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 98 |
1 files changed, 51 insertions, 47 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<Expr>& vars, + const std::vector<Expr>& 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<Expr>& 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<Expr>& RewriteRuleCommand::getVars() const throw() { return d_vars; -}; -const RewriteRuleCommand::VExpr & RewriteRuleCommand::getGuards() const throw(){ +} + +const std::vector<Expr>& 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<Expr>& vars, + const std::vector<Expr>& guards, + const std::vector<Expr>& 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<Expr>& vars, + const std::vector<Expr>& 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<Expr>& PropagateRuleCommand::getVars() const throw() { return d_vars; -}; -const PropagateRuleCommand::VExpr & PropagateRuleCommand::getGuards() const throw(){ +} + +const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() { return d_guards; -}; -const PropagateRuleCommand::VExpr & PropagateRuleCommand::getHeads() const throw(){ +} + +const std::vector<Expr>& 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() { |