#include <termination_defs.hh>

Static Public Member Functions
static void	all_affine_ranking_functions_PR (const Constraint_System &cs_before, const Constraint_System &cs_after, NNC_Polyhedron &mu_space)

static bool	one_affine_ranking_function_PR (const Constraint_System &cs_before, const Constraint_System &cs_after, Generator &mu)

static bool	one_affine_ranking_function_PR_original (const Constraint_System &cs, Generator &mu)

static void	all_affine_ranking_functions_PR_original (const Constraint_System &cs, NNC_Polyhedron &mu_space)

template<typename PSET >
static void	assign_all_inequalities_approximation (const PSET &pset_before, const PSET &pset_after, Constraint_System &cs)

Detailed Description

Definition at line 36 of file termination_defs.hh.

Member Function Documentation

void Parma_Polyhedra_Library::Termination_Helpers::all_affine_ranking_functions_PR	(	const Constraint_System &	cs_before,
		const Constraint_System &	cs_after,
		NNC_Polyhedron &	mu_space
	)

static

Definition at line 784 of file termination.cc.

Referenced by Parma_Polyhedra_Library::Implementation::Termination::all_affine_ranking_functions_PR().

                                                             {
   Constraint_System cs_eqs;
   Linear_Expression le_ineq;
   Parma_Polyhedra_Library::Implementation::Termination
     ::fill_constraint_system_PR(cs_before, cs_after, cs_eqs, le_ineq);
 
 #if PRINT_DEBUG_INFO
   Variable::output_function_type* p_default_output_function
     = Variable::get_output_function();
   Variable::set_output_function(output_function_PR);
 
   output_function_PR_r = num_constraints(cs_before);
   output_function_PR_s = num_constraints(cs_after);
 
   std::cout << "*** cs_eqs ***" << std::endl;
   using namespace IO_Operators;
   std::cout << cs_eqs << std::endl;
   std::cout << "*** le_ineq ***" << std::endl;
   std::cout << le_ineq << std::endl;
 #endif
 
   NNC_Polyhedron ph(cs_eqs);
   ph.add_constraint(le_ineq < 0);
   // u_3 corresponds to space dimensions 0, ..., s - 1.
   const dimension_type s = Implementation::num_constraints(cs_after);
   ph.remove_higher_space_dimensions(s);
 
 #if PRINT_DEBUG_INFO
   std::cout << "*** ph ***" << std::endl;
   std::cout << ph << std::endl;
 
   Variable::set_output_function(p_default_output_function);
 #endif
 
   const dimension_type n = cs_before.space_dimension();
 
   const Generator_System& gs_in = ph.generators();
   Generator_System gs_out;
   Generator_System::const_iterator gs_in_it = gs_in.begin();
   Generator_System::const_iterator gs_in_end = gs_in.end();
   if (gs_in_it == gs_in_end) {
     // The system is unsatisfiable.
     mu_space = NNC_Polyhedron(n + 1, EMPTY);
   }
   else {
     for ( ; gs_in_it != gs_in_end; ++gs_in_it) {
       const Generator& g = *gs_in_it;
       Linear_Expression le;
       le.set_space_dimension(n);
       // Set le to the multiplication of Linear_Expression(g) by E'_C.
       dimension_type row_index = 0;
       for (Constraint_System::const_iterator i = cs_after.begin(),
              cs_after_end = cs_after.end();
            i != cs_after_end;
            ++i, ++row_index) {
         Coefficient_traits::const_reference
           g_i = g.coefficient(Variable(row_index));
         if (g_i != 0) {
           le.linear_combine(i->expr, 1, -g_i, 1, n + 1);
         }
       }
 
       // Add to gs_out the transformed generator.
       switch (g.type()) {
       case Generator::LINE:
         if (!le.all_homogeneous_terms_are_zero()) {
           gs_out.insert(line(le));
         }
         break;
       case Generator::RAY:
         if (!le.all_homogeneous_terms_are_zero()) {
           gs_out.insert(ray(le));
         }
         break;
       case Generator::POINT:
         gs_out.insert(point(le, g.divisor()));
         break;
       case Generator::CLOSURE_POINT:
         gs_out.insert(closure_point(le, g.divisor()));
         break;
       }
     }
 
     mu_space = NNC_Polyhedron(gs_out);
     // mu_0 is zero.
     mu_space.add_space_dimensions_and_embed(1);
   }
 }

void Parma_Polyhedra_Library::Termination_Helpers::all_affine_ranking_functions_PR_original	(	const Constraint_System &	cs,
		NNC_Polyhedron &	mu_space
	)

static

Definition at line 877 of file termination.cc.

Referenced by Parma_Polyhedra_Library::Implementation::Termination::all_affine_ranking_functions_PR_original().

                                                                      {
   PPL_ASSERT(cs.space_dimension() % 2 == 0);
   const dimension_type n = cs.space_dimension() / 2;
   const dimension_type m = Implementation::num_constraints(cs);
 
   if (m == 0) {
     // If there are no constraints at all, we have non-termination,
     // i.e., no affine ranking function at all.
     mu_space = NNC_Polyhedron(n + 1, EMPTY);
     return;
   }
 
   Constraint_System cs_eqs;
   Linear_Expression le_ineq;
   Parma_Polyhedra_Library::Implementation::Termination
     ::fill_constraint_system_PR_original(cs, cs_eqs, le_ineq);
 
   NNC_Polyhedron ph(cs_eqs);
   ph.add_constraint(le_ineq < 0);
   // lambda_2 corresponds to space dimensions m, ..., 2*m-1.
   const Variables_Set lambda1(Variable(0), Variable(m-1));
   ph.remove_space_dimensions(lambda1);
 
 #if PRINT_DEBUG_INFO
   std::cout << "*** ph ***" << std::endl;
   std::cout << ph << std::endl;
 
   Variable::set_output_function(p_default_output_function);
 #endif
 
   const Generator_System& gs_in = ph.generators();
   Generator_System::const_iterator gs_in_it = gs_in.begin();
   Generator_System::const_iterator gs_in_end = gs_in.end();
   if (gs_in_it == gs_in_end) {
     // The system is unsatisfiable.
     mu_space = NNC_Polyhedron(n + 1, EMPTY);
   }
   else {
     Generator_System gs_out;
     for ( ; gs_in_it != gs_in_end; ++gs_in_it) {
       const Generator& g = *gs_in_it;
       Linear_Expression le;
       le.set_space_dimension(n);
       // Set le to the multiplication of Linear_Expression(g) by E'_C.
       dimension_type row_index = 0;
       for (Constraint_System::const_iterator i = cs.begin(),
              cs_end = cs.end(); i != cs_end; ++i, ++row_index) {
         const Variable lambda2_i(row_index);
         Coefficient_traits::const_reference g_i = g.coefficient(lambda2_i);
         if (g_i != 0) {
           le.linear_combine(i->expr, 1, -g_i, 1, n + 1);
         }
       }
 
       // Add to gs_out the transformed generator.
       switch (g.type()) {
       case Generator::LINE:
         if (!le.all_homogeneous_terms_are_zero()) {
           gs_out.insert(line(le));
         }
         break;
       case Generator::RAY:
         if (!le.all_homogeneous_terms_are_zero()) {
           gs_out.insert(ray(le));
         }
         break;
       case Generator::POINT:
         gs_out.insert(point(le, g.divisor()));
         break;
       case Generator::CLOSURE_POINT:
         gs_out.insert(closure_point(le, g.divisor()));
         break;
       }
     }
 
     mu_space = NNC_Polyhedron(gs_out);
     // mu_0 is zero.
     mu_space.add_space_dimensions_and_embed(1);
   }
 }

template<typename PSET >

void Parma_Polyhedra_Library::Termination_Helpers::assign_all_inequalities_approximation	(	const PSET &	pset_before,
		const PSET &	pset_after,
		Constraint_System &	cs
	)

static

Definition at line 224 of file termination_templates.hh.

References Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation(), Parma_Polyhedra_Library::Constraint_System::begin(), Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::Constraint_System::shift_space_dimensions(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().

                                                                {
   Implementation::Termination
     ::assign_all_inequalities_approximation(pset_before, cs);
   cs.shift_space_dimensions(Variable(0), cs.space_dimension());
   Constraint_System cs_after;
   Implementation::Termination
     ::assign_all_inequalities_approximation(pset_after, cs_after);
   // FIXME: provide an "append" for constraint systems.
   for (Constraint_System::const_iterator i = cs_after.begin(),
          cs_after_end = cs_after.end(); i != cs_after_end; ++i) {
     cs.insert(*i);
   }
 }

bool Parma_Polyhedra_Library::Termination_Helpers::one_affine_ranking_function_PR	(	const Constraint_System &	cs_before,
		const Constraint_System &	cs_after,
		Generator &	mu
	)

static

Definition at line 675 of file termination.cc.

                                                 {
   Constraint_System cs_mip;
   Linear_Expression le_ineq;
   Parma_Polyhedra_Library::Implementation::Termination
     ::fill_constraint_system_PR(cs_before, cs_after, cs_mip, le_ineq);
 
 #if PRINT_DEBUG_INFO
   Variable::output_function_type* p_default_output_function
     = Variable::get_output_function();
   Variable::set_output_function(output_function_PR);
 
   output_function_PR_r = num_constraints(cs_before);
   output_function_PR_s = num_constraints(cs_after);
 
   std::cout << "*** cs_mip ***" << std::endl;
   using namespace IO_Operators;
   std::cout << cs_mip << std::endl;
   std::cout << "*** le_ineq ***" << std::endl;
   std::cout << le_ineq << std::endl;
 
   Variable::set_output_function(p_default_output_function);
 #endif
 
   // Turn minimization problem into satisfiability.
   cs_mip.insert(le_ineq <= -1);
 
   const MIP_Problem mip(cs_mip.space_dimension(), cs_mip);
   if (!mip.is_satisfiable()) {
     return false;
   }
 
   const Generator& fp = mip.feasible_point();
   PPL_ASSERT(fp.is_point());
 
   // u_3 corresponds to space dimensions 0, ..., s - 1.
   const dimension_type n = cs_before.space_dimension();
   // mu_0 is zero: properly set space dimension.
   Linear_Expression le;
   le.set_space_dimension(1 + n);
   // Multiply u_3 by E'_C to obtain mu_1, ..., mu_n.
   dimension_type row_index = 0;
   for (Constraint_System::const_iterator i = cs_after.begin(),
          cs_after_end = cs_after.end();
        i != cs_after_end;
        ++i, ++row_index) {
     Coefficient_traits::const_reference
       fp_i = fp.coefficient(Variable(row_index));
     if (fp_i != 0) {
       le.linear_combine(i->expr, 1, -fp_i, 1, n + 1);
     }
   }
   // Note that we can neglect the divisor of `fp' since it is positive.
   mu = point(le);
   return true;
 }

bool Parma_Polyhedra_Library::Termination_Helpers::one_affine_ranking_function_PR_original	(	const Constraint_System &	cs,
		Generator &	mu
	)

static

Definition at line 735 of file termination.cc.

Referenced by Parma_Polyhedra_Library::Implementation::Termination::one_affine_ranking_function_PR_original().

                                                          {
   PPL_ASSERT(cs.space_dimension() % 2 == 0);
   const dimension_type n = cs.space_dimension() / 2;
   const dimension_type m = Implementation::num_constraints(cs);
 
   Constraint_System cs_mip;
   Linear_Expression le_ineq;
   Parma_Polyhedra_Library::Implementation::Termination
     ::fill_constraint_system_PR_original(cs, cs_mip, le_ineq);
 
 #if PRINT_DEBUG_INFO
   std::cout << "*** cs_mip ***" << std::endl;
   using namespace IO_Operators;
   std::cout << cs_mip << std::endl;
   std::cout << "*** le_ineq ***" << std::endl;
   std::cout << le_ineq << std::endl;
 #endif
 
   // Turn minimization problem into satisfiability.
   cs_mip.insert(le_ineq <= -1);
 
   const MIP_Problem mip = MIP_Problem(cs_mip.space_dimension(), cs_mip);
   if (!mip.is_satisfiable()) {
     return false;
   }
   const Generator& fp = mip.feasible_point();
   PPL_ASSERT(fp.is_point());
   // mu_0 is zero: properly set space dimension.
   Linear_Expression le;
   le.set_space_dimension(1 + n);
   // Multiply -lambda_2 by A' to obtain mu_1, ..., mu_n.
   // lambda_2 corresponds to space dimensions m, ..., 2*m - 1.
   dimension_type row_index = m;
   for (Constraint_System::const_iterator i = cs.begin(),
          cs_end = cs.end(); i != cs_end; ++i, ++row_index) {
     const Variable lambda_2(row_index);
     Coefficient_traits::const_reference fp_i = fp.coefficient(lambda_2);
     if (fp_i != 0) {
       le.linear_combine(i->expr, 1, -fp_i, 1, n + 1);
     }
   }
   // Note that we can neglect the divisor of `fp' since it is positive.
   mu = point(le);
   return true;
 }

The documentation for this class was generated from the following files:

Static Public Member Functions

Detailed Description

Member Function Documentation