Bug Fixes : 4851 4858 4880 for nsatz

the function in_ideal of ideal.ml supposes the list of polynomials
does not contain zero and is duplicate free.
I force this invariant in the call of in_ideal in nsatz.ml4

the function clean_pol returns the reduced list plus a list of
booleans that indicates which polynomials have been deleted

the function expand_pol translates back the certificate of
the reduced to list to the complete list thanks to the list
of booleans.

The fix is quadratic with respect to the input list which should
be ok for reasonable usage of nsatz.
If there is some performance issue we could improve the in_pol
function.

0 files changed, 0 insertions, 0 deletions