diff options
-rw-r--r-- | .github/workflows/ci.yml | 2 | ||||
-rw-r--r-- | CMakeLists.txt | 17 | ||||
-rw-r--r-- | COPYING | 2 | ||||
-rw-r--r-- | INSTALL.md | 8 | ||||
-rw-r--r-- | cmake/FindPoly.cmake | 24 | ||||
-rwxr-xr-x | configure.sh | 14 | ||||
-rwxr-xr-x | contrib/get-poly | 31 | ||||
-rw-r--r-- | src/CMakeLists.txt | 7 | ||||
-rw-r--r-- | src/base/configuration.cpp | 13 | ||||
-rw-r--r-- | src/base/configuration.h | 2 | ||||
-rw-r--r-- | src/base/configuration_private.h | 6 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 1 | ||||
-rw-r--r-- | src/util/CMakeLists.txt | 7 | ||||
-rw-r--r-- | src/util/poly_util.cpp | 282 | ||||
-rw-r--r-- | src/util/poly_util.h | 136 | ||||
-rw-r--r-- | src/util/real_algebraic_number.h.in | 25 | ||||
-rw-r--r-- | src/util/real_algebraic_number_poly_imp.cpp | 175 | ||||
-rw-r--r-- | src/util/real_algebraic_number_poly_imp.h | 160 | ||||
-rw-r--r-- | test/unit/CMakeLists.txt | 4 | ||||
-rw-r--r-- | test/unit/util/CMakeLists.txt | 3 | ||||
-rw-r--r-- | test/unit/util/real_algebraic_number_black.h | 83 |
21 files changed, 998 insertions, 4 deletions
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() @@ -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))); + } +}; |