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

7 files changed, 77 insertions, 9 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;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8e5a9dae4..95f35a5a6 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -797,8 +797,13 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       }
     }
   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
-    Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
-    if(n.getKind() == kind::SKOLEM) {
+    const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c; 
+    Node n = Node::fromExpr( dfc->getFunction() );
+    if(dfc->getPrintInModelSetByUser()){
+      if(!dfc->getPrintInModel()){
+        return;
+      }
+    }else if(n.getKind() == kind::SKOLEM) {
       // don't print out internal stuff
       return;
     }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ab805a6c5..247c367b4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3017,7 +3017,12 @@ void SmtEnginePrivate::processAssertions() {
 
   if( options::sortInference() ){
     //sort inference technique
-    d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess );
+    SortInference * si = d_smt.d_theoryEngine->getSortInference();
+    si->simplify( d_assertionsToPreprocess );
+    for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
+      d_smt.setPrintFuncInModel( it->first, false );
+      d_smt.setPrintFuncInModel( it->second, true );
+    }
   }
 
   //if( options::quantConflictFind() ){
@@ -4120,4 +4125,27 @@ void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) {
   d_theoryEngine->setUserAttribute(attr, expr.getNode());
 }
 
+void SmtEngine::setPrintFuncInModel( Node f, bool p ) {
+  Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
+  Expr fe = f.toExpr();
+  for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){
+    Command * c = d_modelGlobalCommands[i];
+    DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
+    if(dfc != NULL) {
+      if( dfc->getFunction()==fe ){
+        dfc->setPrintInModel( p );
+      }
+    }
+  }
+  for( unsigned i=0; i<d_modelCommands->size(); i++ ){
+    Command * c = (*d_modelCommands)[i];
+    DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
+    if(dfc != NULL) {
+      if( dfc->getFunction()==fe ){
+        dfc->setPrintInModel( p );
+      }
+    }
+  }
+}
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 72237ff1c..c53156a3c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -653,6 +653,11 @@ public:
    */
   void setUserAttribute(const std::string& attr, Expr expr);
 
+  /**
+   * Set print function in model
+   */
+  void setPrintFuncInModel( Node f, bool p );
+  
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index b38ed7d63..90382c365 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -580,6 +580,8 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
         ss << "io_" << op;
         TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );
         d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );
+        Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl;
+        d_model_replace_f[op] = d_symbol_map[op];
       }else{
         d_symbol_map[op] = op;
       }
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h
index cd80f57d8..4cf2ab732 100644
--- a/src/util/sort_inference.h
+++ b/src/util/sort_inference.h
@@ -26,7 +26,7 @@
 
 namespace CVC4 {
 
-class SortInference{
+class SortInference {
 private:
   //all subsorts
   std::vector< int > d_sub_sorts;
@@ -69,7 +69,6 @@ private:
   void printSort( const char* c, int t );
   //process
   int process( Node n, std::map< Node, Node >& var_bound );
-
 //for monotonicity inference
 private:
   void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound );
@@ -107,6 +106,9 @@ public:
   bool isWellSorted( Node n );
   //get constraints for being well-typed according to computed sub-types
   void getSortConstraints( Node n, SortInference::UnionFind& uf );
+public:
+  //list of all functions and the uninterpreted symbols they were replaced with
+  std::map< Node, Node > d_model_replace_f;
 };
 
 }