ll_red_nf_redsb
/ll_red_nf_noredsb
functions on rewriting systems, where the tails of the polynomials was constant and the leading term linear.
They can be used in a more general setting (which allows to eliminate auxiliary variable).
In particular we can use ll_red_nf_redsb
to speedup substitution of a variable
by a value
also in the more general case, that the lexicographical leading term of
is equal to
.
This can be tested most efficiently by the expression
x.set().navigation().value()>v.set().navigation().value().
In many cases, we have a bigger equation system, where many variables have a linear leading term w.r.t. lexicographical ordering (at least one can optimize the formulation of the equations to fulfill these condition). These systems can be handled by the function eliminate in the module polybori.ll. I returns three results:
In [1]: from polybori.ll import eliminate In [2]: E=[x(1)+1,x(1)+x(2),x(2)+x(3)*x(4)] In [3]: (L,f,R)=eliminate(E) In [4]: L Out[4]: [x(1) + 1, x(2) + x(3)*x(4)] In [5]: R Out[5]: [x(3)*x(4) + 1] In [6]: f(x(1)+x(2)) Out[6]: x(3)*x(4) + 1
2009-10-25