Example

In [1]: r=declare_ring([Block("x",10),Block("y",10)],globals())

In [2]: x(0)>x(1)
Out[2]: True

In [3]: x(0)>x(1)*x(2)
Out[3]: True

In [4]: change_ordering(dlex)

In [5]: x(0)>x(1)
Out[5]: True

In [6]: x(0)>x(1)*x(2)
Out[6]: False

In [7]: change_ordering(dp_asc)

In [8]: x(0)>x(1)
Out[8]: False

In [9]: x(0)>x(1)*x(2)
Out[9]: False

In [10]: change_ordering(block_dlex)

In [11]: append_ring_block(10)

In [12]: x(0)>x(1)
Out[12]: True

In [13]: x(0)>x(1)*x(2)
Out[13]: False

In [14]: x(0)>y(0)*y(1)*y(2)
Out[14]: True

In [15]: change_ordering(block_dp_asc)

In [16]: x(0)>x(1)
Out[16]: False

In [17]: x(0)>y(0)
Out[17]: False

In [18]: x(0)>x(1)*x(2)
Out[18]: False

In [19]: append_ring_block(10)

In [20]: x(0)>y(0)
Out[20]: True

In [21]: x(0)>y(0)*y(1)
Out[21]: True
In this example, we have an ordering composed of two blocks, the first with ten variables, the second contains the rest of variables $ y(0), \ldots y(9)$ (per default indices start at 0).

Even, if there is a natural block structure, like in this example, we have to explicit call append_ring_block in a block ordering to set the start indices of these blocks.

This can be simplified using the variable block_start_hints created by our ring declaration.

In [1]: declare_ring([Block("x",2),Block("y",3),Block("z",2)],globals())
Out[1]: <polybori.dynamic.PyPolyBoRi.Ring object at 0x1848b10>

In [2]: change_ordering(block_dp_asc)

In [3]: for b in block_start_hints:
   ...:     append_ring_block(b)
   ...:     
   ...:     

In [4]: block_start_hints
Out[4]: [2, 5]

Another important feature in POLYBORI is the ability to iterate over a polynomial in the current monomial ordering.

In [1]: r=declare_ring([Block("x",10),Block("y",10)],globals())

In [2]: f=x(0)+x(1)*x(2)+x(2)

In [3]: for t in f.terms():
   print t
   
x(0)
x(1)*x(2)
x(2)

In [4]: change_ordering(dp_asc)

In [5]: for t in f.terms():
    print t

x(1)*x(2)
x(2)
x(0)
This is a nontrivial functionality, as the natural order of paths in ZDDs is lexicographical.



2010-09-29