src/util/divisible.h

   1 /*********************                                                        */
   2 /*! \file divisible.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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
  25 #include "base/exception.h"
  26 #include "util/integer.h"
  27
  28 namespace CVC4 {
  29
  30 /**
  31  * The structure representing the divisibility-by-k predicate.
  32  */
  33 struct CVC4_PUBLIC Divisible {
  34   const Integer k;
  35
  36   Divisible(const Integer& n);
  37
  38   bool operator==(const Divisible& d) const {
  39     return k == d.k;
  40   }
  41
  42   bool operator!=(const Divisible& d) const {
  43     return !(*this == d);
  44   }
  45 };/* struct Divisible */
  46
  47 /**
  48  * Hash function for the Divisible objects.
  49  */
  50 struct CVC4_PUBLIC DivisibleHashFunction {
  51   size_t operator()(const Divisible& d) const {
  52     return d.k.hash();
  53   }
  54 };/* struct DivisibleHashFunction */
  55
  56 inline std::ostream& operator <<(std::ostream& os, const Divisible& d) CVC4_PUBLIC;
  57 inline std::ostream& operator <<(std::ostream& os, const Divisible& d) {
  58   return os << "divisible-by-" << d.k;
  59 }
  60
  61 }/* CVC4 namespace */
  62
  63 #endif /* CVC4__DIVISIBLE_H */