diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-25 06:56:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-25 06:56:14 +0000 |
commit | cb7363eef352200615e1a0d3729cea8b2c74d265 (patch) | |
tree | d57f6a9cfab879c1027e7282f63d0fae14fc0153 /src/util/cardinality.h | |
parent | e39882bd8a308711135a1ff644293fd9c46e6433 (diff) |
Weekend work. The main points:
* Type::getCardinality() returns the cardinality for for all types.
Theories give a cardinality in the their kinds file. For
cardinalities that depend on a type argument, a "cardinality
computer" function is named in the kinds file, which takes a
TypeNode and returns its cardinality.
* There's a bitmap for the set of "active theories" in the
TheoryEngine. Theories become "active" when a term that is owned by
them, or whose type is owned by them, is pre-registered (run CVC4
with --verbose to see theory activation). Non-active theories don't
get any calls for check() or propagate() or anything, and if we're
running in single-theory mode, the shared term manager doesn't have
to get involved. This is really important for get() performance
(which can only skimp on walking the entire sub-DAG only if the
theory doesn't require it AND the shared term manager doesn't
require it).
* TheoryEngine now does not call presolve(), registerTerm(),
notifyRestart(), etc., on a Theory if that theory doesn't declare
that property in its kinds file. To avoid coding errors,
mktheorytraits greps the theory header and gives warnings if:
+ the theory appears to declare one of the functions (check,
propagate, etc.) that isn't listed among its kinds file properties
(but probably should be)
+ the theory appears NOT to declare one of the functions listed in
its kinds file properties
* some bounded token stream work
Diffstat (limited to 'src/util/cardinality.h')
-rw-r--r-- | src/util/cardinality.h | 234 |
1 files changed, 234 insertions, 0 deletions
diff --git a/src/util/cardinality.h b/src/util/cardinality.h new file mode 100644 index 000000000..c520c2735 --- /dev/null +++ b/src/util/cardinality.h @@ -0,0 +1,234 @@ +/********************* */ +/*! \file cardinality.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 cardinality + ** + ** Simple class to represent a cardinality; used by the CVC4 type system + ** give the cardinality of sorts. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CARDINALITY_H +#define __CVC4__CARDINALITY_H + +#include <iostream> +#include <utility> + +#include "util/integer.h" +#include "util/Assert.h" + +namespace CVC4 { + +/** + * A simple representation of a cardinality. We store an + * arbitrary-precision integer for finite cardinalities, and we + * distinguish infinite cardinalities represented as Beth numbers. + */ +class CVC4_PUBLIC Cardinality { + /** Cardinality of the integers */ + static const Integer s_intCard; + + /** Cardinality of the reals */ + static const Integer s_realCard; + + /** + * In the case of finite cardinality, this is >= 0, and is equal to + * the cardinality. If infinite, it is < 0, and is Beth[|card|-1]. + * That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc. + */ + Integer d_card; + +public: + + /** The cardinality of the set of integers. */ + static const Cardinality INTEGERS; + + /** The cardinality of the set of real numbers. */ + static const Cardinality REALS; + + /** + * Representation for a Beth number, used only to construct + * Cardinality objects. + */ + class Beth { + Integer d_index; + + public: + Beth(const Integer& beth) : d_index(beth) { + CheckArgument(beth >= 0, beth, + "Beth index must be a nonnegative integer, not %s.", + beth.toString().c_str()); + } + + const Integer& getNumber() const throw() { + return d_index; + } + };/* class Cardinality::Beth */ + + /** + * Construct a finite cardinality equal to the integer argument. + * The argument must be nonnegative. If we change this to an + * "unsigned" argument to enforce the restriction, we mask some + * errors that automatically convert, like "Cardinality(-1)". + */ + Cardinality(long card) : d_card(card) { + CheckArgument(card >= 0, card, + "Cardinality must be a nonnegative integer, not %ld.", card); + Assert(isFinite()); + } + + /** + * Construct a finite cardinality equal to the integer argument. + * The argument must be nonnegative. + */ + Cardinality(const Integer& card) : d_card(card) { + CheckArgument(card >= 0, card, + "Cardinality must be a nonnegative integer, not %s.", + card.toString().c_str()); + Assert(isFinite()); + } + + /** + * Construct an infinite cardinality equal to the given Beth number. + */ + Cardinality(Beth beth) : d_card(-beth.getNumber() - 1) { + Assert(!isFinite()); + } + + /** Returns true iff this cardinality is finite. */ + bool isFinite() const throw() { + return d_card >= 0; + } + + /** + * Returns true iff this cardinality is finite or countably + * infinite. + */ + bool isCountable() const throw() { + return d_card >= s_intCard; + } + + /** + * In the case that this cardinality is finite, return its + * cardinality. (If this cardinality is infinite, this function + * throws an IllegalArgumentException.) + */ + const Integer& getFiniteCardinality() const throw(IllegalArgumentException) { + CheckArgument(isFinite(), *this, "This cardinality is not finite."); + return d_card; + } + + /** + * In the case that this cardinality is infinite, return its Beth + * number. (If this cardinality is finite, this function throws an + * IllegalArgumentException.) + */ + Integer getBethNumber() const throw(IllegalArgumentException) { + CheckArgument(!isFinite(), *this, "This cardinality is not infinite."); + return -d_card - 1; + } + + /** Assigning addition of this cardinality with another. */ + Cardinality& operator+=(const Cardinality& c) throw(); + + /** Assigning multiplication of this cardinality with another. */ + Cardinality& operator*=(const Cardinality& c) throw(); + + /** Assigning exponentiation of this cardinality with another. */ + Cardinality& operator^=(const Cardinality& c) throw(IllegalArgumentException); + + /** Add two cardinalities. */ + Cardinality operator+(const Cardinality& c) const throw() { + Cardinality card(*this); + card += c; + return card; + } + + /** Multiply two cardinalities. */ + Cardinality operator*(const Cardinality& c) const throw() { + Cardinality card(*this); + card *= c; + return card; + } + + /** + * Exponentiation of two cardinalities. Throws an exception if both + * are finite and the exponent is too large. + */ + Cardinality operator^(const Cardinality& c) const throw(IllegalArgumentException) { + Cardinality card(*this); + card ^= c; + return card; + } + + /** Test for equality between cardinalities. */ + bool operator==(const Cardinality& c) const throw() { + return d_card == c.d_card; + } + + /** Test for disequality between cardinalities. */ + bool operator!=(const Cardinality& c) const throw() { + return !(*this == c); + } + + /** Test whether this cardinality is less than another. */ + bool operator<(const Cardinality& c) const throw() { + return + ( isFinite() && !c.isFinite() ) || + ( isFinite() && c.isFinite() && d_card < c.d_card ) || + ( !isFinite() && !c.isFinite() && d_card > c.d_card ); + } + + /** + * Test whether this cardinality is less than or equal to + * another. + */ + bool operator<=(const Cardinality& c) const throw() { + return *this < c || *this == c; + } + + /** Test whether this cardinality is greater than another. */ + bool operator>(const Cardinality& c) const throw() { + return !(*this <= c); + } + + /** + * Test whether this cardinality is greater than or equal to + * another. + */ + bool operator>=(const Cardinality& c) const throw() { + return !(*this < c); + } + + /** + * Return a string representation of this cardinality. + */ + std::string toString() const throw(); + +};/* class Cardinality */ + + +/** Print an element of the InfiniteCardinality enumeration. */ +std::ostream& operator<<(std::ostream& out, Cardinality::Beth b) + throw() CVC4_PUBLIC; + + +/** Print a cardinality in a human-readable fashion. */ +std::ostream& operator<<(std::ostream& out, const Cardinality& c) + throw() CVC4_PUBLIC; + + +}/* CVC4 namespace */ + +#endif /* __CVC4__CARDINALITY_H */ |