Finish --dump-instantiations option. Update scripts.

2 files changed, 11 insertions, 11 deletions

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 */