Commit 8941a4c3 authored by Ballabriga Clément's avatar Ballabriga Clément
Browse files

proprification pour jordy

parent d0be79f7
......@@ -11,7 +11,7 @@
#include "MyHTable.h"
// #define POLY_DEBUG 1
#define POLY_DEBUG 1
namespace otawa {
namespace poly {
......
......@@ -10,6 +10,11 @@ namespace poly {
namespace PPL = Parma_Polyhedra_Library;
//typedef PPL::C_Polyhedron Shape;
typedef PPL::Octagonal_Shape<PPL::Coefficient> Shape;
typedef unsigned long long guid_t;
typedef std::GMP_Integer coef_t;
typedef PPL::dimension_type dim_t;
......@@ -139,7 +144,7 @@ class WPoly {
class Eliminator {
public:
inline Eliminator(const std::vector<PPL::dimension_type> &victims,
PPL::C_Polyhedron &p) : _victims(victims), _p(p), _dom(_p.space_dimension() - 1),
Shape &p) : _victims(victims), _p(p), _dom(_p.space_dimension() - 1),
_codom(_dom - _victims.size()) {
}
......@@ -160,7 +165,7 @@ class WPoly {
inline bool has_empty_codomain() const { return _p.space_dimension() == _victims.size(); }
private:
const std::vector<PPL::dimension_type> &_victims;
const PPL::C_Polyhedron & _p;
const Shape & _p;
const int _dom;
const int _codom;
};
......@@ -241,7 +246,7 @@ class WPoly {
inline WPoly(bool empty) {
poly = PPL::C_Polyhedron(0, empty ? PPL::EMPTY : PPL::UNIVERSE);
poly = Shape(0, empty ? PPL::EMPTY : PPL::UNIVERSE);
}
......@@ -301,7 +306,8 @@ class WPoly {
elm::cout << "\n\n";
*/
PPL::Constraint pplc = translate(c);
poly.add_constraint(pplc);
// poly.add_constraint(pplc);
poly.refine_with_constraint(pplc);
/*
elm::cout << "constraint added: " << c << "\ntranslated to: ";
pplc.print();
......@@ -322,7 +328,7 @@ class WPoly {
WCons back_translate(const PPL::Constraint &c) const;
void print(output_t &out) const;
inline const PPL::C_Polyhedron& getPoly() { return poly; }
inline const Shape& getPoly() { return poly; }
inline bool maximize(const WLinExpr&expr, coef_t &sup_n, coef_t &sup_d, bool &maximum) const {
return poly.maximize(translate(expr), sup_n, sup_d, maximum);
......@@ -391,7 +397,7 @@ class WPoly {
inline void poly_hull_assign(const WPoly &src) {
WPoly copie = src;
combine(copie, false);
poly.poly_hull_assign(copie.poly);
poly.upper_bound_assign(copie.poly);
}
// widening
......@@ -399,7 +405,7 @@ class WPoly {
WPoly copie = src;
combine(copie, false);
PPL::Constraint_System dummy;
poly.bounded_H79_extrapolation_assign(copie.poly, dummy);
poly.widening_assign(copie.poly /* , dummy */);
}
private:
......@@ -424,7 +430,7 @@ class WPoly {
std::map<guid_t,dim_t> adapter;
dim_t next = 0;
PPL::C_Polyhedron poly;
Shape poly;
};
......
......@@ -57,6 +57,13 @@ void WPoly::print(output_t &out) const {
poly.print();
fflush(stdout);
out << "]\n" << endl;
poly.minimized_constraints();
out << "\nRaw poly: [";
fflush(stdout);
poly.print();
fflush(stdout);
out << "]\n" << endl;
out << "Map: [";
for (std::map<guid_t,dim_t>::const_iterator it=adapter.begin(); it != adapter.end(); it++) {
PPL::Variable pv(it->second);
......@@ -71,12 +78,22 @@ void WPoly::print(output_t &out) const {
out << "v" << it->first << " -> " << name << "; ";
}
out << "] " << endl << endl;
out << "\nRaw poly1: [";
fflush(stdout);
poly.print();
fflush(stdout);
out << "WPoly: ";
for (WPoly::ConsIterator it(*this); it; it++) {
out << (*it) << "; ";
// out << (*it) << "; ";
}
out << "]" << endl;
out << endl;
out << "\nRaw poly2: [";
fflush(stdout);
poly.print();
fflush(stdout);
out << "]\n" << endl;
}
/* Constraint & Linear combination building operators */
......@@ -200,6 +217,8 @@ WCons WPoly::back_translate(const Constraint &c) const {
}
}
le = le + c.inhomogeneous_term();
elm::cout << "to be translated:" << "\n";
c.print();
if (c.is_equality()) {
return le == 0;
} else {
......
int main(void) {
int i;
int j;
int c;
int d;
int cond1, cond2;
for (i = 0; i < 10; i++);
j = -42;
if (cond1) {
c = 10;
} else {
c = 20;
}
d = c;
i = 100 + c -d;
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment