1 files changed, 6 insertions, 11 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 2bfd7e16c..4a8369483 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -26,6 +26,7 @@
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
+#include "theory/uf/proof_equality_engine.h"
 #include "theory/uf/symmetry_breaker.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
@@ -112,17 +113,6 @@ private:
    */
   bool propagateLit(TNode literal);
 
-  /**
-   * Explain why this literal is true by adding assumptions
-   * with proof (if "pf" is non-NULL).
-   */
-  void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf);
-
-  /**
-   * Explain a literal, with proof (if "pf" is non-NULL).
-   */
-  Node explain(TNode literal, eq::EqProof* pf);
-
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionsTerms;
 
@@ -202,6 +192,9 @@ private:
   CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
 
  private:
+  /** Explain why this literal is true by building an explanation */
+  void explain(TNode literal, Node& exp);
+
   bool areCareDisequal(TNode x, TNode y);
   void addCarePairs(const TNodeTrie* t1,
                     const TNodeTrie* t2,
@@ -213,6 +206,8 @@ private:
   UfProofRuleChecker d_ufProofChecker;
   /** A (default) theory state object */
   TheoryState d_state;
+  /** A (default) inference manager */
+  TheoryInferenceManager d_im;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */