diff options
Diffstat (limited to 'src/util/subrange_bound.h')
-rw-r--r-- | src/util/subrange_bound.h | 94 |
1 files changed, 94 insertions, 0 deletions
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h new file mode 100644 index 000000000..fc6a259b4 --- /dev/null +++ b/src/util/subrange_bound.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file subrange_bound.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "util/integer.h" +#include "util/Assert.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 SubrangeBound { + bool d_nobound; + Integer d_bound; + +public: + + /** Construct an infinite SubrangeBound. */ + SubrangeBound() throw() : + d_nobound(true), + d_bound() { + } + + /** Construct a finite SubrangeBound. */ + SubrangeBound(const Integer& i) throw() : + d_nobound(false), + d_bound(i) { + } + + ~SubrangeBound() throw() { + } + + /** Get the finite SubrangeBound, failing an assertion if infinite. */ + Integer getBound() const throw(IllegalArgumentException) { + CheckArgument(!d_nobound, this, "SubrangeBound is infinite"); + return d_bound; + } + + /** Returns true iff this is a finite SubrangeBound. */ + bool hasBound() const throw() { + return !d_nobound; + } + + /** Test two SubrangeBounds for equality. */ + bool operator==(const SubrangeBound& b) const throw() { + return hasBound() == b.hasBound() && + (!hasBound() || getBound() == b.getBound()); + } + + /** Test two SubrangeBounds for disequality. */ + bool operator!=(const SubrangeBound& b) const throw() { + return !(*this == b); + } + +};/* class SubrangeBound */ + +inline std::ostream& +operator<<(std::ostream& out, const SubrangeBound& bound) throw() { + if(bound.hasBound()) { + out << bound.getBound(); + } else { + out << '_'; + } + + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__SUBRANGE_BOUND_H */ |