summaryrefslogtreecommitdiff
path: root/src/util/subrange_bound.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/subrange_bound.h')
-rw-r--r--src/util/subrange_bound.h234
1 files changed, 0 insertions, 234 deletions
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
deleted file mode 100644
index 1f1cb84d7..000000000
--- a/src/util/subrange_bound.h
+++ /dev/null
@@ -1,234 +0,0 @@
-/********************* */
-/*! \file subrange_bound.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 "cvc4_public.h"
-
-#ifndef __CVC4__SUBRANGE_BOUND_H
-#define __CVC4__SUBRANGE_BOUND_H
-
-#include <limits>
-
-#include "base/exception.h"
-#include "util/integer.h"
-
-namespace CVC4 {
-
-/**
- * Representation of a subrange bound. A bound can either exist and be
- * a finite arbitrary-precision integer, or not exist (and thus be
- * an infinite bound). For example, the CVC language subrange [-5.._]
- * has a lower bound of -5 and an infinite upper bound.
- */
-class CVC4_PUBLIC SubrangeBound {
- public:
- /** Construct an infinite SubrangeBound. */
- SubrangeBound() : d_nobound(true), d_bound() {}
-
- /** Construct a finite SubrangeBound. */
- SubrangeBound(const Integer& i) : d_nobound(false), d_bound(i) {}
-
- ~SubrangeBound() {}
-
- /**
- * Get the finite SubrangeBound, failing an assertion if infinite.
- *
- * @throws IllegalArgumentException if the bound is infinite.
- */
- const Integer& getBound() const;
-
- /** Returns true iff this is a finite SubrangeBound. */
- bool hasBound() const { return !d_nobound; }
-
- /** Test two SubrangeBounds for equality. */
- bool operator==(const SubrangeBound& b) const {
- return hasBound() == b.hasBound() &&
- (!hasBound() || getBound() == b.getBound());
- }
-
- /** Test two SubrangeBounds for disequality. */
- bool operator!=(const SubrangeBound& b) const { return !(*this == b); }
-
- /**
- * Is this SubrangeBound "less than" another? For two
- * SubrangeBounds that "have bounds," this is defined as expected.
- * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
- * bound, b1 < b2 (but note also that b1 > b2). This strange
- * behavior is due to the fact that a SubrangeBound without a bound
- * is the representation for both +infinity and -infinity.
- */
- bool operator<(const SubrangeBound& b) const {
- return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
- (hasBound() && b.hasBound() && getBound() < b.getBound());
- }
-
- /**
- * Is this SubrangeBound "less than or equal to" another? For two
- * SubrangeBounds that "have bounds," this is defined as expected.
- * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
- * bound, b1 < b2 (but note also that b1 > b2). This strange
- * behavior is due to the fact that a SubrangeBound without a bound
- * is the representation for both +infinity and -infinity.
- */
- bool operator<=(const SubrangeBound& b) const {
- return !hasBound() || !b.hasBound() ||
- (hasBound() && b.hasBound() && getBound() <= b.getBound());
- }
-
- /**
- * Is this SubrangeBound "greater than" another? For two
- * SubrangeBounds that "have bounds," this is defined as expected.
- * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
- * bound, b1 > b2 (but note also that b1 < b2). This strange
- * behavior is due to the fact that a SubrangeBound without a bound
- * is the representation for both +infinity and -infinity.
- */
- bool operator>(const SubrangeBound& b) const {
- return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
- (hasBound() && b.hasBound() && getBound() < b.getBound());
- }
-
- /**
- * Is this SubrangeBound "greater than or equal to" another? For
- * two SubrangeBounds that "have bounds," this is defined as
- * expected. For a finite SubrangeBound b1 and a SubrangeBounds b2
- * without a bound, b1 > b2 (but note also that b1 < b2). This
- * strange behavior is due to the fact that a SubrangeBound without
- * a bound is the representation for both +infinity and -infinity.
- */
- bool operator>=(const SubrangeBound& b) const {
- return !hasBound() || !b.hasBound() ||
- (hasBound() && b.hasBound() && getBound() <= b.getBound());
- }
-
- static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b) {
- if (a.hasBound() && b.hasBound()) {
- return SubrangeBound(Integer::min(a.getBound(), b.getBound()));
- } else {
- return SubrangeBound();
- }
- }
-
- static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b) {
- if (a.hasBound() && b.hasBound()) {
- return SubrangeBound(Integer::max(a.getBound(), b.getBound()));
- } else {
- return SubrangeBound();
- }
- }
-
- private:
- bool d_nobound;
- Integer d_bound;
-}; /* class SubrangeBound */
-
-class CVC4_PUBLIC SubrangeBounds {
- public:
- SubrangeBound lower;
- SubrangeBound upper;
-
- SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u);
-
- bool operator==(const SubrangeBounds& bounds) const {
- return lower == bounds.lower && upper == bounds.upper;
- }
-
- bool operator!=(const SubrangeBounds& bounds) const {
- return !(*this == bounds);
- }
-
- /**
- * Is this pair of SubrangeBounds "less than" (contained inside) the
- * given pair of SubrangeBounds? Think of this as a subtype
- * relation, e.g., [0,2] < [0,3]
- */
- bool operator<(const SubrangeBounds& bounds) const {
- return (lower > bounds.lower && upper <= bounds.upper) ||
- (lower >= bounds.lower && upper < bounds.upper);
- }
-
- /**
- * Is this pair of SubrangeBounds "less than or equal" (contained
- * inside) the given pair of SubrangeBounds? Think of this as a
- * subtype relation, e.g., [0,2] < [0,3]
- */
- bool operator<=(const SubrangeBounds& bounds) const {
- return lower >= bounds.lower && upper <= bounds.upper;
- }
-
- /**
- * Is this pair of SubrangeBounds "greater than" (does it contain)
- * the given pair of SubrangeBounds? Think of this as a supertype
- * relation, e.g., [0,3] > [0,2]
- */
- bool operator>(const SubrangeBounds& bounds) const {
- return (lower < bounds.lower && upper >= bounds.upper) ||
- (lower <= bounds.lower && upper > bounds.upper);
- }
-
- /**
- * Is this pair of SubrangeBounds "greater than" (does it contain)
- * the given pair of SubrangeBounds? Think of this as a supertype
- * relation, e.g., [0,3] > [0,2]
- */
- bool operator>=(const SubrangeBounds& bounds) const {
- return lower <= bounds.lower && upper >= bounds.upper;
- }
-
- /**
- * Returns true if the join of two subranges is not (- infinity, + infinity).
- */
- static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b);
-
- /**
- * Returns the join of two subranges, a and b.
- * precondition: joinIsBounded(a,b) is true
- */
- static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b);
-
-}; /* class SubrangeBounds */
-
-struct CVC4_PUBLIC SubrangeBoundsHashFunction {
- inline size_t operator()(const SubrangeBounds& bounds) const {
- // We use Integer::hash() rather than Integer::getUnsignedLong()
- // because the latter might overflow and throw an exception
- size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash()
- : std::numeric_limits<size_t>::max();
- size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash()
- : std::numeric_limits<size_t>::max();
- return l + 0x9e3779b9 + (u << 6) + (u >> 2);
- }
-}; /* struct SubrangeBoundsHashFunction */
-
-inline std::ostream& operator<<(std::ostream& out,
- const SubrangeBound& bound) CVC4_PUBLIC;
-
-inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) {
- if (bound.hasBound()) {
- out << bound.getBound();
- } else {
- out << '_';
- }
-
- return out;
-}
-
-std::ostream& operator<<(std::ostream& out,
- const SubrangeBounds& bounds) CVC4_PUBLIC;
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4__SUBRANGE_BOUND_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback