More misc. arithmetic cleanup. Removing unused files and functions. Also removing an ugly forward declaration that was needed to get error set bound information on basic variables.

1 files changed, 15 insertions, 1 deletions

diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 0d754d159..718799e9f 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -3,10 +3,10 @@
 
 #include "expr/node.h"
 #include "util/rational.h"
-#include "context/cdlist.h"
 
 #include "theory/arith/theory_arith_private_forward.h"
 #include "theory/arith/arithvar.h"
+#include "theory/arith/bound_counts.h"
 
 namespace CVC4 {
 namespace theory {
@@ -87,6 +87,20 @@ public:
   void operator()(Node n);
 };
 
+class BoundCountingLookup {
+private:
+  TheoryArithPrivate& d_ta;
+public:
+  BoundCountingLookup(TheoryArithPrivate& ta) : d_ta(ta) {}
+  const BoundsInfo& boundsInfo(ArithVar basic) const;
+  BoundCounts atBounds(ArithVar basic) const{
+    return boundsInfo(basic).atBounds();
+  }
+  BoundCounts hasBounds(ArithVar basic) const {
+    return boundsInfo(basic).hasBounds();
+  }
+};
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */