From: Tim King <taking@cs.nyu.edu>
Date: Thu, 17 Feb 2011 00:55:11 +0000 (+0000)
Subject: Deleting depricated files.
X-Git-Tag: cvc5-1.0.0~8709
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6bfdda562cc4d838f9b1e90b7c7107162bf5200e;p=cvc5.git

Deleting depricated files.
---

diff --git a/src/theory/arith/arithvar_dense_set.h b/src/theory/arith/arithvar_dense_set.h
deleted file mode 100644
index 274246fbe..000000000
--- a/src/theory/arith/arithvar_dense_set.h
+++ /dev/null
@@ -1,72 +0,0 @@
-/*********************                                                        */
-/*! \file arithvar_dense_set.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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 <vector>
-#include "theory/arith/arith_utilities.h"
-
-
-#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H
-#define __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class ArithVarDenseSet {
-private:
-  std::vector<bool> d_set;
-
-public:
-  ArithVarDenseSet() : d_set() {}
-
-  size_t size() const {
-    return d_set.size();
-  }
-
-  void increaseSize(ArithVar max){
-    Assert(max >= size());
-    d_set.resize(max+1, false);
-  }
-
-  bool isMember(ArithVar x) const{
-    return d_set[x];
-  }
-
-  void init(ArithVar x, bool val) {
-    Assert(x >= size());
-    increaseSize(x);
-    d_set[x] = val;
-  }
-
-  void add(ArithVar x){
-    Assert(!isMember(x));
-    d_set[x] = true;
-  }
-
-  void remove(ArithVar x){
-    Assert(isMember(x));
-    d_set[x] = false;
-  }
-};
-
-}; /* namespace arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
-#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H */
diff --git a/src/theory/arith/normal_form_notes.txt b/src/theory/arith/normal_form_notes.txt
deleted file mode 100644
index a692ef471..000000000
--- a/src/theory/arith/normal_form_notes.txt
+++ /dev/null
@@ -1,566 +0,0 @@
-
-/** DRAFT 1
- * Normal form for predicates:
- *    TRUE
- *    FALSE
- *    var_i |><| b
- *    \sum_i product_i  |><| b
- *  where
- *   1) b is of type CONST_RATIONAL
- *   2) |><| is of type <=, >, =, < or >=
- *   3) product_i is in product normal form,
- *   4) product_i is not 0,
- *   5) product_i's are in strictly ascending productOrder,
- *   6) product_i has at least 2 members,
- *   7) product_1 has a positive coefficient, and
- *   8) var_i has metakind variable.
- *
- * Normal form for terms:
- *    c
- *    c + \sum_i product_i
- *  where
- *   1) c is of type CONST_RATIONAL,
- *   2) product_i is in product normal form,
- *   3) product_i is not a constant,
- *   4) and product_i's are in strictly ascending productOrder.
- *
- * Normal form for products:
- *    d
- *    var_i
- *    e * \prod var_i
- *  where
- *   1) d,e is of type CONST_RATIONAL,
- *   2) e != 0,
- *   3) e != 1 or there are at least 2 variables,
- *   2) var_i is of metakind VARIABLE,
- *   3) and var_i are in increasing (not strict) nodeOrder.
- *
- * productOrder is well defined over normal form products as follows:
- *   cmp(d,d') = rational order.
- *   cmp(d,var_i)= -1
- *   cmp(var_i,var_j) is the node order
- *   cmp(var_i,d * \prod var_i) = -1
- *   cmp(p = d * \prod var_i, p' = d' * \prod var_i')=
- *      if(len(p) == len(p'))
- *      then tupleCompare(var_i, var_i')
- *      else len(p) - len(p')
- */
-
-
-
-/** DRAFT 2
- * Normal form for predicates:
- *    TRUE
- *    FALSE
- *    var |><| b
- *    (\sum_{i=1 to N} p_i)  |><| b
- *  where
- *   1) b is of type CONST_RATIONAL
- *   2) |><| is of kind <, <=, =, >= or >
- *   3) p_i is in PNF,
- *   5) p_i's are in strictly ascending <p,
- *   6) N >= 2,
- *   7) the kind of (\sum_{i=1 to N} p_i) is an N arity PLUS,
- *   8) p_1 has coefficient 1, and
- *   9) var has metakind variable.
- *
- * PNF:
- *    v
- *    d * v
- *    (\prod_{i=1 to M} v_i)
- *    d * (\prod_{i=1 to M} v_i)
- *  where
- *   1) d is of type CONST_RATIONAL,
- *   2) d != 0,
- *   3) d != 1,
- *   4) M>=2,
- *   5) v, v_i are of metakind VARIABLE,
- *   6) v_i are in increasing (not strict) nodeOrder, and
- *   7) the kind of (\prod_{i=1 to M} v_i) is an M arity MULT.
- *
- * <p is defined over PNF as follows (skipping some symmetry):
- *   cmp(  v,   v') is the node order over v and v'
- *   cmp(  v,d'*v') is the node order over v and v'
- *   cmp(d*v,d'*v') is the node order over v and v'
- *   cmp(  v,   (\prod v'_i)) = -1
- *   cmp(d*v,   (\prod  v_i)) = -1
- *   cmp(  v, d*(\prod v'_i)) = -1
- *   cmp(d*v, d*(\prod  v_i)) = -1
- *   cmp((\prod_{i=1 to M} v_i),(\prod_{i=1 to M'} v'_i))=
- *      if(M == M')
- *      then tupleCompare(v_i, v'_i)
- *      else M - M'
- *   cmp((\prod_{i=1 to M} v_i), d*(\prod_{i=1 to M'} v'_i))=
- *      if(M == M')
- *      then tupleCompare(v_i, v'_i)
- *      else M - M'
- *   cmp(d * (\prod_{i=1 to M} v_i), d' * (\prod_{i=1 to M'} v'_i))=
- *      if(M == M')
- *      then tupleCompare(v_i, v'_i)
- *      else M - M'
- *
- * Rewrite Normal Form for Terms:
- *    b
- *    p
- *    c + p
- *    (\sum_{i=1 to N} p_i)
- *    c + (\sum_{i=1 to N} p_i)
- *  where
- *   1) b,c is of type CONST_RATIONAL,
- *   2) c != 0,
- *   3) p, p_i is in PNF,
- *   4) N >= 2
- *   5) the kind of (\sum_{i=1 to N} p_i) is an N arity PLUS,
- *   6) and p_i's are in strictly <p.
- *
- */
-
-
-bool isVarMultList(TNode v){
-  for(v = 1 to l.getLength()){
-    if(!isVar(v[i])){
-      return false;
-    }
-  }
-
-  for(v = 2 to l.getLength()){
-    if(!(v[i-1] <= v[i])){
-      return false;
-    }
-  }
-  return true;
-}
-
-bool isPNF(TNode p){
-   if(p.getKind() == MULT){
-     if(p[0].getKind() == CONST_RATIONAL){
-       if(p[0].getConst<CONST_RATIONAL>() != 0 &&
-          p[0].getConst<CONST_RATIONAL> != 1){
-         if(p[1].getKind() != MULT){
-           if(p[1].getMetaKind() == VARIABLE){
-             return true; // d * v
-           }else{
-             return false;
-           }
-         }else{
-           if(isVarMultList(p[1])){
-             return true; // d * (\prod_{i=1 to M} v_i)
-           }else{
-             return false;
-           }
-         }
-       }else{
-         return false;
-       }
-     }else{
-       if(isVarMultList(p)){
-         return true; //(\prod_{i=1 to M} v_i)
-       }else{
-         return false;
-       }
-     }
-   }else{
-     if(p.getMetaKind() == VARIABLE){
-       return true; // v
-     }else{
-       return false;
-     }
-   }
-}
-
-
-bool <p(TNode p0, TNode p1){
-  PNFType t0 = same as the comments in isPNF(p0);
-  PNFType t1 = same as the comments in isPNF(p1);
-
-  bool t0IsVar = (t0 == "v") ||(t0 == "d*v");
-  bool t1IsVar = (t1 == "v") ||(t1 == "d*v");
-
-  if(t0IsVar && t1IsVar){
-    TNode v0 = (t0 == "d*v") ? p0[1] : p0;
-    TNode v1 = (t1 == "d*v") ? p1[1] : p1;
-    return v0 < v1;
-  }else if(!t0IsVar && t1IsVar){
-    return false;
-  }else if(t0IsVar && !t1IsVar){
-    return true;
-  }else{
-    TNode prod0 = (t0 == "d * (\prod_{i=1 to M} v_i)") ? p0[1] : p0;
-    TNode prod1 = (t1 == "d * (\prod_{i=1 to M} v_i)") ? p1[1] : p1;
-
-    int M0 = prod0.getNumChildren();
-    int M1 = prod1.getNumChildren();
-
-    if(M0 == M1){
-      for(i in 1 to M0){
-        if(prod0[i] < prod[i]){
-          return true;
-        }
-      }
-      return false;
-    }else{
-      return M0 < M1;
-    }
-  }
-}
-
-bool isPNFSum(TNode p){
-
-  for(i = 1 to p.getNumChildren()){
-    if(!isPNF(p[i])){
-      return false;
-    }
-  }
-  for(i = 2 to p.getNumChildren()){
-    if(!(p[i-1] <p p[i])){
-      return false;
-    }
-  }
-  return true;
-}
-
-string isNormalFormTerm(TNode t){
-  Kind k = t.getKind();
-  if(k != PLUS){
-    if(k == CONST_RATIONAL){
-      return true; // b
-    }else if(isPNF(p)){
-      return true; // p
-    }else{
-      return false;
-    }
-  }else{
-    if(t[0].getKind() == CONST_RATIONAL){
-      if(t[0].getConst<CONST_RATIONAL>() != 0){
-        if(t[1].getKind() == PLUS){
-          if(isPNFSum(t[1])){
-            return true; // c + (\sum_{i=1 to N} p_i)
-          }else{
-            return false;
-          }
-        }else{
-          if(isPNF(t[1])){
-            return true; // c + p
-          }else{
-            return false;
-          }
-        }
-      }else{
-        return false;
-      }
-    }else{
-      if(isPNFSum(t)){
-        return true; // (\sum_{i=1 to N} p_i)
-      }else{
-        return false;
-      }
-    }
-  }
-}
-
-/***********************************************/
-/***********************************************/
-/******************* DRAFT 3 *******************/
-/***********************************************/
-/***********************************************/
-
-/** DRAFT 3
- * Normal form for predicates:
- *    TRUE
- *    FALSE
- *    v |><| b
- *    p |><| b
- *    (+ p_1 .. p_N)  |><| b
- *  where
- *   1) b is of type CONST_RATIONAL
- *   2) |><| is of kind <, <=, =, >= or >
- *   3) p, p_i is in PNF,
- *   5) p_i's are in strictly ascending <p,
- *   6) N >= 2,
- *   7) the kind of (+ p_1 .. p_N) is an N arity PLUS,
- *   8) p.d, p_1.d are 1, and
- *   9) v has metakind variable.
- *
- * PNF(t):
- *    (* d v_1 v_2 ... v_M)
- *  where
- *   1) d is of type CONST_RATIONAL,
- *   2) d != 0,
- *   4) M>=1,
- *   5) v_i are of metakind VARIABLE,
- *   6) v_i are in increasing (not strict) nodeOrder, and
- *   7) the kind of t is an M+1 arity MULT.
- *
- * <p is defined over PNF as follows (skipping some symmetry):
- *   cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
- *      if(M == M'):
- *      then tupleCompare(v_i, v'_i)
- *      else M -M'
- *
- * Rewrite Normal Form for Terms:
- *    b
- *    v
- *    (+ c p_1 p_2 ... p_N)  |  not(N=1 and c=0 and p_1.d=1)
- *  where
- *   1) b,c is of type CONST_RATIONAL,
- *   2) c != 0,
- *   3) p_i is in PNF,
- *   4) N >= 1
- *   5) the kind of (+ c p_1 p_2 ... p_N) is an N+1 arity PLUS,
- *   6) and p_i's are in strictly <p.
- *
- */
-
-
-/* Assuming that the terms have been normalized, how much work is the case splitting.
- * The following should provide a good insight into how difficult it is to use
- * these normal forms when writing code.
- */
-
-enum PredicateNFKind{TRUE, FALSE, v |><| b, p |><| b, (+ p_1 .. p_N)  |><| b};
-
-PredicateNFKind kindOfNormalFormPredicate(TNode n){
-  if(n.getKind() == CONST_BOOLEAN){
-    if(n.getConst<bool>()){
-      return TRUE;
-    }else{
-      return FALSE;
-    }
-  }else{
-    TNode left = n[0];
-    if(left.getMetaKind() == metakind::VARIABLE){
-      return v |><| b;
-    }else if(left.getKind() == MULT){
-      return p |><| b;
-    }else{
-      return (+ p_1 .. p_N)  |><| b;
-    }
-  }
-}
-
-enum TermNFKind{c, v, (+ c p_1 p_2 ... p_N)};
-
-TermNFKind kindOfTermNFKind(TNode n){
-  if(n.getMetaKind() == metakind::CONSTANT){
-     return c;
-  }else if(n.getMetaKind() == metakind::VARIABLE){
-     return v;
-  }else{
-     return (+ c p_1 p_2 ... p_N) 
-  }
-}
-
-
-/* Verify that the term meets all of the criteria for a normal form.
- * This should provide good insight into how difficult it is to write/debug
- * the rewriters themselves, and other parts of the code that are
- * "highly knowledgable" about the normal form (such as helper functions).
- */
-
-
-bool rangeIsSorted(bool strict, TNode::iterator start, TNode::iterator stop, NodeComparitor cmp){
-  if(start == stop) return true;
-  TNode prev = *start;
-  ++start;
-  while(start != stop){
-    TNode curr = *start;
-    int tmp = cmp(prev, curr);
-    if(strict && tmp >= 0
-      !strict && tmp > 0
-    ){
-      return false;
-    }
-    prev = curr;
-    ++start;
-  }
-  return true;
-}
-
-bool rangeAll(TNode::iterator start, TNode::iterator stop, NodePredicate rho){
-  for(;start != stop; ++start){
-    if(! rho(*start))  return false;
-  }
-  return true;
-}
-bool isPNF(TNode p){
-   return
-      p.getKind() == MULT &&
-      p[0].getKind() == CONST_RATIONAL&&
-      p[0].getConst<CONST_RATIONAL>() != 0 &&
-      rangeIsSorted(false, p.begin()+1, p.end(), nodeOrder) &&
-      rangeAll(p.begin()+1, p.end(), \t -> t.getMetaKind() == metakind::VARIABLE);
-}
-
-
-bool cmpPNF(TNode p0, TNode p1){
-  int M0 = p0.getNumChildren();
-  int M1 = p1.getNumChildren();
-
-  if(M0 == M1){
-    for(int i=1; i< M0; ++i){
-      int cmp = nodeOrder(p0[i],p1[i]);
-      if(cmp != 0){
-        return cmp;
-      }
-    }
-    return 0;
-  }else{
-    return M0 - M1;
-  }
-}
-
-bool isNormalFormTerm(TNode t){
-  if(t.getKind() == CONST_RATIONAL){
-    return true;
-  }else if(t.getMetaKind() == VARIABLE){
-    return true;
-  }else if(t.getKind() == PLUS){ //may be (+ c p_1 p_2 ... p_N)
-    int N = t.getNumChildren()-1;
-    TNode c = t[0];
-    return c.getKind() == CONST_RATIONAL &&
-           c.getConst<Rational>() !- 0 &&
-           N >= 1 &&  //This check is redundent because of an invariant in NodeBuilder<>
-           rangeAll(p.begin()+1, p.end(), isPNF) &&
-           rangeIsSorted(true, p.begin()+1, p.end(), cmpPNF);
-  }else{
-    return false;
-  }
-}
-
-bool isNormalFormAtom(TNode n){
-  if(n.getKind() == CONST_BOOLEAN){
-    return true;
-  }else if(n.getKind() \in {<, <=, ==, >=, >}){
-    TNode left = n[0];
-    TNode right = n[1];
-    if(right.getKind() == CONST_RATIONAL){
-      if(left.getMetaKind() == VARIABLE){
-        return true;
-      }else if(left.getKind() == MULT){
-        return isPNF(left) && left[0] == 1;
-      }else if(left.getKind() == PLUS){
-        return left.getNumChildren() >= 2 &&
-               rangeAll(left.begin(), left.end(), isPNF) &&
-               left[0][0] == 1 &&
-               rangeIsSorted(true, left.begin(), left.end(), cmpPNF);
-      }else{
-        return false;
-      }
-    }else{
-      return false;
-    }
-  }else{
-    return false;
-  }
-}
-
-/***********************************************/
-/***********************************************/
-/******************* DRAFT 4 *******************/
-/***********************************************/
-/***********************************************/
-
-/** DRAFT 4
- * variable := n
- *   guards
- *     n getMetaKind() == metakind::VARIABLE
-
- * constant := n
- *   guards
-      n.getKind() == kind::CONST_RATIONAL
-
- * monomial := variable | (* [variable])
- *   guards
- *     len [variable] >= 2
- *     isSorted nodeOrder (getMList monomial)
-
-
- * coeff_mono := monomial | (* coeff monomial)
- *   guards
- *     coeff is renaming for constant
-       coeff \not\in {0,1}
-
- * sum := coeff_mono | (+ [coeff_mono])
- *   guards
- *     len [coeff_mono] >= 2
- *     isStronglySorted cmono_cmp [coeff_mono]
-
- * cons_sum := sum |  (+ constant_1 sum) | constant_0
- *   guards
- *     constant_1, constant_0 are accepted by constant
- *     constant_1 != 1
-
- * comparison := leads_with_one |><| constant
- *   guards
- *     |><| is GEQ, EQ, LEQ
- *     isStronglySorted cmono_cmp (monomial::[coeff_monomial])
- *     leads with_one is a subexpression of sum s.t. it is also accepted by
- *     leads_with_one :=  monomial | (+ monomial [coeff_monomial])
-
- * Normal Form for terms := cons_sum
- * Normal Form for atoms := TRUE | FALSE | comparison | (not comparison)
- *
- * Important Notes:
- *
- *  The languages for each are stratified. i.e. it is either the case that
- *  they or all of their children belong to a language that is strictly
- *  smaller according to the following partial order.
- *    constant -> monomial -> coeff_mono -> sum -> cons_sum
- *    variable                                     comparison
- *  This partial order is not unique, but it is simple.
- *
- *  This gives rise to the notion of the tightest language that accepts a node,
- *  which is simply the least according to the stratification order above.
- *
- *  Each subexpression of a normal form is also a normal form.
- *
- *  The tightest language that accepts a node does not always indicate the
- *  tighest language of the children:
- *     (+ v1 (* v1 v2) (* 2 (* v1 v2 v2)))
-
- * TAGGING:
- *  A node in normal form is tagged with the tightest binding above that
- *  accepts/generates it.
- *  All subexpressions are also in normal form and are also tagged.
- *  The tags for terms are as follows:
- *    enum { CONSTANT, VARIABLE, MONOMIAL, COEFF_MONOMIAL, SUM, CONS_SUM};
- */
-
- Auxillary
- let rec tuple_cmp elem_cmp pairs_list =
-      match pair_list with
-         [] -> 0
-        |(x,y)::ps -> let cmp_res = elem_cmp x y in
-                       if cmp_res <> 0
-                       then cmp_res
-                       else tuple_cmp elem_cmp ps
-
- let lex_cmp elem_cmp l0 l1 =
-      if len l0 == len l1
-      then tuple_cmp elem_cmp (zip l0 l1)
-      else (len l0) - (len l1)
-
- let rec adjacent l =
-      mathc l with
-       a::b::xs -> (a,b)::(adjacent b::xs)
-      | _ -> []
-
- let isWeaklySorted cmp l =
-     forall (fun (x,y) -> cmp x y <= 0) (adjacent l)
-
- let isStronglySorted cmp l =
-     forall (fun (x,y) -> cmp x y < 0) (adjacent l)
-
- let getMList monomial =
-         match monomial with
-           variable -> [variable]
-          |(* [variable]) -> [variable]
-
- let drop_coeff coeff_mono =
-      match coeff_mono in
-         monomial -> monomial
-        |(* coeff monomial) -> monomial
-
-let mono_cmp m0 m1 = lex_cmp nodeOrder (getMList m0) (getMList m1)
-let cmono_cmp cm0 cm1 = mono_cmp (drop_coeff cm0) (drop_coeff cm1)
-
diff --git a/src/theory/arith/ordered_bounds_list.h b/src/theory/arith/ordered_bounds_list.h
deleted file mode 100644
index f3bf3d58b..000000000
--- a/src/theory/arith/ordered_bounds_list.h
+++ /dev/null
@@ -1,231 +0,0 @@
-/*********************                                                        */
-/*! \file ordered_bounds_list.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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_BOUNDS_LIST_H
-#define __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
-
-#include "expr/node.h"
-#include "util/rational.h"
-#include "expr/kind.h"
-
-#include <vector>
-#include <algorithm>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-struct RightHandRationalLT
-{
-  bool operator()(TNode s1, TNode s2) const
-  {
-    Assert(s1.getNumChildren() >= 2);
-    Assert(s2.getNumChildren() >= 2);
-
-    Assert(s1[1].getKind() == kind::CONST_RATIONAL);
-    Assert(s2[1].getKind() == kind::CONST_RATIONAL);
-
-    TNode rh1 = s1[1];
-    TNode rh2 = s2[1];
-    const Rational& c1 = rh1.getConst<Rational>();
-    const Rational& c2 = rh2.getConst<Rational>();
-    return c1.cmp(c2) < 0;
-  }
-};
-
-struct RightHandRationalGT
-{
-  bool operator()(TNode s1, TNode s2) const
-  {
-    Assert(s1.getNumChildren() >= 2);
-    Assert(s2.getNumChildren() >= 2);
-
-    Assert(s1[1].getKind() == kind::CONST_RATIONAL);
-    Assert(s2[1].getKind() == kind::CONST_RATIONAL);
-
-    TNode rh1 = s1[1];
-    TNode rh2 = s2[1];
-    const Rational& c1 = rh1.getConst<Rational>();
-    const Rational& c2 = rh2.getConst<Rational>();
-    return c1.cmp(c2) > 0;
-  }
-};
-
-/**
- * An OrderedBoundsList is a lazily sorted vector of Arithmetic constraints.
- * The intended use is for a list of rewriting arithmetic atoms.
- * An example of such a list would be [(<= x 5);(= y 78); (>= x 9)].
- *
- * Nodes are required to have a CONST_RATIONAL child as their second node.
- * Nodes are sorted in increasing order according to RightHandRationalLT.
- *
- * The lists are lazily sorted in the sense that the list is not sorted until
- * an operation to access the element is attempted.
- *
- * An append() may make the list no longer sorted.
- * After an append() operation all iterators for the list become invalid.
- */
-class OrderedBoundsList {
-private:
-  bool d_isSorted;
-  std::vector<Node> d_list;
-
-public:
-  typedef std::vector<Node>::const_iterator iterator;
-  typedef std::vector<Node>::const_reverse_iterator reverse_iterator;
-
-  /**
-   * Constucts a new and empty OrderBoundsList.
-   * The empty list is initially sorted.
-   */
-  OrderedBoundsList() : d_isSorted(true){}
-
-  /**
-   * Appends a node onto the back of the list.
-   * The list may no longer be sorted.
-   */
-  void append(TNode n){
-    Assert(n.getNumChildren() >= 2);
-    Assert(n[1].getKind() == kind::CONST_RATIONAL);
-    d_isSorted = false;
-    d_list.push_back(n);
-  }
-
-  /** returns the size of the list */
-  unsigned int size(){
-    return d_list.size();
-  }
-
-  /** returns the i'th element in the sort list. This may sort the list.*/
-  TNode at(unsigned int idx){
-    sortIfNeeded();
-    return d_list.at(idx);
-  }
-
-  /** returns true if the list is known to be sorted. */
-  bool isSorted() const{
-    return d_isSorted;
-  }
-
-  /** sorts the list. */
-  void sort(){
-    d_isSorted = true;
-    std::sort(d_list.begin(), d_list.end(), RightHandRationalLT());
-  }
-
-  /**
-   * returns an iterator to the list that iterates in ascending order.
-   * This may sort the list.
-   */
-  iterator begin(){
-    sortIfNeeded();
-    return d_list.begin();
-  }
-  /**
-   * returns an iterator to the end of the list when interating in ascending order.
-   */
-  iterator end() const{
-    return d_list.end();
-  }
-
-  /**
-   * returns an iterator to the list that iterates in descending order.
-   * This may sort the list.
-   */
-  reverse_iterator rbegin(){
-    sortIfNeeded();
-    return d_list.rend();
-  }
-  /**
-   * returns an iterator to the end of the list when interating in descending order.
-   */
-  reverse_iterator rend() const{
-    return d_list.rend();
-  }
-
-  /**
-   * returns an iterator to the least strict upper bound of value.
-   * if the list is [(<= x 2);(>= x 80);(< y 70)]
-   * then *upper_bound((< z 70)) == (>= x 80)
-   *
-   * This may sort the list.
-   * see stl::upper_bound for more information.
-   */
-  iterator upper_bound(TNode value){
-    sortIfNeeded();
-    return std::upper_bound(begin(), end(), value, RightHandRationalLT());
-  }
-  /**
-   * returns an iterator to the greatest lower bound of value.
-   * This is bound is not strict.
-   * if the list is [(<= x 2);(>= x 80);(< y 70)]
-   * then *lower_bound((< z 70)) == (< y 70)
-   *
-   * This may sort the list.
-   * see stl::upper_bound for more information.
-   */
-  iterator lower_bound(TNode value){
-    sortIfNeeded();
-    return std::lower_bound(begin(), end(), value, RightHandRationalLT());
-  }
-  /**
-   * see OrderedBoundsList::upper_bound for more information.
-   * The difference is that the iterator goes in descending order.
-   */
-  reverse_iterator reverse_upper_bound(TNode value){
-    sortIfNeeded();
-    return std::upper_bound(rbegin(), rend(), value, RightHandRationalGT());
-  }
-  /**
-   * see OrderedBoundsList::lower_bound for more information.
-   * The difference is that the iterator goes in descending order.
-   */
-  reverse_iterator reverse_lower_bound(TNode value){
-    sortIfNeeded();
-    return std::lower_bound(rbegin(), rend(), value, RightHandRationalGT());
-  }
-
-  /**
-   * This is an O(n) method for searching the array to check if it contains n.
-   */
-  bool contains(TNode n) const {
-    for(std::vector<Node>::const_iterator i = d_list.begin(); i != d_list.end(); ++i){
-      if(*i == n) return true;
-    }
-    return false;
-  }
-private:
-  /** Sorts the list if it is not already sorted.  */
-  void sortIfNeeded(){
-    if(!d_isSorted){
-      sort();
-    }
-  }
-};
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H */