1 #include "../operators/properties.h"
3 #include <carl-common/util/streamingOperators.h>
7 using carl::operator<<;
13 for (
const auto& poly : delin.
nullified()) {
16 for (
const auto& poly : delin.
nonzero()) {
19 for (
const auto& [ran,irexprs] : delin.
roots()) {
20 for (
const auto& ir : irexprs) {
40 boost::container::flat_map<datastructures::PolyRef, datastructures::IndexedRoot>
result;
42 auto it = interval.
lower();
44 for (
const auto& root : it->second) {
45 if (!closest ||
result.find(root.root.poly) ==
result.end()) {
46 result.emplace(root.root.poly, root.root);
49 if (it != delin.
roots().begin()) it--;
57 boost::container::flat_map<datastructures::PolyRef, datastructures::IndexedRoot>
result;
59 auto it = interval.
upper();
60 while(it != delin.
roots().end()) {
61 for (
const auto& root : it->second) {
62 if (!closest ||
result.find(root.root.poly) ==
result.end()) {
63 result.emplace(root.root.poly, root.root);
76 if (der->cell().lower_unbounded() || der->cell().upper_unbounded()) {
81 auto p_closest_below =
roots_below(der->delin(), der->cell(),
true);
82 auto p_closest_above =
roots_above(der->delin(), der->cell(),
true);
83 auto p_farthest_below =
roots_below(der->delin(), der->cell(),
false);
84 auto p_farthest_above =
roots_above(der->delin(), der->cell(),
false);
87 bool is_below = p_closest_below.find(poly) != p_closest_below.end();
88 bool is_above = p_closest_above.find(poly) != p_closest_above.end();
89 assert(is_below || is_above);
90 if (is_below && !is_above) {
91 std::optional<datastructures::IndexedRoot> other_root;
92 for (
const auto& other_poly : response.
ordering.
polys(poly)) {
93 if (p_closest_above.find(other_poly) != p_closest_above.end()) {
94 other_root = p_closest_above.at(other_poly);
104 }
else if (!is_below && is_above) {
105 std::optional<datastructures::IndexedRoot> other_root;
106 for (
const auto& other_poly : response.
ordering.
polys(poly)) {
107 if (p_closest_below.find(other_poly) != p_closest_below.end()) {
108 other_root = p_closest_below.at(other_poly);
125 for (
const auto& [k,v] : der->delin().roots()) {
126 for (
const auto& tir : v) {
127 if (!response.
equational.contains(tir.root.poly)) {
138 for (
const auto& poly_delin : poly_delins.
data) {
173 if (der->cell().is_section()) {
177 auto reduced_cell = reduced_delineation.
delineate_cell(der->main_var_sample());
207 auto reduced_cell = reduced_delineation.
delineate_cell(der->main_var_sample());
210 if (der->cell().is_section()) {
248 if (der->cell().is_section()) {
252 auto reduced_cell = reduced_delineation.
delineate_cell(der->main_var_sample());
270 if (der->cell().is_section()) {
274 auto reduced_cell = reduced_delineation.
delineate_cell(der->main_var_sample());
294 auto reduced_cell = reduced_delineation.
delineate_cell(der->main_var_sample());
296 response.
ordering = global_ordering;
298 if (der->cell().is_section()) {
304 for (
const auto& poly_delin : poly_delins.
data) {
305 if (response.
equational.contains(poly_delin.first))
continue;
308 for (
const auto& poly : der->delin().nullified()) {
311 for (
const auto& poly : der->delin().nonzero()) {
An interval of a delineation.
bool lower_unbounded() const
bool upper_unbounded() const
const auto & upper() const
const auto & lower() const
Represents the delineation of a set of polynomials (at a sample), that is.
const auto & nonzero() const
The set of polynomials without roots.
const auto & roots() const
Returns the underlying root map, which is a set of real algebraic numbers to indexed root expressions...
const auto & nullified() const
The set of nullified polynomials.
auto delineate_cell(const RAN &sample) const
Computes the bounds of the interval around the given sample w.r.t.
Describes an ordering of IndexedRoots.
void add_leq(RootFunction first, RootFunction second)
std::optional< SymbolicInterval > biggest_cell_wrt
void polys(boost::container::flat_set< PolyRef > &result) const
void add_less(RootFunction first, RootFunction second)
const auto & lower() const
Return the lower bound.
const auto & upper() const
Returns the upper bound.
const IndexedRoot & section_defining() const
In case of a section, the defining indexed root is returned.
std::shared_ptr< SampledDerivation< Properties > > SampledDerivationRef
void chain_ordering(const datastructures::PolyRef poly, const PolyDelineation &poly_delin, datastructures::IndexedRootOrdering &ordering)
void simplest_chain_ordering(datastructures::Projections &proj, const datastructures::Delineation &delin, datastructures::IndexedRootOrdering &ordering, bool enable_weak=false)
void simplify(const datastructures::PolyRef poly, datastructures::Delineation &delin)
datastructures::SymbolicInterval compute_simplest_cell(datastructures::Projections &proj, const datastructures::DelineationInterval &del, bool enable_weak=false)
void simplest_biggest_cell_ordering(datastructures::Projections &, const datastructures::Delineation &delin, const datastructures::DelineationInterval &delin_interval, const datastructures::SymbolicInterval &interval, datastructures::IndexedRootOrdering &ordering, bool enable_weak=false)
void simplest_ldb_ordering(datastructures::Projections &proj, const datastructures::Delineation &delin, const datastructures::DelineationInterval &delin_interval, const datastructures::SymbolicInterval &interval, datastructures::IndexedRootOrdering &ordering, boost::container::flat_set< datastructures::PolyRef > &equational, bool enable_weak, bool use_global_cache)
auto get_local_del_polys(const datastructures::Delineation &delin)
Local delineability.
void local_del_ordering(datastructures::Projections &proj, const datastructures::PolyRef poly, const cadcells::Assignment &ass, const cadcells::RAN &sample, datastructures::Delineation &delin, const datastructures::SymbolicInterval &interval, datastructures::IndexedRootOrdering &ordering)
bool local_del_poly_independent(const datastructures::Delineation &delin, const datastructures::PolyRef &poly)
void decompose(datastructures::Delineation &delin, const datastructures::DelineationInterval &delin_interval, PolyDelineations &poly_delins)
Heuristics for computing representations.
boost::container::flat_map< datastructures::PolyRef, datastructures::IndexedRoot > roots_below(const datastructures::Delineation &delin, const datastructures::DelineationInterval &interval, bool closest)
void handle_section_all_equational(const datastructures::Delineation &delin, datastructures::CellRepresentation< T > &response)
datastructures::CellRepresentation< T > compute_cell_lowest_degree_barriers(datastructures::SampledDerivationRef< T > &der, LocalDelMode ldel_mode=LocalDelMode::NONE, bool enable_weak=false, bool use_global_cache=false, datastructures::IndexedRootOrdering global_ordering=datastructures::IndexedRootOrdering())
void handle_projective_ordering(datastructures::SampledDerivationRef< T > &der, datastructures::CellRepresentation< T > &response)
@ LOWEST_DEGREE_BARRIERS_CACHE_GLOBAL
@ BIGGEST_CELL_FILTER_ONLY_INDEPENDENT
@ LOWEST_DEGREE_BARRIERS_EQ
@ LOWEST_DEGREE_BARRIERS_PDEL
@ LOWEST_DEGREE_BARRIERS_FILTER_ONLY_INDEPENDENT
@ LOWEST_DEGREE_BARRIERS_FILTER
void handle_cell_reduction(datastructures::Delineation &reduced_delineation, datastructures::DelineationInterval &reduced_cell, datastructures::CellRepresentation< T > &response)
void handle_connectedness(datastructures::SampledDerivationRef< T > &der, datastructures::CellRepresentation< T > &response, bool enable_weak=false)
void handle_local_del_simplify_non_independent(datastructures::Delineation &reduced_delineation)
datastructures::CellRepresentation< T > compute_cell_biggest_cell(datastructures::SampledDerivationRef< T > &der, LocalDelMode ldel_mode=LocalDelMode::NONE, bool enable_weak=false)
void handle_local_del_simplify_all(datastructures::Delineation &reduced_delineation)
void handle_ordering_polys(datastructures::SampledDerivationRef< T > &der, datastructures::CellRepresentation< T > &response)
boost::container::flat_map< datastructures::PolyRef, datastructures::IndexedRoot > roots_above(const datastructures::Delineation &delin, const datastructures::DelineationInterval &interval, bool closest)
void handle_local_del(datastructures::SampledDerivationRef< T > &der, datastructures::Delineation &reduced_delineation, datastructures::CellRepresentation< T > &response)
#define SMTRAT_STATISTICS_CALL(function)
IndexedRootOrdering ordering
An ordering on the roots that protects the cell.
boost::container::flat_set< PolyRef > ordering_polys
Polys considered in the indexed root ordering.
SymbolicInterval description
Description of a cell.
boost::container::flat_set< PolyRef > equational
Polynomials that should be projected using the equational constraints projection.
boost::container::flat_set< PolyRef > ordering_non_projective_polys
Polys that are considered "non-projectively" in the ordering.
PolyRef poly
A multivariate polynomial.
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
Note: If connected(i) holds, then the indexed root ordering must contain an ordering between the inte...
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
boost::container::flat_map< datastructures::PolyRef, PolyDelineation > data