src/theory/arith/ordered_bounds_list.h

   1
   2
   3 #include "cvc4_private.h"
   4
   5
   6 #ifndef __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
   7 #define __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
   8
   9 #include "expr/node.h"
  10 #include "util/rational.h"
  11 #include "expr/kind.h"
  12
  13 #include <vector>
  14 #include <algorithm>
  15
  16 namespace CVC4 {
  17 namespace theory {
  18 namespace arith {
  19
  20 struct RightHandRationalLT
  21 {
  22   bool operator()(TNode s1, TNode s2) const
  23   {
  24     Assert(s1.getNumChildren() >= 2);
  25     Assert(s2.getNumChildren() >= 2);
  26
  27     Assert(s1[1].getKind() == kind::CONST_RATIONAL);
  28     Assert(s2[1].getKind() == kind::CONST_RATIONAL);
  29
  30     TNode rh1 = s1[1];
  31     TNode rh2 = s2[1];
  32     const Rational& c1 = rh1.getConst<Rational>();
  33     const Rational& c2 = rh2.getConst<Rational>();
  34     return c1.cmp(c2) < 0;
  35   }
  36 };
  37
  38 struct RightHandRationalGT
  39 {
  40   bool operator()(TNode s1, TNode s2) const
  41   {
  42     Assert(s1.getNumChildren() >= 2);
  43     Assert(s2.getNumChildren() >= 2);
  44
  45     Assert(s1[1].getKind() == kind::CONST_RATIONAL);
  46     Assert(s2[1].getKind() == kind::CONST_RATIONAL);
  47
  48     TNode rh1 = s1[1];
  49     TNode rh2 = s2[1];
  50     const Rational& c1 = rh1.getConst<Rational>();
  51     const Rational& c2 = rh2.getConst<Rational>();
  52     return c1.cmp(c2) > 0;
  53   }
  54 };
  55
  56 /**
  57  * An OrderedBoundsList is a lazily sorted vector of Arithmetic constraints.
  58  * The intended use is for a list of rewriting arithmetic atoms.
  59  * An example of such a list would be [(<= x 5);(= y 78); (>= x 9)].
  60  *
  61  * Nodes are required to have a CONST_RATIONAL child as their second node.
  62  * Nodes are sorted in increasing order according to RightHandRationalLT.
  63  *
  64  * The lists are lazily sorted in the sense that the list is not sorted until
  65  * an operation to access the element is attempted.
  66  *
  67  * An append() may make the list no longer sorted.
  68  * After an append() operation all iterators for the list become invalid.
  69  */
  70 class OrderedBoundsList {
  71 private:
  72   bool d_isSorted;
  73   std::vector<Node> d_list;
  74
  75 public:
  76   typedef std::vector<Node>::const_iterator iterator;
  77   typedef std::vector<Node>::const_reverse_iterator reverse_iterator;
  78
  79   /**
  80    * Constucts a new and empty OrderBoundsList.
  81    * The empty list is initially sorted.
  82    */
  83   OrderedBoundsList() : d_isSorted(true){}
  84
  85   /**
  86    * Appends a node onto the back of the list.
  87    * The list may no longer be sorted.
  88    */
  89   void append(TNode n){
  90     Assert(n.getNumChildren() >= 2);
  91     Assert(n[1].getKind() == kind::CONST_RATIONAL);
  92     d_isSorted = false;
  93     d_list.push_back(n);
  94   }
  95
  96   /** returns the size of the list */
  97   unsigned int size(){
  98     return d_list.size();
  99   }
 100
 101   /** returns the i'th element in the sort list. This may sort the list.*/
 102   TNode at(unsigned int idx){
 103     sortIfNeeded();
 104     return d_list.at(idx);
 105   }
 106
 107   /** returns true if the list is known to be sorted. */
 108   bool isSorted() const{
 109     return d_isSorted;
 110   }
 111
 112   /** sorts the list. */
 113   void sort(){
 114     d_isSorted = true;
 115     std::sort(d_list.begin(), d_list.end(), RightHandRationalLT());
 116   }
 117
 118   /**
 119    * returns an iterator to the list that iterates in ascending order.
 120    * This may sort the list.
 121    */
 122   iterator begin(){
 123     sortIfNeeded();
 124     return d_list.begin();
 125   }
 126   /**
 127    * returns an iterator to the end of the list when interating in ascending order.
 128    */
 129   iterator end() const{
 130     return d_list.end();
 131   }
 132
 133   /**
 134    * returns an iterator to the list that iterates in descending order.
 135    * This may sort the list.
 136    */
 137   reverse_iterator rbegin(){
 138     sortIfNeeded();
 139     return d_list.rend();
 140   }
 141   /**
 142    * returns an iterator to the end of the list when interating in descending order.
 143    */
 144   reverse_iterator rend() const{
 145     return d_list.rend();
 146   }
 147
 148   /**
 149    * returns an iterator to the least strict upper bound of value.
 150    * if the list is [(<= x 2);(>= x 80);(< y 70)]
 151    * then *upper_bound((< z 70)) == (>= x 80)
 152    *
 153    * This may sort the list.
 154    * see stl::upper_bound for more information.
 155    */
 156   iterator upper_bound(TNode value){
 157     sortIfNeeded();
 158     return std::upper_bound(begin(), end(), value, RightHandRationalLT());
 159   }
 160   /**
 161    * returns an iterator to the greatest lower bound of value.
 162    * This is bound is not strict.
 163    * if the list is [(<= x 2);(>= x 80);(< y 70)]
 164    * then *lower_bound((< z 70)) == (< y 70)
 165    *
 166    * This may sort the list.
 167    * see stl::upper_bound for more information.
 168    */
 169   iterator lower_bound(TNode value){
 170     sortIfNeeded();
 171     return std::lower_bound(begin(), end(), value, RightHandRationalLT());
 172   }
 173   /**
 174    * see OrderedBoundsList::upper_bound for more information.
 175    * The difference is that the iterator goes in descending order.
 176    */
 177   reverse_iterator reverse_upper_bound(TNode value){
 178     sortIfNeeded();
 179     return std::upper_bound(rbegin(), rend(), value, RightHandRationalGT());
 180   }
 181   /**
 182    * see OrderedBoundsList::lower_bound for more information.
 183    * The difference is that the iterator goes in descending order.
 184    */
 185   reverse_iterator reverse_lower_bound(TNode value){
 186     sortIfNeeded();
 187     return std::lower_bound(rbegin(), rend(), value, RightHandRationalGT());
 188   }
 189
 190   /**
 191    * This is an O(n) method for searching the array to check if it contains n.
 192    */
 193   bool contains(TNode n) const {
 194     for(std::vector<Node>::const_iterator i = d_list.begin(); i != d_list.end(); ++i){
 195       if(*i == n) return true;
 196     }
 197     return false;
 198   }
 199 private:
 200   /** Sorts the list if it is not already sorted.  */
 201   void sortIfNeeded(){
 202     if(!d_isSorted){
 203       sort();
 204     }
 205   }
 206 };
 207
 208 }/* CVC4::theory::arith namespace */
 209 }/* CVC4::theory namespace */
 210 }/* CVC4 namespace */
 211
 212 #endif /* __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H */