[PPL-devel] [GIT] ppl/ppl(pip): Exploit variable integrality when creating tautology constraints.

[Enea Zaffanella]

Module: ppl/ppl
Branch: pip
Commit: 0e4098c48d6fe9daae9d405112df1aac7ed66742
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0e4098c48d6fe9daae9d405112df1aac7ed66742

Author: Enea Zaffanella <zaffanella at cs.unipr.it>
Date:   Thu Feb 10 10:46:03 2011 +0100

Exploit variable integrality when creating tautology constraints.
Factored out helper function
  void integral_simplification(Row&);
used when generating tautology and sign splitting constraints.

---

 src/PIP_Tree.cc |   67 ++++++++++++++++++++++++++++++------------------------
 1 files changed, 37 insertions(+), 30 deletions(-)

diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc
index 1a21047..38a30e5 100644
--- a/src/PIP_Tree.cc
+++ b/src/PIP_Tree.cc
@@ -488,6 +488,33 @@ gcd_assign_iter(Coefficient& gcd, Iter first, Iter last) {
   }
 }
 
+// Simplify row by exploiting variable integrality.
+void
+integral_simplification(Row& row) {
+  if (row[0] != 0) {
+    Row::const_iterator j_begin = row.begin();
+    Row::const_iterator j_end = row.end();
+    PPL_ASSERT(j_begin != j_end && j_begin.index() == 0 && *j_begin != 0);
+    /* Find next column with a non-zero value (there should be one). */
+    ++j_begin;
+    PPL_ASSERT(j_begin != j_end);
+    for ( ; *j_begin == 0; ++j_begin)
+      PPL_ASSERT(j_begin != j_end);
+    /* Use it to initialize gcd. */
+    PPL_DIRTY_TEMP_COEFFICIENT(gcd);
+    gcd = *j_begin;
+    ++j_begin;
+    gcd_assign_iter(gcd, j_begin, j_end);
+    if (gcd != 1) {
+      PPL_DIRTY_TEMP_COEFFICIENT(mod);
+      pos_mod_assign(mod, row[0], gcd);
+      row[0] -= mod;
+    }
+  }
+  /* Final normalization. */
+  row.normalize();
+}
+
 // Divide all coefficients in row x and denominator y by their GCD.
 void
 row_normalize(Row& x, Coefficient& den) {
@@ -2730,25 +2757,26 @@ PIP_Solution_Node::solve(const PIP_Problem& pip,
       }
 
       if (i_neg != not_a_dim) {
-        Row copy = tableau.t[i_neg];
-        copy.normalize();
-        context.add_row(copy);
-        add_constraint(copy, all_params);
+        Row tautology = tableau.t[i_neg];
+        /* Simplify tautology by exploiting integrality. */
+        integral_simplification(tautology);
+        context.add_row(tautology);
+        add_constraint(tautology, all_params);
         sign[i_neg] = POSITIVE;
 #ifdef NOISY_PIP
         {
-          Linear_Expression expr = Linear_Expression(copy.get(0));
+          Linear_Expression expr = Linear_Expression(tautology.get(0));
           dimension_type j = 1;
           for (Variables_Set::const_iterator p = all_params.begin(),
                  p_end = all_params.end(); p != p_end; ++p, ++j)
-            add_mul_assign(expr, copy.get(j), Variable(*p));
-          Constraint tautology(expr >= 0);
+            add_mul_assign(expr, tautology.get(j), Variable(*p));
           using namespace IO_Operators;
           std::cerr << std::setw(2 * indent_level) << ""
                     << "Row " << i_neg
                     << ": mixed param sign, negative var coeffs\n";
           std::cerr << std::setw(2 * indent_level) << ""
-                    << "==> adding tautology: " << tautology << ".\n";
+                    << "==> adding tautology: "
+                    << Constraint(expr >= 0) << ".\n";
         }
 #endif // #ifdef NOISY_PIP
         // Jump to next iteration.
@@ -2776,28 +2804,7 @@ PIP_Solution_Node::solve(const PIP_Problem& pip,
 
       Row t_test(tableau.t[best_i]);
       /* Simplify t_test by exploiting integrality. */
-      if (t_test[0] != 0) {
-        Row::const_iterator j_begin = t_test.begin();
-        Row::const_iterator j_end = t_test.end();
-        PPL_ASSERT(j_begin != j_end && j_begin.index() == 0 && *j_begin != 0);
-        /* Find next column with a non-zero value (there should be one). */
-        ++j_begin;
-        PPL_ASSERT(j_begin != j_end);
-        for ( ; *j_begin == 0; ++j_begin)
-          PPL_ASSERT(j_begin != j_end);
-        /* Use it to initialize gcd. */
-        PPL_DIRTY_TEMP_COEFFICIENT(gcd);
-        gcd = *j_begin;
-        ++j_begin;
-        gcd_assign_iter(gcd, j_begin, j_end);
-        if (gcd != 1) {
-          PPL_DIRTY_TEMP_COEFFICIENT(mod);
-          pos_mod_assign(mod, t_test[0], gcd);
-          t_test[0] -= mod;
-        }
-      }
-      /* Normalize t_test. */
-      t_test.normalize();
+      integral_simplification(t_test);
 
 #ifdef NOISY_PIP
       {