1 files changed, 45 insertions, 37 deletions
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 03cb81785..5e933ea49 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -17,9 +17,10 @@
 
 #pragma once
 
+#include <stdint.h>
+
 #include <map>
 #include <queue>
-#include <stdint.h>
 #include <vector>
 
 #include "context/cdhashset.h"
@@ -32,18 +33,16 @@
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "options/arith_options.h"
+#include "smt/environment.h"
 #include "smt/logic_exception.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/arith/arith_rewriter.h"
-#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/attempt_solution_simplex.h"
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint.h"
-#include "theory/arith/constraint.h"
-#include "theory/arith/delta_rational.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/dio_solver.h"
 #include "theory/arith/dual_simplex.h"
@@ -51,10 +50,8 @@
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/matrix.h"
-#include "theory/arith/matrix.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/partial_model.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/soi_simplex.h"
 #include "theory/arith/theory_arith.h"
@@ -91,10 +88,11 @@ class NonlinearExtension;
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArithPrivate {
-private:
-
+ private:
   static const uint32_t RESET_START = 2;
 
+  Environment* d_env;
+
   TheoryArith& d_containing;
 
   bool d_nlIncomplete;
@@ -423,47 +421,57 @@ private:
   Node ppRewriteTerms(TNode atom);
 
 public:
-  TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
-  ~TheoryArithPrivate();
-
-  /**
-   * Does non-context dependent setup for a node connected to a theory.
-   */
-  void preRegisterTerm(TNode n);
-  Node expandDefinition(LogicRequest &logicRequest, Node node);
-
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ TheoryArithPrivate(Environment* env,
+                    TheoryArith& containing,
+                    context::Context* c,
+                    context::UserContext* u,
+                    OutputChannel& out,
+                    Valuation valuation,
+                    const LogicInfo& logicInfo);
+ ~TheoryArithPrivate();
 
-  void check(Theory::Effort e);
-  bool needsCheckLastEffort();
-  void propagate(Theory::Effort e);
-  Node explain(TNode n);
-  bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
-  bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp );
+ /**
+  * Does non-context dependent setup for a node connected to a theory.
+  */
+ void preRegisterTerm(TNode n);
+ Node expandDefinition(LogicRequest& logicRequest, Node node);
 
-  Rational deltaValueForTotalOrder() const;
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
-  bool collectModelInfo(TheoryModel* m);
+ void check(Theory::Effort e);
+ bool needsCheckLastEffort();
+ void propagate(Theory::Effort e);
+ Node explain(TNode n);
+ bool getCurrentSubstitution(int effort,
+                             std::vector<Node>& vars,
+                             std::vector<Node>& subs,
+                             std::map<Node, std::vector<Node> >& exp);
+ bool isExtfReduced(int effort, Node n, Node on, std::vector<Node>& exp);
 
-  void shutdown(){ }
+ Rational deltaValueForTotalOrder() const;
 
-  void presolve();
-  void notifyRestart();
-  Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+ bool collectModelInfo(TheoryModel* m);
 
-  std::string identify() const { return std::string("TheoryArith"); }
+ void shutdown() {}
 
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
+ void presolve();
+ void notifyRestart();
+ Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ Node ppRewrite(TNode atom);
+ void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 
-  void addSharedTerm(TNode n);
+ std::string identify() const { return std::string("TheoryArith"); }
 
-  Node getModelValue(TNode var);
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+ void addSharedTerm(TNode n);
 
-  std::pair<bool, Node> entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out);
+ Node getModelValue(TNode var);
 
+ std::pair<bool, Node> entailmentCheck(
+     TNode lit,
+     const ArithEntailmentCheckParameters& params,
+     ArithEntailmentCheckSideEffects& out);
 
 private: