Making the values argument const in the SetUserAttributeCommand const… (#1249)

* Making the values argument const in the SetUserAttributeCommand constructor. Misc. cleanup of SetUserAttributeCommand.
* Removing override keyword that was making SWIG unhappy.

2 files changed, 48 insertions, 36 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 82b494382..8012c868c 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -850,43 +850,46 @@ Command* DefineNamedFunctionCommand::clone() const {
 
 /* class SetUserAttribute */
 
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() :
-  d_attr( attr ), d_expr( expr ){
-}
-
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
-                                                  std::vector<Expr>& values ) throw() :
-  d_attr( attr ), d_expr( expr ){
-  d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() );
-}
-
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
-                                                  const std::string& value ) throw() :
-  d_attr( attr ), d_expr( expr ), d_str_value( value ){
-}
+SetUserAttributeCommand::SetUserAttributeCommand(
+    const std::string& attr, Expr expr, const std::vector<Expr>& expr_values,
+    const std::string& str_value) throw()
+    : d_attr(attr),
+      d_expr(expr),
+      d_expr_values(expr_values),
+      d_str_value(str_value) {}
+
+SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
+                                                 Expr expr) throw()
+    : SetUserAttributeCommand(attr, expr, {}, "") {}
+
+SetUserAttributeCommand::SetUserAttributeCommand(
+    const std::string& attr, Expr expr, const std::vector<Expr>& values) throw()
+    : SetUserAttributeCommand(attr, expr, values, "") {}
+
+SetUserAttributeCommand::SetUserAttributeCommand(
+    const std::string& attr, Expr expr, const std::string& value) throw()
+    : SetUserAttributeCommand(attr, expr, {}, value) {}
 
 void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) {
   try {
-    if(!d_expr.isNull()) {
-      smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
+    if (!d_expr.isNull()) {
+      smtEngine->setUserAttribute(d_attr, d_expr, d_expr_values, d_str_value);
     }
     d_commandStatus = CommandSuccess::instance();
-  } catch(exception& e) {
+  } catch (exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
 }
 
-Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){
+Command* SetUserAttributeCommand::exportTo(
+    ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   Expr expr = d_expr.exportTo(exprManager, variableMap);
-  SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value );
-  c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() );
-  return c;
+  return new SetUserAttributeCommand(d_attr, expr, d_expr_values, d_str_value);
 }
 
-Command* SetUserAttributeCommand::clone() const{
-  SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value );
-  c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() );
-  return c;
+Command* SetUserAttributeCommand::clone() const {
+  return new SetUserAttributeCommand(d_attr, d_expr, d_expr_values,
+                                     d_str_value);
 }
 
 std::string SetUserAttributeCommand::getCommandName() const throw() {
diff --git a/src/smt/command.h b/src/smt/command.h
index 839927fc1..dcd818f83 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -468,21 +468,30 @@ public:
  *  via the syntax (! expr :attr)
  */
 class CVC4_PUBLIC SetUserAttributeCommand : public Command {
-protected:
-  std::string d_attr;
-  Expr d_expr;
-  std::vector<Expr> d_expr_values;
-  std::string d_str_value;
-public:
-  SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
-  SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw();
-  SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw();
+ public:
+  SetUserAttributeCommand(const std::string& attr, Expr expr) throw();
+  SetUserAttributeCommand(const std::string& attr, Expr expr,
+                          const std::vector<Expr>& values) throw();
+  SetUserAttributeCommand(const std::string& attr, Expr expr,
+                          const std::string& value) throw();
   ~SetUserAttributeCommand() throw() {}
+
   void invoke(SmtEngine* smtEngine);
-  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap);
   Command* clone() const;
   std::string getCommandName() const throw();
-};/* class SetUserAttributeCommand */
+
+ private:
+  SetUserAttributeCommand(const std::string& attr, Expr expr,
+                          const std::vector<Expr>& expr_values,
+                          const std::string& str_value) throw();
+
+  const std::string d_attr;
+  const Expr d_expr;
+  const std::vector<Expr> d_expr_values;
+  const std::string d_str_value;
+}; /* class SetUserAttributeCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
 protected: