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
std::ostream & operator<<(std::ostream &, const Command &)
size_t operator()(const Divisible &d) const
CVC4's exception base class and some associated utilities.
Hash function for the Divisible objects.
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