Expand CNF using encoding back-end

[hbierlee]

This PR expands the to_cnf function to all CPMpy models (insofar supported by other Boolean solvers). It does so by passing all constraints through pindakaas transform and encoding, and reading the Pindakaas encoding object back to CPMpy.

TODO

• constraints which are only clauses do not have to pass through pindakaas

[hbierlee]

Ready to be reviewed. Outstanding issues and my reasons for not resolving them:

• The to_cnf now requires the pindakaas back-end, even though it is only used to encode non-clausal constraints (i.e. integer/pb constraints). We could try to make this optional, so that Boolean models can be encoded w/o installing pindakaas, but since the install is so easy, and it's hard to predict when non-clausal constrains arise during transformation, so I think we should just encourage users to install the dependency.
• Note that in the write_dimacs test, the order of clauses can be slightly unexpected, because of an optimization in to_cnf which puts simple clauses before encoded constraints (e.g. sums). I don't think this is worth fixing. The CNF ordering of clauses (or lits in clauses) is not guaranteed in general, even though it's a bit painful to look at (for me).
• There are some linearization optimizations and fixes which should be made (supporting BV*BV=1, some other sub-optimal linearizations which should remain clauses). But this is a new, general transformation improving PR.

[tias]

yes, I think that this is the right way.

I see that you change the signature of to_cnf to also return ivarmap, which I would like to avoid.

I don't think the solver 'copies' the ivarmap when you give it to it; which would mean that the ivarmap given by the function caller might be updated when the function returns, hence not needing to return ivarmap. Can you check that?

[hbierlee]

ah, yeah, actually, of course we do not need to return it. If you need it, you should just also be in charge of creating the ivarmap and passing it along.

[IgnaceBleukx]

A solution to this would be to compare sets of lines, which is basically what we want for this tool anyway
E.g.

gt_clauses = set(gt_cnf.split("\n")[1:])
txt_clauses = set(cnf_txt.split("\n")[1:])
self.assertSetEqual(gt_clauses, txt_clauses)