diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.h | 10 | ||||
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/cardinality.cpp | 126 | ||||
-rw-r--r-- | src/util/cardinality.h | 234 | ||||
-rw-r--r-- | src/util/datatype.h | 3 | ||||
-rw-r--r-- | src/util/debug.h | 2 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 33 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 45 | ||||
-rw-r--r-- | src/util/language.cpp | 65 | ||||
-rw-r--r-- | src/util/language.h | 41 | ||||
-rw-r--r-- | src/util/subrange_bound.h | 5 |
11 files changed, 524 insertions, 43 deletions
diff --git a/src/util/Assert.h b/src/util/Assert.h index 0ff89bedf..e38a3f9cf 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -221,6 +221,16 @@ public: va_end(args); } + InternalErrorException(const char* function, const char* file, unsigned line, + std::string fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Internal error detected", "", + function, file, line, fmt.c_str(), args); + va_end(args); + } + };/* class InternalErrorException */ #ifdef CVC4_DEBUG diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e76858d80..a6ff0ea40 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -45,8 +45,11 @@ libutil_la_SOURCES = \ stats.cpp \ dynamic_array.h \ language.h \ + language.cpp \ triple.h \ subrange_bound.h \ + cardinality.h \ + cardinality.cpp \ trans_closure.h \ trans_closure.cpp \ boolean_simplification.h \ 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 */ 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 */ diff --git a/src/util/datatype.h b/src/util/datatype.h index 26e58264a..74bff1843 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -150,6 +150,7 @@ public: /** Get the name of this constructor argument. */ std::string getName() const throw(); + /** * Get the selector for this constructor argument; this call is * only permitted after resolution. @@ -203,12 +204,14 @@ public: * to this Datatype constructor. */ void addArg(std::string selectorName, Type selectorType); + /** * Add an argument (i.e., a data field) of the given name to this * Datatype constructor that refers to an as-yet-unresolved * Datatype (which may be mutually-recursive). */ void addArg(std::string selectorName, Datatype::UnresolvedType selectorType); + /** * Add a self-referential (i.e., a data field) of the given name * to this Datatype constructor that refers to the enclosing diff --git a/src/util/debug.h b/src/util/debug.h index 4fc5d5caa..402c5bed4 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -20,6 +20,8 @@ ** util/Assert.h. **/ +#include "cvc4_private.h" + #ifndef __CVC4__DEBUG_H #define __CVC4__DEBUG_H diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index d13c946de..8c3fc14e5 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -142,25 +142,45 @@ public: } - Integer operator+(const Integer& y) const{ + Integer operator+(const Integer& y) const { return Integer( d_value + y.d_value ); } + Integer& operator+=(const Integer& y) { + d_value += y.d_value; + return *this; + } Integer operator-(const Integer& y) const { return Integer( d_value - y.d_value ); } + Integer& operator-=(const Integer& y) { + d_value -= y.d_value; + return *this; + } Integer operator*(const Integer& y) const { return Integer( d_value * y.d_value ); } + Integer& operator*=(const Integer& y) { + d_value *= y.d_value; + return *this; + } Integer operator/(const Integer& y) const { return Integer( cln::floor1(d_value, y.d_value) ); } + Integer& operator/=(const Integer& y) { + d_value = cln::floor1(d_value, y.d_value); + return *this; + } Integer operator%(const Integer& y) const { return Integer( cln::floor2(d_value, y.d_value).remainder ); } + Integer& operator%=(const Integer& y) { + d_value = cln::floor2(d_value, y.d_value).remainder; + return *this; + } /** Raise this Integer to the power <code>exp</code>. * @@ -208,8 +228,15 @@ public: //friend std::ostream& operator<<(std::ostream& os, const Integer& n); - long getLong() const { return cln::cl_I_to_long(d_value); } - unsigned long getUnsignedLong() const {return cln::cl_I_to_ulong(d_value); } + long getLong() const { + // supposed to throw if not representable in type "long" + return cln::cl_I_to_long(d_value); + } + + unsigned long getUnsignedLong() const { + // supposed to throw if not representable in type "unsigned long" + return cln::cl_I_to_ulong(d_value); + } /** * Computes the hash of the node from the first word of the diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 13bed50b3..c1d46ca65 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -25,6 +25,7 @@ #include <string> #include <iostream> +#include "util/Assert.h" #include "util/gmp_util.h" namespace CVC4 { @@ -84,7 +85,7 @@ public: return d_value == y.d_value; } - Integer operator-() const{ + Integer operator-() const { return Integer(-(d_value)); } @@ -110,23 +111,45 @@ public: } - Integer operator+(const Integer& y) const{ + Integer operator+(const Integer& y) const { return Integer( d_value + y.d_value ); } + Integer& operator+=(const Integer& y) { + d_value += y.d_value; + return *this; + } Integer operator-(const Integer& y) const { return Integer( d_value - y.d_value ); } + Integer& operator-=(const Integer& y) { + d_value -= y.d_value; + return *this; + } Integer operator*(const Integer& y) const { return Integer( d_value * y.d_value ); } + Integer& operator*=(const Integer& y) { + d_value *= y.d_value; + return *this; + } + Integer operator/(const Integer& y) const { return Integer( d_value / y.d_value ); } + Integer& operator/=(const Integer& y) { + d_value /= y.d_value; + return *this; + } + Integer operator%(const Integer& y) const { return Integer( d_value % y.d_value ); } + Integer& operator%=(const Integer& y) { + d_value %= y.d_value; + return *this; + } /** Raise this Integer to the power <code>exp</code>. * @@ -144,8 +167,22 @@ public: //friend std::ostream& operator<<(std::ostream& os, const Integer& n); - long getLong() const { return d_value.get_si(); } - unsigned long getUnsignedLong() const {return d_value.get_ui(); } + long getLong() const { + long si = d_value.get_si(); +#ifdef CVC4_ASSERTIONS + // ensure there wasn't overflow + Assert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0); +#endif /* CVC4_ASSERTIONS */ + return si; + } + unsigned long getUnsignedLong() const { + unsigned long ui = d_value.get_ui(); +#ifdef CVC4_ASSERTIONS + // ensure there wasn't overflow + Assert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0); +#endif /* CVC4_ASSERTIONS */ + return ui; + } /** * Computes the hash of the node from the first word of the diff --git a/src/util/language.cpp b/src/util/language.cpp new file mode 100644 index 000000000..da54a4783 --- /dev/null +++ b/src/util/language.cpp @@ -0,0 +1,65 @@ +/********************* */ +/*! \file language.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 Definition of input and output languages + ** + ** Definition of input and output languages. + **/ + +#include "util/language.h" + +namespace CVC4 { +namespace language { + +InputLanguage toInputLanguage(OutputLanguage language) { + switch(language) { + case output::LANG_SMTLIB: + case output::LANG_SMTLIB_V2: + case output::LANG_CVC4: + // these entries directly correspond (by design) + return InputLanguage(int(language)); + + default: { + std::stringstream ss; + ss << "Cannot map output language `" << language + << "' to an input language."; + throw CVC4::Exception(ss.str()); + } + }/* switch(language) */ +}/* toInputLanguage() */ + +OutputLanguage toOutputLanguage(InputLanguage language) { + switch(language) { + case input::LANG_SMTLIB: + case input::LANG_SMTLIB_V2: + case input::LANG_CVC4: + // these entries directly correspond (by design) + return OutputLanguage(int(language)); + + default: + // Revert to the default (AST) language. + // + // We used to throw an exception here, but that's not quite right. + // We often call this while constructing exceptions, for one, and + // it's better to output SOMETHING related to the original + // exception rather than mask it with another exception. Also, + // the input language isn't always defined---e.g. during the + // initial phase of the main CVC4 driver while it determines which + // language is appropriate, and during unit tests. Also, when + // users are writing their own code against the library. + return output::LANG_AST; + }/* switch(language) */ +}/* toOutputLanguage() */ + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ diff --git a/src/util/language.h b/src/util/language.h index 814f8dcd1..dbda6a315 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -31,7 +31,7 @@ namespace language { namespace input { -enum Language { +enum CVC4_PUBLIC Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 /** Auto-detect the language */ @@ -58,6 +58,7 @@ enum Language { LANG_MAX };/* enum Language */ +inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, Language lang) { switch(lang) { case LANG_AUTO: @@ -82,7 +83,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { namespace output { -enum Language { +enum CVC4_PUBLIC Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] @@ -109,6 +110,7 @@ enum Language { LANG_MAX };/* enum Language */ +inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, Language lang) { switch(lang) { case LANG_SMTLIB: @@ -138,39 +140,8 @@ typedef language::output::Language OutputLanguage; namespace language { -inline InputLanguage toInputLanguage(OutputLanguage language) { - switch(language) { - case output::LANG_SMTLIB: - case output::LANG_SMTLIB_V2: - case output::LANG_CVC4: - // these entries directly correspond (by design) - return InputLanguage(int(language)); - - default: { - std::stringstream ss; - ss << "Cannot map output language `" << language - << "' to an input language."; - throw CVC4::Exception(ss.str()); - } - }/* switch(language) */ -}/* toInputLanguage() */ - -inline OutputLanguage toOutputLanguage(InputLanguage language) { - switch(language) { - case input::LANG_SMTLIB: - case input::LANG_SMTLIB_V2: - case input::LANG_CVC4: - // these entries directly correspond (by design) - return OutputLanguage(int(language)); - - default: { - std::stringstream ss; - ss << "Cannot map input language `" << language - << "' to an output language."; - throw CVC4::Exception(ss.str()); - } - }/* switch(language) */ -}/* toOutputLanguage() */ +InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC; +OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC; }/* CVC4::language namespace */ }/* CVC4 namespace */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index fc6a259b4..0c84b214e 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -33,7 +33,7 @@ namespace CVC4 { * an infinite bound). For example, the CVC language subrange [-5.._] * has a lower bound of -5 and an infinite upper bound. */ -class SubrangeBound { +class CVC4_PUBLIC SubrangeBound { bool d_nobound; Integer d_bound; @@ -79,6 +79,9 @@ public: };/* class SubrangeBound */ inline std::ostream& +operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) throw() { if(bound.hasBound()) { out << bound.getBound(); |