Add LetBinder to bv_values

[N1ark]

Opening this because the change was in a branch that was rotting; adds LetBinder to bv_values/encoder.ml, which handles creating let-binds for values before encoding them to the solver.

The algorithm, given a value v, min_occurrences and min_binds

1. Count occurrences of each non-atomic occurrence in a value -> count map
2. Only keep bindings where the count >= min_occurrences
3. If the size of the map is < min_binds, return v
4. Generate the early bindings: for each bound value,
   • replace all other bound values within it with a variable associated to it
   • keep track of its encoded form, and its dependencies (ie. all mentioned variables within it)
5. Check the already-known variables of v (ie. externally defined ones)
6. Recursively generate binding groups; ie sets of bindings that do not refer to each other, resulting in (string, sexp) list list; each inner list is a group, and all groups should be defined in order
7. Actually replace the bindings in v, return it
   Then one can encode v, and wrap it in the let-binds, using LetBinder.apply_bindings

I would like to make this a functor or part of the behaviour of solvers, so that it can be shared, but it would require exposing quite a few functions that seem too specific to be worth requiring:

• Value.map_if : f:(t -> t option) -> t -> t, which recursively tries replacing values if f v is Some
• Value.hash : t -> int (tbh this is chill)
• Value.is_atom : t -> bool or something like Value.can_bind : t -> bool; basically a function to ensure atoms aren't let-bound since that's pointless

If you think this is worth pursuing I'm happy to add it; we can keep this as draft otherwise.

Example of output encoding (notice the |208|, |252|, |282|, |342| and |297|)

(declare-fun |3| () (_ BitVec 8))
(declare-fun |1| () (_ BitVec 32))
(assert
 (let ((|208| ((_ sign_extend 32) |1|)))
  (let ((|252| (bvsub |208| #x0000000000000001)))
   (let
    ((|282| (bvsdiv |252| #x0000000000000064))
     (|342| (bvadd #x000000000000126c |252|)))
    (let ((|297| (bvsub |282| #x0000000000000001)))
     (and (not (= ((_ extract 4 0) |3|) #b00000))
      (= #x00000000 (bvsrem |1| #x00000004))
      (= #x00000000 (bvsrem |1| #x00000064))
      (= #x00000000 (bvsrem |1| #x00000190))
      (bvule ((_ zero_extend 3) ((_ extract 4 0) |3|)) #x1d)
      (not (bvsaddo |208| #xffffffffffffffff))
      (= #b1 ((_ extract 63 63) (bvsrem |252| #x0000000000000064)))
      (not (bvsaddo #x0000000000000002 (bvneg |297|))) (not (bvnego |297|))
      (not
       (bvsaddo (bvsub #x0000000000000002 |297|)
        (bvsdiv |297| #x0000000000000004)))
      (not (bvsaddo |252| #x000000000000126c))
      (not (bvsmulo #x000000000000016d |342|))
      (not
       (bvsaddo (bvmul #x000000000000016d |342|)
        (bvsdiv |342| #x0000000000000004)))
      (not
       (bvsaddo
        (bvadd (bvmul #x000000000000016d |342|)
         (bvsdiv |342| #x0000000000000004))
        #x00000000000001cb))
      (not
       (bvsaddo
        (bvadd
         (bvadd (bvmul #x000000000000016d |342|)
          (bvsdiv |342| #x0000000000000004))
         #x00000000000001cb)
        ((_ zero_extend 56) ((_ zero_extend 3) ((_ extract 4 0) |3|)))))
      (not
       (bvsaddo
        (bvadd ((_ zero_extend 56) ((_ zero_extend 3) ((_ extract 4 0) |3|)))
         (bvadd
          (bvadd (bvmul #x000000000000016d |342|)
           (bvsdiv |342| #x0000000000000004))
          #x00000000000001cb))
        (bvadd (bvsub #x0000000000000002 |297|)
         (bvsdiv |297| #x0000000000000004))))
      (not
       (bvsaddo
        (bvadd
         (bvadd (bvsub #x0000000000000002 |297|)
          (bvsdiv |297| #x0000000000000004))
         (bvadd
          ((_ zero_extend 56) ((_ zero_extend 3) ((_ extract 4 0) |3|)))
          (bvadd
           (bvadd (bvmul #x000000000000016d |342|)
            (bvsdiv |342| #x0000000000000004))
           #x00000000000001cb)))
        #xffffffffffdabc80))
      (bvsaddo
       (bvsub
        (bvadd
         (bvadd (bvsub #x0000000000000002 |297|)
          (bvsdiv |297| #x0000000000000004))
         (bvadd
          ((_ zero_extend 56) ((_ zero_extend 3) ((_ extract 4 0) |3|)))
          (bvadd
           (bvadd (bvmul #x000000000000016d |342|)
            (bvsdiv |342| #x0000000000000004))
           #x00000000000001cb)))
        #x0000000000254380)
       #x0000000000009e8b)))))))