Public interface for quantifier elimination. Minor changes to datatypes rewriter.

2 files changed, 44 insertions, 0 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 5eca87903..f2d5c640d 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -212,6 +212,18 @@ void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& term
   }
 }
 
+void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const {
+  if( terms.size()==q[0].getNumChildren() ){
+    insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+  }else{
+    for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
+      terms.push_back( it->first );
+      it->second.getInstantiations( insts, q, vars, terms );
+      terms.pop_back();
+    }
+  }
+}
+
 
 bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
                                     context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
@@ -298,6 +310,20 @@ void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& te
   }
 }
 
+void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const{
+  if( d_valid.get() ){
+    if( terms.size()==q[0].getNumChildren() ){
+      insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+    }else{
+      for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
+        terms.push_back( it->first );
+        it->second->getInstantiations( insts, q, vars, terms );
+        terms.pop_back();
+      }
+    }
+  }
+}
+
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index f1c1c952a..abe31b48d 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -101,6 +101,7 @@ public:
   std::map< Node, InstMatchTrie > d_data;
 private:
   void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
+  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const;
 public:
   InstMatchTrie(){}
   ~InstMatchTrie(){}
@@ -131,6 +132,14 @@ public:
     std::vector< TNode > terms;
     print( out, q, terms );
   }
+  void getInstantiations( std::vector< Node >& insts, Node q ) {
+    std::vector< TNode > terms;
+    std::vector< TNode > vars;
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      vars.push_back( q[0][i] );
+    }
+    getInstantiations( insts, q, vars, terms );
+  }
   void clear() { d_data.clear(); }
 };/* class InstMatchTrie */
 
@@ -143,6 +152,7 @@ public:
   context::CDO< bool > d_valid;
 private:
   void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
+  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const;
 public:
   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
   ~CDInstMatchTrie(){}
@@ -173,6 +183,14 @@ public:
     std::vector< TNode > terms;
     print( out, q, terms );
   }
+  void getInstantiations( std::vector< Node >& insts, Node q ) {
+    std::vector< TNode > terms;
+    std::vector< TNode > vars;
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      vars.push_back( q[0][i] );
+    }
+    getInstantiations( insts, q, vars, terms );
+  }
 };/* class CDInstMatchTrie */