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
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.