SAT to solve `restrict` calls

[rw]

Is there a way to use the included SAT solver as an alternative to using the restrict function? I am finding restrict too slow when evaluating 64-bit brent_kung_add instances. (I'm a new user to the library, so this question may be demonstrating a misunderstanding of how to use it.)

[cjdrake]

You might run into difficulties with that approach. First, SAT is NP-complete, so there are cases where the runtime will be very high. Second, it will not give you a new expression, but rather a solution point, which you will have to reconstruct into a DNF or CNF.