Partial merge of integers work; this is simple B&B and some pseudoboolean

infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

1 files changed, 17 insertions, 1 deletions

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 8c3fc14e5..664027cdc 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -182,7 +182,8 @@ public:
     return *this;
   }
 
-  /** Raise this Integer to the power <code>exp</code>.
+  /**
+   * Raise this Integer to the power <code>exp</code>.
    *
    * @param exp the exponent
    */
@@ -197,6 +198,21 @@ public:
     }
   }
 
+  /**
+   * Return the greatest common divisor of this integer with another.
+   */
+  Integer gcd(const Integer& y) const {
+    cln::cl_I result = cln::gcd(d_value, y.d_value);
+    return Integer(result);
+  }
+
+  /**
+   * Return the absolute value of this integer.
+   */
+  Integer abs() const {
+    return d_value >= 0 ? *this : -*this;
+  }
+
   std::string toString(int base = 10) const{
     std::stringstream ss;
     switch(base){