From 0a7e733a5cee4733ca8ca9fff1f6eab6fc22a549 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 17 Jul 2020 09:06:31 +0200
Subject: [PATCH] Integration of libpoly (#4679)

This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration.
Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities.
---
 .github/workflows/ci.yml                     |   2 +
 CMakeLists.txt                               |  17 ++
 COPYING                                      |   2 +-
 INSTALL.md                                   |   8 +-
 cmake/FindPoly.cmake                         |  24 ++
 configure.sh                                 |  14 +
 contrib/get-poly                             |  31 ++
 src/CMakeLists.txt                           |   7 +
 src/base/configuration.cpp                   |  13 +-
 src/base/configuration.h                     |   2 +
 src/base/configuration_private.h             |   6 +
 src/options/options_handler.cpp              |   1 +
 src/util/CMakeLists.txt                      |   7 +
 src/util/poly_util.cpp                       | 282 +++++++++++++++++++
 src/util/poly_util.h                         | 136 +++++++++
 src/util/real_algebraic_number.h.in          |  25 ++
 src/util/real_algebraic_number_poly_imp.cpp  | 175 ++++++++++++
 src/util/real_algebraic_number_poly_imp.h    | 160 +++++++++++
 test/unit/CMakeLists.txt                     |   4 +
 test/unit/util/CMakeLists.txt                |   3 +
 test/unit/util/real_algebraic_number_black.h |  83 ++++++
 21 files changed, 998 insertions(+), 4 deletions(-)
 create mode 100644 cmake/FindPoly.cmake
 create mode 100755 contrib/get-poly
 create mode 100644 src/util/poly_util.cpp
 create mode 100644 src/util/poly_util.h
 create mode 100644 src/util/real_algebraic_number.h.in
 create mode 100644 src/util/real_algebraic_number_poly_imp.cpp
 create mode 100644 src/util/real_algebraic_number_poly_imp.h
 create mode 100644 test/unit/util/real_algebraic_number_black.h

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index da97a2cd2..7dd080f71 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -99,6 +99,7 @@ jobs:
       if: steps.restore-deps.outputs.cache-hit != 'true'
       run: |
         ./contrib/get-antlr-3.4
+        ./contrib/get-poly
         ./contrib/get-symfpu
         ./contrib/get-cadical
         ./contrib/get-cryptominisat
@@ -136,6 +137,7 @@ jobs:
       run: |
         ${{ matrix.env }} ./configure.sh ${{ matrix.config }} \
           --python3 \
+          --poly \
           --prefix=$(pwd)/build/install \
           --unit-testing
 
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 7d5ffc68f..f4aa6c611 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -73,6 +73,9 @@ endif()
 if(LFSC_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}")
 endif()
+if(POLY_DIR)
+  list(APPEND CMAKE_PREFIX_PATH "${POLY_DIR}")
+endif()
 if(SYMFPU_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${SYMFPU_DIR}")
 endif()
@@ -141,6 +144,7 @@ cvc4_option(USE_READLINE      "Use readline for better interactive support")
 #    > for options where we don't need to detect if set by user (default: OFF)
 option(USE_DRAT2ER            "Include drat2er for making eager BV proofs")
 option(USE_LFSC               "Use LFSC proof checker")
+option(USE_POLY               "Use LibPoly for polynomial arithmetic")
 option(USE_SYMFPU             "Use SymFPU for floating point support")
 option(USE_PYTHON2            "Prefer using Python 2 (for Python bindings)")
 option(USE_PYTHON3            "Prefer using Python 3 (for Python bindings)")
@@ -160,6 +164,7 @@ set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
 set(KISSAT_DIR        "" CACHE STRING "Set Kissat install directory")
 set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
+set(POLY_DIR          "" CACHE STRING "Set LibPoly install directory")
 set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 
 # Prepend binaries with prefix on make install
@@ -501,6 +506,14 @@ if(USE_LFSC)
   add_definitions(-DCVC4_USE_LFSC)
 endif()
 
+if(USE_POLY)
+  find_package(Poly REQUIRED)
+  add_definitions(-DCVC4_USE_POLY)
+  set(CVC4_USE_POLY_IMP 1)
+else()
+  set(CVC4_USE_POLY_IMP 0)
+endif()
+
 if(USE_READLINE)
   set(GPL_LIBS "${GPL_LIBS} readline")
   find_package(Readline REQUIRED)
@@ -687,6 +700,7 @@ print_config("drat2er                   :" USE_DRAT2ER)
 print_config("GLPK                      :" USE_GLPK)
 print_config("Kissat                    :" USE_KISSAT)
 print_config("LFSC                      :" USE_LFSC)
+print_config("LibPoly                   :" USE_POLY)
 
 if(CVC4_USE_CLN_IMP)
   message("MP library                : cln")
@@ -723,6 +737,9 @@ endif()
 if(LFSC_DIR)
   message("LFSC dir                  : ${LFSC_DIR}")
 endif()
+if(POLY_DIR)
+  message("LibPoly dir               : ${POLY_DIR}")
+endif()
 if(SYMFPU_DIR)
   message("SYMFPU dir                : ${SYMFPU_DIR}")
 endif()
diff --git a/COPYING b/COPYING
index d4fc07ed2..e0d15cf03 100644
--- a/COPYING
+++ b/COPYING
@@ -79,6 +79,7 @@ CVC4 optionally links against the following libraries:
   CaDiCaL            (https://github.com/arminbiere/cadical)
   CryptoMiniSat      (https://github.com/msoos/cryptominisat)
   LFSC checker       (https://github.com/CVC4/LFSC)
+  LibPoly            (https://github.com/SRI-CSL/libpoly)
 
 Linking CVC4 against these libraries does not affect the license terms of the
 CVC4 code.  See the respective projects for copyright and licensing
@@ -111,4 +112,3 @@ CVC4 can be optionally configured to link against GNU Readline for improved
 text-editing support in interactive mode.  GNU Readline is available here:
 
   http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html
-
diff --git a/INSTALL.md b/INSTALL.md
index ae22e2d71..2c73827c1 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -129,6 +129,12 @@ dependency.
 with --check-proofs. It can be installed using the `contrib/get-lfsc` script.  
 Configure CVC4 with `configure.sh --lfsc` to build with this dependency.
 
+### LibPoly (Optional polynomial library)
+
+[LibPoly](https://github.com/SRI-CSL/libpoly) is required for CAD-based nonlinear reasoning.
+It can be installed using the `contrib/get-poly` script.
+Configure CVC4 with `configure.sh --poly` to build with this dependency.
+
 ### CLN >= v1.3 (Class Library for Numbers)
 
 [CLN](http://www.ginac.de/CLN)
@@ -317,5 +323,3 @@ are configured to **run** in parallel with the maximum number of threads
 available on the system. Override with `ARGS=-jN`.
 
 Use `-jN` for parallel **building** with `N` threads.
-
-
diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake
new file mode 100644
index 000000000..5f4383732
--- /dev/null
+++ b/cmake/FindPoly.cmake
@@ -0,0 +1,24 @@
+# Find LibPoly
+# POLY_FOUND - system has LibPoly
+# POLY_INCLUDE_DIR - the LibPoly include directory
+# POLY_LIBRARIES - Libraries needed to use LibPoly
+
+# Note: contrib/get-poly copies header files to deps/install/include/poly.
+# However, includes in LibPoly headers are not prefixed with "poly/" and therefore
+# we have to look for headers in include/poly instead of include/.
+find_path(POLY_INCLUDE_DIR NAMES poly/poly.h PATH_SUFFIXES poly)
+find_library(POLY_LIB NAMES poly)
+find_library(POLY_LIBXX NAMES polyxx)
+set(POLY_LIBRARIES "${POLY_LIBXX};${POLY_LIB}")
+unset(POLY_LIB CACHE)
+unset(POLY_LIBXX CACHE)
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(Poly
+  DEFAULT_MSG
+  POLY_INCLUDE_DIR POLY_LIBRARIES)
+
+mark_as_advanced(POLY_INCLUDE_DIR POLY_LIBRARIES)
+if(POLY_LIBRARIES)
+  message(STATUS "Found LibPoly: ${POLY_LIBRARIES}")
+endif()
diff --git a/configure.sh b/configure.sh
index 988b7a392..f720e67c2 100755
--- a/configure.sh
+++ b/configure.sh
@@ -62,6 +62,7 @@ The following flags enable optional packages (disable with --no-<option name>).
   --drat2er                use drat2er (required for eager BV proofs)
   --kissat                 use the Kissat SAT solver
   --lfsc                   use the LFSC proof checker
+  --poly                   use the LibPoly library
   --symfpu                 use SymFPU for floating point solver
   --readline               support the readline library
 
@@ -76,6 +77,7 @@ Optional Path to Optional Packages:
   --gmp-dir=PATH           path to top level of GMP installation
   --kissat-dir=PATH        path to top level of Kissat source tree
   --lfsc-dir=PATH          path to top level of LFSC source tree
+  --poly-dir=PATH          path to top level of LibPoly source tree
   --symfpu-dir=PATH        path to top level of SymFPU source tree
 
 EOF
@@ -124,6 +126,7 @@ glpk=default
 gpl=default
 kissat=default
 lfsc=default
+poly=default
 muzzle=default
 ninja=default
 optimized=default
@@ -155,6 +158,7 @@ glpk_dir=default
 gmp_dir=default
 kissat_dir=default
 lfsc_dir=default
+poly_dir=default
 symfpu_dir=default
 
 #--------------------------------------------------------------------------#
@@ -241,6 +245,9 @@ do
     --lfsc) lfsc=ON;;
     --no-lfsc) lfsc=OFF;;
 
+    --poly) poly=ON;;
+    --no-poly) poly=OFF;;
+
     --muzzle) muzzle=ON;;
     --no-muzzle) muzzle=OFF;;
 
@@ -321,6 +328,9 @@ do
     --lfsc-dir) die "missing argument to $1 (try -h)" ;;
     --lfsc-dir=*) lfsc_dir=${1##*=} ;;
 
+    --poly-dir) die "missing argument to $1 (try -h)" ;;
+    --poly-dir=*) poly_dir=${1##*=} ;;
+
     --symfpu-dir) die "missing argument to $1 (try -h)" ;;
     --symfpu-dir=*) symfpu_dir=${1##*=} ;;
 
@@ -417,6 +427,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
 [ $lfsc != default ] \
   && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc"
+[ $poly != default ] \
+  && cmake_opts="$cmake_opts -DUSE_POLY=$poly"
 [ $symfpu != default ] \
   && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu"
 [ "$abc_dir" != default ] \
@@ -439,6 +451,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DKISSAT=$kissat_dir"
 [ "$lfsc_dir" != default ] \
   && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir"
+[ "$poly_dir" != default ] \
+  && cmake_opts="$cmake_opts -DPOLY_DIR=$poly_dir"
 [ "$symfpu_dir" != default ] \
   && cmake_opts="$cmake_opts -DSYMFPU_DIR=$symfpu_dir"
 [ "$install_prefix" != default ] \
diff --git a/contrib/get-poly b/contrib/get-poly
new file mode 100755
index 000000000..a0bc181ed
--- /dev/null
+++ b/contrib/get-poly
@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+#
+source "$(dirname "$0")/get-script-header.sh"
+
+POLY_DIR="$DEPS_DIR/poly"
+version="v0.1.8"
+
+check_dep_dir "$POLY_DIR"
+setup_dep \
+  "https://github.com/SRI-CSL/libpoly/archive/master.tar.gz" "$POLY_DIR"
+# TODO(Gereon, #4706): Go back to fixed version with the next release
+
+pwd
+cd "$POLY_DIR/build/"
+
+CMAKEFLAGS="\
+  -DCMAKE_BUILD_TYPE=Release \
+  -DLIBPOLY_BUILD_PYTHON_API=OFF \
+  -DLIBPOLY_BUILD_STATIC=ON \
+  -DLIBPOLY_BUILD_STATIC_PIC=ON \
+"
+
+echo "Installing to $INSTALL_DIR"
+
+cmake -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" $CMAKEFLAGS  ../ && make -j${NPROC} install
+
+echo
+echo "Using poly version $version"
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure.sh --poly
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4f87778a3..5c1a18900 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -900,6 +900,10 @@ if(USE_LFSC)
   target_link_libraries(cvc4 ${LFSC_LIBRARIES})
   target_include_directories(cvc4 PRIVATE ${LFSC_INCLUDE_DIR})
 endif()
+if(USE_POLY)
+  target_link_libraries(cvc4 ${POLY_LIBRARIES})
+  target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR})
+endif()
 if(USE_SYMFPU)
   target_include_directories(cvc4
     PUBLIC $<BUILD_INTERFACE:${SymFPU_INCLUDE_DIR}>)
