BV primitives

[bclement-ocp]

Add support for the SMT-LIB2 Bit-Vector primitives.
Features:

• Support for the all the SMT-LIB2 Bit-Vector primitives
• Fix the bugs that are present in older versions:
  • Assertion failure in "src/lib/reasoners/bitv.ml", line 538 #645
  • Assertion failure in "src/lib/reasoners/bitv.ml", line 569 #649
  • Unsoundness with bit-vectors. #664
• Don't fully expand bv2nat (maybe nat2bv too?) right away
• Remove the Canonizer in "bitv.ml", build simple-terms straight away and use only simple terms internally.
• Update website documentation Add documentation for new features #648

[bclement-ocp]

Regarding the 3rd point, I am not sure we want to do this, at least for 2.5.0

I believe going through the canonizer allows to avoid work in some complex cases; for instance consider (complex_expression @ [|0|]) ^ {1, 1} where complex_expression has a lot of concat / extract etc. If we go through the canonizer, we can avoid some of the work required to parse the complex_expression. If we remove the canonizer and only use simple terms, we will do a lot of computation and simplifications inside the complex_expression that will ultimately be thrown away.

Note that we don't avoid all the work required to parse the complex_expression (because we still make the term → canonizer translation). We could avoid this by making the canonizer lazy somehow (either with a constructor I_Term of E.t that gets "forced" when needed — or with actual Lazy.t).

[hra687261]

I believe going through the canonizer allows to avoid work in some complex cases

From what I understand of the code, the make_rec function in the Canonizer goes through the entire complex_expression building the entire combination of I_Comp and I_Ext which will be only applied once the sigma function is called.
By removing the canonizer and producing simple_terms right away, that intermediary state with I_Comps and I_Exts will be skipped and we will produce simple terms right away.
With (complex_expression @ [|0|]) ^ {0, 0}:
Instead of producing I_Ext (I_Comp (make_rec complex_expression, make_rec [|0|]), 0, 0, 1) then applying the sigma function on it (which will go through the entire thing to apply the concatenations and extractions), we would just produce make_rec [|0|] because the extraction will be applied right away to produce simple terms.
The bounds of extractions will be passed down and applied as soon as possible, the only case in which they won't and in which they'll produce simple terms (Ext _) is when they come across a variable over which the extraction can't be applied anyway.

[bclement-ocp]

Ah, right, the canonizer AST currently does not record information about the size of the vectors.

The way I see it, there are two ways we can do these simplifications:

1. Inside the theory, in which case there should be a dedicated mini-AST rather than using Expr.t (e.g. extend the canonizer ast with size information)
2. Outside the theory with smart constructors in Expr
3. Outside the theory (or at the theory boundary) in a simplification pass

I have a slight preference for 1. (partly because we can rely on the compiler a bit more for pattern matching exhaustiveness), which is the current approach with the canonizer, but I'd be fine with 3. 2 I think is problematic because it can have adverse effect on triggers (it can break syntactic triggers, and we are not well equipped for that, see e.g. the issues we had with arith simplifications).

I think you are more or less doing 3. already from a quick skim of the current state of the PR, so maybe we can get rid of the canonizer at the same time in that case.

[bclement-ocp]

I see you have checked " Support for the all the SMT-LIB2 Bit-Vector primitives" does that mean that #669 is ready for review?

[hra687261]

I guess the task is not specific enough, does support all the BV primitives of the SMT-LIB? Yes
But since the PR is still a draft, then it's not really ready, I haven't switched to the not-full expansion of bv2nat, I'm working on it rn and I'll mark as ready for review once that is done.
I've started an attempt for the 3rd task (in a similar way to the fst technique you mentioned), but I'm not sure if I want to add it into this PR or have a separate one, it might make things too complex for a single PR.

[bclement-ocp]

I think it's fine to go step by step and have the non-expanded version of bv2nat first then expand it in another PR (I prefer smaller PRs personally), but if you want to do it all in one go it's OK as well; I thought that PR was specifically for the 1st task which is why I asked.

Ideally removing the canonizer should be in a separate PR, unless it is needed for the rest. If it's not needed for the rest, I am also not convinced we want that 3rd task for 2.5.0, it's not part of our engagements (it's an implementation detail) and we are already late for the release.

[hra687261]

It's not needed for the rest, I guess we can review this one then.
I'll open two separate PRs for the non-expanded version of bv2nat and for removal of the canonizer.
Although, since the removal of the canonizer was planned, some function do a few too many conversions from terms to simple_terms and vice-versa, which is not great.

[bclement-ocp]

To clarify, I am not against including it in 2.5.0 if it happens to be ready on time, but it should not block/slow down PRs that do need to be in 2.5.0

[bclement-ocp]

Doc update is tracked in part of #648