carl  24.04
Computer ARithmetic Library
ran.h
Go to the documentation of this file.
1 #pragma once
2 
3 /**
4  * @file
5  * Represent a real algebraic number (RAN) in one of several ways:
6  * - Implicitly by a univariate polynomial and an interval.
7  * - Implicitly by a polynomial and a sequence of signs (called Thom encoding).
8  * - Explicitly by a rational number.
9  * Rationale:
10  * - A real number cannot always be adequately represented in finite memory, since
11  * it may be infinitely long. Representing
12  * it by a float or any other finite-precision representation and doing
13  * arithmetic may introduce unacceptable rounding errors.
14  * The algebraic reals, a subset of the reals, is the set of those reals that can be represented
15  * as the root of a univariate polynomial with rational coefficients so there is always
16  * an implicit, finite, full-precision
17  * representation by an univariate polynomial and an isolating interval that
18  * contains this root (only this root and no other). It is also possible
19  * to do relatively fast arithmetic with this representation without rounding errors.
20  * - When the algebraic real is only finitely long prefer the rational number
21  * representation because it's faster.
22  * - The idea of the Thom-Encoding is as follows: Take a square-free univariate polynomial p
23  * with degree n that has the algebraic real as its root, compute the first n-1 derivates of p,
24  * plug in this algebraic real into each derivate and only keep the sign.
25  * Then polynomial p with this sequence of signs uniquely represents this algebraic real.
26  */
27 
28 
29 #include <carl-common/config.h>
30 
31 
32 #include "interval/Ran.h"
33 #include "interval/Evaluation.h"
34 #include "interval/RealRoots.h"
35 
36 //#include "thom/ran_thom.h"
37 //#include "thom/ran_thom_evaluation.h"
38 
39 #ifdef USE_LIBPOLY
40 #include "libpoly/LPRan.h"
41 #include "libpoly/Evaluation.h"
42 #include "libpoly/RealRoots.h"
43 #endif