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/integer_cln_imp.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/integer_cln_imp.h')
-rw-r--r-- | src/util/integer_cln_imp.h | 33 |
1 files changed, 30 insertions, 3 deletions
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 |