1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
/******************************************************************************
* 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.
*/
struct VariableInformation
{
poly::Variable var;
/** Maximum degree of this variable. */
std::size_t max_degree = 0;
/** Maximum degree of the leading coefficient of this variable. */
std::size_t max_lc_degree = 0;
/** Maximum of total degrees of terms that contain this variable. */
std::size_t max_terms_tdegree = 0;
/** Sum of degrees of this variable 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 */
|
