1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
/********************* */
/*! \file subrange_bound.cpp
** \verbatim
** Top contributors (to current version):
** Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Representation of subrange bounds
**
** Simple class to represent a subrange bound, either infinite
** (no bound) or finite (an arbitrary precision integer).
**/
#include "util/subrange_bound.h"
#include <limits>
#include "base/cvc4_assert.h"
#include "base/exception.h"
#include "util/integer.h"
namespace CVC4 {
std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) {
out << bounds.lower << ".." << bounds.upper;
return out;
}
/** Get the finite SubrangeBound, failing an assertion if infinite. */
const Integer& SubrangeBound::getBound() const {
PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite");
return d_bound;
}
SubrangeBounds::SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u)
: lower(l), upper(u) {
PrettyCheckArgument(
!l.hasBound() || !u.hasBound() || l.getBound() <= u.getBound(), l,
"Bad subrange bounds specified");
}
bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a,
const SubrangeBounds& b) {
return (a.lower.hasBound() && b.lower.hasBound()) ||
(a.upper.hasBound() && b.upper.hasBound());
}
SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a,
const SubrangeBounds& b) {
DebugCheckArgument(joinIsBounded(a, b), a);
SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower);
SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper);
return SubrangeBounds(newLower, newUpper);
}
} /* namespace CVC4 */
|
