Cleanup of some command stuff, fixes broken Java build.

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() {