Add support for quantifier-specific instantiation levels. Add option for setting inst-level 0 only for input terms.

2 files changed, 18 insertions, 14 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 16484a320..33be85d11 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -744,22 +744,22 @@ Command* DefineNamedFunctionCommand::clone() const {
 SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() :
   d_attr( attr ), d_expr( expr ){
 }
-/*
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& id, Expr expr,
+
+SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
                                                   std::vector<Expr>& values ) throw() :
-  d_id( id ), d_expr( expr ){
+  d_attr( attr ), d_expr( expr ){
   d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() );
 }
 
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& id, Expr expr,
-                                                  std::string& value ) throw() :
-  d_id( id ), d_expr( expr ), d_str_value( value ){
+SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
+                                                  const std::string& value ) throw() :
+  d_attr( attr ), d_expr( expr ), d_str_value( value ){
 }
-*/
+
 void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
   try {
     if(!d_expr.isNull()) {
-      smtEngine->setUserAttribute( d_attr, d_expr );
+      smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
     }
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
@@ -769,11 +769,15 @@ void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
 
 Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){
   Expr expr = d_expr.exportTo(exprManager, variableMap);
-  return new SetUserAttributeCommand( d_attr, expr );
+  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;
 }
 
 Command* SetUserAttributeCommand::clone() const{
-  return new SetUserAttributeCommand( d_attr, d_expr );
+  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;
 }
 
 std::string SetUserAttributeCommand::getCommandName() const throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 606618d21..c4e7fbf89 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -439,12 +439,12 @@ 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;
+  std::vector<Expr> d_expr_values;
+  std::string d_str_value;
 public:
   SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
-  //SetUserAttributeCommand( const std::string& id, Expr expr, std::vector<Expr>& values ) throw();
-  //SetUserAttributeCommand( const std::string& id, Expr expr, std::string& value ) 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();
   ~SetUserAttributeCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);