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.
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
run: |
${{ matrix.env }} ./configure.sh ${{ matrix.config }} \
--python3 \
+ --poly \
--prefix=$(pwd)/build/install \
--unit-testing
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()
# > 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)")
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
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)
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")
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()
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
text-editing support in interactive mode. GNU Readline is available here:
http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html
-
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)
available on the system. Override with `ARGS=-jN`.
Use `-jN` for parallel **building** with `N` threads.
-
-
--- /dev/null
+# 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()
--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
--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
gpl=default
kissat=default
lfsc=default
+poly=default
muzzle=default
ninja=default
optimized=default
gmp_dir=default
kissat_dir=default
lfsc_dir=default
+poly_dir=default
symfpu_dir=default
#--------------------------------------------------------------------------#
--lfsc) lfsc=ON;;
--no-lfsc) lfsc=OFF;;
+ --poly) poly=ON;;
+ --no-poly) poly=OFF;;
+
--muzzle) muzzle=ON;;
--no-muzzle) muzzle=OFF;;
--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##*=} ;;
&& 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 ] \
&& 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 ] \
--- /dev/null
+#!/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
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}>)
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
${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)
}
}
- 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"
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()
return IS_LFSC_BUILD;
}
+bool Configuration::isBuiltWithPoly()
+{
+ return IS_POLY_BUILD;
+}
+
bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; }
unsigned Configuration::getNumDebugTags() {
static bool isBuiltWithLfsc();
+ static bool isBuiltWithPoly();
+
static bool isBuiltWithSymFPU();
/* Return the number of debug tags */
#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 */
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());
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
maybe.h
ostream_util.cpp
ostream_util.h
+ poly_util.cpp
+ poly_util.h
proof.h
random.cpp
random.h
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()
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
# 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()
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)
--- /dev/null
+/********************* */
+/*! \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)));
+ }
+};
projects / cvc5.git / commitdiff