1 files changed, 9 insertions, 16 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index e1c55f113..a5d64a652 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -72,12 +72,10 @@
 #include "context/cdqueue.h"
 
 #include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/delta_rational.h"
-
 #include "theory/arith/congruence_manager.h"
-
 #include "theory/arith/constraint_forward.h"
+#include "theory/arith/callbacks.h"
 
 #include <vector>
 #include <list>
@@ -604,6 +602,8 @@ public:
   /** The node must have a proof already and be eligible for propagation! */
   void propagate();
 
+  bool satisfiedBy(const DeltaRational& dr) const;
+
 private:
   /**
    * Marks the node as having a proof and being selfExplaining.
@@ -620,11 +620,6 @@ private:
   void markAsTrue(Constraint a, Constraint b);
   void markAsTrue(const std::vector<Constraint>& b);
 
-public:
-
-
-private:
-
   void debugPrint() const;
 
   /**
@@ -776,20 +771,18 @@ private:
   static bool emptyDatabase(const std::vector<PerVariableDatabase>& vec);
 
   /** Map from nodes to arithvars. */
-  const ArithVarNodeMap& d_av2nodeMap;
+  const ArithVariables& d_avariables;
 
-  const ArithVarNodeMap& getArithVarNodeMap() const{
-    return d_av2nodeMap;
+  const ArithVariables& getArithVariables() const{
+    return d_avariables;
   }
 
   ArithCongruenceManager& d_congruenceManager;
 
-  //Constraint allocateConstraintForLiteral(ArithVar v, Node literal);
-
   const context::Context * const d_satContext;
   const int d_satAllocationLevel;
 
-  NodeCallBack& d_raiseConflict;
+  RaiseConflict d_raiseConflict;
 
   friend class ConstraintValue;
 
@@ -797,9 +790,9 @@ public:
 
   ConstraintDatabase( context::Context* satContext,
                       context::Context* userContext,
-                      const ArithVarNodeMap& av2nodeMap,
+                      const ArithVariables& variables,
                       ArithCongruenceManager& dm,
-                      NodeCallBack& conflictCallBack);
+                      RaiseConflict conflictCallBack);
 
   ~ConstraintDatabase();