1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 61aa8257f..6201cf152 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -64,9 +64,11 @@ public:
   bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
   /** returns true is a and b are disequal in the current context */
   bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
+  /** get congruent term */
+  TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp );
 private:
   /** term index */
-  std::map< Node, TermArgTrie > d_func_map_trie;
+  std::map< Node, TermArgTrie > d_uf_func_map_trie;
   /** union find for terms beyond what is stored in equality engine */
   std::map< Node, Node > d_uf;
   std::map< Node, std::vector< Node > > d_uf_exp;
@@ -75,6 +77,8 @@ private:
   std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list;
   /** add arg */
   void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch );
+  /** register term */
+  void registerUfTerm( TNode n );
 public:
   enum {
     STATUS_CONFLICT,
@@ -110,10 +114,13 @@ private:
     virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
       return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
     }
+    virtual void filterInstantiations() { d_ip.filterInstantiations(); }
   };
   InstantiationNotifyInstPropagator d_notify;
   /** notify instantiation method */
   bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+  /** remove instance ids */
+  void filterInstantiations();  
   /** allocate instantiation */
   unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body );
   /** equality query */
@@ -142,6 +149,7 @@ private:
   std::vector< unsigned > d_update_list;
   /** relevant instances */
   std::map< unsigned, bool > d_relevant_inst;
+  bool d_has_relevant_inst;
 private:
   bool update( unsigned id, InstInfo& i, bool firstTime = false );
   void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );