1 files changed, 5 insertions, 3 deletions

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5bf3d7900..5004a82dc 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -48,7 +48,7 @@ private:
   /** calculated no match terms */

   bool d_matching_active;

   /** terms processed */

-  std::map< Node, bool > d_processed;

+  std::hash_set< Node, NodeHashFunction > d_processed;

 public:

   TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}

   ~TermDb(){}

@@ -61,7 +61,7 @@ public:
   /** map from type nodes to terms of that type */

   std::map< TypeNode, std::vector< Node > > d_type_map;

   /** add a term to the database */

-  void addTerm( Node n, std::vector< Node >& added, bool withinQuant = false );

+  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );

   /** reset (calculate which terms are active) */

   void reset( Theory::Effort effort );

   /** set active */

@@ -75,7 +75,9 @@ public:
         has operator "op", and n'["index"] = n.

       for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }

   */

-  std::map< Node, std::map< Node, std::map< int, std::vector< Node > > > > d_parents;

+  /* Todo replace int by size_t */

+  std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node >  >, NodeHashFunction  > , NodeHashFunction > d_parents;

+  const std::vector<Node> & getParents(TNode n, TNode f, int arg);

 private:

   //map from types to model basis terms

   std::map< TypeNode, Node > d_model_basis_term;