@@ -1021,9 +1025,11 @@ install(FILES
           util/integer_cln_imp.h
           util/integer_gmp_imp.h
           util/maybe.h
+          util/poly_util.h
           util/proof.h
           util/rational_cln_imp.h
           util/rational_gmp_imp.h
+          util/real_algebraic_number_poly_imp.h
           util/regexp.h
           util/resource_manager.h
           util/result.h
@@ -1035,6 +1041,7 @@ install(FILES
           ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h
           ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
           ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
+          ${CMAKE_CURRENT_BINARY_DIR}/util/real_algebraic_number.h
         DESTINATION
           ${INCLUDE_INSTALL_DIR}/cvc4/util)
 
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 5fcc5170b..c50311840 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -179,7 +179,7 @@ std::string Configuration::copyright() {
     }
   }
 
-  if (Configuration::isBuiltWithGmp())
+  if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
   {
     ss << "This version of CVC4 is linked against the following third party\n"
        << "libraries covered by the LGPLv3 license.\n"
@@ -188,6 +188,12 @@ std::string Configuration::copyright() {
       ss << "  GMP - Gnu Multi Precision Arithmetic Library\n"
          << "  See http://gmplib.org for copyright information.\n\n";
     }
+    if (Configuration::isBuiltWithPoly())
+    {
+      ss << "  LibPoly polynomial library\n"
+         << "  See https://github.com/SRI-CSL/libpoly for copyright and\n"
+         << "  licensing information.\n\n";
+    }
   }
 
   if (Configuration::isBuiltWithCln()
@@ -269,6 +275,11 @@ bool Configuration::isBuiltWithLfsc() {
   return IS_LFSC_BUILD;
 }
 
+bool Configuration::isBuiltWithPoly()
+{
+  return IS_POLY_BUILD;
+}
+
 bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; }
 
 unsigned Configuration::getNumDebugTags() {
diff --git a/src/base/configuration.h b/src/base/configuration.h
index de060fa00..40914e531 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -107,6 +107,8 @@ public:
 
   static bool isBuiltWithLfsc();
 
+  static bool isBuiltWithPoly();
+
   static bool isBuiltWithSymFPU();
 
   /* Return the number of debug tags */
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 9c58e7898..906cf831d 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -138,6 +138,12 @@ namespace CVC4 {
 #define IS_LFSC_BUILD false
 #endif /* CVC4_USE_LFSC */
 
+#if CVC4_USE_POLY
+#define IS_POLY_BUILD true
+#else /* CVC4_USE_POLY */
+#define IS_POLY_BUILD false
+#endif /* CVC4_USE_POLY */
+
 #if HAVE_LIBREADLINE
 #  define IS_READLINE_BUILD true
 #else /* HAVE_LIBREADLINE */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index dd5265777..380325a1b 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -442,6 +442,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
   print_config_cond("kissat", Configuration::isBuiltWithKissat());
   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
+  print_config_cond("poly", Configuration::isBuiltWithPoly());
   print_config_cond("readline", Configuration::isBuiltWithReadline());
   print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
   
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 028288dbc..09bbfc518 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,6 +1,7 @@
 configure_file(floatingpoint.h.in floatingpoint.h)
 configure_file(rational.h.in rational.h)
 configure_file(integer.h.in integer.h)
+configure_file(real_algebraic_number.h.in real_algebraic_number.h)
 
 libcvc4_add_sources(
   abstract_value.cpp
@@ -23,6 +24,8 @@ libcvc4_add_sources(
   maybe.h
   ostream_util.cpp
   ostream_util.h
+  poly_util.cpp
+  poly_util.h
   proof.h
   random.cpp
   random.h
@@ -59,3 +62,7 @@ endif()
 if(CVC4_USE_GMP_IMP)
   libcvc4_add_sources(rational_gmp_imp.cpp integer_gmp_imp.cpp)
 endif()
+
+if(CVC4_USE_POLY_IMP)
+  libcvc4_add_sources(real_algebraic_number_poly_imp.cpp real_algebraic_number_poly_imp.h)
+endif()
diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp
new file mode 100644
index 000000000..b4c5d1bf2
--- /dev/null
+++ b/src/util/poly_util.cpp
@@ -0,0 +1,282 @@
+/*********************                                                        */
+/*! \file poly_util.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for working with LibPoly.
+ **
+ ** Utilities for working with LibPoly.
+ **/
+
+#include "poly_util.h"
+
+#ifdef CVC4_POLY_IMP
+
+#include <poly/polyxx.h>
+
+#include <map>
+
+#include "base/check.h"
+#include "maybe.h"
+#include "util/integer.h"
+#include "util/rational.h"
+#include "util/real_algebraic_number.h"
+
+namespace CVC4 {
+namespace poly_utils {
+
+namespace {
+/**
+ * Convert arbitrary data using a string as intermediary.
+ * Assumes the existence of operator<<(std::ostream&, const From&) and To(const
+ * std::string&); should be the last resort for type conversions: it may not
+ * only yield bad performance, but is also dependent on compatible string
+ * representations. Use with care!
+ */
+template <typename To, typename From>
+To cast_by_string(const From& f)
+{
+  std::stringstream s;
+  s << f;
+  return To(s.str());
+}
+}  // namespace
+
+Integer toInteger(const poly::Integer& i)
+{
+  const mpz_class& gi = *poly::detail::cast_to_gmp(&i);
+#ifdef CVC4_GMP_IMP
+  return Integer(gi);
+#endif
+#ifdef CVC4_CLN_IMP
+  if (std::numeric_limits<long>::min() <= gi
+      && gi <= std::numeric_limits<long>::max())
+  {
+    return Integer(gi.get_si());
+  }
+  else
+  {
+    return cast_by_string<Integer, poly::Integer>(i);
+  }
+#endif
+}
+Rational toRational(const poly::Integer& i) { return Rational(toInteger(i)); }
+Rational toRational(const poly::Rational& r)
+{
+#ifdef CVC4_GMP_IMP
+  return Rational(*poly::detail::cast_to_gmp(&r));
+#endif
+#ifdef CVC4_CLN_IMP
+  return Rational(toInteger(numerator(r)), toInteger(denominator(r)));
+#endif
+}
+Rational toRational(const poly::DyadicRational& dr)
+{
+  return Rational(toInteger(numerator(dr)), toInteger(denominator(dr)));
+}
+
+poly::Integer toInteger(const Integer& i)
+{
+#ifdef CVC4_GMP_IMP
+  return poly::Integer(i.getValue());
+#endif
+#ifdef CVC4_CLN_IMP
+  if (std::numeric_limits<long>::min() <= i.getValue()
+      && i.getValue() <= std::numeric_limits<long>::max())
+  {
+    return poly::Integer(cln::cl_I_to_long(i.getValue()));
+  }
+  else
+  {
+    return poly::Integer(cast_by_string<mpz_class, Integer>(i));
+  }
+#endif
+}
+std::vector<poly::Integer> toInteger(const std::vector<Integer>& vi)
+{
+  std::vector<poly::Integer> res;
+  for (const auto& i : vi) res.emplace_back(toInteger(i));
+  return res;
+}
+poly::Rational toRational(const Rational& r)
+{
+#ifdef CVC4_GMP_IMP
+  return poly::Rational(r.getValue());
+#endif
+#ifdef CVC4_CLN_IMP
+  return poly::Rational(toInteger(r.getNumerator()),
+                        toInteger(r.getDenominator()));
+#endif
+}
+
+Maybe<poly::DyadicRational> toDyadicRational(const Rational& r)
+{
+  Integer den = r.getDenominator();
+  if (den.isOne())
+  {  // It's an integer anyway.
+    return poly::DyadicRational(toInteger(r.getNumerator()));
+  }
+  unsigned long exp = den.isPow2();
+  if (exp > 0)
+  {
+    // It's a dyadic rational.
+    return div_2exp(poly::DyadicRational(toInteger(r.getNumerator())), exp - 1);
+  }
+  return Maybe<poly::DyadicRational>();
+}
+
+Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
+{
+  poly::Integer den = denominator(r);
+  if (den == poly::Integer(1))
+  {  // It's an integer anyway.
+    return poly::DyadicRational(numerator(r));
+  }
+  // Use bit_size as an estimate for the dyadic exponent.
+  unsigned long size = bit_size(den) - 1;
+  if (mul_pow2(poly::Integer(1), size) == den)
+  {
+    // It's a dyadic rational.
+    return div_2exp(poly::DyadicRational(numerator(r)), size);
+  }
+  return Maybe<poly::DyadicRational>();
+}
+
+poly::Rational approximateToDyadic(const poly::Rational& r,
+                                   const poly::Rational& original)
+{
+  // Multiply both numerator and denominator by two.
+  // Increase or decrease the numerator, depending on whether r is too small or
+  // too large.
+  poly::Integer n = mul_pow2(numerator(r), 1);
+  if (r < original)
+  {
+    ++n;
+  }
+  else if (r > original)
+  {
+    --n;
+  }
+  return poly::Rational(n, mul_pow2(denominator(r), 1));
+}
+
+poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p,
+                                              const Rational& lower,
+                                              const Rational& upper)
+{
+  Maybe<poly::DyadicRational> ml = toDyadicRational(lower);
+  Maybe<poly::DyadicRational> mu = toDyadicRational(upper);
+  if (ml && mu)
+  {
+    return poly::AlgebraicNumber(std::move(p),
+                                 poly::DyadicInterval(ml.value(), mu.value()));
+  }
+  // The encoded real algebraic number did not have dyadic rational endpoints.
+  poly::Rational origl = toRational(lower);
+  poly::Rational origu = toRational(upper);
+  poly::Rational l(floor(origl));
+  poly::Rational u(ceil(origu));
+  poly::RationalInterval ri(l, u);
+  while (count_real_roots(p, ri) != 1)
+  {
+    l = approximateToDyadic(l, origl);
+    u = approximateToDyadic(u, origu);
+    ri = poly::RationalInterval(l, u);
+  }
+  Assert(count_real_roots(p, poly::RationalInterval(l, u)) == 1);
+  ml = toDyadicRational(l);
+  mu = toDyadicRational(u);
+  Assert(ml && mu) << "Both bounds should be dyadic by now.";
+  return poly::AlgebraicNumber(std::move(p),
+                               poly::DyadicInterval(ml.value(), mu.value()));
+}
+
+RealAlgebraicNumber toRanWithRefinement(poly::UPolynomial&& p,
+                                        const Rational& lower,
+                                        const Rational& upper)
+{
+  return RealAlgebraicNumber(
+      toPolyRanWithRefinement(std::move(p), lower, upper));
+}
+
+std::size_t totalDegree(const poly::Polynomial& p)
+{
+  std::size_t tdeg = 0;
+
+  lp_polynomial_traverse_f f =
+      [](const lp_polynomial_context_t* ctx, lp_monomial_t* m, void* data) {
+        std::size_t sum = 0;
+        for (std::size_t i = 0; i < m->n; ++i)
+        {
+          sum += m->p[i].d;
+        }
+
+        std::size_t* td = static_cast<std::size_t*>(data);
+        *td = std::max(*td, sum);
+      };
+
+  lp_polynomial_traverse(p.get_internal(), f, &tdeg);
+
+  return tdeg;
+}
+
+struct GetVarInfo
+{
+  VariableInformation* info;
+  std::size_t cur_var_degree = 0;
+  std::size_t cur_lc_degree = 0;
+};
+void getVariableInformation(VariableInformation& vi,
+                            const poly::Polynomial& poly)
+{
+  GetVarInfo varinfo;
+  varinfo.info = &vi;
+  lp_polynomial_traverse_f f =
+      [](const lp_polynomial_context_t* ctx, lp_monomial_t* m, void* data) {
+        GetVarInfo* gvi = static_cast<GetVarInfo*>(data);
+        VariableInformation* info = gvi->info;
+        // Total degree of this term
+        std::size_t tdeg = 0;
+        // Degree of this variable within this term
+        std::size_t vardeg = 0;
+        for (std::size_t i = 0; i < m->n; ++i)
+        {
+          tdeg += m->p[i].d;
+          if (m->p[i].x == info->var)
+          {
+            info->max_degree = std::max(info->max_degree, m->p[i].d);
+            info->sum_degree += m->p[i].d;
+            ++info->num_terms;
+            vardeg = m->p[i].d;
+          }
+        }
+        if (vardeg > 0)
+        {
+          if (gvi->cur_var_degree < vardeg)
+          {
+            gvi->cur_lc_degree = tdeg - vardeg;
+          }
+          info->max_terms_tdegree = std::max(info->max_terms_tdegree, tdeg);
+        }
+      };
+
+  lp_polynomial_traverse(poly.get_internal(), f, &varinfo);
+  vi.max_lc_degree = std::max(vi.max_lc_degree, varinfo.cur_lc_degree);
+}
+
+}  // namespace poly_utils
+}  // namespace CVC4
+
+#endif
diff --git a/src/util/poly_util.h b/src/util/poly_util.h
new file mode 100644
index 000000000..e54652002
--- /dev/null
+++ b/src/util/poly_util.h
@@ -0,0 +1,136 @@
+/*********************                                                        */
+/*! \file poly_util.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for working with LibPoly.
+ **
+ ** Utilities for working with LibPoly.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__POLY_UTIL_H
+#define CVC4__POLY_UTIL_H
+
+
+#include <vector>
+
+#include "maybe.h"
+#include "util/integer.h"
+#include "util/rational.h"
+#include "util/real_algebraic_number.h"
+
+#ifdef CVC4_POLY_IMP
+
+#include <poly/polyxx.h>
+
+namespace CVC4 {
+/**
+ * Utilities for working with libpoly.
+ * This namespace contains various basic conversion routines necessary for the
+ * integration of LibPoly. Firstly, LibPoly is based on GMP and hence we need
+ * conversion from and to CLN (in case CLN is enabled). Otherwise, conversion of
+ * number types mostly reduces to simple type casts.
+ * Furthermore, conversions between poly::Rational and poly::DyadicRational and
+ * constructors for algebraic numbers that need initial refinement of the
+ * interval are provided.
+ */
+namespace poly_utils {
+
+/** Converts a poly::Integer to a CVC4::Integer. */
+Integer toInteger(const poly::Integer& i);
+/** Converts a poly::Integer to a CVC4::Rational. */
+Rational toRational(const poly::Integer& r);
+/** Converts a poly::Rational to a CVC4::Rational. */
+Rational toRational(const poly::Rational& r);
+/** Converts a poly::DyadicRational to a CVC4::Rational. */
+Rational toRational(const poly::DyadicRational& dr);
+
+/** Converts a CVC4::Integer to a poly::Integer. */
+poly::Integer toInteger(const Integer& i);
+/** Converts a vector of CVC4::Integers to a vector of poly::Integers. */
+std::vector<poly::Integer> toInteger(const std::vector<Integer>& vi);
+/** Converts a CVC4::Rational to a poly::Rational. */
+poly::Rational toRational(const Rational& r);
+/**
+ * Converts a CVC4::Rational to a poly::DyadicRational. If the input is not
+ * dyadic, no result is produced.
+ */
+Maybe<poly::DyadicRational> toDyadicRational(const Rational& r);
+/**
+ * Converts a poly::Rational to a poly::DyadicRational. If the input is not
+ * dyadic, no result is produced.
+ */
+Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r);
+
+/**
+ * Iteratively approximates a poly::Rational by a dyadic poly::Rational.
+ * Assuming that r is dyadic, makes one refinement step to move r closer to
+ * original.
+ * Assumes one starts with lower(original) or ceil(original) for r.
+ */
+poly::Rational approximateToDyadic(const poly::Rational& r,
+                                   const poly::Rational& original);
+
+/**
+ * Constructs a poly::AlgebraicNumber, allowing for refinement of the
+ * CVC4::Rational bounds. As a poly::AlgebraicNumber works on
+ * poly::DyadicRationals internally, the bounds are iteratively refined using
+ * approximateToDyadic until the respective interval is isolating. If the
+ * provided rational bounds are already dyadic, the refinement is skipped.
+ */
+poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p,
+                                              const Rational& lower,
+                                              const Rational& upper);
+
+/**
+ * Constructs a CVC4::RealAlgebraicNumber, simply wrapping
+ * toPolyRanWithRefinement.
+ */
+RealAlgebraicNumber toRanWithRefinement(poly::UPolynomial&& p,
+                                        const Rational& lower,
+                                        const Rational& upper);
+
+std::size_t totalDegree(const poly::Polynomial& p);
+
+/**
+ * Collects information about a single variable in a set of polynomials.
+ * Used for determining a variable ordering.
+ */
+struct VariableInformation
+{
+  poly::Variable var;
+  /** Maximum degree of this variable. */
+  std::size_t max_degree = 0;
+  /** Maximum degree of the leading coefficient of this variable. */
+  std::size_t max_lc_degree = 0;
+  /** Maximum of total degrees of terms that contain this variable. */
+  std::size_t max_terms_tdegree = 0;
+  /** Sum of degrees of this variable. */
+  std::size_t sum_degree = 0;
+  /** Number of terms that contain this variable. */
+  std::size_t num_terms = 0;
+};
+
+void getVariableInformation(VariableInformation& vi,
+                            const poly::Polynomial& poly);
+
+}  // namespace poly_utils
+}  // namespace CVC4
+
+#endif
+
+#endif /* CVC4__POLY_UTIL_H */
diff --git a/src/util/real_algebraic_number.h.in b/src/util/real_algebraic_number.h.in
new file mode 100644
index 000000000..f8fb6567c
--- /dev/null
+++ b/src/util/real_algebraic_number.h.in
@@ -0,0 +1,25 @@
+/*********************                                                        */
+/*! \file real_algebraic_number.h.in
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A real algebraic number constant
+ **
+ ** A real algebraic number constant.
+ **/
+
+// these gestures are used to avoid a public header dependence on cvc4autoconfig.h
+
+#if /* use libpoly */ @CVC4_USE_POLY_IMP@
+#  define CVC4_POLY_IMP
+#endif /* @CVC4_USE_POLY_IMP@ */
+
+#ifdef CVC4_POLY_IMP
+#  include "util/real_algebraic_number_poly_imp.h"
+#endif /* CVC4_POLY_IMP */
diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp
new file mode 100644
index 000000000..dc3098b19
--- /dev/null
+++ b/src/util/real_algebraic_number_poly_imp.cpp
@@ -0,0 +1,175 @@
+/*********************                                                        */
+/*! \file real_algebraic_number_poly_imp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of RealAlgebraicNumber based on libpoly.
+ **
+ ** Implementation of RealAlgebraicNumber based on libpoly.
+ **/
+
+#include "cvc4autoconfig.h"
+#include "util/real_algebraic_number.h"
+
+#ifndef CVC4_POLY_IMP  // Make sure this comes after cvc4autoconfig.h
+#error "This source should only ever be built if CVC4_POLY_IMP is on!"
+#endif /* CVC4_POLY_IMP */
+
+#include <poly/polyxx.h>
+
+#include <limits>
+
+#include "base/check.h"
+#include "util/poly_util.h"
+
+namespace CVC4 {
+
+RealAlgebraicNumber::RealAlgebraicNumber(poly::AlgebraicNumber&& an)
+    : d_value(std::move(an))
+{
+}
+
+RealAlgebraicNumber::RealAlgebraicNumber(const Integer& i)
+    : d_value(poly::DyadicRational(poly_utils::toInteger(i)))
+{
+}
+
+RealAlgebraicNumber::RealAlgebraicNumber(const Rational& r)
+{
+  poly::Rational pr = poly_utils::toRational(r);
+  auto dr = poly_utils::toDyadicRational(r);
+  if (dr)
+  {
+    d_value = poly::AlgebraicNumber(dr.value());
+  }
+  else
+  {
+    d_value = poly::AlgebraicNumber(
+        poly::UPolynomial({numerator(pr), -denominator(pr)}),
+        poly::DyadicInterval(floor(pr), ceil(pr)));
+  }
+}
+
+RealAlgebraicNumber::RealAlgebraicNumber(const std::vector<long>& coefficients,
+                                         long lower,
+                                         long upper)
+{
+  for (long c : coefficients)
+  {
+    Assert(std::numeric_limits<std::int32_t>::min() <= c
+           && c <= std::numeric_limits<std::int32_t>::max())
+        << "Coefficients need to fit within 32 bit integers. Please use the "
+           "constructor based on Integer instead.";
+  }
+  d_value = poly::AlgebraicNumber(poly::UPolynomial(coefficients),
+                                  poly::DyadicInterval(lower, upper));
+}
+
+RealAlgebraicNumber::RealAlgebraicNumber(
+    const std::vector<Integer>& coefficients,
+    const Rational& lower,
+    const Rational& upper)
+{
+  *this = poly_utils::toRanWithRefinement(
+      poly::UPolynomial(poly_utils::toInteger(coefficients)), lower, upper);
+}
+RealAlgebraicNumber::RealAlgebraicNumber(
+    const std::vector<Rational>& coefficients,
+    const Rational& lower,
+    const Rational& upper)
+{
+  Integer factor = Integer(1);
+  for (const auto& c : coefficients)
+  {
+    factor = factor.lcm(c.getDenominator());
+  }
+  std::vector<poly::Integer> coeffs;
+  for (const auto& c : coefficients)
+  {
+    Assert((c * factor).getDenominator() == Integer(1));
+    coeffs.emplace_back(poly_utils::toInteger((c * factor).getNumerator()));
+  }
+  *this = poly_utils::toRanWithRefinement(
+      poly::UPolynomial(std::move(coeffs)), lower, upper);
+}
+
+std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber& ran)
+{
+  return os << ran.getValue();
+}
+
+bool operator==(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() == rhs.getValue();
+}
+bool operator!=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() != rhs.getValue();
+}
+bool operator<(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() < rhs.getValue();
+}
+bool operator<=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() <= rhs.getValue();
+}
+bool operator>(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() > rhs.getValue();
+}
+bool operator>=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() >= rhs.getValue();
+}
+
+RealAlgebraicNumber operator+(const RealAlgebraicNumber& lhs,
+                              const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() + rhs.getValue();
+}
+RealAlgebraicNumber operator-(const RealAlgebraicNumber& lhs,
+                              const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() - rhs.getValue();
+}
+RealAlgebraicNumber operator-(const RealAlgebraicNumber& ran)
+{
+  return -ran.getValue();
+}
+RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs,
+                              const RealAlgebraicNumber& rhs)
+{
+  return lhs.getValue() * rhs.getValue();
+}
+
+RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs,
+                                const RealAlgebraicNumber& rhs)
+{
+  lhs.getValue() = lhs.getValue() + rhs.getValue();
+  return lhs;
+}
+RealAlgebraicNumber& operator-=(RealAlgebraicNumber& lhs,
+                                const RealAlgebraicNumber& rhs)
+{
+  lhs.getValue() = lhs.getValue() - rhs.getValue();
+  return lhs;
+}
+RealAlgebraicNumber& operator*=(RealAlgebraicNumber& lhs,
+                                const RealAlgebraicNumber& rhs)
+{
+  lhs.getValue() = lhs.getValue() * rhs.getValue();
+  return lhs;
+}
+
+int sgn(const RealAlgebraicNumber& ran) { return sgn(ran.getValue()); }
+bool isZero(const RealAlgebraicNumber& ran) { return is_zero(ran.getValue()); }
+bool isOne(const RealAlgebraicNumber& ran) { return is_one(ran.getValue()); }
+
+}  // namespace CVC4
diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h
new file mode 100644
index 000000000..beee648f0
--- /dev/null
+++ b/src/util/real_algebraic_number_poly_imp.h
@@ -0,0 +1,160 @@
+/*********************                                                        */
+/*! \file real_algebraic_number_poly_imp.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Algebraic number constants; wraps a libpoly algebraic number.
+ **
+ ** Algebraic number constants; wraps a libpoly algebraic number.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__REAL_ALGEBRAIC_NUMBER_H
+#define CVC4__REAL_ALGEBRAIC_NUMBER_H
+
+#include <vector>
+
+#include <poly/polyxx.h>
+
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+/**
+ * Represents a real algebraic number based on poly::AlgebraicNumber.
+ * This real algebraic number is represented by a (univariate) polynomial and an
+ * isolating interval. The interval contains exactly one real root of the
+ * polynomial, which is the number the real algebraic number as a whole
+ * represents.
+ * This representation can hold rationals (where the interval can be a point
+ * interval and the polynomial is omitted), an irrational algebraic number (like
+ * square roots), but no trancendentals (like pi).
+ * Note that the interval representation uses dyadic rationals (denominators are
+ * only powers of two).
+ */
+class CVC4_PUBLIC RealAlgebraicNumber
+{
+ public:
+  /** Construct as zero. */
+  RealAlgebraicNumber() = default;
+  /** Move from a poly::AlgebraicNumber type. */
+  RealAlgebraicNumber(poly::AlgebraicNumber&& an);
+  /** Copy from an Integer. */
+  RealAlgebraicNumber(const Integer& i);
+  /** Copy from a Rational. */
+  RealAlgebraicNumber(const Rational& r);
+  /**
+   * Construct from a polynomial with the given coefficients and an open
+   * interval with the given bounds.
+   */
+  RealAlgebraicNumber(const std::vector<long>& coefficients,
+                      long lower,
+                      long upper);
+  /**
+   * Construct from a polynomial with the given coefficients and an open
+   * interval with the given bounds. If the bounds are not dyadic, we need to
+   * perform refinement to find a suitable dyadic interval.
+   * See poly_utils::toRanWithRefinement for more details.
+   */
+  RealAlgebraicNumber(const std::vector<Integer>& coefficients,
+                      const Rational& lower,
+                      const Rational& upper);
+  /**
+   * Construct from a polynomial with the given coefficients and an open
+   * interval with the given bounds. If the bounds are not dyadic, we need to
+   * perform refinement to find a suitable dyadic interval.
+   * See poly_utils::toRanWithRefinement for more details.
+   */
+  RealAlgebraicNumber(const std::vector<Rational>& coefficients,
+                      const Rational& lower,
+                      const Rational& upper);
+
+  /** Copy constructor. */
+  RealAlgebraicNumber(const RealAlgebraicNumber& ran) = default;
+  /** Move constructor. */
+  RealAlgebraicNumber(RealAlgebraicNumber&& ran) = default;
+
+  /** Default destructor. */
+  ~RealAlgebraicNumber() = default;
+
+  /** Copy assignment. */
+  RealAlgebraicNumber& operator=(const RealAlgebraicNumber& ran) = default;
+  /** Move assignment. */
+  RealAlgebraicNumber& operator=(RealAlgebraicNumber&& ran) = default;
+
+  /** Get the internal value as a const reference. */
+  const poly::AlgebraicNumber& getValue() const { return d_value; }
+  /** Get the internal value as a non-const reference. */
+  poly::AlgebraicNumber& getValue() { return d_value; }
+
+ private:
+  /**
+   * Stores the actual real algebraic number.
+   */
+  poly::AlgebraicNumber d_value;
+}; /* class RealAlgebraicNumber */
+
+/** Stream a real algebraic number to an output stream. */
+CVC4_PUBLIC std::ostream& operator<<(std::ostream& os,
+                                     const RealAlgebraicNumber& ran);
+
+/** Compare two real algebraic numbers. */
+CVC4_PUBLIC bool operator==(const RealAlgebraicNumber& lhs,
+                            const RealAlgebraicNumber& rhs);
+/** Compare two real algebraic numbers. */
+CVC4_PUBLIC bool operator!=(const RealAlgebraicNumber& lhs,
+                            const RealAlgebraicNumber& rhs);
+/** Compare two real algebraic numbers. */
+CVC4_PUBLIC bool operator<(const RealAlgebraicNumber& lhs,
+                           const RealAlgebraicNumber& rhs);
+/** Compare two real algebraic numbers. */
+CVC4_PUBLIC bool operator<=(const RealAlgebraicNumber& lhs,
+                            const RealAlgebraicNumber& rhs);
+/** Compare two real algebraic numbers. */
+CVC4_PUBLIC bool operator>(const RealAlgebraicNumber& lhs,
+                           const RealAlgebraicNumber& rhs);
+/** Compare two real algebraic numbers. */
+CVC4_PUBLIC bool operator>=(const RealAlgebraicNumber& lhs,
+                            const RealAlgebraicNumber& rhs);
+
+/** Add two real algebraic numbers. */
+CVC4_PUBLIC RealAlgebraicNumber operator+(const RealAlgebraicNumber& lhs,
+                                          const RealAlgebraicNumber& rhs);
+/** Subtract two real algebraic numbers. */
+CVC4_PUBLIC RealAlgebraicNumber operator-(const RealAlgebraicNumber& lhs,
+                                          const RealAlgebraicNumber& rhs);
+/** Negate a real algebraic number. */
+CVC4_PUBLIC RealAlgebraicNumber operator-(const RealAlgebraicNumber& ran);
+/** Multiply two real algebraic numbers. */
+CVC4_PUBLIC RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs,
+                                          const RealAlgebraicNumber& rhs);
+
+/** Add and assign two real algebraic numbers. */
+CVC4_PUBLIC RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs,
+                                            const RealAlgebraicNumber& rhs);
+/** Subtract and assign two real algebraic numbers. */
+CVC4_PUBLIC RealAlgebraicNumber& operator-=(RealAlgebraicNumber& lhs,
+                                            const RealAlgebraicNumber& rhs);
+/** Multiply and assign two real algebraic numbers. */
+CVC4_PUBLIC RealAlgebraicNumber& operator*=(RealAlgebraicNumber& lhs,
+                                            const RealAlgebraicNumber& rhs);
+
+/** Compute the sign of a real algebraic number. */
+CVC4_PUBLIC int sgn(const RealAlgebraicNumber& ran);
+
+/** Check whether a real algebraic number is zero. */
+CVC4_PUBLIC bool isZero(const RealAlgebraicNumber& ran);
+/** Check whether a real algebraic number is one. */
+CVC4_PUBLIC bool isOne(const RealAlgebraicNumber& ran);
+
+}  // namespace CVC4
+
+#endif /* CVC4__REAL_ALGEBRAIC_NUMBER_H */
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 9b9a2a100..bd7c1ea22 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -65,6 +65,10 @@ macro(cvc4_add_unit_test is_white name output_dir)
     # We don't link against LFSC, because CVC4 is already linked against it.
     target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
   endif()
