Merge branch 'development'

CMakeLists.txt

@@ -14,7 +14,7 @@ include(carlmacros)
 
 set(PROJECT_FULLNAME "carl")
 set(PROJECT_DESCRIPTION "Computer ARithmetic Library")
-set_version(23 05)
+set_version(24 02)
 message(STATUS "Version: ${PROJECT_FULLNAME} ${PROJECT_VERSION_FULL}")
 
 # # # # # # # # # # # # # # # # # # # # # #

cmake/FindPoly.cmake

@@ -15,6 +15,9 @@ if(LIBPOLY_INCLUDE_DIR AND LIBPOLY_SHARED AND LIBPOLY_STATIC AND LIBPOLYXX_SHARE
 endif()
 
 if(NOT LIBPOLY_FOUND_SYSTEM)
+	get_target_property(GMP_LIB GMP_SHARED IMPORTED_LOCATION)
+	get_target_property(GMP_LIBRARY_DIR GMP_STATIC INTERFACE_INCLUDE_DIRECTORIES)
+
 	ExternalProject_Add(
 	LIBPOLY-EP
 	GIT_REPOSITORY https://github.com/SRI-CSL/libpoly
@@ -25,7 +28,8 @@ if(NOT LIBPOLY_FOUND_SYSTEM)
 			-DLIBPOLY_BUILD_PYTHON_API=OFF
 			-DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE}
 			-DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=TRUE
-			-DGMP_INCLUDE_DIR=${GMP_INCLUDE_DIR}
+			-DGMP_INCLUDE_DIR=${GMP_LIBRARY_DIR}
+			-DGMP_LIBRARY=${GMP_LIB}
 		BUILD_COMMAND ${CMAKE_COMMAND} <SOURCE_DIR>
 		COMMAND ${CMAKE_MAKE_PROGRAM} poly polyxx static_poly static_polyxx static_pic_poly static_pic_polyxx
 		COMMAND ${CMAKE_MAKE_PROGRAM} install
@@ -41,6 +45,7 @@ if(NOT LIBPOLY_FOUND_SYSTEM)
 #		COMMAND ${CMAKE_COMMAND} -E remove_directory <BINARY_DIR>/test/
 #	)
 
+	get_target_property(GMP_INCLUDE_DIR GMP_STATIC INTERFACE_SYSTEM_INCLUDE_DIRECTORIES)
 	get_target_property(GMP_LIBRARY GMP_STATIC IMPORTED_LOCATION)
 	get_filename_component(GMP_LIBRARY_DIR ${GMP_LIBRARY} DIRECTORY)
 
@@ -51,12 +56,12 @@ if(NOT LIBPOLY_FOUND_SYSTEM)
 	set(LIBPOLYXX_SHARED "${CMAKE_BINARY_DIR}/resources/lib/libpolyxx${DYNAMIC_EXT}")
 	set(LIBPOLYXX_STATIC "${CMAKE_BINARY_DIR}/resources/lib/libpolyxx${STATIC_EXT}")
 
-
 add_dependencies(LIBPOLY-EP GMP_SHARED GMPXX_SHARED)
 
 endif()
 
 
+
 add_library(LIBPOLY_SHARED SHARED IMPORTED GLOBAL)
 target_link_libraries(LIBPOLY_SHARED INTERFACE GMP_SHARED)
 set_target_properties(LIBPOLY_SHARED PROPERTIES

resources/gmp.cmake

@@ -1,18 +1,26 @@
 if(UNIX)
+	message(STATUS "Trying to build GMP from source.")
+
+	# GMP needs M4 to be installed
 	find_program(M4 m4)
 	if(NOT M4)
-		message(FATAL_ERROR "Can not build gmp, missing binary for m4")
-	endif()
+		message(FATAL_ERROR "Unable to build GMP from source. Could not find M4. Please install it.")
+	endif ()
 	mark_as_advanced(M4)
 
+	# GMP needs makeinfo to be installed but is only necessary for the documentation
+	# just disable it
+	set(CONFIGURE_ENV env "MAKEINFO=true")
+
 	ExternalProject_Add(
-		GMP-EP
-		URL "https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2"
-		URL_MD5 86ee6e54ebfc4a90b643a65e402c4048
-		DOWNLOAD_NO_PROGRESS 1
-		BUILD_IN_SOURCE YES
-		CONFIGURE_COMMAND ./configure --enable-cxx --prefix=<INSTALL_DIR>
+			GMP-EP
+			URL https://ftp.gnu.org/gnu/gmp/gmp-${GMP_VERSION}.tar.bz2
+			URL_HASH SHA1=db38c7b67f8eea9f2e5b8a48d219165b2fdab11f
+			CONFIGURE_COMMAND ${CONFIGURE_ENV} <SOURCE_DIR>/configure --prefix=<INSTALL_DIR> --with-pic --enable-cxx
+			BUILD_COMMAND ${MAKE}
+			BUILD_BYPRODUCTS ${GMP_LIBRARIES}
 	)
+
 elseif(WIN32)
 	ExternalProject_Add(
 		GMP-EP
@@ -52,3 +60,5 @@ add_dependencies(GMP_STATIC GMP-EP)
 add_dependencies(GMPXX_SHARED GMP-EP)
 add_dependencies(GMPXX_STATIC GMP-EP)
 add_dependencies(resources GMP_SHARED GMP_STATIC GMPXX_SHARED GMPXX_STATIC)
+
+

src/carl-arith/extended/VariableComparison.h

@@ -80,32 +80,49 @@ namespace carl {
 		VariableComparison invert_relation() const {
 			return VariableComparison(m_var, m_value, carl::inverse(m_relation), m_negated);
 		}
+		VariableComparison resolve_negation() const {
+			if (m_negated) return VariableComparison(m_var, m_value, carl::inverse(m_relation), false);
+			else return *this;
+		}
 	};
 
 	/**
 	 * Convert this variable comparison "v < root(..)" into a simpler
 	 * polynomial (in)equality against zero "p(..) < 0" if that is possible.
 	 * @return std::nullopt if conversion impossible.
 	 */
-	template<typename Poly>
+	template<typename Poly, std::enable_if_t<!needs_context_type<Poly>::value, bool> = true>
 	std::optional<BasicConstraint<Poly>> as_constraint(const VariableComparison<Poly>& f) {
 		Relation rel = f.negated() ? inverse(f.relation()) : f.relation();
 		if (std::holds_alternative<typename VariableComparison<Poly>::MR>(f.value())) {
 			const auto& mr = std::get<typename VariableComparison<Poly>::MR>(f.value());
 			if (mr.poly().degree(mr.var()) != 1) return std::nullopt;
 			if (mr.k() != 1) return std::nullopt;
 			auto lcoeff = mr.poly().coeff(mr.var(), 1);
-			if (!lcoeff.is_constant()) return std::nullopt;
+			if (!is_constant(lcoeff)) return std::nullopt;
 			auto ccoeff = mr.poly().coeff(mr.var(), 0);
 			return BasicConstraint<Poly>(Poly(f.var()) + ccoeff / lcoeff, rel);
-		}
-		assert(!needs_context_type<Poly>::value);
-		if constexpr(!needs_context_type<Poly>::value) {
-			if (!std::get<typename VariableComparison<Poly>::RAN>(f.value()).is_numeric()) return std::nullopt;
-			return BasicConstraint<Poly>(Poly(f.var()) - Poly(std::get<typename VariableComparison<Poly>::RAN>(f.value()).value()), rel);
-		} else {
-			static_assert(dependent_false_v<Poly>);
-		}
+		} else if (!std::get<typename VariableComparison<Poly>::RAN>(f.value()).is_numeric()) return std::nullopt;
+		else return BasicConstraint<Poly>(Poly(f.var()) - Poly(std::get<typename VariableComparison<Poly>::RAN>(f.value()).value()), rel);
+	}
+
+	/**
+	 * Convert this variable comparison "v < root(..)" into a simpler
+	 * polynomial (in)equality against zero "p(..) < 0" if that is possible.
+	 * @return std::nullopt if conversion impossible.
+	 */
+	template<typename Poly, std::enable_if_t<needs_context_type<Poly>::value, bool> = true>
+	std::optional<BasicConstraint<Poly>> as_constraint(const VariableComparison<Poly>& f) {
+		Relation rel = f.negated() ? inverse(f.relation()) : f.relation();
+		assert (std::holds_alternative<typename VariableComparison<Poly>::MR>(f.value()));
+		const auto& mr = std::get<typename VariableComparison<Poly>::MR>(f.value());
+		assert(mr.var() == mr.poly().main_var());
+		if (mr.poly().degree() != 1) return std::nullopt;
+		if (mr.k() != 1) return std::nullopt;
+		auto lcoeff = mr.poly().lcoeff();
+		if (!is_constant(lcoeff)) return std::nullopt;
+		auto ccoeff = mr.poly().coeff(0);
+		return BasicConstraint<Poly>(Poly(mr.poly().context(), f.var())*lcoeff + ccoeff, lcoeff>0 ? rel : carl::turn_around(rel));
 	}
 
 	/**

src/carl-arith/poly/libpoly/CoCoAAdaptorLP.h

@@ -242,12 +242,10 @@ class CoCoAAdaptorLP {
     // 	return res;
     // }
 
-    // auto GBasis(const std::vector<Coeff>& p) const {
-    // 	auto start = CARL_TIME_START();
-    // 	auto res = convert(cocoawrapper::ReducedGBasis(convert(p)));
-    // 	CARL_TIME_FINISH(cocoa::statistics().gbasis, start);
-    // 	return res;
-    // }
+    auto GBasis(const std::vector<LPPolynomial>& p) const {
+    	auto res = convert(cocoawrapper::ReducedGBasis(convert(p)));
+    	return res;
+    }
 };
 
 } // namespace carl

src/carl-arith/poly/libpoly/Functions.h

@@ -36,6 +36,10 @@ inline LPPolynomial content(const LPPolynomial& p) {
     return LPPolynomial(p.context(), poly::content(p.get_polynomial()));
 }
 
+inline LPPolynomial derivative(const LPPolynomial& p) {
+    return LPPolynomial(p.context(), poly::derivative(p.get_polynomial()));
+}
+
 /*
  * @brief wrapper for the polynomial primitive_part calculation using libpoly.
  * @param LPPolynomial p
@@ -140,6 +144,12 @@ inline std::vector<LPPolynomial> content_free_factors(const LPPolynomial& p) {
     return result;
 }
 
+inline std::vector<LPPolynomial> groebner_basis(const std::vector<LPPolynomial>& polys) {
+    if (polys.size() <= 1) return polys;
+    CoCoAAdaptorLP adaptor = CoCoAAdaptorLP(polys.at(0).context());
+    return adaptor.GBasis(polys);
+}
+
 } // namespace carl
 
 #endif

src/carl-arith/poly/libpoly/LPPolynomial.cpp

@@ -32,20 +32,20 @@ LPPolynomial& LPPolynomial::operator=(LPPolynomial&& rhs) {
 
 LPPolynomial::LPPolynomial(const LPContext& context)
     : m_poly(context.lp_context()), m_context(context) {
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
     assert(lp_polynomial_check_order(m_poly.get_internal()));
 }
 
 LPPolynomial::LPPolynomial(const LPContext& context, const poly::Polynomial& p)
     : m_poly(p), m_context(context) {
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 
     assert(lp_polynomial_check_order(m_poly.get_internal()));
     assert(context.lp_context() == lp_polynomial_get_context(get_internal()));
 }
 LPPolynomial::LPPolynomial(const LPContext& context, poly::Polynomial&& p)
     : m_poly(std::move(p)), m_context(context) {
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 
     assert(lp_polynomial_check_order(m_poly.get_internal()));
     assert(context.lp_context() == lp_polynomial_get_context(get_internal()));
@@ -54,15 +54,15 @@ LPPolynomial::LPPolynomial(const LPContext& context, poly::Polynomial&& p)
 LPPolynomial::LPPolynomial(const LPContext& context, long val)
     : m_context(context) {
     lp_polynomial_construct_simple(m_poly.get_internal(), context.lp_context(), poly::Integer(val).get_internal(), 0, 0);
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 
     assert(lp_polynomial_check_order(m_poly.get_internal()));
 }
 
 LPPolynomial::LPPolynomial(const LPContext& context, const mpz_class& val)
     : m_context(context) {
     lp_polynomial_construct_simple(m_poly.get_internal(), context.lp_context(), val.get_mpz_t(), lp_variable_null, 0) ;
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 
     assert(lp_polynomial_check_order(m_poly.get_internal()));
 }
@@ -74,15 +74,15 @@ LPPolynomial::LPPolynomial(const LPContext& context, const mpq_class& val) : LPP
 LPPolynomial::LPPolynomial(const LPContext& context, const Variable& var, const mpz_class& coeff, unsigned int degree)
     : m_context(context) {
     lp_polynomial_construct_simple(m_poly.get_internal(), context.lp_context(), poly::Integer(coeff).get_internal(), *context.lp_variable(var), degree);
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 
     assert(lp_polynomial_check_order(m_poly.get_internal()));
 }
 
 LPPolynomial::LPPolynomial(const LPContext& context, const Variable& var)
     : m_context(context) {
     lp_polynomial_construct_simple(m_poly.get_internal(), context.lp_context(), poly::Integer(1).get_internal(), *context.lp_variable(var), 1);
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 
     assert(lp_polynomial_check_order(m_poly.get_internal()));
 }
@@ -100,7 +100,7 @@ LPPolynomial::LPPolynomial(const LPContext& context, const Variable& mainVar, co
         lp_polynomial_construct_simple(temp.get_internal(), context.lp_context(), poly::Integer(coeff).get_internal(), *var, (unsigned int)pow);
         m_poly += temp;
     }
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 }
 
 LPPolynomial::LPPolynomial(const LPContext& context, const Variable& mainVar, const std::vector<mpz_class>& coefficients)
@@ -117,7 +117,7 @@ LPPolynomial::LPPolynomial(const LPContext& context, const Variable& mainVar, co
         lp_polynomial_construct_simple(temp.get_internal(), context.lp_context(), poly::Integer(coeff).get_internal(), *var, (unsigned int)pow);
         m_poly += temp;
     }
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 }
 
 LPPolynomial::LPPolynomial(const LPContext& context, const Variable& mainVar, std::vector<mpz_class>&& coefficients)
@@ -133,7 +133,7 @@ LPPolynomial::LPPolynomial(const LPContext& context, const Variable& mainVar, st
         lp_polynomial_construct_simple(temp.get_internal(), context.lp_context(), poly::Integer(std::move(coeff)).get_internal(), *var, (unsigned int)pow);
         m_poly += temp;
     }
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 }
 
 LPPolynomial::LPPolynomial(const LPContext& context, const Variable& mainVar, const std::map<unsigned int, mpz_class>& coefficients)
@@ -147,7 +147,7 @@ LPPolynomial::LPPolynomial(const LPContext& context, const Variable& mainVar, co
         lp_polynomial_construct_simple(temp.get_internal(), context.lp_context(), poly::Integer(coef.second).get_internal(), *var, coef.first);
         m_poly += temp;
     }
-    lp_polynomial_set_external(m_poly.get_internal());
+    //lp_polynomial_set_external(m_poly.get_internal());
 }
 
 bool LPPolynomial::has(const Variable& var) const {
@@ -401,6 +401,61 @@ std::size_t LPPolynomial::degree(Variable::Arg var) const {
     return travers.degree;
 }
 
+std::vector<std::size_t>  LPPolynomial::monomial_total_degrees() const {
+    struct degree_travers {
+        std::vector<std::size_t> degree;
+    };
+
+    auto getDegree = [](const lp_polynomial_context_t* /*ctx*/,
+                        lp_monomial_t* m,
+                        void* d) {
+        degree_travers& v = *static_cast<degree_travers*>(d);
+
+        size_t current_degree = 0;
+        // iterate over the number of variables and add up their degrees
+        for (size_t i = 0; i < m->n; i++) {
+            current_degree += m->p[i].d;
+        }
+        v.degree.push_back(current_degree);
+    };
+
+    degree_travers travers;
+    lp_polynomial_traverse(get_internal(), getDegree, &travers);
+
+    return travers.degree;
+}
+
+std::vector<std::size_t>  LPPolynomial::monomial_degrees(Variable::Arg var) const {
+    struct degree_travers {
+        std::vector<std::size_t> degree;
+        lp_variable_t var; // the variable we are looking for
+    };
+
+    auto getDegree = [](const lp_polynomial_context_t* /*ctx*/,
+                        lp_monomial_t* m,
+                        void* d) {
+        degree_travers& v = *static_cast<degree_travers*>(d);
+
+        size_t current_degree = 0;
+        // iterate over the number of variables and add up their degrees
+        for (size_t i = 0; i < m->n; i++) {
+            if (m->p[i].x == v.var) {
+                current_degree = m->p[i].d;
+                break;
+            }
+        }
+        v.degree.push_back(current_degree);
+    };
+
+    degree_travers travers;
+    auto lp_var = context().lp_variable(var);
+    assert(lp_var.has_value());
+    travers.var = *lp_var;
+    lp_polynomial_traverse(get_internal(), getDegree, &travers);
+
+    return travers.degree;
+}
+
 mpz_class LPPolynomial::unit_part() const {
     //As we can only have integer coefficients, they do not form a field
     //Thus the unit part is the sign of the leading coefficient, if it is not zero

src/carl-arith/poly/libpoly/LPPolynomial.h

@@ -180,6 +180,10 @@ class LPPolynomial {
 		return LPPolynomial(m_context, poly::leading_coefficient(m_poly));
 	}
 
+	LPPolynomial coeff(std::size_t k) const {
+		return LPPolynomial(m_context, poly::coefficient(m_poly, k));
+	}
+
 	/** Obtain all non-zero coefficients of a polynomial. */
 	std::vector<LPPolynomial> coefficients() const {
 		std::vector<LPPolynomial> res;
@@ -378,6 +382,10 @@ class LPPolynomial {
 
 	std::size_t degree(Variable::Arg var) const ;
 
+	std::vector<std::size_t> monomial_total_degrees() const;
+	std::vector<std::size_t> monomial_degrees(Variable::Arg var) const;
+
+
 	/**
 	 * Calculates the coefficient of var^exp.
 	 * @param var Variable.

src/carl-arith/poly/umvpoly/CoCoAAdaptorStatistics.h

@@ -9,9 +9,9 @@ namespace cocoa {
 
 class CoCoAAdaptorStatistics : public statistics::Statistics {
 public:
-    statistics::timer gcd;
-    statistics::timer factorize;
-    statistics::timer gbasis;
+    statistics::Timer gcd;
+    statistics::Timer factorize;
+    statistics::Timer gbasis;
     void collect() {
         Statistics::addKeyValuePair("gcd", gcd);
         Statistics::addKeyValuePair("factorize", factorize);