merge from symmetry branch

1 files changed, 7 insertions, 2 deletions

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index eaab96f27..d78504dc8 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -27,6 +27,7 @@
 
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/uf/symmetry_breaker.h"
 
 #include "context/cdo.h"
 #include "context/cdset.h"
@@ -87,6 +88,9 @@ private:
   /** True node for predicates = false */
   Node d_false;
 
+  /** Symmetry analyzer */
+  SymmetryBreaker d_symb;
+
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
@@ -113,12 +117,13 @@ public:
   void preRegisterTerm(TNode term);
   void explain(TNode n);
 
+  void staticLearning(TNode in, NodeBuilder<>& learned);
+  void presolve();
+
   std::string identify() const {
     return "THEORY_UF";
   }
 
-  void staticLearning(TNode in, NodeBuilder<>& learned);
-
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */