diff options
Diffstat (limited to 'src/util/subrange_bound.h')
-rw-r--r-- | src/util/subrange_bound.h | 234 |
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 */ |