Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLazy for stringsExp.

1 files changed, 8 insertions, 5 deletions

diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 4a6943119..70b05c351 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef EQUALITY_INFER_H
-#define EQUALITY_INFER_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
+#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
 
 #include <ext/hash_set>
 #include <iostream>
@@ -60,14 +60,17 @@ private:
   /** use list */
   NodeListMap d_uselist;
   void addToUseList( Node used, Node eqc );
+  /** pending merges */
+  NodeList d_pending_merges;
 public:
   EqualityInference(context::Context* c);
   virtual ~EqualityInference();
-  /** notification when equality engine is updated */
+  /** input : notification when equality engine is updated */
   void eqNotifyNewClass(TNode t);
   void eqNotifyMerge(TNode t1, TNode t2);
-  
-  NodeList d_pending_merges;
+  /** output : inferred equalities */
+  unsigned getNumPendingMerges() { return d_pending_merges.size(); }
+  Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; }  
 };
 
 }