From 4126787789711ea66525dc5f8ec349fef6ff65f8 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Mon, 29 May 2023 20:24:33 +0200 Subject: [PATCH 01/37] fix smtcomp ran printing --- src/carl-io/SMTLIBStream.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/carl-io/SMTLIBStream.h b/src/carl-io/SMTLIBStream.h index 3c867853..e30577f7 100644 --- a/src/carl-io/SMTLIBStream.h +++ b/src/carl-io/SMTLIBStream.h @@ -160,7 +160,7 @@ class SMTLIBStream { *this << " " << *it; } *this << ") "; - *this << "(" << ran.interval().lower() << " " << ran.interval().upper() << ")"; + *this << ran.interval().lower() << " " << ran.interval().upper(); *this << ")"; } From 6ed8fa352057d7749f3117353048b08338dbb775 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Tue, 30 May 2023 09:08:50 +0200 Subject: [PATCH 02/37] fix smtcomp ran printing --- src/carl-io/SMTLIBStream.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/carl-io/SMTLIBStream.h b/src/carl-io/SMTLIBStream.h index e30577f7..e8a5782c 100644 --- a/src/carl-io/SMTLIBStream.h +++ b/src/carl-io/SMTLIBStream.h @@ -153,7 +153,7 @@ class SMTLIBStream { *this << "(root-of-with-interval "; const auto& coeffs = p.coefficients(); auto it = coeffs.begin(); - *this << "(" << *it; + *this << "(coeffs " << *it; it++; for (; it != coeffs.end(); it++) { assert(carl::is_integer(*it)); From 0bbb62cba430b14cc7d76fefc53070f42fe7ed5f Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Tue, 30 May 2023 09:36:44 +0200 Subject: [PATCH 03/37] fix smtlib model printing --- src/carl-io/SMTLIBStream.h | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/carl-io/SMTLIBStream.h b/src/carl-io/SMTLIBStream.h index e8a5782c..308d4a12 100644 --- a/src/carl-io/SMTLIBStream.h +++ b/src/carl-io/SMTLIBStream.h @@ -114,7 +114,7 @@ class SMTLIBStream { template void write(const Model& model) { - *this << "(model" << std::endl; + *this << "(" << std::endl; for (const auto& m: model) { auto value = m.second; value = model.evaluated(m.first); @@ -289,6 +289,11 @@ class SMTLIBStream { default: *this << "?"; break; } } + + void write(const bool b) { + if (b) *this << "true"; + else *this << "false"; + } template void write(T&& t) { From 7d70f430b74cbdd6bf8eb7ca677a6188cd40f31f Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Tue, 30 May 2023 12:26:43 +0200 Subject: [PATCH 04/37] fix smtlib model printing --- src/carl-io/SMTLIBStream.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/carl-io/SMTLIBStream.h b/src/carl-io/SMTLIBStream.h index 308d4a12..0eb676e0 100644 --- a/src/carl-io/SMTLIBStream.h +++ b/src/carl-io/SMTLIBStream.h @@ -114,7 +114,7 @@ class SMTLIBStream { template void write(const Model& model) { - *this << "(" << std::endl; + *this << "(model " << std::endl; for (const auto& m: model) { auto value = m.second; value = model.evaluated(m.first); From 6e68d5d11e7c2231141701414c6cc81a5c580307 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 7 Jul 2023 10:10:58 +0200 Subject: [PATCH 05/37] lp features --- src/carl-arith/extended/VariableComparison.h | 33 ++++++++++++++------ src/carl-arith/poly/libpoly/Functions.h | 4 +++ src/carl-arith/poly/libpoly/LPPolynomial.h | 4 +++ 3 files changed, 31 insertions(+), 10 deletions(-) diff --git a/src/carl-arith/extended/VariableComparison.h b/src/carl-arith/extended/VariableComparison.h index b281ea94..fb3c0abd 100644 --- a/src/carl-arith/extended/VariableComparison.h +++ b/src/carl-arith/extended/VariableComparison.h @@ -87,7 +87,7 @@ namespace carl { * polynomial (in)equality against zero "p(..) < 0" if that is possible. * @return std::nullopt if conversion impossible. */ - template + template::value, bool> = true> std::optional> as_constraint(const VariableComparison& f) { Relation rel = f.negated() ? inverse(f.relation()) : f.relation(); if (std::holds_alternative::MR>(f.value())) { @@ -95,17 +95,30 @@ namespace carl { 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(f.var()) + ccoeff / lcoeff, rel); - } - assert(!needs_context_type::value); - if constexpr(!needs_context_type::value) { - if (!std::get::RAN>(f.value()).is_numeric()) return std::nullopt; - return BasicConstraint(Poly(f.var()) - Poly(std::get::RAN>(f.value()).value()), rel); - } else { - static_assert(dependent_false_v); - } + } else if (!std::get::RAN>(f.value()).is_numeric()) return std::nullopt; + else return BasicConstraint(Poly(f.var()) - Poly(std::get::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::value, bool> = true> + std::optional> as_constraint(const VariableComparison& f) { + Relation rel = f.negated() ? inverse(f.relation()) : f.relation(); + assert (std::holds_alternative::MR>(f.value())); + const auto& mr = std::get::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(mr.poly().context(), f.var())*lcoeff + ccoeff, lcoeff>0 ? rel : carl::turn_around(rel)); } /** diff --git a/src/carl-arith/poly/libpoly/Functions.h b/src/carl-arith/poly/libpoly/Functions.h index ac200fe6..413b777f 100644 --- a/src/carl-arith/poly/libpoly/Functions.h +++ b/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 diff --git a/src/carl-arith/poly/libpoly/LPPolynomial.h b/src/carl-arith/poly/libpoly/LPPolynomial.h index 2d5d0ffe..9960069f 100644 --- a/src/carl-arith/poly/libpoly/LPPolynomial.h +++ b/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 coefficients() const { std::vector res; From 4314e5141a0fdb0d7547c3010313acf8f2af63e1 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Fri, 14 Jul 2023 15:04:26 +0200 Subject: [PATCH 06/37] turn off sanitizeFactors (related bug seems fixed) --- src/carl-arith/poly/umvpoly/functions/Factorization.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/carl-arith/poly/umvpoly/functions/Factorization.h b/src/carl-arith/poly/umvpoly/functions/Factorization.h index e1e94adf..2aead38c 100644 --- a/src/carl-arith/poly/umvpoly/functions/Factorization.h +++ b/src/carl-arith/poly/umvpoly/functions/Factorization.h @@ -79,7 +79,7 @@ Factors> factorization(const MultivariatePolynomia }; auto factors = s(p); - helper::sanitizeFactors(p, factors); + // helper::sanitizeFactors(p, factors); return factors; } From a4e2f6bb5a0bc9d618f914758e188172b147413d Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Mon, 24 Jul 2023 11:17:05 +0200 Subject: [PATCH 07/37] streaming operator for flat_map --- src/carl-common/util/streamingOperators.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/carl-common/util/streamingOperators.h b/src/carl-common/util/streamingOperators.h index 35ef0155..ad3baa28 100644 --- a/src/carl-common/util/streamingOperators.h +++ b/src/carl-common/util/streamingOperators.h @@ -22,6 +22,7 @@ #include #include #include "boost/container/flat_set.hpp" +#include "boost/container/flat_map.hpp" namespace carl { @@ -225,6 +226,18 @@ inline std::ostream& operator<<(std::ostream& os, const std::unordered_map:, :, ...}` + * @param os Output stream. + * @param m map to be printed. + * @return Output stream. + */ +template +inline std::ostream& operator<<(std::ostream& os, const boost::container::flat_map& m) { + return os << "{" << stream_joined(", ", m, [](auto& o, const auto& p){ o << p.first << " : " << p.second; }) << "}"; +} + /** * Output a std::unordered_set with arbitrary content. * The format is `{: , , ...}` From a65c05d0d3a5f83b541887ed797d4fceb14fc600 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Tue, 8 Aug 2023 16:52:34 +0200 Subject: [PATCH 08/37] remove sanitize_factors for good --- .../poly/umvpoly/functions/Factorization.h | 29 ++----------------- 1 file changed, 2 insertions(+), 27 deletions(-) diff --git a/src/carl-arith/poly/umvpoly/functions/Factorization.h b/src/carl-arith/poly/umvpoly/functions/Factorization.h index 2aead38c..0647a682 100644 --- a/src/carl-arith/poly/umvpoly/functions/Factorization.h +++ b/src/carl-arith/poly/umvpoly/functions/Factorization.h @@ -20,32 +20,8 @@ namespace helper { Factors> trivialFactorization(const MultivariatePolynomial& p) { return { std::make_pair(p, 1) }; } - - template - void sanitizeFactors(const MultivariatePolynomial& reference, Factors>& factors) { - MultivariatePolynomial p(1); - for (const auto& f: factors) { - p *= carl::pow(f.first, f.second); - } - if (p == reference) return; - if (p == -reference) { - CARL_LOG_WARN("carl.core.factorize", "The factorization had an incorrect sign, correct it."); - CARL_LOG_WARN("carl.core.factorize", reference << " -> " << factors); - MultivariatePolynomial factor(-1); - auto it = std::find_if(factors.begin(), factors.end(), [](const auto& f){ return f.first.is_constant(); }); - if (it != factors.end()) { - assert(it->second == 1); - factor *= it->first; - factors.erase(it); - } - factors.emplace(factor, 1); - return; - } - CARL_LOG_WARN("carl.core.factorize", "The factorization was incorrect, return trivial factorization."); - CARL_LOG_WARN("carl.core.factorize", reference << " -> " << factors); - factors = trivialFactorization(reference); - } -} + +} // namespace helper /** * Try to factorize a multivariate polynomial.. @@ -79,7 +55,6 @@ Factors> factorization(const MultivariatePolynomia }; auto factors = s(p); - // helper::sanitizeFactors(p, factors); return factors; } From 49ee7d6a018ef9ad9c6e0cbf3018523181802b51 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Thu, 14 Sep 2023 16:49:27 +0200 Subject: [PATCH 09/37] gbasis for lppolynomial --- src/carl-arith/poly/libpoly/CoCoAAdaptorLP.h | 10 ++++------ src/carl-arith/poly/libpoly/Functions.h | 6 ++++++ 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/carl-arith/poly/libpoly/CoCoAAdaptorLP.h b/src/carl-arith/poly/libpoly/CoCoAAdaptorLP.h index f14ca945..4d7b9be1 100644 --- a/src/carl-arith/poly/libpoly/CoCoAAdaptorLP.h +++ b/src/carl-arith/poly/libpoly/CoCoAAdaptorLP.h @@ -242,12 +242,10 @@ class CoCoAAdaptorLP { // return res; // } - // auto GBasis(const std::vector& 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& p) const { + auto res = convert(cocoawrapper::ReducedGBasis(convert(p))); + return res; + } }; } // namespace carl diff --git a/src/carl-arith/poly/libpoly/Functions.h b/src/carl-arith/poly/libpoly/Functions.h index 413b777f..be61f7e2 100644 --- a/src/carl-arith/poly/libpoly/Functions.h +++ b/src/carl-arith/poly/libpoly/Functions.h @@ -144,6 +144,12 @@ inline std::vector content_free_factors(const LPPolynomial& p) { return result; } +inline std::vector groebner_basis(const std::vector& polys) { + if (polys.size() <= 1) return polys; + CoCoAAdaptorLP adaptor = CoCoAAdaptorLP(polys.at(0).context()); + return adaptor.GBasis(polys); +} + } // namespace carl #endif \ No newline at end of file From 96e47ae3ca5a69d9dffa5f1cfe24a5ff9689de93 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 22 Sep 2023 14:57:56 +0200 Subject: [PATCH 10/37] bugfix --- src/carl-formula/formula/Formula.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/carl-formula/formula/Formula.h b/src/carl-formula/formula/Formula.h index 441bd21f..214325c7 100644 --- a/src/carl-formula/formula/Formula.h +++ b/src/carl-formula/formula/Formula.h @@ -490,8 +490,7 @@ namespace carl */ const_iterator end() const { - assert( mpContent->mType == FormulaType::AND || mpContent->mType == FormulaType::OR - || mpContent->mType == FormulaType::IFF || mpContent->mType == FormulaType::XOR ); + assert( is_nary() ); return std::get>(mpContent->mContent).end(); } From fdbbdf8ef30464f4bcb9872ca4c906cf8110cafc Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 22 Sep 2023 14:58:02 +0200 Subject: [PATCH 11/37] =?UTF-8?q?coca=20gr=C3=B6bner?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../poly/umvpoly/functions/Groebner.h | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 src/carl-arith/poly/umvpoly/functions/Groebner.h diff --git a/src/carl-arith/poly/umvpoly/functions/Groebner.h b/src/carl-arith/poly/umvpoly/functions/Groebner.h new file mode 100644 index 00000000..a92bb886 --- /dev/null +++ b/src/carl-arith/poly/umvpoly/functions/Groebner.h @@ -0,0 +1,17 @@ +#pragma once + +#include "../CoCoAAdaptor.h" + +namespace carl { + +template +class MultivariatePolynomial; + +template +std::vector> groebner_basis(const std::vector>& polys) { + if (polys.size() <= 1) return polys; + CoCoAAdaptor adaptor(polys); + return adaptor.GBasis(polys); +} + +} From a3de28142f48d2a247bb2c6c7cb5cc4ad8288a9d Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Mon, 25 Sep 2023 12:55:44 +0200 Subject: [PATCH 12/37] ran interface --- src/carl-arith/ran/interval/Ran.h | 4 ++-- src/carl-arith/ran/libpoly/LPRan.cpp | 8 ++++++++ src/carl-arith/ran/libpoly/LPRan.h | 3 +++ 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/carl-arith/ran/interval/Ran.h b/src/carl-arith/ran/interval/Ran.h index 7107f6f7..b930f66b 100644 --- a/src/carl-arith/ran/interval/Ran.h +++ b/src/carl-arith/ran/interval/Ran.h @@ -150,14 +150,13 @@ class IntRepRealAlgebraicNumber { } } -public: // TODO should be private +public: void refine() const { if (is_numeric()) return; Number pivot = carl::sample(interval_int()); refine_internal(pivot); } -private: std::optional refine_using(const Number& pivot) const { if (interval_int().contains(pivot)) { if (is_numeric()) return Sign::ZERO; @@ -166,6 +165,7 @@ class IntRepRealAlgebraicNumber { return std::nullopt; } +private: /// Refines until the number is either numeric or the interval does not contain any integer. void refine_to_integrality() const { while (!interval_int().is_point_interval() && interval_int().contains_integer()) { diff --git a/src/carl-arith/ran/libpoly/LPRan.cpp b/src/carl-arith/ran/libpoly/LPRan.cpp index 0645bcf1..f3eff88a 100644 --- a/src/carl-arith/ran/libpoly/LPRan.cpp +++ b/src/carl-arith/ran/libpoly/LPRan.cpp @@ -275,6 +275,10 @@ void refine(const LPRealAlgebraicNumber& n) { CARL_LOG_DEBUG("carl.ran.libpoly", "Finished Refining Algebraic NumberType : " << n); } +void LPRealAlgebraicNumber::refine() const { + carl::refine(*this); +} + /** * Refine until n is numeric (rational) or until pivot is not in the isolating interval of n * NOT CONST, the number is the same, but internally might change @@ -290,6 +294,10 @@ void refine_using(const LPRealAlgebraicNumber& n, const NumberType& pivot) { CARL_LOG_DEBUG("carl.ran.libpoly", "Finished Refining Algebraic NumberType : " << n); } +void LPRealAlgebraicNumber::refine_using(const NumberType& pivot) const { + carl::refine_using(*this, pivot); +} + /** * Same as above, but with libpoly dyadic rational as pivot */ diff --git a/src/carl-arith/ran/libpoly/LPRan.h b/src/carl-arith/ran/libpoly/LPRan.h index 6bbba349..50a5c54a 100644 --- a/src/carl-arith/ran/libpoly/LPRan.h +++ b/src/carl-arith/ran/libpoly/LPRan.h @@ -144,6 +144,9 @@ class LPRealAlgebraicNumber { friend NumberType sample_between(const NumberType& lower, const LPRealAlgebraicNumber& upper); friend NumberType floor(const LPRealAlgebraicNumber& n); friend NumberType ceil(const LPRealAlgebraicNumber& n); + + void refine() const; + void refine_using(const LPRealAlgebraicNumber::NumberType& pivot) const; }; bool compare(const LPRealAlgebraicNumber&, const LPRealAlgebraicNumber&, const Relation); From 7ae6b92a19bcd3e59b8cd793c3b58167fdb83a09 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Tue, 26 Sep 2023 10:31:30 +0200 Subject: [PATCH 13/37] fix bug --- src/carl-arith/ran/libpoly/LPRan.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/carl-arith/ran/libpoly/LPRan.cpp b/src/carl-arith/ran/libpoly/LPRan.cpp index f3eff88a..034434e3 100644 --- a/src/carl-arith/ran/libpoly/LPRan.cpp +++ b/src/carl-arith/ran/libpoly/LPRan.cpp @@ -154,9 +154,11 @@ const UnivariatePolynomial LPRealAlgebraicNumber::polynomial() const } const Interval LPRealAlgebraicNumber::interval() const { - const NumberType& lo = get_lower_bound(); - const NumberType& up = get_upper_bound(); - return Interval(lo, BoundType::STRICT, up, BoundType::STRICT); + if (is_numeric()) { + return Interval(get_lower_bound()); + } else { + return Interval(get_lower_bound(), BoundType::STRICT, get_upper_bound(), BoundType::STRICT); + } } const NumberType LPRealAlgebraicNumber::get_upper_bound() const { From 0e75f18b4d040501d44aa034cf496a2a14a33c6a Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Tue, 26 Sep 2023 16:17:39 +0200 Subject: [PATCH 14/37] remove refine_using from lp --- src/carl-arith/ran/libpoly/LPRan.cpp | 37 ---------------------------- src/carl-arith/ran/libpoly/LPRan.h | 3 --- 2 files changed, 40 deletions(-) diff --git a/src/carl-arith/ran/libpoly/LPRan.cpp b/src/carl-arith/ran/libpoly/LPRan.cpp index 034434e3..c1381139 100644 --- a/src/carl-arith/ran/libpoly/LPRan.cpp +++ b/src/carl-arith/ran/libpoly/LPRan.cpp @@ -281,38 +281,6 @@ void LPRealAlgebraicNumber::refine() const { carl::refine(*this); } -/** - * Refine until n is numeric (rational) or until pivot is not in the isolating interval of n - * NOT CONST, the number is the same, but internally might change - */ - -void refine_using(const LPRealAlgebraicNumber& n, const NumberType& pivot) { - CARL_LOG_DEBUG("carl.ran.libpoly", "Refining Algebraic NumberType : " << n); - //Convert pivot to libpoly rational - poly::Rational pivot_libpoly = to_libpoly_rational(pivot); - while (!n.is_numeric() && n.libpoly_interval() == pivot_libpoly) { - lp_algebraic_number_refine_const(n.get_internal()); - } - CARL_LOG_DEBUG("carl.ran.libpoly", "Finished Refining Algebraic NumberType : " << n); -} - -void LPRealAlgebraicNumber::refine_using(const NumberType& pivot) const { - carl::refine_using(*this, pivot); -} - -/** - * Same as above, but with libpoly dyadic rational as pivot - */ - -void refine_using(const LPRealAlgebraicNumber& n, const poly::DyadicRational& pivot) { - CARL_LOG_DEBUG("carl.ran.libpoly", "Refining Algebraic NumberType : " << n); - while (!n.is_numeric() && n.libpoly_interval() == pivot) { - lp_algebraic_number_refine_const(n.get_internal()); - } - CARL_LOG_DEBUG("carl.ran.libpoly", "Finished Refining Algebraic NumberType : " << n); -} - - NumberType branching_point(const LPRealAlgebraicNumber& n) { //return carl::sample(n.interval_int()); refine(n); @@ -454,13 +422,8 @@ const carl::Variable LPRealAlgebraicNumber::auxVariable = fresh_real_variable("_ bool compare(const LPRealAlgebraicNumber& lhs, const NumberType& rhs, const Relation relation) { - poly::Rational rat = to_libpoly_rational(rhs); - //refine unitl rhs in not in interval of lhs - //Technically not necessary because libpoly does that in compare, but whatever - refine_using(lhs, rhs); - int cmp = lp_algebraic_number_cmp_rational(lhs.get_internal(), rat.get_internal()); switch (relation) { diff --git a/src/carl-arith/ran/libpoly/LPRan.h b/src/carl-arith/ran/libpoly/LPRan.h index 50a5c54a..4fc4e397 100644 --- a/src/carl-arith/ran/libpoly/LPRan.h +++ b/src/carl-arith/ran/libpoly/LPRan.h @@ -146,7 +146,6 @@ class LPRealAlgebraicNumber { friend NumberType ceil(const LPRealAlgebraicNumber& n); void refine() const; - void refine_using(const LPRealAlgebraicNumber::NumberType& pivot) const; }; bool compare(const LPRealAlgebraicNumber&, const LPRealAlgebraicNumber&, const Relation); @@ -162,8 +161,6 @@ LPRealAlgebraicNumber::NumberType floor(const LPRealAlgebraicNumber& n); LPRealAlgebraicNumber::NumberType ceil(const LPRealAlgebraicNumber& n); void refine(const LPRealAlgebraicNumber& n); -void refine_using(const LPRealAlgebraicNumber& n, const LPRealAlgebraicNumber::NumberType& pivot); -void refine_using(const LPRealAlgebraicNumber& n, const poly::DyadicRational& pivot); inline bool is_zero(const LPRealAlgebraicNumber& n) { refine(n); From 4e782ff672758b97a7a47e4bfc2aca87b769559a Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Tue, 26 Sep 2023 17:37:39 +0200 Subject: [PATCH 15/37] fix bug --- src/carl-arith/ran/libpoly/LPRan.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/carl-arith/ran/libpoly/LPRan.cpp b/src/carl-arith/ran/libpoly/LPRan.cpp index c1381139..70d20fa1 100644 --- a/src/carl-arith/ran/libpoly/LPRan.cpp +++ b/src/carl-arith/ran/libpoly/LPRan.cpp @@ -155,7 +155,7 @@ const UnivariatePolynomial LPRealAlgebraicNumber::polynomial() const const Interval LPRealAlgebraicNumber::interval() const { if (is_numeric()) { - return Interval(get_lower_bound()); + return Interval(value()); } else { return Interval(get_lower_bound(), BoundType::STRICT, get_upper_bound(), BoundType::STRICT); } From 436e5986474e0b6b9e2b15b7e4805d4890348fa5 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Mon, 2 Oct 2023 15:18:30 +0200 Subject: [PATCH 16/37] logging --- src/carl-arith/ran/libpoly/RealRoots.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/carl-arith/ran/libpoly/RealRoots.cpp b/src/carl-arith/ran/libpoly/RealRoots.cpp index 1d70a2c4..5d47a8fc 100644 --- a/src/carl-arith/ran/libpoly/RealRoots.cpp +++ b/src/carl-arith/ran/libpoly/RealRoots.cpp @@ -85,7 +85,9 @@ RealRootsResult real_roots( lp_value_destruct(&val); } + CARL_LOG_TRACE("carl.ran.libpoly", "Call libpoly"); std::vector roots = poly::isolate_real_roots(polynomial.get_polynomial(), assignment); + CARL_LOG_TRACE("carl.ran.libpoly", "Libpoly returned"); if (roots.empty()) { CARL_LOG_DEBUG("carl.ran.libpoly", " Checking for nullification -> Evaluation at " << mainVar << "= 1"); From b767332a489988ee90383b7aba39975b0a009fd9 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Tue, 14 Nov 2023 09:31:13 +0100 Subject: [PATCH 17/37] better statistics --- .../poly/umvpoly/CoCoAAdaptorStatistics.h | 6 +-- src/carl-statistics/MultiCounter.h | 26 ++++++++++ src/carl-statistics/Serialization.h | 15 ++++++ src/carl-statistics/Series.h | 28 +++++++++++ src/carl-statistics/Statistics.h | 48 ++++++++++++------- src/carl-statistics/Timing.h | 14 +++++- src/carl-statistics/carl-statistics.h | 2 +- src/tests/carl-statistics/Test_Statistics.cpp | 4 +- 8 files changed, 119 insertions(+), 24 deletions(-) create mode 100644 src/carl-statistics/MultiCounter.h create mode 100644 src/carl-statistics/Serialization.h create mode 100644 src/carl-statistics/Series.h diff --git a/src/carl-arith/poly/umvpoly/CoCoAAdaptorStatistics.h b/src/carl-arith/poly/umvpoly/CoCoAAdaptorStatistics.h index ce683e60..cf8c542b 100644 --- a/src/carl-arith/poly/umvpoly/CoCoAAdaptorStatistics.h +++ b/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); diff --git a/src/carl-statistics/MultiCounter.h b/src/carl-statistics/MultiCounter.h new file mode 100644 index 00000000..b49d5291 --- /dev/null +++ b/src/carl-statistics/MultiCounter.h @@ -0,0 +1,26 @@ +#pragma once + +#include + +namespace carl::statistics { + +template +class MultiCounter { + boost::container::flat_map m_data; + +public: + void inc(const T& key, std::size_t inc) { + m_data.try_emplace(key).first->second += inc; + } + + void collect(std::map& data, const std::string& key) const { + std::stringstream ss; + for (const auto& [k,v] : m_data) { + serialize(ss, k); + ss << ":" << v << ";"; + } + data.emplace(key, ss.str()); + } +}; + +} \ No newline at end of file diff --git a/src/carl-statistics/Serialization.h b/src/carl-statistics/Serialization.h new file mode 100644 index 00000000..474ca912 --- /dev/null +++ b/src/carl-statistics/Serialization.h @@ -0,0 +1,15 @@ +#pragma once + +namespace carl::statistics { + +template +void serialize(std::stringstream& ss, const std::pair& pair) { + ss << "[" << pair.first << "," << pair.second << "]"; +} + +template +void serialize(std::stringstream& ss, const T& v) { + ss << v; +} + +} \ No newline at end of file diff --git a/src/carl-statistics/Series.h b/src/carl-statistics/Series.h new file mode 100644 index 00000000..15216bfc --- /dev/null +++ b/src/carl-statistics/Series.h @@ -0,0 +1,28 @@ +#pragma once + +namespace carl::statistics { + +class Series { + std::size_t m_count = 0; + std::size_t m_sum = 0; + std::size_t m_min = 0; + std::size_t m_max = 0; + +public: + void add(std::size_t n) { + m_sum += n; + m_min = m_count == 0 ? n : std::min(m_min, n); + m_max = m_count == 0 ? n : std::min(m_max, n); + m_count++; + } + + void collect(std::map& data, const std::string& key) const { + data.emplace(key+".count", std::to_string(m_count)); + data.emplace(key+".sum", std::to_string(m_sum)); + data.emplace(key+".min", std::to_string(m_min)); + data.emplace(key+".max", std::to_string(m_max)); + data.emplace(key+".avg", std::to_string((float)m_sum/m_count)); + } +}; + +} \ No newline at end of file diff --git a/src/carl-statistics/Statistics.h b/src/carl-statistics/Statistics.h index 465768f8..6202c62b 100644 --- a/src/carl-statistics/Statistics.h +++ b/src/carl-statistics/Statistics.h @@ -1,13 +1,16 @@ #pragma once -#include "StatisticsCollector.h" -#include "Timing.h" - #include #include #include #include +#include "StatisticsCollector.h" +#include "Serialization.h" +#include "Timing.h" +#include "Series.h" +#include "MultiCounter.h" + namespace carl { namespace statistics { @@ -21,23 +24,34 @@ class Statistics { }) != val.end(); } protected: - template - void addKeyValuePair(const std::string& key, const T& value) { + void addKeyValuePair(const std::string& key, const std::string& value) { assert(!has_illegal_chars(key) && "spaces, (, ) are not allowed here"); if (has_illegal_chars(key)) return; - if constexpr(std::is_same::value) { - assert(!has_illegal_chars(static_cast(value)) && "spaces, (, ) are not allowed here"); - if (has_illegal_chars(value)) return; - mCollected.emplace(key, value); - } else if constexpr(std::is_same::value) { - mCollected.emplace(key+"_count", std::to_string(static_cast(value).count())); - mCollected.emplace(key+"_overall_ms", std::to_string(static_cast(value).overall_ms())); - } else { - std::stringstream ss; - ss << value; - mCollected.emplace(key, ss.str()); - } + assert(!has_illegal_chars(static_cast(value)) && "spaces, (, ) are not allowed here"); + if (has_illegal_chars(value)) return; + mCollected.emplace(key, value); + } + + void addKeyValuePair(const std::string& key, const Timer& value) { + value.collect(mCollected, key); } + + void addKeyValuePair(const std::string& key, const Series& value) { + value.collect(mCollected, key); + } + + template + void addKeyValuePair(const std::string& key, const MultiCounter& value) { + value.collect(mCollected, key); + } + + template + void addKeyValuePair(const std::string& key, const T& value) { + std::stringstream ss; + serialize(ss, value); + mCollected.emplace(key, ss.str()); + } + public: Statistics() = default; virtual ~Statistics() = default; diff --git a/src/carl-statistics/Timing.h b/src/carl-statistics/Timing.h index d7a34a6b..9dc8d124 100644 --- a/src/carl-statistics/Timing.h +++ b/src/carl-statistics/Timing.h @@ -27,9 +27,10 @@ namespace timing { } } -class timer { +class Timer { std::size_t m_count = 0; timing::duration m_overall = timing::zero(); + timing::time_point m_current_start; public: static timing::time_point start() { @@ -39,12 +40,23 @@ class timer { ++m_count; m_overall += timing::since(start); } + void start_this() { + m_current_start = start(); + } + void finish() { + finish(m_current_start); + } auto count() const { return m_count; } auto overall_ms() const { return m_overall.count(); } + + void collect(std::map& data, const std::string& key) const { + data.emplace(key+".count", std::to_string(count())); + data.emplace(key+".overall_ms", std::to_string(overall_ms())); + } }; } diff --git a/src/carl-statistics/carl-statistics.h b/src/carl-statistics/carl-statistics.h index 2e5cac6d..be7a3172 100644 --- a/src/carl-statistics/carl-statistics.h +++ b/src/carl-statistics/carl-statistics.h @@ -21,7 +21,7 @@ namespace statistics { #ifdef CARL_DEVOPTION_Statistics #define CARL_INIT_STATISTICS(class, variable, name) class& variable = carl::statistics::get(name) #define CARL_CALL_STATISTICS(function) function - #define CARL_TIME_START(variable) auto variable = carl::statistics::timer::start() + #define CARL_TIME_START(variable) auto variable = carl::statistics::Timer::start() #define CARL_TIME_FINISH(timer, variable) timer.finish(variable) #else #define CARL_INIT_STATISTICS(class, variable, name) diff --git a/src/tests/carl-statistics/Test_Statistics.cpp b/src/tests/carl-statistics/Test_Statistics.cpp index 7cb06624..e25e1b6b 100644 --- a/src/tests/carl-statistics/Test_Statistics.cpp +++ b/src/tests/carl-statistics/Test_Statistics.cpp @@ -8,9 +8,9 @@ TEST(Statistics, Timer) { - auto start = carl::statistics::timer::start(); + auto start = carl::statistics::Timer::start(); std::this_thread::sleep_for(std::chrono::milliseconds(50)); - carl::statistics::timer timer; + carl::statistics::Timer timer; timer.finish(start); ASSERT_EQ(timer.count(), 1); } From 3168319490a3781ade42730fb1ea4b4efc43c281 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Tue, 14 Nov 2023 16:18:19 +0100 Subject: [PATCH 18/37] bugfix --- src/carl-statistics/Series.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/carl-statistics/Series.h b/src/carl-statistics/Series.h index 15216bfc..50bbe1b5 100644 --- a/src/carl-statistics/Series.h +++ b/src/carl-statistics/Series.h @@ -12,7 +12,7 @@ class Series { void add(std::size_t n) { m_sum += n; m_min = m_count == 0 ? n : std::min(m_min, n); - m_max = m_count == 0 ? n : std::min(m_max, n); + m_max = m_count == 0 ? n : std::max(m_max, n); m_count++; } From 0cda34e9ba89c29196623148d0ffafe3634c5c9c Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 24 Nov 2023 10:32:29 +0100 Subject: [PATCH 19/37] degrees in lp --- src/carl-arith/poly/libpoly/LPPolynomial.cpp | 55 ++++++++++++++++++++ src/carl-arith/poly/libpoly/LPPolynomial.h | 4 ++ 2 files changed, 59 insertions(+) diff --git a/src/carl-arith/poly/libpoly/LPPolynomial.cpp b/src/carl-arith/poly/libpoly/LPPolynomial.cpp index 873a0968..371ac5bc 100644 --- a/src/carl-arith/poly/libpoly/LPPolynomial.cpp +++ b/src/carl-arith/poly/libpoly/LPPolynomial.cpp @@ -401,6 +401,61 @@ std::size_t LPPolynomial::degree(Variable::Arg var) const { return travers.degree; } +std::vector LPPolynomial::monomial_total_degrees() const { + struct degree_travers { + std::vector degree; + }; + + auto getDegree = [](const lp_polynomial_context_t* /*ctx*/, + lp_monomial_t* m, + void* d) { + degree_travers& v = *static_cast(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 LPPolynomial::monomial_degrees(Variable::Arg var) const { + struct degree_travers { + std::vector 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(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 diff --git a/src/carl-arith/poly/libpoly/LPPolynomial.h b/src/carl-arith/poly/libpoly/LPPolynomial.h index 9960069f..28c557b0 100644 --- a/src/carl-arith/poly/libpoly/LPPolynomial.h +++ b/src/carl-arith/poly/libpoly/LPPolynomial.h @@ -382,6 +382,10 @@ class LPPolynomial { std::size_t degree(Variable::Arg var) const ; + std::vector monomial_total_degrees() const; + std::vector monomial_degrees(Variable::Arg var) const; + + /** * Calculates the coefficient of var^exp. * @param var Variable. From 61a7ca3d950ba058c0907f0ce7cecc36c73a43f0 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Mon, 27 Nov 2023 09:36:28 +0100 Subject: [PATCH 20/37] add ifdef --- src/carl-formula/formula/FormulaContent.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/carl-formula/formula/FormulaContent.h b/src/carl-formula/formula/FormulaContent.h index 1223d378..2ef87713 100644 --- a/src/carl-formula/formula/FormulaContent.h +++ b/src/carl-formula/formula/FormulaContent.h @@ -155,10 +155,12 @@ namespace carl { const FormulaContent *mNegation = nullptr; /// The propositions of this formula. Condition mProperties; + #ifdef THREAD_SAFE /// Mutex for access to activity. mutable std::mutex mActivityMutex; /// Mutex for collecting the variables within this formula. mutable std::mutex mVariablesMutex; + #endif /// Container collecting the variables which occur in this formula. mutable Variables* mpVariables = nullptr; From d742e18009fa90eb41b20a68c68c48413927addc Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Tue, 28 Nov 2023 11:27:29 +0100 Subject: [PATCH 21/37] shrink_to_fit --- src/carl-formula/formula/FormulaContent.tpp | 1 + src/carl-formula/formula/FormulaPool.h | 2 ++ 2 files changed, 3 insertions(+) diff --git a/src/carl-formula/formula/FormulaContent.tpp b/src/carl-formula/formula/FormulaContent.tpp index 7792c11f..ebd932b3 100644 --- a/src/carl-formula/formula/FormulaContent.tpp +++ b/src/carl-formula/formula/FormulaContent.tpp @@ -95,6 +95,7 @@ namespace carl { { assert( !std::get>(mContent).empty() ); assert( is_nary() ); + std::get>(mContent).shrink_to_fit(); for (const auto& subformula: std::get>(mContent)) { carl::hash_add(mHash, subformula.hash()); } diff --git a/src/carl-formula/formula/FormulaPool.h b/src/carl-formula/formula/FormulaPool.h index 77ca2ce6..5a63f1ce 100644 --- a/src/carl-formula/formula/FormulaPool.h +++ b/src/carl-formula/formula/FormulaPool.h @@ -49,8 +49,10 @@ namespace carl std::unique_ptr mPoolBuckets; /// The formula pool. underlying_set mPool; + #ifdef THREAD_SAFE /// Mutex to avoid multiple access to the pool mutable std::recursive_mutex mMutexPool; + #endif /// FastPointerMap,const FormulaContent*> mTseitinVars; From 9139bb68fdc440448141313a7d8423171eaab738 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Wed, 29 Nov 2023 15:21:06 +0100 Subject: [PATCH 22/37] selectively merge changes from Philips branch --- src/carl-arith/ran/Conversion.h | 2 ++ src/carl-common/util/hash.h | 6 ++++++ src/carl-formula/formula/Formula.h | 2 +- src/carl-formula/formula/Logic.h | 4 +++- 4 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/carl-arith/ran/Conversion.h b/src/carl-arith/ran/Conversion.h index 8b340da5..af36d774 100644 --- a/src/carl-arith/ran/Conversion.h +++ b/src/carl-arith/ran/Conversion.h @@ -1,6 +1,8 @@ #pragma once #include +#include +#include namespace carl { diff --git a/src/carl-common/util/hash.h b/src/carl-common/util/hash.h index 98ed61bb..f86dffa7 100644 --- a/src/carl-common/util/hash.h +++ b/src/carl-common/util/hash.h @@ -2,6 +2,7 @@ #include #include +#include namespace carl { @@ -48,6 +49,11 @@ inline void hash_add(std::size_t& seed, const std::vector& v) { for (const auto& t: v) carl::hash_add(seed, t); } +template +inline void hash_add(std::size_t& seed, const std::set& s) { + for (const auto& t: s) carl::hash_add(seed, t); +} + /** * Variadic version of `hash_add` to add an arbitrary number of values to the seed. */ diff --git a/src/carl-formula/formula/Formula.h b/src/carl-formula/formula/Formula.h index 214325c7..f4f8055f 100644 --- a/src/carl-formula/formula/Formula.h +++ b/src/carl-formula/formula/Formula.h @@ -456,7 +456,7 @@ namespace carl { if( mpContent->mType == FormulaType::BOOL || mpContent->mType == FormulaType::CONSTRAINT || mpContent->mType == FormulaType::TRUE || mpContent->mType == FormulaType::FALSE || mpContent->mType == FormulaType::NOT || mpContent->mType == FormulaType::UEQ - || mpContent->mType == FormulaType::BITVECTOR ) + || mpContent->mType == FormulaType::BITVECTOR || mpContent->mType == FormulaType::EXISTS || mpContent->mType == FormulaType::FORALL) return 1; else return std::get>(mpContent->mContent).size(); diff --git a/src/carl-formula/formula/Logic.h b/src/carl-formula/formula/Logic.h index f6f2ad7d..7c419476 100644 --- a/src/carl-formula/formula/Logic.h +++ b/src/carl-formula/formula/Logic.h @@ -5,7 +5,7 @@ namespace carl { enum class Logic { - QF_BV, QF_IDL, QF_LIA, QF_LIRA, QF_LRA, QF_NIA, QF_NIRA, QF_NRA, QF_PB, QF_RDL, QF_UF, UNDEFINED + QF_BV, QF_IDL, QF_LIA, QF_LIRA, QF_LRA, QF_NIA, QF_NIRA, QF_NRA, QF_PB, QF_RDL, QF_UF, NRA, LRA, UNDEFINED }; inline std::ostream& operator<<(std::ostream& os, const Logic& l) { @@ -21,6 +21,8 @@ inline std::ostream& operator<<(std::ostream& os, const Logic& l) { case Logic::QF_PB: os << "QF_PB"; break; case Logic::QF_RDL: os << "QF_RDL"; break; case Logic::QF_UF: os << "QF_UF"; break; + case Logic::NRA: os << "NRA"; break; + case Logic::LRA: os << "LRA"; break; case Logic::UNDEFINED: os << "undefined"; break; } return os; From a6654493fd4e885d499a3d175075da74d0842fe1 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Wed, 29 Nov 2023 17:33:33 +0100 Subject: [PATCH 23/37] add condition for quantifier to formulas --- src/carl-formula/formula/Condition.h | 34 +++++++++++++++------------- src/carl-formula/formula/Formula.tpp | 11 +++++---- 2 files changed, 24 insertions(+), 21 deletions(-) diff --git a/src/carl-formula/formula/Condition.h b/src/carl-formula/formula/Condition.h index 6388226d..2075b2b8 100644 --- a/src/carl-formula/formula/Condition.h +++ b/src/carl-formula/formula/Condition.h @@ -60,27 +60,29 @@ namespace carl { PROP_IS_A_CLAUSE | PROP_IS_A_LITERAL | PROP_IS_AN_ATOM | PROP_IS_LITERAL_CONJUNCTION; //Propositions which hold, if they hold in at least one sub formula (16-63) - static constexpr Condition PROP_CONTAINS_EQUATION = Condition( 16 ); - static constexpr Condition PROP_CONTAINS_INEQUALITY = Condition( 17 ); - static constexpr Condition PROP_CONTAINS_STRICT_INEQUALITY = Condition( 18 ); - static constexpr Condition PROP_CONTAINS_LINEAR_POLYNOMIAL = Condition( 19 ); - static constexpr Condition PROP_CONTAINS_NONLINEAR_POLYNOMIAL = Condition( 20 ); - static constexpr Condition PROP_CONTAINS_MULTIVARIATE_POLYNOMIAL = Condition( 21 ); - static constexpr Condition PROP_CONTAINS_BOOLEAN = Condition( 22 ); - static constexpr Condition PROP_CONTAINS_INTEGER_VALUED_VARS = Condition( 23 ); - static constexpr Condition PROP_CONTAINS_REAL_VALUED_VARS = Condition( 24 ); - static constexpr Condition PROP_CONTAINS_UNINTERPRETED_EQUATIONS = Condition( 25 ); - static constexpr Condition PROP_CONTAINS_BITVECTOR = Condition( 26 ); - static constexpr Condition PROP_CONTAINS_PSEUDOBOOLEAN = Condition( 27 ); - static constexpr Condition PROP_VARIABLE_DEGREE_GREATER_THAN_TWO = Condition( 28 ); + static constexpr Condition PROP_CONTAINS_EQUATION = Condition( 16 ); + static constexpr Condition PROP_CONTAINS_INEQUALITY = Condition( 17 ); + static constexpr Condition PROP_CONTAINS_STRICT_INEQUALITY = Condition( 18 ); + static constexpr Condition PROP_CONTAINS_LINEAR_POLYNOMIAL = Condition( 19 ); + static constexpr Condition PROP_CONTAINS_NONLINEAR_POLYNOMIAL = Condition( 20 ); + static constexpr Condition PROP_CONTAINS_MULTIVARIATE_POLYNOMIAL = Condition( 21 ); + static constexpr Condition PROP_CONTAINS_BOOLEAN = Condition( 22 ); + static constexpr Condition PROP_CONTAINS_INTEGER_VALUED_VARS = Condition( 23 ); + static constexpr Condition PROP_CONTAINS_REAL_VALUED_VARS = Condition( 24 ); + static constexpr Condition PROP_CONTAINS_UNINTERPRETED_EQUATIONS = Condition( 25 ); + static constexpr Condition PROP_CONTAINS_BITVECTOR = Condition( 26 ); + static constexpr Condition PROP_CONTAINS_PSEUDOBOOLEAN = Condition( 27 ); + static constexpr Condition PROP_VARIABLE_DEGREE_GREATER_THAN_TWO = Condition( 28 ); static constexpr Condition PROP_VARIABLE_DEGREE_GREATER_THAN_THREE = Condition( 29 ); - static constexpr Condition PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR = Condition( 30 ); - static constexpr Condition PROP_CONTAINS_WEAK_INEQUALITY = Condition( 31 ); + static constexpr Condition PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR = Condition( 30 ); + static constexpr Condition PROP_CONTAINS_WEAK_INEQUALITY = Condition( 31 ); + static constexpr Condition PROP_CONTAINS_QUANTIFIER = Condition( 32 ); + static const Condition WEAK_CONDITIONS = PROP_CONTAINS_EQUATION | PROP_CONTAINS_INEQUALITY | PROP_CONTAINS_STRICT_INEQUALITY | PROP_CONTAINS_LINEAR_POLYNOMIAL | PROP_CONTAINS_LINEAR_POLYNOMIAL | PROP_CONTAINS_NONLINEAR_POLYNOMIAL | PROP_CONTAINS_MULTIVARIATE_POLYNOMIAL | PROP_CONTAINS_INEQUALITY | PROP_CONTAINS_BOOLEAN | PROP_CONTAINS_REAL_VALUED_VARS | PROP_CONTAINS_INTEGER_VALUED_VARS | PROP_CONTAINS_UNINTERPRETED_EQUATIONS | PROP_CONTAINS_BITVECTOR | PROP_CONTAINS_PSEUDOBOOLEAN - | PROP_VARIABLE_DEGREE_GREATER_THAN_TWO | PROP_VARIABLE_DEGREE_GREATER_THAN_THREE | PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR; + | PROP_VARIABLE_DEGREE_GREATER_THAN_TWO | PROP_VARIABLE_DEGREE_GREATER_THAN_THREE | PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR | PROP_CONTAINS_QUANTIFIER; } // namespace carl diff --git a/src/carl-formula/formula/Formula.tpp b/src/carl-formula/formula/Formula.tpp index 6a47cd82..ff9e36e7 100644 --- a/src/carl-formula/formula/Formula.tpp +++ b/src/carl-formula/formula/Formula.tpp @@ -23,13 +23,14 @@ namespace carl switch( _content.mType ) { case FormulaType::EXISTS: - { - ///@todo do something here - break; - } case FormulaType::FORALL: { - ///@todo do something here + _content.mProperties |= PROP_CONTAINS_QUANTIFIER; + for (auto subFormula = std::get>(_content.mContent).begin(); subFormula != std::get>(_content.mContent).end(); ++subFormula) + { + Condition subFormulaConds = subFormula->properties(); + _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS); + } break; } case FormulaType::TRUE: From 21d920191a10f0c52b47b40c996e852cd947d05a Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Thu, 30 Nov 2023 16:30:19 +0100 Subject: [PATCH 24/37] bugfix --- src/carl-formula/formula/Formula.tpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/carl-formula/formula/Formula.tpp b/src/carl-formula/formula/Formula.tpp index ff9e36e7..1c3a60c1 100644 --- a/src/carl-formula/formula/Formula.tpp +++ b/src/carl-formula/formula/Formula.tpp @@ -26,11 +26,8 @@ namespace carl case FormulaType::FORALL: { _content.mProperties |= PROP_CONTAINS_QUANTIFIER; - for (auto subFormula = std::get>(_content.mContent).begin(); subFormula != std::get>(_content.mContent).end(); ++subFormula) - { - Condition subFormulaConds = subFormula->properties(); - _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS); - } + auto subFormula = std::get>(_content.mContent).mFormula; + _content.mProperties |= (subFormula.properties() & WEAK_CONDITIONS); break; } case FormulaType::TRUE: From 6a3d5d0589b635221d681c152ddef975357a14cf Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 1 Dec 2023 14:07:12 +0100 Subject: [PATCH 25/37] compielr warning --- src/carl-statistics/Series.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/carl-statistics/Series.h b/src/carl-statistics/Series.h index 50bbe1b5..9f7660a2 100644 --- a/src/carl-statistics/Series.h +++ b/src/carl-statistics/Series.h @@ -21,7 +21,7 @@ class Series { data.emplace(key+".sum", std::to_string(m_sum)); data.emplace(key+".min", std::to_string(m_min)); data.emplace(key+".max", std::to_string(m_max)); - data.emplace(key+".avg", std::to_string((float)m_sum/m_count)); + data.emplace(key+".avg", std::to_string((float)m_sum/(float)m_count)); } }; From 06c028aa01d7cee0cda2ce4d04a80c096473acf3 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 1 Dec 2023 14:07:26 +0100 Subject: [PATCH 26/37] Prenex normal form --- src/carl-formula/formula/functions/PNF.h | 203 +++++++++++++++++++++++ src/carl-formula/formula/functions/QF.h | 107 ------------ src/tests/carl-formula/Test_PNF.cpp | 59 +++++++ 3 files changed, 262 insertions(+), 107 deletions(-) create mode 100644 src/carl-formula/formula/functions/PNF.h delete mode 100644 src/carl-formula/formula/functions/QF.h create mode 100644 src/tests/carl-formula/Test_PNF.cpp diff --git a/src/carl-formula/formula/functions/PNF.h b/src/carl-formula/formula/functions/PNF.h new file mode 100644 index 00000000..9cfdff97 --- /dev/null +++ b/src/carl-formula/formula/functions/PNF.h @@ -0,0 +1,203 @@ +#pragma once + +#include "../Formula.h" +#include "Substitution.h" +#include "aux.h" + +namespace carl { + +enum class Quantifier { + EXISTS, + FORALL, + FREE +}; +inline std::ostream& operator<<(std::ostream& os, const Quantifier& type) { + switch (type) { + case Quantifier::EXISTS: + os << "exists"; + return os; + case Quantifier::FORALL: + os << "forall"; + return os; + case Quantifier::FREE: + os << "free"; + return os; + } +} + +using QuantifierPrefix = std::vector>; + +template +Formula to_pnf(const Formula& f, QuantifierPrefix& prefix, boost::container::flat_set& used_vars, bool negated = false) { + switch (f.type()) { + case FormulaType::AND: + case FormulaType::IFF: + case FormulaType::OR: + case FormulaType::XOR: { + if (!negated) { + Formulas subs; + for (auto& sub : f.subformulas()) { + subs.push_back(to_pnf(sub, prefix, used_vars, false)); + } + return Formula(f.type(), std::move(subs)); + } else if (f.type() == FormulaType::AND || f.type() == FormulaType::OR) { + Formulas subs; + for (auto& sub : f.subformulas()) { + subs.push_back(to_pnf(sub, prefix, used_vars, false)); + } + if (f.type() == FormulaType::AND) { + return Formula(FormulaType::OR, std::move(subs)); + } else { + return Formula(FormulaType::AND, std::move(subs)); + } + } else if (f.type() == FormulaType::IFF) { + Formulas sub1; + Formulas sub2; + for (auto& sub : f.subformulas()) { + sub1.push_back(to_pnf(sub, prefix, used_vars, true)); + sub2.push_back(to_pnf(sub, prefix, used_vars, false)); + } + return Formula(FormulaType::AND, {Formula(FormulaType::OR, std::move(sub1)), Formula(FormulaType::OR, std::move(sub2))}); + } else if (f.type() == FormulaType::XOR) { + auto lhs = to_pnf(f, prefix, used_vars, false); + auto rhs = to_pnf(formula::aux::connectPrecedingSubformulas(f), prefix, used_vars, false); + return Formula(FormulaType::IFF, std::vector>({lhs, rhs})); + } + assert(false); + } + case FormulaType::BOOL: + case FormulaType::CONSTRAINT: + case FormulaType::FALSE: + case FormulaType::UEQ: + case FormulaType::BITVECTOR: + case FormulaType::TRUE: + case FormulaType::VARCOMPARE: + case FormulaType::VARASSIGN: { + if (negated) + return f.negated(); + else + return f; + } + case FormulaType::EXISTS: + case FormulaType::FORALL: { + Quantifier q = ((f.type() == FormulaType::EXISTS) ^ negated) ? Quantifier::EXISTS : Quantifier::FORALL; + Formula sub = f.quantified_formula(); + for (auto v : f.quantified_variables()) { + if (used_vars.contains(v)) { + auto new_v = fresh_variable(v.type()); + std::stringstream ss; ss << v.name() << "_" << new_v.id(); + VariablePool::getInstance().set_name(new_v, ss.str()); + sub = substitute(sub, v, Poly(new_v)); + v = new_v; + } else { + used_vars.insert(v); + } + prefix.push_back(std::make_pair(q, v)); + } + return to_pnf(sub, prefix, used_vars, negated); + } + case FormulaType::IMPLIES: + if (negated) { + return Formula(FormulaType::AND, {to_pnf(f.premise(), prefix, used_vars, false), to_pnf(f.conclusion(), prefix, used_vars, true)}); + } else { + return Formula(FormulaType::IMPLIES, {to_pnf(f.premise(), prefix, used_vars, false), to_pnf(f.conclusion(), prefix, used_vars, false)}); + } + case FormulaType::ITE: + return Formula(FormulaType::ITE, {to_pnf(f.condition(), prefix, used_vars, negated), to_pnf(f.first_case(), prefix, used_vars, negated), to_pnf(f.second_case(), prefix, used_vars, negated)}); + case FormulaType::NOT: + return to_pnf(f.subformula(), prefix, used_vars, !negated); + default: + assert(false); + return Formula(FormulaType::FALSE); + } +} + +template +void free_variables(const Formula& f, boost::container::flat_set& current_quantified_vars, boost::container::flat_set& free_vars) { + switch (f.type()) { + case FormulaType::AND: + case FormulaType::IFF: + case FormulaType::OR: + case FormulaType::XOR: { + for (auto& sub : f.subformulas()) { + free_variables(sub, current_quantified_vars, free_vars); + } + break; + } + case FormulaType::BOOL: + case FormulaType::CONSTRAINT: + case FormulaType::VARCOMPARE: + case FormulaType::UEQ: + case FormulaType::BITVECTOR:{ + for (auto v : variables(f)) { + if (!current_quantified_vars.contains(v)) { + free_vars.insert(v); + } + } + break; + } + case FormulaType::VARASSIGN: { + assert(false); + break; + } + case FormulaType::EXISTS: + case FormulaType::FORALL: { + auto old = current_quantified_vars; + current_quantified_vars.insert(f.quantified_variables().begin(), f.quantified_variables().end()); + free_variables(f.quantified_formula(), current_quantified_vars, free_vars); + current_quantified_vars = old; + break; + } + case FormulaType::IMPLIES: + free_variables(f.premise(), current_quantified_vars, free_vars); + free_variables(f.conclusion(), current_quantified_vars, free_vars); + break; + case FormulaType::ITE: + free_variables(f.condition(), current_quantified_vars, free_vars); + free_variables(f.first_case(), current_quantified_vars, free_vars); + free_variables(f.second_case(), current_quantified_vars, free_vars); + break; + case FormulaType::NOT: + free_variables(f.subformula(), current_quantified_vars, free_vars); + break; + case FormulaType::FALSE: + case FormulaType::TRUE: { + break; + } + default: + assert(false); + } +} + +template +auto free_variables(const Formula& f) { + boost::container::flat_set current_quantified_vars; + boost::container::flat_set free_vars; + free_variables(f, current_quantified_vars, free_vars); + return free_vars; +} + +/** + * Transforms this formula to its equivalent in prenex normal form. + * @param negated Used for internal recursion. + * @return A pair of the prefix and the matrix. + */ +template +std::pair> to_pnf(const Formula& f) { + QuantifierPrefix p; + boost::container::flat_set used_vars = free_variables(f); + auto m = to_pnf(f, p, used_vars, false); + return std::make_pair(p, m); +} + +template +inline Formula to_formula(const QuantifierPrefix& prefix, const Formula& matrix) { + Formula res = matrix; + for (auto p = prefix.rbegin(); p != prefix.rend(); p++) { + assert(p->first != Quantifier::FREE); + res = Formula(p->first == Quantifier::EXISTS ? FormulaType::EXISTS : FormulaType::FORALL, std::vector({p->second}), res); + } + return res; +} + +} // namespace carl \ No newline at end of file diff --git a/src/carl-formula/formula/functions/QF.h b/src/carl-formula/formula/functions/QF.h deleted file mode 100644 index bc3d3135..00000000 --- a/src/carl-formula/formula/functions/QF.h +++ /dev/null @@ -1,107 +0,0 @@ -#pragma once - -#include "../Formula.h" -#include "Substitution.h" -#include "aux.h" - -namespace carl { - -// not transformed yet; was a member of Formula - -/** - * Transforms this formula to its quantifier free equivalent. - * The quantifiers are represented by the parameter variables. Each entry in variables contains all variables between two quantifier alternations. - * The even entries (starting with 0) are quantified existentially, the odd entries are quantified universally. - * @param variables Contains the quantified variables. - * @param level Used for internal recursion. - * @param negated Used for internal recursion. - * @return The quantifier-free version of this formula. - */ -template -Formula toQF(std::vector& variables, unsigned level = 0, bool negated = false) { - switch (type()) { - case FormulaType::AND: - case FormulaType::IFF: - case FormulaType::OR: - case FormulaType::XOR: - { - if (!negated) { - Formulas subs; - for (auto& sub: subformulas()) { - subs.push_back(sub.toQF(variables, level, false)); - } - return Formula( type(), std::move(subs) ); - } else if (type() == FormulaType::AND || type() == FormulaType::OR) { - Formulas subs; - for (auto& sub: subformulas()) { - subs.push_back(sub.toQF(variables, level, true)); - } - if (type() == FormulaType::AND) return Formula(FormulaType::OR, std::move(subs)); - else return Formula(FormulaType::AND, std::move(subs)); - } else if (type() == FormulaType::IFF) { - Formulas sub1; - Formulas sub2; - for (auto& sub: subformulas()) { - sub1.push_back(sub.toQF(variables, level, true)); - sub2.push_back(sub.toQF(variables, level, false)); - } - return Formula(FormulaType::AND, {Formula(FormulaType::OR, std::move(sub1)), Formula(FormulaType::OR, std::move(sub2))}); - } else if (type() == FormulaType::XOR) { - auto lhs = back().toQF(variables, level, false); - auto rhs = connectPrecedingSubformulas().toQF(variables, level, true); - return Formula(FormulaType::IFF, {lhs, rhs}); - } - assert(false); - } - case FormulaType::BOOL: - case FormulaType::CONSTRAINT: - case FormulaType::FALSE: - case FormulaType::UEQ: - case FormulaType::BITVECTOR: - case FormulaType::TRUE: - case FormulaType::VARCOMPARE: - case FormulaType::VARASSIGN: - { - if (negated) return Formula( NOT, *this ); - else return *this; - } - case FormulaType::EXISTS: - case FormulaType::FORALL: - { - unsigned cur = 0; - if ((level % 2 == (type() == FormulaType::EXISTS ? (unsigned)0 : (unsigned)1)) ^ negated) cur = level; - else cur = level+1; - Variables vars(quantified_variables().begin(), quantified_variables().end()); - Formula f = quantified_formula(); - for (auto it = vars.begin(); it != vars.end();) { - if (it->type() == VariableType::VT_BOOL) { - // Just leave boolean variables at the base level up to the SAT solver. - if (cur > 0) { - f = Formula( - (type() == FormulaType::EXISTS ? FormulaType::OR : FormulaType::AND), - {carl::substitute(f,*it, Formula( FormulaType::TRUE )), - carl::substitute(f, *it, Formula( FormulaType::FALSE ))} - ); - } - it = vars.erase(it); - } - else it++; - } - if (vars.size() > 0) { - while (variables.size() <= cur) variables.emplace_back(); - variables[cur].insert(vars.begin(), vars.end()); - } - return f.toQF(variables, cur, negated); - } - case FormulaType::IMPLIES: - if (negated) return Formula(FormulaType::AND, {premise().toQF(variables, level, false), conclusion().toQF(variables, level, true)}); - else return Formula( FormulaType::IMPLIES, {premise().toQF(variables, level, false), conclusion().toQF(variables, level, false)}); - case FormulaType::ITE: - return Formula( FormulaType::ITE, {condition().toQF(variables, level, negated), first_case().toQF(variables, level, negated), second_case().toQF(variables, level, negated)}); - case FormulaType::NOT: - return subformula().toQF(variables, level, !negated); - } - return Formula( FormulaType::TRUE ); -} - -} \ No newline at end of file diff --git a/src/tests/carl-formula/Test_PNF.cpp b/src/tests/carl-formula/Test_PNF.cpp new file mode 100644 index 00000000..fc741f9f --- /dev/null +++ b/src/tests/carl-formula/Test_PNF.cpp @@ -0,0 +1,59 @@ + +#include +#include +#include + +#include "../Common.h" + +using namespace carl; + +typedef MultivariatePolynomial Poly; +typedef Constraint ConstraintT; +typedef Formula FormulaT; + +TEST(PNF, testNegation) { + // Example: not (forall x. exists y. x - y > 0) -> exists x. forall y. x - y <= 0 + auto x = carl::fresh_real_variable("x"); + auto y = carl::fresh_real_variable("y"); + auto formula = FormulaT(carl::FormulaType::NOT, FormulaT(carl::FormulaType::FORALL, std::vector({x}), FormulaT(carl::FormulaType::EXISTS, std::vector({y}), FormulaT(Poly(x) - Poly(y), carl::Relation::GREATER)))); + auto prenexed = FormulaT(carl::FormulaType::EXISTS, std::vector({x}), FormulaT(carl::FormulaType::FORALL, std::vector({y}), FormulaT(Poly(x) - Poly(y), carl::Relation::LEQ))); + + auto [quantifiers, matrix] = carl::to_pnf(formula); + auto prenex = to_formula(quantifiers, matrix); + + std::cout << "Formula: " << formula << std::endl; + std::cout << "Prenexed: " << prenex << std::endl; + + EXPECT_EQ(prenexed, prenex); +} + +TEST(PNF, testAndOr) { + // Example: (forall x. x > 0) and (exists x. x < 0) -> (forall x. x > 0) and (exists y. y < 0) with y != x + auto x = carl::fresh_real_variable("x"); + auto formula = FormulaT(carl::FormulaType::AND, {FormulaT(carl::FormulaType::FORALL, std::vector({x}), FormulaT(Poly(x), carl::Relation::GREATER)), FormulaT(carl::FormulaType::EXISTS, std::vector({x}), FormulaT(Poly(x), carl::Relation::LESS))}); + + auto [quantifiers, matrix] = carl::to_pnf(formula); + auto prenex = to_formula(quantifiers, matrix); + + std::cout << "Formula: " << formula << std::endl; + std::cout << "Prenexed: " << prenex << std::endl; + + EXPECT_EQ(formula.variables().size(), 1); + EXPECT_EQ(prenex.variables().size(), 2); +} + + +TEST(PNF, testImplication){ + // Example: (forall x. x - 1 > 0) => (exists x. x < 0) + auto x = carl::fresh_real_variable("x"); + auto formula = FormulaT(carl::FormulaType::IMPLIES, {FormulaT(carl::FormulaType::FORALL, std::vector({x}), FormulaT(Poly(x)-Poly(1), carl::Relation::GREATER)), FormulaT(carl::FormulaType::EXISTS, std::vector({x}), FormulaT(Poly(x), carl::Relation::LESS))}); + + auto [quantifiers, matrix] = carl::to_pnf(formula); + auto prenex = to_formula(quantifiers, matrix); + + std::cout << "Formula: " << formula << std::endl; + std::cout << "Prenexed: " << prenex << std::endl; + + EXPECT_EQ(formula.variables().size(), 1); + EXPECT_EQ(prenex.variables().size(), 2); +} \ No newline at end of file From 9e9682c9c780737faa4744bd4adca65605c64b66 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 1 Dec 2023 14:32:56 +0100 Subject: [PATCH 27/37] bugfix --- src/carl-formula/formula/functions/PNF.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/carl-formula/formula/functions/PNF.h b/src/carl-formula/formula/functions/PNF.h index 9cfdff97..b138f2fe 100644 --- a/src/carl-formula/formula/functions/PNF.h +++ b/src/carl-formula/formula/functions/PNF.h @@ -43,7 +43,7 @@ Formula to_pnf(const Formula& f, QuantifierPrefix& prefix, boost::co } else if (f.type() == FormulaType::AND || f.type() == FormulaType::OR) { Formulas subs; for (auto& sub : f.subformulas()) { - subs.push_back(to_pnf(sub, prefix, used_vars, false)); + subs.push_back(to_pnf(sub, prefix, used_vars, true)); } if (f.type() == FormulaType::AND) { return Formula(FormulaType::OR, std::move(subs)); @@ -187,6 +187,7 @@ std::pair> to_pnf(const Formula& f) { QuantifierPrefix p; boost::container::flat_set used_vars = free_variables(f); auto m = to_pnf(f, p, used_vars, false); + assert(!p.empty() || f == m); return std::make_pair(p, m); } From 8715d16e81efedda7f2b07b4f14b89c58efaa646 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 1 Dec 2023 14:59:57 +0100 Subject: [PATCH 28/37] fix --- src/carl-formula/formula/functions/PNF.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/carl-formula/formula/functions/PNF.h b/src/carl-formula/formula/functions/PNF.h index b138f2fe..96fe087a 100644 --- a/src/carl-formula/formula/functions/PNF.h +++ b/src/carl-formula/formula/functions/PNF.h @@ -187,7 +187,6 @@ std::pair> to_pnf(const Formula& f) { QuantifierPrefix p; boost::container::flat_set used_vars = free_variables(f); auto m = to_pnf(f, p, used_vars, false); - assert(!p.empty() || f == m); return std::make_pair(p, m); } From 663b3c919cebfa0820958aab7de5111b97ce499d Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 1 Dec 2023 15:25:04 +0100 Subject: [PATCH 29/37] add conditions --- src/carl-formula/formula/Condition.h | 10 +++++++--- src/carl-formula/formula/Formula.tpp | 24 ++++++++++++++++++++---- 2 files changed, 27 insertions(+), 7 deletions(-) diff --git a/src/carl-formula/formula/Condition.h b/src/carl-formula/formula/Condition.h index 2075b2b8..4a4b42d7 100644 --- a/src/carl-formula/formula/Condition.h +++ b/src/carl-formula/formula/Condition.h @@ -56,8 +56,10 @@ namespace carl { static constexpr Condition PROP_IS_A_LITERAL = Condition( 4 ); static constexpr Condition PROP_IS_AN_ATOM = Condition( 5 ); static constexpr Condition PROP_IS_LITERAL_CONJUNCTION = Condition( 6 ); + static constexpr Condition PROP_IS_IN_PNF = Condition( 7 ); static const Condition STRONG_CONDITIONS = PROP_IS_IN_NNF | PROP_IS_IN_CNF | PROP_IS_PURE_CONJUNCTION | - PROP_IS_A_CLAUSE | PROP_IS_A_LITERAL | PROP_IS_AN_ATOM | PROP_IS_LITERAL_CONJUNCTION; + PROP_IS_A_CLAUSE | PROP_IS_A_LITERAL | PROP_IS_AN_ATOM | PROP_IS_LITERAL_CONJUNCTION | + PROP_IS_IN_PNF; //Propositions which hold, if they hold in at least one sub formula (16-63) static constexpr Condition PROP_CONTAINS_EQUATION = Condition( 16 ); @@ -76,13 +78,15 @@ namespace carl { static constexpr Condition PROP_VARIABLE_DEGREE_GREATER_THAN_THREE = Condition( 29 ); static constexpr Condition PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR = Condition( 30 ); static constexpr Condition PROP_CONTAINS_WEAK_INEQUALITY = Condition( 31 ); - static constexpr Condition PROP_CONTAINS_QUANTIFIER = Condition( 32 ); + static constexpr Condition PROP_CONTAINS_QUANTIFIER_EXISTS = Condition( 32 ); + static constexpr Condition PROP_CONTAINS_QUANTIFIER_FORALL = Condition( 33 ); + static const Condition WEAK_CONDITIONS = PROP_CONTAINS_EQUATION | PROP_CONTAINS_INEQUALITY | PROP_CONTAINS_STRICT_INEQUALITY | PROP_CONTAINS_LINEAR_POLYNOMIAL | PROP_CONTAINS_LINEAR_POLYNOMIAL | PROP_CONTAINS_NONLINEAR_POLYNOMIAL | PROP_CONTAINS_MULTIVARIATE_POLYNOMIAL | PROP_CONTAINS_INEQUALITY | PROP_CONTAINS_BOOLEAN | PROP_CONTAINS_REAL_VALUED_VARS | PROP_CONTAINS_INTEGER_VALUED_VARS | PROP_CONTAINS_UNINTERPRETED_EQUATIONS | PROP_CONTAINS_BITVECTOR | PROP_CONTAINS_PSEUDOBOOLEAN - | PROP_VARIABLE_DEGREE_GREATER_THAN_TWO | PROP_VARIABLE_DEGREE_GREATER_THAN_THREE | PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR | PROP_CONTAINS_QUANTIFIER; + | PROP_VARIABLE_DEGREE_GREATER_THAN_TWO | PROP_VARIABLE_DEGREE_GREATER_THAN_THREE | PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR | PROP_CONTAINS_QUANTIFIER_EXISTS | PROP_CONTAINS_QUANTIFIER_FORALL; } // namespace carl diff --git a/src/carl-formula/formula/Formula.tpp b/src/carl-formula/formula/Formula.tpp index 1c3a60c1..299eed2f 100644 --- a/src/carl-formula/formula/Formula.tpp +++ b/src/carl-formula/formula/Formula.tpp @@ -23,11 +23,19 @@ namespace carl switch( _content.mType ) { case FormulaType::EXISTS: + { + _content.mProperties |= PROP_CONTAINS_QUANTIFIER_EXISTS; + auto subFormula = std::get>(_content.mContent).mFormula; + _content.mProperties |= (subFormula.properties() & WEAK_CONDITIONS); + _content.mProperties |= (subFormula.properties() & PROP_IS_IN_PNF); + break; + } case FormulaType::FORALL: { - _content.mProperties |= PROP_CONTAINS_QUANTIFIER; + _content.mProperties |= PROP_CONTAINS_QUANTIFIER_FORALL; auto subFormula = std::get>(_content.mContent).mFormula; _content.mProperties |= (subFormula.properties() & WEAK_CONDITIONS); + _content.mProperties |= (subFormula.properties() & PROP_IS_IN_PNF); break; } case FormulaType::TRUE: @@ -53,11 +61,13 @@ namespace carl if( PROP_IS_AN_ATOM <= subFormulaConds ) _content.mProperties |= PROP_IS_A_CLAUSE | PROP_IS_A_LITERAL | PROP_IS_IN_CNF | PROP_IS_LITERAL_CONJUNCTION; _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS); + if (!(PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds) && !(PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds)) + _content.mProperties |= PROP_IS_IN_PNF; break; } case FormulaType::OR: { - _content.mProperties |= PROP_IS_A_CLAUSE | PROP_IS_IN_CNF | PROP_IS_IN_NNF; + _content.mProperties |= PROP_IS_A_CLAUSE | PROP_IS_IN_CNF | PROP_IS_IN_NNF | PROP_IS_IN_PNF; for (auto subFormula = std::get>(_content.mContent).begin(); subFormula != std::get>(_content.mContent).end(); ++subFormula) { Condition subFormulaConds = subFormula->properties(); @@ -69,12 +79,14 @@ namespace carl if( !(PROP_IS_IN_NNF<=subFormulaConds) ) _content.mProperties &= ~PROP_IS_IN_NNF; _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS); + if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds) + _content.mProperties &= ~PROP_IS_IN_PNF; } break; } case FormulaType::AND: { - _content.mProperties |= PROP_IS_LITERAL_CONJUNCTION | PROP_IS_PURE_CONJUNCTION | PROP_IS_IN_CNF | PROP_IS_IN_NNF; + _content.mProperties |= PROP_IS_LITERAL_CONJUNCTION | PROP_IS_PURE_CONJUNCTION | PROP_IS_IN_CNF | PROP_IS_IN_NNF | PROP_IS_IN_PNF; for (auto subFormula = std::get>(_content.mContent).begin(); subFormula != std::get>(_content.mContent).end(); ++subFormula) { Condition subFormulaConds = subFormula->properties(); @@ -94,6 +106,8 @@ namespace carl if( !(PROP_IS_IN_NNF<=subFormulaConds) ) _content.mProperties &= ~PROP_IS_IN_NNF; _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS); + if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds) + _content.mProperties &= ~PROP_IS_IN_PNF; } break; } @@ -102,13 +116,15 @@ namespace carl case FormulaType::IFF: case FormulaType::XOR: { - _content.mProperties |= PROP_IS_IN_NNF; + _content.mProperties |= PROP_IS_IN_NNF | PROP_IS_IN_PNF; for (auto subFormula = std::get>(_content.mContent).begin(); subFormula != std::get>(_content.mContent).end(); ++subFormula) { Condition subFormulaConds = subFormula->properties(); if( !(PROP_IS_IN_NNF<=subFormulaConds) ) _content.mProperties &= ~PROP_IS_IN_NNF; _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS); + if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds) + _content.mProperties &= ~PROP_IS_IN_PNF; } break; } From ee9275c091a86bd3ffe987e37d284fd2733c1d2f Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Fri, 15 Dec 2023 10:10:41 +0100 Subject: [PATCH 30/37] fix serialization bug --- src/carl-statistics/MultiCounter.h | 2 +- src/carl-statistics/Statistics.h | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/carl-statistics/MultiCounter.h b/src/carl-statistics/MultiCounter.h index b49d5291..fc9e365b 100644 --- a/src/carl-statistics/MultiCounter.h +++ b/src/carl-statistics/MultiCounter.h @@ -17,7 +17,7 @@ class MultiCounter { std::stringstream ss; for (const auto& [k,v] : m_data) { serialize(ss, k); - ss << ":" << v << ";"; + ss << "=" << v << ";"; } data.emplace(key, ss.str()); } diff --git a/src/carl-statistics/Statistics.h b/src/carl-statistics/Statistics.h index 6202c62b..04be9ef0 100644 --- a/src/carl-statistics/Statistics.h +++ b/src/carl-statistics/Statistics.h @@ -20,14 +20,14 @@ class Statistics { std::map mCollected; bool has_illegal_chars(const std::string& val) const { return std::find_if(val.begin(), val.end(), [](char c) { - return c == '(' || c == ')' || std::isspace(static_cast(c)); + return c == ':' || c == '(' || c == ')' || std::isspace(static_cast(c)); }) != val.end(); } protected: void addKeyValuePair(const std::string& key, const std::string& value) { - assert(!has_illegal_chars(key) && "spaces, (, ) are not allowed here"); + assert(!has_illegal_chars(key) && "spaces, (, ), : are not allowed here"); if (has_illegal_chars(key)) return; - assert(!has_illegal_chars(static_cast(value)) && "spaces, (, ) are not allowed here"); + assert(!has_illegal_chars(static_cast(value)) && "spaces, (, ), : are not allowed here"); if (has_illegal_chars(value)) return; mCollected.emplace(key, value); } From 826e1e2775e028b5fc4b2ef5a676b36a3c0a6646 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Thu, 21 Dec 2023 13:35:01 +0100 Subject: [PATCH 31/37] comment out lp_polynomial_set_external --- src/carl-arith/poly/libpoly/LPPolynomial.cpp | 22 ++++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/carl-arith/poly/libpoly/LPPolynomial.cpp b/src/carl-arith/poly/libpoly/LPPolynomial.cpp index 371ac5bc..55c92335 100644 --- a/src/carl-arith/poly/libpoly/LPPolynomial.cpp +++ b/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,7 +54,7 @@ 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())); } @@ -62,7 +62,7 @@ LPPolynomial::LPPolynomial(const LPContext& context, long val) 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,7 +74,7 @@ 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())); } @@ -82,7 +82,7 @@ LPPolynomial::LPPolynomial(const LPContext& context, const Variable& var, const 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& 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&& 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& 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 { From 5ed47a6739a4bd8a323659b05ebcf67acb72a35c Mon Sep 17 00:00:00 2001 From: Philip Kroll Date: Mon, 15 Jan 2024 08:46:46 +0100 Subject: [PATCH 32/37] Resolve "CMAKE unable to install GMP automatically" --- cmake/FindPoly.cmake | 9 +++++++-- resources/gmp.cmake | 26 ++++++++++++++++++-------- src/tests/pycarl/CMakeLists.txt | 4 ++-- 3 files changed, 27 insertions(+), 12 deletions(-) diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake index 8048e767..7fd4b012 100644 --- a/cmake/FindPoly.cmake +++ b/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} 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 /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 diff --git a/resources/gmp.cmake b/resources/gmp.cmake index b5ea811a..357d849d 100644 --- a/resources/gmp.cmake +++ b/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= + GMP-EP + URL https://ftp.gnu.org/gnu/gmp/gmp-${GMP_VERSION}.tar.bz2 + URL_HASH SHA1=db38c7b67f8eea9f2e5b8a48d219165b2fdab11f + CONFIGURE_COMMAND ${CONFIGURE_ENV} /configure --prefix= --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) + + diff --git a/src/tests/pycarl/CMakeLists.txt b/src/tests/pycarl/CMakeLists.txt index 38268783..61b36489 100644 --- a/src/tests/pycarl/CMakeLists.txt +++ b/src/tests/pycarl/CMakeLists.txt @@ -1,6 +1,6 @@ -find_package(PythonInterp) +find_package(Python COMPONENTS Interpreter) -if (PYTHONINTERP_FOUND) +if (Python_Interpreter_FOUND) add_test( NAME pycarl COMMAND ${PYTHON_EXECUTABLE} ${CMAKE_SOURCE_DIR}/src/tests/pycarl/runAllTests.py) else() message(WARNING "Did not find a python interpreter, disabling pycarl tests.") From 4829b6bed060bec9c225d552738fd323e7491e54 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Mon, 15 Jan 2024 08:58:28 +0100 Subject: [PATCH 33/37] Serialization in carl-statistics --- src/carl-statistics/Serialization.h | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/carl-statistics/Serialization.h b/src/carl-statistics/Serialization.h index 474ca912..f69ebfff 100644 --- a/src/carl-statistics/Serialization.h +++ b/src/carl-statistics/Serialization.h @@ -1,12 +1,24 @@ #pragma once +#include + namespace carl::statistics { template -void serialize(std::stringstream& ss, const std::pair& pair) { +inline void serialize(std::stringstream& ss, const std::pair& pair) { ss << "[" << pair.first << "," << pair.second << "]"; } +template +inline void serialize(std::stringstream& ss, const std::vector& v) { + ss << carl::stream_joined(";", v); +} + +template +inline void serialize(std::stringstream& ss, const std::map& m) { + return ss << stream_joined(";", m, [](auto& o, const auto& p){ o << p.first << "=" << p.second; }); +} + template void serialize(std::stringstream& ss, const T& v) { ss << v; From 6faee117dae3f832b33767a677e20cf148cb9f96 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Mon, 22 Jan 2024 13:58:35 +0100 Subject: [PATCH 34/37] minor updates to carl --- src/carl-arith/extended/VariableComparison.h | 4 ++++ src/carl-formula/formula/functions/NNF.h | 2 +- src/carl-formula/formula/functions/Negations.h | 11 +++++++++-- src/carl-io/SMTLIBStream.h | 2 +- 4 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/carl-arith/extended/VariableComparison.h b/src/carl-arith/extended/VariableComparison.h index fb3c0abd..f9540861 100644 --- a/src/carl-arith/extended/VariableComparison.h +++ b/src/carl-arith/extended/VariableComparison.h @@ -80,6 +80,10 @@ 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; + } }; /** diff --git a/src/carl-formula/formula/functions/NNF.h b/src/carl-formula/formula/functions/NNF.h index 20f829ac..ad70382f 100644 --- a/src/carl-formula/formula/functions/NNF.h +++ b/src/carl-formula/formula/functions/NNF.h @@ -14,7 +14,7 @@ Formula to_nnf(const Formula& formula) { return formula; } if(formula.is_literal()){ - return resolve_negation(formula, false); + return resolve_negation(formula, false, true); } switch(formula.type()){ diff --git a/src/carl-formula/formula/functions/Negations.h b/src/carl-formula/formula/functions/Negations.h index ca7609d9..860c8425 100644 --- a/src/carl-formula/formula/functions/Negations.h +++ b/src/carl-formula/formula/functions/Negations.h @@ -9,7 +9,10 @@ namespace carl { * the negation. */ template -Formula resolve_negation( const Formula& f, bool _keepConstraint = true ) { +Formula resolve_negation( const Formula& f, bool _keepConstraint = true, bool resolve_varcomp = false) { + if (resolve_varcomp && f.type() == FormulaType::VARCOMPARE && f.variable_comparison().negated()) { + return Formula(f.variable_comparison().resolve_negation()); + } if( f.type() != FormulaType::NOT ) return f; FormulaType newType = f.type(); switch( f.subformula().type() ) @@ -67,7 +70,11 @@ Formula resolve_negation( const Formula& f, bool _keepConstraint = tru } } case FormulaType::VARCOMPARE: { - return Formula(f.subformula().variable_comparison().negation()); + if (resolve_varcomp) { + return Formula(f.subformula().variable_comparison().invert_relation()); + } else { + return Formula(f.subformula().variable_comparison().negation()); + } } case FormulaType::VARASSIGN: { assert(false); diff --git a/src/carl-io/SMTLIBStream.h b/src/carl-io/SMTLIBStream.h index 0eb676e0..3f7d7b1c 100644 --- a/src/carl-io/SMTLIBStream.h +++ b/src/carl-io/SMTLIBStream.h @@ -26,7 +26,7 @@ namespace carl::io { * Allows to print carl data structures in SMTLIB syntax. */ class SMTLIBStream { -private: +public: std::stringstream mStream; void write(const mpz_class& n) { *this << carl::toString(n, false); } From bef608b6998d58fc0a388c0bcd1f7d2f5327b853 Mon Sep 17 00:00:00 2001 From: Jasper Nalbach Date: Mon, 22 Jan 2024 14:02:51 +0100 Subject: [PATCH 35/37] revert change in SMTLIBStream --- src/carl-io/SMTLIBStream.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/carl-io/SMTLIBStream.h b/src/carl-io/SMTLIBStream.h index 3f7d7b1c..0eb676e0 100644 --- a/src/carl-io/SMTLIBStream.h +++ b/src/carl-io/SMTLIBStream.h @@ -26,7 +26,7 @@ namespace carl::io { * Allows to print carl data structures in SMTLIB syntax. */ class SMTLIBStream { -public: +private: std::stringstream mStream; void write(const mpz_class& n) { *this << carl::toString(n, false); } From 8dbf3554cb0647d2f22314cb7c219804ac4a27f6 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Thu, 1 Feb 2024 09:34:51 +0100 Subject: [PATCH 36/37] disable pycarl --- src/tests/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tests/CMakeLists.txt b/src/tests/CMakeLists.txt index 7081b368..3bdf50f4 100644 --- a/src/tests/CMakeLists.txt +++ b/src/tests/CMakeLists.txt @@ -25,7 +25,7 @@ add_subdirectory(carl-arith-interval) add_subdirectory(carl-arith-intervalcontraction) add_subdirectory(carl-formula) add_subdirectory(benchmarks) -add_subdirectory(pycarl) +# add_subdirectory(pycarl) # Only for debugging. #add_subdirectory(debug) From 45bb8096b34292f088e1b041a64f92f76d05d9c1 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Thu, 1 Feb 2024 13:49:57 +0100 Subject: [PATCH 37/37] update version --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a7ce4fc1..06a573a5 100644 --- a/CMakeLists.txt +++ b/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}") # # # # # # # # # # # # # # # # # # # # # #