Finish --dump-instantiations option. Update scripts.

4 files changed, 25 insertions, 25 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4deb43f42..c6b76e850 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3801,15 +3801,16 @@ Proof* SmtEngine::getProof() throw(ModalException) {
 }
 
 void SmtEngine::printInstantiations( std::ostream& out ) {
-  //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
-  out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl;
-  //}
+  SmtScope smts(this);
+  if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
+    out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl;
+  }
   if( d_theoryEngine ){
     d_theoryEngine->printInstantiations( out );
   }
-  //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
-  out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl;
-  //}
+  if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
+    out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl;
+  }
 }
 
 vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 703a44d03..292190168 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -27,7 +27,7 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
-InstMatch::InstMatch( Node f ) {
+InstMatch::InstMatch( TNode f ) {
   for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
     d_vals.push_back( Node::null() );
   }
@@ -198,12 +198,12 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
   }
 }
 
-void InstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const {
+void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const {
   if( terms.size()==q[0].getNumChildren() ){
     out << "  ( ";
     for( unsigned i=0; i<terms.size(); i++ ){
-      if( i>0 ) out << ", ";
-      //out << terms[i];
+      if( i>0 ){ out << ", ";}
+      out << terms[i];
     }
     out << " )" << std::endl;
   }else{
@@ -282,13 +282,13 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
   }
 }
 
-void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const{
+void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{
   if( d_valid.get() ){
     if( terms.size()==q[0].getNumChildren() ){
       out << "  ( ";
       for( unsigned i=0; i<terms.size(); i++ ){
         if( i>0 ) out << ", ";
-        //out << terms[i];
+        out << terms[i];
       }
       out << " )" << std::endl;
     }else{
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index accd3baed..d728d18a2 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -41,7 +41,7 @@ public:
   std::vector< Node > d_vals;
 public:
   InstMatch(){}
-  InstMatch( Node f );
+  explicit InstMatch( TNode f );
   InstMatch( InstMatch* m );
 
   /** fill all unfilled values with m */
@@ -101,7 +101,7 @@ public:
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
 private:
-  void print( std::ostream& out, Node q, std::vector< Node >& terms ) const;
+  void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
 public:
   InstMatchTrie(){}
   ~InstMatchTrie(){}
@@ -129,7 +129,7 @@ public:
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
   void print( std::ostream& out, Node q ) const{
-    std::vector< Node > terms;
+    std::vector< TNode > terms;
     print( out, q, terms );
   }
 };/* class InstMatchTrie */
@@ -142,7 +142,7 @@ public:
   /** is valid */
   context::CDO< bool > d_valid;
 private:
-  void print( std::ostream& out, Node q, std::vector< Node >& terms ) const;
+  void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
 public:
   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
   ~CDInstMatchTrie(){}
@@ -170,7 +170,7 @@ public:
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
                      bool modInst = false, int index = 0, bool onlyExist = false );
   void print( std::ostream& out, Node q ) const{
-    std::vector< Node > terms;
+    std::vector< TNode > terms;
     print( out, q, terms );
   }
 };/* class CDInstMatchTrie */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 83733da42..3714ca4d0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -623,19 +623,18 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
 }
 
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
-  //Trace("ajr-temp") << "QE print inst." << std::endl;
-  //if( options::incrementalSolving() ){
-  //  for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
-  //    out << "Instantiations of " << it->first << " : " << std::endl;
-  //    it->second->print( out, it->first );
-  //  }
-  //}else{
+  if( options::incrementalSolving() ){
+    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
+      out << "Instantiations of " << it->first << " : " << std::endl;
+      it->second->print( out, it->first );
+    }
+  }else{
     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
       out << "Instantiations of " << it->first << " : " << std::endl;
       it->second.print( out, it->first );
       out << std::endl;
     }
-  //}
+  }
 }
 
 QuantifiersEngine::Statistics::Statistics():