[PPL-devel] [GIT] ppl/ppl(pip): Implemented some helper functions for the PIP solver.
François Galea
francois.galea at uvsq.fr
Thu Sep 10 16:27:44 CEST 2009
Module: ppl/ppl
Branch: pip
Commit: f6b3b1cf93a95d152d50a2fce5a3211cc8fa891f
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6b3b1cf93a95d152d50a2fce5a3211cc8fa891f
Author: François Galea <francois.galea at uvsq.fr>
Date: Thu Sep 10 15:46:25 2009 +0200
Implemented some helper functions for the PIP solver.
---
src/PIP_Tree.cc | 48 +++++++++++++++++++++++++++++++++++-------------
src/PIP_Tree.defs.hh | 19 +++++++++++--------
2 files changed, 46 insertions(+), 21 deletions(-)
diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc
index db52260..42a903e 100644
--- a/src/PIP_Tree.cc
+++ b/src/PIP_Tree.cc
@@ -23,6 +23,27 @@ site: http://www.cs.unipr.it/ppl/ . */
#include <ppl-config.h>
#include "PIP_Tree.defs.hh"
+namespace PPL = Parma_Polyhedra_Library;
+
+namespace {
+
+// Compute x += c * y
+void
+add_assign(PPL::Row& x, const PPL::Row& y, const PPL::Coefficient &c) {
+ for (PPL::dimension_type i=0; i<x.size(); ++i)
+ x[i] += c * y[i];
+}
+
+// Merge constraint systems such as x = x U z
+void
+merge(PPL::Constraint_System &x, const PPL::Constraint_System &y) {
+ PPL::Constraint_System::const_iterator i;
+ for (i=y.begin(); i!=y.end(); ++i)
+ x.insert(*i);
+}
+
+} // namespace
+
namespace Parma_Polyhedra_Library {
PIP_Decision_Node::~PIP_Decision_Node() {
@@ -99,8 +120,7 @@ PIP_Decision_Node::solve(PIP_Tree_Node **parent_ref,
PIP_Problem_Status stt;
PIP_Problem_Status stf = UNFEASIBLE_PIP_PROBLEM;
Constraint_System context_true(context);
- //FIXME: not implemented yet (merging of constraint systems)
- //context_true.merge(_constraints);
+ merge(context_true, _constraints);
stt = true_child->solve(&true_child, context_true);
if (false_child) {
// Decision nodes with false child must have exactly one constraint
@@ -125,6 +145,12 @@ PIP_Solution_Node::Rational_Matrix::normalize() {
//FIXME
}
+//! Returns the allocated capacity of each Row of the Matrix.
+dimension_type
+PIP_Solution_Node::Rational_Matrix::capacity() {
+ return row_capacity;
+}
+
void
PIP_Solution_Node::Rational_Matrix::ascii_dump(std::ostream& s) const {
s << "denominator " << denominator << "\n";
@@ -177,7 +203,7 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node **parent_ref,
dimension_type first_pending_constraint,
const Constraint_Sequence &input_cs,
const Variables_Set ¶meters) {
- dimension_type i, j;
+ dimension_type i;
dimension_type n_params = parameters.size();
dimension_type n_vars = external_space_dim - n_params;
dimension_type internal_space_dim = tableau.t.num_columns()-1;
@@ -208,8 +234,8 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node **parent_ref,
cst < input_cs.end(); ++cst) {
int v = 0;
int p = 1;
- Row var(n_vars, Row::Flags());
- Row param(n_params+1, Row::Flags());
+ Row var(n_vars, tableau.s.capacity(), Row::Flags());
+ Row param(n_params+1, tableau.t.capacity(), Row::Flags());
Coefficient cnst_term = -cst->inhomogeneous_term();
if (cst->is_strict_inequality())
// convert c > 0 <=> c-1 >= 0
@@ -219,19 +245,15 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node **parent_ref,
if (parameters.count(i) == 1) {
param[p++] = cst->coefficient(Variable(i)) * denom_t;
} else {
- Coefficient c = cst->coefficient(Variable(i)) * denom_s;
+ Coefficient c = cst->coefficient(Variable(i));
dimension_type idx = mapping[v];
if (basis[v])
// Basic variable : add c * x_i
- var[idx] += c;
+ var[idx] += c * denom_s;
else {
// Nonbasic variable : add c * row_i
- const Row &sr = tableau.s[idx];
- const Row &st = tableau.t[idx];
- for (j=0; j<sr.size(); j++)
- var[j] += c*sr[j];
- for (j=0; j<st.size(); j++)
- param[j] += c*st[j];
+ add_assign(var, tableau.s[idx], c);
+ add_assign(param, tableau.t[idx], c);
}
++v;
}
diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh
index 64debe6..f02631a 100644
--- a/src/PIP_Tree.defs.hh
+++ b/src/PIP_Tree.defs.hh
@@ -92,10 +92,10 @@ protected:
/*! \brief
Execute a parametric simplex on the tableau, under specified context.
-
+
\param parent_ref
a pointer to the parent reference to \p this
-
+
\param context
the context, being a set of constraints on the parameters
@@ -132,7 +132,7 @@ public:
/*! \brief
Returns the system of parameter constraints controlling \p *this.
-
+
The column indices in the constraints are numbered from \c 0 to
<tt>np-1</tt>, where \c np is the total number of parameters. They are
ordered with the same order as the parameter indices in the original
@@ -178,6 +178,9 @@ private:
*/
void normalize();
+ //! Returns the allocated capacity of each Row of the Matrix.
+ dimension_type capacity();
+
//! Tests whether the matrix is integer, \e ie. the denominator is 1.
bool is_integer() const;
@@ -254,10 +257,10 @@ protected:
/*! \brief
Execute a parametric simplex on the tableau, under specified context.
-
+
\param parent_ref
a pointer to the parent reference to \p this
-
+
\param context
the context, being a set of constraints on the parameters
@@ -290,7 +293,7 @@ public:
/*! \brief
Returns the system of parameter constraints controlling \p *this.
-
+
The column indices in the constraints are numbered from \c 0 to
<tt>np-1</tt>, where \c np is the total number of parameters. They are
ordered with the same order as the parameter indices in the original
@@ -372,10 +375,10 @@ protected:
/*! \brief
Execute a parametric simplex on the tableau, under specified context.
-
+
\param parent_ref
a pointer to the parent reference to \p this
-
+
\param context
the context, being a set of constraints on the parameters
More information about the PPL-devel
mailing list