Interfaced Polyhedron::positive_time_elapse_assign().

Various other improvements.

19 files changed, 212 insertions, 28 deletions

diff --git a/doc/definitions.dox b/doc/definitions.dox
index 1594a9d28..b5c600777 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -530,7 +530,7 @@ One possibility for precisely approximating the semantics of programs that
 operate on bounded integer variables is to follow the approach described
 in \ref SK07 "[SK07]".  The idea is to associate space dimensions to the
 <EM>unwrapped values</EM> of bounded variables.  Suppose <CODE>j</CODE>
-is a \f$w\textrm{-bit}\f$, unsigned program variable associated to a space 
+is a \f$w\textrm{-bit}\f$, unsigned program variable associated to a space
 dimension
 labeled by the variable \f$x\f$.  If \f$x\f$ is constrained by some
 numerical abstraction to take values in a set \f$S \sseq \Rset\f$, then
@@ -1483,25 +1483,25 @@ is defined as
 \f]
 
 \subsection affine_form_relation Affine Form Relations.
-Let \f$\mathbb{F}_{\mathrm{f}}\f$ be the set of floating point numbers 
-representables in a certain 
-format \f$\mathrm{f}\f$ and let \f$\mathbb{I}_\mathrm{f}\f$ be the set of 
+Let \f$\mathbb{F}_{\mathrm{f}}\f$ be the set of floating point numbers
+representables in a certain
+format \f$\mathrm{f}\f$ and let \f$\mathbb{I}_\mathrm{f}\f$ be the set of
 real intervals with bounds in \f$\mathbb{F}_{\mathrm{f}}\f$.
-We can define a <EM>floating-point interval linear form</EM> 
+We can define a <EM>floating-point interval linear form</EM>
 \f$\langle\vect{\alpha}, \vect{x}\rangle
- + \beta\f$ 
+ + \beta\f$
 as:
