termination_defs.hh

Go to the documentation of this file.

/* Utilities for termination analysis: declarations.
   Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
   Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)

This file is part of the Parma Polyhedra Library (PPL).

The PPL is free software; you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by the
Free Software Foundation; either version 3 of the License, or (at your
option) any later version.

The PPL is distributed in the hope that it will be useful, but WITHOUT
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software Foundation,
Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.

For the most up-to-date information see the Parma Polyhedra Library
site: http://bugseng.com/products/ppl/ . */

#ifndef PPL_termination_defs_hh
#define PPL_termination_defs_hh 1

#include "termination_types.hh"

#include "Generator_types.hh"
#include "C_Polyhedron_types.hh"
#include "NNC_Polyhedron_types.hh"
#include "Constraint_System_types.hh"

namespace Parma_Polyhedra_Library {

class Termination_Helpers {
public:
  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);
}; // class Termination_Helpers



template <typename PSET>
bool
termination_test_MS(const PSET& pset);

template <typename PSET>
bool
termination_test_MS_2(const PSET& pset_before, const PSET& pset_after);

template <typename PSET>
bool
one_affine_ranking_function_MS(const PSET& pset, Generator& mu);

template <typename PSET>
bool
one_affine_ranking_function_MS_2(const PSET& pset_before,
                                 const PSET& pset_after,
                                 Generator& mu);

template <typename PSET>
void
all_affine_ranking_functions_MS(const PSET& pset, C_Polyhedron& mu_space);

template <typename PSET>
void
all_affine_ranking_functions_MS_2(const PSET& pset_before,
                                  const PSET& pset_after,
                                  C_Polyhedron& mu_space);

template <typename PSET>
void
all_affine_quasi_ranking_functions_MS(const PSET& pset,
                                      C_Polyhedron& decreasing_mu_space,
                                      C_Polyhedron& bounded_mu_space);

template <typename PSET>
void
all_affine_quasi_ranking_functions_MS_2(const PSET& pset_before,
                                        const PSET& pset_after,
                                        C_Polyhedron& decreasing_mu_space,
                                        C_Polyhedron& bounded_mu_space);

template <typename PSET>
bool
termination_test_PR(const PSET& pset);

template <typename PSET>
bool
termination_test_PR_2(const PSET& pset_before, const PSET& pset_after);

template <typename PSET>
bool
one_affine_ranking_function_PR(const PSET& pset, Generator& mu);

template <typename PSET>
bool
one_affine_ranking_function_PR_2(const PSET& pset_before,
                                 const PSET& pset_after,
                                 Generator& mu);

template <typename PSET>
void
all_affine_ranking_functions_PR(const PSET& pset, NNC_Polyhedron& mu_space);

template <typename PSET>
void
all_affine_ranking_functions_PR_2(const PSET& pset_before,
                                  const PSET& pset_after,
                                  NNC_Polyhedron& mu_space);


} // namespace Parma_Polyhedra_Library

#include "termination_templates.hh"

#endif // !defined(PPL_termination_defs_hh)