Functions
void	assign_all_inequalities_approximation (const Constraint_System &cs_in, Constraint_System &cs_out)

template<>
void	assign_all_inequalities_approximation (const C_Polyhedron &ph, Constraint_System &cs)

void	fill_constraint_systems_MS (const Constraint_System &cs, Constraint_System &cs_out1, Constraint_System &cs_out2)
	Fill the constraint system(s) for the application of the Mesnard and Serebrenik improved termination tests. More...

void	fill_constraint_system_PR (const Constraint_System &cs_before, const Constraint_System &cs_after, Constraint_System &cs_out, Linear_Expression &le_out)
	Fill the constraint system(s) for the application of the Podelski and Rybalchenko improved termination tests. More...

void	fill_constraint_system_PR_original (const Constraint_System &cs, Constraint_System &cs_out, Linear_Expression &le_out)

bool	termination_test_MS (const Constraint_System &cs)

bool	one_affine_ranking_function_MS (const Constraint_System &cs, Generator &mu)

void	all_affine_ranking_functions_MS (const Constraint_System &cs, C_Polyhedron &mu_space)

void	all_affine_quasi_ranking_functions_MS (const Constraint_System &cs, C_Polyhedron &decreasing_mu_space, C_Polyhedron &bounded_mu_space)

bool	termination_test_PR_original (const Constraint_System &cs)

bool	termination_test_PR (const Constraint_System &cs_before, const Constraint_System &cs_after)

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

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

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

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

template<typename PSET >
void	assign_all_inequalities_approximation (const PSET &pset, Constraint_System &cs)

Function Documentation

void Parma_Polyhedra_Library::Implementation::Termination::all_affine_quasi_ranking_functions_MS	(	const Constraint_System &	cs,
		C_Polyhedron &	decreasing_mu_space,
		C_Polyhedron &	bounded_mu_space
	)

Definition at line 558 of file termination.cc.

Referenced by Parma_Polyhedra_Library::all_affine_quasi_ranking_functions_MS(), and Parma_Polyhedra_Library::all_affine_quasi_ranking_functions_MS_2().

                                                                       {
   Constraint_System cs_out1;
   Constraint_System cs_out2;
   fill_constraint_systems_MS(cs, cs_out1, cs_out2);
 
   C_Polyhedron ph1(cs_out1);
   C_Polyhedron ph2(cs_out2);
   const dimension_type n = cs.space_dimension() / 2;
   ph1.remove_higher_space_dimensions(n);
   ph1.add_space_dimensions_and_embed(1);
   ph2.remove_higher_space_dimensions(n+1);
 
 #if PRINT_DEBUG_INFO
   Variable::output_function_type* p_default_output_function
     = Variable::get_output_function();
   Variable::set_output_function(output_function_MS);
 
   output_function_MS_n = n;
   output_function_MS_m = num_constraints(cs);
 
   std::cout << "*** ph1 projected ***" << std::endl;
   output_function_MS_which = 4;
   using namespace IO_Operators;
   std::cout << ph1.minimized_constraints() << std::endl;
 
   std::cout << "*** ph2 projected ***" << std::endl;
   std::cout << ph2.minimized_constraints() << std::endl;
 
   Variable::set_output_function(p_default_output_function);
 #endif
 
   decreasing_mu_space.m_swap(ph1);
   bounded_mu_space.m_swap(ph2);
 }

void Parma_Polyhedra_Library::Implementation::Termination::all_affine_ranking_functions_MS	(	const Constraint_System &	cs,
		C_Polyhedron &	mu_space
	)

Definition at line 514 of file termination.cc.

