diff options
Diffstat (limited to 'src')
| -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 |
11 files changed, 813 insertions, 1 deletions
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 */ |