codac
codac_SepProj.h
1 //============================================================================
2 // I B E X
3 // File : ibex_sepProj.h
4 // Author : Benoit Desrochers
5 // Copyright : Benoit Desrochers
6 // License : See the LICENSE file
7 // Created : May 04, 2015
8 //============================================================================
9 
10 #ifndef __IBEX_SEP_PROJ_H__
11 #define __IBEX_SEP_PROJ_H__
12 
13 
14 #include <ibex_IntervalVector.h>
15 #include <ibex_Sep.h>
16 //#include "ibex_SepFixPoint.h"
17 #include <ibex_LargestFirst.h>
18 #include <vector>
19 #include <queue>
20 #include <stack>
21 
22 using ibex::IntervalVector;
23 using ibex::Interval;
24 using ibex::Sep;
25 using ibex::LargestFirst;
26 
27 namespace codac {
28 
29 typedef std::pair<IntervalVector, IntervalVector> TwoItv;
30 
31 typedef struct ImpactStatus_{
32  bool impact_cin;
33  bool impact_cout;
34  IntervalVector *first_cin_boxes, *first_cout_boxes;
35  int n_in, n_out;
36 
37  ImpactStatus_ () : impact_cin(false), impact_cout(false),
38  first_cin_boxes(NULL), first_cout_boxes(NULL){
39  n_in = 0; n_out = 0;
40  clearFlags();
41  }
42 
43  ImpactStatus_(IntervalVector& x_in, IntervalVector& x_out):
44  impact_cin(false), impact_cout(false),
45  first_cin_boxes(NULL), first_cout_boxes(NULL){
46  n_in = 0; n_out = 0;
47  clearFlags();
48  if( !( x_in == x_out) ){ // already contracted
49  IntervalVector x0(x_in | x_out);
50  setCinFlags(x_in, x0);
51  setCoutFlags(x_out, x0);
52  }
53  }
54 
55 // ImpactStatus_(const ImpactStatus_& other):
56 // impact_cin(other.impact_cin),
57 // impact_cout(other.impact_cout),
58 // n_in(other.n_in),
59 // n_out(other.n_out) {
60 
61 // if (n_in > 0){
62 // first_cin_boxes = new IntervalVector[n_in];
63 // for (uint i = 0; i < n_in; i++){
64 // first_cin_boxes[i] = new IntervalVector(other.first_cin_boxes[i]);
65 // }
66 // }
67 // if (n_out > 0){
68 // first_cout_boxes = new IntervalVector[n_out];
69 // for (uint i = 0; i < n_out; i++){
70 // first_cout_boxes[i] = new IntervalVector(other.first_cout_boxes[i]);
71 // }
72 // }
73 // }
74 
75 
76 
77  ~ImpactStatus_(){
78  clearFlags();
79  }
80 
81  void clearFlags(){
82  n_in = 0;
83  n_out = 0;
84  if (first_cin_boxes != NULL) delete[] first_cin_boxes;
85  if (first_cout_boxes != NULL) delete[] first_cout_boxes;
86  first_cin_boxes = NULL;
87  first_cout_boxes = NULL;
88  impact_cin = false;
89  impact_cout = false;
90  }
91 
92 
93  void setCinFlags(IntervalVector& x_in, IntervalVector& x0){
94  if( !impact_cin ){
95  if ( ! (x_in == x0)){
96  impact_cin = true;
97  n_in = x0.diff(x_in,first_cin_boxes); // calculate the set difference
98  }
99  }
100  }
101 
102  void setCoutFlags(IntervalVector& x_out, IntervalVector& x0){
103  if(!impact_cout){
104  if ( !(x_out == x0)){
105  impact_cout = true;
106  n_out = x0.diff(x_out,first_cout_boxes); // calculate the set difference
107  }
108  }
109  }
110 
111  void reset_and_setCoutFlags(IntervalVector& x_out, IntervalVector& x0){
112  impact_cout = false;
113  if (first_cout_boxes != NULL){
114  delete[] first_cout_boxes;
115  first_cout_boxes = NULL;
116  }
117  setCoutFlags(x_out, x0);
118  }
119 
120  void reconstrut_v2(IntervalVector &x_in, IntervalVector& x_out, IntervalVector& x_old){
121  // std::cerr << x_in << " " << x_out << " " << x_old << "\n";
122  // std::cerr << impact_cout << " " << impact_cin << "\n";
123  if (x_out.is_empty() && impact_cout && impact_cin){
124  x_in = x_old;
125  return;
126  }
127  if (!x_in.is_empty() && !x_out.is_empty()){
128  if (impact_cin == true){
129  if (impact_cout == false){
130  x_out = x_old;
131  } else {
132  for(int i = 0; i < n_in; i++){
133  x_out |= first_cin_boxes[i];
134  }
135  }
136  }
137  if(impact_cout == true){
138  if(impact_cin == false){
139  x_in = x_old;
140  } else {
141  for(int i = 0; i < n_out; i++){
142  x_in |= first_cout_boxes[i];
143  }
144  }
145  }
146  } else if (x_in.is_empty() && impact_cin == true){
147  if(impact_cout == false){
148  x_out = x_old;
149  } else {
150  for(int i = 0; i < n_in; i++){
151  x_out |= first_cin_boxes[i];
152  }
153  }
154  } else if (x_out.is_empty() && impact_cout == true){
155  if(impact_cin == false){
156  x_in = x_old;
157  } else {
158  for(int i = 0; i < n_out; i++){
159  x_in |= first_cout_boxes[i];
160  }
161  }
162  } else {
163  std::cout << "#########################################################\n";
164  std::cout << "x_in " << x_in << " x_out " << x_out << "\n";
165  std::cout << "x_old " << x_old << "n_in " << n_in << " n_out " << n_out;
166  std::cout << " impact_cin " << impact_cin << " ";
167  std::cout << " impact_cout " << impact_cout << " ";
168  std::cout << "\n";
169  std::cout << "#########################################################\n";
170  assert(false);
171  }
172  }
173 
174 
175  void reconstrut(IntervalVector &x_in, IntervalVector& x_out, IntervalVector& x_old){
176  IntervalVector x = x_in & x_out;
177  IntervalVector *rest;
178 
179  if (x == x_old) return;
180  if (impact_cin == true && impact_cout == false){
181  x_out = x_old;
182  x_in = x;
183  } else if (impact_cin == false && impact_cout == true){
184  x_in = x_old;
185  x_out = x;
186  } else if (impact_cin == true && impact_cout == true){
187  int n = x_old.diff(x, rest);
188 // for(uint i = 0; i < n; i++){
189 // std::cout << "rest " << i << ": " << rest[i] << "\n" << std::flush;
190 // }
191 // for(uint i = 0; i < n_in; i++){
192 // std::cout << "in " << i << ": " << first_cin_boxes[i] << "\n" << std::flush;
193 // }
194 // for(uint i = 0; i < n_out; i++){
195 // std::cout << "out " << i << ": " << first_cout_boxes[i] << "\n" << std::flush;
196 // }
197  // std::cout << rest[0] << " " << rest_in[0] << " " << rest_out[0] << std::endl;
198  std::cerr << n_in << " " << n_out << " " << n << "\n";
199  assert(n_in == 1);
200  assert(n_out == 1);
201  assert(n == 2);
202  for (int i = 0; i < n; i++){
203  for(int j = 0; j < n_in; j++){
204  if(first_cin_boxes[j].intersects(rest[i])){
205  x_out |= rest[i];
206  break;
207  }
208  }
209  for(int j = 0; j < n_out; j++){
210  if(first_cout_boxes[j].intersects(rest[i])){
211  x_in |= rest[i];
212  break;
213  }
214  }
215  }
216  delete[] rest;
217  } else {
218  assert(false);
219  }
220  }
221 
222 } ImpactStatus;
223 
245 class SepProj : public Sep {
246 
247 public:
258  SepProj(Sep& sep, const IntervalVector& y_init, double prec);
259 
270  SepProj(Sep& sep, const Interval& y_init, double prec);
271 
276  ~SepProj();
277 
278 
285  void separate(IntervalVector &x_in, IntervalVector &x_out);
286 
287 protected:
288 
301  bool process(IntervalVector &x_in, IntervalVector &x_out, IntervalVector &y, ImpactStatus &impact, bool use_point);
302 
303 
304  bool separate_fixPoint(IntervalVector& x_in, IntervalVector& x_out, IntervalVector &y);
305 
309  Sep& sep;
310 
311 
315  IntervalVector y_init;
316 
320  double prec;
321 
326  // int nbx;
327 
328 
332 // bool impact_cin, impact_cout;
333 
337 // IntervalVector *first_cin_boxes, *first_cout_boxes;
338 // int n_in, n_out;
339 
343  LargestFirst* bsc;
344 
351 private:
352  bool fixpoint(IntervalVector &x, IntervalVector &x_out_res, IntervalVector &y);
353 
354 
355 };
356 
357 
358 
359 
360 } // namespace pyibex
361 
362 #endif // __IBEX_SEP_PROJ_H__
IntervalVector y_init
Initial box of the parameters (can be set dynamically)
Definition: codac_SepProj.h:315
FixPoint of a separator The fixpoint of a separator is computed by calling the "::"separate function ...
Definition: codac_capd_helpers.h:9
LargestFirst * bsc
internal variable used to count the number of call of the SepProj::process method ...
Definition: codac_SepProj.h:343
Sep & sep
The Separator.
Definition: codac_SepProj.h:309
Projection of a separator.
Definition: codac_SepProj.h:245
double prec
precision
Definition: codac_SepProj.h:320