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 */
bool operator!=(const Divisible &d) const
Definition: divisible.h:41
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.
Definition: divisible.h:49
const Integer k
Definition: divisible.h:33
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Macros that should be defined everywhere during the building of the libraries and driver binary...
size_t operator()(const Divisible &d) const
Definition: divisible.h:50
std::ostream & operator<<(std::ostream &out, SimplificationMode mode)
The structure representing the divisibility-by-k predicate.
Definition: divisible.h:32
bool operator==(const Divisible &d) const
Definition: divisible.h:37