Cleanup of some command stuff, fixes broken Java build.

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<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() {
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<Expr>& vars,
+                     const std::vector<Expr>& guards,
+                     Expr head,
+                     Expr body,
+                     const Triggers& d_triggers) throw();
+  RewriteRuleCommand(const std::vector<Expr>& 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<Expr>& getVars() const throw();
+  const std::vector<Expr>& 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<Expr>& vars,
+                       const std::vector<Expr>& guards,
+                       const std::vector<Expr>& heads,
+                       Expr body,
+                       const Triggers& d_triggers,
+                       /* true if we want a deduction rule */
+                       bool d_deduction = false) throw();
+  PropagateRuleCommand(const std::vector<Expr>& vars,
+                       const std::vector<Expr>& 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<Expr>& getVars() const throw();
+  const std::vector<Expr>& getGuards() const throw();
+  const std::vector<Expr>& 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);