Referenced by Parma_Polyhedra_Library::all_affine_ranking_functions_MS(), and Parma_Polyhedra_Library::all_affine_ranking_functions_MS_2().

                                                         {
   Constraint_System cs_out1;
   Constraint_System cs_out2;
   fill_constraint_systems_MS(cs, cs_out1, cs_out2);
 
   C_Polyhedron ph1(cs_out1);
   C_Polyhedron ph2(cs_out2);
   const dimension_type n = cs.space_dimension() / 2;
   ph1.remove_higher_space_dimensions(n);
   ph1.add_space_dimensions_and_embed(1);
   ph2.remove_higher_space_dimensions(n+1);
 
 #if PRINT_DEBUG_INFO
   Variable::output_function_type* p_default_output_function
     = Variable::get_output_function();
   Variable::set_output_function(output_function_MS);
 
   output_function_MS_n = n;
   output_function_MS_m = num_constraints(cs);
 
   std::cout << "*** ph1 projected ***" << std::endl;
   output_function_MS_which = 4;
   using namespace IO_Operators;
   std::cout << ph1.minimized_constraints() << std::endl;
 
   std::cout << "*** ph2 projected ***" << std::endl;
   std::cout << ph2.minimized_constraints() << std::endl;
 #endif
 
   ph1.intersection_assign(ph2);
 
 #if PRINT_DEBUG_INFO
   std::cout << "*** intersection ***" << std::endl;
   using namespace IO_Operators;
   std::cout << ph1.minimized_constraints() << std::endl;
 
   Variable::set_output_function(p_default_output_function);
 #endif
 
   mu_space.m_swap(ph1);
 }

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

Definition at line 656 of file termination.cc.

References Parma_Polyhedra_Library::Termination_Helpers::all_affine_ranking_functions_PR().

Referenced by Parma_Polyhedra_Library::all_affine_ranking_functions_PR_2().

                                                           {
   Termination_Helpers::all_affine_ranking_functions_PR(cs_before, cs_after,
                                                        mu_space);
 }

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

Definition at line 664 of file termination.cc.

References Parma_Polyhedra_Library::Termination_Helpers::all_affine_ranking_functions_PR_original().

Referenced by Parma_Polyhedra_Library::all_affine_ranking_functions_PR().

                                                                    {
   Termination_Helpers::all_affine_ranking_functions_PR_original(cs, mu_space);
 }

void Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation	(	const Constraint_System &	cs_in,
		Constraint_System &	cs_out
	)

Definition at line 35 of file termination.cc.

References Parma_Polyhedra_Library::Constraint_System::begin(), c, Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Constraint::expression(), Parma_Polyhedra_Library::Constraint_System::has_equalities(), Parma_Polyhedra_Library::Constraint_System::has_strict_inequalities(), Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::Constraint::is_equality(), and Parma_Polyhedra_Library::Constraint::is_strict_inequality().

                                                                  {
   if (cs_in.has_strict_inequalities() || cs_in.has_equalities()) {
     // Here we have some strict inequality and/or equality constraints:
     // translate them into non-strict inequality constraints.
     for (Constraint_System::const_iterator i = cs_in.begin(),
            i_end = cs_in.end(); i != i_end; ++i) {
       const Constraint& c = *i;
       if (c.is_equality()) {
         // Insert the two corresponding opposing inequalities.
         const Linear_Expression expr(c.expression());
         cs_out.insert(expr >= 0);
         cs_out.insert(expr <= 0);
       }
       else if (c.is_strict_inequality()) {
         // Insert the non-strict approximation.
         const Linear_Expression expr(c.expression());
         cs_out.insert(expr >= 0);
       }
       else {
         // Insert as is.
         cs_out.insert(c);
       }
     }
   }
   else {
     // No strict inequality and no equality constraints.
     cs_out = cs_in;
   }
 }

template<>

void Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation	(	const C_Polyhedron &	ph,
		Constraint_System &	cs
	)

Definition at line 68 of file termination.cc.

References Parma_Polyhedra_Library::Constraint_System::begin(), c, Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Constraint::expression(), Parma_Polyhedra_Library::Constraint_System::has_equalities(), Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::Constraint::is_equality(), and Parma_Polyhedra_Library::Polyhedron::minimized_constraints().

                                                              {
   const Constraint_System& ph_cs = ph.minimized_constraints();
   if (ph_cs.has_equalities()) {
     // Translate equalities into inequalities.
     for (Constraint_System::const_iterator i = ph_cs.begin(),
            i_end = ph_cs.end(); i != i_end; ++i) {
       const Constraint& c = *i;
       if (c.is_equality()) {
         // Insert the two corresponding opposing inequalities.
         const Linear_Expression expr(c.expression());
         cs.insert(expr >= 0);
         cs.insert(expr <= 0);
       }
       else {
         // Insert as is.
         cs.insert(c);
       }
     }
   }
   else {
     // No equality constraints (and no strict inequalities).
     cs = ph_cs;
   }
 }

