SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
heuristics_cell.h
Go to the documentation of this file.
1 #include "../operators/properties.h"
2 
3 #include <carl-common/util/streamingOperators.h>
4 
6 
7  using carl::operator<<;
8 
9 template<typename T>
11  // TODO sometimes it might be beneficial to not include nullified or nonzero polynomials
12 
13  for (const auto& poly : delin.nullified()) {
14  response.equational.insert(poly);
15  }
16  for (const auto& poly : delin.nonzero()) {
17  response.equational.insert(poly);
18  }
19  for (const auto& [ran,irexprs] : delin.roots()) {
20  for (const auto& ir : irexprs) {
21  if (ir.root.poly != response.description.section_defining().poly) {
22  response.equational.insert(ir.root.poly);
23  }
24  }
25  }
26 }
27 
28 template<typename T>
30  if (der->contains(operators::properties::cell_connected{der->level()}) && !response.description.is_section() && !response.description.lower().is_infty() && !response.description.upper().is_infty()) {
31  if (enable_weak) {
32  response.ordering.add_leq(response.description.lower().value(), response.description.upper().value());
33  } else {
34  response.ordering.add_less(response.description.lower().value(), response.description.upper().value());
35  }
36  }
37 }
38 
39 inline boost::container::flat_map<datastructures::PolyRef, datastructures::IndexedRoot> roots_below(const datastructures::Delineation& delin, const datastructures::DelineationInterval& interval, bool closest) {
40  boost::container::flat_map<datastructures::PolyRef, datastructures::IndexedRoot> result;
41  if (!interval.lower_unbounded()) {
42  auto it = interval.lower();
43  while(true) {
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);
47  }
48  }
49  if (it != delin.roots().begin()) it--;
50  else break;
51  }
52  }
53  return result;
54 }
55 
56 inline boost::container::flat_map<datastructures::PolyRef, datastructures::IndexedRoot> roots_above(const datastructures::Delineation& delin, const datastructures::DelineationInterval& interval, bool closest) {
57  boost::container::flat_map<datastructures::PolyRef, datastructures::IndexedRoot> result;
58  if (!interval.upper_unbounded()) {
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);
64  }
65  }
66  it++;
67  }
68  }
69  return result;
70 }
71 
72 template<typename T>
74  response.ordering.set_projective();
75 
76  if (der->cell().lower_unbounded() || der->cell().upper_unbounded()) {
77  for (const auto& poly : response.ordering_polys) {
78  response.ordering_non_projective_polys.insert(poly);
79  }
80  } else {
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);
85 
86  for (const auto& poly : response.ordering_polys) {
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);
95  break;
96  }
97  }
98 
99  if (other_root) {
100  response.ordering.add_leq(*other_root, p_farthest_below.at(poly));
101  } else {
102  response.ordering_non_projective_polys.insert(poly);
103  }
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);
109  break;
110  }
111  }
112 
113  if (other_root) {
114  response.ordering.add_leq(*other_root, p_farthest_above.at(poly));
115  } else {
116  response.ordering_non_projective_polys.insert(poly);
117  }
118  }
119  }
120  }
121 }
122 
123 template<typename T>
125  for (const auto& [k,v] : der->delin().roots()) {
126  for (const auto& tir : v) {
127  if (!response.equational.contains(tir.root.poly)) {
128  response.ordering_polys.insert(tir.root.poly);
129  }
130  }
131  }
132 }
133 
134 template<typename T>
136  util::PolyDelineations poly_delins;
137  util::decompose(reduced_delineation, reduced_cell, poly_delins);
138  for (const auto& poly_delin : poly_delins.data) {
139  chain_ordering(poly_delin.first, poly_delin.second, response.ordering);
140  }
141 }
142 
143 template<typename T>
145  for (const auto poly : util::get_local_del_polys(reduced_delineation)) {
146  util::local_del_ordering(der->proj(), poly, der->underlying_sample(), der->main_var_sample(), reduced_delineation, response.description, response.ordering);
147  }
148 }
149 
151  for (const auto poly : util::get_local_del_polys(reduced_delineation)) {
152  util::simplify(poly, reduced_delineation);
153  }
154 }
155 
156 
158  for (const auto poly : util::get_local_del_polys(reduced_delineation)) {
159  if (!util::local_del_poly_independent(reduced_delineation, poly)) {
160  util::simplify(poly, reduced_delineation);
161  }
162  }
163 }
164 
166 
167 template <>
169  template<typename T>
172  response.description = util::compute_simplest_cell(der->proj(), der->cell());
173  if (der->cell().is_section()) {
174  handle_section_all_equational(der->delin(), response);
175  } else { // sector
176  datastructures::Delineation reduced_delineation = der->delin();
177  auto reduced_cell = reduced_delineation.delineate_cell(der->main_var_sample());
178  handle_cell_reduction(reduced_delineation, reduced_cell, response);
179  util::simplest_biggest_cell_ordering(der->proj(), reduced_delineation, reduced_cell, response.description, response.ordering);
180  }
181  handle_connectedness(der, response);
182  handle_ordering_polys(der, response);
183  SMTRAT_STATISTICS_CALL(statistics().got_representation_equational(response.equational.size()));
184  return response;
185  }
186 };
187 
188 template <>
190  template<typename T>
192  auto response = cell<CellHeuristic::BIGGEST_CELL>::compute(der);
193  handle_projective_ordering(der, response);
194  return response;
195  }
196 };
197 
198 template<typename T>
201  datastructures::Delineation reduced_delineation = der->delin();
202  if (ldel_mode == LocalDelMode::ONLY_INDEPENDENT) {
203  handle_local_del_simplify_non_independent(reduced_delineation);
204  } else if (ldel_mode == LocalDelMode::SIMPLIFY) {
205  handle_local_del_simplify_all(reduced_delineation);
206  }
207  auto reduced_cell = reduced_delineation.delineate_cell(der->main_var_sample());
208  response.description = util::compute_simplest_cell(der->proj(), reduced_cell, enable_weak);
209  response.ordering.biggest_cell_wrt = response.description;
210  if (der->cell().is_section()) {
211  handle_local_del_simplify_non_independent(reduced_delineation);
212  handle_local_del(der, reduced_delineation, response);
213  handle_section_all_equational(reduced_delineation, response);
214  } else { // sector
215  handle_local_del(der, reduced_delineation, response);
216  handle_cell_reduction(reduced_delineation, reduced_cell, response);
217  util::simplest_biggest_cell_ordering(der->proj(), reduced_delineation, reduced_cell, response.description, response.ordering, enable_weak);
218  }
219  handle_connectedness(der, response, enable_weak);
220  handle_ordering_polys(der, response);
221  SMTRAT_STATISTICS_CALL(statistics().got_representation_equational(response.equational.size()));
222  return response;
223 }
224 
225 template <>
227  template<typename T>
229  return compute_cell_biggest_cell(der, LocalDelMode::ALL, true);
230  }
231 };
232 
233 template <>
235  template<typename T>
238  }
239 };
240 
241 template <>
243  template<typename T>
246  response.description = util::compute_simplest_cell(der->proj(), der->cell());
247 
248  if (der->cell().is_section()) {
249  handle_section_all_equational(der->delin(), response);
250  } else { // sector
251  datastructures::Delineation reduced_delineation = der->delin();
252  auto reduced_cell = reduced_delineation.delineate_cell(der->main_var_sample());
253  handle_cell_reduction(reduced_delineation, reduced_cell, response);
254  util::simplest_chain_ordering(der->proj(), reduced_delineation, response.ordering);
255  }
256  handle_connectedness(der, response);
257  handle_ordering_polys(der, response);
258  SMTRAT_STATISTICS_CALL(statistics().got_representation_equational(response.equational.size()));
259  return response;
260  }
261 };
262 
263 template <>
265  template<typename T>
268  response.description = util::compute_simplest_cell(der->proj(), der->cell());
269 
270  if (der->cell().is_section()) {
271  handle_section_all_equational(der->delin(), response);
272  } else { // sector
273  datastructures::Delineation reduced_delineation = der->delin();
274  auto reduced_cell = reduced_delineation.delineate_cell(der->main_var_sample());
275  handle_cell_reduction(reduced_delineation, reduced_cell, response);
276  util::simplest_ldb_ordering(der->proj(), reduced_delineation, reduced_cell, response.description, response.ordering, response.equational, false, false);
277  }
278  handle_connectedness(der, response);
279  handle_ordering_polys(der, response);
280  SMTRAT_STATISTICS_CALL(statistics().got_representation_equational(response.equational.size()));
281  return response;
282  }
283 };
284 
285 template<typename T>
288  datastructures::Delineation reduced_delineation = der->delin();
289  if (ldel_mode == LocalDelMode::ONLY_INDEPENDENT) {
290  handle_local_del_simplify_non_independent(reduced_delineation);
291  } else if (ldel_mode == LocalDelMode::SIMPLIFY) {
292  handle_local_del_simplify_all(reduced_delineation);
293  }
294  auto reduced_cell = reduced_delineation.delineate_cell(der->main_var_sample());
295  response.description = util::compute_simplest_cell(der->proj(), reduced_cell, enable_weak);
296  response.ordering = global_ordering;
297 
298  if (der->cell().is_section()) {
299  handle_local_del_simplify_non_independent(reduced_delineation);
300  handle_local_del(der, reduced_delineation, response);
301  util::PolyDelineations poly_delins;
302  util::decompose(reduced_delineation, reduced_cell, poly_delins);
303  util::simplest_ldb_ordering(der->proj(), reduced_delineation, reduced_cell, response.description, response.ordering, response.equational, enable_weak, use_global_cache);
304  for (const auto& poly_delin : poly_delins.data) {
305  if (response.equational.contains(poly_delin.first)) continue;
306  chain_ordering(poly_delin.first, poly_delin.second, response.ordering);
307  }
308  for (const auto& poly : der->delin().nullified()) {
309  response.equational.insert(poly);
310  }
311  for (const auto& poly : der->delin().nonzero()) {
312  response.equational.insert(poly);
313  }
314  } else { // sector
315  handle_local_del(der, reduced_delineation, response);
316  util::simplest_ldb_ordering(der->proj(), reduced_delineation, reduced_cell, response.description, response.ordering, response.equational, enable_weak, use_global_cache);
317  }
318  handle_connectedness(der, response, enable_weak);
319  handle_ordering_polys(der, response);
320  SMTRAT_STATISTICS_CALL(statistics().got_representation_equational(response.equational.size()));
321  return response;
322 }
323 
324 template <>
326  template<typename T>
329  }
330 };
331 
332 template <>
334  template<typename T>
337  }
338 };
339 
340 template <>
342  template<typename T>
345  handle_projective_ordering(der, response);
346  return response;
347  }
348 };
349 
350 template <>
352  template<typename T>
355  }
356 };
357 
358 template <>
360  template<typename T>
363  }
364 };
365 
366 }
Represents the delineation of a set of polynomials (at a sample), that is.
Definition: delineation.h:118
const auto & nonzero() const
The set of polynomials without roots.
Definition: delineation.h:144
const auto & roots() const
Returns the underlying root map, which is a set of real algebraic numbers to indexed root expressions...
Definition: delineation.h:132
const auto & nullified() const
The set of nullified polynomials.
Definition: delineation.h:138
auto delineate_cell(const RAN &sample) const
Computes the bounds of the interval around the given sample w.r.t.
Definition: delineation.h:154
Describes an ordering of IndexedRoots.
Definition: roots.h:400
void add_leq(RootFunction first, RootFunction second)
Definition: roots.h:420
std::optional< SymbolicInterval > biggest_cell_wrt
Definition: roots.h:418
void polys(boost::container::flat_set< PolyRef > &result) const
Definition: roots.h:561
void add_less(RootFunction first, RootFunction second)
Definition: roots.h:435
const auto & lower() const
Return the lower bound.
Definition: roots.h:285
const auto & upper() const
Returns the upper bound.
Definition: roots.h:292
const IndexedRoot & section_defining() const
In case of a section, the defining indexed root is returned.
Definition: roots.h:277
std::shared_ptr< SampledDerivation< Properties > > SampledDerivationRef
Definition: derivation.h:25
void chain_ordering(const datastructures::PolyRef poly, const PolyDelineation &poly_delin, datastructures::IndexedRootOrdering &ordering)
Definition: util.h:399
void simplest_chain_ordering(datastructures::Projections &proj, const datastructures::Delineation &delin, datastructures::IndexedRootOrdering &ordering, bool enable_weak=false)
Definition: util.h:139
void simplify(const datastructures::PolyRef poly, datastructures::Delineation &delin)
Definition: util.h:619
datastructures::SymbolicInterval compute_simplest_cell(datastructures::Projections &proj, const datastructures::DelineationInterval &del, bool enable_weak=false)
Definition: util.h:56
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)
Definition: util.h:89
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)
Definition: util.h:161
auto get_local_del_polys(const datastructures::Delineation &delin)
Local delineability.
Definition: util.h:421
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)
Definition: util.h:446
bool local_del_poly_independent(const datastructures::Delineation &delin, const datastructures::PolyRef &poly)
Definition: util.h:433
void decompose(datastructures::Delineation &delin, const datastructures::DelineationInterval &delin_interval, PolyDelineations &poly_delins)
Definition: util.h:361
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)
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)
Definition: Statistics.h:23
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.
Definition: roots.h:17
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...
Definition: heuristics.h:24
static datastructures::CellRepresentation< T > compute(datastructures::SampledDerivationRef< T > &der)
boost::container::flat_map< datastructures::PolyRef, PolyDelineation > data
Definition: util.h:352