GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/divisible.h Lines: 5 7 71.4 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
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 CVC4 {
30
31
/**
32
 * The structure representing the divisibility-by-k predicate.
33
 */
34
24
struct Divisible
35
{
36
  const Integer k;
37
38
  Divisible(const Integer& n);
39
40
16
  bool operator==(const Divisible& d) const {
41
16
    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
40
  size_t operator()(const Divisible& d) const {
55
40
    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
}/* CVC4 namespace */
65
66
#endif /* CVC4__DIVISIBLE_H */