Sharing equivalent sub-expressions independent of their StableName

[bruderj15]

As pointed out in https://github.com/bruderj15/Hasmtlib/issues/43#issuecomment-2289023488, one can go way further than implementing observable sharing just by StableNames we did with v3.4.0.

One could check expressions for equivalence. Even better: Beforehand, reduce to some self-defined (maybe there are even some defined already, check literature) normalform and compare this.

This indeed sounds like it will enable a whole lot more sharing. While this also poses a greater runtime-cost, it may be beneficial for solver-performance in medium-hard problems. Evaluation needed to confirm.

This does not mean to replace the existing implementation for the sharing. Just add some SharingMode, default to sharing by StableName and allow user to change it:

data SharingMode = None | StableName | Equivalence
instance Default SharingMode where
  def = StableName

setSharingMode :: MonadSMT s m => SharingMode -> m ()

[bruderj15]

May use #113 for sharing if solvers actually uses it to share.