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

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 9f502c2ea7fd883d2aa7ea81989cd47f6e0c6bbd..23a2b74c22869a7f72ef6f83c2fbaba5de0cd9f6 100644 (file)
--- 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 ed6be86de36d3e74697bc85b302e5f989ef203ca..c3d0363bb3ed1515ad69771d007883f8e9776c90 100644 (file)
--- 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 8e5a9dae4b63d088b8de00fab91dd69f04ab27a7..95f35a5a6838eff832fe438f0a56cfeeccaff36b 100644 (file)
--- 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 ab805a6c589de393d4e8769b10fe31de3c88d8aa..247c367b4e430a1561b2189d047b10fe3b6bf578 100644 (file)
--- 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 72237ff1ca2db7b1b03bba9e9a9a99ea9f8688a8..c53156a3cb7a6ba9d808bdd746d20e9ab7880c3a 100644 (file)
--- 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 b38ed7d63c8ac448c5edba11aab7ee381baffcf3..90382c365de77dc44602622bb9d61a54dc450426 100644 (file)
--- 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 cd80f57d8cf1562da9c5ed1e4205e7cfaeed5cdf..4cf2ab73294631925ff02d0dc0a9496c0207e846 100644 (file)
--- 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;
 };
 
 }