diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-08-17 08:51:51 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-08-17 08:51:51 -0700 |
commit | 33ca2a3f2359493a9154a229a30ad3aa3a21f2aa (patch) | |
tree | 2faebdb98cff292d4b4cd9aed254a685efada15b /src/util | |
parent | 7766f0ba088ad6d6c58ea9678477b255c9e52fee (diff) |
Remove unused SubrangeBound(s) classes (#221)
As discussed in pull request #220, commit
360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s).
There were still a few mentions of it left in the code, most of them commented
out. The occurrences in expr.i and expr_manager.i, however, created issues with
the Python wrapper. This commit removes the SubrangeBound(s) implementation and
other leftovers.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/subrange_bound.cpp | 61 | ||||
-rw-r--r-- | src/util/subrange_bound.h | 234 | ||||
-rw-r--r-- | src/util/subrange_bound.i | 24 |
4 files changed, 0 insertions, 322 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 877525de7..027abce64 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -55,8 +55,6 @@ libutil_la_SOURCES = \ statistics.h \ statistics_registry.cpp \ statistics_registry.h \ - subrange_bound.cpp \ - subrange_bound.h \ tuple.h \ unsafe_interrupt_exception.h \ utility.h @@ -102,7 +100,6 @@ EXTRA_DIST = \ result.i \ sexpr.i \ statistics.i \ - subrange_bound.i \ tuple.i \ unsafe_interrupt_exception.i diff --git a/src/util/subrange_bound.cpp b/src/util/subrange_bound.cpp deleted file mode 100644 index b49a3ef27..000000000 --- a/src/util/subrange_bound.cpp +++ /dev/null @@ -1,61 +0,0 @@ -/********************* */ -/*! \file subrange_bound.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 "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 */ 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 */ diff --git a/src/util/subrange_bound.i b/src/util/subrange_bound.i deleted file mode 100644 index c12bd11e4..000000000 --- a/src/util/subrange_bound.i +++ /dev/null @@ -1,24 +0,0 @@ -%{ -#include "util/subrange_bound.h" -%} - -%rename(equals) CVC4::SubrangeBound::operator==(const SubrangeBound&) const; -%ignore CVC4::SubrangeBound::operator!=(const SubrangeBound&) const; -%rename(less) CVC4::SubrangeBound::operator<(const SubrangeBound&) const; -%rename(lessEqual) CVC4::SubrangeBound::operator<=(const SubrangeBound&) const; -%rename(greater) CVC4::SubrangeBound::operator>(const SubrangeBound&) const; -%rename(greaterEqual) CVC4::SubrangeBound::operator>=(const SubrangeBound&) const; - -%rename(equals) CVC4::SubrangeBounds::operator==(const SubrangeBounds&) const; -%ignore CVC4::SubrangeBounds::operator!=(const SubrangeBounds&) const; -%rename(less) CVC4::SubrangeBounds::operator<(const SubrangeBounds&) const; -%rename(lessEqual) CVC4::SubrangeBounds::operator<=(const SubrangeBounds&) const; -%rename(greater) CVC4::SubrangeBounds::operator>(const SubrangeBounds&) const; -%rename(greaterEqual) CVC4::SubrangeBounds::operator>=(const SubrangeBounds&) const; - -%rename(apply) CVC4::SubrangeBoundsHashFunction::operator()(const SubrangeBounds&) const; - -%ignore CVC4::operator<<(std::ostream&, const SubrangeBound&); -%ignore CVC4::operator<<(std::ostream&, const SubrangeBounds&); - -%include "util/subrange_bound.h" |