For casc : print models of functions rewritten by sort inference.

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;