Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/poly_util.cpp	Lines:	74	163	45.4 %
Date:	2021-05-22	Branches:	62	364	17.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Utilities for working with LibPoly.
 */

#include "poly_util.h"

#ifdef CVC5_POLY_IMP

#include <poly/polyxx.h>

#include <map>
#include <sstream>

#include "base/check.h"
#include "maybe.h"
#include "util/integer.h"
#include "util/rational.h"
#include "util/real_algebraic_number.h"

namespace cvc5 {
namespace poly_utils {

namespace {
/**
 * Convert arbitrary data using a string as intermediary.
 * Assumes the existence of operator<<(std::ostream&, const From&) and To(const
 * std::string&); should be the last resort for type conversions: it may not
 * only yield bad performance, but is also dependent on compatible string
 * representations. Use with care!
 */
template <typename To, typename From>
To cast_by_string(const From& f)
{
  std::stringstream s;
  s << f;
  return To(s.str());
}
}  // namespace

Integer toInteger(const poly::Integer& i)
{
  const mpz_class& gi = *poly::detail::cast_to_gmp(&i);
#ifdef CVC5_GMP_IMP
  return Integer(gi);
#endif
#ifdef CVC5_CLN_IMP
  if (std::numeric_limits<long>::min() <= gi
      && gi <= std::numeric_limits<long>::max())
  {
    return Integer(gi.get_si());
  }
  else
  {
    return cast_by_string<Integer, poly::Integer>(i);
  }
#endif
}
Rational toRational(const poly::Integer& i) { return Rational(toInteger(i)); }
Rational toRational(const poly::Rational& r)
{
#ifdef CVC5_GMP_IMP
  return Rational(*poly::detail::cast_to_gmp(&r));
#endif
#ifdef CVC5_CLN_IMP
  return Rational(toInteger(numerator(r)), toInteger(denominator(r)));
#endif
}
Rational toRational(const poly::DyadicRational& dr)
{
  return Rational(toInteger(numerator(dr)), toInteger(denominator(dr)));
}
Rational toRationalAbove(const poly::Value& v)
{
  if (is_algebraic_number(v))
  {
    return toRational(get_upper_bound(as_algebraic_number(v)));
  }
  else if (is_dyadic_rational(v))
  {
    return toRational(as_dyadic_rational(v));
  }
  else if (is_integer(v))
  {
    return toRational(as_integer(v));
  }
  else if (is_rational(v))
  {
    return toRational(as_rational(v));
  }
  Assert(false) << "Can not convert " << v << " to rational.";
  return Rational();
}
Rational toRationalBelow(const poly::Value& v)
{
  if (is_algebraic_number(v))
  {
    return toRational(get_lower_bound(as_algebraic_number(v)));
  }
  else if (is_dyadic_rational(v))
  {
    return toRational(as_dyadic_rational(v));
  }
  else if (is_integer(v))
  {
    return toRational(as_integer(v));
  }
  else if (is_rational(v))
  {
    return toRational(as_rational(v));
  }
  Assert(false) << "Can not convert " << v << " to rational.";
  return Rational();
}

poly::Integer toInteger(const Integer& i)
{
#ifdef CVC5_GMP_IMP
  return poly::Integer(i.getValue());
#endif
#ifdef CVC5_CLN_IMP
  if (std::numeric_limits<long>::min() <= i.getValue()
      && i.getValue() <= std::numeric_limits<long>::max())
  {
    return poly::Integer(cln::cl_I_to_long(i.getValue()));
  }
  else
  {
    return poly::Integer(cast_by_string<mpz_class, Integer>(i));
  }
#endif
}
std::vector<poly::Integer> toInteger(const std::vector<Integer>& vi)
{
  std::vector<poly::Integer> res;
  for (const auto& i : vi) res.emplace_back(toInteger(i));
  return res;
}
poly::Rational toRational(const Rational& r)
{
#ifdef CVC5_GMP_IMP
  return poly::Rational(r.getValue());
#endif
#ifdef CVC5_CLN_IMP
  return poly::Rational(toInteger(r.getNumerator()),
                        toInteger(r.getDenominator()));
#endif
}

Maybe<poly::DyadicRational> toDyadicRational(const Rational& r)
{
  Integer den = r.getDenominator();
  if (den.isOne())
  {  // It's an integer anyway.
    return poly::DyadicRational(toInteger(r.getNumerator()));
  }
  unsigned long exp = den.isPow2();
  if (exp > 0)
  {
    // It's a dyadic rational.
    return div_2exp(poly::DyadicRational(toInteger(r.getNumerator())), exp - 1);
  }
  return Maybe<poly::DyadicRational>();
}

Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
{
  poly::Integer den = denominator(r);
  if (den == poly::Integer(1))
  {  // It's an integer anyway.
    return poly::DyadicRational(numerator(r));
  }
  // Use bit_size as an estimate for the dyadic exponent.
  unsigned long size = bit_size(den) - 1;
  if (mul_pow2(poly::Integer(1), size) == den)
  {
    // It's a dyadic rational.
    return div_2exp(poly::DyadicRational(numerator(r)), size);
  }
  return Maybe<poly::DyadicRational>();
}

poly::Rational approximateToDyadic(const poly::Rational& r,
                                   const poly::Rational& original)
{
  // Multiply both numerator and denominator by two.
  // Increase or decrease the numerator, depending on whether r is too small or
  // too large.
  poly::Integer n = mul_pow2(numerator(r), 1);
  if (r < original)
  {
    ++n;
  }
  else if (r > original)
  {
    --n;
  }
  return poly::Rational(n, mul_pow2(denominator(r), 1));
}

poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p,
                                              const Rational& lower,
                                              const Rational& upper)
{
  Maybe<poly::DyadicRational> ml = toDyadicRational(lower);
  Maybe<poly::DyadicRational> mu = toDyadicRational(upper);
  if (ml && mu)
  {
    return poly::AlgebraicNumber(std::move(p),
                                 poly::DyadicInterval(ml.value(), mu.value()));
  }
  // The encoded real algebraic number did not have dyadic rational endpoints.
  poly::Rational origl = toRational(lower);
  poly::Rational origu = toRational(upper);
  poly::Rational l(floor(origl));
  poly::Rational u(ceil(origu));
  poly::RationalInterval ri(l, u);
  while (count_real_roots(p, ri) != 1)
  {
    l = approximateToDyadic(l, origl);
    u = approximateToDyadic(u, origu);
    ri = poly::RationalInterval(l, u);
  }
  Assert(count_real_roots(p, poly::RationalInterval(l, u)) == 1);
  ml = toDyadicRational(l);
  mu = toDyadicRational(u);
  Assert(ml && mu) << "Both bounds should be dyadic by now.";
  return poly::AlgebraicNumber(std::move(p),
                               poly::DyadicInterval(ml.value(), mu.value()));
}

RealAlgebraicNumber toRanWithRefinement(poly::UPolynomial&& p,
                                        const Rational& lower,
                                        const Rational& upper)
{
  return RealAlgebraicNumber(
      toPolyRanWithRefinement(std::move(p), lower, upper));
}

std::size_t totalDegree(const poly::Polynomial& p)
{
  std::size_t tdeg = 0;

  lp_polynomial_traverse_f f =
      [](const lp_polynomial_context_t* ctx, lp_monomial_t* m, void* data) {
        std::size_t sum = 0;
        for (std::size_t i = 0; i < m->n; ++i)
        {
          sum += m->p[i].d;
        }

        std::size_t* td = static_cast<std::size_t*>(data);
        *td = std::max(*td, sum);
      };

  lp_polynomial_traverse(p.get_internal(), f, &tdeg);

  return tdeg;
}

std::ostream& operator<<(std::ostream& os, const VariableInformation& vi)
{
  if (vi.var == poly::Variable())
  {
    os << "Totals: ";
    os << "max deg " << vi.max_degree;
    os << ", sum term deg " << vi.sum_term_degree;
    os << ", sum poly deg " << vi.sum_poly_degree;
    os << ", num polys " << vi.num_polynomials;
    os << ", num terms " << vi.num_terms;
  }
  else
  {
    os << "Info for " << vi.var << ": ";
    os << "max deg " << vi.max_degree;
    os << ", max lc deg: " << vi.max_lc_degree;
    os << ", max term tdeg: " << vi.max_terms_tdegree;
    os << ", sum term deg " << vi.sum_term_degree;
    os << ", sum poly deg " << vi.sum_poly_degree;
    os << ", num polys " << vi.num_polynomials;
    os << ", num terms " << vi.num_terms;
  }
  return os;
}

struct GetVarInfo
{
  VariableInformation* info;
  std::size_t cur_var_degree = 0;
  std::size_t cur_lc_degree = 0;
};
void getVariableInformation(VariableInformation& vi,
                            const poly::Polynomial& poly)
{
  GetVarInfo varinfo;
  varinfo.info = &vi;
  lp_polynomial_traverse_f f =
      [](const lp_polynomial_context_t* ctx, lp_monomial_t* m, void* data) {
        GetVarInfo* gvi = static_cast<GetVarInfo*>(data);
        VariableInformation* info = gvi->info;
        // Total degree of this term
        std::size_t tdeg = 0;
        // Degree of this variable within this term
        std::size_t vardeg = 0;
        for (std::size_t i = 0; i < m->n; ++i)
        {
          tdeg += m->p[i].d;
          if (m->p[i].x == info->var)
          {
            info->max_degree = std::max(info->max_degree, m->p[i].d);
            info->sum_term_degree += m->p[i].d;
            vardeg = m->p[i].d;
          }
        }
        if (info->var == poly::Variable())
        {
          ++info->num_terms;
          info->max_degree = std::max(info->max_degree, tdeg);
          info->sum_term_degree += tdeg;
        }
        else if (vardeg > 0)
        {
          ++info->num_terms;
          if (gvi->cur_var_degree < vardeg)
          {
            gvi->cur_lc_degree = tdeg - vardeg;
          }
          info->max_terms_tdegree = std::max(info->max_terms_tdegree, tdeg);
        }
      };
  std::size_t tmp_max_degree = vi.max_degree;
  std::size_t tmp_num_terms = vi.num_terms;
  vi.max_degree = 0;
  vi.num_terms = 0;
  lp_polynomial_traverse(poly.get_internal(), f, &varinfo);
  vi.max_lc_degree = std::max(vi.max_lc_degree, varinfo.cur_lc_degree);
  if (vi.num_terms > 0)
  {
    ++vi.num_polynomials;
  }
  vi.sum_poly_degree += vi.max_degree;
  vi.max_degree = std::max(vi.max_degree, tmp_max_degree);
  vi.num_terms += tmp_num_terms;
}

}  // namespace poly_utils
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Utilities for working with LibPoly.
14		*/
15
16		#include "poly_util.h"
17
18		#ifdef CVC5_POLY_IMP
19
20		#include <poly/polyxx.h>
21
22		#include <map>
23		#include <sstream>
24
25		#include "base/check.h"
26		#include "maybe.h"
27		#include "util/integer.h"
28		#include "util/rational.h"
29		#include "util/real_algebraic_number.h"
30
31		namespace cvc5 {
32		namespace poly_utils {
33
34		namespace {
35		/**
36		* Convert arbitrary data using a string as intermediary.
37		* Assumes the existence of operator<<(std::ostream&, const From&) and To(const
38		* std::string&); should be the last resort for type conversions: it may not
39		* only yield bad performance, but is also dependent on compatible string
40		* representations. Use with care!
41		*/
42		template <typename To, typename From>
43	212	To cast_by_string(const From& f)
44		{
45	424	std::stringstream s;
46	212	s << f;
47	424	return To(s.str());
48		}
49		} // namespace
50
51	123	Integer toInteger(const poly::Integer& i)
52		{
53	123	const mpz_class& gi = *poly::detail::cast_to_gmp(&i);
54		#ifdef CVC5_GMP_IMP
55		return Integer(gi);
56		#endif
57		#ifdef CVC5_CLN_IMP
58	246	if (std::numeric_limits<long>::min() <= gi
59	123	&& gi <= std::numeric_limits<long>::max())
60		{
61	123	return Integer(gi.get_si());
62		}
63		else
64		{
65		return cast_by_string<Integer, poly::Integer>(i);
66		}
67		#endif
68		}
69	27	Rational toRational(const poly::Integer& i) { return Rational(toInteger(i)); }
70	30	Rational toRational(const poly::Rational& r)
71		{
72		#ifdef CVC5_GMP_IMP
73		return Rational(*poly::detail::cast_to_gmp(&r));
74		#endif
75		#ifdef CVC5_CLN_IMP
76	30	return Rational(toInteger(numerator(r)), toInteger(denominator(r)));
77		#endif
78		}
79	18	Rational toRational(const poly::DyadicRational& dr)
80		{
81	18	return Rational(toInteger(numerator(dr)), toInteger(denominator(dr)));
82		}
83		Rational toRationalAbove(const poly::Value& v)
84		{
85		if (is_algebraic_number(v))
86		{
87		return toRational(get_upper_bound(as_algebraic_number(v)));
88		}
89		else if (is_dyadic_rational(v))
90		{
91		return toRational(as_dyadic_rational(v));
92		}
93		else if (is_integer(v))
94		{
95		return toRational(as_integer(v));
96		}
97		else if (is_rational(v))
98		{
99		return toRational(as_rational(v));
100		}
101		Assert(false) << "Can not convert " << v << " to rational.";
102		return Rational();
103		}
104		Rational toRationalBelow(const poly::Value& v)
105		{
106		if (is_algebraic_number(v))
107		{
108		return toRational(get_lower_bound(as_algebraic_number(v)));
109		}
110		else if (is_dyadic_rational(v))
111		{
112		return toRational(as_dyadic_rational(v));
113		}
114		else if (is_integer(v))
115		{
116		return toRational(as_integer(v));
117		}
118		else if (is_rational(v))
119		{
120		return toRational(as_rational(v));
121		}
122		Assert(false) << "Can not convert " << v << " to rational.";
123		return Rational();
124		}
125
126	2064	poly::Integer toInteger(const Integer& i)
127		{
128		#ifdef CVC5_GMP_IMP
129		return poly::Integer(i.getValue());
130		#endif
131		#ifdef CVC5_CLN_IMP
132	6192	if (std::numeric_limits<long>::min() <= i.getValue()
133	6192	&& i.getValue() <= std::numeric_limits<long>::max())
134		{
135	1852	return poly::Integer(cln::cl_I_to_long(i.getValue()));
136		}
137		else
138		{
139	212	return poly::Integer(cast_by_string<mpz_class, Integer>(i));
140		}
141		#endif
142		}
143		std::vector<poly::Integer> toInteger(const std::vector<Integer>& vi)
144		{
145		std::vector<poly::Integer> res;
146		for (const auto& i : vi) res.emplace_back(toInteger(i));
147		return res;
148		}
149	94	poly::Rational toRational(const Rational& r)
150		{
151		#ifdef CVC5_GMP_IMP
152		return poly::Rational(r.getValue());
153		#endif
154		#ifdef CVC5_CLN_IMP
155	188	return poly::Rational(toInteger(r.getNumerator()),
156	282	toInteger(r.getDenominator()));
157		#endif
158		}
159
160	2	Maybe<poly::DyadicRational> toDyadicRational(const Rational& r)
161		{
162	4	Integer den = r.getDenominator();
163	2	if (den.isOne())
164		{ // It's an integer anyway.
165	2	return poly::DyadicRational(toInteger(r.getNumerator()));
166		}
167		unsigned long exp = den.isPow2();
168		if (exp > 0)
169		{
170		// It's a dyadic rational.
171		return div_2exp(poly::DyadicRational(toInteger(r.getNumerator())), exp - 1);
172		}
173		return Maybe<poly::DyadicRational>();
174		}
175
176		Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
177		{
178		poly::Integer den = denominator(r);
179		if (den == poly::Integer(1))
180		{ // It's an integer anyway.
181		return poly::DyadicRational(numerator(r));
182		}
183		// Use bit_size as an estimate for the dyadic exponent.
184		unsigned long size = bit_size(den) - 1;
185		if (mul_pow2(poly::Integer(1), size) == den)
186		{
187		// It's a dyadic rational.
188		return div_2exp(poly::DyadicRational(numerator(r)), size);
189		}
190		return Maybe<poly::DyadicRational>();
191		}
192
193		poly::Rational approximateToDyadic(const poly::Rational& r,
194		const poly::Rational& original)
195		{
196		// Multiply both numerator and denominator by two.
197		// Increase or decrease the numerator, depending on whether r is too small or
198		// too large.
199		poly::Integer n = mul_pow2(numerator(r), 1);
200		if (r < original)
201		{
202		++n;
203		}
204		else if (r > original)
205		{
206		--n;
207		}
208		return poly::Rational(n, mul_pow2(denominator(r), 1));
209		}
210
211		poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p,
212		const Rational& lower,
213		const Rational& upper)
214		{
215		Maybe<poly::DyadicRational> ml = toDyadicRational(lower);
216		Maybe<poly::DyadicRational> mu = toDyadicRational(upper);
217		if (ml && mu)
218		{
219		return poly::AlgebraicNumber(std::move(p),
220		poly::DyadicInterval(ml.value(), mu.value()));
221		}
222		// The encoded real algebraic number did not have dyadic rational endpoints.
223		poly::Rational origl = toRational(lower);
224		poly::Rational origu = toRational(upper);
225		poly::Rational l(floor(origl));
226		poly::Rational u(ceil(origu));
227		poly::RationalInterval ri(l, u);
228		while (count_real_roots(p, ri) != 1)
229		{
230		l = approximateToDyadic(l, origl);
231		u = approximateToDyadic(u, origu);
232		ri = poly::RationalInterval(l, u);
233		}
234		Assert(count_real_roots(p, poly::RationalInterval(l, u)) == 1);
235		ml = toDyadicRational(l);
236		mu = toDyadicRational(u);
237		Assert(ml && mu) << "Both bounds should be dyadic by now.";
238		return poly::AlgebraicNumber(std::move(p),
239		poly::DyadicInterval(ml.value(), mu.value()));
240		}
241
242		RealAlgebraicNumber toRanWithRefinement(poly::UPolynomial&& p,
243		const Rational& lower,
244		const Rational& upper)
245		{
246		return RealAlgebraicNumber(
247		toPolyRanWithRefinement(std::move(p), lower, upper));
248		}
249
250	72694	std::size_t totalDegree(const poly::Polynomial& p)
251		{
252	72694	std::size_t tdeg = 0;
253
254	72694	lp_polynomial_traverse_f f =
255	287772	[](const lp_polynomial_context_t* ctx, lp_monomial_t* m, void* data) {
256	143886	std::size_t sum = 0;
257	235030	for (std::size_t i = 0; i < m->n; ++i)
258		{
259	91144	sum += m->p[i].d;
260		}
261
262	143886	std::size_t* td = static_cast<std::size_t*>(data);
263	143886	td = std::max(td, sum);
264	287772	};
265
266	72694	lp_polynomial_traverse(p.get_internal(), f, &tdeg);
267
268	72694	return tdeg;
269		}
270
271		std::ostream& operator<<(std::ostream& os, const VariableInformation& vi)
272		{
273		if (vi.var == poly::Variable())
274		{
275		os << "Totals: ";
276		os << "max deg " << vi.max_degree;
277		os << ", sum term deg " << vi.sum_term_degree;
278		os << ", sum poly deg " << vi.sum_poly_degree;
279		os << ", num polys " << vi.num_polynomials;
280		os << ", num terms " << vi.num_terms;
281		}
282		else
283		{
284		os << "Info for " << vi.var << ": ";
285		os << "max deg " << vi.max_degree;
286		os << ", max lc deg: " << vi.max_lc_degree;
287		os << ", max term tdeg: " << vi.max_terms_tdegree;
288		os << ", sum term deg " << vi.sum_term_degree;
289		os << ", sum poly deg " << vi.sum_poly_degree;
290		os << ", num polys " << vi.num_polynomials;
291		os << ", num terms " << vi.num_terms;
292		}
293		return os;
294		}
295
296	1582	struct GetVarInfo
297		{
298		VariableInformation* info;
299		std::size_t cur_var_degree = 0;
300		std::size_t cur_lc_degree = 0;
301		};
302	1582	void getVariableInformation(VariableInformation& vi,
303		const poly::Polynomial& poly)
304		{
305	1582	GetVarInfo varinfo;
306	1582	varinfo.info = &vi;
307	1582	lp_polynomial_traverse_f f =
308	6422	[](const lp_polynomial_context_t* ctx, lp_monomial_t* m, void* data) {
309	3211	GetVarInfo* gvi = static_cast<GetVarInfo*>(data);
310	3211	VariableInformation* info = gvi->info;
311		// Total degree of this term
312	3211	std::size_t tdeg = 0;
313		// Degree of this variable within this term
314	3211	std::size_t vardeg = 0;
315	5709	for (std::size_t i = 0; i < m->n; ++i)
316		{
317	2498	tdeg += m->p[i].d;
318	2498	if (m->p[i].x == info->var)
319		{
320	1104	info->max_degree = std::max(info->max_degree, m->p[i].d);
321	1104	info->sum_term_degree += m->p[i].d;
322	1104	vardeg = m->p[i].d;
323		}
324		}
325	3211	if (info->var == poly::Variable())
326		{
327		++info->num_terms;
328		info->max_degree = std::max(info->max_degree, tdeg);
329		info->sum_term_degree += tdeg;
330		}
331	3211	else if (vardeg > 0)
332		{
333	1104	++info->num_terms;
334	1104	if (gvi->cur_var_degree < vardeg)
335		{
336	1104	gvi->cur_lc_degree = tdeg - vardeg;
337		}
338	1104	info->max_terms_tdegree = std::max(info->max_terms_tdegree, tdeg);
339		}
340	6422	};
341	1582	std::size_t tmp_max_degree = vi.max_degree;
342	1582	std::size_t tmp_num_terms = vi.num_terms;
343	1582	vi.max_degree = 0;
344	1582	vi.num_terms = 0;
345	1582	lp_polynomial_traverse(poly.get_internal(), f, &varinfo);
346	1582	vi.max_lc_degree = std::max(vi.max_lc_degree, varinfo.cur_lc_degree);
347	1582	if (vi.num_terms > 0)
348		{
349	992	++vi.num_polynomials;
350		}
351	1582	vi.sum_poly_degree += vi.max_degree;
352	1582	vi.max_degree = std::max(vi.max_degree, tmp_max_degree);
353	1582	vi.num_terms += tmp_num_terms;
354	1582	}
355
356		} // namespace poly_utils
357	28194	} // namespace cvc5
358
359		#endif