template<typename PSET >

void Parma_Polyhedra_Library::Implementation::Termination::assign_all_inequalities_approximation	(	const PSET &	pset,
		Constraint_System &	cs
	)

inline

Definition at line 166 of file termination_templates.hh.

References assign_all_inequalities_approximation().

Referenced by Parma_Polyhedra_Library::all_affine_quasi_ranking_functions_MS_2(), Parma_Polyhedra_Library::all_affine_ranking_functions_MS_2(), Parma_Polyhedra_Library::Termination_Helpers::assign_all_inequalities_approximation(), Parma_Polyhedra_Library::one_affine_ranking_function_MS_2(), and Parma_Polyhedra_Library::termination_test_MS_2().

                                                              {
   assign_all_inequalities_approximation(pset.minimized_constraints(), cs);
 }

void Parma_Polyhedra_Library::Implementation::Termination::fill_constraint_system_PR	(	const Constraint_System &	cs_before,
		const Constraint_System &	cs_after,
		Constraint_System &	cs_out,
		Linear_Expression &	le_out
	)

Fill the constraint system(s) for the application of the Podelski and Rybalchenko improved termination tests.

Parameters

cs_before	The input constraint system describing the state before the execution of the loop body, where variables indices are allocated as follows: $x_1, \ldots, x_n$ go onto space dimensions $0, \ldots, n-1$ . The system does not contain any equality.
cs_after	The input constraint system describing the state after the execution of the loop body, where variables indices are allocated as follows: $x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ , $x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ . The system does not contain any equality.
cs_out	The output constraint system, where variables indices are allocated as follows: goes onto space dimensions $0, \ldots, s-1$ ; goes onto space dimensions $s, \ldots, s+r-1$ ; goes onto space dimensions $s+r, \ldots, s+2r-1$ .

The improved Podelski-Rybalchenko method described in the paper is based on a loop encoding of the form

$\begin{pmatrix} A_B & \vect{0} \\ A_C & A'_C \end{pmatrix} \begin{pmatrix} \vect{x} \\ \vect{x}' \end{pmatrix} \leq \begin{pmatrix} \vect{b}_B \\ \vect{b}_C \end{pmatrix},$

where $A_B \in \Qset^{r \times n}$ , $A_C \in \Qset^{s \times n}$ , $A'_C \in \Qset^{s \times n}$ , $\vect{b}_B \in \Qset^r$ , $\vect{b}_C \in \Qset^s$ . The corresponding system is:

