[PPL-devel] PPL for linear expression comparison and constraint derivation

[Roberto Bagnara]

On 09/19/14 18:56, Aleksandra Jovanovic wrote:
> I am interested in starting to use Parma Polyhedra library for my research. 
> I do have a specific problem and I would like to check whether PPL could be 
> used for solving.
> 
> I need to compare two linear expression and derive the necessary constraints on the variables 
> such that one of them is minimum/maximum. 
> For example, what should be the relation between x, a and b such that 3x+a+5b is smaller than 
> x+5a+3b (just an example I haven’t paid attention to the actually numbers). Are there functions in PPL 
> that I could use to solve this?

Dear Alexandra,

does the following answer your question?

$ cat p.cc
#include <ppl.hh>

using namespace std;
using namespace Parma_Polyhedra_Library;
using namespace Parma_Polyhedra_Library::IO_Operators;

int main() {
  NNC_Polyhedron ph(3);
  Variable A(0);
  Variable B(1);
  Variable C(2);
  ph.add_constraint(3*A + B + 5*C < A + 5*B + 3*C);
  cout << ph.minimized_constraints() << endl;
  return 0;
}
$ g++ -W -Wall p.cc -lppl -lgmpxx -lgmp
$ a.out
-A + 2*B - C > 0
$

Note that I interpreted "smaller" as "strictly smaller".
If strict constraints are not required, using C_Polyhedron
instead of NNC_Polyhedron will be more efficient.
Please do not hesitate to come back to us (by writing
to ppl-devel at cs.unipr.it) if I misinterpreted your question
or you need more information.
Kind regards,

   Roberto

-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com