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