$\begin{aligned} (\vect{v}_1-\vect{v}_2)^\transpose A_B - \vect{v}_3^\transpose A_C &= \vect{0}^\transpose, \\ \vect{v}_2^\transpose A_B + \vect{v}_3^\transpose (A_C+A_C') &= \vect{0}^\transpose, \\ \vect{v}_2 \vect{b}_B + \vect{v}_3 \vect{b}_C &< 0, \end{aligned}$

where $\vect{v}_1 \in \Qset_+^r$ , $\vect{v}_2 \in \Qset_+^r$ , $\vect{v}_3 \in \Qset_+^s$ . The space of ranking functions is then spanned by $\vect{v}_3^\transpose A_C' \vect x$ .

In contrast, our encoding is of the form

$\begin{pmatrix} \vect{0} & E_B \\ E'_C & E_C \end{pmatrix} \begin{pmatrix} \vect{x}' \\ \vect{x} \end{pmatrix} + \begin{pmatrix} \vect{d}_B \\ \vect{d}_C \end{pmatrix} \geq \vect{0},$

where ${E}_B = -{A}_B$ , ${E}_C = -{A}_C$ , ${E}'_C = -{A}'_C$ , $\vect{d}_B = \vect{b}_B$ and $\vect{d}_C = \vect{b}_C$ . The corresponding system is:

$\begin{aligned} (\vect{u}_1-\vect{u}_2)^\transpose E_B - \vect{u}_3^\transpose E_C &= \vect{0}^\transpose, \\ \vect{u}_2^\transpose E_B + \vect{u}_3^\transpose (E_C+E_C') &= \vect{0}^\transpose, \\ \vect{u}_2 \vect{d}_B + \vect{u}_3 \vect{d}_C &> 0, \end{aligned}$

where $\vect{u}_1 \in \Qset_-^r$ , $\vect{u}_2 \in \Qset_-^r$ , $\vect{u}_3 \in \Qset_-^s$ . The space of ranking functions is then spanned by $\vect{u}_3^\transpose E_C' \vect x$ .

Parameters

le_out The expression to be minimized in the context of cs_out: a value of or less entails termination.

Definition at line 348 of file termination.cc.

Referenced by Parma_Polyhedra_Library::Termination_Helpers::all_affine_ranking_functions_PR(), Parma_Polyhedra_Library::Termination_Helpers::one_affine_ranking_function_PR(), and termination_test_PR().

                                                      {
   PPL_ASSERT(cs_after.space_dimension() % 2 == 0);
   PPL_ASSERT(2*cs_before.space_dimension() == cs_after.space_dimension());
   const dimension_type n = cs_before.space_dimension();
   const dimension_type r = num_constraints(cs_before);
   const dimension_type s = num_constraints(cs_after);
   const dimension_type m = r + s;
 
   // Make sure linear expressions are not reallocated multiple times.
   if (m > 0) {
     le_out.set_space_dimension(m + r);
   }
   std::vector<Linear_Expression> les_eq(2*n, le_out);
 
   dimension_type row_index = 0;
   for (Constraint_System::const_iterator i = cs_before.begin(),
          cs_before_end = cs_before.end();
        i != cs_before_end;
        ++i, ++row_index) {
     const Variable u1_i(m + row_index);
     const Variable u2_i(s + row_index);
     const Constraint::expr_type e_i = i->expression();
     for (Constraint::expr_type::const_iterator
            j = e_i.begin(), j_end = e_i.end(); j != j_end; ++j) {
       Coefficient_traits::const_reference A_ij_B = *j;
       const Variable v = j.variable();
       // (u1 - u2) A_B, in the context of j-th constraint.
       add_mul_assign(les_eq[v.id()], A_ij_B, u1_i);
       sub_mul_assign(les_eq[v.id()], A_ij_B, u2_i);
       // u2 A_B, in the context of (j+n)-th constraint.
       add_mul_assign(les_eq[v.id() + n], A_ij_B, u2_i);
     }
     Coefficient_traits::const_reference b_B = e_i.inhomogeneous_term();
     if (b_B != 0) {
       // u2 b_B, in the context of the strict inequality constraint.
       add_mul_assign(le_out, b_B, u2_i);
     }
   }
 
   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) {
     const Variable u3_i(row_index);
     const Constraint::expr_type e_i = i->expression();
     for (Constraint::expr_type::const_iterator
            j = e_i.lower_bound(Variable(n)),
            j_end = e_i.end(); j != j_end; ++j) {
       Coefficient_traits::const_reference A_ij_C = *j;
       const Variable v = j.variable();
       // - u3 A_C, in the context of the j-th constraint.
       sub_mul_assign(les_eq[v.id() - n], A_ij_C, u3_i);
       // u3 A_C, in the context of the (j+n)-th constraint.
       add_mul_assign(les_eq[v.id()], A_ij_C, u3_i);
     }
     for (Constraint::expr_type::const_iterator j = e_i.begin(),
            j_end = e_i.lower_bound(Variable(n)); j != j_end; ++j) {
       Coefficient_traits::const_reference Ap_ij_C = *j;
       // u3 Ap_C, in the context of the (j+n)-th constraint.
       add_mul_assign(les_eq[j.variable().id() + n], Ap_ij_C, u3_i);
     }
     Coefficient_traits::const_reference b_C = e_i.inhomogeneous_term();
     if (b_C != 0) {
       // u3 b_C, in the context of the strict inequality constraint.
       add_mul_assign(le_out, b_C, u3_i);
     }
   }
 
   // Add the nonnegativity constraints for u_1, u_2 and u_3.
   for (dimension_type i = s + 2*r; i-- > 0; ) {
     cs_out.insert(Variable(i) >= 0);
   }
 
   for (dimension_type j = 2*n; j-- > 0; ) {
     cs_out.insert(les_eq[j] == 0);
   }
 }

void Parma_Polyhedra_Library::Implementation::Termination::fill_constraint_system_PR_original	(	const Constraint_System &	cs,
		Constraint_System &	cs_out,
		Linear_Expression &	le_out
	)

Definition at line 431 of file termination.cc.

Referenced by Parma_Polyhedra_Library::Termination_Helpers::all_affine_ranking_functions_PR_original(), Parma_Polyhedra_Library::Termination_Helpers::one_affine_ranking_function_PR_original(), and termination_test_PR_original().

                                                               {
   PPL_ASSERT(cs.space_dimension() % 2 == 0);
   const dimension_type n = cs.space_dimension() / 2;
   const dimension_type m = num_constraints(cs);
 
   // Make sure linear expressions are not reallocated multiple times.
   if (m > 0) {
     le_out.set_space_dimension(2*m);
   }
   std::vector<Linear_Expression> les_eq(3*n, le_out);
 
   dimension_type row_index = 0;
   for (Constraint_System::const_iterator i = cs.begin(),
          cs_end = cs.end(); i != cs_end; ++i, ++row_index) {
     const Constraint::expr_type e_i = i->expression();
     const Variable lambda1_i(row_index);
     const Variable lambda2_i(m + row_index);
     for (Constraint::expr_type::const_iterator j = e_i.begin(),
           j_end = e_i.lower_bound(Variable(n)); j != j_end; ++j) {
       Coefficient_traits::const_reference Ap_ij = *j;
       const Variable v = j.variable();
       // lambda_1 A'
       add_mul_assign(les_eq[v.id()], Ap_ij, lambda1_i);
       // lambda_2 A'
       add_mul_assign(les_eq[v.id()+n+n], Ap_ij, lambda2_i);
     }
     for (Constraint::expr_type::const_iterator
            j = e_i.lower_bound(Variable(n)),
            j_end = e_i.end(); j != j_end; ++j) {
       Coefficient_traits::const_reference A_ij = *j;
       const Variable v = j.variable();
       // (lambda_1 - lambda_2) A
       add_mul_assign(les_eq[v.id()], A_ij, lambda1_i);
       sub_mul_assign(les_eq[v.id()], A_ij, lambda2_i);
       // lambda_2 A
       add_mul_assign(les_eq[v.id()+n], A_ij, lambda2_i);
     }
     Coefficient_traits::const_reference b = e_i.inhomogeneous_term();
     if (b != 0) {
       // lambda2 b
       add_mul_assign(le_out, b, lambda2_i);
     }
   }
 
   // Add the non-negativity constraints for lambda_1 and lambda_2.
   for (dimension_type i = 2*m; i-- > 0; ) {
     cs_out.insert(Variable(i) >= 0);
   }
 
   for (dimension_type j = 3*n; j-- > 0; ) {
     cs_out.insert(les_eq[j] == 0);
   }
 }

void Parma_Polyhedra_Library::Implementation::Termination::fill_constraint_systems_MS	(	const Constraint_System &	cs,
		Constraint_System &	cs_out1,
		Constraint_System &	cs_out2
	)

Fill the constraint system(s) for the application of the Mesnard and Serebrenik improved termination tests.

Parameters

cs	The input constraint system, where variables indices are allocated as follows: $x'_1, \ldots, x'_n$ go onto space dimensions $0, \ldots, n-1$ , $x_1, \ldots, x_n$ go onto space dimensions $n, \ldots, 2n-1$ . The system does not contain any equality.
cs_out1	The first output constraint system.
cs_out2	The second output constraint system, if any: it may be an alias for `cs_out1`.

The allocation of variable indices in the output constraint systems cs_out1 and cs_out2 is as follows, where $m$ is the number of constraints in cs:

$\mu_1, \ldots, \mu_n$ go onto space dimensions $0, \ldots, n-1$ ;
$\mu_0$ goes onto space dimension ;
$y_1, \ldots, y_m$ go onto space dimensions $n+1, \ldots, n+m$ ;

if we use the same constraint system, that is &cs_out1 == &cs_out2, then

$z_1, ..., z_m, z_{m+1}, z_{m+2}$ go onto space dimensions ;

otherwise

$z_1, ..., z_m, z_{m+1}, z_{m+2}$ go onto space dimensions .

Definition at line 134 of file termination.cc.

Referenced by all_affine_quasi_ranking_functions_MS(), all_affine_ranking_functions_MS(), one_affine_ranking_function_MS(), and termination_test_MS().

                                                        {
   PPL_ASSERT(cs.space_dimension() % 2 == 0);
   const dimension_type n = cs.space_dimension() / 2;
   const dimension_type m = num_constraints(cs);
 
 #if PRINT_DEBUG_INFO
   Variable::output_function_type* p_default_output_function
     = Variable::get_output_function();
   Variable::set_output_function(output_function_MS);
 
   output_function_MS_n = n;
   output_function_MS_m = m;
 
   std::cout << "*** cs ***" << std::endl;
   output_function_MS_which = 0;
   using namespace IO_Operators;
   std::cout << cs << std::endl;
 #endif
 
   const dimension_type y_begin = n+1;
   const dimension_type z_begin = y_begin + ((&cs_out1 == &cs_out2) ? m : 0);
 
   // Make sure linear expressions have the correct space dimension.
   Linear_Expression y_le;
   y_le.set_space_dimension(y_begin + m);
   Linear_Expression z_le;
   z_le.set_space_dimension(z_begin + m + 2);
   std::vector<Linear_Expression> y_les(2*n, y_le);
   std::vector<Linear_Expression> z_les(2*n + 1, z_le);
 
   dimension_type y = y_begin;
   dimension_type z = z_begin;
   for (Constraint_System::const_iterator i = cs.begin(),
          cs_end = cs.end(); i != cs_end; ++i) {
     const Variable v_y(y);
     const Variable v_z(z);
     ++y;
     ++z;
     cs_out1.insert(v_y >= 0);
     cs_out2.insert(v_z >= 0);
     const Constraint& c_i = *i;
     Coefficient_traits::const_reference b_i = c_i.inhomogeneous_term();
     if (b_i != 0) {
       // Note that b_i is to the left ot the relation sign, hence here
       // we have -= and not += just to avoid negating b_i.
       sub_mul_assign(y_le, b_i, v_y);
       sub_mul_assign(z_le, b_i, v_z);
     }
     for (Constraint::expr_type::const_iterator j = c_i.expression().begin(),
           j_end = c_i.expression().end(); j != j_end; ++j) {
       Coefficient_traits::const_reference a_i_j = *j;
       const Variable v = j.variable();
       add_mul_assign(y_les[v.id()], a_i_j, v_y);
       add_mul_assign(z_les[v.id()], a_i_j, v_z);
     }
   }
   z_le += Variable(z);
   z_les[2*n] += Variable(z);
   cs_out2.insert(Variable(z) >= 0);
   ++z;
   z_le -= Variable(z);
   z_les[2*n] -= Variable(z);
   cs_out2.insert(Variable(z) >= 0);
   cs_out1.insert(y_le >= 1);
   cs_out2.insert(z_le >= 0);
   dimension_type j = 2*n;
   while (j-- > n) {
     cs_out1.insert(y_les[j] == Variable(j-n));
     cs_out2.insert(z_les[j] == Variable(j-n));
   }
   ++j;
   while (j-- > 0) {
     cs_out1.insert(y_les[j] == -Variable(j));
     cs_out2.insert(z_les[j] == 0);
   }
   cs_out2.insert(z_les[2*n] == Variable(n));
 
 #if PRINT_DEBUG_INFO
   if (&cs_out1 == &cs_out2) {
     std::cout << "*** cs_mip ***" << std::endl;
     output_function_MS_which = 3;
     using namespace IO_Operators;
     std::cout << cs_mip << std::endl;
   }
   else {
     std::cout << "*** cs_out1 ***" << std::endl;
     output_function_MS_which = 1;
     using namespace IO_Operators;
     std::cout << cs_out1 << std::endl;
 
     std::cout << "*** cs_out2 ***" << std::endl;
     output_function_MS_which = 2;
     using namespace IO_Operators;
     std::cout << cs_out2 << std::endl;
   }
 
   Variable::set_output_function(p_default_output_function);
 #endif
 }

bool Parma_Polyhedra_Library::Implementation::Termination::one_affine_ranking_function_MS	(	const Constraint_System &	cs,
		Generator &	mu
	)

Definition at line 497 of file termination.cc.

References Parma_Polyhedra_Library::Generator::divisor(), Parma_Polyhedra_Library::Generator::expression(), Parma_Polyhedra_Library::MIP_Problem::feasible_point(), fill_constraint_systems_MS(), Parma_Polyhedra_Library::Generator::is_point(), Parma_Polyhedra_Library::MIP_Problem::is_satisfiable(), Parma_Polyhedra_Library::Boundary_NS::le(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().

Referenced by Parma_Polyhedra_Library::one_affine_ranking_function_MS(), and Parma_Polyhedra_Library::one_affine_ranking_function_MS_2().

                                                                            {
   Constraint_System cs_mip;
   fill_constraint_systems_MS(cs, cs_mip, cs_mip);
 
   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());
   const dimension_type n = cs.space_dimension() / 2;
   const Linear_Expression le(fp.expression(), n + 1);
   mu = point(le, fp.divisor());
   return true;
 }

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

Definition at line 642 of file termination.cc.

Referenced by Parma_Polyhedra_Library::one_affine_ranking_function_PR_2().

                                               {
   return Termination_Helpers
     ::one_affine_ranking_function_PR(cs_before, cs_after, mu);
 }

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

Definition at line 650 of file termination.cc.

References Parma_Polyhedra_Library::Termination_Helpers::one_affine_ranking_function_PR_original().

Referenced by Parma_Polyhedra_Library::one_affine_ranking_function_PR().

                                                        {
   return Termination_Helpers::one_affine_ranking_function_PR_original(cs, mu);
 }

bool Parma_Polyhedra_Library::Implementation::Termination::termination_test_MS ( const Constraint_System & cs )

Definition at line 488 of file termination.cc.

References fill_constraint_systems_MS(), Parma_Polyhedra_Library::MIP_Problem::is_satisfiable(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().

Referenced by Parma_Polyhedra_Library::termination_test_MS(), and Parma_Polyhedra_Library::termination_test_MS_2().

                                                  {
   Constraint_System cs_mip;
   fill_constraint_systems_MS(cs, cs_mip, cs_mip);
 
   const MIP_Problem mip = MIP_Problem(cs_mip.space_dimension(), cs_mip);
   return mip.is_satisfiable();
 }

bool Parma_Polyhedra_Library::Implementation::Termination::termination_test_PR	(	const Constraint_System &	cs_before,
		const Constraint_System &	cs_after
	)

Definition at line 611 of file termination.cc.

References fill_constraint_system_PR(), Parma_Polyhedra_Library::Variable::get_output_function(), Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::MIP_Problem::is_satisfiable(), Parma_Polyhedra_Library::Implementation::num_constraints(), Parma_Polyhedra_Library::Variable::set_output_function(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().

Referenced by Parma_Polyhedra_Library::termination_test_PR_2().

                                                        {
   Constraint_System cs_mip;
   Linear_Expression le_ineq;
   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);
   return mip.is_satisfiable();
 }

bool Parma_Polyhedra_Library::Implementation::Termination::termination_test_PR_original ( const Constraint_System & cs )

Definition at line 596 of file termination.cc.

References fill_constraint_system_PR_original(), Parma_Polyhedra_Library::MIP_Problem::is_satisfiable(), and Parma_Polyhedra_Library::Constraint_System::space_dimension().

Referenced by Parma_Polyhedra_Library::termination_test_PR().

                                                           {
   PPL_ASSERT(cs.space_dimension() % 2 == 0);
 
   Constraint_System cs_mip;
   Linear_Expression le_ineq;
   fill_constraint_system_PR_original(cs, cs_mip, le_ineq);
 
   // Turn minimization problem into satisfiability.
   cs_mip.insert(le_ineq <= -1);
 
   const MIP_Problem mip(cs_mip.space_dimension(), cs_mip);
   return mip.is_satisfiable();
 }

Functions

Function Documentation