1 files changed, 10 insertions, 15 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 43c962e30..decbf93bd 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -21,7 +21,9 @@
 #include "theory/arith/arith_preprocess.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
+#include "theory/arith/branch_and_bound.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/arith/pp_rewrite_eq.h"
 #include "theory/theory.h"
 
 namespace cvc5 {
@@ -39,16 +41,7 @@ class TheoryArithPrivate;
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArith : public Theory {
- private:
   friend class TheoryArithPrivate;
-
-  TheoryArithPrivate* d_internal;
-
-  TimerStat d_ppRewriteTimer;
-
-  /** Used to prove pp-rewrites */
-  EagerProofGenerator d_ppPfGen;
-
  public:
   TheoryArith(context::Context* c,
               context::UserContext* u,
@@ -136,17 +129,20 @@ class TheoryArith : public Theory {
   }
 
  private:
-  /**
-   * Preprocess equality, applies ppRewrite for equalities. This method is
-   * distinct from ppRewrite since it is not allowed to construct lemmas.
-   */
-  TrustNode ppRewriteEq(TNode eq);
   /** Get the proof equality engine */
   eq::ProofEqEngine* getProofEqEngine();
+  /** Timer for ppRewrite */
+  TimerStat d_ppRewriteTimer;
   /** The state object wrapping TheoryArithPrivate  */
   ArithState d_astate;
   /** The arith::InferenceManager. */
   InferenceManager d_im;
+  /** The preprocess rewriter for equality */
+  PreprocessRewriteEq d_ppre;
+  /** The branch and bound utility */
+  BranchAndBound d_bab;
+  /** The (old) linear arithmetic solver */
+  TheoryArithPrivate* d_internal;
 
   /**
    * The non-linear extension, responsible for all approaches for non-linear
@@ -159,7 +155,6 @@ class TheoryArith : public Theory {
   ArithPreprocess d_arithPreproc;
   /** The theory rewriter for this theory. */
   ArithRewriter d_rewriter;
-
 };/* class TheoryArith */
 
 }  // namespace arith