PPL Example of widening with tokens

widening_with_token_ppl.cc

//  Created by Samir Genaim on 13/02/2017.
//  Modified by Jesus Domenech on 06/11/2017.
//
// compile with:
//   g++ widening_with_token_ppl.cc -I/usr/local/src/ppl-1.2/src -I/usr/local/src/ppl-1.2 -I/opt/local/include -L/opt/local/lib -lppl -lgmp
#include <iostream>
#include "ppl_header.hh"
using namespace std;
void
print_constraints(const Constraint_System& cs,
                  const std::string& intro) {
  if (!intro.empty())
    cout << intro << "\n";
  Constraint_System::const_iterator i = cs.begin();
  Constraint_System::const_iterator cs_end = cs.end();
  bool printed_something = i != cs_end;
  while (i != cs_end) {
    using IO_Operators::operator<<;
    cout << *i++;
    if (i != cs_end)
      cout << ",\n";
  }
  cout << (printed_something ? "." : "true.") << std::endl;
}
void
print_constraints(const Polyhedron& p,
                  const std::string& intro) {
  print_constraints(p.constraints(),intro);
}
int main() {
  Variable x(0);
  Variable y(1);
  C_Polyhedron ph1(2);
  ph1.add_constraint(x >= 0);
  ph1.add_constraint(y >= 0);
  ph1.add_constraint(x <= 3);
  ph1.add_constraint(y <= 2);
  print_constraints(ph1, "*** ph1 ***");
  /*
  *** ph1 ***
  A >= 0,
  B >= 0,
  -A >= -3,
  -B >= -2.
  */
  C_Polyhedron ph2(2);
  ph2.add_constraint(x >= 0);
  ph2.add_constraint(y >= 0);
  ph2.add_constraint(x <= 2);
  ph2.add_constraint(y <= 2);
  print_constraints(ph2, "*** ph2 ***");
  /*
  *** ph2 ***
  A  >= 0,
  B >= 0,
  -A >= -2,
  -B >= -2.
  */
  unsigned tp = 1;
  cout << "*** tp = " << tp << endl;
  /*
  *** tp = 1
  */
  ph1.H79_widening_assign(ph2,&tp);
  print_constraints(ph1, "*** ph1 after widening ***");
  cout << "*** tp = " << tp << endl;
  /*
  *** ph1 after widening***
  A >= 0,
  B >= 0,
  -A >= -3,
  -B >= -2.
  *** tp = 0
  */
  ph1.H79_widening_assign(ph2,&tp);
  print_constraints(ph1, "*** ph1 after widening ***");
  cout << "*** tp = " << tp << endl;
   /*
  *** ph1 after widening***
  A >= 0,
  B >= 0,
  -B >= -2.
  *** tp = 0
  */
  
  return 0;
}