3 #include "cvc4_private.h"
6 #ifndef __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
7 #define __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
10 #include "util/rational.h"
11 #include "expr/kind.h"
20 struct RightHandRationalLT
22 bool operator()(TNode s1
, TNode s2
) const
24 Assert(s1
.getNumChildren() >= 2);
25 Assert(s2
.getNumChildren() >= 2);
27 Assert(s1
[1].getKind() == kind::CONST_RATIONAL
);
28 Assert(s2
[1].getKind() == kind::CONST_RATIONAL
);
32 const Rational
& c1
= rh1
.getConst
<Rational
>();
33 const Rational
& c2
= rh2
.getConst
<Rational
>();
34 return c1
.cmp(c2
) < 0;
38 struct RightHandRationalGT
40 bool operator()(TNode s1
, TNode s2
) const
42 Assert(s1
.getNumChildren() >= 2);
43 Assert(s2
.getNumChildren() >= 2);
45 Assert(s1
[1].getKind() == kind::CONST_RATIONAL
);
46 Assert(s2
[1].getKind() == kind::CONST_RATIONAL
);
50 const Rational
& c1
= rh1
.getConst
<Rational
>();
51 const Rational
& c2
= rh2
.getConst
<Rational
>();
52 return c1
.cmp(c2
) > 0;
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)].
61 * Nodes are required to have a CONST_RATIONAL child as their second node.
62 * Nodes are sorted in increasing order according to RightHandRationalLT.
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.
67 * An append() may make the list no longer sorted.
68 * After an append() operation all iterators for the list become invalid.
70 class OrderedBoundsList
{
73 std::vector
<Node
> d_list
;
76 typedef std::vector
<Node
>::const_iterator iterator
;
77 typedef std::vector
<Node
>::const_reverse_iterator reverse_iterator
;
80 * Constucts a new and empty OrderBoundsList.
81 * The empty list is initially sorted.
83 OrderedBoundsList() : d_isSorted(true){}
86 * Appends a node onto the back of the list.
87 * The list may no longer be sorted.
90 Assert(n
.getNumChildren() >= 2);
91 Assert(n
[1].getKind() == kind::CONST_RATIONAL
);
96 /** returns the size of the list */
101 /** returns the i'th element in the sort list. This may sort the list.*/
102 TNode
at(unsigned int idx
){
104 return d_list
.at(idx
);
107 /** returns true if the list is known to be sorted. */
108 bool isSorted() const{
112 /** sorts the list. */
115 std::sort(d_list
.begin(), d_list
.end(), RightHandRationalLT());
119 * returns an iterator to the list that iterates in ascending order.
120 * This may sort the list.
124 return d_list
.begin();
127 * returns an iterator to the end of the list when interating in ascending order.
129 iterator
end() const{
134 * returns an iterator to the list that iterates in descending order.
135 * This may sort the list.
137 reverse_iterator
rbegin(){
139 return d_list
.rend();
142 * returns an iterator to the end of the list when interating in descending order.
144 reverse_iterator
rend() const{
145 return d_list
.rend();
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)
153 * This may sort the list.
154 * see stl::upper_bound for more information.
156 iterator
upper_bound(TNode value
){
158 return std::upper_bound(begin(), end(), value
, RightHandRationalLT());
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)
166 * This may sort the list.
167 * see stl::upper_bound for more information.
169 iterator
lower_bound(TNode value
){
171 return std::lower_bound(begin(), end(), value
, RightHandRationalLT());
174 * see OrderedBoundsList::upper_bound for more information.
175 * The difference is that the iterator goes in descending order.
177 reverse_iterator
reverse_upper_bound(TNode value
){
179 return std::upper_bound(rbegin(), rend(), value
, RightHandRationalGT());
182 * see OrderedBoundsList::lower_bound for more information.
183 * The difference is that the iterator goes in descending order.
185 reverse_iterator
reverse_lower_bound(TNode value
){
187 return std::lower_bound(rbegin(), rend(), value
, RightHandRationalGT());
191 * This is an O(n) method for searching the array to check if it contains n.
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;
200 /** Sorts the list if it is not already sorted. */
208 }/* CVC4::theory::arith namespace */
209 }/* CVC4::theory namespace */
210 }/* CVC4 namespace */
212 #endif /* __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H */