-        \f[\left<\vect{\alpha}, \vect{x}\right> + \beta = 
-        \alpha_0x_0 + \ldots + 
+        \f[\left<\vect{\alpha}, \vect{x}\right> + \beta =
+        \alpha_0x_0 + \ldots +
         \alpha_{n-1}x_{n-1} + \beta,\f]
 
-where \f$\beta\f$, \f$\vect{\alpha}_k \in \mathbb{I}_{\mathrm{f}}\f$ 
-for each \f$k = 0, \ldots, n - 1\f$. 
+where \f$\beta\f$, \f$\vect{\alpha}_k \in \mathbb{I}_{\mathrm{f}}\f$
+for each \f$k = 0, \ldots, n - 1\f$.
 
-Given a such linear form \f$\mathrm{lf}\f$ and a primed variable \f$x'_k\f$ the 
-<EM>affine form image</EM> operator computes the bounded affine image of a 
+Given a such linear form \f$\mathrm{lf}\f$ and a primed variable \f$x'_k\f$ the
+<EM>affine form image</EM> operator computes the bounded affine image of a
 polyhedron \f$\cP\f$ under \f$\mathrm{lb} \leq x'_k \leq \mathrm{ub}\f$, where
-\f$\mathrm{lb}\f$ and \f$\mathrm{ub}\f$ are the upper and lower bound 
+\f$\mathrm{lb}\f$ and \f$\mathrm{ub}\f$ are the upper and lower bound
 of \f$\mathrm{lf}\f$ respectively.
 
 \subsection Generalized_Affine_Relations Generalized Affine Relations.
@@ -1585,15 +1585,18 @@ Note that the above set might not be an NNC polyhedron.
 
 \subsection Positive_Time_Elapse_Operator Positive Time-Elapse Operator
 
-The <EM>positive time-elapse</EM> operator has been defined in \ref BFM11 "[BFM11,"
-\ref BFM12 "BFM12]".
+The <EM>positive time-elapse</EM> operator has been defined in
+\ref BFM11 "[BFM11,BFM12]".
 The operator provided by the library works on NNC
 polyhedra.  For any two NNC polyhedra \f$\cP, \cQ \in \Pset_n\f$, the
 positive time-elapse between \f$\cP\f$ and \f$\cQ\f$, denoted \f$ \cP
 \nearrow_{>0} \cQ\f$, is the NNC polyhedron containing exactly the set
-\f[ 
-\bigl\{\, \vect{p} + \lambda \vect{q} \in \Rset^n \bigm| \vect{p}
-\in \cP, \vect{q} \in \cQ, \lambda \in \Rset^{>0} \,\bigr\},
+\f[
+  \bigl\{\,
+    \vect{p} + \lambda \vect{q} \in \Rset^n
+  \bigm|
+    \vect{p} \in \cP, \vect{q} \in \cQ, \lambda \in \Rset^{>0}
+  \,\bigr\},
 \f]
 where \f$\Rset^{>0}\f$ denotes the set of strictly positive
 reals. Notice that, differently from the case of the time-elapse
diff --git a/interfaces/C/ppl_interface_generator_c_cc_code.m4 b/interfaces/C/ppl_interface_generator_c_cc_code.m4
index f33799527..2c45fc1a4 100644
--- a/interfaces/C/ppl_interface_generator_c_cc_code.m4
+++ b/interfaces/C/ppl_interface_generator_c_cc_code.m4
@@ -407,6 +407,27 @@ CATCH_ALL
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+`int
+ppl_@CLASS@_positive_time_elapse_assign
+(ppl_@CLASS@_t x,
+ ppl_const_@CLASS@_t y) try {
+  if (Interfaces::is_necessarily_closed_for_interfaces(*to_const(x))) {
+    C_Polyhedron& xx = static_cast<C_Polyhedron&>(*to_nonconst(x));
+    const C_Polyhedron& yy = static_cast<const C_Polyhedron&>(*to_const(y));
+    xx.positive_time_elapse_assign(yy);
+  }
+  else {
+    NNC_Polyhedron& xx = static_cast<NNC_Polyhedron&>(*to_nonconst(x));
+    const NNC_Polyhedron& yy = static_cast<const NNC_Polyhedron&>(*to_const(y));
+    xx.positive_time_elapse_assign(yy);
+  }
+  return 0;
+}
+CATCH_ALL
+
+')
+
 m4_define(`ppl_@CLASS@_@UB_EXACT@_code',
 `int
 ppl_@CLASS@_@UB_EXACT@
diff --git a/interfaces/C/ppl_interface_generator_c_h_code.m4 b/interfaces/C/ppl_interface_generator_c_h_code.m4
index b95b6ced6..14f8e998e 100644
--- a/interfaces/C/ppl_interface_generator_c_h_code.m4
+++ b/interfaces/C/ppl_interface_generator_c_h_code.m4
@@ -376,6 +376,15 @@ PPL_PROTO((ppl_@CLASS@_t x,
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+`/*! \relates ppl_@CLASS@_tag */
+int
+ppl_@CLASS@_positive_time_elapse_assign
+PPL_PROTO((ppl_@CLASS@_t x,
+           ppl_const_@CLASS@_t y));
+
+')
+
 m4_define(`ppl_@CLASS@_@UB_EXACT@_code',
 `/*! \relates ppl_@CLASS@_tag */
 int
diff --git a/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_code.m4 b/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_code.m4
index 012326606..95eccfa9e 100644
--- a/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_code.m4
+++ b/interfaces/Java/jni/ppl_interface_generator_java_classes_cc_code.m4
@@ -778,6 +778,24 @@ CATCH_ALL
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+`dnl
+JNIEXPORT jboolean JNICALL
+Java_parma_1polyhedra_1library_@1TOPOLOGY@@1CLASS@_positive_time_elapse_assign
+(JNIEnv* env, jobject j_this, jobject j_y) {
+  try {
+    @TOPOLOGY@@CPP_CLASS@* this_ptr
+      = reinterpret_cast<@TOPOLOGY@@CPP_CLASS@*>(get_ptr(env, j_this));
+    @TOPOLOGY@@CPP_CLASS@* y_ptr
+      = reinterpret_cast<@TOPOLOGY@@CPP_CLASS@*>(get_ptr(env, j_y));
+    this_ptr->positive_time_elapse_assign(*y_ptr);
+  }
+  CATCH_ALL;
+  return false;
+}
+
+')
+
 m4_define(`ppl_@CLASS@_simplify_using_context_assign_code',
 `dnl
 JNIEXPORT jboolean JNICALL
diff --git a/interfaces/Java/parma_polyhedra_library/ppl_interface_generator_java_classes_java_code.m4 b/interfaces/Java/parma_polyhedra_library/ppl_interface_generator_java_classes_java_code.m4
index 66c41944b..952d803e9 100644
--- a/interfaces/Java/parma_polyhedra_library/ppl_interface_generator_java_classes_java_code.m4
+++ b/interfaces/Java/parma_polyhedra_library/ppl_interface_generator_java_classes_java_code.m4
@@ -337,6 +337,14 @@ ___BEGIN_OF_FILE___ @CLASS@.java << ___END_OF_FILE___
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+`dnl
+___END_OF_FILE___
+___BEGIN_OF_FILE___ @CLASS@.java << ___END_OF_FILE___
+    public native void positive_time_elapse_assign(@CLASS@ p);
+
+')
+
 m4_define(`ppl_@CLASS@_simplify_using_context_assign_code',
 `dnl
 ___END_OF_FILE___
diff --git a/interfaces/Java/tests/ppl_interface_generator_java_test_java_code.m4 b/interfaces/Java/tests/ppl_interface_generator_java_test_java_code.m4
index d166ed064..784f292c6 100644
--- a/interfaces/Java/tests/ppl_interface_generator_java_test_java_code.m4
+++ b/interfaces/Java/tests/ppl_interface_generator_java_test_java_code.m4
@@ -191,6 +191,20 @@ m4_define(`ppl_@CLASS@_@BINOP@_code',
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+    `dnl
+{
+    PPL_Test.print_if_noisy("Testing positive_time_elapse_assign: ");
+    @TOPOLOGY@@CLASS@ gd1 = new @TOPOLOGY@@CLASS@(@CONSTRAINER@s1);
+    @TOPOLOGY@@CLASS@ gd2 = new @TOPOLOGY@@CLASS@(@CONSTRAINER@s2);
+    gd1.positive_time_elapse_assign(gd2);
+    report_success_or_failure(gd1.OK());
+    gd1.free();
+    gd2.free();
+}
+
+')
+
 m4_define(`ppl_@CLASS@_simplify_using_context_assign_code',
     `dnl
 {
diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4
index 3ef489c0e..89a3b2a84 100644
--- a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4
+++ b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4
@@ -264,6 +264,33 @@ CATCH_ALL
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+`dnl
+extern "C"
+CAMLprim value
+ppl_@CLASS@_positive_time_elapse_assign(value ph1, value ph2) try {
+  CAMLparam2(ph1, ph2);
+  if (Interfaces::is_necessarily_closed_for_interfaces
+        (*p_Polyhedron_val(ph1))) {
+    C_Polyhedron& xx
+      = static_cast<C_Polyhedron&>(*p_Polyhedron_val(ph1));
+    const C_Polyhedron& yy
+      = static_cast<const C_Polyhedron&>(*p_Polyhedron_val(ph2));
+    xx.positive_time_elapse_assign(yy);
+  }
+  else {
+    NNC_Polyhedron& xx
+      = static_cast<NNC_Polyhedron&>(*p_Polyhedron_val(ph1));
+    const NNC_Polyhedron& yy
+      = static_cast<const NNC_Polyhedron&>(*p_Polyhedron_val(ph2));
+    xx.positive_time_elapse_assign(yy);
+  }
+  CAMLreturn(Val_unit);
+}
+CATCH_ALL
+
+')
+
 m4_define(`ppl_@CLASS@_simplify_using_context_assign_code',
 `dnl
 extern "C"
diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4
index 472f86f24..18de75e38 100644
--- a/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4
+++ b/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4
@@ -145,6 +145,14 @@ external ppl_@CLASS@_@BINOP@:
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+`dnl
+external ppl_@CLASS@_positive_time_elapse_assign:
+  @!CLASS@ -> @!CLASS@ -> unit
+  = "ppl_@CLASS@_positive_time_elapse_assign"
+
+')
+
 m4_define(`ppl_@CLASS@_simplify_using_context_assign_code',
 `dnl
 external ppl_@CLASS@_simplify_using_context_assign:
diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4
index cb33cb6eb..cad33907d 100644
--- a/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4
+++ b/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4
@@ -132,6 +132,13 @@ val ppl_@CLASS@_@BINOP@:
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+`dnl
+val ppl_@CLASS@_positive_time_elapse_assign:
+   @!CLASS@ -> @!CLASS@ -> unit
+
+')
+
 m4_define(`ppl_@CLASS@_simplify_using_context_assign_code',
 `dnl
 val ppl_@CLASS@_simplify_using_context_assign:
diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4
index a7f739c9f..303817313 100644
--- a/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4
+++ b/interfaces/Prolog/ppl_interface_generator_prolog_cc_code.m4
@@ -1081,6 +1081,34 @@ m4_define(`ppl_@CLASS@_@BINOP@_code',
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+  `extern "C" Prolog_foreign_return_type
+  ppl_@CLASS@_positive_time_elapse_assign
+  (Prolog_term_ref t_lhs, Prolog_term_ref t_rhs) {
+  static const char* where = "ppl_@CLASS@_positive_time_elapse_assign";
+  try {
+    const Polyhedron* xlhs = term_to_handle<Polyhedron >(t_lhs, where);
+    if (Interfaces::is_necessarily_closed_for_interfaces(*xlhs)) {
+      C_Polyhedron* lhs = term_to_handle<C_Polyhedron >(t_lhs, where);
+      const C_Polyhedron* rhs = term_to_handle<C_Polyhedron >(t_rhs, where);
+      PPL_CHECK(lhs);
+      PPL_CHECK(rhs);
+      lhs->positive_time_elapse_assign(*rhs);
+    }
+    else {
+      NNC_Polyhedron* lhs = term_to_handle<NNC_Polyhedron >(t_lhs, where);
+      const NNC_Polyhedron* rhs = term_to_handle<NNC_Polyhedron >(t_rhs, where);
+      PPL_CHECK(lhs);
+      PPL_CHECK(rhs);
+      lhs->positive_time_elapse_assign(*rhs);
+    }
+    return PROLOG_SUCCESS;
+  }
+  CATCH_ALL;
+}
+
+')
+
 m4_define(`ppl_@CLASS@_simplify_using_context_assign_code',
   `extern "C" Prolog_foreign_return_type
   ppl_@CLASS@_simplify_using_context_assign
diff --git a/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4 b/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4
index e0066fa87..054ac3308 100644
--- a/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4
+++ b/interfaces/Prolog/ppl_interface_generator_prolog_hh_code.m4
@@ -294,6 +294,13 @@ m4_define(`ppl_@CLASS@_@BINOP@_code',
 
 ')
 
+m4_define(`ppl_@CLASS@_positive_time_elapse_assign_code',
+  `extern "C" Prolog_foreign_return_type
+  ppl_@CLASS@_positive_time_elapse_assign
+  (Prolog_term_ref t_lhs, Prolog_term_ref t_rhs);
+
+')
+
 m4_define(`ppl_@CLASS@_simplify_using_context_assign_code',
   `extern "C" Prolog_foreign_return_type
   ppl_@CLASS@_simplify_using_context_assign
diff --git a/interfaces/ppl_interface_generator_common_procedure_generators.m4 b/interfaces/ppl_interface_generator_common_procedure_generators.m4
index 47f528233..d6c4e286f 100644
--- a/interfaces/ppl_interface_generator_common_procedure_generators.m4
+++ b/interfaces/ppl_interface_generator_common_procedure_generators.m4
@@ -75,6 +75,7 @@ ppl_@CLASS@_add_@CLASS_REPRESENT@s/2 *nofail +all,
 ppl_@CLASS@_refine_with_@REFINE_REPRESENT@/2 *nofail +all,
 ppl_@CLASS@_refine_with_@REFINE_REPRESENT@s/2 *nofail +all,
 ppl_@CLASS@_@BINOP@/2 *nofail +all,
+ppl_@CLASS@_positive_time_elapse_assign/2 *nofail +polyhedron,
 ppl_@CLASS@_@UB_EXACT@/2 +all,
 ppl_@CLASS@_simplify_using_context_assign/3 +simple_pps,
 ppl_@CLASS@_constrains/2 +all,
diff --git a/src/C_Polyhedron.cc b/src/C_Polyhedron.cc
index 20cfa1422..96717e4ae 100644
--- a/src/C_Polyhedron.cc
+++ b/src/C_Polyhedron.cc
@@ -98,3 +98,12 @@ PPL::C_Polyhedron::poly_hull_assign_if_exact(const C_Polyhedron& y) {
 #undef USE_BHZ09
 #undef USE_BFT00
 }
+
+
+void
+PPL::C_Polyhedron::positive_time_elapse_assign(const Polyhedron& y) {
+  NNC_Polyhedron nnc_this(*this);
+  nnc_this.positive_time_elapse_assign(y);
+  *this = nnc_this;
+}
+
diff --git a/src/C_Polyhedron_defs.hh b/src/C_Polyhedron_defs.hh
index 022c7df8a..4dc2fc9dc 100644
--- a/src/C_Polyhedron_defs.hh
+++ b/src/C_Polyhedron_defs.hh
@@ -273,6 +273,17 @@ public:
 
   //! Same as poly_hull_assign_if_exact(y).
   bool upper_bound_assign_if_exact(const C_Polyhedron& y);
+
+  /*! \brief
+    Assigns to \p *this the smallest C polyhedron containing the
+    result of computing the
+    \ref Positive_Time_Elapse_Operator "positive time-elapse"
+    between \p *this and \p y.
+
+    \exception std::invalid_argument
+    Thrown if \p *this and \p y are dimension-incompatible.
+  */
+  void positive_time_elapse_assign(const Polyhedron& y);
 };
 
 #include "C_Polyhedron_inlines.hh"
diff --git a/src/NNC_Polyhedron.cc b/src/NNC_Polyhedron.cc
index 7db5270a4..65fb42191 100644
--- a/src/NNC_Polyhedron.cc
+++ b/src/NNC_Polyhedron.cc
@@ -86,8 +86,3 @@ PPL::NNC_Polyhedron::poly_hull_assign_if_exact(const NNC_Polyhedron& y) {
 #endif
 #undef USE_BHZ09
 }
-
-void
-PPL::NNC_Polyhedron::positive_time_elapse_assign(const Polyhedron& y) {
-  Polyhedron::positive_time_elapse_assign(y);
-}
diff --git a/src/NNC_Polyhedron_defs.hh b/src/NNC_Polyhedron_defs.hh
index 3eefffd1e..bf8caf225 100644
--- a/src/NNC_Polyhedron_defs.hh
+++ b/src/NNC_Polyhedron_defs.hh
@@ -251,8 +251,10 @@ public:
   bool upper_bound_assign_if_exact(const NNC_Polyhedron& y);
 
   /*! \brief
-    Assigns to \p *this the result of computing the
-    "positive time-elapse" between \p *this and \p y.
+    Assigns to \p *this (the best approximation of) the result of
+    computing the
+    \ref Positive_Time_Elapse_Operator "positive time-elapse"
+    between \p *this and \p y.
 
     \exception std::invalid_argument
     Thrown if \p *this and \p y are dimension-incompatible.
diff --git a/src/NNC_Polyhedron_inlines.hh b/src/NNC_Polyhedron_inlines.hh
index 3ef89ad6d..7e19c3411 100644
--- a/src/NNC_Polyhedron_inlines.hh
+++ b/src/NNC_Polyhedron_inlines.hh
@@ -148,6 +148,11 @@ NNC_Polyhedron::upper_bound_assign_if_exact(const NNC_Polyhedron& y) {
   return poly_hull_assign_if_exact(y);
 }
 
+inline void
+NNC_Polyhedron::positive_time_elapse_assign(const Polyhedron& y) {
+  Polyhedron::positive_time_elapse_assign_impl(y);
+}
+
 } // namespace Parma_Polyhedra_Library
 
 #endif // !defined(PPL_NNC_Polyhedron_inlines_hh)
diff --git a/src/Polyhedron_defs.hh b/src/Polyhedron_defs.hh
index f5fbd4984..ecc2bc6cd 100644
--- a/src/Polyhedron_defs.hh
+++ b/src/Polyhedron_defs.hh
@@ -1554,6 +1554,17 @@ public:
   void time_elapse_assign(const Polyhedron& y);
 
   /*! \brief
+    Assigns to \p *this (the best approximation of) the result of
+    computing the
+    \ref Positive_Time_Elapse_Operator "positive time-elapse"
+    between \p *this and \p y.
+
+    \exception std::invalid_argument
+    Thrown if \p *this and \p y are dimension-incompatible.
+  */
+  void positive_time_elapse_assign(const Polyhedron& y);
+
+  /*! \brief
     \ref Wrapping_Operator "Wraps" the specified dimensions of the
     vector space.
 
@@ -2832,13 +2843,13 @@ protected:
                                        const Row2& eq);
 
   /*! \brief
-    Assigns to \p *this the result of computing the
+    Assuming \p *this is NNC, assigns to \p *this the result of the
     "positive time-elapse" between \p *this and \p y.
 
     \exception std::invalid_argument
     Thrown if \p *this and \p y are dimension-incompatible.
   */
-  void positive_time_elapse_assign(const Polyhedron& y);
+  void positive_time_elapse_assign_impl(const Polyhedron& y);
 };
 
 #include "Ph_Status_inlines.hh"
diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc
index 827d04933..8d455cb52 100644
--- a/src/Polyhedron_nonpublic.cc
+++ b/src/Polyhedron_nonpublic.cc
@@ -2215,7 +2215,7 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* vars_p,
 }
 
 void
-PPL::Polyhedron::positive_time_elapse_assign(const Polyhedron& y) {
+PPL::Polyhedron::positive_time_elapse_assign_impl(const Polyhedron& y) {
   // Private method: the caller must ensure the following.
   PPL_ASSERT(!is_necessarily_closed());