1 files changed, 77 insertions, 0 deletions
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
new file mode 100644
index 000000000..4a6943119
--- /dev/null
+++ b/src/theory/quantifiers/equality_infer.h
@@ -0,0 +1,77 @@
+/*********************                                                        */
+/*! \file equality_infer.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief additional inference for equalities
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef EQUALITY_INFER_H
+#define EQUALITY_INFER_H
+
+#include <ext/hash_set>
+#include <iostream>
+#include <map>
+#include <vector>
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "context/cdhashset.h"
+#include "theory/theory.h"
+
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class EqualityInference
+{
+  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
+  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
+  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDHashMap< Node, NodeList *, NodeHashFunction > NodeListMap;
+private:
+  context::Context * d_c;
+  Node d_one;
+  class EqcInfo {
+  public:
+    EqcInfo(context::Context* c);
+    ~EqcInfo(){}
+    context::CDO< Node > d_rep;
+    context::CDO< bool > d_valid;
+  };
+
+  /** information necessary for equivalence classes */
+  NodeMap d_elim_vars;
+  std::map< Node, EqcInfo * > d_eqci;
+  NodeMap d_rep_to_eqc;
+  /** set eqc rep */
+  void setEqcRep( Node t, Node r, EqcInfo * eqci );
+  /** use list */
+  NodeListMap d_uselist;
+  void addToUseList( Node used, Node eqc );
+public:
+  EqualityInference(context::Context* c);
+  virtual ~EqualityInference();
+  /** notification when equality engine is updated */
+  void eqNotifyNewClass(TNode t);
+  void eqNotifyMerge(TNode t1, TNode t2);
+  
+  NodeList d_pending_merges;
+};
+
+}
+}
+}
+
+#endif