20 #ifndef __CVC4__DIVISIBLE_H 21 #define __CVC4__DIVISIBLE_H 24 #include "util/integer.h" 57 return os <<
"divisible-by-" << d.
k;
size_t hash() const
Computes the hash of the node from the first word of the numerator, the denominator.
bool operator!=(const Divisible &d) const
size_t operator()(const Divisible &d) const
CVC4's exception base class and some associated utilities.
Hash function for the Divisible objects.
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
Macros that should be defined everywhere during the building of the libraries and driver binary...
The structure representing the divisibility-by-k predicate.
bool operator==(const Divisible &d) const