diff options
author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-06-17 15:25:58 +0200 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:39 -0400 |
commit | 0fe78eebc0c0f2d01c7aa64725bee08ba5aa2274 (patch) | |
tree | 475b094989b0828d7d82e41160a010a6134e8674 /src/expr | |
parent | 35cdae503bd88633a52333bf06fbf80cd81926e2 (diff) |
For casc : print models of functions rewritten by sort inference.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 29 | ||||
-rw-r--r-- | src/expr/command.h | 5 |
2 files changed, 30 insertions, 4 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 9f502c2ea..23a2b74c2 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -519,7 +519,9 @@ std::string DeclarationDefinitionCommand::getSymbol() const throw() { DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() : DeclarationDefinitionCommand(id), d_func(func), - d_type(t) { + d_type(t), + d_printInModel(true), + d_printInModelSetByUser(false){ } Expr DeclareFunctionCommand::getFunction() const throw() { @@ -530,18 +532,37 @@ Type DeclareFunctionCommand::getType() const throw() { return d_type; } +bool DeclareFunctionCommand::getPrintInModel() const throw() { + return d_printInModel; +} + +bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { + return d_printInModelSetByUser; +} + +void DeclareFunctionCommand::setPrintInModel( bool p ) { + d_printInModel = p; + d_printInModelSetByUser = true; +} + void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), - d_type.exportTo(exprManager, variableMap)); + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), + d_type.exportTo(exprManager, variableMap)); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; } Command* DeclareFunctionCommand::clone() const { - return new DeclareFunctionCommand(d_symbol, d_func, d_type); + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; } std::string DeclareFunctionCommand::getCommandName() const throw() { diff --git a/src/expr/command.h b/src/expr/command.h index ed6be86de..c3d0363bb 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -351,11 +351,16 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: Expr d_func; Type d_type; + bool d_printInModel; + bool d_printInModelSetByUser; public: DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw(); ~DeclareFunctionCommand() throw() {} Expr getFunction() const throw(); Type getType() const throw(); + bool getPrintInModel() const throw(); + bool getPrintInModelSetByUser() const throw(); + void setPrintInModel( bool p ); void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; |