[PPL-devel] Fwd: Question regarding OCaml Interface of PPL

[Enea Zaffanella]

Hello Brian.

Sorry for the noise of the previous answer, I just stumbled on the 
"Send" button by mistake.

On 03/07/2012 09:08 AM, Enea Zaffanella wrote:
> On 03/06/2012 09:33 PM, Roberto Bagnara wrote:
>>
>>
>> -------- Original Message --------
>> Subject: Question regarding OCaml Interface of PPL
>> Date: Tue, 6 Mar 2012 13:49:10 -0500
>> From: Brian Pak <bpak at andrew.cmu.edu>
>> To: support at bugseng.com
>>
>> Hi all,
>>
>> I'm a student in Carnegie Mellon University in US, and trying to use PPL
>> for my research project.
>>
>> First, thank you for your great work! It is truly amazing :)
>
>
>
>> I was fiddling with the library and interfaces (especially OCaml), and
>> got stuck on one thing. I wanted to use 'get_interval' or
>> 'get_lower/upper_bound' functions in Box class, but it seems it's not
>> available in OCaml interface. Is there any way to get around this?

You are right, these methods are available in the C++ interface but they 
are not (yet) available in the other languages interfaces.

As a workaround, the same effect can be used by calling methods

   bool maximize(const Linear_Expression& expr,
		Coefficient& sup_n, Coefficient& sup_d,
                 bool& maximum) const;

   bool minimize(const Linear_Expression& expr,
		Coefficient& sup_n, Coefficient& sup_d,
                 bool& minimum) const;

passing in a linear expression expressing the space dimension of 
interest as argument `expr' (which is the objective function).
These are available in the OCaml interface:

val ppl_Z_Box_maximize :
z_box ->
linear_expression -> bool * Gmp.Z.t * Gmp.Z.t * bool
val ppl_Z_Box_minimize :
z_box ->
linear_expression -> bool * Gmp.Z.t * Gmp.Z.t * bool


>> I'm not too familiar with these mathematical concepts (I'm reading
>> materials to grasp better understanding, though), but here's what I want
>> to accomplish:
>> - Given n variables where each of them is bounded (in some linear
>> relation) -- build a constraint system out of these
>> - Generate an n-polytope that above equations describe (currently
>> planning to use C_Polyhedron)

This sounds ok.

>> - I want to enumerate integer points in this polytope, but that's known
>> to be difficult (please correct me if I'm wrong)

You are right, unless the constraints you are using satisfy special 
properties (e.g., bounded differences or octagonal shapes).

>> - Create an n-dimensional Box object from C_Polyhedron we generated
>> (which is basically a hyper-rectangle surrounding the polytope,
>> possibly?)

Yes. In principle this can be done even for unbounded polyhedra: you 
will obtain an hyper-rectangle which is unbounded in some directions.
But I understand you are only interested in polytopes (so as to obtain a 
finite number of integral points).

>> - Get the interval (low and upper bound) for each variable for the Box
>> above.
>> - Pick a random point in the Box (hopefully this is easier since we know
>> the interval of each dimension)

Ok.

As said above, you can use the maximize/minimize functions as workarounds.

>> - Perform a rejection sampling to check if the picked point is contained
>> in the polytope.
>> - There doesn't seem to be a way to do this natively, so I'm planning to
>> use the trick where I make a very small polytope that is constrained by
>> Variable(0) == c_1 && Variable(1) == c_2 && … && Variable(n-1) == c_n,
>> and use 'contains' function to check if it's contained in the polytope
>> (represented by C_Polyhedron object above).

There actually is native support for checking if a point is included in 
a C_Polyhedron. The point needs to be (actually, it is more easily) 
expressed as a Generator and then you can use C_Polyhedron method

Poly_Gen_Relation relation_with (const Generator &g) const
  	Returns the relations holding between the polyhedron *this and the 
generator g.

If the returned value is Poly_Gen_Relation::subsumes(), then the point 
is included in the polyhedron.

In the OCaml interface the corresponding function is:

   ppl_Polyhedron_relation_with_generator handle generator

and we have

type poly_gen_relation = Subsumes


Hoping this will be helpful.

Enea.

>>
>> Thanks for your help in advance! :D
>> -Brian
>> _______________________________________________
>> PPL-devel mailing list
>> PPL-devel at cs.unipr.it
>> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
>>
>
> _______________________________________________
> PPL-devel mailing list
> PPL-devel at cs.unipr.it
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
>