/******************************************************************************

 * Top contributors (to current version):

 *   Gereon Kremer, Aina Niemetz

 *

 * 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 "cvc5_private.h"

#ifndef CVC5__POLY_UTIL_H

#define CVC5__POLY_UTIL_H

#include <vector>

#include "maybe.h"

#include "util/integer.h"

#include "util/rational.h"

#include "util/real_algebraic_number.h"

#ifdef CVC5_POLY_IMP

#include <poly/polyxx.h>

namespace cvc5 {

/**

 * Utilities for working with libpoly.

 * This namespace contains various basic conversion routines necessary for the

 * integration of LibPoly. Firstly, LibPoly is based on GMP and hence we need

 * conversion from and to CLN (in case CLN is enabled). Otherwise, conversion of

 * number types mostly reduces to simple type casts.

 * Furthermore, conversions between poly::Rational and poly::DyadicRational and

 * constructors for algebraic numbers that need initial refinement of the

 * interval are provided.

 */

namespace poly_utils {

/** Converts a poly::Integer to a cvc5::Integer. */

Integer toInteger(const poly::Integer& i);

/** Converts a poly::Integer to a cvc5::Rational. */

Rational toRational(const poly::Integer& r);

/** Converts a poly::Rational to a cvc5::Rational. */

Rational toRational(const poly::Rational& r);

/** Converts a poly::DyadicRational to a cvc5::Rational. */

Rational toRational(const poly::DyadicRational& dr);

/** Converts a poly::Value to a cvc5::Rational (that may be a bit above). */

Rational toRationalAbove(const poly::Value& v);

/** Converts a poly::Value to a cvc5::Rational (that may be a bit below). */

Rational toRationalBelow(const poly::Value& v);

/** Converts a cvc5::Integer to a poly::Integer. */

poly::Integer toInteger(const Integer& i);

/** Converts a vector of cvc5::Integers to a vector of poly::Integers. */

std::vector<poly::Integer> toInteger(const std::vector<Integer>& vi);

/** Converts a cvc5::Rational to a poly::Rational. */

poly::Rational toRational(const Rational& r);

/**

 * Converts a cvc5::Rational to a poly::DyadicRational. If the input is not

 * dyadic, no result is produced.

 */

Maybe<poly::DyadicRational> toDyadicRational(const Rational& r);

/**

 * Converts a poly::Rational to a poly::DyadicRational. If the input is not

 * dyadic, no result is produced.

 */

Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r);

/**

 * Iteratively approximates a poly::Rational by a dyadic poly::Rational.

 * Assuming that r is dyadic, makes one refinement step to move r closer to

 * original.

 * Assumes one starts with lower(original) or ceil(original) for r.

 */

poly::Rational approximateToDyadic(const poly::Rational& r,

                                   const poly::Rational& original);

/**

 * Constructs a poly::AlgebraicNumber, allowing for refinement of the

 * cvc5::Rational bounds. As a poly::AlgebraicNumber works on

 * poly::DyadicRationals internally, the bounds are iteratively refined using

 * approximateToDyadic until the respective interval is isolating. If the

 * provided rational bounds are already dyadic, the refinement is skipped.

 */

poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p,

                                              const Rational& lower,

                                              const Rational& upper);

/**

 * Constructs a cvc5::RealAlgebraicNumber, simply wrapping

 * toPolyRanWithRefinement.

 */

RealAlgebraicNumber toRanWithRefinement(poly::UPolynomial&& p,

                                        const Rational& lower,

                                        const Rational& upper);

std::size_t totalDegree(const poly::Polynomial& p);

/**

 * Collects information about a single variable in a set of polynomials.

 * Used for determining a variable ordering.

 */

{

  poly::Variable var;

  /** Maximum degree of this variable. */

  std::size_t max_degree = 0;

  /** Maximum degree of the leading coefficient of this variable. */

  std::size_t max_lc_degree = 0;

  /** Maximum of total degrees of terms that contain this variable. */

  std::size_t max_terms_tdegree = 0;

  /** Sum of degrees of this variable within all terms. */

  std::size_t sum_term_degree = 0;

  /** Sum of degrees of this variable within all polynomials. */

  std::size_t sum_poly_degree = 0;

  /** Number of polynomials that contain this variable. */

  std::size_t num_polynomials = 0;

  /** Number of terms that contain this variable. */

  std::size_t num_terms = 0;

};

std::ostream& operator<<(std::ostream& os, const VariableInformation& vi);

void getVariableInformation(VariableInformation& vi,

                            const poly::Polynomial& poly);

}  // namespace poly_utils

}  // namespace cvc5

#endif

#endif /* CVC5__POLY_UTIL_H */