diff options
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 48 |
1 files changed, 45 insertions, 3 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index f93df3722..648c64388 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -462,13 +462,17 @@ DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, d_type(t) { } +Expr DeclareFunctionCommand::getFunction() const throw() { + return d_func; +} + Type DeclareFunctionCommand::getType() const throw() { return d_type; } void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this; - smtEngine->addToModelFunction( d_func ); + smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_FUN ); d_commandStatus = CommandSuccess::instance(); } @@ -500,7 +504,7 @@ Type DeclareTypeCommand::getType() const throw() { void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this; - smtEngine->addToModelType( d_type ); + smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_SORT ); d_commandStatus = CommandSuccess::instance(); } @@ -644,6 +648,43 @@ Command* DefineNamedFunctionCommand::clone() const { return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); } +/* class SetUserAttribute */ + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() : + d_attr( attr ), d_expr( expr ){ +} +/* +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& id, Expr expr, + std::vector<Expr>& values ) throw() : + d_id( id ), 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 ){ +} +*/ +void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){ + try { + if(!d_expr.isNull()) { + smtEngine->setUserAttribute( d_attr, d_expr ); + } + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){ + Expr expr = d_expr.exportTo(exprManager, variableMap); + return new SetUserAttributeCommand( d_attr, expr ); +} + +Command* SetUserAttributeCommand::clone() const{ + return new SetUserAttributeCommand( d_attr, d_expr ); +} + /* class Simplify */ SimplifyCommand::SimplifyCommand(Expr term) throw() : @@ -1095,7 +1136,7 @@ void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); v.push_back(smtEngine->getOption(d_flag)); stringstream ss; - + ss << SExpr(v); d_result = ss.str(); d_commandStatus = CommandSuccess::instance(); @@ -1148,6 +1189,7 @@ DatatypeDeclarationCommand::getDatatypes() const throw() { void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this; + smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_DATATYPES ); d_commandStatus = CommandSuccess::instance(); } |