Add files missing from last commit

3 files changed, 101 insertions, 0 deletions

diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp
new file mode 100644
index 000000000..4e20d6b5f
--- /dev/null
+++ b/src/util/divisible.cpp
@@ -0,0 +1,29 @@
+/*********************                                                        */
+/*! \file divisible.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "util/divisible.h"
+#include "util/exception.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+Divisible::Divisible(const Integer& n) : k(n) {
+  CheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N");
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/divisible.h b/src/util/divisible.h
new file mode 100644
index 000000000..0c0c7bc5b
--- /dev/null
+++ b/src/util/divisible.h
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file divisible.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__DIVISIBLE_H
+#define __CVC4__DIVISIBLE_H
+
+#include <iostream>
+#include "util/integer.h"
+#include "util/exception.h"
+
+namespace CVC4 {
+
+/**
+ * The structure representing the divisibility-by-k predicate.
+ */
+struct CVC4_PUBLIC Divisible {
+  const Integer k;
+
+  Divisible(const Integer& n);
+
+  bool operator==(const Divisible& d) const {
+    return k == d.k;
+  }
+
+  bool operator!=(const Divisible& d) const {
+    return !(*this == d);
+  }
+};/* struct Divisible */
+
+/**
+ * Hash function for the Divisible objects.
+ */
+struct CVC4_PUBLIC DivisibleHashFunction {
+  size_t operator()(const Divisible& d) const {
+    return d.k.hash();
+  }
+};/* struct DivisibleHashFunction */
+
+inline std::ostream& operator <<(std::ostream& os, const Divisible& d) CVC4_PUBLIC;
+inline std::ostream& operator <<(std::ostream& os, const Divisible& d) {
+  return os << "divisible-by-" << d.k;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DIVISIBLE_H */
diff --git a/src/util/divisible.i b/src/util/divisible.i
new file mode 100644
index 000000000..7599360ca
--- /dev/null
+++ b/src/util/divisible.i
@@ -0,0 +1,10 @@
+%{
+#include "util/divisible.h"
+%}
+
+%rename(equals) CVC4::Divisible::operator==(const Divisible&) const;
+%ignore CVC4::Divisible::operator!=(const Divisible&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Divisible&);
+
+%include "util/divisible.h"