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]: TrueIn this example, we have an ordering composed of two blocks, the first with ten variables, the second contains the rest of variables
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.