Updated to PPLite 0.11.

Now the Apron wrapper for PPLite requires a C++11 compiler
(while the PPLite library itself requires C++17).

COPYING

@@ -29,6 +29,10 @@ of the original package are not covered by the License described in this
 file. They are distributed under the GNU General Public License version 2,
 included in the COPYING file contained in those subdirectories.
 
+The files contained in the pplite subdirectory of the original package
+are not covered by the License described in this file. They are distributed
+under the GNU General Public License version 3, included in the COPYING
+file contained in those subdirectories.
 
 ----------------------------------------------------------------------
 

Makefile.config.model

@@ -171,9 +171,10 @@ CXXFLAGS_DEBUG = \
 -Wno-unused -Wno-unused-parameter -Wno-unused-function \
 -fPIC -g -O0 -UNDEBUG
 
-# PPLite requires using the C++17 language standard
-PPLITE_CXXFLAGS = -std=c++17 $CXXFLAGS
-PPLITE_CXXFLAGS_DEBUG = -std=c++17 $CXXFLAGS_DEBUG
+# The PPLite wrapper requires using the C++11 language standard
+# (note: building PPLite from sources requires the C++17 language standard)
+PPLITE_CXXFLAGS = -std=c++11 $CXXFLAGS
+PPLITE_CXXFLAGS_DEBUG = -std=c++11 $CXXFLAGS_DEBUG
 
 
 AR = ar

README.md

@@ -51,10 +51,12 @@ Compiling the built-in domains with the C interface requires:
 Compiling the PPL-based domains requires the [Parma Polyhedra Library](http://bugseng.com/products/ppl) (tested with version 1.2) and gcc (no clang).
 
 Compiling the PPLite-based domains requires the
-[PPLite library](https://github.com/ezaffanella/PPLite)
-(tested with version 0.10.1), which also depends on Flint.
-Note that the library and its wrapper require using a C++ compiler
-(g++ or clang++) supporting the c++17 language standard.
+[PPLite library](https://github.com/ezaffanella/PPLite),
+which also depends on Flint.
+Note that building the PPLite library from sources requires using a
+C++ compiler (g++ or clang++) that supports the c++17 language standard;
+however, starting from PPLite version 0.11, the Apron wrapper for PPLite
+can be compiled using a C++ compiler supporting the c++11 language standard.
 
 
 ### Additional language support

configure

@@ -422,7 +422,7 @@ then
         has_pplite=0;
     else
         if test "x$pplite_prefix" != "x"; then PPLITE_PREFIX="$pplite_prefix"; fi
-        checkprefix "$cxx $cxxflags -std=c++17" pplite/globals.hh pplite "$PPLITE_PREFIX"
+        checkprefix "$cxx $cxxflags -std=c++11" pplite/globals.hh pplite "$PPLITE_PREFIX"
         if test $? -eq 0; then has_pplite=0; fi
         pplite_prefix="$prefix"
     fi
@@ -652,9 +652,9 @@ CXX = $cxx
 CXXFLAGS = -U__STRICT_ANSI__ -DNDEBUG -O3 $cxxflags
 CXXFLAGS_DEBUG = -U__STRICT_ANSI__ -UNDEBUG -O0 -g $cxxflags
 
-# PPLite requires using the C++17 language standard
-PPLITE_CXXFLAGS = -std=c++17 -DNDEBUG -O3 $cxxflags
-PPLITE_CXXFLAGS_DEBUG = -std=c++17 -UNDEBUG -O0 -g $cxxflags
+# The PPLite wrapper requires using the C++11 language standard
+PPLITE_CXXFLAGS = -std=c++11 -DNDEBUG -O3 $cxxflags
+PPLITE_CXXFLAGS_DEBUG = -std=c++11 -UNDEBUG -O0 -g $cxxflags
 
 EXT_DLL = $ext_dll
 

pplite/README

@@ -14,8 +14,8 @@ This package is a wrapper for the PPLite library
 Requirements:
 - APRON
 - ITV
-- PPLite library version 0.10 (to be installed from sources)
-- Flint and GMPXX (the latter normally installed with GMP)
+- PPLite library version 0.11 (to be installed from sources)
+- Flint, MPFR and GMPXX (the latter normally installed with GMP)
 - for apron_pplite_test: NewPolka APRON module
 
 If HAS_PPLITE is defined in ../Makefile.config, then the main APRON Makefile
@@ -33,7 +33,7 @@ What is provided:
 - flag_exact and flag_best are correcty sets
 - all the widenings are available through the algorithm parameter
 - some functions not availble in PPLite are emulated
-- a unit testing program apron_pplite_test for regression testing;
+- a unit testing program ap_pplite_test for regression testing;
   it works by comparing the result of PPLite and NewPolka
   on random polyhedra
 

pplite/pplite_poly.cc

@@ -24,8 +24,6 @@
 namespace pplite {
 namespace apron {
 
-static const char* PPLITE_VERSION = "0.10.1";
-
 /* Internal structure in managers */
 struct pplite_internal {
   using Abs_Poly = dynamic::Abs_Poly;
@@ -513,7 +511,9 @@ ap_pplite_poly_sat_lincons(ap_manager_t* man, pplite_poly* a,
       return false;
     }
     if (not itv_lincons_is_quasilinear(&lincons)) {
-      auto [empty, env] = to_itv_array(a);
+      auto p = to_itv_array(a);
+      bool empty = p.first;
+      const auto& env = p.second;
       if (empty) {
         assert(env == nullptr);
         // found empty after integral refinement
@@ -807,7 +807,9 @@ ap_pplite_poly_meet_lincons_array(ap_manager_t* man,
     bool exact = itv_lincons_array_set_ap_lincons0_array(intern->itv,
                                                          &array2, array);
     if (not itv_lincons_array_is_quasilinear(&array2)) {
-      auto [empty, env] = to_itv_array(a);
+      auto p = to_itv_array(a);
+      bool empty = p.first;
+      const auto& env = p.second;
       if (empty) {
         assert(env == nullptr);
         // found empty after refining integral bounds
@@ -1438,7 +1440,7 @@ ap_pplite_manager_alloc(bool strict) {
   const char* name = (strict ?
                       "PPLite polyhedra, strict mode" :
                       "PPLite polyhedra, loose mode");
-  ap_manager_t* man = ap_manager_alloc(name, PPLITE_VERSION,
+  ap_manager_t* man = ap_manager_alloc(name, PPLITE_PACKAGE_VERSION,
                                        intern, &ap_pplite_internal_free);
   assert(man);