+  if(USE_POLY)
+    # We don't link against libpoly, because CVC4 is already linked against it.
+    target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR})
+  endif()
   if(${is_white})
     target_compile_options(${name} PRIVATE -fno-access-control)
   endif()
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 5bccc9137..af2ca0dfa 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -17,4 +17,7 @@ cvc4_add_unit_test_black(listener_black util)
 cvc4_add_unit_test_black(output_black util)
 cvc4_add_unit_test_black(rational_black util)
 cvc4_add_unit_test_white(rational_white util)
+if(CVC4_USE_POLY_IMP)
+cvc4_add_unit_test_black(real_algebraic_number_black util)
+endif()
 cvc4_add_unit_test_black(stats_black util)
diff --git a/test/unit/util/real_algebraic_number_black.h b/test/unit/util/real_algebraic_number_black.h
new file mode 100644
index 000000000..5fb41b50d
--- /dev/null
+++ b/test/unit/util/real_algebraic_number_black.h
@@ -0,0 +1,83 @@
+/*********************                                                        */
+/*! \file real_algebraic_number_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::RealAlgebraicNumber.
+ **
+ ** Black box testing of CVC4::RealAlgebraicNumber.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "util/real_algebraic_number.h"
+
+using namespace CVC4;
+using namespace std;
+
+#ifndef CVC4_POLY_IMP
+#error "This unit test should only be enabled for CVC4_POLY_IMP"
+#endif
+
+class RealAlgebraicNumberBlack : public CxxTest::TestSuite
+{
+ public:
+  void testCreation()
+  {
+    TS_ASSERT(isZero(RealAlgebraicNumber()));
+    TS_ASSERT(isOne(RealAlgebraicNumber(Integer(1))));
+    TS_ASSERT(!isOne(RealAlgebraicNumber(Rational(2))));
+    RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+    TS_ASSERT(RealAlgebraicNumber(Integer(1)) < sqrt2);
+    TS_ASSERT(sqrt2 < RealAlgebraicNumber(Integer(2)));
+  }
+
+  void testComparison()
+  {
+    RealAlgebraicNumber msqrt3({-3, 0, 1}, -2, -1);
+    RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
+    RealAlgebraicNumber zero;
+    RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+    RealAlgebraicNumber sqrt3({-3, 0, 1}, 1, 2);
+
+    TS_ASSERT(msqrt3 < msqrt2);
+    TS_ASSERT(msqrt3 < zero);
+    TS_ASSERT(msqrt3 < sqrt2);
+    TS_ASSERT(msqrt3 < sqrt3);
+    TS_ASSERT(msqrt2 < zero);
+    TS_ASSERT(msqrt2 < sqrt2);
+    TS_ASSERT(msqrt2 < sqrt3);
+    TS_ASSERT(zero < sqrt2);
+    TS_ASSERT(zero < sqrt3);
+    TS_ASSERT(sqrt2 < sqrt3);
+  }
+
+  void testSgn()
+  {
+    RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
+    RealAlgebraicNumber zero;
+    RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+
+    TS_ASSERT_EQUALS(sgn(msqrt2), -1);
+    TS_ASSERT_EQUALS(sgn(zero), 0);
+    TS_ASSERT_EQUALS(sgn(sqrt2), 1);
+  }
+
+  void testArithmetic()
+  {
+    RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
+    RealAlgebraicNumber zero;
+    RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+
+    TS_ASSERT_EQUALS(msqrt2 + sqrt2, zero);
+    TS_ASSERT_EQUALS(-msqrt2, sqrt2);
+    TS_ASSERT_EQUALS(-msqrt2 + sqrt2, sqrt2 + sqrt2);
+    TS_ASSERT_EQUALS(msqrt2 * sqrt2, RealAlgebraicNumber(Integer(-2)));
+  }
+};
-- 
2.30.2