1 files changed, 0 insertions, 116 deletions
diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
deleted file mode 100644
index 8887daa8d..000000000
--- a/src/theory/arith/ordered_set.h
+++ /dev/null
@@ -1,116 +0,0 @@
-/*********************                                                        */
-/*! \file ordered_set.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ORDERED_SET_H
-#define __CVC4__THEORY__ARITH__ORDERED_SET_H
-
-#include <map>
-#include <set>
-#include "expr/kind.h"
-#include "expr/node.h"
-#include "util/Assert.h"
-#include "theory/arith/arith_utilities.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-inline const Rational& rightHandRational(TNode ineq){
-  Assert(ineq.getKind() == kind::LEQ
-         || ineq.getKind() == kind::GEQ
-         || ineq.getKind() == kind::EQUAL);
-  TNode righthand = ineq[1];
-  Assert(righthand.getKind() == kind::CONST_RATIONAL);
-  return righthand.getConst<Rational>();
-}
-
-class BoundValueEntry {
-private:
-  const Rational& value;
-  TNode d_leq, d_geq;
-
-  BoundValueEntry(const Rational& v, TNode l, TNode g):
-    value(v),
-    d_leq(l),
-    d_geq(g)
-  {}
-
-public:
-  Node getLeq() const{
-    Assert(hasLeq());
-    return d_leq;
-  }
-  Node getGeq() const{
-    Assert(hasGeq());
-    return d_geq;
-  }
-
-  static BoundValueEntry mkFromLeq(TNode leq){
-    Assert(leq.getKind() == kind::LEQ);
-    return BoundValueEntry(rightHandRational(leq), leq, TNode::null());
-  }
-
-  static BoundValueEntry mkFromGeq(TNode geq){
-    Assert(geq.getKind() == kind::GEQ);
-    return BoundValueEntry(rightHandRational(geq), TNode::null(), geq);
-  }
-
-  void addLeq(TNode leq){
-    Assert(leq.getKind() == kind::LEQ);
-    Assert(rightHandRational(leq) == getValue());
-    // [MGD] With context-dependent pre-registration, we could get the
-    // same one twice
-    Assert(!hasLeq() || d_leq == leq);
-    d_leq = leq;
-  }
-
-  void addGeq(TNode geq){
-    Assert(geq.getKind() == kind::GEQ);
-    Assert(rightHandRational(geq) == getValue());
-    // [MGD] With context-dependent pre-registration, we could get the
-    // same one twice
-    Assert(!hasGeq() || d_geq == geq);
-    d_geq = geq;
-  }
-
-  bool hasGeq() const { return d_geq != TNode::null(); }
-  bool hasLeq() const { return d_leq != TNode::null(); }
-
-
-  const Rational& getValue() const{
-    return value;
-  }
-
-  bool operator<(const BoundValueEntry& other){
-    return value < other.value;
-  }
-};
-
-typedef std::map<Rational, BoundValueEntry> BoundValueSet;
-
-typedef std::set<TNode, RightHandRationalLT> EqualValueSet;
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ORDERED_SET_H */