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.cpp | |
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.cpp')
-rw-r--r-- | src/util/cardinality.cpp | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp new file mode 100644 index 000000000..d38be1c92 --- /dev/null +++ b/src/util/cardinality.cpp @@ -0,0 +1,126 @@ +/********************* */ +/*! \file cardinality.cpp + ** \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 + ** + ** Implementation of a simple class to represent a cardinality. + **/ + +#include "util/cardinality.h" + +namespace CVC4 { + +const Integer Cardinality::s_intCard(-1); +const Integer Cardinality::s_realCard(-2); + +const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0)); +const Cardinality Cardinality::REALS(Cardinality::Beth(1)); + +Cardinality& Cardinality::operator+=(const Cardinality& c) throw() { + if(isFinite() && c.isFinite()) { + d_card += c.d_card; + return *this; + } + if(*this >= c) { + return *this; + } else { + return *this = c; + } +} + +/** Assigning multiplication of this cardinality with another. */ +Cardinality& Cardinality::operator*=(const Cardinality& c) throw() { + if(*this == 0 || c == 0) { + return *this = 0; + } else if(!isFinite() || !c.isFinite()) { + if(*this >= c) { + return *this; + } else { + return *this = c; + } + } else { + d_card *= c.d_card; + return *this; + } +} + +/** Assigning exponentiation of this cardinality with another. */ +Cardinality& Cardinality::operator^=(const Cardinality& c) + throw(IllegalArgumentException) { + if(c == 0) { + // (anything) ^ 0 == 1 + d_card = 1; + return *this; + } else if(*this == 0) { + // 0 ^ (>= 1) == 0 + return *this; + } else if(*this == 1) { + // 1 ^ (>= 1) == 1 + return *this; + } else if(c == 1) { + // (anything) ^ 1 == (that thing) + return *this; + } else if(isFinite() && c.isFinite()) { + // finite ^ finite == finite + // + // Note: can throw an assertion if c is too big for + // exponentiation + d_card = d_card.pow(c.d_card.getUnsignedLong()); + return *this; + } else if(!isFinite() && c.isFinite()) { + // inf ^ finite == inf + return *this; + } else { + Assert(*this >= 2 && !c.isFinite(), + "fall-through case not as expected:\n%s\n%s", + this->toString().c_str(), c.toString().c_str()); + // (>= 2) ^ beth_k == beth_(k+1) + // unless the base is already > the exponent + if(*this > c) { + return *this; + } + d_card = c.d_card - 1; + return *this; + } +} + + +std::string Cardinality::toString() const throw() { + std::stringstream ss; + ss << *this; + return ss.str(); +} + + +std::ostream& operator<<(std::ostream& out, + Cardinality::Beth b) + throw() { + out << "beth[" << b.getNumber() << ']'; + + return out; +} + + +std::ostream& operator<<(std::ostream& out, const Cardinality& c) + throw() { + if(c.isFinite()) { + out << c.getFiniteCardinality(); + } else { + out << Cardinality::Beth(c.getBethNumber()); + } + + return out; +} + + +}/* CVC4 namespace */ |