Linearizing reified variables for solver without ivarmap duplicates domain constraints if called multiple times

[hbierlee]

As discussed internally, we'll have a different issue for non-ivarmap solvers where the problem remain.

However, for solvers without ivarmap, it is created each function call, so there the issue likely remains. I think for those solvers, they should also just have an ivarmap if we're going to do any int2bool powered rewriting. I'm setting this PR as ready, since that issue should probably be a different PR.

Originally posted by @hbierlee in #860 (comment)

[hbierlee]

A test to show the problem, in fact, the channelling constraint is also duplicated.

========================================================= FAILURES ==========================================================
_______ TestLinearizeReifiedVariablesThreshold.test_linearize_reified_variables_over_multiple_constraints_no_ivarmap ________

self = <test_trans_linearize.TestLinearizeReifiedVariablesThreshold object at 0xffff7ce229f0>

    def test_linearize_reified_variables_over_multiple_constraints_no_ivarmap(self):
        """With min_values=2, (a==1)|(a==2) is replaced, no channel constraint."""
    
        a = self.a
        out = []
        for con in [(a == 1) | (a == 2), (a == 3) | (a == 2)]:
            cpm_cons = toplevel_list(con)
            cpm_cons = flatten_constraint(con, csemap=self.csemap)
            out += linearize_reified_variables(cpm_cons, min_values=2, csemap=self.csemap)
    
>       assert str(out) == "[(BV[a == 1]) or (BV[a == 2]), sum([BV[a == 1], BV[a == 2], BV[a == 3]]) == 1, sum([1, 0, -1, -2]
 * [a, BV[a == 1], BV[a == 2], BV[a == 3]]) == 1, (BV[a == 3]) or (BV[a == 2])"
E       AssertionError: assert '[(BV[a == 1]...== 3]]) == 1]' == '[(BV[a == 1]... (BV[a == 2])'
E         
E         Skipping 164 identical leading characters in diff, use -v to show
E         - BV[a == 2])
E         + BV[a == 2]), sum([BV[a == 1], BV[a == 2], BV[a == 3]]) == 1, sum([1, 0, -1, -2] * [a, BV[a == 1], BV[a == 2], BV[
a == 3]]) == 1]

tests/test_trans_linearize.py:645: AssertionError