src/util/divisible.h

   1 /*********************                                                        */
   2 /*! \file divisible.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_public.h"
  19
  20 #ifndef CVC4__DIVISIBLE_H
  21 #define CVC4__DIVISIBLE_H
  22
  23 #include <iosfwd>
  24 #include <ostream>
  25 #include <stddef.h>
  26
  27 #include "util/integer.h"
  28
  29 namespace CVC5 {
  30
  31 /**
  32  * The structure representing the divisibility-by-k predicate.
  33  */
  34 struct Divisible
  35 {
  36   const Integer k;
  37
  38   Divisible(const Integer& n);
  39
  40   bool operator==(const Divisible& d) const {
  41     return k == d.k;
  42   }
  43
  44   bool operator!=(const Divisible& d) const {
  45     return !(*this == d);
  46   }
  47 }; /* struct Divisible */
  48
  49 /**
  50  * Hash function for the Divisible objects.
  51  */
  52 struct DivisibleHashFunction
  53 {
  54   size_t operator()(const Divisible& d) const {
  55     return d.k.hash();
  56   }
  57 }; /* struct DivisibleHashFunction */
  58
  59 inline std::ostream& operator<<(std::ostream& os, const Divisible& d);
  60 inline std::ostream& operator <<(std::ostream& os, const Divisible& d) {
  61   return os << "divisible-by-" << d.k;
  62 }
  63
  64 }  // namespace CVC5
  65
  66 #endif /* CVC4__DIVISIBLE_H */