cvc4-1.4
divisible.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__DIVISIBLE_H
21 #define __CVC4__DIVISIBLE_H
22 
23 #include <iostream>
24 #include "util/integer.h"
25 #include "util/exception.h"
26 
27 namespace CVC4 {
28 
33  const Integer k;
34 
35  Divisible(const Integer& n);
36 
37  bool operator==(const Divisible& d) const {
38  return k == d.k;
39  }
40 
41  bool operator!=(const Divisible& d) const {
42  return !(*this == d);
43  }
44 };/* struct Divisible */
45 
50  size_t operator()(const Divisible& d) const {
51  return d.k.hash();
52  }
53 };/* struct DivisibleHashFunction */
54 
55 inline std::ostream& operator <<(std::ostream& os, const Divisible& d) CVC4_PUBLIC;
56 inline std::ostream& operator <<(std::ostream& os, const Divisible& d) {
57  return os << "divisible-by-" << d.k;
58 }
59 
60 }/* CVC4 namespace */
61 
62 #endif /* __CVC4__DIVISIBLE_H */
Definition: expr.h:106
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
Definition: divisible.h:41
size_t operator()(const Divisible &d) const
Definition: divisible.h:50
CVC4&#39;s exception base class and some associated utilities.
Hash function for the Divisible objects.
Definition: divisible.h:49
const Integer k
Definition: divisible.h:33
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
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.
Definition: divisible.h:32
bool operator==(const Divisible &d) const
Definition: divisible.h:37