diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-15 22:57:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-15 22:57:14 +0000 |
commit | 5e5956d492ab18b5b4d4bb51117ac760867a525d (patch) | |
tree | 0c151baa58810722288ad986dfa13123de273739 /src/util/integer_cln_imp.h | |
parent | ec4e1bdba56565d6372cb19ded12c9cadc506870 (diff) |
Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer
implemented. This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0. Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder. (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)
Diffstat (limited to 'src/util/integer_cln_imp.h')
-rw-r--r-- | src/util/integer_cln_imp.h | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 21f6c7581..d13c946de 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -50,7 +50,7 @@ private: */ //const mpz_class& get_mpz() const { return d_value; } const cln::cl_I& get_cl_I() const { return d_value; } - + /** * Constructs an Integer by copying a GMP C++ primitive. */ @@ -219,6 +219,16 @@ public: return equal_hashcode(d_value); } + /** + * Returns true iff bit n is set. + * + * @param n the bit to test (0 == least significant bit) + * @return true if bit n is set in this integer; false otherwise + */ + bool testBit(unsigned n) const { + return cln::logbitp(n, d_value); + } + friend class CVC4::Rational; };/* class Integer */ @@ -235,4 +245,3 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n) { }/* CVC4 namespace */ #endif /* __CVC4__INTEGER_H */ - |